From 24d60fa5654a32b09dc8de79b7704fbf40051478 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 11 May 2013 17:36:07 -0500
Subject: [PATCH] Preliminary version of finite model finding over bounded
 integer quantification. Minor update to casc script.

---
 contrib/run-script-casc24-fnt               |   2 +-
 src/theory/arith/theory_arith_private.cpp   |   7 +
 src/theory/arith/theory_arith_private.h     |   3 +-
 src/theory/quantifiers/bounded_integers.cpp | 202 +++++++++++++++++++-
 src/theory/quantifiers/bounded_integers.h   |  55 +++++-
 src/theory/quantifiers/full_model_check.cpp |  20 +-
 src/theory/quantifiers/model_builder.cpp    |   2 +-
 src/theory/quantifiers/model_engine.cpp     |  14 +-
 src/theory/quantifiers/model_engine.h       |   2 +-
 src/theory/quantifiers/quant_util.cpp       |   8 +-
 src/theory/quantifiers/quant_util.h         |   1 +
 src/theory/quantifiers_engine.cpp           |   2 +-
 src/theory/quantifiers_engine.h             |   2 +
 src/theory/rep_set.cpp                      |  88 +++++++--
 src/theory/rep_set.h                        |  21 +-
 15 files changed, 376 insertions(+), 53 deletions(-)

diff --git a/contrib/run-script-casc24-fnt b/contrib/run-script-casc24-fnt
index ef3cd4b65..c53ac4be9 100755
--- a/contrib/run-script-casc24-fnt
+++ b/contrib/run-script-casc24-fnt
@@ -1,6 +1,6 @@
 #!/bin/bash
 
-cvc4=cvc4
+cvc4=./cvc4
 bench="$1"
 
 file=${bench##*/}
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index d911ecf77..060f6dbba 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -67,6 +67,8 @@
 
 #include "theory/arith/options.h"
 
+#include "theory/quantifiers/bounded_integers.h"
+
 #include <stdint.h>
 
 #include <vector>
@@ -89,6 +91,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context
   d_unknownsInARow(0),
   d_hasDoneWorkSinceCut(false),
   d_learner(u),
+  d_quantEngine(qe),
   d_assertionsThatDoNotMatchTheirLiterals(c),
   d_nextIntegerCheckVar(0),
   d_constantIntegerVariables(c),
@@ -1373,6 +1376,10 @@ Constraint TheoryArithPrivate::constraintFromFactQueue(){
   Assert(!done());
   TNode assertion = get();
 
+  if( options::finiteModelFind() ){
+    d_quantEngine->getBoundedIntegers()->assertNode(assertion);
+  }
+
   Kind simpleKind = Comparison::comparisonKind(assertion);
   Constraint constraint = d_constraintDatabase.lookup(assertion);
   if(constraint == NullConstraint){
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 2ea3bb68e..86c8e213e 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -132,7 +132,8 @@ private:
   /** Static learner. */
   ArithStaticLearner d_learner;
 
-
+  /** quantifiers engine */
+  QuantifiersEngine * d_quantEngine;
   //std::vector<ArithVar> d_pool;
 public:
   void releaseArithVar(ArithVar v);
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 03a52539e..a9eb72b03 100755
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/bounded_integers.h"
 #include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/first_order_model.h"
 
 using namespace CVC4;
 using namespace std;
@@ -21,15 +22,123 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 using namespace CVC4::kind;
 
-BoundedIntegers::BoundedIntegers(QuantifiersEngine* qe) : QuantifiersModule(qe){
+void BoundedIntegers::RangeModel::initialize() {
+  //add initial split lemma
+  Node ltr = NodeManager::currentNM()->mkNode( LT, d_range, NodeManager::currentNM()->mkConst( Rational(0) ) );
+  ltr = Rewriter::rewrite( ltr );
+  Trace("bound-integers-lemma") << " *** bound int: initial split on " << ltr << std::endl;
+  d_bi->getQuantifiersEngine()->getOutputChannel().split( ltr );
+  Node ltr_lit = ltr.getKind()==NOT ? ltr[0] : ltr;
+  d_range_literal[-1] = ltr_lit;
+  d_lit_to_range[ltr_lit] = -1;
+  d_lit_to_pol[ltr_lit] = ltr.getKind()!=NOT;
+  //register with bounded integers
+  Trace("bound-integers-debug") << "Literal " << ltr_lit << " is literal for " << d_range << std::endl;
+  d_bi->addLiteralFromRange(ltr_lit, d_range);
+}
+
+void BoundedIntegers::RangeModel::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() ){
+    Trace("bound-integers-assert") << "With polarity = " << pol << " (req "<< d_lit_to_pol[nlit] << ")";
+    Trace("bound-integers-assert") << ", found literal " << nlit;
+    Trace("bound-integers-assert") << ", it is bound literal " << d_lit_to_range[nlit] << " for " << d_range << std::endl;
+    d_range_assertions[nlit] = (pol==d_lit_to_pol[nlit]);
+    if( pol!=d_lit_to_pol[nlit] ){
+      //check if we need a new split?
+      if( !d_has_range ){
+        bool needsRange = true;
+        for( std::map< Node, int >::iterator it = d_lit_to_range.begin(); it != d_lit_to_range.end(); ++it ){
+          if( d_range_assertions.find( it->first )==d_range_assertions.end() ){
+            needsRange = false;
+            break;
+          }
+        }
+        if( needsRange ){
+          allocateRange();
+        }
+      }
+    }else{
+      if (!d_has_range || d_lit_to_range[nlit]<d_curr_range ){
+        Trace("bound-integers-bound") << "Successfully bound " << d_range << " to " << d_lit_to_range[nlit] << std::endl;
+        d_curr_range = d_lit_to_range[nlit];
+      }
+      //set the range
+      d_has_range = true;
+    }
+  }else{
+    Message() << "Could not find literal " << nlit << " for range " << d_range << std::endl;
+    exit(0);
+  }
+}
+
+void BoundedIntegers::RangeModel::allocateRange() {
+  d_curr_max++;
+  int newBound = d_curr_max;
+  Trace("bound-integers-proc") << "Allocate range bound " << newBound << " for " << d_range << std::endl;
+  //TODO: newBound should be chosen in a smarter way
+  Node ltr = NodeManager::currentNM()->mkNode( LEQ, d_range, NodeManager::currentNM()->mkConst( Rational(newBound) ) );
+  ltr = Rewriter::rewrite( ltr );
+  Trace("bound-integers-lemma") << " *** bound int: split on " << ltr << std::endl;
+  d_bi->getQuantifiersEngine()->getOutputChannel().split( ltr );
+  Node ltr_lit = ltr.getKind()==NOT ? ltr[0] : ltr;
+  d_range_literal[newBound] = ltr_lit;
+  d_lit_to_range[ltr_lit] = newBound;
+  d_lit_to_pol[ltr_lit] = ltr.getKind()!=NOT;
+  //register with bounded integers
+  d_bi->addLiteralFromRange(ltr_lit, d_range);
+}
+
+Node BoundedIntegers::RangeModel::getNextDecisionRequest() {
+  //request the current cardinality as a decision literal, if not already asserted
+  for( std::map< Node, int >::iterator it = d_lit_to_range.begin(); it != d_lit_to_range.end(); ++it ){
+    int i = it->second;
+    if( !d_has_range || i<d_curr_range ){
+      Node rn = it->first;
+      Assert( !rn.isNull() );
+      if( d_range_assertions.find( rn )==d_range_assertions.end() ){
+        if (!d_lit_to_pol[it->first]) {
+          rn = rn.negate();
+        }
+        Trace("bound-integers-dec") << "For " << d_range << ", make decision " << rn << " to make range " << i << std::endl;
+        return rn;
+      }
+    }
+  }
+  return Node::null();
+}
+
+
+BoundedIntegers::BoundedIntegers(context::Context* c, QuantifiersEngine* qe) :
+QuantifiersModule(qe), d_assertions(c){
+
+}
 
+bool BoundedIntegers::isBound( Node f, Node v ) {
+  return std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end();
+}
+
+bool BoundedIntegers::hasNonBoundVar( Node f, Node b ) {
+  if( b.getKind()==BOUND_VARIABLE ){
+    if( isBound( f, b ) ){
+      return true;
+    }
+  }else{
+    for( unsigned i=0; i<b.getNumChildren(); i++ ){
+      if( hasNonBoundVar( f, b[i] ) ){
+        return true;
+      }
+    }
+  }
+  return false;
 }
 
 void BoundedIntegers::processLiteral( Node f, Node lit, bool pol ) {
   if( lit.getKind()==GEQ && lit[0].getType().isInteger() ){
     std::map< Node, Node > msum;
     if (QuantArith::getMonomialSumLit( lit, msum )){
-      Trace("bound-integers") << "Literal " << lit << " is monomial sum : " << std::endl;
+      Trace("bound-integers") << "Literal (polarity = " << pol << ") " << lit << " is monomial sum : " << std::endl;
       for(std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
         Trace("bound-integers") << "  ";
         if( !it->second.isNull() ){
@@ -48,7 +157,27 @@ void BoundedIntegers::processLiteral( Node f, Node lit, bool pol ) {
         if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE ){
           Node veq;
           if( QuantArith::isolate( it->first, msum, veq, GEQ ) ){
-            Trace("bound-integers") << "Isolated for " << it->first << " : " << veq << std::endl;
+            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-integers") << "Isolated for " << it->first << " : (" << n1 << " >= " << n2 << ")" << std::endl;
+            Node bv = n1.getKind()==BOUND_VARIABLE ? n1 : n2;
+            if( !isBound( f, bv ) ){
+              if( !hasNonBoundVar( f, n1.getKind()==BOUND_VARIABLE ? n2 : n1 ) ) {
+                Trace("bound-integers") << "The bound is relevant." << std::endl;
+                d_bounds[n1.getKind()==BOUND_VARIABLE ? 0 : 1][f][bv] = (n1.getKind()==BOUND_VARIABLE ? n2 : n1);
+              }
+            }
           }
         }
       }
@@ -76,6 +205,15 @@ void BoundedIntegers::check( Theory::Effort e ) {
 
 }
 
+
+void BoundedIntegers::addLiteralFromRange( Node lit, Node r ) {
+  d_lit_to_ranges[lit].push_back(r);
+  //check if it is already asserted?
+  if(d_assertions.find(lit)!=d_assertions.end()){
+    d_rms[r]->assertNode( d_assertions[lit] ? lit : lit.negate() );
+  }
+}
+
 void BoundedIntegers::registerQuantifier( Node f ) {
   Trace("bound-integers") << "Register quantifier " << f << std::endl;
   bool hasIntType = false;
@@ -86,14 +224,68 @@ void BoundedIntegers::registerQuantifier( Node f ) {
     }
   }
   if( hasIntType ){
-    process( f, f[1], true );
+    bool success;
+    do{
+      success = false;
+      process( f, f[1], true );
+      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);
+            success = true;
+          }
+        }
+      }
+    }while( success );
+    Trace("bound-integers") << "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 );
+      Trace("bound-integers") << "  " << d_bounds[0][f][v] << " <= " << v << " <= " << d_bounds[1][f][v] << " (range is " << d_range[f][v] << ")" << std::endl;
+    }
+    if( d_set[f].size()==f[0].getNumChildren() ){
+      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( std::find(d_ranges.begin(), d_ranges.end(), r)==d_ranges.end() ){
+          d_ranges.push_back( r );
+          d_rms[r] = new RangeModel(this, r, d_quantEngine->getSatContext() );
+          d_rms[r]->initialize();
+        }
+      }
+    }
   }
 }
 
 void BoundedIntegers::assertNode( Node n ) {
-
+  Trace("bound-integers-assert") << "Assert " << n << std::endl;
+  Node nlit = n.getKind()==NOT ? n[0] : n;
+  if( d_lit_to_ranges.find(nlit)!=d_lit_to_ranges.end() ){
+    Trace("bound-integers-assert") << "This is the bounding literal for " << d_lit_to_ranges[nlit].size() << " ranges." << std::endl;
+    for( unsigned i=0; i<d_lit_to_ranges[nlit].size(); i++) {
+      Node r = d_lit_to_ranges[nlit][i];
+      Trace("bound-integers-assert") << "  ...this is a bounding literal for " << r << std::endl;
+      d_rms[r]->assertNode( n );
+    }
+  }
+  d_assertions[nlit] = n.getKind()!=NOT;
 }
 
 Node BoundedIntegers::getNextDecisionRequest() {
+  Trace("bound-integers-dec") << "bi: Get next decision request?" << std::endl;
+  for( unsigned i=0; i<d_ranges.size(); i++) {
+    Node d = d_rms[d_ranges[i]]->getNextDecisionRequest();
+    if (!d.isNull()) {
+      return d;
+    }
+  }
   return Node::null();
 }
+
+
+Node BoundedIntegers::getValueInModel( Node n ) {
+  return d_quantEngine->getModel()->getValue( n );
+}
\ No newline at end of file
diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h
index 570e27a10..4445493c9 100755
--- a/src/theory/quantifiers/bounded_integers.h
+++ b/src/theory/quantifiers/bounded_integers.h
@@ -18,26 +18,73 @@
 
 #include "theory/quantifiers_engine.h"
 
+#include "context/context.h"
+#include "context/context_mm.h"
+#include "context/cdchunk_list.h"
+
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
 class BoundedIntegers : public QuantifiersModule
 {
+  typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
+  typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
+  typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
 private:
-  std::map< Node, std::map< Node, Node > > d_lowers;
-  std::map< Node, std::map< Node, Node > > d_uppers;
-  std::map< Node, std::map< Node, bool > > d_set;
+  //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];
+  std::map< Node, std::vector< Node > > d_set;
+  std::map< Node, std::map< Node, Node > > d_range;
   void hasFreeVar( Node f, Node n );
   void process( Node f, Node n, bool pol );
   void processLiteral( Node f, Node lit, bool pol );
+  std::vector< Node > d_bound_quants;
+private:
+  class RangeModel {
+  private:
+    BoundedIntegers * d_bi;
+    void allocateRange();
+  public:
+    RangeModel(BoundedIntegers * bi, Node r, context::Context* c) : d_bi(bi),
+      d_range(r), d_curr_max(-1), d_range_assertions(c), d_has_range(c,false), d_curr_range(c,-1) {}
+    Node d_range;
+    int d_curr_max;
+    std::map< int, Node > d_range_literal;
+    std::map< Node, bool > d_lit_to_pol;
+    std::map< Node, int > d_lit_to_range;
+    NodeBoolMap d_range_assertions;
+    context::CDO< bool > d_has_range;
+    context::CDO< int > d_curr_range;
+    void initialize();
+    void assertNode(Node n);
+    Node getNextDecisionRequest();
+  };
+  Node getValueInModel( Node n );
+private:
+  //information for minimizing ranges
+  std::vector< Node > d_ranges;
+  //map to range model objects
+  std::map< Node, RangeModel * > d_rms;
+  //literal to range
+  std::map< Node, std::vector< Node > > d_lit_to_ranges;
+  //list of currently asserted arithmetic literals
+  NodeBoolMap d_assertions;
+private:
+  void addLiteralFromRange( Node lit, Node r );
 public:
-  BoundedIntegers( QuantifiersEngine* qe );
+  BoundedIntegers( context::Context* c, QuantifiersEngine* qe );
 
   void check( Theory::Effort e );
   void registerQuantifier( Node f );
   void assertNode( Node n );
   Node getNextDecisionRequest();
+  Node getLowerBound( Node f, Node v ){ return d_bounds[0][f][v]; }
+  Node getUpperBound( Node f, Node v ){ return d_bounds[1][f][v]; }
+  Node getLowerBoundValue( Node f, Node v ){ return getValueInModel( d_bounds[0][f][v] ); }
+  Node getUpperBoundValue( Node f, Node v ){ return getValueInModel( d_bounds[1][f][v] ); }
 };
 
 }
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 4ce9dba21..4904368a2 100755
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -535,31 +535,33 @@ int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c
   Trace("fmc-exh") << "Exhaustive instantiate based on index " << c_index << " : " << c << " ";
   debugPrintCond("fmc-exh", c, true);
   Trace("fmc-exh")<< std::endl;
-  if( riter.setQuantifier( f ) ){
+  if( riter.setQuantifier( d_qe, f ) ){
     std::vector< RepDomain > dom;
     for (unsigned i=0; i<c.getNumChildren(); i++) {
       TypeNode tn = c[i].getType();
       if( d_rep_ids.find(tn)!=d_rep_ids.end() ){
-        RepDomain rd;
+        //RepDomain rd;
         if( isStar(c[i]) ){
           //add the full range
-          for( std::map< Node, int >::iterator it = d_rep_ids[tn].begin();
-               it != d_rep_ids[tn].end(); ++it ){
-            rd.push_back(it->second);
-          }
+          //for( std::map< Node, int >::iterator it = d_rep_ids[tn].begin();
+          //     it != d_rep_ids[tn].end(); ++it ){
+          //  rd.push_back(it->second);
+          //}
         }else{
           if (d_rep_ids[tn].find(c[i])!=d_rep_ids[tn].end()) {
-            rd.push_back(d_rep_ids[tn][c[i]]);
+            //rd.push_back(d_rep_ids[tn][c[i]]);
+            riter.d_domain[i].clear();
+            riter.d_domain[i].push_back(d_rep_ids[tn][c[i]]);
           }else{
             return -1;
           }
         }
-        dom.push_back(rd);
+        //dom.push_back(rd);
       }else{
         return -1;
       }
     }
-    riter.setDomain(dom);
+    //riter.setDomain(dom);
     //now do full iteration
     while( !riter.isFinished() ){
       Trace("fmc-exh-debug") << "Inst : ";
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 25e07de5d..677f0c94b 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -69,7 +69,7 @@ void ModelEngineBuilder::debugModel( FirstOrderModel* fm ){
         vars.push_back( f[0][j] );
       }
       RepSetIterator riter( &(fm->d_rep_set) );
-      riter.setQuantifier( f );
+      riter.setQuantifier( d_qe, f );
       while( !riter.isFinished() ){
         std::vector< Node > terms;
         for( int i=0; i<riter.getNumTerms(); i++ ){
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 90b8c62ba..bc900d9a9 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -216,7 +216,7 @@ int ModelEngine::checkModel( int checkOption ){
         }
         //if we need to consider this quantifier on this iteration
         if( checkQuant ){
-          addedLemmas += exhaustiveInstantiate( f, optUseRelevantDomain(), e );
+          addedLemmas += exhaustiveInstantiate( f, e );
           if( Trace.isOn("model-engine-warn") ){
             if( addedLemmas>10000 ){
               Debug("fmf-exit") << std::endl;
@@ -241,7 +241,7 @@ int ModelEngine::checkModel( int checkOption ){
   return addedLemmas;
 }
 
-int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain, int effort ){
+int ModelEngine::exhaustiveInstantiate( Node f, int effort ){
   int addedLemmas = 0;
 
   bool useModel = d_builder->optUseModel();
@@ -263,18 +263,16 @@ int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain, int effor
     Debug("inst-fmf-ei") << std::endl;
     //create a rep set iterator and iterate over the (relevant) domain of the quantifier
     RepSetIterator riter( &(d_quantEngine->getModel()->d_rep_set) );
-    if( riter.setQuantifier( f ) ){
-      Debug("inst-fmf-ei") << "Set domain..." << std::endl;
-      //set the domain for the iterator (the sufficient set of instantiations to try)
-      if( useRelInstDomain ){
-        riter.setDomain( d_rel_domain.d_quant_inst_domain[f] );
-      }
+    if( riter.setQuantifier( d_quantEngine, f ) ){
       Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl;
       d_quantEngine->getModel()->resetEvaluate();
       Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl;
       int tests = 0;
       int triedLemmas = 0;
       while( !riter.isFinished() && ( addedLemmas==0 || !optOneInstPerQuantRound() ) ){
+        for( int i=0; i<(int)riter.d_index.size(); i++ ){
+          Trace("try") << i << " : " << riter.d_index[i] << " : " << riter.getTerm( i ) << std::endl;
+        }
         d_testLemmas++;
         int eval = 0;
         int depIndex;
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index d2cd8807a..d88a36d01 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -54,7 +54,7 @@ private:
   //check model
   int checkModel( int checkOption );
   //exhaustively instantiate quantifier (possibly using mbqi), return number of lemmas produced
-  int exhaustiveInstantiate( Node f, bool useRelInstDomain = false, int effort = 0 );
+  int exhaustiveInstantiate( Node f, int effort = 0 );
 private:
   //temporary statistics
   int d_triedLemmas;
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 6b07a87e0..53f67853b 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -71,7 +71,7 @@ bool QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind
     Rational r = msum[v].isNull() ? Rational(1) : msum[v].getConst<Rational>();
     if ( r.sgn()!=0 ){
       for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
-        if( it->first!=v ){
+        if( it->first.isNull() || it->first!=v ){
           Node m;
           if( !it->first.isNull() ){
             if ( !it->second.isNull() ){
@@ -111,6 +111,12 @@ Node QuantArith::negate( Node t ) {
   return tt;
 }
 
+Node QuantArith::offset( Node t, int i ) {
+  Node tt = NodeManager::currentNM()->mkNode( PLUS, NodeManager::currentNM()->mkConst( Rational(i) ), t );
+  tt = Rewriter::rewrite( tt );
+  return tt;
+}
+
 
 void QuantRelevance::registerQuantifier( Node f ){
   //compute symbols in f
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index d248a8999..86c7bc3a0 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -36,6 +36,7 @@ public:
   static bool getMonomialSumLit( Node lit, std::map< Node, Node >& msum );
   static bool isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k );
   static Node negate( Node t );
+  static Node offset( Node t, int i );
 };
 
 
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 5c24f89b7..ef8169433 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -62,7 +62,7 @@ d_lemmas_produced_c(u){
     d_model_engine = new quantifiers::ModelEngine( c, this );
     d_modules.push_back( d_model_engine );
 
-    d_bint = new quantifiers::BoundedIntegers( this );
+    d_bint = new quantifiers::BoundedIntegers( c, this );
     d_modules.push_back( d_bint );
   }else{
     d_model_engine = NULL;
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 85da53087..2ff2100b2 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -158,6 +158,8 @@ public:
   void getPhaseReqTerms( Node f, std::vector< Node >& nodes );
   /** get efficient e-matching utility */
   EfficientEMatcher* getEfficientEMatcher() { return d_eem; }
+  /** get bounded integers utility */
+  quantifiers::BoundedIntegers * getBoundedIntegers() { return d_bint; }
 public:
   /** initialize */
   void finishInit();
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index f6da32bbf..fe3e39d45 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/rep_set.h"
 #include "theory/type_enumerator.h"
+#include "theory/quantifiers/bounded_integers.h"
 
 using namespace std;
 using namespace CVC4;
@@ -99,25 +100,33 @@ RepSetIterator::RepSetIterator( RepSet* rs ) : d_rep_set( rs ){
 
 }
 
-bool RepSetIterator::setQuantifier( Node f ){
+int RepSetIterator::domainSize( int i ) {
+  if( d_enum_type[i]==ENUM_DOMAIN_ELEMENTS ){
+    return d_domain[i].size();
+  }else{
+    return d_domain[i][0];
+  }
+}
+
+bool RepSetIterator::setQuantifier( QuantifiersEngine * qe, Node f ){
   Assert( d_types.empty() );
   //store indicies
   for( size_t i=0; i<f[0].getNumChildren(); i++ ){
     d_types.push_back( f[0][i].getType() );
   }
-  return initialize();
+  return initialize(qe, f);
 }
 
-bool RepSetIterator::setFunctionDomain( Node op ){
+bool RepSetIterator::setFunctionDomain( QuantifiersEngine * qe, Node op ){
   Assert( d_types.empty() );
   TypeNode tn = op.getType();
   for( size_t i=0; i<tn.getNumChildren()-1; i++ ){
     d_types.push_back( tn[i] );
   }
-  return initialize();
+  return initialize(qe, Node::null());
 }
 
-bool RepSetIterator::initialize(){
+bool RepSetIterator::initialize(QuantifiersEngine * qe, Node f){
   for( size_t i=0; i<d_types.size(); i++ ){
     d_index.push_back( 0 );
     //store default index order
@@ -126,13 +135,48 @@ 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" );
         Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl;
         d_rep_set->add( var );
       }
-    }else if( tn.isInteger() || tn.isReal() ){
+    }else if( tn.isInteger() ){
+      //check if it is bound
+      if( !f.isNull() && qe && qe->getBoundedIntegers() ){
+        Node l = qe->getBoundedIntegers()->getLowerBoundValue( f, f[0][i] );
+        Node u = qe->getBoundedIntegers()->getUpperBoundValue( f, f[0][i] );
+        if( !l.isNull() && !u.isNull() ){
+          Trace("bound-int-reps") << "Can limit bounds of " << f[0][i] << " to " << l << "..." << u << std::endl;
+          Node range = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MINUS, u, l ) );
+          Node ra = Rewriter::rewrite( NodeManager::currentNM()->mkNode( LEQ, range, NodeManager::currentNM()->mkConst( Rational( 9999 ) ) ) );
+          if( ra==NodeManager::currentNM()->mkConst(true) ){
+            long rr = range.getConst<Rational>().getNumerator().getLong()+1;
+            if (rr<0) {
+              Trace("bound-int-reps")  << "Empty bound range." << std::endl;
+              //empty
+              d_enum_type.push_back( ENUM_DOMAIN_ELEMENTS );
+            }else{
+              Trace("bound-int-reps")  << "Actual bound range is " << rr << std::endl;
+              d_lower_bounds[i] = l;
+              d_domain[i].push_back( (int)rr );
+              d_enum_type.push_back( ENUM_RANGE );
+            }
+            isSet = true;
+          }else{
+            Trace("fmf-incomplete") << "Incomplete because of integer quantification, bounds are too big." << std::endl;
+            d_incomplete = true;
+          }
+        }else{
+          Trace("fmf-incomplete") << "Incomplete because of integer quantification, no bounds found." << std::endl;
+          d_incomplete = true;
+        }
+      }else{
+        Trace("fmf-incomplete") << "Incomplete because of integer quantification." << std::endl;
+        d_incomplete = 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
@@ -142,12 +186,15 @@ bool RepSetIterator::initialize(){
       Trace("fmf-incomplete") << "Incomplete because of unknown type " << tn << std::endl;
       d_incomplete = true;
     }
-    if( d_rep_set->hasType( tn ) ){
-      for( size_t j=0; j<d_rep_set->d_type_reps[tn].size(); j++ ){
-        d_domain[i].push_back( j );
+    if( !isSet ){
+      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++ ){
+          d_domain[i].push_back( j );
+        }
+      }else{
+        return false;
       }
-    }else{
-      return false;
     }
   }
   return true;
@@ -161,7 +208,7 @@ void RepSetIterator::setIndexOrder( std::vector< int >& indexOrder ){
     d_var_order[d_index_order[i]] = i;
   }
 }
-
+/*
 void RepSetIterator::setDomain( std::vector< RepDomain >& domain ){
   d_domain.clear();
   d_domain.insert( d_domain.begin(), domain.begin(), domain.end() );
@@ -172,14 +219,14 @@ void RepSetIterator::setDomain( std::vector< RepDomain >& domain ){
     }
   }
 }
-
+*/
 void RepSetIterator::increment2( int counter ){
   Assert( !isFinished() );
 #ifdef DISABLE_EVAL_SKIP_MULTIPLE
   counter = (int)d_index.size()-1;
 #endif
   //increment d_index
-  while( counter>=0 && d_index[counter]==(int)(d_domain[counter].size()-1) ){
+  while( counter>=0 && d_index[counter]==(int)(domainSize(counter)-1) ){
     counter--;
   }
   if( counter==-1 ){
@@ -203,10 +250,17 @@ bool RepSetIterator::isFinished(){
 }
 
 Node RepSetIterator::getTerm( int i ){
-  TypeNode tn = d_types[d_index_order[i]];
-  Assert( d_rep_set->d_type_reps.find( tn )!=d_rep_set->d_type_reps.end() );
   int index = d_index_order[i];
-  return d_rep_set->d_type_reps[tn][d_domain[index][d_index[index]]];
+  if( d_enum_type[index]==ENUM_DOMAIN_ELEMENTS ){
+    TypeNode tn = d_types[index];
+    Assert( d_rep_set->d_type_reps.find( tn )!=d_rep_set->d_type_reps.end() );
+    return d_rep_set->d_type_reps[tn][d_domain[index][d_index[index]]];
+  }else{
+    Node t = NodeManager::currentNM()->mkNode(PLUS, d_lower_bounds[index],
+                                                    NodeManager::currentNM()->mkConst( Rational(d_index[index]) ) );
+    t = Rewriter::rewrite( t );
+    return t;
+  }
 }
 
 void RepSetIterator::debugPrint( const char* c ){
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index 24fa7473e..b92d9d2c6 100644
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -23,6 +23,8 @@
 namespace CVC4 {
 namespace theory {
 
+class QuantifiersEngine;
+
 /** this class stores a representative set */
 class RepSet {
 public:
@@ -53,15 +55,26 @@ typedef std::vector< int > RepDomain;
 /** this class iterates over a RepSet */
 class RepSetIterator {
 private:
+  enum {
+    ENUM_DOMAIN_ELEMENTS,
+    ENUM_RANGE,
+  };
+
   //initialize function
-  bool initialize();
+  bool initialize(QuantifiersEngine * qe, Node f);
+  //enumeration type?
+  std::vector< int > d_enum_type;
+  //for enum ranges
+  std::map< int, Node > d_lower_bounds;
+  //domain size
+  int domainSize( int i );
 public:
   RepSetIterator( RepSet* rs );
   ~RepSetIterator(){}
   //set that this iterator will be iterating over instantiations for a quantifier
-  bool setQuantifier( Node f );
+  bool setQuantifier( QuantifiersEngine * qe, Node f );
   //set that this iterator will be iterating over the domain of a function
-  bool setFunctionDomain( Node op );
+  bool setFunctionDomain( QuantifiersEngine * qe, Node op );
 public:
   //pointer to model
   RepSet* d_rep_set;
@@ -90,7 +103,7 @@ public:
   /** set index order */
   void setIndexOrder( std::vector< int >& indexOrder );
   /** set domain */
-  void setDomain( std::vector< RepDomain >& domain );
+  //void setDomain( std::vector< RepDomain >& domain );
   /** increment the iterator at index=counter */
   void increment2( int counter );
   /** increment the iterator */
-- 
2.30.2