Initial infrastructure for bounded set quantification (disabled). Refactoring and fixes for --fmf-bound-int. Fix simple memory leaks in strings and bounded integers.

9 files changed, 333 insertions, 156 deletions

diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index d32ef59a1..7184624da 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -28,7 +28,7 @@ using namespace CVC4::theory::quantifiers;
 using namespace CVC4::kind;
 
 
-BoundedIntegers::RangeModel::RangeModel(BoundedIntegers * bi, Node r, context::Context* c, context::Context* u, bool isProxy) : d_bi(bi),
+BoundedIntegers::IntRangeModel::IntRangeModel(BoundedIntegers * bi, Node r, context::Context* c, context::Context* u, bool isProxy) : d_bi(bi),
       d_range(r), d_curr_max(-1), d_lit_to_range(u), d_range_assertions(c), d_has_range(c,false), d_curr_range(c,-1), d_ranges_proxied(u) { 
   if( options::fmfBoundIntLazy() ){
     d_proxy_range = isProxy ? r : NodeManager::currentNM()->mkSkolem( "pbir", r.getType() );
@@ -40,7 +40,7 @@ BoundedIntegers::RangeModel::RangeModel(BoundedIntegers * bi, Node r, context::C
   }
 }
 
-void BoundedIntegers::RangeModel::initialize() {
+void BoundedIntegers::IntRangeModel::initialize() {
   //add initial split lemma
   Node ltr = NodeManager::currentNM()->mkNode( LT, d_proxy_range, NodeManager::currentNM()->mkConst( Rational(0) ) );
   ltr = Rewriter::rewrite( ltr );
@@ -55,7 +55,7 @@ void BoundedIntegers::RangeModel::initialize() {
   d_bi->addLiteralFromRange(ltr_lit, d_range);
 }
 
-void BoundedIntegers::RangeModel::assertNode(Node n) {
+void BoundedIntegers::IntRangeModel::assertNode(Node n) {
   bool pol = n.getKind()!=NOT;
   Node nlit = n.getKind()==NOT ? n[0] : n;
   if( d_lit_to_range.find( nlit )!=d_lit_to_range.end() ){
@@ -93,7 +93,7 @@ void BoundedIntegers::RangeModel::assertNode(Node n) {
   }
 }
 
-void BoundedIntegers::RangeModel::allocateRange() {
+void BoundedIntegers::IntRangeModel::allocateRange() {
   d_curr_max++;
   int newBound = d_curr_max;
   Trace("bound-int-proc") << "Allocate range bound " << newBound << " for " << d_range << std::endl;
@@ -110,7 +110,7 @@ void BoundedIntegers::RangeModel::allocateRange() {
   d_bi->addLiteralFromRange(ltr_lit, d_range);
 }
 
-Node BoundedIntegers::RangeModel::getNextDecisionRequest() {
+Node BoundedIntegers::IntRangeModel::getNextDecisionRequest() {
   //request the current cardinality as a decision literal, if not already asserted
   for( NodeIntMap::iterator it = d_lit_to_range.begin(); it != d_lit_to_range.end(); ++it ){
     int i = (*it).second;
@@ -129,7 +129,7 @@ Node BoundedIntegers::RangeModel::getNextDecisionRequest() {
   return Node::null();
 }
 
-bool BoundedIntegers::RangeModel::proxyCurrentRange() {
+bool BoundedIntegers::IntRangeModel::proxyCurrentRange() {
   //Trace("model-engine") << "Range(" << d_range << ") currently is " << d_curr_max.get() << std::endl;
   if( d_range!=d_proxy_range ){
     //int curr = d_curr_range.get();
@@ -148,11 +148,24 @@ bool BoundedIntegers::RangeModel::proxyCurrentRange() {
 }
 
 
+
+
+
 BoundedIntegers::BoundedIntegers(context::Context* c, QuantifiersEngine* qe) :
 QuantifiersModule(qe), d_assertions(c){
 
 }
 
+BoundedIntegers::~BoundedIntegers() { 
+  for( std::map< Node, RangeModel * >::iterator it = d_rms.begin(); it != d_rms.end(); ++it ){
+    delete it->second;
+  }
+}
+
+void BoundedIntegers::presolve() {
+  d_bnd_it.clear();
+}
+
 bool BoundedIntegers::isBound( Node f, Node v ) {
   return std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end();
 }
@@ -172,62 +185,79 @@ bool BoundedIntegers::hasNonBoundVar( Node f, Node b ) {
   return false;
 }
 
-void BoundedIntegers::processLiteral( Node f, Node lit, bool pol,
+void BoundedIntegers::processLiteral( Node q, Node lit, bool pol,
+                                      std::map< Node, unsigned >& bound_lit_type_map,
                                       std::map< int, std::map< Node, Node > >& bound_lit_map,
-                                      std::map< int, std::map< Node, bool > >& bound_lit_pol_map ) {
-  if( lit.getKind()==GEQ && lit[0].getType().isInteger() ){
-    std::map< Node, Node > msum;
-    if (QuantArith::getMonomialSumLit( lit, msum )){
-      Trace("bound-int-debug") << "Literal (polarity = " << pol << ") " << lit << " is monomial sum : " << std::endl;
-      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( f, 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 );
+                                      std::map< int, std::map< Node, bool > >& bound_lit_pol_map,
+                                      std::map< int, std::map< Node, Node > >& bound_int_range_term ) {
+  if( lit.getKind()==GEQ ){
+    if( lit[0].getType().isInteger() ){
+      std::map< Node, Node > msum;
+      if( QuantArith::getMonomialSumLit( lit, msum ) ){
+        Trace("bound-int-debug") << "Literal (polarity = " << pol << ") " << lit << " is monomial sum : " << std::endl;
+        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 );
+                }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] = lit;
+                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( f, t ) ) {
-              Trace("bound-int-debug") << "The bound is relevant." << std::endl;
-              int loru = n1==it->first ? 0 : 1;
-              d_bounds[loru][f][it->first] = t;
-              bound_lit_map[loru][it->first] = lit;
-              bound_lit_pol_map[loru][it->first] = pol;
-            }else{
-              Trace("bound-int-debug") << "The term " << t << " has non-bound variable." << std::endl;
             }
           }
         }
       }
     }
+  }else if( lit.getKind()==MEMBER ){
+    //TODO: enable this when sets models are fixed
+    /*
+    if( !pol && lit[0].getKind()==BOUND_VARIABLE && !isBound( q, lit[0] ) && !lit[1].hasBoundVar() ){
+      Trace("bound-int-debug") << "Literal (polarity = " << pol << ") " << lit << " is membership." << std::endl;
+      bound_lit_type_map[lit[0]] = BOUND_SET_MEMBER;
+      bound_lit_map[0][lit[0]] = lit;
+      bound_lit_pol_map[0][lit[0]] = pol;
+    }
+    */
   }else if( lit.getKind()==LEQ || lit.getKind()==LT || lit.getKind()==GT ) {
     Message() << "BoundedIntegers : Bad kind for literal : " << lit << std::endl;
   }
 }
 
-void BoundedIntegers::process( Node f, Node n, bool pol,
+void BoundedIntegers::process( Node q, Node n, bool pol,
+                               std::map< Node, unsigned >& bound_lit_type_map,
                                std::map< int, std::map< Node, Node > >& bound_lit_map,
-                               std::map< int, std::map< Node, bool > >& bound_lit_pol_map ){
+                               std::map< int, std::map< Node, bool > >& bound_lit_pol_map,
+                               std::map< int, std::map< Node, Node > >& bound_int_range_term ){
   if( (n.getKind()==OR && pol) || (n.getKind()==AND && !pol) ){
     for( unsigned i=0; i<n.getNumChildren(); i++) {
-      process( f, n[i], pol, bound_lit_map, bound_lit_pol_map );
+      process( q, n[i], pol, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term );
     }
   }else if( n.getKind()==NOT ){
-    process( f, n[0], !pol, bound_lit_map, bound_lit_pol_map );
+    process( q, n[0], !pol, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term );
   }else {
-    processLiteral( f, n, pol, bound_lit_map, bound_lit_pol_map );
+    processLiteral( q, n, pol, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term );
   }
 }
 
@@ -258,58 +288,99 @@ void BoundedIntegers::addLiteralFromRange( Node lit, Node r ) {
   }
 }
 
+void BoundedIntegers::setBoundedVar( Node q, Node v, unsigned bound_type ) {
+  d_bound_type[q][v] = bound_type;
+  d_set_nums[q][v] = d_set[q].size();
+  d_set[q].push_back( v );
+  Trace("bound-int-var") << "Bound variable #" << d_set_nums[q][v] << " : " << v << std::endl; 
+}
+
 void BoundedIntegers::registerQuantifier( Node f ) {
   Trace("bound-int") << "Register quantifier " << f << std::endl;
-  bool hasIntType = false;
-  int finiteTypes = 0;
-  std::map< Node, int > numMap;
-  for( unsigned i=0; i<f[0].getNumChildren(); i++) {
-    numMap[f[0][i]] = i;
-    if( f[0][i].getType().isInteger() ){
-      hasIntType = true;
-    }
-    else if( f[0][i].getType().isSort() || f[0][i].getType().getCardinality().isFinite() ){
-      finiteTypes++;
-    }
-  }
-  if( hasIntType ){
-    bool success;
-    do{
-      std::map< int, std::map< Node, Node > > bound_lit_map;
-      std::map< int, std::map< Node, bool > > bound_lit_pol_map;
-      success = false;
-      process( f, f[1], true, bound_lit_map, bound_lit_pol_map );
-      for( std::map< Node, Node >::iterator it = d_bounds[0][f].begin(); it != d_bounds[0][f].end(); ++it ){
-        Node v = it->first;
-        if( !isBound(f,v) ){
-          if( d_bounds[1][f].find(v)!=d_bounds[1][f].end() ){
-            d_set[f].push_back(v);
-            d_set_nums[f].push_back(numMap[v]);
+  
+  bool success;
+  do{
+    std::map< Node, unsigned > bound_lit_type_map;
+    std::map< int, std::map< Node, Node > > bound_lit_map;
+    std::map< int, std::map< Node, bool > > bound_lit_pol_map;
+    std::map< int, std::map< Node, Node > > bound_int_range_term;
+    success = false;
+    process( f, f[1], true, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term );
+    //for( std::map< Node, Node >::iterator it = d_bounds[0][f].begin(); it != d_bounds[0][f].end(); ++it ){
+    for( std::map< Node, unsigned >::iterator it = bound_lit_type_map.begin(); it != bound_lit_type_map.end(); ++it ){
+      Node v = it->first;
+      if( !isBound( f, v ) ){
+        bool setBoundVar = false;
+        if( it->second==BOUND_INT_RANGE ){
+          //must have both
+          if( bound_lit_map[0].find( v )!=bound_lit_map[0].end() && bound_lit_map[1].find( v )!=bound_lit_map[1].end() ){
+            setBoundedVar( f, v, BOUND_INT_RANGE );
+            setBoundVar = true;
             success = true;
-            //set Attributes on literals
             for( unsigned b=0; b<2; b++ ){
-              Assert( bound_lit_map[b].find( v )!=bound_lit_map[b].end() );
+              //set the bounds
+              Assert( bound_int_range_term[b].find( v )!=bound_int_range_term[b].end() );
+              d_bounds[b][f][v] = bound_int_range_term[b][v];
+            }
+            Node r = NodeManager::currentNM()->mkNode( MINUS, d_bounds[1][f][v], d_bounds[0][f][v] );
+            d_range[f][v] = Rewriter::rewrite( r );
+            Trace("bound-int") << "Variable " << v << " is bound because of int range literals " << bound_lit_map[0][v] << " and " << bound_lit_map[1][v] << std::endl;
+          }
+        }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];
+          Trace("bound-int") << "Variable " << v << " is bound because of set membership literal " << bound_lit_map[0][v] << std::endl;
+        }
+        if( setBoundVar ){
+          //set Attributes on literals
+          for( unsigned b=0; b<2; b++ ){
+            if( bound_lit_map[b].find( v )!=bound_lit_map[b].end() ){
               Assert( bound_lit_pol_map[b].find( v )!=bound_lit_pol_map[b].end() );
               BoundIntLitAttribute bila;
               bound_lit_map[b][v].setAttribute( bila, bound_lit_pol_map[b][v] ? 1 : 0 );
+            }else{
+              Assert( it->second!=BOUND_INT_RANGE );
             }
-            Trace("bound-int") << "Variable " << v << " is bound because of literals " << bound_lit_map[0][v] << " and " << bound_lit_map[1][v] << std::endl;
           }
         }
       }
-    }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];
-      Node r = NodeManager::currentNM()->mkNode( MINUS, d_bounds[1][f][v], d_bounds[0][f][v] );
-      d_range[f][v] = Rewriter::rewrite( r );
+    }
+  }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;
+    }
+  }
+  
+  bool bound_success = true;
+  for( unsigned i=0; i<f[0].getNumChildren(); i++) {
+    if( d_bound_type[f].find( f[0][i] )==d_bound_type[f].end() ){
+      TypeNode tn = f[0][i].getType();
+      if( !tn.isSort() && !getTermDatabase()->mayComplete( tn ) ){
+        Trace("bound-int-warn") << "Warning : Bounded Integers : Due to quantification on " << f[0][i] << ", could not find bounds for " << f << std::endl;
+        bound_success = false;
+        break;
+      }
     }
-    if( d_set[f].size()==(f[0].getNumChildren()-finiteTypes) ){
-      d_bound_quants.push_back( f );
-      for( unsigned i=0; i<d_set[f].size(); i++) {
-        Node v = d_set[f][i];
-        Node r = d_range[f][v];
+  }
+  
+  if( bound_success ){
+    d_bound_quants.push_back( f );
+    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 || d_bound_type[f][v]==BOUND_SET_MEMBER ){
+        Node r;
+        if( d_bound_type[f][v]==BOUND_INT_RANGE ){
+          r = d_range[f][v];
+        }else if( d_bound_type[f][v]==BOUND_SET_MEMBER ){
+          r = NodeManager::currentNM()->mkNode( CARD, d_setm_range[f][v] );
+        }
         bool isProxy = false;
         if( r.hasBoundVar() ){
           //introduce a new bound
@@ -319,18 +390,15 @@ void BoundedIntegers::registerQuantifier( Node f ) {
           r = new_range;
           isProxy = true;
         }
-        if( r.getKind()!=CONST_RATIONAL ){
+        if( !r.isConst() ){
           if( std::find(d_ranges.begin(), d_ranges.end(), r)==d_ranges.end() ){
-            Trace("bound-int") << "For " << v << ", bounded Integer Module will try to minimize : " << r << " " << r.getKind() << std::endl;
+            Trace("bound-int") << "For " << v << ", bounded Integer Module will try to minimize : " << r << std::endl;
             d_ranges.push_back( r );
-            d_rms[r] = new RangeModel(this, r, d_quantEngine->getSatContext(), d_quantEngine->getUserContext(), isProxy );
+            d_rms[r] = new IntRangeModel( this, r, d_quantEngine->getSatContext(), d_quantEngine->getUserContext(), isProxy );
             d_rms[r]->initialize();
           }
         }
       }
-    }else{
-      Trace("bound-int-warn") << "Warning : Bounded Integers : Could not find bounds for " << f << std::endl;
-      //Message() << "Bound integers : Cannot infer bounds of " << f << std::endl;
     }
   }
 }
@@ -376,39 +444,28 @@ Node BoundedIntegers::getNextDecisionRequest() {
   return Node::null();
 }
 
+unsigned BoundedIntegers::getBoundVarType( Node q, Node v ) {
+  std::map< Node, unsigned >::iterator it = d_bound_type[q].find( v );
+  if( it==d_bound_type[q].end() ){
+    return BOUND_NONE;
+  }else{
+    return it->second;
+  }
+}
+
 void BoundedIntegers::getBounds( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ) {
   l = d_bounds[0][f][v];
   u = d_bounds[1][f][v];
   if( d_nground_range[f].find(v)!=d_nground_range[f].end() ){
-    //must create substitution
+    //get the substitution
     std::vector< Node > vars;
     std::vector< Node > subs;
-    Trace("bound-int-rsi") << "Get bound value in model of variable " << v << std::endl;
-    for( unsigned i=0; i<d_set[f].size(); i++) {
-      if( d_set[f][i]!=v ){
-        Trace("bound-int-rsi") << "Look up the value for " << d_set[f][i] << " " << rsi->d_var_order[d_set_nums[f][i]] << std::endl;
-        Trace("bound-int-rsi") << "term : " << rsi->getTerm(rsi->d_var_order[d_set_nums[f][i]]) << std::endl;
-        vars.push_back(d_set[f][i]);
-        subs.push_back(rsi->getTerm(rsi->d_var_order[d_set_nums[f][i]]));
-      }else{
-        break;
-      }
-    }
-    Trace("bound-int-rsi") << "Do substitution..." << std::endl;
-    //check if it has been instantiated
-    if (!vars.empty() && !d_bnd_it[f][v].hasInstantiated(subs)){
-      //must add the lemma
-      Node nn = d_nground_range[f][v];
-      nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
-      Node lem = NodeManager::currentNM()->mkNode( LEQ, nn, d_range[f][v] );
-      Trace("bound-int-lemma") << "*** Add lemma to minimize instantiated non-ground term " << lem << std::endl;
-      d_quantEngine->getOutputChannel().lemma(lem, false, true);
-      l = Node::null();
-      u = Node::null();
-      return;
-    }else{
+    if( getRsiSubsitution( f, v, vars, subs, rsi ) ){
       u = u.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
       l = l.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+    }else{
+      u = Node::null();
+      l = Node::null();
     }
   }
 }
@@ -416,12 +473,86 @@ void BoundedIntegers::getBounds( Node f, Node v, RepSetIterator * rsi, Node & l,
 void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ) {
   getBounds( f, v, rsi, l, u );
   Trace("bound-int-rsi") << "Get value in model for..." << l << " and " << u << std::endl;
-  l = d_quantEngine->getModel()->getCurrentModelValue( l );
-  u = d_quantEngine->getModel()->getCurrentModelValue( u );
+  if( !l.isNull() ){
+    l = d_quantEngine->getModel()->getCurrentModelValue( l );
+  }
+  if( !u.isNull() ){
+    u = d_quantEngine->getModel()->getCurrentModelValue( u );
+  }
   Trace("bound-int-rsi") << "Value is " << l << " ... " << u << std::endl;
   return;
 }
 
-bool BoundedIntegers::isGroundRange(Node f, Node v) {
-  return isBoundVar(f,v) && !getLowerBound(f,v).hasBoundVar() && !getUpperBound(f,v).hasBoundVar();
+bool BoundedIntegers::isGroundRange( Node q, Node v ) {
+  if( isBoundVar(q,v) ){
+    if( d_bound_type[q][v]==BOUND_INT_RANGE ){
+      return !getLowerBound(q,v).hasBoundVar() && !getUpperBound(q,v).hasBoundVar();
+    }else if( d_bound_type[q][v]==BOUND_SET_MEMBER ){
+      return !d_setm_range[q][v].hasBoundVar();
+    }
+  }
+  return false;
 }
+
+Node BoundedIntegers::getSetRange( Node q, Node v, RepSetIterator * rsi ) {
+  Node sr = d_setm_range[q][v];
+  if( d_nground_range[q].find(v)!=d_nground_range[q].end() ){
+    //get the substitution
+    std::vector< Node > vars;
+    std::vector< Node > subs;
+    if( getRsiSubsitution( q, v, vars, subs, rsi ) ){
+      sr = sr.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+    }else{
+      sr = Node::null();
+    }
+  }
+  return sr;
+}
+
+Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) {
+  Node sr = getSetRange( q, v, rsi );
+  if( !sr.isNull() ){
+    Trace("bound-int-rsi") << "Get value in model for..." << sr << std::endl;
+    sr = d_quantEngine->getModel()->getCurrentModelValue( sr );
+    Trace("bound-int-rsi") << "Value is " << sr << std::endl;
+  }
+  return sr;
+}
+
+bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& vars, std::vector< Node >& subs, RepSetIterator * rsi ) {
+
+  Trace("bound-int-rsi") << "Get bound value in model of variable " << v << std::endl;
+  Assert( d_set_nums[q].find( v )!=d_set_nums[q].end() );
+  int vindex = d_set_nums[q][v];
+  Assert( d_set_nums[q][v]==vindex );
+  Trace("bound-int-rsi-debug") << "  index order is " << vindex << std::endl;
+  //must take substitution for all variables that are iterating at higher level
+  for( int i=0; i<vindex; i++) {
+    Assert( d_set_nums[q][d_set[q][i]]==i );
+    Trace("bound-int-rsi") << "Look up the value for " << d_set[q][i] << " " << i << std::endl;
+    int v = rsi->getVariableOrder( i );
+    Assert( q[0][v]==d_set[q][i] );
+    Node t = rsi->getCurrentTerm( v );
+    Trace("bound-int-rsi") << "term : " << t << std::endl;
+    vars.push_back( d_set[q][i] );
+    subs.push_back( t );
+  }
+  
+  //check if it has been instantiated
+  if( !vars.empty() && !d_bnd_it[q][v].hasInstantiated(subs) ){
+    if( d_bound_type[q][v]==BOUND_INT_RANGE ){
+      //must add the lemma
+      Node nn = d_nground_range[q][v];
+      nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+      Node lem = NodeManager::currentNM()->mkNode( LEQ, nn, d_range[q][v] );
+      Trace("bound-int-lemma") << "*** Add lemma to minimize instantiated non-ground term " << lem << std::endl;
+      d_quantEngine->getOutputChannel().lemma(lem, false, true);
+    }else{
+      //TODO : sets
+    }
+    return false;
+  }else{
+    return true;
+  }
+}
+
diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h
index 7d15097bd..ab4bcba96 100644
--- a/src/theory/quantifiers/bounded_integers.h
+++ b/src/theory/quantifiers/bounded_integers.h
@@ -39,31 +39,57 @@ class BoundedIntegers : public QuantifiersModule
   typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
   typedef context::CDHashMap<int, bool> IntBoolMap;
+public:
+  enum {
+    BOUND_FINITE,
+    BOUND_INT_RANGE,
+    BOUND_SET_MEMBER,
+    BOUND_NONE
+  };
 private:
   //for determining bounds
   bool isBound( Node f, Node v );
   bool hasNonBoundVar( Node f, Node b );
-  std::map< Node, std::map< Node, Node > > d_bounds[2];
+  //bound type
+  std::map< Node, std::map< Node, unsigned > > d_bound_type;
   std::map< Node, std::vector< Node > > d_set;
-  std::map< Node, std::vector< int > > d_set_nums;
+  std::map< Node, std::map< Node, int > > d_set_nums;
+  //integer lower/upper bounds
+  std::map< Node, std::map< Node, Node > > d_bounds[2];
   std::map< Node, std::map< Node, Node > > d_range;
   std::map< Node, std::map< Node, Node > > d_nground_range;
+  //set membership range
+  std::map< Node, std::map< Node, Node > > d_setm_range;
   void hasFreeVar( Node f, Node n );
   void process( Node f, Node n, bool pol,
+                std::map< Node, unsigned >& bound_lit_type_map,
                 std::map< int, std::map< Node, Node > >& bound_lit_map,
-                std::map< int, std::map< Node, bool > >& bound_lit_pol_map );
+                std::map< int, std::map< Node, bool > >& bound_lit_pol_map,
+                std::map< int, std::map< Node, Node > >& bound_int_range_term );
   void processLiteral( Node f, Node lit, bool pol,
+                       std::map< Node, unsigned >& bound_lit_type_map,
                        std::map< int, std::map< Node, Node > >& bound_lit_map,
-                       std::map< int, std::map< Node, bool > >& bound_lit_pol_map  );
+                       std::map< int, std::map< Node, bool > >& bound_lit_pol_map,
+                       std::map< int, std::map< Node, Node > >& bound_int_range_term  );
   std::vector< Node > d_bound_quants;
 private:
   class RangeModel {
+  public:
+    RangeModel(){}
+    virtual ~RangeModel(){}
+    virtual void initialize() = 0;
+    virtual void assertNode(Node n) = 0;
+    virtual Node getNextDecisionRequest() = 0;
+    virtual bool proxyCurrentRange() = 0;
+  };
+  class IntRangeModel : public RangeModel {
   private:
     BoundedIntegers * d_bi;
     void allocateRange();
     Node d_proxy_range;
   public:
-    RangeModel(BoundedIntegers * bi, Node r, context::Context* c, context::Context* u, bool isProxy);
+    IntRangeModel( BoundedIntegers * bi, Node r, context::Context* c, context::Context* u, bool isProxy);
+    virtual ~IntRangeModel(){}
     Node d_range;
     int d_curr_max;
     std::map< int, Node > d_range_literal;
@@ -108,27 +134,36 @@ private:
   std::map< Node, std::map< Node, BoundInstTrie > > d_bnd_it;
 private:
   void addLiteralFromRange( Node lit, Node r );
+  
+  void setBoundedVar( Node f, Node v, unsigned bound_type );
 public:
   BoundedIntegers( context::Context* c, QuantifiersEngine* qe );
-  ~BoundedIntegers() throw() {}
-
+  virtual ~BoundedIntegers();
+  
+  void presolve();
   bool needsCheck( Theory::Effort e );
   void check( Theory::Effort e, unsigned quant_e );
   void registerQuantifier( Node f );
   void assertNode( Node n );
   Node getNextDecisionRequest();
-  bool isBoundVar( Node f, Node v ) { return std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end(); }
-  unsigned getNumBoundVars( Node f ) { return d_set[f].size(); }
-  Node getBoundVar( Node f, int i ) { return d_set[f][i]; }
-  int getBoundVarNum( Node f, int i ) { return d_set_nums[f][i]; }
-  Node getLowerBound( Node f, Node v ){ return d_bounds[0][f][v]; }
-  Node getUpperBound( Node f, Node v ){ return d_bounds[1][f][v]; }
+  bool isBoundVar( Node q, Node v ) { return std::find( d_set[q].begin(), d_set[q].end(), v )!=d_set[q].end(); }
+  unsigned getBoundVarType( Node q, Node v );
+  unsigned getNumBoundVars( Node q ) { return d_set[q].size(); }
+  Node getBoundVar( Node q, int i ) { return d_set[q][i]; }
+  //for integer range
+  Node getLowerBound( Node q, Node v ){ return d_bounds[0][q][v]; }
+  Node getUpperBound( Node q, Node v ){ return d_bounds[1][q][v]; }
   void getBounds( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u );
   void getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u );
   bool isGroundRange(Node f, Node v);
+  //for set range
+  Node getSetRange( Node q, Node v, RepSetIterator * rsi );
+  Node getSetRangeValue( Node q, Node v, RepSetIterator * rsi );
 
   /** Identify this module */
   std::string identify() const { return "BoundedIntegers"; }
+private:
+  bool getRsiSubsitution( Node q, Node v, std::vector< Node >& vars, std::vector< Node >& subs, RepSetIterator * rsi );
 };
 
 }
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index a833f48d2..670f0eff3 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -406,8 +406,8 @@ Node FirstOrderModelIG::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri
   //check the type of n
   if( n.getKind()==INST_CONSTANT ){
     int v = n.getAttribute(InstVarNumAttribute());
-    depIndex = ri->d_var_order[ v ];
-    val = ri->getTerm( v );
+    depIndex = ri->getIndexOrder( v );
+    val = ri->getCurrentTerm( v );
   }else if( n.getKind()==ITE ){
     int depIndex1, depIndex2;
     int eval = evaluate( n[0], depIndex1, ri );
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 8835d00bc..a0665cb7f 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -764,7 +764,7 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
     Trace("fmc-exh-debug") << "Set element domains..." << std::endl;
     //set the domains based on the entry
     for (unsigned i=0; i<c.getNumChildren(); i++) {
-      if (riter.d_enum_type[i]==RepSetIterator::ENUM_DOMAIN_ELEMENTS) {
+      if( riter.d_enum_type[i]==RepSetIterator::ENUM_DOMAIN_ELEMENTS || riter.d_enum_type[i]==RepSetIterator::ENUM_SET_MEMBERS ){
         TypeNode tn = c[i].getType();
         if( d_rep_ids.find(tn)!=d_rep_ids.end() ){
           if( fm->isInterval(c[i]) || fm->isStar(c[i]) ){
@@ -773,6 +773,7 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
             if (d_rep_ids[tn].find(c[i])!=d_rep_ids[tn].end()) {
               riter.d_domain[i].clear();
               riter.d_domain[i].push_back(d_rep_ids[tn][c[i]]);
+              riter.d_enum_type[i] = RepSetIterator::ENUM_DOMAIN_ELEMENTS;
             }else{
               Trace("fmc-exh") << "---- Does not have rep : " << c[i] << " for type " << tn << std::endl;
               return false;
@@ -792,7 +793,7 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
       std::vector< Node > ev_inst;
       std::vector< Node > inst;
       for( int i=0; i<riter.getNumTerms(); i++ ){
-        Node rr = riter.getTerm( i );
+        Node rr = riter.getCurrentTerm( i );
         Node r = rr;
         //if( r.getType().isSort() ){
         r = fm->getUsedRepresentative( r );
@@ -826,18 +827,18 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
       int index = riter.increment();
       Trace("fmc-exh-debug") << "Incremented index " << index << std::endl;
       if( !riter.isFinished() ){
-        if (index>=0 && riter.d_index[index]>0 && addedLemmas>0 && riter.d_enum_type[index]==RepSetIterator::ENUM_RANGE) {
+        if (index>=0 && riter.d_index[index]>0 && addedLemmas>0 && riter.d_enum_type[index]==RepSetIterator::ENUM_INT_RANGE) {
           Trace("fmc-exh-debug") << "Since this is a range enumeration, skip to the next..." << std::endl;
           riter.increment2( index-1 );
         }
       }
     }
     d_addedLemmas += addedLemmas;
-    Trace("fmc-exh") << "----Finished Exhaustive instantiate, lemmas = " << addedLemmas << ", incomplete=" << riter.d_incomplete << std::endl;
-    return addedLemmas>0 || !riter.d_incomplete;
+    Trace("fmc-exh") << "----Finished Exhaustive instantiate, lemmas = " << addedLemmas << ", incomplete=" << riter.isIncomplete() << std::endl;
+    return addedLemmas>0 || !riter.isIncomplete();
   }else{
     Trace("fmc-exh") << "----Finished Exhaustive instantiate, failed." << std::endl;
-    return false;
+    return !riter.isIncomplete();
   }
 }
 
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 5b5f9fc22..efd765c86 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -278,8 +278,8 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
         Trace("auto-gen-trigger-debug") << "Collected pat terms for " << bd << ", no-patterns : " << d_user_no_gen[f].size() << std::endl;
         for( unsigned i=0; i<patTermsF.size(); i++ ){
           Assert( tinfo.find( patTermsF[i] )!=tinfo.end() );
-          Trace("auto-gen-trigger-debug") << "   " << patTermsF[i];
-          Trace("auto-gen-trigger-debug") << " info[" << tinfo[patTermsF[i]].d_reqPol << ", " << tinfo[patTermsF[i]].d_reqPolEq << ", " << tinfo[patTermsF[i]].d_fv.size() << "]" << std::endl;
+          Trace("auto-gen-trigger-debug") << "   " << patTermsF[i] << std::endl;
+          Trace("auto-gen-trigger-debug2") << "     info = [" << tinfo[patTermsF[i]].d_reqPol << ", " << tinfo[patTermsF[i]].d_reqPolEq << ", " << tinfo[patTermsF[i]].d_fv.size() << "]" << std::endl;
         }
         Trace("auto-gen-trigger-debug") << std::endl;
       }
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 42fd7c354..10a5ae41b 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -66,7 +66,7 @@ void QModelBuilder::debugModel( FirstOrderModel* fm ){
           tests++;
           std::vector< Node > terms;
           for( int k=0; k<riter.getNumTerms(); k++ ){
-            terms.push_back( riter.getTerm( k ) );
+            terms.push_back( riter.getCurrentTerm( k ) );
           }
           Node n = d_qe->getInstantiation( f, vars, terms );
           Node val = fm->getValue( n );
@@ -84,7 +84,9 @@ void QModelBuilder::debugModel( FirstOrderModel* fm ){
         }
         Trace("quant-check-model") << "." << std::endl;
       }else{
-        Trace("quant-check-model") << "Warning: Could not test quantifier " << f << std::endl;
+        if( riter.isIncomplete() ){
+          Trace("quant-check-model") << "Warning: Could not test quantifier " << f << std::endl;
+        }
       }
     }
   }
@@ -399,15 +401,19 @@ bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
       Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl;
       while( !riter.isFinished() && ( d_addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
         d_triedLemmas++;
-        for( int i=0; i<(int)riter.d_index.size(); i++ ){
-          Trace("try") << i << " : " << riter.d_index[i] << " : " << riter.getTerm( i ) << std::endl;
+        if( Debug.isOn("inst-fmf-ei-debug") ){
+          for( int i=0; i<(int)riter.d_index.size(); i++ ){
+            Debug("inst-fmf-ei-debug") << i << " : " << riter.d_index[i] << " : " << riter.getCurrentTerm( i ) << std::endl;
+          }
         }
         int eval = 0;
         int depIndex;
         //see if instantiation is already true in current model
-        Debug("fmf-model-eval") << "Evaluating ";
-        riter.debugPrintSmall("fmf-model-eval");
-        Debug("fmf-model-eval") << "Done calculating terms." << std::endl;
+        if( Debug.isOn("fmf-model-eval") ){
+          Debug("fmf-model-eval") << "Evaluating ";
+          riter.debugPrintSmall("fmf-model-eval");
+          Debug("fmf-model-eval") << "Done calculating terms." << std::endl;
+        }
         //if evaluate(...)==1, then the instantiation is already true in the model
         //  depIndex is the index of the least significant variable that this evaluation relies upon
         depIndex = riter.getNumTerms()-1;
@@ -425,7 +431,7 @@ bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
           //instantiation was not shown to be true, construct the match
           InstMatch m( f );
           for( int i=0; i<riter.getNumTerms(); i++ ){
-            m.set( d_qe, riter.d_index_order[i], riter.getTerm( i ) );
+            m.set( d_qe, i, riter.getCurrentTerm( i ) );
           }
           Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
           //add as instantiation
@@ -463,8 +469,8 @@ bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
         Trace("model-engine-warn") << std::endl;
       }
     }
-     //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
-    d_incomplete_check = riter.d_incomplete;
+    //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
+    d_incomplete_check = riter.isIncomplete();
     return true;
   }else{
     return false;
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 3063e7a2f..f855154af 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -282,15 +282,15 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
     //create a rep set iterator and iterate over the (relevant) domain of the quantifier
     RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) );
     if( riter.setQuantifier( f ) ){
-      Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.d_incomplete << "..." << std::endl;
-      if( !riter.d_incomplete ){
+      Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
+      if( !riter.isIncomplete() ){
         int triedLemmas = 0;
         int addedLemmas = 0;
         while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
           //instantiation was not shown to be true, construct the match
           InstMatch m( f );
           for( int i=0; i<riter.getNumTerms(); i++ ){
-            m.set( d_quantEngine, riter.d_index_order[i], riter.getTerm( i ) );
+            m.set( d_quantEngine, i, riter.getCurrentTerm( i ) );
           }
           Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
           triedLemmas++;
@@ -310,11 +310,10 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
         d_statistics.d_exh_inst_lemmas += addedLemmas;
       }
     }else{
-      Trace("fmf-exh-inst") << "...exhaustive instantiation failed to set, incomplete=" << riter.d_incomplete << "..." << std::endl;
-      Assert( riter.d_incomplete );
+      Trace("fmf-exh-inst") << "...exhaustive instantiation did set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
     }
     //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
-    d_incomplete_check = d_incomplete_check || riter.d_incomplete;
+    d_incomplete_check = d_incomplete_check || riter.isIncomplete();
   }
 }
 
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 334e42375..5645c3401 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -168,6 +168,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi
           }
           
           Node op = getMatchOperator( n );
+          Trace("term-db-debug") << "  match operator is : " << op << std::endl;
           d_op_map[op].push_back( n );
           added.insert( n );
           
@@ -893,6 +894,7 @@ void TermDb::makeInstantiationConstantsFor( Node q ){
     Debug("quantifiers-engine") << "Instantiation constants for " << q << " : " << std::endl;
     for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
       d_vars[q].push_back( q[0][i] );
+      d_var_num[q][q[0][i]] = i;
       //make instantiation constants
       Node ic = NodeManager::currentNM()->mkInstConstant( q[0][i].getType() );
       d_inst_constants_map[ic] = q;
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 3f931014b..7ab3668eb 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -300,6 +300,7 @@ public:
 private:
   /** map from universal quantifiers to the list of variables */
   std::map< Node, std::vector< Node > > d_vars;
+  std::map< Node, std::map< Node, unsigned > > d_var_num;
   /** map from universal quantifiers to the list of instantiation constants */
   std::map< Node, std::vector< Node > > d_inst_constants;
   /** map from universal quantifiers to their inst constant body */
@@ -311,6 +312,8 @@ private:
   /** make instantiation constants for */
   void makeInstantiationConstantsFor( Node q );
 public:
+  /** get variable number */
+  unsigned getVariableNum( Node q, Node v ) { return d_var_num[q][v]; }
   /** get the i^th instantiation constant of q */
   Node getInstantiationConstant( Node q, int i ) const;
   /** get number of instantiation constants for q */