Add support for interval models in bounded integers MBQI (in progress).

1 files changed, 32 insertions, 14 deletions

diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 180c4bbcf..b44cc6779 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -139,7 +139,6 @@ bool RepSetIterator::initialize(){
     //store default domain
     d_domain.push_back( RepDomain() );
     TypeNode tn = d_types[i];
-    bool isSet = false;
     if( tn.isSort() ){
       if( !d_rep_set->hasType( tn ) ){
         Node var = NodeManager::currentNM()->mkSkolem( "repSet_$$", tn, "is a variable created by the RepSetIterator" );
@@ -147,31 +146,36 @@ bool RepSetIterator::initialize(){
         d_rep_set->add( var );
       }
     }else if( tn.isInteger() ){
+      bool inc = false;
       //check if it is bound
       if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){
         if( d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][i] ) ){
           Trace("bound-int-rsi") << "Rep set iterator: variable #" << i << " is bounded integer." << std::endl;
           d_enum_type.push_back( ENUM_RANGE );
-          isSet = true;
         }else{
-          Trace("fmf-incomplete") << "Incomplete because of integer quantification, no bounds found." << std::endl;
-          d_incomplete = true;
+          inc = true;
         }
       }else{
-        Trace("fmf-incomplete") << "Incomplete because of integer quantification." << std::endl;
-        d_incomplete = true;
+        inc = true;
       }
-    }else if( tn.isReal() ){
-      Trace("fmf-incomplete") << "Incomplete because of infinite type " << tn << std::endl;
-      d_incomplete = true;
-    //enumerate if the sort is reasonably small, the upper bound of 128 is chosen arbitrarily for now
-    }else if( tn.getCardinality().isFinite() && tn.getCardinality().getFiniteCardinality().toUnsignedInt()<=128 ){
+      if( inc ){
+        //check if it is otherwise bound
+        if( d_bounds[0].find(i)!=d_bounds[0].end() && d_bounds[1].find(i)!=d_bounds[1].end() ){
+          Trace("bound-int-rsi") << "Rep set iterator: variable #" << i << " is bounded." << std::endl;
+          d_enum_type.push_back( ENUM_RANGE );
+        }else{
+          Trace("fmf-incomplete") << "Incomplete because of integer quantification of " << d_owner[0][i] << "." << std::endl;
+          d_incomplete = true;
+        }
+      }
+    //enumerate if the sort is reasonably small, the upper bound of 1000 is chosen arbitrarily for now
+    }else if( tn.getCardinality().isFinite() && tn.getCardinality().getFiniteCardinality().toUnsignedInt()<=1000 ){
       d_rep_set->complete( tn );
     }else{
-      Trace("fmf-incomplete") << "Incomplete because of unknown type " << tn << std::endl;
+      Trace("fmf-incomplete") << "Incomplete because of quantification of type " << tn << std::endl;
       d_incomplete = true;
     }
-    if( !isSet ){
+    if( d_enum_type.size()<=i ){
       d_enum_type.push_back( ENUM_DOMAIN_ELEMENTS );
       if( d_rep_set->hasType( tn ) ){
         for( size_t j=0; j<d_rep_set->d_type_reps[tn].size(); j++ ){
@@ -182,7 +186,7 @@ bool RepSetIterator::initialize(){
       }
     }
   }
-  //must set a variable index order
+  //must set a variable index order based on bounded integers
   if (d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers()) {
     Trace("bound-int-rsi") << "Calculating variable order..." << std::endl;
     std::vector< int > varOrder;
@@ -211,6 +215,7 @@ bool RepSetIterator::initialize(){
     Trace("bound-int-rsi") << std::endl;
     setIndexOrder(indexOrder);
   }
+  //now reset the indices
   for (unsigned i=0; i<d_index.size(); i++) {
     if (!resetIndex(i, true)){
       break;
@@ -255,6 +260,19 @@ bool RepSetIterator::resetIndex( int i, bool initial ) {
         return false;
       }else{
         Trace("bound-int-rsi") << "Can limit bounds of " << d_owner[0][ii] << " to " << l << "..." << u << std::endl;
+        for( unsigned b=0; b<2; b++ ){
+          if( d_bounds[b].find(ii)!=d_bounds[b].end() ){
+            Trace("bound-int-rsi") << "May further limit bound(" << b << ") based on " << d_bounds[b][ii] << std::endl;
+            if( b==0 && d_bounds[b][ii].getConst<Rational>() > l.getConst<Rational>() ){
+              l = d_bounds[b][ii];
+            }else if( b==1 && d_bounds[b][ii].getConst<Rational>() <= u.getConst<Rational>() ){
+              u = NodeManager::currentNM()->mkNode( MINUS, d_bounds[b][ii],
+                                                    NodeManager::currentNM()->mkConst( Rational(1) ) );
+              u = Rewriter::rewrite( u );
+            }
+          }
+        }
+
         Node range = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MINUS, u, l ) );
         Node ra = Rewriter::rewrite( NodeManager::currentNM()->mkNode( LEQ, range, NodeManager::currentNM()->mkConst( Rational( 9999 ) ) ) );
         d_domain[ii].clear();