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.

1 files changed, 65 insertions, 41 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;
+      }
     }
   }