Fix for when variables are (partially) bound in multiple ways, add regression. Improve printing for bound int module. Track when relations are enabled in sets, set incomplete if card+rels are both enabled since model construction is not guaranteed to succeed.

7 files changed, 102 insertions, 48 deletions

diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index e9ac9b484..1e8449dbf 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -246,8 +246,8 @@ void BoundedIntegers::process( Node q, Node n, bool pol,
       if( success && !isBound( q, v ) ){
         Trace("bound-int-debug") << "Success with variable " << v << std::endl;
         bound_lit_type_map[v] = BOUND_FIXED_SET;
-        bound_lit_map[0][v] = n;
-        bound_lit_pol_map[0][v] = pol;
+        bound_lit_map[3][v] = n;
+        bound_lit_pol_map[3][v] = pol;
         bound_fixed_set[v].clear();
         bound_fixed_set[v].insert( bound_fixed_set[v].end(), v_cases.begin(), v_cases.end() );
       }
@@ -260,8 +260,8 @@ void BoundedIntegers::process( Node q, Node n, bool pol,
       if( processEqDisjunct( q, n, v, v_cases ) ){
         if( !isBound( q, v ) ){
           bound_lit_type_map[v] = BOUND_FIXED_SET;
-          bound_lit_map[0][v] = n;
-          bound_lit_pol_map[0][v] = pol;
+          bound_lit_map[3][v] = n;
+          bound_lit_pol_map[3][v] = pol;
           Assert( v_cases.size()==1 );
           bound_fixed_set[v].clear();
           bound_fixed_set[v].push_back( v_cases[0] );
@@ -278,32 +278,35 @@ void BoundedIntegers::process( Node q, Node n, bool pol,
         QuantArith::debugPrintMonomialSum( msum, "bound-int-debug" );
         for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
           if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE && !isBound( q, it->first ) ){
-            Node veq;
-            if( QuantArith::isolate( it->first, msum, veq, GEQ )!=0 ){
-              Node n1 = veq[0];
-              Node n2 = veq[1];
-              if(pol){
-                //flip
-                n1 = veq[1];
-                n2 = veq[0];
-                if( n1.getKind()==BOUND_VARIABLE ){
-                  n2 = QuantArith::offset( n2, 1 );
+            //if not bound in another way
+            if( bound_lit_type_map.find( it->first )==bound_lit_type_map.end() || bound_lit_type_map[it->first] == BOUND_INT_RANGE ){
+              Node veq;
+              if( QuantArith::isolate( it->first, msum, veq, GEQ )!=0 ){
+                Node n1 = veq[0];
+                Node n2 = veq[1];
+                if(pol){
+                  //flip
+                  n1 = veq[1];
+                  n2 = veq[0];
+                  if( n1.getKind()==BOUND_VARIABLE ){
+                    n2 = QuantArith::offset( n2, 1 );
+                  }else{
+                    n1 = QuantArith::offset( n1, -1 );
+                  }
+                  veq = NodeManager::currentNM()->mkNode( GEQ, n1, n2 );
+                }
+                Trace("bound-int-debug") << "Isolated for " << it->first << " : (" << n1 << " >= " << n2 << ")" << std::endl;
+                Node t = n1==it->first ? n2 : n1;
+                if( !hasNonBoundVar( q, t ) ) {
+                  Trace("bound-int-debug") << "The bound is relevant." << std::endl;
+                  int loru = n1==it->first ? 0 : 1;
+                  bound_lit_type_map[it->first] = BOUND_INT_RANGE;
+                  bound_int_range_term[loru][it->first] = t;
+                  bound_lit_map[loru][it->first] = n;
+                  bound_lit_pol_map[loru][it->first] = pol;
                 }else{
-                  n1 = QuantArith::offset( n1, -1 );
+                  Trace("bound-int-debug") << "The term " << t << " has non-bound variable." << std::endl;
                 }
-                veq = NodeManager::currentNM()->mkNode( GEQ, n1, n2 );
-              }
-              Trace("bound-int-debug") << "Isolated for " << it->first << " : (" << n1 << " >= " << n2 << ")" << std::endl;
-              Node t = n1==it->first ? n2 : n1;
-              if( !hasNonBoundVar( q, t ) ) {
-                Trace("bound-int-debug") << "The bound is relevant." << std::endl;
-                int loru = n1==it->first ? 0 : 1;
-                bound_lit_type_map[it->first] = BOUND_INT_RANGE;
-                bound_int_range_term[loru][it->first] = t;
-                bound_lit_map[loru][it->first] = n;
-                bound_lit_pol_map[loru][it->first] = pol;
-              }else{
-                Trace("bound-int-debug") << "The term " << t << " has non-bound variable." << std::endl;
               }
             }
           }
@@ -314,8 +317,8 @@ void BoundedIntegers::process( Node q, Node n, bool pol,
     if( !pol && n[0].getKind()==BOUND_VARIABLE && !isBound( q, n[0] ) && !hasNonBoundVar( q, n[1] ) ){
       Trace("bound-int-debug") << "literal (polarity = " << pol << ") " << n << " is membership." << std::endl;
       bound_lit_type_map[n[0]] = BOUND_SET_MEMBER;
-      bound_lit_map[0][n[0]] = n;
-      bound_lit_pol_map[0][n[0]] = pol;
+      bound_lit_map[2][n[0]] = n;
+      bound_lit_pol_map[2][n[0]] = pol;
     }
   }else{
     Assert( n.getKind()!=LEQ && n.getKind()!=LT && n.getKind()!=GT );
@@ -391,10 +394,10 @@ void BoundedIntegers::preRegisterQuantifier( Node f ) {
         }else if( it->second==BOUND_SET_MEMBER ){
           setBoundedVar( f, v, BOUND_SET_MEMBER );
           setBoundVar = true;
-          d_setm_range[f][v] = bound_lit_map[0][v][1];
-          d_setm_range_lit[f][v] = bound_lit_map[0][v];
+          d_setm_range[f][v] = bound_lit_map[2][v][1];
+          d_setm_range_lit[f][v] = bound_lit_map[2][v];
           d_range[f][v] = NodeManager::currentNM()->mkNode( CARD, d_setm_range[f][v] );
-          Trace("bound-int") << "Variable " << v << " is bound because of set membership literal " << bound_lit_map[0][v] << std::endl;
+          Trace("bound-int") << "Variable " << v << " is bound because of set membership literal " << bound_lit_map[2][v] << std::endl;
         }else if( it->second==BOUND_FIXED_SET ){
           setBoundedVar( f, v, BOUND_FIXED_SET );
           setBoundVar = true;
@@ -406,7 +409,7 @@ void BoundedIntegers::preRegisterQuantifier( Node f ) {
               d_fixed_set_gr_range[f][v].push_back( t ); 
             }
           } 
-          Trace("bound-int") << "Variable " << v << " is bound because of disequality conjunction " << bound_lit_map[0][v] << std::endl;
+          Trace("bound-int") << "Variable " << v << " is bound because of disequality conjunction " << bound_lit_map[3][v] << std::endl;
         }
         if( setBoundVar ){
           success = true;
@@ -438,13 +441,34 @@ void BoundedIntegers::preRegisterQuantifier( Node f ) {
     }
   }while( success );
   
-  Trace("bound-int") << "Bounds are : " << std::endl;
-  for( unsigned i=0; i<d_set[f].size(); i++) {
-    Node v = d_set[f][i];
-    if( d_bound_type[f][v]==BOUND_INT_RANGE ){
-      Trace("bound-int") << "  " << d_bounds[0][f][v] << " <= " << v << " <= " << d_bounds[1][f][v] << " (range is " << d_range[f][v] << ")" << std::endl;
-    }else if( d_bound_type[f][v]==BOUND_SET_MEMBER ){
-      Trace("bound-int") << "  " << v << " in " << d_setm_range[f][v] << std::endl;
+  if( Trace.isOn("bound-int") ){
+    Trace("bound-int") << "Bounds are : " << std::endl;
+    for( unsigned i=0; i<f[0].getNumChildren(); i++) {
+      Node v = f[0][i];
+      if( std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end() ){
+        Assert( d_bound_type[f].find( v )!=d_bound_type[f].end() );
+        if( d_bound_type[f][v]==BOUND_INT_RANGE ){
+          Trace("bound-int") << "  " << d_bounds[0][f][v] << " <= " << v << " <= " << d_bounds[1][f][v] << " (range is " << d_range[f][v] << ")" << std::endl;
+        }else if( d_bound_type[f][v]==BOUND_SET_MEMBER ){
+          Trace("bound-int") << "  " << v << " in " << d_setm_range[f][v] << std::endl;
+        }else if( d_bound_type[f][v]==BOUND_FIXED_SET ){
+          Trace("bound-int") << "  " << v << " in { ";
+          for( unsigned i=0; i<d_fixed_set_ngr_range[f][v].size(); i++ ){ 
+            Trace("bound-int") << d_fixed_set_ngr_range[f][v][i] << " ";
+          }
+          for( unsigned i=0; i<d_fixed_set_gr_range[f][v].size(); i++ ){ 
+            Trace("bound-int") << d_fixed_set_gr_range[f][v][i] << " ";
+          }
+          Trace("bound-int") << "}" << std::endl;
+        }else if( d_bound_type[f][v]==BOUND_FINITE ){
+          Trace("bound-int") << "  " << v << " has small finite type." << std::endl;
+        }else{
+          Trace("bound-int") << "  " << v << " has unknown bound." << std::endl;
+          Assert( false );
+        }
+      }else{
+        Trace("bound-int") << "  " << "*** " << v << " is unbounded." << std::endl;
+      }
     }
   }
   
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 6880a995d..40da5d7d0 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -72,6 +72,7 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
   d_equalityEngine.addFunctionKind(kind::CARD);
 
   d_card_enabled = false;
+  d_rels_enabled = false;
 
 }/* TheorySetsPrivate::TheorySetsPrivate() */
 
@@ -513,6 +514,7 @@ void TheorySetsPrivate::fullEffortCheck(){
     d_bop_index.clear();
     d_op_list.clear();
     d_card_enabled = false;
+    d_rels_enabled = false;
     d_eqc_to_card_term.clear();
 
     std::vector< Node > lemmas;
@@ -559,7 +561,9 @@ void TheorySetsPrivate::fullEffortCheck(){
             }else{
               d_congruent[n] = d_singleton_index[r];
             }
-          }else if( n.getKind()!=kind::EMPTYSET ){
+          }else if( n.getKind()==kind::EMPTYSET ){
+            d_eqc_emptyset[tn] = eqc;
+          }else{
             Node r1 = d_equalityEngine.getRepresentative( n[0] );
             Node r2 = d_equalityEngine.getRepresentative( n[1] );
             if( d_bop_index[n.getKind()][r1].find( r2 )==d_bop_index[n.getKind()][r1].end() ){
@@ -568,8 +572,6 @@ void TheorySetsPrivate::fullEffortCheck(){
             }else{
               d_congruent[n] = d_bop_index[n.getKind()][r1][r2];
             }
-          }else{
-            d_eqc_emptyset[tn] = eqc;
           }
           d_nvar_sets[eqc].push_back( n );
           Trace("sets-debug2") << "Non-var-set[" << eqc << "] : " << n << std::endl;
@@ -588,8 +590,13 @@ void TheorySetsPrivate::fullEffortCheck(){
             d_eqc_to_card_term[ r ] = n;
             registerCardinalityTerm( n[0], lemmas );
           }
-        }else if( isSet ){
-          d_set_eqc_list[eqc].push_back( n );
+        }else{
+          if( d_rels->isRelationKind( n.getKind() ) ){
+            d_rels_enabled = true;
+          }
+          if( isSet ){
+            d_set_eqc_list[eqc].push_back( n );
+          }
         }
         ++eqc_i;
       }
@@ -1527,6 +1534,11 @@ void TheorySetsPrivate::check(Theory::Effort level) {
   // invoke the relational solver
   if( !d_conflict && !d_sentLemma ){
     d_rels->check(level);  
+    //incomplete if we have both cardinality constraints and relational operators?
+    // TODO: should internally check model, return unknown if fail
+    if( level == Theory::EFFORT_FULL && d_card_enabled && d_rels_enabled ){
+      d_external.d_out->setIncomplete();
+    }
   }
   Trace("sets-check") << "Sets finish Check effort " << level << std::endl;
 }/* TheorySetsPrivate::check() */
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 8a6eaac2f..0a3745654 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -130,6 +130,7 @@ private:
   //cardinality
 private:
   bool d_card_enabled;
+  bool d_rels_enabled;
   std::map< Node, Node > d_eqc_to_card_term;
   NodeSet d_card_processed;
   std::map< Node, std::vector< Node > > d_card_parent;
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 97e67a423..bd4ee5de0 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -824,7 +824,9 @@ int TheorySetsRels::EqcInfo::counter        = 0;
     d_tcr_tcGraph.clear();
     d_tc_lemmas_last.clear();
   }
-
+  bool TheorySetsRels::isRelationKind( Kind k ) {
+    return k == kind::TRANSPOSE || k == kind::PRODUCT || k == kind::JOIN || k == kind::TCLOSURE;
+  }
   void TheorySetsRels::doTCLemmas() {
     Trace("rels-debug") << "[Theory::Rels] **************** Start doTCLemmas !" << std::endl;
     std::map< Node, std::vector< Node > >::iterator tc_lemma_it = d_tc_lemmas_last.begin();
@@ -1387,6 +1389,7 @@ int TheorySetsRels::EqcInfo::counter        = 0;
         NodeSet::const_iterator     mem_it  = t2_ei->d_mem.begin();
 
         while(mem_it != t2_ei->d_mem.end()) {
+          Assert( !t2_ei->d_tc.get().isNull() );
           addTCMemAndSendInfer(t1_ei, NodeManager::currentNM()->mkNode(kind::MEMBER,*mem_it, t2_ei->d_tc.get()), (*t2_ei->d_mem_exp.find(*mem_it)).second);
           mem_it++;
         }
@@ -1397,6 +1400,7 @@ int TheorySetsRels::EqcInfo::counter        = 0;
         while(t1_mem_it != t1_ei->d_mem.end()) {
           NodeMap::const_iterator       reason_it       = t1_ei->d_mem_exp.find(*t1_mem_it);
           Assert(reason_it != t1_ei->d_mem_exp.end());
+          Assert( !t1_ei->d_tc.get().isNull() );
           addTCMemAndSendInfer(t1_ei, NodeManager::currentNM()->mkNode(kind::MEMBER,*t1_mem_it, t1_ei->d_tc.get()), (*reason_it).second);
           t1_mem_it++;
         }
@@ -1404,6 +1408,7 @@ int TheorySetsRels::EqcInfo::counter        = 0;
         NodeSet::const_iterator     t2_mem_it  = t2_ei->d_mem.begin();
 
         while(t2_mem_it != t2_ei->d_mem.end()) {
+          Assert( !t2_ei->d_tc.get().isNull() );
           addTCMemAndSendInfer(t1_ei, NodeManager::currentNM()->mkNode(kind::MEMBER,*t2_mem_it, t2_ei->d_tc.get()), (*t2_ei->d_mem_exp.find(*t2_mem_it)).second);
           t2_mem_it++;
         }
diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h
index b5c839a66..65a1c4164 100644
--- a/src/theory/sets/theory_sets_rels.h
+++ b/src/theory/sets/theory_sets_rels.h
@@ -64,6 +64,7 @@ public:
   void check(Theory::Effort);
   void doPendingLemmas();
 
+  bool isRelationKind( Kind k );
 private:
   /** equivalence class info
    * d_mem tuples that are members of this equivalence class
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index 218dde7d4..03fe780b8 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -63,7 +63,8 @@ TESTS =	\
 	fmf-strange-bounds-2.smt2 \
 	fmf-bound-2dim.smt2 \
 	memory_model-R_cpp-dd.cvc \
-	bug764.smt2
+	bug764.smt2 \
+	ko-bound-set.cvc
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/fmf/ko-bound-set.cvc b/test/regress/regress0/fmf/ko-bound-set.cvc
new file mode 100644
index 000000000..eebcbc2f8
--- /dev/null
+++ b/test/regress/regress0/fmf/ko-bound-set.cvc
@@ -0,0 +1,10 @@
+% EXPECT: invalid
+OPTION "finite-model-find";
+OPTION "fmf-bound-int";
+OPTION "produce-models";
+
+X, Y : SET OF INT;
+
+ASSERT FORALL(x : INT): x IS_IN X => x > 0;
+QUERY ||X|| = 5 AND Y = X | {9} => ||Y|| <= 4;
+