Fixes related to sets.

5 files changed, 91 insertions, 50 deletions

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<Rational>() <= LONG_MAX, "Exceeded LONG_MAX in sets model");
-          unsigned vu = v.getConst<Rational>().getNumerator().toUnsignedInt();
-          Assert( els.size()<=vu );
-          while( els.size()<vu ){
-            els.push_back( NodeManager::currentNM()->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<Rational>() <= LONG_MAX, "Exceeded LONG_MAX in sets model");
+            unsigned vu = v.getConst<Rational>().getNumerator().toUnsignedInt();
+            Assert( els.size()<=vu );
+            while( els.size()<vu ){
+              els.push_back( NodeManager::currentNM()->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; j<d_nf[eqc].size(); j++ ){
-          Assert( mvals.find( d_nf[eqc][j] )!=mvals.end() );
-          els.push_back( mvals[d_nf[eqc][j]] );
+          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; j<d_nf[eqc].size(); j++ ){
+            Assert( mvals.find( d_nf[eqc][j] )!=mvals.end() );
+            els.push_back( mvals[d_nf[eqc][j]] );
+          }
         }
       }
+      Node rep = NormalForm::mkBop( kind::UNION, els, eqc.getType() );
+      rep = Rewriter::rewrite( rep );
+      Trace("sets-model") << "* Assign representative of " << eqc << " to " << rep << std::endl;
+      mvals[eqc] = rep;
+      m->assertEquality( 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)
+