From 161fae584b4019ca472a5657a46bb18486b367e9 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 2 Mar 2017 16:40:39 -0600 Subject: [PATCH] Fixes related to sets. --- src/theory/quantifiers/bounded_integers.cpp | 4 + src/theory/sets/theory_sets_private.cpp | 111 +++++++++++--------- src/theory/sets/theory_sets_private.h | 1 + test/regress/regress0/sets/Makefile.am | 3 +- test/regress/regress0/sets/abt-min.smt2 | 22 ++++ 5 files changed, 91 insertions(+), 50 deletions(-) create mode 100644 test/regress/regress0/sets/abt-min.smt2 diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index 37fbff03a..6b53612d7 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -657,6 +657,10 @@ Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) { if( !sr.isNull() ){ Trace("bound-int-rsi") << "Get value in model for..." << sr << std::endl; sr = d_quantEngine->getModel()->getCurrentModelValue( sr ); + //if non-constant, then sr does not occur in the model, we fail + if( !sr.isConst() ){ + return Node::null(); + } Trace("bound-int-rsi") << "Value is " << sr << std::endl; //as heuristic, map to term model if( sr.getKind()!=EMPTYSET ){ diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index c14ef02b2..5550ee1b0 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -506,6 +506,7 @@ void TheorySetsPrivate::fullEffortCheck(){ d_sentLemma = false; d_addedFact = false; d_set_eqc.clear(); + d_set_eqc_relevant.clear(); d_set_eqc_list.clear(); d_eqc_emptyset.clear(); d_eqc_singleton.clear(); @@ -540,19 +541,24 @@ void TheorySetsPrivate::fullEffortCheck(){ Trace("sets-eqc") << n << " "; } if( n.getKind()==kind::MEMBER ){ - Node s = d_equalityEngine.getRepresentative( n[1] ); - Node x = d_equalityEngine.getRepresentative( n[0] ); - int pindex = eqc==d_true ? 0 : ( eqc==d_false ? 1 : -1 ); - if( pindex!=-1 ){ - if( d_pol_mems[pindex][s].find( x )==d_pol_mems[pindex][s].end() ){ - d_pol_mems[pindex][s][x] = n; - Trace("sets-debug2") << "Membership[" << x << "][" << s << "] : " << n << ", pindex = " << pindex << std::endl; + if( eqc.isConst() ){ + Node s = d_equalityEngine.getRepresentative( n[1] ); + Node x = d_equalityEngine.getRepresentative( n[0] ); + int pindex = eqc==d_true ? 0 : ( eqc==d_false ? 1 : -1 ); + if( pindex!=-1 ){ + if( d_pol_mems[pindex][s].find( x )==d_pol_mems[pindex][s].end() ){ + d_pol_mems[pindex][s][x] = n; + d_set_eqc_relevant[s] = true; + Trace("sets-debug2") << "Membership[" << x << "][" << s << "] : " << n << ", pindex = " << pindex << std::endl; + } + if( d_members_index[s].find( x )==d_members_index[s].end() ){ + d_members_index[s][x] = n; + d_op_list[kind::MEMBER].push_back( n ); + } + }else{ + Assert( false ); } } - if( d_members_index[s].find( x )==d_members_index[s].end() ){ - d_members_index[s][x] = n; - d_op_list[kind::MEMBER].push_back( n ); - } }else if( n.getKind()==kind::SINGLETON || n.getKind()==kind::UNION || n.getKind()==kind::INTERSECTION || n.getKind()==kind::SETMINUS || n.getKind()==kind::EMPTYSET ){ if( n.getKind()==kind::SINGLETON ){ //singleton lemma @@ -570,6 +576,8 @@ void TheorySetsPrivate::fullEffortCheck(){ }else{ Node r1 = d_equalityEngine.getRepresentative( n[0] ); Node r2 = d_equalityEngine.getRepresentative( n[1] ); + d_set_eqc_relevant[r1] = true; + d_set_eqc_relevant[r2] = true; if( d_bop_index[n.getKind()][r1].find( r2 )==d_bop_index[n.getKind()][r1].end() ){ d_bop_index[n.getKind()][r1][r2] = n; d_op_list[n.getKind()].push_back( n ); @@ -590,6 +598,7 @@ void TheorySetsPrivate::fullEffortCheck(){ //TODO: extend approach for this case } Node r = d_equalityEngine.getRepresentative( n[0] ); + d_set_eqc_relevant[r] = true; if( d_eqc_to_card_term.find( r )==d_eqc_to_card_term.end() ){ d_eqc_to_card_term[ r ] = n; registerCardinalityTerm( n[0], lemmas ); @@ -1735,51 +1744,55 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel) { std::map< Node, Node > mvals; for( int i=(int)(d_set_eqc.size()-1); i>=0; i-- ){ Node eqc = d_set_eqc[i]; - std::vector< Node > els; - bool is_base = !d_card_enabled || ( d_nf[eqc].size()==1 && d_nf[eqc][0]==eqc ); - if( is_base ){ - Trace("sets-model") << "Collect elements of base eqc " << eqc << std::endl; - // members that must be in eqc - std::map< Node, std::map< Node, Node > >::iterator itm = d_pol_mems[0].find( eqc ); - if( itm!=d_pol_mems[0].end() ){ - for( std::map< Node, Node >::iterator itmm = itm->second.begin(); itmm != itm->second.end(); ++itmm ){ - Node t = NodeManager::currentNM()->mkNode( kind::SINGLETON, itmm->first ); - els.push_back( t ); + if( d_set_eqc_relevant.find( eqc )==d_set_eqc_relevant.end() ){ + Trace("sets-model") << "* Do not assign value for " << eqc << " since is not relevant." << std::endl; + }else{ + std::vector< Node > els; + bool is_base = !d_card_enabled || ( d_nf[eqc].size()==1 && d_nf[eqc][0]==eqc ); + if( is_base ){ + Trace("sets-model") << "Collect elements of base eqc " << eqc << std::endl; + // members that must be in eqc + std::map< Node, std::map< Node, Node > >::iterator itm = d_pol_mems[0].find( eqc ); + if( itm!=d_pol_mems[0].end() ){ + for( std::map< Node, Node >::iterator itmm = itm->second.begin(); itmm != itm->second.end(); ++itmm ){ + Node t = NodeManager::currentNM()->mkNode( kind::SINGLETON, itmm->first ); + els.push_back( t ); + } } } - } - if( d_card_enabled ){ - TypeNode elementType = eqc.getType().getSetElementType(); - if( is_base ){ - std::map< Node, Node >::iterator it = d_eqc_to_card_term.find( eqc ); - if( it!=d_eqc_to_card_term.end() ){ - //slack elements from cardinality value - Node v = d_external.d_valuation.getModelValue(it->second); - Trace("sets-model") << "Cardinality of " << eqc << " is " << v << std::endl; - Assert(v.getConst() <= LONG_MAX, "Exceeded LONG_MAX in sets model"); - unsigned vu = v.getConst().getNumerator().toUnsignedInt(); - Assert( els.size()<=vu ); - while( els.size()mkNode( kind::SINGLETON, NodeManager::currentNM()->mkSkolem( "msde", elementType ) ) ); + if( d_card_enabled ){ + TypeNode elementType = eqc.getType().getSetElementType(); + if( is_base ){ + std::map< Node, Node >::iterator it = d_eqc_to_card_term.find( eqc ); + if( it!=d_eqc_to_card_term.end() ){ + //slack elements from cardinality value + Node v = d_external.d_valuation.getModelValue(it->second); + Trace("sets-model") << "Cardinality of " << eqc << " is " << v << std::endl; + Assert(v.getConst() <= LONG_MAX, "Exceeded LONG_MAX in sets model"); + unsigned vu = v.getConst().getNumerator().toUnsignedInt(); + Assert( els.size()<=vu ); + while( els.size()mkNode( kind::SINGLETON, NodeManager::currentNM()->mkSkolem( "msde", elementType ) ) ); + } + }else{ + Trace("sets-model") << "No slack elements for " << eqc << std::endl; } }else{ - Trace("sets-model") << "No slack elements for " << eqc << std::endl; - } - }else{ - Trace("sets-model") << "Build value for " << eqc << " based on normal form, size = " << d_nf[eqc].size() << std::endl; - //it is union of venn regions - for( unsigned j=0; jassertEquality( eqc, rep, true ); + m->assertRepresentative( rep ); } - Node rep = NormalForm::mkBop( kind::UNION, els, eqc.getType() ); - rep = Rewriter::rewrite( rep ); - Trace("sets-model") << "Set representative of " << eqc << " to " << rep << std::endl; - mvals[eqc] = rep; - m->assertEquality( eqc, rep, true ); - m->assertRepresentative( rep ); } } diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 0a3745654..1c9a7e22a 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -116,6 +116,7 @@ private: NodeMap d_proxy_to_term; NodeSet d_lemmas_produced; std::vector< Node > d_set_eqc; + std::map< Node, bool > d_set_eqc_relevant; std::map< Node, std::vector< Node > > d_set_eqc_list; std::map< TypeNode, Node > d_eqc_emptyset; std::map< Node, Node > d_eqc_singleton; diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index fb5084b9d..eeced7430 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -71,7 +71,8 @@ TESTS = \ card-4.smt2 \ card-5.smt2 \ card-6.smt2 \ - card-7.smt2 + card-7.smt2 \ + abt-min.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/sets/abt-min.smt2 b/test/regress/regress0/sets/abt-min.smt2 new file mode 100644 index 000000000..3bf1a9b6a --- /dev/null +++ b/test/regress/regress0/sets/abt-min.smt2 @@ -0,0 +1,22 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +(set-logic ALL) +(declare-sort Atom 0) + +(declare-fun k (Atom Atom) (Set Atom)) + +(declare-fun t0 () Atom) +(declare-fun t1 () Atom) +(declare-fun t2 () Atom) +(declare-fun v () Atom) +(declare-fun b2 () Atom) + +(assert (forall ((b Atom)) (or +(member v (k t0 b)) +(member v (k t1 b)) +) )) + +(assert (not (member v (k t2 b2)))) + +(check-sat) + -- 2.30.2