From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 25 Sep 2015 15:58:56 +0000 (+0200)
Subject: Clear term caches for quantifiers + incremental, fixes bug 674.  Refactoring of term... 
X-Git-Tag: cvc5-1.0.0~6232
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=773963f4342bb860fe4deb1d3c65d801b6acd72f;p=cvc5.git

Clear term caches for quantifiers + incremental, fixes bug 674.  Refactoring of term database, other refactoring. Bug fixes for cbqi+datatypes.
---

diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 48041e894..4619d74e5 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -100,7 +100,7 @@ Node CandidateGeneratorQE::getNextCandidate(){
   if( d_mode==cand_term_db ){
     //get next candidate term in the uf term database
     while( d_term_iter<d_term_iter_limit ){
-      Node n = d_qe->getTermDatabase()->d_op_map[d_op][d_term_iter];
+      Node n = d_qe->getTermDatabase()->getGroundTerm( d_op, d_term_iter );
       d_term_iter++;
       if( isLegalCandidate( n ) ){
         if( d_qe->getTermDatabase()->hasTermCurrent( n ) ){
@@ -221,7 +221,7 @@ Node CandidateGeneratorQEAll::getNextCandidate() {
     Assert( d_qe->getTermDatabase()->d_type_map[d_match_pattern_type].empty() );
     //must return something
     d_firstTime = false;
-    return d_qe->getTermDatabase()->getFreeVariableForType( d_match_pattern_type );
+    return d_qe->getTermDatabase()->getModelBasisTerm( d_match_pattern_type );
   }
   return Node::null();
 }
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 896cf5dff..1cdad589b 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -1722,8 +1722,8 @@ void TermGenEnv::collectSignatureInformation() {
   d_func_args.clear();
   TypeNode tnull;
   for( std::map< Node, TermArgTrie >::iterator it = getTermDatabase()->d_func_map_trie.begin(); it != getTermDatabase()->d_func_map_trie.end(); ++it ){
-    if( !getTermDatabase()->d_op_map[it->first].empty() ){
-      Node nn = getTermDatabase()->d_op_map[it->first][0];
+    if( getTermDatabase()->getNumGroundTerms( it->first )>0 ){
+      Node nn = getTermDatabase()->getGroundTerm( it->first, 0 );
       Trace("sg-rel-sig-debug") << "Check in signature : " << nn << std::endl;
       if( d_cg->isHandledTerm( nn ) && nn.getKind()!=APPLY_SELECTOR_TOTAL && !nn.getType().isBoolean() ){
         bool do_enum = true;
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index cb969088d..180ccc448 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -88,15 +88,6 @@ bool InstMatch::empty() {
   return true;
 }
 
-void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){
-  for( unsigned i=0; i<d_vals.size(); i++ ){
-    if( d_vals[i].isNull() ){
-      Node ic = qe->getTermDatabase()->getInstantiationConstant( f, i );
-      d_vals[i] = qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
-    }
-  }
-}
-
 void InstMatch::makeRepresentative( QuantifiersEngine* qe ){
   for( unsigned i=0; i<d_vals.size(); i++ ){
     if( !d_vals[i].isNull() ){
@@ -132,7 +123,7 @@ void InstMatch::getTerms( QuantifiersEngine* qe, Node f, std::vector< Node >& in
     Node val = get( i );
     if( val.isNull() ){
       Node ic =  qe->getTermDatabase()->getInstantiationConstant( f, i );
-      val = qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
+      val = qe->getTermDatabase()->getModelBasisTerm( ic.getType() );
     }
     inst.push_back( val );
   }
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index 21220491f..6424b67d3 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -53,8 +53,6 @@ public:
   void debugPrint( const char* c );
   /** is complete? */
   bool isComplete();
-  /** make complete */
-  void makeComplete( Node f, QuantifiersEngine* qe );
   /** make representative */
   void makeRepresentative( QuantifiersEngine* qe );
   /** empty */
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 67b9d9ca2..3a626cb92 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -76,11 +76,13 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
   }else{
     std::map< Node, std::map< Node, bool > > subs_proc;
     //Node v = d_single_inv_map_to_prog[d_single_inv[0][i]];
+    bool is_cv = false;
     Node pv;
     if( curr_var.empty() ){
       pv = d_vars[i];
     }else{
       pv = curr_var.back();
+      is_cv = true;
     }
     TypeNode pvtn = pv.getType();
     Trace("cbqi-inst-debug") << "[Find instantiation for " << pv << "]" << std::endl;
@@ -89,19 +91,23 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
       pv_value = d_qe->getModel()->getValue( pv );
       Trace("cbqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl;
     }
+    Node pvr = pv;
+    if( d_qe->getMasterEqualityEngine()->hasTerm( pv ) ){
+      pvr = d_qe->getMasterEqualityEngine()->getRepresentative( pv );
+    }
 
     //if in effort=2, we must choose at least one model value
     if( (i+1)<d_vars.size() || effort!=2 ){
+      
       //[1] easy case : pv is in the equivalence class as another term not containing pv
       Trace("cbqi-inst-debug") << "[1] try based on equivalence class." << std::endl;
-      std::map< Node, Node >::iterator itr = d_curr_rep.find( pv );
-      if( itr!=d_curr_rep.end() ){
-        std::map< Node, std::vector< Node > >::iterator it_eqc = d_curr_eqc.find( itr->second );
-        Assert( it_eqc!=d_curr_eqc.end() );
+      std::map< Node, std::vector< Node > >::iterator it_eqc = d_curr_eqc.find( pvr );
+      if( it_eqc!=d_curr_eqc.end() ){
+        Trace("cbqi-inst-debug2") << "...eqc has size " << it_eqc->second.size() << std::endl;
         for( unsigned k=0; k<it_eqc->second.size(); k++ ){
           Node n = it_eqc->second[k];
           if( n!=pv ){
-            Trace("cbqi-inst-debug") << "..[1] " << i << "...try based on equal term " << n << std::endl;
+            Trace("cbqi-inst-debug") << "...try based on equal term " << n << std::endl;
             //compute d_subs_fv, which program variables are contained in n
             computeProgVars( n );
             //must be an eligible term
@@ -130,22 +136,24 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
             }
           }
         }
+      }else{
+        Trace("cbqi-inst-debug2") << "...eqc not found." << std::endl;
       }
 
       //[2] : we can solve an equality for pv
       if( pvtn.isInteger() || pvtn.isReal() ){
         ///iterate over equivalence classes to find cases where we can solve for the variable
         TypeNode pvtnb = pvtn.getBaseType();
-        Trace("cbqi-inst-debug") << "[2] try based on solving over equivalence classes." << std::endl;
+        Trace("cbqi-inst-debug") << "[2] try based on solving arithmetic equivalence classes." << std::endl;
         for( unsigned k=0; k<d_curr_type_eqc[pvtnb].size(); k++ ){
           Node r = d_curr_type_eqc[pvtnb][k];
-          std::map< Node, std::vector< Node > >::iterator it_eqc = d_curr_eqc.find( r );
+          std::map< Node, std::vector< Node > >::iterator it_reqc = d_curr_eqc.find( r );
           std::vector< Node > lhs;
           std::vector< bool > lhs_v;
           std::vector< Node > lhs_coeff;
-          Assert( it_eqc!=d_curr_eqc.end() );
-          for( unsigned kk=0; kk<it_eqc->second.size(); kk++ ){
-            Node n = it_eqc->second[kk];
+          Assert( it_reqc!=d_curr_eqc.end() );
+          for( unsigned kk=0; kk<it_reqc->second.size(); kk++ ){
+            Node n = it_reqc->second[kk];
             Trace("cbqi-inst-debug2") << "...look at term " << n << std::endl;
             //compute the variables in n
             computeProgVars( n );
@@ -228,11 +236,9 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
           }
         }
       }else if( pvtn.isDatatype() ){
+        Trace("cbqi-inst-debug") << "[2] try based on constructors in equivalence class." << std::endl;
         //look in equivalence class for a constructor
-        if( itr!=d_curr_rep.end() ){
-          std::map< Node, std::vector< Node > >::iterator it_eqc = d_curr_eqc.find( itr->second );
-          Assert( it_eqc!=d_curr_eqc.end() );
-          Trace("cbqi-inst-debug") << "[2] try based on constructors in equivalence class." << std::endl;
+        if( it_eqc!=d_curr_eqc.end() ){
           for( unsigned k=0; k<it_eqc->second.size(); k++ ){
             Node n = it_eqc->second[k];
             if( n.getKind()==APPLY_CONSTRUCTOR ){
@@ -240,6 +246,9 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
               cons[pv] = n.getOperator();
               const Datatype& dt = ((DatatypeType)(pvtn).toType()).getDatatype();
               unsigned cindex = Datatype::indexOf( n.getOperator().toExpr() );
+              if( is_cv ){
+                curr_var.pop_back();
+              }
               //now must solve for selectors applied to pv
               for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){
                 curr_var.push_back( NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][j].getSelector() ), pv ) );
@@ -253,12 +262,15 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
                 for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){
                   curr_var.pop_back();
                 }
+                if( is_cv ){
+                  curr_var.push_back( pv );
+                }
                 break;
               }
             }
           }
         }else{
-          Trace("cbqi-inst-debug2") << "... " << i << " does not have a representative." << std::endl;
+          Trace("cbqi-inst-debug2") << "... " << i << " does not have an eqc." << std::endl;
         }
       }
 
@@ -1122,7 +1134,6 @@ void CegInstantiator::processAssertions() {
   Trace("cbqi-proc") << "--- Process assertions, #var = " << d_vars.size() << ", #aux-var = " << d_aux_vars.size() << std::endl;
   d_curr_asserts.clear();
   d_curr_eqc.clear();
-  d_curr_rep.clear();
   d_curr_type_eqc.clear();
 
   eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine();
@@ -1140,7 +1151,6 @@ void CegInstantiator::processAssertions() {
     //collect information about eqc
     if( ee->hasTerm( pv ) ){
       Node pvr = ee->getRepresentative( pv );
-      d_curr_rep[pv] = pvr;
       if( d_curr_eqc.find( pvr )==d_curr_eqc.end() ){
         Trace("cbqi-proc") << "Collect equivalence class " << pvr << std::endl;
         eq::EqClassIterator eqc_i = eq::EqClassIterator( pvr, ee );
@@ -1191,11 +1201,14 @@ void CegInstantiator::processAssertions() {
       d_curr_type_eqc[rtn].push_back( r );
       if( d_curr_eqc.find( r )==d_curr_eqc.end() ){
         Trace("cbqi-proc") << "Collect equivalence class " << r << std::endl;
+        Trace("cbqi-proc-debug") << "  ";
         eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
         while( !eqc_i.isFinished() ){
+          Trace("cbqi-proc-debug") << *eqc_i << " ";
           d_curr_eqc[r].push_back( *eqc_i );
           ++eqc_i;
         }
+        Trace("cbqi-proc-debug") << std::endl;
       }
     }
     ++eqcs_i;
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 6447da1a9..2074e0f4b 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -58,7 +58,6 @@ private:
   //current assertions
   std::map< TheoryId, std::vector< Node > > d_curr_asserts;
   std::map< Node, std::vector< Node > > d_curr_eqc;
-  std::map< Node, Node > d_curr_rep;
   std::map< TypeNode, std::vector< Node > > d_curr_type_eqc;
   //auxiliary variables
   std::vector< Node > d_aux_vars;
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 47c2e1c5b..b7d82bc9e 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -458,9 +458,7 @@ bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node
     //check constraints
     for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){
       //apply substitution to the tconstraint
-      Node cons = it->first.substitute( p->getTermDatabase()->d_vars[d_q].begin(),
-                                        p->getTermDatabase()->d_vars[d_q].end(),
-                                        terms.begin(), terms.end() );
+      Node cons = p->getTermDatabase()->getInstantiatedNode( it->first, d_q, terms );
       cons = it->second ? cons : cons.negate();
       if( !entailmentTest( p, cons, p->d_effort==QuantConflictFind::effort_conflict ) ){
         return true;
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index 05e33c7b2..a70d36ac0 100644
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -38,7 +38,6 @@ struct PrioritySort {
 
 
 RewriteEngine::RewriteEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule(qe) {
-  d_true = NodeManager::currentNM()->mkConst( true );
   d_needsSort = false;
 }
 
@@ -277,7 +276,7 @@ void RewriteEngine::registerQuantifier( Node f ) {
             body_c.push_back( d_rr[f][1][j].negate() );
           }
         }
-      }else if( d_rr[f][1]!=d_true ){
+      }else if( d_rr[f][1]!=d_quantEngine->getTermDatabase()->d_true ){
         if( MatchGen::isHandled( d_rr[f][1] ) ){
           body_c.push_back( d_rr[f][1].negate() );
         }
@@ -307,4 +306,4 @@ Node RewriteEngine::getInstConstNode( Node n, Node q ) {
   }else{
     return it->second;
   }
-}
\ No newline at end of file
+}
diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
index 2e2578af5..6ad76c541 100644
--- a/src/theory/quantifiers/rewrite_engine.h
+++ b/src/theory/quantifiers/rewrite_engine.h
@@ -39,7 +39,6 @@ class RewriteEngine : public QuantifiersModule
   std::vector< Node > d_rr_quant;
   std::vector< Node > d_priority_order;
   std::map< Node, Node > d_rr;
-  Node d_true;
   /** explicitly provided patterns */
   std::map< Node, std::vector< inst::Trigger* > > d_rr_triggers;
   /** get the quantifer info object */
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index bb35ac4cd..d6f8b3af7 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -78,7 +78,7 @@ void TermArgTrie::debugPrint( const char * c, Node n, unsigned depth ) {
   }
 }
 
-TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_ccount( u ), d_op_id_count( 0 ), d_typ_id_count( 0 ) {
+TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_id_count( 0 ), d_typ_id_count( 0 ) {
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
   d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
@@ -98,7 +98,11 @@ unsigned TermDb::getNumGroundTerms( Node f ) {
   }else{
     return 0;
   }
-  //return d_op_ccount[f];
+}
+
+Node TermDb::getGroundTerm( Node f, unsigned i ) {
+  Assert( i<d_op_map[f].size() );
+  return d_op_map[f][i];
 }
 
 Node TermDb::getOperator( Node n ) {
@@ -128,51 +132,42 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi
   //don't add terms in quantifier bodies
   if( withinQuant && !options::registerQuantBodyTerms() ){
     return;
-  }
-  bool rec = false;
-  if( d_processed.find( n )==d_processed.end() ){
-    d_processed.insert(n);
-    if( !TermDb::hasInstConstAttr(n) ){
-      Trace("term-db-debug") << "register term : " << n << std::endl;
-      d_type_map[ n.getType() ].push_back( n );
-      //if this is an atomic trigger, consider adding it
-      //Call the children?
-      if( inst::Trigger::isAtomicTrigger( n ) ){
-        Trace("term-db") << "register term in db " << n << std::endl;
-        Node op = getOperator( n );
-        /*
-        int occ = d_op_ccount[op];
-        if( occ<(int)d_op_map[op].size() ){
-          d_op_map[op][occ] = n;
-        }else{
+  }else{
+    bool rec = false;
+    if( d_processed.find( n )==d_processed.end() ){
+      d_processed.insert(n);
+      if( !TermDb::hasInstConstAttr(n) ){
+        Trace("term-db-debug") << "register term : " << n << std::endl;
+        d_type_map[ n.getType() ].push_back( n );
+        //if this is an atomic trigger, consider adding it
+        if( inst::Trigger::isAtomicTrigger( n ) ){
+          Trace("term-db") << "register term in db " << n << std::endl;
+          Node op = getOperator( n );
           d_op_map[op].push_back( n );
-        }
-        d_op_ccount[op].set( occ + 1 );
-        */
-        d_op_map[op].push_back( n );
-        added.insert( n );
-
-        if( options::eagerInstQuant() ){
-          for( size_t i=0; i<n.getNumChildren(); i++ ){
-            if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){
-              int addedLemmas = 0;
-              for( size_t i=0; i<d_op_triggers[op].size(); i++ ){
-                addedLemmas += d_op_triggers[op][i]->addTerm( n );
+          added.insert( n );
+
+          if( options::eagerInstQuant() ){
+            for( unsigned i=0; i<n.getNumChildren(); i++ ){
+              if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){
+                int addedLemmas = 0;
+                for( unsigned i=0; i<d_op_triggers[op].size(); i++ ){
+                  addedLemmas += d_op_triggers[op][i]->addTerm( n );
+                }
               }
             }
           }
         }
       }
+      rec = true;
     }
-    rec = true;
-  }
-  if( withinInstClosure && d_iclosure_processed.find( n )==d_iclosure_processed.end() ){
-    d_iclosure_processed.insert( n );
-    rec = true;
-  }
-  if( rec && n.getKind()!=FORALL ){
-    for( size_t i=0; i<n.getNumChildren(); i++ ){
-      addTerm( n[i], added, withinQuant, withinInstClosure );
+    if( withinInstClosure && d_iclosure_processed.find( n )==d_iclosure_processed.end() ){
+      d_iclosure_processed.insert( n );
+      rec = true;
+    }
+    if( rec && n.getKind()!=FORALL ){
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        addTerm( n[i], added, withinQuant, withinInstClosure );
+      }
     }
   }
 }
@@ -413,25 +408,6 @@ bool TermDb::isInstClosure( Node r ) {
   return d_iclosure_processed.find( r )!=d_iclosure_processed.end();
 }
 
-//checks whether a type is not Array and is reasonably small enough (<1000) such that all of its domain elements can be enumerated
-bool TermDb::mayComplete( TypeNode tn ) {
-  std::map< TypeNode, bool >::iterator it = d_may_complete.find( tn );
-  if( it==d_may_complete.end() ){
-    bool mc = false;
-    if( isClosedEnumerableType( tn ) && tn.getCardinality().isFinite() && !tn.getCardinality().isLargeFinite() ){
-      Node card = NodeManager::currentNM()->mkConst( Rational(tn.getCardinality().getFiniteCardinality()) );
-      Node oth = NodeManager::currentNM()->mkConst( Rational(1000) );
-      Node eq = NodeManager::currentNM()->mkNode( LEQ, card, oth );
-      eq = Rewriter::rewrite( eq );
-      mc = eq==d_true;
-    }
-    d_may_complete[tn] = mc;
-    return mc;
-  }else{
-    return it->second;
-  }
-}
-
 void TermDb::setHasTerm( Node n ) {
   Trace("term-db-debug2") << "hasTerm : " << n  << std::endl;
   //if( inst::Trigger::isAtomicTrigger( n ) ){
@@ -441,13 +417,14 @@ void TermDb::setHasTerm( Node n ) {
       setHasTerm( n[i] );
     }
   }
-    /*
-  }else{
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      setHasTerm( n[i] );
-    }
-  }
-  */
+}
+
+void TermDb::presolve() {
+  //reset the caches that are SAT context-independent
+  d_op_map.clear();
+  d_type_map.clear();
+  d_processed.clear();
+  d_iclosure_processed.clear();
 }
 
 void TermDb::reset( Theory::Effort effort ){
@@ -593,7 +570,7 @@ Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
   if( d_model_basis_term.find( tn )==d_model_basis_term.end() ){
     Node mbt;
     if( tn.isInteger() || tn.isReal() ){
-      mbt = NodeManager::currentNM()->mkConst( Rational( 0 ) );
+      mbt = d_zero;
     }else if( isClosedEnumerableType( tn ) ){
       mbt = tn.mkGroundTerm();
     }else{
@@ -603,6 +580,9 @@ Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
         ss << "e_" << tn;
         mbt = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "is a model basis term" );
         Trace("mkVar") << "ModelBasis:: Make variable " << mbt << " : " << tn << std::endl;
+        if( options::instMaxLevel()!=-1 ){
+          QuantifiersEngine::setInstantiationLevelAttr( mbt, 0 );
+        }
       }else{
         mbt = d_type_map[ tn ][ 0 ];
       }
@@ -632,24 +612,24 @@ Node TermDb::getModelBasisOpTerm( Node op ){
   return d_model_basis_op_term[op];
 }
 
-Node TermDb::getModelBasis( Node f, Node n ){
+Node TermDb::getModelBasis( Node q, Node n ){
   //make model basis
-  if( d_model_basis_terms.find( f )==d_model_basis_terms.end() ){
-    for( int j=0; j<(int)f[0].getNumChildren(); j++ ){
-      d_model_basis_terms[f].push_back( getModelBasisTerm( f[0][j].getType() ) );
+  if( d_model_basis_terms.find( q )==d_model_basis_terms.end() ){
+    for( unsigned j=0; j<q[0].getNumChildren(); j++ ){
+      d_model_basis_terms[q].push_back( getModelBasisTerm( q[0][j].getType() ) );
     }
   }
-  Node gn = n.substitute( d_inst_constants[f].begin(), d_inst_constants[f].end(),
-                          d_model_basis_terms[f].begin(), d_model_basis_terms[f].end() );
+  Node gn = n.substitute( d_inst_constants[q].begin(), d_inst_constants[q].end(),
+                          d_model_basis_terms[q].begin(), d_model_basis_terms[q].end() );
   return gn;
 }
 
-Node TermDb::getModelBasisBody( Node f ){
-  if( d_model_basis_body.find( f )==d_model_basis_body.end() ){
-    Node n = getInstConstantBody( f );
-    d_model_basis_body[f] = getModelBasis( f, n );
+Node TermDb::getModelBasisBody( Node q ){
+  if( d_model_basis_body.find( q )==d_model_basis_body.end() ){
+    Node n = getInstConstantBody( q );
+    d_model_basis_body[q] = getModelBasis( q, n );
   }
-  return d_model_basis_body[f];
+  return d_model_basis_body[q];
 }
 
 void TermDb::computeModelBasisArgAttribute( Node n ){
@@ -660,7 +640,7 @@ void TermDb::computeModelBasisArgAttribute( Node n ){
     }
     uint64_t val = 0;
     //determine if it has model basis attribute
-    for( int j=0; j<(int)n.getNumChildren(); j++ ){
+    for( unsigned j=0; j<n.getNumChildren(); j++ ){
       if( n[j].getAttribute(ModelBasisAttribute()) ){
         val++;
       }
@@ -670,21 +650,21 @@ void TermDb::computeModelBasisArgAttribute( Node n ){
   }
 }
 
-void TermDb::makeInstantiationConstantsFor( Node f ){
-  if( d_inst_constants.find( f )==d_inst_constants.end() ){
-    Debug("quantifiers-engine") << "Instantiation constants for " << f << " : " << std::endl;
-    for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
-      d_vars[f].push_back( f[0][i] );
+void TermDb::makeInstantiationConstantsFor( Node q ){
+  if( d_inst_constants.find( q )==d_inst_constants.end() ){
+    Debug("quantifiers-engine") << "Instantiation constants for " << q << " : " << std::endl;
+    for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+      d_vars[q].push_back( q[0][i] );
       //make instantiation constants
-      Node ic = NodeManager::currentNM()->mkInstConstant( f[0][i].getType() );
-      d_inst_constants_map[ic] = f;
-      d_inst_constants[ f ].push_back( ic );
+      Node ic = NodeManager::currentNM()->mkInstConstant( q[0][i].getType() );
+      d_inst_constants_map[ic] = q;
+      d_inst_constants[ q ].push_back( ic );
       Debug("quantifiers-engine") << "  " << ic << std::endl;
       //set the var number attribute
       InstVarNumAttribute ivna;
-      ic.setAttribute(ivna,i);
+      ic.setAttribute( ivna, i );
       InstConstantAttribute ica;
-      ic.setAttribute(ica,f);
+      ic.setAttribute( ica, q );
       //also set the no-match attribute
       NoMatchAttribute nma;
       ic.setAttribute(nma,true);
@@ -695,16 +675,16 @@ void TermDb::makeInstantiationConstantsFor( Node f ){
 
 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() ){
+    Node q;
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      q = getInstConstAttr(n[i]);
+      if( !q.isNull() ){
         break;
       }
     }
     InstConstantAttribute ica;
-    n.setAttribute(ica,f);
-    if( !f.isNull() ){
+    n.setAttribute(ica, q);
+    if( !q.isNull() ){
       //also set the no-match attribute
       NoMatchAttribute nma;
       n.setAttribute(nma,true);
@@ -730,9 +710,9 @@ void TermDb::getBoundVars( Node n, std::vector< Node >& 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 );
+/** get the i^th instantiation constant of q */
+Node TermDb::getInstantiationConstant( Node q, int i ) const {
+  std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( q );
   if( it!=d_inst_constants.end() ){
     return it->second[i];
   }else{
@@ -740,9 +720,9 @@ Node TermDb::getInstantiationConstant( Node f, int i ) const {
   }
 }
 
-/** get number of instantiation constants for f */
-int TermDb::getNumInstantiationConstants( Node f ) const {
-  std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( f );
+/** get number of instantiation constants for q */
+int TermDb::getNumInstantiationConstants( Node q ) const {
+  std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( q );
   if( it!=d_inst_constants.end() ){
     return (int)it->second.size();
   }else{
@@ -750,19 +730,19 @@ int TermDb::getNumInstantiationConstants( Node f ) const {
   }
 }
 
-Node TermDb::getInstConstantBody( Node f ){
-  std::map< Node, Node >::iterator it = d_inst_const_body.find( f );
+Node TermDb::getInstConstantBody( Node q ){
+  std::map< Node, Node >::iterator it = d_inst_const_body.find( q );
   if( it==d_inst_const_body.end() ){
-    Node n = getInstConstantNode( f[1], f );
-    d_inst_const_body[ f ] = n;
+    Node n = getInstConstantNode( q[1], q );
+    d_inst_const_body[ q ] = n;
     return n;
   }else{
     return it->second;
   }
 }
 
-Node TermDb::getCounterexampleLiteral( Node f ){
-  if( d_ce_lit.find( f )==d_ce_lit.end() ){
+Node TermDb::getCounterexampleLiteral( Node q ){
+  if( d_ce_lit.find( q )==d_ce_lit.end() ){
     /*
     Node ceBody = getInstConstantBody( f );
     //check if any variable are of bad types, and fail if so
@@ -776,18 +756,23 @@ Node TermDb::getCounterexampleLiteral( Node f ){
     Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() );
     //otherwise, ensure literal
     Node ceLit = d_quantEngine->getValuation().ensureLiteral( g );
-    d_ce_lit[ f ] = ceLit;
+    d_ce_lit[ q ] = ceLit;
   }
-  return d_ce_lit[ f ];
+  return d_ce_lit[ q ];
 }
 
-Node TermDb::getInstConstantNode( Node n, Node f ){
-  makeInstantiationConstantsFor( f );
-  Node n2 = n.substitute( d_vars[f].begin(), d_vars[f].end(),
-                          d_inst_constants[f].begin(), d_inst_constants[f].end() );
+Node TermDb::getInstConstantNode( Node n, Node q ){
+  makeInstantiationConstantsFor( q );
+  Node n2 = n.substitute( d_vars[q].begin(), d_vars[q].end(),
+                          d_inst_constants[q].begin(), d_inst_constants[q].end() );
   return n2;
 }
 
+Node TermDb::getInstantiatedNode( Node n, Node q, std::vector< Node >& terms ) {
+  Assert( d_vars[q].size()==terms.size() );
+  return n.substitute( d_vars[q].begin(), d_vars[q].end(), terms.begin(), terms.end() );
+}
+
 
 void getSelfSel( const DatatypeConstructor& dc, Node n, TypeNode ntn, std::vector< Node >& selfSel ){
   for( unsigned j=0; j<dc.getNumArgs(); j++ ){
@@ -979,34 +964,23 @@ bool TermDb::isClosedEnumerableType( TypeNode tn ) {
   }
 }
 
-Node TermDb::getFreeVariableForInstConstant( Node n ){
-  return getFreeVariableForType( n.getType() );
-}
-
-Node TermDb::getFreeVariableForType( TypeNode tn ) {
-  if( d_free_vars.find( tn )==d_free_vars.end() ){
-    for( unsigned i=0; i<d_type_map[ tn ].size(); i++ ){
-      if( !quantifiers::TermDb::hasInstConstAttr(d_type_map[ tn ][ i ]) ){
-        d_free_vars[tn] = d_type_map[ tn ][ i ];
-      }
-    }
-    if( d_free_vars.find( tn )==d_free_vars.end() ){
-      //if integer or real, make zero
-      if( tn.isInteger() || tn.isReal() ){
-        Rational z(0);
-        d_free_vars[tn] = NodeManager::currentNM()->mkConst( z );
-      }else{
-        Node n = NodeManager::currentNM()->mkSkolem( "freevar", tn, "is a free variable created by termdb" );
-        d_free_vars[tn] = n;
-        Trace("mkVar") << "FreeVar:: Make variable " << n << " : " << tn << std::endl;
-        //must set instantiation level attribute to 0 if we are using instantiation max level
-        if( options::instMaxLevel()!=-1 ){
-          QuantifiersEngine::setInstantiationLevelAttr( n, 0 );
-        }
-      }
+//checks whether a type is not Array and is reasonably small enough (<1000) such that all of its domain elements can be enumerated
+bool TermDb::mayComplete( TypeNode tn ) {
+  std::map< TypeNode, bool >::iterator it = d_may_complete.find( tn );
+  if( it==d_may_complete.end() ){
+    bool mc = false;
+    if( isClosedEnumerableType( tn ) && tn.getCardinality().isFinite() && !tn.getCardinality().isLargeFinite() ){
+      Node card = NodeManager::currentNM()->mkConst( Rational(tn.getCardinality().getFiniteCardinality()) );
+      Node oth = NodeManager::currentNM()->mkConst( Rational(1000) );
+      Node eq = NodeManager::currentNM()->mkNode( LEQ, card, oth );
+      eq = Rewriter::rewrite( eq );
+      mc = eq==d_true;
     }
+    d_may_complete[tn] = mc;
+    return mc;
+  }else{
+    return it->second;
   }
-  return d_free_vars[tn];
 }
 
 void TermDb::computeVarContains( Node n, std::vector< Node >& varContains ) {
@@ -1328,7 +1302,7 @@ Node TermDb::getVtsDelta( bool isFree, bool create ) {
   if( create ){
     if( d_vts_delta_free.isNull() ){
       d_vts_delta_free = NodeManager::currentNM()->mkSkolem( "delta_free", NodeManager::currentNM()->realType(), "free delta for virtual term substitution" );
-      Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_vts_delta_free, NodeManager::currentNM()->mkConst( Rational( 0 ) ) );
+      Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_vts_delta_free, d_zero );
       d_quantEngine->getOutputChannel().lemma( delta_lem );
     }
     if( d_vts_delta.isNull() ){
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 477b964ee..682a9f8e0 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -134,15 +134,10 @@ private:
   std::hash_set< Node, NodeHashFunction > d_processed;
   /** terms processed */
   std::hash_set< Node, NodeHashFunction > d_iclosure_processed;
-private:
   /** select op map */
   std::map< Node, std::map< TypeNode, Node > > d_par_op_map;
-  /** count number of ground terms per operator (user-context dependent) */
-  NodeIntMap d_op_ccount;
   /** set has term */
   void setHasTerm( Node n );
-  /** may complete */
-  std::map< TypeNode, bool > d_may_complete;
 public:
   TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe );
   ~TermDb(){}
@@ -152,25 +147,34 @@ public:
   /** constants */
   Node d_zero;
   Node d_one;
-  /** ground terms */
-  unsigned getNumGroundTerms( Node f );
-  /** count number of non-redundant ground terms per operator */
-  std::map< Node, int > d_op_nonred_count;
+  
   /** map from operators to ground terms for that operator */
   std::map< Node, std::vector< Node > > d_op_map;
+  /** map from type nodes to terms of that type */
+  std::map< TypeNode, std::vector< Node > > d_type_map;
+  
+  
+  /** count number of non-redundant ground terms per operator */
+  std::map< Node, int > d_op_nonred_count;
+  /**mapping from UF terms to representatives of their arguments */
+  std::map< TNode, std::vector< TNode > > d_arg_reps;
+  /** map from operators to trie */
+  std::map< Node, TermArgTrie > d_func_map_trie;
+  std::map< Node, TermArgTrie > d_func_map_eqc_trie;
   /** has map */
   std::map< Node, bool > d_has_map;
   /** map from reps to a term in eqc in d_has_map */
   std::map< Node, Node > d_term_elig_eqc;
-  /** map from operators to trie */
-  std::map< Node, TermArgTrie > d_func_map_trie;
-  std::map< Node, TermArgTrie > d_func_map_eqc_trie;
-  /**mapping from UF terms to representatives of their arguments */
-  std::map< TNode, std::vector< TNode > > d_arg_reps;
-  /** map from type nodes to terms of that type */
-  std::map< TypeNode, std::vector< Node > > d_type_map;
+  
+public:
+  /** ground terms for operator */
+  unsigned getNumGroundTerms( Node f );
+  /** get ground term for operator */
+  Node getGroundTerm( Node f, unsigned i );
   /** add a term to the database */
   void addTerm( Node n, std::set< Node >& added, bool withinQuant = false, bool withinInstClosure = false );
+  /** presolve (called once per user check-sat) */
+  void presolve();
   /** reset (calculate which terms are active) */
   void reset( Theory::Effort effort );
   /** get operator*/
@@ -200,8 +204,7 @@ public:
   Node getEligibleTermInEqc( TNode r );
   /** is inst closure */
   bool isInstClosure( Node r );
-  /** may complete */
-  bool mayComplete( TypeNode tn );
+  
 //for model basis
 private:
   //map from types to model basis terms
@@ -220,12 +223,14 @@ public:
   //get model basis term for op
   Node getModelBasisOpTerm( Node op );
   //get model basis
-  Node getModelBasis( Node f, Node n );
+  Node getModelBasis( Node q, Node n );
   //get model basis body
-  Node getModelBasisBody( Node f );
+  Node getModelBasisBody( Node q );
 
 //for inst constant
 private:
+  /** map from universal quantifiers to the list of variables */
+  std::map< Node, std::vector< Node > > d_vars;
   /** map from universal quantifiers to the list of instantiation constants */
   std::map< Node, std::vector< Node > > d_inst_constants;
   /** map from universal quantifiers to their inst constant body */
@@ -235,30 +240,32 @@ private:
   /** instantiation constants to universal quantifiers */
   std::map< Node, Node > d_inst_constants_map;
   /** make instantiation constants for */
-  void makeInstantiationConstantsFor( Node f );
+  void makeInstantiationConstantsFor( Node q );
 public:
-  /** get the i^th instantiation constant of f */
-  Node getInstantiationConstant( Node f, int i ) const;
-  /** get number of instantiation constants for f */
-  int getNumInstantiationConstants( Node f ) const;
-  /** get the ce body f[e/x] */
-  Node getInstConstantBody( Node f );
+  /** get the i^th instantiation constant of q */
+  Node getInstantiationConstant( Node q, int i ) const;
+  /** get number of instantiation constants for q */
+  int getNumInstantiationConstants( Node q ) const;
+  /** get the ce body q[e/x] */
+  Node getInstConstantBody( Node q );
   /** get counterexample literal (for cbqi) */
-  Node getCounterexampleLiteral( Node f );
-  /** returns node n with bound vars of f replaced by instantiation constants of f
+  Node getCounterexampleLiteral( Node q );
+  /** returns node n with bound vars of q replaced by instantiation constants of q
       node n : is the future pattern
-      node f : is the quantifier containing which bind the variable
+      node q : is the quantifier containing which bind the variable
       return a pattern where the variable are replaced by variable for
       instantiation.
    */
-  Node getInstConstantNode( Node n, Node f );
+  Node getInstConstantNode( Node n, Node q );
+  /** get substituted node */
+  Node getInstantiatedNode( Node n, Node q, std::vector< Node >& terms );
 
   static Node getInstConstAttr( Node n );
   static bool hasInstConstAttr( Node n );
 //for bound variables
 public:
   //get bound variables in n
-  static void getBoundVars( Node n, std::vector< Node >& bvs);
+  static void getBoundVars( Node n, std::vector< Node >& bvs );
 
 
 //for skolem
@@ -285,24 +292,16 @@ private:
   std::vector< TypeEnumerator > d_typ_enum;
   // closed enumerable type cache
   std::map< TypeNode, bool > d_typ_closed_enum;
+  /** may complete */
+  std::map< TypeNode, bool > d_may_complete;
 public:
   //get nth term for type
   Node getEnumerateTerm( TypeNode tn, unsigned index );
   //does this type have an enumerator that produces constants that are handled by ground theory solvers
   bool isClosedEnumerableType( TypeNode tn );
-
-//miscellaneous
-public:
-  /** map from universal quantifiers to the list of variables */
-  std::map< Node, std::vector< Node > > d_vars;
-  /** free variable for instantiation constant type */
-  std::map< TypeNode, Node > d_free_vars;
-public:
-  /** get free variable for instantiation constant */
-  Node getFreeVariableForInstConstant( Node n );
-  /** get free variable for type */
-  Node getFreeVariableForType( TypeNode tn );
-
+  // may complete
+  bool mayComplete( TypeNode tn );
+  
 //for triggers
 private:
   /** helper function for compute var contains */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 24d422909..a2c6a9ddf 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -81,7 +81,8 @@ quantifiers::TermDb * QuantifiersModule::getTermDatabase() {
 QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te):
 d_te( te ),
 d_lemmas_produced_c(u),
-d_skolemized(u){
+d_skolemized(u),
+d_presolve(u, true){
   d_eq_query = new EqualityQueryQuantifiersEngine( this );
   d_term_db = new quantifiers::TermDb( c, u, this );
   d_tr_trie = new inst::TriggerTrie;
@@ -288,6 +289,15 @@ void QuantifiersEngine::presolve() {
   for( unsigned i=0; i<d_modules.size(); i++ ){
     d_modules[i]->presolve();
   }
+  d_term_db->presolve();
+  d_presolve = false;
+  //clear presolve cache
+  for( unsigned i=0; i<d_presolve_cache.size(); i++ ){
+    addTermToDatabase( d_presolve_cache[i], d_presolve_cache_wq[i], d_presolve_cache_wic[i] );
+  }
+  d_presolve_cache.clear();
+  d_presolve_cache_wq.clear();
+  d_presolve_cache_wic.clear();
 }
 
 void QuantifiersEngine::check( Theory::Effort e ){
@@ -315,6 +325,9 @@ void QuantifiersEngine::check( Theory::Effort e ){
       }
     }
   }
+  
+  d_hasAddedLemma = false;
+  
   Trace("quant-engine-debug") << "Quantifiers Engine call to check, level = " << e << std::endl;
   if( needsCheck ){
     Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl;
@@ -345,7 +358,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
     }
 
     //reset relevant information
-    d_hasAddedLemma = false;
 
     //flush previous lemmas (for instance, if was interupted), or other lemmas to process
     flushLemmas();
@@ -419,7 +431,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
     Trace("quant-engine") << "Finished quantifiers engine check." << std::endl;
   }else{
     Trace("quant-engine") << "Quantifiers Engine does not need check." << std::endl;
-    d_hasAddedLemma = false;
   }
   //SAT case
   if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){
@@ -597,17 +608,23 @@ quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() {
 }
 
 void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool withinInstClosure ){
-  std::set< Node > added;
-  getTermDatabase()->addTerm( n, added, withinQuant, withinInstClosure );
-  //maybe have triggered instantiations if we are doing eager instantiation
-  if( options::eagerInstQuant() ){
-    flushLemmas();
-  }
-  //added contains also the Node that just have been asserted in this branch
-  if( d_quant_rel ){
-    for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){
-      if( !withinQuant ){
-        d_quant_rel->setRelevance( i->getOperator(), 0 );
+  if( d_presolve ){
+    d_presolve_cache.push_back( n );
+    d_presolve_cache_wq.push_back( withinQuant );
+    d_presolve_cache_wic.push_back( withinInstClosure );
+  }else{
+    std::set< Node > added;
+    getTermDatabase()->addTerm( n, added, withinQuant, withinInstClosure );
+    //maybe have triggered instantiations if we are doing eager instantiation
+    if( options::eagerInstQuant() ){
+      flushLemmas();
+    }
+    //added contains also the Node that just have been asserted in this branch
+    if( d_quant_rel ){
+      for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){
+        if( !withinQuant ){
+          d_quant_rel->setRelevance( i->getOperator(), 0 );
+        }
       }
     }
   }
@@ -742,31 +759,31 @@ Node QuantifiersEngine::getSubstitute( Node n, std::vector< Node >& terms ){
 }
 
 
-Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){
+Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms ){
   Node body;
   //process partial instantiation if necessary
-  if( d_term_db->d_vars[f].size()!=vars.size() ){
-    body = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
+  if( d_term_db->d_vars[q].size()!=vars.size() ){
+    body = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
     std::vector< Node > uninst_vars;
     //doing a partial instantiation, must add quantifier for all uninstantiated variables
-    for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
-      if( std::find( vars.begin(), vars.end(), f[0][i] )==vars.end() ){
-        uninst_vars.push_back( f[0][i] );
+    for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+      if( std::find( vars.begin(), vars.end(), q[0][i] )==vars.end() ){
+        uninst_vars.push_back( q[0][i] );
       }
     }
     Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, uninst_vars );
     body = NodeManager::currentNM()->mkNode( FORALL, bvl, body );
-    Trace("partial-inst") << "Partial instantiation : " << f << std::endl;
+    Trace("partial-inst") << "Partial instantiation : " << q << std::endl;
     Trace("partial-inst") << "                      : " << body << std::endl;
   }else{
     if( options::cbqi() ){
-      body = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
+      body = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
     }else{
       //do optimized version
-      Node icb = d_term_db->getInstConstantBody( f );
+      Node icb = d_term_db->getInstConstantBody( q );
       body = getSubstitute( icb, terms );
       if( Debug.isOn("check-inst") ){
-        Node body2 = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
+        Node body2 = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
         if( body!=body2 ){
           Debug("check-inst") << "Substitution is wrong : " << body << " " << body2 << std::endl;
         }
@@ -776,16 +793,15 @@ Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& vars, std
   return body;
 }
 
-Node QuantifiersEngine::getInstantiation( Node f, InstMatch& m ){
+Node QuantifiersEngine::getInstantiation( Node q, InstMatch& m ){
   std::vector< Node > vars;
   std::vector< Node > terms;
-  computeTermVector( f, m, vars, terms );
-  return getInstantiation( f, vars, terms );
+  computeTermVector( q, m, vars, terms );
+  return getInstantiation( q, vars, terms );
 }
 
-Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& terms ) {
-  d_term_db->makeInstantiationConstantsFor( f );
-  return getInstantiation( f, d_term_db->d_inst_constants[f], terms );
+Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& terms ) {
+  return getInstantiation( q, d_term_db->d_vars[q], terms );
 }
 
 /*
@@ -835,31 +851,31 @@ void QuantifiersEngine::addRequirePhase( Node lit, bool req ){
   d_phase_req_waiting[lit] = req;
 }
 
-bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool mkRep, bool modEq, bool modInst, bool doVts ){
+bool QuantifiersEngine::addInstantiation( Node q, InstMatch& m, bool mkRep, bool modEq, bool modInst, bool doVts ){
   std::vector< Node > terms;
-  m.getTerms( this, f, terms );
-  return addInstantiation( f, terms, mkRep, modEq, modInst, doVts );
+  m.getTerms( this, q, terms );
+  return addInstantiation( q, terms, mkRep, modEq, modInst, doVts );
 }
 
-bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bool mkRep, bool modEq, bool modInst, bool doVts ) {
+bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bool mkRep, bool modEq, bool modInst, bool doVts ) {
   // For resource-limiting (also does a time check).
   getOutputChannel().safePoint(options::quantifierStep());
 
-  Assert( terms.size()==f[0].getNumChildren() );
-  Trace("inst-add-debug") << "For quantified formula " << f << ", add instantiation: " << std::endl;
+  Assert( terms.size()==q[0].getNumChildren() );
+  Trace("inst-add-debug") << "For quantified formula " << q << ", add instantiation: " << std::endl;
   for( unsigned i=0; i<terms.size(); i++ ){
-    Trace("inst-add-debug") << "  " << f[0][i] << " -> " << terms[i] << std::endl;
+    Trace("inst-add-debug") << "  " << q[0][i] << " -> " << terms[i] << std::endl;
     //make it representative, this is helpful for recognizing duplication
     if( mkRep ){
       //pick the best possible representative for instantiation, based on past use and simplicity of term
-      terms[i] = d_eq_query->getInternalRepresentative( terms[i], f, i );
+      terms[i] = d_eq_query->getInternalRepresentative( terms[i], q, i );
     }
   }
 
   //check based on instantiation level
   if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){
     for( unsigned i=0; i<terms.size(); i++ ){
-      if( !d_term_db->isTermEligibleForInstantiation( terms[i], f, true ) ){
+      if( !d_term_db->isTermEligibleForInstantiation( terms[i], q, true ) ){
         return false;
       }
     }
@@ -868,9 +884,9 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo
   if( options::instNoEntail() ){
     std::map< TNode, TNode > subs;
     for( unsigned i=0; i<terms.size(); i++ ){
-      subs[f[0][i]] = terms[i];
+      subs[q[0][i]] = terms[i];
     }
-    if( d_term_db->isEntailed( f[1], subs, false, true ) ){
+    if( d_term_db->isEntailed( q[1], subs, false, true ) ){
       Trace("inst-add-debug") << " -> Currently entailed." << std::endl;
       return false;
     }
@@ -881,17 +897,17 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo
   if( options::incrementalSolving() ){
     Trace("inst-add-debug") << "Adding into context-dependent inst trie, modEq = " << modEq << ", modInst = " << modInst << std::endl;
     inst::CDInstMatchTrie* imt;
-    std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( f );
+    std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( q );
     if( it!=d_c_inst_match_trie.end() ){
       imt = it->second;
     }else{
       imt = new CDInstMatchTrie( getUserContext() );
-      d_c_inst_match_trie[f] = imt;
+      d_c_inst_match_trie[q] = imt;
     }
-    alreadyExists = !imt->addInstMatch( this, f, terms, getUserContext(), modEq, modInst );
+    alreadyExists = !imt->addInstMatch( this, q, terms, getUserContext(), modEq, modInst );
   }else{
     Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
-    alreadyExists = !d_inst_match_trie[f].addInstMatch( this, f, terms, modEq, modInst );
+    alreadyExists = !d_inst_match_trie[q].addInstMatch( this, q, terms, modEq, modInst );
   }
   if( alreadyExists ){
     Trace("inst-add-debug") << " -> Already exists." << std::endl;
@@ -902,7 +918,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo
 
   //add the instantiation
   Trace("inst-add-debug") << "Constructing instantiation..." << std::endl;
-  bool addedInst = addInstantiation( f, d_term_db->d_vars[f], terms, doVts );
+  bool addedInst = addInstantiation( q, d_term_db->d_vars[q], terms, doVts );
   //report the result
   if( addedInst ){
     Trace("inst-add-debug") << " -> Success." << std::endl;
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 5e8db2561..3cdd5bae7 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -190,6 +190,12 @@ private:
   /** inst round counters */
   int d_ierCounter;
   int d_ierCounter_lc;
+  /** has presolve been called */
+  context::CDO< bool > d_presolve;
+  /** presolve cache */
+  std::vector< Node > d_presolve_cache;
+  std::vector< bool > d_presolve_cache_wq;
+  std::vector< bool > d_presolve_cache_wic;
 private:
   KEEP_STATISTIC(TimerStat, d_time, "theory::QuantifiersEngine::time");
 public:
@@ -278,11 +284,11 @@ private:
   void flushLemmas();
 public:
   /** get instantiation */
-  Node getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms );
+  Node getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms );
   /** get instantiation */
-  Node getInstantiation( Node f, InstMatch& m );
+  Node getInstantiation( Node q, InstMatch& m );
   /** get instantiation */
-  Node getInstantiation( Node f, std::vector< Node >& terms );
+  Node getInstantiation( Node q, std::vector< Node >& terms );
   /** do substitution */
   Node getSubstitute( Node n, std::vector< Node >& terms );
   /** add lemma lem */
@@ -290,9 +296,9 @@ public:
   /** add require phase */
   void addRequirePhase( Node lit, bool req );
   /** do instantiation specified by m */
-  bool addInstantiation( Node f, InstMatch& m, bool mkRep = true, bool modEq = false, bool modInst = false, bool doVts = false );
+  bool addInstantiation( Node q, InstMatch& m, bool mkRep = true, bool modEq = false, bool modInst = false, bool doVts = false );
   /** add instantiation */
-  bool addInstantiation( Node f, std::vector< Node >& terms, bool mkRep = true, bool modEq = false, bool modInst = false, bool doVts = false );
+  bool addInstantiation( Node q, std::vector< Node >& terms, bool mkRep = true, bool modEq = false, bool modInst = false, bool doVts = false );
   /** split on node n */
   bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true );
   /** add split equality */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index d34f0cd12..48f8b257c 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -92,7 +92,9 @@ void TheoryEngine::finishInit() {
 }
 
 void TheoryEngine::eqNotifyNewClass(TNode t){
-  d_quantEngine->addTermToDatabase( t );
+  if( d_logicInfo.isQuantified() ){
+    d_quantEngine->addTermToDatabase( t );
+  }
 }
 
 void TheoryEngine::eqNotifyPreMerge(TNode t1, TNode t2){
diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am
index 501e7b2c6..649cbee90 100644
--- a/test/regress/regress0/push-pop/Makefile.am
+++ b/test/regress/regress0/push-pop/Makefile.am
@@ -41,7 +41,8 @@ BUG_TESTS = \
   quant-fun-proc-unmacro.smt2 \
   quant-fun-proc-unfd.smt2 \
   bug654-dd.smt2 \
-  bug-fmf-fun-skolem.smt2
+  bug-fmf-fun-skolem.smt2 \
+  bug674.smt2
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 
diff --git a/test/regress/regress0/push-pop/bug674.smt2 b/test/regress/regress0/push-pop/bug674.smt2
new file mode 100644
index 000000000..967681ec3
--- /dev/null
+++ b/test/regress/regress0/push-pop/bug674.smt2
@@ -0,0 +1,28 @@
+; COMMAND-LINE: --quant-ind --incremental --rewrite-divk
+(set-logic ALL_SUPPORTED)
+(declare-datatypes () ((Lst (cons (head Int) (tail Lst)) (nil))))
+(define-fun-rec app ((l1 Lst) (l2 Lst)) Lst (ite (is-nil l1) l2 (cons (head l1) (app (tail l1) l2))))
+(define-fun-rec rev ((l Lst)) Lst (ite (is-nil l) nil (app (rev (tail l)) (cons (head l) nil))))
+; EXPECT: unsat
+(push 1)
+(assert (not (=> true (and (forall (($l1$0 Lst) ($l2$0 Lst) ($l3$0 Lst)) (= (app $l1$0 (app $l2$0 $l3$0)) (app (app $l1$0 $l2$0) $l3$0)))))))
+(check-sat)
+(pop 1)
+
+(assert (forall (($l1$0 Lst) ($l2$0 Lst) ($l3$0 Lst)) (= (app $l1$0 (app $l2$0 $l3$0)) (app (app $l1$0 $l2$0) $l3$0))))
+
+; EXPECT: unsat
+(push 1)
+(assert (not (=> true (and (forall (($l1$0 Lst) ($l2$0 Lst)) (= (rev (app $l1$0 $l2$0)) (app (rev $l2$0) (rev $l1$0))))))))
+(check-sat)
+(pop 1)
+
+(assert (forall (($l1$0 Lst) ($l2$0 Lst)) (= (rev (app $l1$0 $l2$0)) (app (rev $l2$0) (rev $l1$0)))))
+
+; EXPECT: unsat
+(push 1)
+(assert (not (=> true (and (forall (($l1$0 Lst)) (= (rev (rev $l1$0)) $l1$0))))))
+(check-sat)
+(pop 1)
+
+