Significant work on bounded integer quantification to handle non-trivial bounds. Refactoring of InstConstantAttribute to be internal to TermDb.

32 files changed, 548 insertions, 342 deletions

diff --git a/src/smt/options b/src/smt/options
index 2680f4105..e5f9c2eaf 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -24,6 +24,8 @@ common-option produceModels produce-models -m --produce-models bool :default fal
  support the get-value and get-model commands
 option checkModels check-models --check-models bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions
+option dumpModels --dump-models bool :default false
+ output models after every SAT/INVALID/UNKNOWN response
 option proof produce-proofs --proof bool :default false :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  turn on proof generation
 # this is just a placeholder for later; it doesn't show up in command-line options listings
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 060f6dbba..3b141bf9e 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1376,7 +1376,7 @@ Constraint TheoryArithPrivate::constraintFromFactQueue(){
   Assert(!done());
   TNode assertion = get();
 
-  if( options::finiteModelFind() ){
+  if( d_quantEngine && d_quantEngine->getBoundedIntegers() ){
     d_quantEngine->getBoundedIntegers()->assertNode(assertion);
   }
 
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index aeac3c79b..4492e6d2d 100755
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/bounded_integers.h"

 #include "theory/quantifiers/quant_util.h"

 #include "theory/quantifiers/first_order_model.h"

+#include "theory/quantifiers/model_engine.h"

 

 using namespace CVC4;

 using namespace std;

@@ -26,14 +27,14 @@ 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;

+  Trace("bound-int-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;

+  Trace("bound-int-debug") << "Literal " << ltr_lit << " is literal for " << d_range << std::endl;

   d_bi->addLiteralFromRange(ltr_lit, d_range);

 }

 

@@ -41,9 +42,9 @@ 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;

+    Trace("bound-int-assert") << "With polarity = " << pol << " (req "<< d_lit_to_pol[nlit] << ")";

+    Trace("bound-int-assert") << ", found literal " << nlit;

+    Trace("bound-int-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?

@@ -61,7 +62,7 @@ void BoundedIntegers::RangeModel::assertNode(Node n) {
       }

     }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;

+        Trace("bound-int-bound") << "Successfully bound " << d_range << " to " << d_lit_to_range[nlit] << std::endl;

         d_curr_range = d_lit_to_range[nlit];

       }

       //set the range

@@ -76,11 +77,11 @@ void BoundedIntegers::RangeModel::assertNode(Node n) {
 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;

+  Trace("bound-int-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;

+  Trace("bound-int-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;

@@ -101,7 +102,7 @@ Node BoundedIntegers::RangeModel::getNextDecisionRequest() {
         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;

+        Trace("bound-int-dec") << "For " << d_range << ", make decision " << rn << " to make range " << i << std::endl;

         return rn;

       }

     }

@@ -121,7 +122,7 @@ bool BoundedIntegers::isBound( Node f, Node v ) {
 

 bool BoundedIntegers::hasNonBoundVar( Node f, Node b ) {

   if( b.getKind()==BOUND_VARIABLE ){

-    if( isBound( f, b ) ){

+    if( !isBound( f, b ) ){

       return true;

     }

   }else{

@@ -138,23 +139,23 @@ 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-debug") << "Literal (polarity = " << pol << ") " << lit << " is monomial sum : " << std::endl;

+      Trace("bound-int-debug") << "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-debug") << "  ";

+        Trace("bound-int-debug") << "  ";

         if( !it->second.isNull() ){

-          Trace("bound-integers-debug") << it->second;

+          Trace("bound-int-debug") << it->second;

           if( !it->first.isNull() ){

-            Trace("bound-integers-debug") << " * ";

+            Trace("bound-int-debug") << " * ";

           }

         }

         if( !it->first.isNull() ){

-          Trace("bound-integers-debug") << it->first;

+          Trace("bound-int-debug") << it->first;

         }

-        Trace("bound-integers-debug") << std::endl;

+        Trace("bound-int-debug") << std::endl;

       }

-      Trace("bound-integers-debug") << std::endl;

+      Trace("bound-int-debug") << std::endl;

       for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){

-        if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE ){

+        if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE && !isBound( f, it->first ) ){

           Node veq;

           if( QuantArith::isolate( it->first, msum, veq, GEQ ) ){

             Node n1 = veq[0];

@@ -170,11 +171,11 @@ void BoundedIntegers::processLiteral( Node f, Node lit, bool pol ) {
               }

               veq = NodeManager::currentNM()->mkNode( GEQ, n1, n2 );

             }

-            Trace("bound-integers-debug") << "Isolated for " << it->first << " : (" << n1 << " >= " << n2 << ")" << std::endl;

+            Trace("bound-int-debug") << "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-debug") << "The bound is relevant." << std::endl;

+                Trace("bound-int-debug") << "The bound is relevant." << std::endl;

                 d_bounds[n1.getKind()==BOUND_VARIABLE ? 0 : 1][f][bv] = (n1.getKind()==BOUND_VARIABLE ? n2 : n1);

               }

             }

@@ -215,12 +216,13 @@ void BoundedIntegers::addLiteralFromRange( Node lit, Node r ) {
 }

 

 void BoundedIntegers::registerQuantifier( Node f ) {

-  Trace("bound-integers") << "Register quantifier " << f << std::endl;

+  Trace("bound-int") << "Register quantifier " << f << std::endl;

   bool hasIntType = false;

+  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;

-      break;

     }

   }

   if( hasIntType ){

@@ -233,24 +235,56 @@ void BoundedIntegers::registerQuantifier( Node f ) {
         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]);

             success = true;

           }

         }

       }

     }while( success );

-    Trace("bound-integers") << "Bounds are : " << std::endl;

+    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 );

-      Trace("bound-integers") << "  " << d_bounds[0][f][v] << " <= " << v << " <= " << d_bounds[1][f][v] << " (range is " << d_range[f][v] << ")" << std::endl;

+      Trace("bound-int") << "  " << 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( quantifiers::TermDb::hasBoundVarAttr(r) ){

+          //introduce a new bound

+          Node new_range = NodeManager::currentNM()->mkSkolem( "bir_$$", r.getType(), "bound for term" );

+          /*

+          std::vector< Node > bvs;

+          quantifiers::TermDb::getBoundVars(r, bvs);

+          Assert(bvs.size()>0);

+          Node body = NodeManager::currentNM()->mkNode( LEQ, r, new_range );

+          std::vector< Node > children;

+          //get all the other bounds

+          for( unsigned j=0; j<bvs.size(); j++) {

+            Node l = NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkConst(Rational(0)), bvs[j]);

+            Node u = NodeManager::currentNM()->mkNode( LEQ, bvs[j], d_range[f][bvs[j]] );

+            children.push_back(l);

+            children.push_back(u);

+          }

+          Node antec = NodeManager::currentNM()->mkNode( AND, children );

+          body = NodeManager::currentNM()->mkNode( IMPLIES, antec, body );

+

+          Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs );

+

+          Node lem = NodeManager::currentNM()->mkNode( FORALL, bvl, body );

+          Trace("bound-int") << "For " << v << ", the quantified formula " << lem << " will be used to minimize the bound." << std::endl;

+          Trace("bound-int-lemma") << " *** bound int: bounding quantified lemma " << lem << std::endl;

+          d_quantEngine->getOutputChannel().lemma( lem );

+          */

+          d_nground_range[f][v] = d_range[f][v];

+          d_range[f][v] = new_range;

+          r = new_range;

+        }

         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 << std::endl;

           d_ranges.push_back( r );

           d_rms[r] = new RangeModel(this, r, d_quantEngine->getSatContext() );

           d_rms[r]->initialize();

@@ -261,13 +295,13 @@ void BoundedIntegers::registerQuantifier( Node f ) {
 }

 

 void BoundedIntegers::assertNode( Node n ) {

-  Trace("bound-integers-assert") << "Assert " << n << std::endl;

+  Trace("bound-int-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;

+    Trace("bound-int-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;

+      Trace("bound-int-assert") << "  ...this is a bounding literal for " << r << std::endl;

       d_rms[r]->assertNode( n );

     }

   }

@@ -275,7 +309,7 @@ void BoundedIntegers::assertNode( Node n ) {
 }

 

 Node BoundedIntegers::getNextDecisionRequest() {

-  Trace("bound-integers-dec") << "bi: Get next decision request?" << std::endl;

+  Trace("bound-int-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()) {

@@ -285,7 +319,48 @@ Node BoundedIntegers::getNextDecisionRequest() {
   return Node::null();

 }

 

+void BoundedIntegers::getBoundValues( 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

+    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);

+      l = Node::null();

+      u = Node::null();

+      return;

+    }else{

+      u = u.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );

+      l = l.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );

+    }

+  }

+  Trace("bound-int-rsi") << "Get value in model for..." << l << " and " << u << std::endl;

+  l = d_quantEngine->getModelEngine()->getModelBuilder()->getCurrentModelValue( d_quantEngine->getModel(), l );

+  u = d_quantEngine->getModelEngine()->getModelBuilder()->getCurrentModelValue( d_quantEngine->getModel(), u );

+  Trace("bound-int-rsi") << "Value is " << l << " ... " << u << std::endl;

+  return;

+}

 

-Node BoundedIntegers::getValueInModel( Node n ) {

-  return d_quantEngine->getModel()->getValue( n );

+bool BoundedIntegers::isGroundRange(Node f, Node v) {

+  return isBoundVar(f,v) && !quantifiers::TermDb::hasBoundVarAttr(getLowerBound(f,v)) && !quantifiers::TermDb::hasBoundVarAttr(getUpperBound(f,v));

 }
\ No newline at end of file
diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h
index 4445493c9..f40e2180c 100755
--- a/src/theory/quantifiers/bounded_integers.h
+++ b/src/theory/quantifiers/bounded_integers.h
@@ -24,8 +24,12 @@
 

 namespace CVC4 {

 namespace theory {

+

+class RepSetIterator;

+

 namespace quantifiers {

 

+

 class BoundedIntegers : public QuantifiersModule

 {

   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;

@@ -37,7 +41,9 @@ private:
   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::vector< int > > d_set_nums;

   std::map< Node, std::map< Node, Node > > d_range;

+  std::map< Node, std::map< Node, Node > > d_nground_range;

   void hasFreeVar( Node f, Node n );

   void process( Node f, Node n, bool pol );

   void processLiteral( Node f, Node lit, bool pol );

@@ -62,7 +68,6 @@ private:
     void assertNode(Node n);

     Node getNextDecisionRequest();

   };

-  Node getValueInModel( Node n );

 private:

   //information for minimizing ranges

   std::vector< Node > d_ranges;

@@ -73,6 +78,25 @@ private:
   //list of currently asserted arithmetic literals

   NodeBoolMap d_assertions;

 private:

+  //class to store whether bounding lemmas have been added

+  class BoundInstTrie

+  {

+  public:

+    std::map< Node, BoundInstTrie > d_children;

+    bool hasInstantiated( std::vector< Node > & vals, int index = 0, bool madeNew = false ){

+      if( index>=(int)vals.size() ){

+        return !madeNew;

+      }else{

+        Node n = vals[index];

+        if( d_children.find(n)==d_children.end() ){

+          madeNew = true;

+        }

+        return d_children[n].hasInstantiated(vals,index+1,madeNew);

+      }

+    }

+  };

+  std::map< Node, std::map< Node, BoundInstTrie > > d_bnd_it;

+private:

   void addLiteralFromRange( Node lit, Node r );

 public:

   BoundedIntegers( context::Context* c, QuantifiersEngine* qe );

@@ -81,10 +105,14 @@ public:
   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]; }

-  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] ); }

+  void getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u );

+  bool isGroundRange(Node f, Node v);

 };

 

 }

diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 0c423de19..6c6a80b90 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -27,7 +27,7 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::inst;
 
 bool CandidateGenerator::isLegalCandidate( Node n ){
-  return ( !n.getAttribute(NoMatchAttribute()) && ( !options::cbqi() || !n.hasAttribute(InstConstantAttribute()) ) );
+  return ( !n.getAttribute(NoMatchAttribute()) && ( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(n) ) );
 }
 
 void CandidateGeneratorQueue::addCandidate( Node n ) {
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index bba9c0163..a11729519 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -397,7 +397,7 @@ struct sortGetMaxVariableNum {
   int computeMaxVariableNum( Node n ){
     if( n.getKind()==INST_CONSTANT ){
       return n.getAttribute(InstVarNumAttribute());
-    }else if( n.hasAttribute(InstConstantAttribute()) ){
+    }else if( TermDb::hasInstConstAttr(n) ){
       int maxVal = -1;
       for( int i=0; i<(int)n.getNumChildren(); i++ ){
         int val = getMaxVariableNum( n[i] );
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 445f0d6c0..b5d4648a1 100755
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -139,7 +139,7 @@ bool Def::addEntry( FullModelChecker * m, Node c, Node v) {
   }

 }

 

-Node Def::evaluate( FullModelChecker * m, std::vector<Node> inst ) {

+Node Def::evaluate( FullModelChecker * m, std::vector<Node>& inst ) {

   int gindex = d_et.getGeneralizationIndex(m, inst);

   if (gindex!=-1) {

     return d_value[gindex];

@@ -148,7 +148,7 @@ Node Def::evaluate( FullModelChecker * m, std::vector<Node> inst ) {
   }

 }

 

-int Def::getGeneralizationIndex( FullModelChecker * m, std::vector<Node> inst ) {

+int Def::getGeneralizationIndex( FullModelChecker * m, std::vector<Node>& inst ) {

   return d_et.getGeneralizationIndex(m, inst);

 }

 

@@ -163,7 +163,7 @@ void Def::simplify(FullModelChecker * m) {
   d_et.reset();

   for (unsigned i=0; i<d_status.size(); i++) {

     if( d_status[i]!=status_redundant ){

-      addEntry(m, d_cond[i], d_value[i]);

+      addEntry(m, cond[i], value[i]);

     }

   }

   d_status.clear();

@@ -435,108 +435,112 @@ void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) {
 

 bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort, int & lemmas ) {

   Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl;

-  if (effort==0) {

-    //register the quantifier

-    if (d_quant_cond.find(f)==d_quant_cond.end()) {

-      std::vector< TypeNode > types;

-      for(unsigned i=0; i<f[0].getNumChildren(); i++){

-        types.push_back(f[0][i].getType());

-        d_quant_var_id[f][f[0][i]] = i;

-      }

-      TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->booleanType() );

-      Node op = NodeManager::currentNM()->mkSkolem( "fmc_$$", typ, "op created for full-model checking" );

-      d_quant_cond[f] = op;

-    }

-

-    //model check the quantifier

-    doCheck(fm, f, d_quant_models[f], f[1]);

-    Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl;

-    d_quant_models[f].debugPrint("fmc", Node::null(), this);

-    Trace("fmc") << std::endl;

-    //consider all entries going to false

-    for (unsigned i=0; i<d_quant_models[f].d_cond.size(); i++) {

-      if( d_quant_models[f].d_value[i]!=d_true) {

-        Trace("fmc-inst") << "Instantiate based on " << d_quant_models[f].d_cond[i] << "..." << std::endl;

-        bool hasStar = false;

-        std::vector< Node > inst;

-        for (unsigned j=0; j<d_quant_models[f].d_cond[i].getNumChildren(); j++) {

-          if (isStar(d_quant_models[f].d_cond[i][j])) {

-            hasStar = true;

-            inst.push_back(getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType()));

-          }else{

-            inst.push_back(d_quant_models[f].d_cond[i][j]);

-          }

+  if (!options::fmfModelBasedInst()) {

+    return false;

+  }else{

+    if (effort==0) {

+      //register the quantifier

+      if (d_quant_cond.find(f)==d_quant_cond.end()) {

+        std::vector< TypeNode > types;

+        for(unsigned i=0; i<f[0].getNumChildren(); i++){

+          types.push_back(f[0][i].getType());

+          d_quant_var_id[f][f[0][i]] = i;

         }

-        bool addInst = true;

-        if( hasStar ){

-          //try obvious (specified by inst)

-          Node ev = d_quant_models[f].evaluate(this, inst);

-          if (ev==d_true) {

-            addInst = false;

-          }

-        }else{

-          //for debugging

-          if (Trace.isOn("fmc-test-inst")) {

-            Node ev = d_quant_models[f].evaluate(this, inst);

-            if( ev==d_true ){

-              std::cout << "WARNING: instantiation was true! " << f << " " << d_quant_models[f].d_cond[i] << std::endl;

-              exit(0);

+        TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->booleanType() );

+        Node op = NodeManager::currentNM()->mkSkolem( "fmc_$$", typ, "op created for full-model checking" );

+        d_quant_cond[f] = op;

+      }

+

+      //model check the quantifier

+      doCheck(fm, f, d_quant_models[f], f[1]);

+      Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl;

+      d_quant_models[f].debugPrint("fmc", Node::null(), this);

+      Trace("fmc") << std::endl;

+      //consider all entries going to false

+      for (unsigned i=0; i<d_quant_models[f].d_cond.size(); i++) {

+        if( d_quant_models[f].d_value[i]!=d_true) {

+          Trace("fmc-inst") << "Instantiate based on " << d_quant_models[f].d_cond[i] << "..." << std::endl;

+          bool hasStar = false;

+          std::vector< Node > inst;

+          for (unsigned j=0; j<d_quant_models[f].d_cond[i].getNumChildren(); j++) {

+            if (isStar(d_quant_models[f].d_cond[i][j])) {

+              hasStar = true;

+              inst.push_back(getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType()));

             }else{

-              Trace("fmc-test-inst") << "...instantiation evaluated to false." << std::endl;

+              inst.push_back(d_quant_models[f].d_cond[i][j]);

             }

           }

-        }

-        if( addInst ){

-          InstMatch m;

-          for( unsigned j=0; j<inst.size(); j++) {

-            m.set( d_qe, f, j, inst[j] );

+          bool addInst = true;

+          if( hasStar ){

+            //try obvious (specified by inst)

+            Node ev = d_quant_models[f].evaluate(this, inst);

+            if (ev==d_true) {

+              addInst = false;

+            }

+          }else{

+            //for debugging

+            if (Trace.isOn("fmc-test-inst")) {

+              Node ev = d_quant_models[f].evaluate(this, inst);

+              if( ev==d_true ){

+                std::cout << "WARNING: instantiation was true! " << f << " " << d_quant_models[f].d_cond[i] << std::endl;

+                exit(0);

+              }else{

+                Trace("fmc-test-inst") << "...instantiation evaluated to false." << std::endl;

+              }

+            }

           }

-          if( d_qe->addInstantiation( f, m ) ){

-            lemmas++;

+          if( addInst ){

+            InstMatch m;

+            for( unsigned j=0; j<inst.size(); j++) {

+              m.set( d_qe, f, j, inst[j] );

+            }

+            if( d_qe->addInstantiation( f, m ) ){

+              lemmas++;

+            }else{

+              //this can happen if evaluation is unknown

+              //might try it next effort level

+              d_star_insts[f].push_back(i);

+            }

           }else{

-            //this can happen if evaluation is unknown

             //might try it next effort level

             d_star_insts[f].push_back(i);

           }

-        }else{

-          //might try it next effort level

-          d_star_insts[f].push_back(i);

         }

       }

-    }

-  }else{

-    if (!d_star_insts[f].empty()) {

-      Trace("fmc-exh") << "Exhaustive instantiate " << f << std::endl;

-      Trace("fmc-exh") << "Definition was : " << std::endl;

-      d_quant_models[f].debugPrint("fmc-exh", Node::null(), this);

-      Trace("fmc-exh") << std::endl;

-      Def temp;

-      //simplify the exceptions?

-      for( int i=(d_star_insts[f].size()-1); i>=0; i--) {

-        //get witness for d_star_insts[f][i]

-        int j = d_star_insts[f][i];

-        if( temp.addEntry( this, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){

-          int lem = exhaustiveInstantiate(fm, f, d_quant_models[f].d_cond[j], j );

-          if( lem==-1 ){

-            //something went wrong, resort to exhaustive instantiation

-            return false;

-          }else{

-            lemmas += lem;

+    }else{

+      if (!d_star_insts[f].empty()) {

+        Trace("fmc-exh") << "Exhaustive instantiate " << f << std::endl;

+        Trace("fmc-exh") << "Definition was : " << std::endl;

+        d_quant_models[f].debugPrint("fmc-exh", Node::null(), this);

+        Trace("fmc-exh") << std::endl;

+        Def temp;

+        //simplify the exceptions?

+        for( int i=(d_star_insts[f].size()-1); i>=0; i--) {

+          //get witness for d_star_insts[f][i]

+          int j = d_star_insts[f][i];

+          if( temp.addEntry( this, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){

+            int lem = exhaustiveInstantiate(fm, f, d_quant_models[f].d_cond[j], j );

+            if( lem==-1 ){

+              //something went wrong, resort to exhaustive instantiation

+              return false;

+            }else{

+              lemmas += lem;

+            }

           }

         }

       }

     }

+    return true;

   }

-  return true;

 }

 

 int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c, int c_index) {

   int addedLemmas = 0;

-  RepSetIterator riter( &(fm->d_rep_set) );

+  RepSetIterator riter( d_qe, &(fm->d_rep_set) );

   Trace("fmc-exh") << "Exhaustive instantiate based on index " << c_index << " : " << c << " ";

   debugPrintCond("fmc-exh", c, true);

   Trace("fmc-exh")<< std::endl;

-  if( riter.setQuantifier( d_qe, f ) ){

+  if( riter.setQuantifier( f ) ){

     std::vector< RepDomain > dom;

     for (unsigned i=0; i<c.getNumChildren(); i++) {

       TypeNode tn = c[i].getType();

@@ -996,4 +1000,20 @@ Node FullModelChecker::getFunctionValue(FirstOrderModel * fm, Node op, const cha
   }

   curr = Rewriter::rewrite( curr );

   return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr);

+}

+

+Node FullModelChecker::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ) {

+  Trace("fmc-uf-model") << "Get model value for " << n << " " << n.getKind() << std::endl;

+  for(unsigned i=0; i<args.size(); i++) {

+    args[i] = getRepresentative(fm, args[i]);

+  }

+  if( n.getKind()==VARIABLE ){

+    Node r = getRepresentative(fm, n);

+    return r;

+  }else if( n.getKind()==APPLY_UF ){

+    getModel(fm, n.getOperator());

+    return d_models[n.getOperator()]->evaluate(this, args);

+  }else{

+    return Node::null();

+  }

 }
\ No newline at end of file
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index 92c866ffd..00a910567 100755
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -65,8 +65,8 @@ public:
     d_has_simplified = false;

   }

   bool addEntry( FullModelChecker * m, Node c, Node v);

-  Node evaluate( FullModelChecker * m, std::vector<Node> inst );

-  int getGeneralizationIndex( FullModelChecker * m, std::vector<Node> inst );

+  Node evaluate( FullModelChecker * m, std::vector<Node>& inst );

+  int getGeneralizationIndex( FullModelChecker * m, std::vector<Node>& inst );

   void simplify( FullModelChecker * m );

   void debugPrint(const char * tr, Node op, FullModelChecker * m);

 };

@@ -141,6 +141,8 @@ public:
 

   /** process build model */

   void processBuildModel(TheoryModel* m, bool fullModel);

+  /** get current model value */

+  Node getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial );

 };

 

 }

diff --git a/src/theory/quantifiers/inst_gen.cpp b/src/theory/quantifiers/inst_gen.cpp
index 192e58d7c..157861670 100644
--- a/src/theory/quantifiers/inst_gen.cpp
+++ b/src/theory/quantifiers/inst_gen.cpp
@@ -29,10 +29,10 @@ using namespace CVC4::theory::quantifiers;
 
 
 InstGenProcess::InstGenProcess( Node n ) : d_node( n ){
-  Assert( n.hasAttribute(InstConstantAttribute()) );
+  Assert( TermDb::hasInstConstAttr(n) );
   int count = 0;
   for( size_t i=0; i<n.getNumChildren(); i++ ){
-    if( n[i].getKind()!=INST_CONSTANT && n[i].hasAttribute(InstConstantAttribute()) ){
+    if( n[i].getKind()!=INST_CONSTANT && TermDb::hasInstConstAttr(n[i]) ){
       d_children.push_back( InstGenProcess( n[i] ) );
       d_children_index.push_back( i );
       d_children_map[ i ] = count;
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index d4988f223..d55f72a88 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -143,7 +143,7 @@ void InstMatch::set(TNode var, TNode n){
   if (Trace.isOn("inst-match-warn")) {
     // For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations
     if( !n.isNull() && !n.getType().isSubtypeOf( var.getType() ) ){
-      Trace("inst-match-warn") << var.getAttribute(InstConstantAttribute()) << std::endl;
+      Trace("inst-match-warn") << quantifiers::TermDb::getInstConstAttr(var) << std::endl;
       Trace("inst-match-warn") << var << " " << var.getType() << " " << n << " " << n.getType() << std::endl ;
     }
   }
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index 105575c49..87c39f046 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -32,7 +32,7 @@ namespace inst {
 
 InstMatchGenerator::InstMatchGenerator( Node pat, int matchPolicy ) : d_matchPolicy( matchPolicy ){
   d_active_add = false;
-  Assert( pat.hasAttribute(InstConstantAttribute()) );
+  Assert( quantifiers::TermDb::hasInstConstAttr(pat) );
   d_pattern = pat;
   d_match_pattern = pat;
   d_next = NULL;
@@ -53,9 +53,9 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat
       d_match_pattern = d_pattern[0];
     }
     if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==GEQ ){
-      if( !d_match_pattern[0].hasAttribute(InstConstantAttribute()) ||
+      if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[0]) ||
           d_match_pattern[0].getKind()==INST_CONSTANT ){
-        Assert( d_match_pattern[1].hasAttribute(InstConstantAttribute()) );
+        Assert( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[1]) );
         Node mp = d_match_pattern[1];
         //swap sides
         Node pat = d_pattern;
@@ -67,9 +67,9 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat
         }
         d_pattern = pat.getKind()==NOT ? d_pattern.negate() : d_pattern;
         d_match_pattern = mp;
-      }else if( !d_match_pattern[1].hasAttribute(InstConstantAttribute()) ||
+      }else if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[1]) ||
                 d_match_pattern[1].getKind()==INST_CONSTANT ){
-        Assert( d_match_pattern[0].hasAttribute(InstConstantAttribute()) );
+        Assert( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[0]) );
         if( d_pattern.getKind()!=NOT ){   //TEMPORARY until we do better implementation of disequality matching
           d_match_pattern = d_match_pattern[0];
         }else if( d_match_pattern[1].getKind()==INST_CONSTANT ){
@@ -79,7 +79,7 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat
     }
     int childMatchPolicy = MATCH_GEN_DEFAULT;
     for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){
-      if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){
+      if( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[i]) ){
         if( d_match_pattern[i].getKind()!=INST_CONSTANT && !Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){
           InstMatchGenerator * cimg = new InstMatchGenerator( d_match_pattern[i], childMatchPolicy );
           d_children.push_back( cimg );
@@ -127,7 +127,7 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat
       d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() );
     }else{
       d_cg = new CandidateGeneratorQueue;
-      if( !Trigger::isArithmeticTrigger( d_match_pattern.getAttribute(InstConstantAttribute()), d_match_pattern, d_arith_coeffs ) ){
+      if( !Trigger::isArithmeticTrigger( quantifiers::TermDb::getInstConstAttr(d_match_pattern), d_match_pattern, d_arith_coeffs ) ){
         Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
         //Warning() << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
         d_matchPolicy = MATCH_GEN_INTERNAL_ERROR;
@@ -161,12 +161,12 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi
     InstMatch prev( &m );
     //if t is null
     Assert( !t.isNull() );
-    Assert( !t.hasAttribute(InstConstantAttribute()) );
+    Assert( !quantifiers::TermDb::hasInstConstAttr(t) );
     Assert( t.getKind()==d_match_pattern.getKind() );
     Assert( !Trigger::isAtomicTrigger( d_match_pattern ) || t.getOperator()==d_match_pattern.getOperator() );
     //first, check if ground arguments are not equal, or a match is in conflict
     for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){
-      if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){
+      if( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[i]) ){
         if( d_match_pattern[i].getKind()==INST_CONSTANT || Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){
           Node vv = d_match_pattern[i];
           Node tt = t[i];
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index dbdf95613..a5031a061 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -143,8 +143,8 @@ int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){
 
 void InstStrategySimplex::addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder<>& t ){
   if( n.getKind()==MULT ){
-    if( n[1].hasAttribute(InstConstantAttribute()) ){
-      f = n[1].getAttribute(InstConstantAttribute());
+    if( TermDb::hasInstConstAttr(n[1]) ){
+      f = TermDb::getInstConstAttr(n[1]);
       if( n[1].getKind()==INST_CONSTANT ){
         d_ceTableaux[x][ n[1] ] = n[0];
       }else{
@@ -155,8 +155,8 @@ void InstStrategySimplex::addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder
       t << n;
     }
   }else{
-    if( n.hasAttribute(InstConstantAttribute()) ){
-      f = n.getAttribute(InstConstantAttribute());
+    if( TermDb::hasInstConstAttr(n) ){
+      f = TermDb::getInstConstAttr(n);
       if( n.getKind()==INST_CONSTANT ){
         d_ceTableaux[x][ n ] = Node::null();
       }else{
@@ -327,81 +327,9 @@ int InstStrategyDatatypesValue::process( Node f, Theory::Effort effort, int e ){
 Node InstStrategyDatatypesValue::getValueFor( Node n ){
   //simply get the ground value for n in the current model, if it exists,
   //  or return an arbitrary ground term otherwise
-  if( !n.hasAttribute(InstConstantAttribute()) ){
+  if( !TermDb::hasInstConstAttr(n) ){
     return n;
   }else{
     return n;
   }
-  /*  FIXME
-
-  Debug("quant-datatypes-debug")  << "get value for " << n << std::endl;
-  if( !n.hasAttribute(InstConstantAttribute()) ){
-    return n;
-  }else{
-    Assert( n.getType().isDatatype() );
-    //check if in equivalence class with ground term
-    Node rep = getRepresentative( n );
-    Debug("quant-datatypes-debug") << "Rep is " << rep << std::endl;
-    if( !rep.hasAttribute(InstConstantAttribute()) ){
-      return rep;
-    }else{
-      if( !n.getType().isDatatype() ){
-        return n.getType().mkGroundTerm();
-      }else{
-        if( n.getKind()==APPLY_CONSTRUCTOR ){
-          std::vector< Node > children;
-          children.push_back( n.getOperator() );
-          for( int i=0; i<(int)n.getNumChildren(); i++ ){
-            children.push_back( getValueFor( n[i] ) );
-          }
-          return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
-        }else{
-          const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype();
-          TheoryDatatypes::EqLists* labels = &((TheoryDatatypes*)d_th)->d_labels;
-          //otherwise, use which constructor the inst constant is current chosen to be
-          if( labels->find( n )!=labels->end() ){
-            TheoryDatatypes::EqList* lbl = (*labels->find( n )).second;
-            int tIndex = -1;
-            if( !lbl->empty() && (*lbl)[ lbl->size()-1 ].getKind()==APPLY_TESTER ){
-              Debug("quant-datatypes-debug") << n << " tester is " << (*lbl)[ lbl->size()-1 ] << std::endl;
-              tIndex = Datatype::indexOf((*lbl)[ lbl->size()-1 ].getOperator().toExpr());
-            }else{
-              Debug("quant-datatypes-debug") << "find possible tester choice" << std::endl;
-              //must find a possible choice
-              vector< bool > possibleCons;
-              possibleCons.resize( dt.getNumConstructors(), true );
-              for( TheoryDatatypes::EqList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ) {
-                Node leqn = (*j);
-                possibleCons[ Datatype::indexOf( leqn[0].getOperator().toExpr() ) ] = false;
-              }
-              for( unsigned int j=0; j<possibleCons.size(); j++ ) {
-                if( possibleCons[j] ){
-                  tIndex = j;
-                  break;
-                }
-              }
-            }
-            Assert( tIndex!=-1 );
-            Node cons = Node::fromExpr( dt[ tIndex ].getConstructor() );
-            Debug("quant-datatypes-debug") << n << " cons is " << cons << std::endl;
-            std::vector< Node > children;
-            children.push_back( cons );
-            for( int i=0; i<(int)dt[ tIndex ].getNumArgs(); i++ ) {
-              Node sn = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( dt[tIndex][i].getSelector() ), n );
-              if( n.hasAttribute(InstConstantAttribute()) ){
-                InstConstantAttribute ica;
-                sn.setAttribute(ica,n.getAttribute(InstConstantAttribute()) );
-              }
-              Node snn = getValueFor( sn );
-              children.push_back( snn );
-            }
-            return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
-          }else{
-            return n.getType().mkGroundTerm();
-          }
-        }
-      }
-    }
-  }
-  */
 }
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 79e36e9f5..76e61707e 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -46,6 +46,37 @@ bool QModelBuilder::optUseModel() {
 }
 
 
+Node QModelBuilder::getCurrentModelValue( FirstOrderModel* fm, Node n, bool partial ) {
+  std::vector< Node > children;
+  if( n.getNumChildren()>0 ){
+    if( n.getKind()!=APPLY_UF && n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+      children.push_back( n.getOperator() );
+    }
+    for (unsigned i=0; i<n.getNumChildren(); i++) {
+      Node nc = getCurrentModelValue( fm, n[i] );
+      if (nc.isNull()) {
+        return Node::null();
+      }else{
+        children.push_back( nc );
+      }
+    }
+    if( n.getKind()==APPLY_UF ){
+      return getCurrentUfModelValue( fm, n, children, partial );
+    }else{
+      Node nn = NodeManager::currentNM()->mkNode( n.getKind(), children );
+      nn = Rewriter::rewrite( nn );
+      return nn;
+    }
+  }else{
+    if( n.getKind()==VARIABLE ){
+      return getCurrentUfModelValue( fm, n, children, partial );
+    }else{
+      return n;
+    }
+  }
+}
+
+
 bool TermArgBasisTrie::addTerm2( FirstOrderModel* fm, Node n, int argIndex ){
   if( argIndex<(int)n.getNumChildren() ){
     Node r;
@@ -71,6 +102,9 @@ QModelBuilder( c, qe ) {
 
 }
 
+Node QModelBuilderIG::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ) {
+  return n;
+}
 
 void QModelBuilderIG::debugModel( FirstOrderModel* fm ){
   //debug the model: cycle through all instantiations for all quantifiers, report ones that are not true
@@ -81,8 +115,8 @@ void QModelBuilderIG::debugModel( FirstOrderModel* fm ){
       for( int j=0; j<(int)f[0].getNumChildren(); j++ ){
         vars.push_back( f[0][j] );
       }
-      RepSetIterator riter( &(fm->d_rep_set) );
-      riter.setQuantifier( d_qe, f );
+      RepSetIterator riter( d_qe, &(fm->d_rep_set) );
+      riter.setQuantifier( f );
       while( !riter.isFinished() ){
         std::vector< Node > terms;
         for( int i=0; i<riter.getNumTerms(); i++ ){
@@ -410,7 +444,7 @@ void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){
       //  constant definitions.
       bool isConst = true;
       std::vector< Node > uf_terms;
-      if( n.hasAttribute(InstConstantAttribute()) ){
+      if( TermDb::hasInstConstAttr(n) ){
         isConst = false;
         if( gn.getKind()==APPLY_UF ){
           uf_terms.push_back( gn );
@@ -418,7 +452,7 @@ void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){
         }else if( gn.getKind()==EQUAL ){
           isConst = true;
           for( int j=0; j<2; j++ ){
-            if( n[j].hasAttribute(InstConstantAttribute()) ){
+            if( TermDb::hasInstConstAttr(n[j]) ){
               if( n[j].getKind()==APPLY_UF &&
                   fm->d_uf_model_tree.find( gn[j].getOperator() )!=fm->d_uf_model_tree.end() ){
                 uf_terms.push_back( gn[j] );
@@ -525,17 +559,16 @@ int QModelBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){
     for( size_t i=0; i<d_quant_selection_lit_candidates[f].size(); i++ ){
       bool phase = d_quant_selection_lit_candidates[f][i].getKind()!=NOT;
       Node lit = d_quant_selection_lit_candidates[f][i].getKind()==NOT ? d_quant_selection_lit_candidates[f][i][0] : d_quant_selection_lit_candidates[f][i];
-      Assert( lit.hasAttribute(InstConstantAttribute()) );
+      Assert( TermDb::hasInstConstAttr(lit) );
       std::vector< Node > tr_terms;
       if( lit.getKind()==APPLY_UF ){
         //only match predicates that are contrary to this one, use literal matching
         Node eq = NodeManager::currentNM()->mkNode( IFF, lit, !phase ? fm->d_true : fm->d_false );
-        d_qe->getTermDatabase()->setInstantiationConstantAttr( eq, f );
         tr_terms.push_back( eq );
       }else if( lit.getKind()==EQUAL ){
         //collect trigger terms
         for( int j=0; j<2; j++ ){
-          if( lit[j].hasAttribute(InstConstantAttribute()) ){
+          if( TermDb::hasInstConstAttr(lit[j]) ){
             if( lit[j].getKind()==APPLY_UF ){
               tr_terms.push_back( lit[j] );
             }else{
@@ -671,7 +704,6 @@ void QModelBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f ){
   //if( !s.isNull() ){
   //  s = Rewriter::rewrite( s );
   //}
-  d_qe->getTermDatabase()->setInstantiationConstantAttr( s, f );
   Trace("sel-form-debug") << "Selection formula " << f << std::endl;
   Trace("sel-form-debug") << "                  " << s << std::endl;
   if( !s.isNull() ){
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index 2b38f3381..f41392eee 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -33,6 +33,8 @@ protected:
   context::CDO< FirstOrderModel* > d_curr_model;
   //quantifiers engine
   QuantifiersEngine* d_qe;
+  /** get current model value */
+  virtual Node getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ) = 0;
 public:
   QModelBuilder( context::Context* c, QuantifiersEngine* qe );
   virtual ~QModelBuilder(){}
@@ -48,6 +50,8 @@ public:
   bool d_considerAxioms;
   /** exist instantiation ? */
   virtual bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ) { return false; }
+  /** get current model value */
+  Node getCurrentModelValue( FirstOrderModel* fm, Node n, bool partial = false );
 };
 
 
@@ -91,6 +95,8 @@ protected:
   bool d_didInstGen;
   /** process build model */
   virtual void processBuildModel( TheoryModel* m, bool fullModel );
+  /** get current model value */
+  Node getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial );
 protected:
   //reset
   virtual void reset( FirstOrderModel* fm ) = 0;
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index b9dcef282..c91d9d3ab 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -187,7 +187,7 @@ int ModelEngine::checkModel(){
   d_relevantLemmas = 0;
   d_totalLemmas = 0;
   Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
-  int e_max = options::fmfFullModelCheck() ? 2 : 1;
+  int e_max = options::fmfFullModelCheck() && options::fmfModelBasedInst() ? 2 : 1;
   for( int e=0; e<e_max; e++) {
     if (addedLemmas==0) {
       for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
@@ -238,8 +238,8 @@ int ModelEngine::exhaustiveInstantiate( Node f, int effort ){
     }
     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( d_quantEngine, f ) ){
+    RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) );
+    if( riter.setQuantifier( f ) ){
       Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl;
       d_quantEngine->getModel()->resetEvaluate();
       Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl;
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 9facdbc5f..e83014789 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -116,6 +116,9 @@ option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :defau
 option fmfFreshDistConst --fmf-fresh-dc bool :default false
  use fresh distinguished representative when applying Inst-Gen techniques
 
+option fmfBoundInt --fmf-bound-int bool :default false
+ finite model finding on bounded integer quantification
+
 option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h"
  policy for instantiating axioms
 
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 53f67853b..59995a510 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -189,13 +189,13 @@ QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){
     for( std::map< Node, bool >::iterator it = d_phase_reqs.begin(); it != d_phase_reqs.end(); ++it ){
       Debug("inst-engine-phase-req") << "   " << it->first << " -> " << it->second << std::endl;
       if( it->first.getKind()==EQUAL ){
-        if( it->first[0].hasAttribute(InstConstantAttribute()) ){
-          if( !it->first[1].hasAttribute(InstConstantAttribute()) ){
+        if( quantifiers::TermDb::hasInstConstAttr(it->first[0]) ){
+          if( !quantifiers::TermDb::hasInstConstAttr(it->first[1]) ){
             d_phase_reqs_equality_term[ it->first[0] ] = it->first[1];
             d_phase_reqs_equality[ it->first[0] ] = it->second;
             Debug("inst-engine-phase-req") << "      " << it->first[0] << ( it->second ? " == " : " != " ) << it->first[1] << std::endl;
           }
-        }else if( it->first[1].hasAttribute(InstConstantAttribute()) ){
+        }else if( quantifiers::TermDb::hasInstConstAttr(it->first[1]) ){
           d_phase_reqs_equality_term[ it->first[1] ] = it->first[0];
           d_phase_reqs_equality[ it->first[1] ] = it->second;
           Debug("inst-engine-phase-req") << "      " << it->first[1] << ( it->second ? " == " : " != " ) << it->first[0] << std::endl;
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 5c71f6e6f..9f156b656 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -211,10 +211,6 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
       if( in.hasAttribute(NestedQuantAttribute()) ){
         setNestedQuantifiers( ret, in.getAttribute(NestedQuantAttribute()) );
       }
-      if( in.hasAttribute(InstConstantAttribute()) ){
-        InstConstantAttribute ica;
-        ret.setAttribute(ica,in.getAttribute(InstConstantAttribute()) );
-      }
       Trace("quantifiers-rewrite") << "*** rewrite " << in << std::endl;
       Trace("quantifiers-rewrite") << " to " << std::endl;
       Trace("quantifiers-rewrite") << ret << std::endl;
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 2b011552c..cf12cf540 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -147,7 +147,7 @@ bool RelevantDomain::computeRelevantInstantiationDomain( Node n, Node parent, in
 
 bool RelevantDomain::extendFunctionDomains( Node n, RepDomain& range ){
   if( n.getKind()==INST_CONSTANT ){
-    Node f = n.getAttribute(InstConstantAttribute());
+    Node f = TermDb::getInstConstAttr(n);
     int var = n.getAttribute(InstVarNumAttribute());
     range.insert( range.begin(), d_quant_inst_domain[f][var].begin(), d_quant_inst_domain[f][var].end() );
     return false;
@@ -177,7 +177,7 @@ bool RelevantDomain::extendFunctionDomains( Node n, RepDomain& range ){
       }
     }
     //get the range
-    if( n.hasAttribute(InstConstantAttribute()) ){
+    if( TermDb::hasInstConstAttr(n) ){
       if( n.getKind()==APPLY_UF && d_active_range.find( op )!=d_active_range.end() ){
         range.insert( range.end(), d_active_range[op].begin(), d_active_range[op].end() );
       }else{
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 417b4ae3a..dc00b5f95 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -74,7 +74,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
     //if this is an atomic trigger, consider adding it
     //Call the children?
     if( inst::Trigger::isAtomicTrigger( n ) ){
-      if( !n.hasAttribute(InstConstantAttribute()) ){
+      if( !TermDb::hasInstConstAttr(n) ){
         Trace("term-db") << "register term in db " << n << std::endl;
         //std::cout << "register trigger term " << n << std::endl;
         Node op = n.getOperator();
@@ -117,7 +117,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
       }
     }
   }else{
-    if( options::efficientEMatching() && !n.hasAttribute(InstConstantAttribute())){
+    if( options::efficientEMatching() && !TermDb::hasInstConstAttr(n)){
       //Efficient e-matching must be notified
       //The term in triggers are not important here
       Debug("term-db") << "New in this branch term " << n << std::endl;
@@ -167,7 +167,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
        while( !eqc.isFinished() ){
          Node en = (*eqc);
          computeModelBasisArgAttribute( en );
-         if( en.getKind()==APPLY_UF && !en.hasAttribute(InstConstantAttribute()) ){
+         if( en.getKind()==APPLY_UF && !TermDb::hasInstConstAttr(en) ){
            if( !en.getAttribute(NoMatchAttribute()) ){
              Node op = en.getOperator();
              if( !d_pred_map_trie[i][op].addTerm( d_quantEngine, en ) ){
@@ -275,33 +275,75 @@ void TermDb::makeInstantiationConstantsFor( Node f ){
       //set the var number attribute
       InstVarNumAttribute ivna;
       ic.setAttribute(ivna,i);
+      InstConstantAttribute ica;
+      ic.setAttribute(ica,f);
+      //also set the no-match attribute
+      NoMatchAttribute nma;
+      ic.setAttribute(nma,true);
     }
   }
 }
 
-void TermDb::setInstantiationConstantAttr( Node n, Node f ){
-  if( !n.hasAttribute(InstConstantAttribute()) ){
-    bool setAttr = false;
-    if( n.getKind()==INST_CONSTANT ){
-      setAttr = true;
-    }else{
-      for( int i=0; i<(int)n.getNumChildren(); i++ ){
-        setInstantiationConstantAttr( n[i], f );
-        if( n[i].hasAttribute(InstConstantAttribute()) ){
-          setAttr = true;
-        }
+
+Node TermDb::getInstConstAttr( Node n ) {
+  if (!n.hasAttribute(InstConstantAttribute()) ){
+    Node f;
+    for( int i=0; i<(int)n.getNumChildren(); i++ ){
+      f = getInstConstAttr(n[i]);
+      if( !f.isNull() ){
+        break;
       }
     }
-    if( setAttr ){
-      InstConstantAttribute ica;
-      n.setAttribute(ica,f);
+    InstConstantAttribute ica;
+    n.setAttribute(ica,f);
+    if( !f.isNull() ){
       //also set the no-match attribute
       NoMatchAttribute nma;
       n.setAttribute(nma,true);
     }
   }
+  return n.getAttribute(InstConstantAttribute());
+}
+
+bool TermDb::hasInstConstAttr( Node n ) {
+  return !getInstConstAttr(n).isNull();
 }
 
+bool TermDb::hasBoundVarAttr( Node n ) {
+  if( !n.getAttribute(HasBoundVarComputedAttribute()) ){
+    bool hasBv = false;
+    if( n.getKind()==BOUND_VARIABLE ){
+      hasBv = true;
+    }else{
+      for (unsigned i=0; i<n.getNumChildren(); i++) {
+        if( hasBoundVarAttr(n[i]) ){
+          hasBv = true;
+          break;
+        }
+      }
+    }
+    HasBoundVarAttribute hbva;
+    n.setAttribute(hbva, hasBv);
+    HasBoundVarComputedAttribute hbvca;
+    n.setAttribute(hbvca, true);
+    Trace("bva") << n << " has bva : " << n.getAttribute(HasBoundVarAttribute()) << std::endl;
+  }
+  return n.getAttribute(HasBoundVarAttribute());
+}
+
+void TermDb::getBoundVars( Node n, std::vector< Node >& bvs) {
+  if (n.getKind()==BOUND_VARIABLE ){
+    if ( std::find( bvs.begin(), bvs.end(), n)==bvs.end() ){
+      bvs.push_back( n );
+    }
+  }else{
+    for( unsigned i=0; i<n.getNumChildren(); i++) {
+      getBoundVars(n[i], bvs);
+    }
+  }
+}
+
+
 /** get the i^th instantiation constant of f */
 Node TermDb::getInstantiationConstant( Node f, int i ) const {
   std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( f );
@@ -347,7 +389,6 @@ Node TermDb::getCounterexampleLiteral( Node f ){
     //otherwise, ensure literal
     Node ceLit = d_quantEngine->getValuation().ensureLiteral( ceBody.notNode() );
     d_ce_lit[ f ] = ceLit;
-    setInstantiationConstantAttr( ceLit, f );
   }
   return d_ce_lit[ f ];
 }
@@ -361,7 +402,6 @@ Node TermDb::convertNodeToPattern( Node n, Node f, const std::vector<Node> & var
   Node n2 = n.substitute( vars.begin(), vars.end(),
                           inst_constants.begin(),
                           inst_constants.end() );
-  setInstantiationConstantAttr( n2, f );
   return n2;
 }
 
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index e5154476a..7b5df2ab8 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -59,6 +59,10 @@ typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
 struct ModelBasisArgAttributeId {};
 typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> ModelBasisArgAttribute;
 
+struct HasBoundVarAttributeId {};
+typedef expr::Attribute<HasBoundVarAttributeId, bool> HasBoundVarAttribute;
+struct HasBoundVarComputedAttributeId {};
+typedef expr::Attribute<HasBoundVarComputedAttributeId, bool> HasBoundVarComputedAttribute;
 
 class QuantifiersEngine;
 
@@ -186,9 +190,15 @@ public:
   Node convertNodeToPattern( Node n, Node f,
                              const std::vector<Node> & vars,
                              const std::vector<Node> & nvars);
-  /** set instantiation constant attr */
-  void setInstantiationConstantAttr( Node n, Node f );
 
+  static Node getInstConstAttr( Node n );
+  static bool hasInstConstAttr( Node n );
+//for bound variables
+public:
+  //does n have bound variables?
+  static bool hasBoundVarAttr( Node n );
+  //get bound variables in n
+  static void getBoundVars( Node n, std::vector< Node >& bvs);
 //for skolem
 private:
   /** map from universal quantifiers to the list of skolem constants */
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 9843cd09e..c68623baa 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -65,7 +65,7 @@ void TheoryQuantifiers::notifyEq(TNode lhs, TNode rhs) {
 
 void TheoryQuantifiers::preRegisterTerm(TNode n) {
   Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl;
-  if( n.getKind()==FORALL && !n.hasAttribute(InstConstantAttribute()) ){
+  if( n.getKind()==FORALL && !TermDb::hasInstConstAttr(n) ){
     getQuantifiersEngine()->registerQuantifier( n );
   }
 }
@@ -149,7 +149,7 @@ Node TheoryQuantifiers::getNextDecisionRequest(){
 
 void TheoryQuantifiers::assertUniversal( Node n ){
   Assert( n.getKind()==FORALL );
-  if( !n.hasAttribute(InstConstantAttribute()) ){
+  if( !TermDb::hasInstConstAttr(n) ){
     getQuantifiersEngine()->registerQuantifier( n );
     getQuantifiersEngine()->assertNode( n );
   }
@@ -157,7 +157,7 @@ void TheoryQuantifiers::assertUniversal( Node n ){
 
 void TheoryQuantifiers::assertExistential( Node n ){
   Assert( n.getKind()== NOT && n[0].getKind()==FORALL );
-  if( !n[0].hasAttribute(InstConstantAttribute()) ){
+  if( !TermDb::hasInstConstAttr(n[0]) ){
     if( d_skolemized.find( n )==d_skolemized.end() ){
       Node body = getQuantifiersEngine()->getTermDatabase()->getSkolemizedBody( n[0] );
       NodeBuilder<> nb(kind::OR);
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 1f1667522..fea8ab6d5 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -124,7 +124,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
       qe->getTermDatabase()->computeVarContains( temp[i] );
       for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ temp[i] ].size(); j++ ){
         Node v = qe->getTermDatabase()->d_var_contains[ temp[i] ][j];
-        if( v.getAttribute(InstConstantAttribute())==f ){
+        if( quantifiers::TermDb::getInstConstAttr(v)==f ){
           if( vars.find( v )==vars.end() ){
             varCount++;
             vars[ v ] = true;
@@ -223,7 +223,7 @@ bool Trigger::isUsableTrigger( std::vector< Node >& nodes, Node f ){
 }
 
 bool Trigger::isUsable( Node n, Node f ){
-  if( n.getAttribute(InstConstantAttribute())==f ){
+  if( quantifiers::TermDb::getInstConstAttr(n)==f ){
     if( isAtomicTrigger( n ) ){
       for( int i=0; i<(int)n.getNumChildren(); i++ ){
         if( !isUsable( n[i], f ) ){
@@ -282,8 +282,6 @@ Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) {
                 int vti = veq[0]==it->first ? 1 : 0;
                 if( isUsableTrigger(veq[vti], f) && !nodeContainsVar( veq[vti], veq[vti==0 ? 1 : 0]) ){
                   rtr = veq;
-                  InstConstantAttribute ica;
-                  rtr.setAttribute(ica,veq[vti].getAttribute(InstConstantAttribute()) );
                 }
               }
             }
@@ -298,13 +296,11 @@ Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) {
           Trace("relational-trigger") << "    polarity : " << pol << std::endl;
         }
         Node rtr2 = (hasPol && pol) ? rtr.negate() : rtr;
-        InstConstantAttribute ica;
-        rtr2.setAttribute(ica,rtr.getAttribute(InstConstantAttribute()) );
         return rtr2;
       }
     }
   }
-  bool usable = n.getAttribute(InstConstantAttribute())==f && isAtomicTrigger( n ) && isUsable( n, f );
+  bool usable = quantifiers::TermDb::getInstConstAttr(n)==f && isAtomicTrigger( n ) && isUsable( n, f );
   Trace("usable") << n << " usable : " << usable << std::endl;
   if( usable ){
     return n;
@@ -325,7 +321,7 @@ bool Trigger::isAtomicTrigger( Node n ){
 bool Trigger::isSimpleTrigger( Node n ){
   if( isAtomicTrigger( n ) ){
     for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      if( n[i].getKind()!=INST_CONSTANT && n[i].hasAttribute(InstConstantAttribute()) ){
+      if( n[i].getKind()!=INST_CONSTANT && quantifiers::TermDb::hasInstConstAttr(n[i]) ){
         return false;
       }
     }
@@ -438,9 +434,9 @@ bool Trigger::isArithmeticTrigger( Node f, Node n, std::map< Node, Node >& coeff
     Assert( coeffs.empty() );
     NodeBuilder<> t(kind::PLUS);
     for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      if( n[i].hasAttribute(InstConstantAttribute()) ){
+      if( quantifiers::TermDb::hasInstConstAttr(n[i]) ){
         if( n[i].getKind()==INST_CONSTANT ){
-          if( n[i].getAttribute(InstConstantAttribute())==f ){
+          if( quantifiers::TermDb::getInstConstAttr(n[i])==f ){
             coeffs[ n[i] ] = Node::null();
           }else{
             coeffs.clear();
@@ -463,13 +459,13 @@ bool Trigger::isArithmeticTrigger( Node f, Node n, std::map< Node, Node >& coeff
     }
     return true;
   }else if( n.getKind()==MULT ){
-    if( n[0].getKind()==INST_CONSTANT && n[0].getAttribute(InstConstantAttribute())==f ){
-      if( !n[1].hasAttribute(InstConstantAttribute()) ){
+    if( n[0].getKind()==INST_CONSTANT && quantifiers::TermDb::getInstConstAttr(n[0])==f ){
+      if( !quantifiers::TermDb::hasInstConstAttr(n[1]) ){
         coeffs[ n[0] ] = n[1];
         return true;
       }
-    }else if( n[1].getKind()==INST_CONSTANT && n[1].getAttribute(InstConstantAttribute())==f ){
-      if( !n[0].hasAttribute(InstConstantAttribute()) ){
+    }else if( n[1].getKind()==INST_CONSTANT && quantifiers::TermDb::getInstConstAttr(n[1])==f ){
+      if( !quantifiers::TermDb::hasInstConstAttr(n[0]) ){
         coeffs[ n[1] ] = n[0];
         return true;
       }
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index ef8169433..89d1ad55a 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -61,9 +61,12 @@ d_lemmas_produced_c(u){
   if( options::finiteModelFind() ){
     d_model_engine = new quantifiers::ModelEngine( c, this );
     d_modules.push_back( d_model_engine );
-
-    d_bint = new quantifiers::BoundedIntegers( c, this );
-    d_modules.push_back( d_bint );
+    if( options::fmfBoundInt() ){
+      d_bint = new quantifiers::BoundedIntegers( c, this );
+      d_modules.push_back( d_bint );
+    }else{
+      d_bint = NULL;
+    }
   }else{
     d_model_engine = NULL;
     d_bint = NULL;
@@ -256,7 +259,6 @@ void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< No
 
 bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){
   Assert( f.getKind()==FORALL );
-  Assert( !f.hasAttribute(InstConstantAttribute()) );
   Assert( vars.size()==terms.size() );
   Node body = getInstantiation( f, vars, terms );
   //make the lemma
@@ -271,7 +273,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std
     Trace("inst") << "*** Instantiate " << f << " with " << std::endl;
     uint64_t maxInstLevel = 0;
     for( int i=0; i<(int)terms.size(); i++ ){
-      if( terms[i].hasAttribute(InstConstantAttribute()) ){
+      if( quantifiers::TermDb::hasInstConstAttr(terms[i]) ){
         Debug("inst")<< "***& Bad Instantiate " << f << " with " << std::endl;
         for( int i=0; i<(int)terms.size(); i++ ){
           Debug("inst") << "   " << terms[i] << std::endl;
@@ -437,8 +439,6 @@ bool QuantifiersEngine::addSplit( Node n, bool reqPhase, bool reqPhasePol ){
 }
 
 bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool reqPhasePol ){
-  //Assert( !n1.hasAttribute(InstConstantAttribute()) );
-  //Assert( !n2.hasAttribute(InstConstantAttribute()) );
   //Assert( !areEqual( n1, n2 ) );
   //Assert( !areDisequal( n1, n2 ) );
   Kind knd = n1.getType()==NodeManager::currentNM()->booleanType() ? IFF : EQUAL;
@@ -468,7 +468,6 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){
       if( d_phase_reqs[f]->isPhaseReq( nodes[i] ) ){
         bool preq = d_phase_reqs[f]->getPhaseReq( nodes[i] );
         nodes[i] = NodeManager::currentNM()->mkNode( IFF, nodes[i], NodeManager::currentNM()->mkConst<bool>(preq) );
-        d_term_db->setInstantiationConstantAttr( nodes[i], f );
         nodeChanged = true;
       }
       //else if( qe->isPhaseReqEquality( f, trNodes[i] ) ){
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index fe3e39d45..6903adda5 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -95,9 +95,8 @@ void RepSet::toStream(std::ostream& out){
 }
 
 
-RepSetIterator::RepSetIterator( RepSet* rs ) : d_rep_set( rs ){
+RepSetIterator::RepSetIterator( QuantifiersEngine * qe, RepSet* rs ) : d_qe(qe), d_rep_set( rs ){
   d_incomplete = false;
-
 }
 
 int RepSetIterator::domainSize( int i ) {
@@ -108,25 +107,29 @@ int RepSetIterator::domainSize( int i ) {
   }
 }
 
-bool RepSetIterator::setQuantifier( QuantifiersEngine * qe, Node f ){
+bool RepSetIterator::setQuantifier( Node f ){
+  Trace("rsi") << "Make rsi for " << f << std::endl;
   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(qe, f);
+  d_owner = f;
+  return initialize();
 }
 
-bool RepSetIterator::setFunctionDomain( QuantifiersEngine * qe, Node op ){
+bool RepSetIterator::setFunctionDomain( Node op ){
+  Trace("rsi") << "Make rsi for " << op << std::endl;
   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(qe, Node::null());
+  d_owner = op;
+  return initialize();
 }
 
-bool RepSetIterator::initialize(QuantifiersEngine * qe, Node f){
+bool RepSetIterator::initialize(){
   for( size_t i=0; i<d_types.size(); i++ ){
     d_index.push_back( 0 );
     //store default index order
@@ -144,30 +147,11 @@ bool RepSetIterator::initialize(QuantifiersEngine * qe, Node f){
       }
     }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;
-          }
+      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;
@@ -197,6 +181,40 @@ bool RepSetIterator::initialize(QuantifiersEngine * qe, Node f){
       }
     }
   }
+  //must set a variable index order
+  if (d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers()) {
+    Trace("bound-int-rsi") << "Calculating variable order..." << std::endl;
+    std::vector< int > varOrder;
+    for( unsigned i=0; i<d_qe->getBoundedIntegers()->getNumBoundVars(d_owner); i++ ){
+      varOrder.push_back(d_qe->getBoundedIntegers()->getBoundVarNum(d_owner,i));
+    }
+    for( unsigned i=0; i<d_owner[0].getNumChildren(); i++) {
+      if( !d_qe->getBoundedIntegers()->isBoundVar(d_owner, d_owner[0][i])) {
+        varOrder.push_back(i);
+      }
+    }
+    Trace("bound-int-rsi") << "Variable order : ";
+    for( unsigned i=0; i<varOrder.size(); i++) {
+      Trace("bound-int-rsi") << varOrder[i] << " ";
+    }
+    Trace("bound-int-rsi") << std::endl;
+    std::vector< int > indexOrder;
+    indexOrder.resize(varOrder.size());
+    for( unsigned i=0; i<varOrder.size(); i++){
+      indexOrder[varOrder[i]] = i;
+    }
+    Trace("bound-int-rsi") << "Will use index order : ";
+    for( unsigned i=0; i<indexOrder.size(); i++) {
+      Trace("bound-int-rsi") << indexOrder[i] << " ";
+    }
+    Trace("bound-int-rsi") << std::endl;
+    setIndexOrder(indexOrder);
+  }
+  for (unsigned i=0; i<d_index.size(); i++) {
+    if (!resetIndex(i, true)){
+      break;
+    }
+  }
   return true;
 }
 
@@ -220,22 +238,65 @@ void RepSetIterator::setDomain( std::vector< RepDomain >& domain ){
   }
 }
 */
+bool RepSetIterator::resetIndex( int i, bool initial ) {
+  d_index[i] = 0;
+  int ii = d_index_order[i];
+  Trace("bound-int-rsi") << "Reset " << i << " " << ii << " " << initial << std::endl;
+  //determine the current range
+  if( d_enum_type[ii]==ENUM_RANGE ){
+    if( initial || !d_qe->getBoundedIntegers()->isGroundRange( d_owner, d_owner[0][ii] ) ){
+      Trace("bound-int-rsi") << "Getting range of " << d_owner[0][ii] << std::endl;
+      Node l, u;
+      d_qe->getBoundedIntegers()->getBoundValues( d_owner, d_owner[0][ii], this, l, u );
+      if( l.isNull() || u.isNull() ){
+        //failed, abort the iterator
+        d_index.clear();
+        return false;
+      }else{
+        Trace("bound-int-rsi") << "Can limit bounds of " << d_owner[0][ii] << " 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 ) ) ) );
+        d_domain[ii].clear();
+        d_lower_bounds[ii] = l;
+        if( ra==NodeManager::currentNM()->mkConst(true) ){
+          long rr = range.getConst<Rational>().getNumerator().getLong()+1;
+          Trace("bound-int-rsi")  << "Actual bound range is " << rr << std::endl;
+          d_domain[ii].push_back( (int)rr );
+        }else{
+          Trace("fmf-incomplete") << "Incomplete because of integer quantification, bounds are too big for " << d_owner[0][ii] << "." << std::endl;
+          d_incomplete = true;
+          d_domain[ii].push_back( 0 );
+        }
+      }
+    }else{
+      Trace("bound-int-rsi") << d_owner[0][ii] << " has ground range, skip." << std::endl;
+    }
+  }
+  return true;
+}
+
 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)(domainSize(counter)-1) ){
+  Trace("rsi-debug") << "domain size of " << counter << " is " << domainSize(counter) << std::endl;
+  while( counter>=0 && d_index[counter]>=(int)(domainSize(counter)-1) ){
     counter--;
+    if( counter>=0){
+      Trace("rsi-debug") << "domain size of " << counter << " is " << domainSize(counter) << std::endl;
+    }
   }
   if( counter==-1 ){
     d_index.clear();
   }else{
+    d_index[counter]++;
     for( int i=(int)d_index.size()-1; i>counter; i-- ){
-      d_index[i] = 0;
+      if (!resetIndex(i)){
+        break;
+      }
     }
-    d_index[counter]++;
   }
 }
 
@@ -256,6 +317,7 @@ Node RepSetIterator::getTerm( int i ){
     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{
+    Trace("rsi-debug") << index << " " << d_lower_bounds[index] << " " << d_index[index] << std::endl;
     Node t = NodeManager::currentNM()->mkNode(PLUS, d_lower_bounds[index],
                                                     NodeManager::currentNM()->mkConst( Rational(d_index[index]) ) );
     t = Rewriter::rewrite( t );
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index b92d9d2c6..fc8db420d 100644
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -59,22 +59,26 @@ private:
     ENUM_DOMAIN_ELEMENTS,
     ENUM_RANGE,
   };
-
+  QuantifiersEngine * d_qe;
   //initialize function
-  bool initialize(QuantifiersEngine * qe, Node f);
+  bool initialize();
   //enumeration type?
   std::vector< int > d_enum_type;
   //for enum ranges
   std::map< int, Node > d_lower_bounds;
   //domain size
   int domainSize( int i );
+  //node this is rep set iterator is for
+  Node d_owner;
+  //reset index
+  bool resetIndex( int i, bool initial = false );
 public:
-  RepSetIterator( RepSet* rs );
+  RepSetIterator( QuantifiersEngine * qe, RepSet* rs );
   ~RepSetIterator(){}
   //set that this iterator will be iterating over instantiations for a quantifier
-  bool setQuantifier( QuantifiersEngine * qe, Node f );
+  bool setQuantifier( Node f );
   //set that this iterator will be iterating over the domain of a function
-  bool setFunctionDomain( QuantifiersEngine * qe, Node op );
+  bool setFunctionDomain( Node op );
 public:
   //pointer to model
   RepSet* d_rep_set;
diff --git a/src/theory/rewriterules/rr_inst_match.cpp b/src/theory/rewriterules/rr_inst_match.cpp
index a4c111f86..4908e5ec0 100644
--- a/src/theory/rewriterules/rr_inst_match.cpp
+++ b/src/theory/rewriterules/rr_inst_match.cpp
@@ -137,14 +137,13 @@ class DumbPatMatcher: public PatMatcher{
 /* The order of the matching is:
    reset arg1, nextMatch arg1, reset arg2, nextMatch arg2, ... */
 ApplyMatcher::ApplyMatcher( Node pat, QuantifiersEngine* qe): d_pattern(pat){
-  //  Assert( pat.hasAttribute(InstConstantAttribute()) );
 
   //set-up d_variables, d_constants, d_childrens
   for( size_t i=0; i< d_pattern.getNumChildren(); ++i ){
     //EqualityQuery* q = qe->getEqualityQuery(d_pattern[i].getType());
     EqualityQuery* q = qe->getEqualityQuery();
     Assert( q != NULL );
-    if( d_pattern[i].hasAttribute(InstConstantAttribute()) ){
+    if( quantifiers::TermDb::hasInstConstAttr(d_pattern[i]) ){
       if( d_pattern[i].getKind()==INST_CONSTANT ){
         //It's a variable
         d_variables.push_back(make_triple((TNode)d_pattern[i],i,q));
@@ -172,7 +171,7 @@ bool ApplyMatcher::reset(TNode t, InstMatch & m, QuantifiersEngine* qe){
 
   //if t is null
   Assert( !t.isNull() );
-  Assert( !t.hasAttribute(InstConstantAttribute()) );
+  Assert( !quantifiers::TermDb::hasInstConstAttr(t) );
   Assert( t.getKind()==d_pattern.getKind() );
   Assert( (t.getKind()!=APPLY_UF && t.getKind()!=APPLY_CONSTRUCTOR)
           || t.getOperator()==d_pattern.getOperator() );
@@ -411,7 +410,7 @@ public:
 size_t numFreeVar(TNode t){
   size_t n = 0;
   for( size_t i=0, size =t.getNumChildren(); i < size; ++i ){
-    if( t[i].hasAttribute(InstConstantAttribute()) ){
+    if( quantifiers::TermDb::hasInstConstAttr(t[i]) ){
       if( t[i].getKind()==INST_CONSTANT ){
         //variable
         ++n;
@@ -958,7 +957,7 @@ Matcher* mkMatcher( Node pat, QuantifiersEngine* qe ){
     /** TODO: something simpler to see if the pattern is a good
         arithmetic pattern */
     std::map< Node, Node > d_arith_coeffs;
-    if( !Trigger::getPatternArithmetic( pat.getAttribute(InstConstantAttribute()), pat, d_arith_coeffs ) ){
+    if( !Trigger::getPatternArithmetic( quantifiers::TermDb::getInstConstAttr(pat), pat, d_arith_coeffs ) ){
       Message() << "(?) Unknown matching pattern is " << pat << std::endl;
       Unimplemented("pattern not implemented");
       return new DumbMatcher();
@@ -983,17 +982,17 @@ Matcher* mkMatcher( Node pat, QuantifiersEngine* qe ){
 
 PatMatcher* mkPattern( Node pat, QuantifiersEngine* qe ){
   Debug("inst-match-gen") << "Pattern term is " << pat << std::endl;
-  Assert( pat.hasAttribute(InstConstantAttribute()) );
+  Assert( quantifiers::TermDb::hasInstConstAttr(pat) );
 
   if( pat.getKind()==kind::NOT && pat[0].getKind() == kind::EQUAL){
     /* Difference */
     return new UfDeqMatcher(pat, qe);
   } else if (pat.getKind() == kind::EQUAL){
-    if( !pat[0].hasAttribute(InstConstantAttribute() )){
-        Assert(pat[1].hasAttribute(InstConstantAttribute()));
+    if( !quantifiers::TermDb::hasInstConstAttr(pat[0])){
+        Assert(quantifiers::TermDb::hasInstConstAttr(pat[1]));
         return new UfCstEqMatcher(pat[1], pat[0], qe);
-    }else if( !pat[1].hasAttribute(InstConstantAttribute() )){
-      Assert(pat[0].hasAttribute(InstConstantAttribute()));
+    }else if( !quantifiers::TermDb::hasInstConstAttr(pat[1] )){
+      Assert(quantifiers::TermDb::hasInstConstAttr(pat[0]));
       return new UfCstEqMatcher(pat[0], pat[1], qe);
     }else{
       std::vector< Node > pats(pat.begin(),pat.end());
@@ -1009,7 +1008,7 @@ PatMatcher* mkPattern( Node pat, QuantifiersEngine* qe ){
     /** TODO: something simpler to see if the pattern is a good
         arithmetic pattern */
     std::map< Node, Node > d_arith_coeffs;
-    if( !Trigger::getPatternArithmetic( pat.getAttribute(InstConstantAttribute()), pat, d_arith_coeffs ) ){
+    if( !Trigger::getPatternArithmetic( quantifiers::TermDb::getInstConstAttr(pat), pat, d_arith_coeffs ) ){
       Debug("inst-match-gen") << "(?) Unknown matching pattern is " << pat << std::endl;
       Message() << "(?) Unknown matching pattern is " << pat << std::endl;
       return new DumbPatMatcher();
@@ -1033,7 +1032,7 @@ PatMatcher* mkPattern( Node pat, QuantifiersEngine* qe ){
 
 ArithMatcher::ArithMatcher(Node pat, QuantifiersEngine* qe): d_pattern(pat){
 
-  if(Trigger::getPatternArithmetic(pat.getAttribute(InstConstantAttribute()), pat, d_arith_coeffs ) )
+  if(Trigger::getPatternArithmetic(quantifiers::TermDb::getInstConstAttr(pat), pat, d_arith_coeffs ) )
     {
     Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_pattern << std::endl;
     Assert(false);
diff --git a/src/theory/rewriterules/rr_inst_match.h b/src/theory/rewriterules/rr_inst_match.h
index 3ec9438fd..aa89430c1 100644
--- a/src/theory/rewriterules/rr_inst_match.h
+++ b/src/theory/rewriterules/rr_inst_match.h
@@ -67,7 +67,7 @@ public:
   /** legal candidate */
   static inline bool isLegalCandidate( TNode n ){
     return !n.getAttribute(NoMatchAttribute()) &&
-      ( !options::cbqi() || !n.hasAttribute(InstConstantAttribute())) &&
+      ( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(n)) &&
       ( !options::efficientEMatching() || n.hasAttribute(AvailableInTermDb()) );
 }
 
diff --git a/src/theory/rewriterules/rr_trigger.cpp b/src/theory/rewriterules/rr_trigger.cpp
index 7e35be7ad..13250cf1b 100644
--- a/src/theory/rewriterules/rr_trigger.cpp
+++ b/src/theory/rewriterules/rr_trigger.cpp
@@ -65,7 +65,7 @@ bool Trigger::getNextMatch(){
 
 int Trigger::addInstantiations( InstMatch& baseMatch ){
   int addedLemmas = d_mg->addInstantiations( baseMatch,
-                                             d_nodes[0].getAttribute(InstConstantAttribute()),
+                                             quantifiers::TermDb::getInstConstAttr(d_nodes[0]),
                                              d_quantEngine);
   if( addedLemmas>0 ){
     Debug("inst-trigger") << "Added " << addedLemmas << " lemmas, trigger was ";
@@ -91,7 +91,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
       qe->getTermDatabase()->computeVarContains( temp[i] );
       for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ temp[i] ].size(); j++ ){
         Node v = qe->getTermDatabase()->d_var_contains[ temp[i] ][j];
-        if( v.getAttribute(InstConstantAttribute())==f ){
+        if( quantifiers::TermDb::getInstConstAttr(v)==f ){
           if( vars.find( v )==vars.end() ){
             vars[ v ] = true;
             foundVar = true;
@@ -181,7 +181,7 @@ bool Trigger::isUsableTrigger( std::vector< Node >& nodes, Node f ){
 }
 
 bool Trigger::isUsable( Node n, Node f ){
-  if( n.getAttribute(InstConstantAttribute())==f ){
+  if( quantifiers::TermDb::getInstConstAttr(n)==f ){
     if( !isAtomicTrigger( n ) && n.getKind()!=INST_CONSTANT ){
       std::map< Node, Node > coeffs;
       return getPatternArithmetic( f, n, coeffs );
@@ -201,7 +201,7 @@ bool Trigger::isUsable( Node n, Node f ){
 bool Trigger::isSimpleTrigger( Node n ){
   if( isAtomicTrigger( n ) ){
     for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      if( n[i].getKind()!=INST_CONSTANT && n[i].hasAttribute(InstConstantAttribute()) ){
+      if( n[i].getKind()!=INST_CONSTANT && quantifiers::TermDb::hasInstConstAttr(n[i]) ){
         return false;
       }
     }
@@ -318,9 +318,9 @@ bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coef
     Assert( coeffs.empty() );
     NodeBuilder<> t(kind::PLUS);
     for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      if( n[i].hasAttribute(InstConstantAttribute()) ){
+      if( quantifiers::TermDb::hasInstConstAttr(n[i]) ){
         if( n[i].getKind()==INST_CONSTANT ){
-          if( n[i].getAttribute(InstConstantAttribute())==f ){
+          if( quantifiers::TermDb::getInstConstAttr(n[i])==f ){
             coeffs[ n[i] ] = Node::null();
           }else{
             coeffs.clear();
@@ -343,12 +343,12 @@ bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coef
     }
     return true;
   }else if( n.getKind()==MULT ){
-    if( n[0].getKind()==INST_CONSTANT && n[0].getAttribute(InstConstantAttribute())==f ){
-      Assert( !n[1].hasAttribute(InstConstantAttribute()) );
+    if( n[0].getKind()==INST_CONSTANT && quantifiers::TermDb::getInstConstAttr(n[0])==f ){
+      Assert( !quantifiers::TermDb::hasInstConstAttr(n[1]) );
       coeffs[ n[0] ] = n[1];
       return true;
-    }else if( n[1].getKind()==INST_CONSTANT && n[1].getAttribute(InstConstantAttribute())==f ){
-      Assert( !n[0].hasAttribute(InstConstantAttribute()) );
+    }else if( n[1].getKind()==INST_CONSTANT && quantifiers::TermDb::getInstConstAttr(n[1])==f ){
+      Assert( !quantifiers::TermDb::hasInstConstAttr(n[0]) );
       coeffs[ n[1] ] = n[0];
       return true;
     }
diff --git a/src/theory/rewriterules/rr_trigger.h b/src/theory/rewriterules/rr_trigger.h
index f1a37d937..f02f38d0e 100644
--- a/src/theory/rewriterules/rr_trigger.h
+++ b/src/theory/rewriterules/rr_trigger.h
@@ -94,8 +94,7 @@ public:
 public:
   /** is usable trigger */
   static inline bool isUsableTrigger( TNode n, TNode f ){
-    //return n.getAttribute(InstConstantAttribute())==f && n.getKind()==APPLY_UF;
-    return n.getAttribute(InstConstantAttribute())==f && isAtomicTrigger( n ) && isUsable( n, f );
+    return quantifiers::TermDb::getInstConstAttr(n)==f && isAtomicTrigger( n ) && isUsable( n, f );
   }
   static inline bool isAtomicTrigger( TNode n ){
     return
diff --git a/src/theory/rewriterules/theory_rewriterules.h b/src/theory/rewriterules/theory_rewriterules.h
index 19cb3e987..a542214b2 100644
--- a/src/theory/rewriterules/theory_rewriterules.h
+++ b/src/theory/rewriterules/theory_rewriterules.h
@@ -263,7 +263,7 @@ private:
                          rewriter::Subst & vars);
 
   //create inst variable
-  std::vector<Node> createInstVariable( std::vector<Node> & vars );
+  std::vector<Node> createInstVariable( Node r, std::vector<Node> & vars );
 
     /** statistics class */
   class Statistics {
diff --git a/src/theory/rewriterules/theory_rewriterules_rules.cpp b/src/theory/rewriterules/theory_rewriterules_rules.cpp
index 589556802..446d30d21 100644
--- a/src/theory/rewriterules/theory_rewriterules_rules.cpp
+++ b/src/theory/rewriterules/theory_rewriterules_rules.cpp
@@ -151,7 +151,7 @@ void TheoryRewriteRules::addRewriteRule(const Node r)
     vars.push_back(*v);
   };
   /* Instantiation version */
-  std::vector<Node> inst_constants = createInstVariable(vars);
+  std::vector<Node> inst_constants = createInstVariable(r,vars);
   /* Body/Remove_term/Guards/Triggers */
   Node body = r[2][1];
   TNode new_terms = r[2][1];
@@ -376,7 +376,7 @@ bool TheoryRewriteRules::addRewritePattern(TNode pattern, TNode body,
 
 }
 
-std::vector<Node> TheoryRewriteRules::createInstVariable( std::vector<Node> & vars ){
+std::vector<Node> TheoryRewriteRules::createInstVariable( Node r, std::vector<Node> & vars ){
   std::vector<Node> inst_constant;
   inst_constant.reserve(vars.size());
   for( std::vector<Node>::const_iterator v = vars.begin();
@@ -384,6 +384,11 @@ std::vector<Node> TheoryRewriteRules::createInstVariable( std::vector<Node> & va
     //make instantiation constants
     Node ic = NodeManager::currentNM()->mkInstConstant( (*v).getType() );
     inst_constant.push_back( ic );
+    InstConstantAttribute ica;
+    ic.setAttribute(ica,r);
+    //also set the no-match attribute
+    NoMatchAttribute nma;
+    ic.setAttribute(nma,true);
   };
   return inst_constant;
 }