From 4ff2946e1338d3f500b7e6bababee50fadad68d6 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 12 Apr 2016 10:13:45 -0500
Subject: [PATCH] Optimizations for QCF to check relevant domain of variable
 argument positions eagerly, global ordering mechanism for quantified formulas
 within check. Refactoring of term database.

---
 src/options/options_handler.cpp               |   2 -
 src/options/quantifiers_modes.h               |   2 -
 src/theory/quantifiers/anti_skolem.cpp        |   2 +-
 .../quantifiers/candidate_generator.cpp       |   1 -
 .../quantifiers/conjecture_generator.cpp      |  18 +-
 src/theory/quantifiers/conjecture_generator.h |   2 +-
 src/theory/quantifiers/first_order_model.cpp  |  89 +++++++-
 src/theory/quantifiers/first_order_model.h    |  16 +-
 src/theory/quantifiers/full_model_check.cpp   |   6 +-
 src/theory/quantifiers/inst_propagator.cpp    |   3 +
 src/theory/quantifiers/inst_strategy_cbqi.cpp |  34 +--
 .../quantifiers/inst_strategy_e_matching.cpp  |  15 +-
 .../quantifiers/instantiation_engine.cpp      |   6 +-
 src/theory/quantifiers/model_builder.cpp      |  14 +-
 src/theory/quantifiers/model_engine.cpp       |  51 +++--
 .../quantifiers/quant_conflict_find.cpp       | 201 ++++++++----------
 src/theory/quantifiers/quant_conflict_find.h  |  14 +-
 src/theory/quantifiers/relevant_domain.cpp    |   2 +-
 src/theory/quantifiers/rewrite_engine.cpp     |   2 +-
 src/theory/quantifiers/term_database.cpp      |  64 ++++--
 src/theory/quantifiers/term_database.h        |  50 +++--
 src/theory/quantifiers_engine.cpp             |  26 ++-
 src/theory/quantifiers_engine.h               |   6 +
 test/regress/regress0/quantifiers/Makefile.am |   3 +-
 .../regress0/quantifiers/qcf-rel-dom-opt.smt2 |  45 ++++
 25 files changed, 432 insertions(+), 242 deletions(-)
 create mode 100644 test/regress/regress0/quantifiers/qcf-rel-dom-opt.smt2

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index d08f5f533..a2809bd67 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -576,8 +576,6 @@ theory::quantifiers::QcfMode OptionsHandler::stringToQcfMode(std::string option,
     return theory::quantifiers::QCF_PROP_EQ;
   } else if(optarg == "partial") {
     return theory::quantifiers::QCF_PARTIAL;
-  } else if(optarg == "mc" ) {
-    return theory::quantifiers::QCF_MC;
   } else if(optarg ==  "help") {
     puts(s_qcfModeHelp.c_str());
     exit(1);
diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index a437cfc97..5749da972 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -83,8 +83,6 @@ enum QcfMode {
   QCF_PROP_EQ,
   /** use qcf for conflicts, propagations and heuristic instantiations */
   QCF_PARTIAL,
-  /** use qcf for model checking */
-  QCF_MC,
 };
 
 enum UserPatMode {
diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp
index ed000427f..c8d18aced 100644
--- a/src/theory/quantifiers/anti_skolem.cpp
+++ b/src/theory/quantifiers/anti_skolem.cpp
@@ -82,7 +82,7 @@ QuantAntiSkolem::QuantAntiSkolem( QuantifiersEngine * qe ) : QuantifiersModule(
 void QuantAntiSkolem::check( Theory::Effort e, unsigned quant_e ) {
   if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
     d_sqtc.clear();
-    for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+    for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
       Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
       if( d_quant_processed.find( q )==d_quant_processed.end() ){
         d_quant_processed[q] = true;
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 38d8c0d81..43f5ee2fd 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -298,7 +298,6 @@ Node CandidateGeneratorQEAll::getNextCandidate() {
     }
   }
   if( d_firstTime ){
-    Assert( d_qe->getTermDatabase()->d_type_map[d_match_pattern_type].empty() );
     //must return something
     d_firstTime = false;
     return d_qe->getTermDatabase()->getModelBasisTerm( d_match_pattern_type );
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index f8a9eefcb..27bbb0f5f 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -34,7 +34,7 @@ struct sortConjectureScore {
 };
 
 
-void OpArgIndex::addTerm( ConjectureGenerator * s, TNode n, unsigned index ){
+void OpArgIndex::addTerm( std::vector< TNode >& terms, TNode n, unsigned index ){
   if( index==n.getNumChildren() ){
     Assert( n.hasOperator() );
     if( std::find( d_ops.begin(), d_ops.end(), n.getOperator() )==d_ops.end() ){
@@ -42,7 +42,7 @@ void OpArgIndex::addTerm( ConjectureGenerator * s, TNode n, unsigned index ){
       d_op_terms.push_back( n );
     }
   }else{
-    d_child[s->getTermDatabase()->d_arg_reps[n][index]].addTerm( s, n, index+1 );
+    d_child[terms[index]].addTerm( terms, n, index+1 );
   }
 }
 
@@ -369,7 +369,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
           TNode n = (*ieqc_i);
           if( getTermDatabase()->hasTermCurrent( n ) ){
             if( isHandledTerm( n ) ){
-              d_op_arg_index[r].addTerm( this, n );
+              d_op_arg_index[r].addTerm( getTermDatabase()->d_arg_reps[n], n );
             }
           }
           ++ieqc_i;
@@ -489,7 +489,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
       d_thm_index.clear();
       std::vector< Node > provenConj;
       quantifiers::FirstOrderModel* m = d_quantEngine->getModel();
-      for( int i=0; i<m->getNumAssertedQuantifiers(); i++ ){
+      for( unsigned i=0; i<m->getNumAssertedQuantifiers(); i++ ){
         Node q = m->getAssertedQuantifier( i );
         Trace("thm-db-debug") << "Is " << q << " a relevant theorem?" << std::endl;
         Node conjEq;
@@ -1569,10 +1569,12 @@ bool TermGenerator::getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode,
         if( d_match_status_child_num==0 ){
           //initial binding
           TNode f = s->getTgFunc( d_typ, d_status_num );
-          std::map< TNode, TermArgTrie >::iterator it = s->getTermDatabase()->d_func_map_eqc_trie[f].d_data.find( eqc );
-          if( it!=s->getTermDatabase()->d_func_map_eqc_trie[f].d_data.end() ){
-            d_match_children.push_back( it->second.d_data.begin() );
-            d_match_children_end.push_back( it->second.d_data.end() );
+          //std::map< TNode, TermArgTrie >::iterator it = s->getTermDatabase()->d_func_map_eqc_trie[f].d_data.find( eqc );
+          Assert( !eqc.isNull() );
+          TermArgTrie * tat = s->getTermDatabase()->getTermArgTrie( eqc, f );
+          if( tat ){
+            d_match_children.push_back( tat->d_data.begin() );
+            d_match_children_end.push_back( tat->d_data.end() );
           }else{
             d_match_status++;
             d_match_status_child_num--;
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index b6e17e7a1..c89d0f2ee 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -39,7 +39,7 @@ public:
   std::map< TNode, OpArgIndex > d_child;
   std::vector< TNode > d_ops;
   std::vector< TNode > d_op_terms;
-  void addTerm( ConjectureGenerator * s, TNode n, unsigned index = 0 );
+  void addTerm( std::vector< TNode >& terms, TNode n, unsigned index = 0 );
   Node getGroundTerm( ConjectureGenerator * s, std::vector< TNode >& args );
   void getGroundTerms( ConjectureGenerator * s, std::vector< TNode >& terms );
 };
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 59bd10493..a833f48d2 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -30,10 +30,23 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 using namespace CVC4::theory::quantifiers::fmcheck;
 
+struct sortQuantifierRelevance {
+  FirstOrderModel * d_fm;
+  bool operator() (Node i, Node j) {
+    int wi = d_fm->getRelevanceValue( i );
+    int wj = d_fm->getRelevanceValue( j );
+    if( wi==wj ){
+      return i<j;
+    }else{
+      return wi<wj;
+    }
+  }
+};
+
 FirstOrderModel::FirstOrderModel(QuantifiersEngine * qe, context::Context* c, std::string name ) :
 TheoryModel( c, name, true ),
 d_qe( qe ), d_forall_asserts( c ), d_isModelSet( c, false ){
-
+  d_rlv_count = 0;
 }
 
 void FirstOrderModel::assertQuantifier( Node n ){
@@ -44,6 +57,19 @@ void FirstOrderModel::assertQuantifier( Node n ){
   }
 }
 
+unsigned FirstOrderModel::getNumAssertedQuantifiers() { 
+  return d_forall_asserts.size(); 
+}
+
+Node FirstOrderModel::getAssertedQuantifier( unsigned i, bool ordered ) { 
+  if( !ordered || d_forall_rlv_assert.empty() ){
+    return d_forall_asserts[i]; 
+  }else{
+    Assert( d_forall_rlv_assert.size()==d_forall_asserts.size() );
+    return d_forall_rlv_assert[i];
+  }
+}
+
 Node FirstOrderModel::getCurrentModelValue( Node n, bool partial ) {
   std::vector< Node > children;
   if( n.getNumChildren()>0 ){
@@ -74,11 +100,11 @@ void FirstOrderModel::initialize() {
   processInitialize( true );
   //this is called after representatives have been chosen and the equality engine has been built
   //for each quantifier, collect all operators we care about
-  for( int i=0; i<getNumAssertedQuantifiers(); i++ ){
+  for( unsigned i=0; i<getNumAssertedQuantifiers(); i++ ){
     Node f = getAssertedQuantifier( i );
     if( d_quant_var_id.find( f )==d_quant_var_id.end() ){
-      for(unsigned i=0; i<f[0].getNumChildren(); i++){
-        d_quant_var_id[f][f[0][i]] = i;
+      for(unsigned j=0; j<f[0].getNumChildren(); j++){
+        d_quant_var_id[f][f[0][j]] = j;
       }
     }
     processInitializeQuantifier( f );
@@ -120,6 +146,61 @@ bool FirstOrderModel::checkNeeded() {
 
 void FirstOrderModel::reset_round() {
   d_quant_active.clear();
+  
+  //order the quantified formulas
+  if( !d_forall_rlv_vec.empty() ){
+    Trace("fm-relevant") << "Build sorted relevant list..." << std::endl;
+    d_forall_rlv_assert.clear();
+    Trace("fm-relevant-debug") << "Mark asserted quantified formulas..." << std::endl;
+    std::map< Node, bool > qassert;
+    for( unsigned i=0; i<d_forall_asserts.size(); i++ ){
+      qassert[d_forall_asserts[i]] = true;
+    }
+    Trace("fm-relevant-debug") << "Sort the relevant quantified formulas..." << std::endl;
+    sortQuantifierRelevance sqr;
+    sqr.d_fm = this;
+    std::sort( d_forall_rlv_vec.begin(), d_forall_rlv_vec.end(), sqr );
+    Trace("fm-relevant-debug") << "Add relevant asserted formulas..." << std::endl;
+    for( int i=(int)(d_forall_rlv_vec.size()-1); i>=0; i-- ){
+      Node q = d_forall_rlv_vec[i];
+      if( qassert.find( q )!=qassert.end() ){
+        Trace("fm-relevant") << "   " << d_forall_rlv[q] << " : " << q << std::endl;
+        d_forall_rlv_assert.push_back( q );
+      }
+    }
+    Trace("fm-relevant-debug") << "Add remaining asserted formulas..." << std::endl;
+    for( unsigned i=0; i<d_forall_asserts.size(); i++ ){
+      Node q = d_forall_asserts[i];
+      if( std::find( d_forall_rlv_assert.begin(), d_forall_rlv_assert.end(), q )==d_forall_rlv_assert.end() ){
+        d_forall_rlv_assert.push_back( q );
+      }else{
+        Trace("fm-relevant-debug") << "...already included " << q << std::endl;
+      }
+    }
+    Trace("fm-relevant-debug") << "Sizes : " << d_forall_rlv_assert.size() << " " << d_forall_asserts.size() << std::endl;
+    Assert( d_forall_rlv_assert.size()==d_forall_asserts.size() );
+  }
+}
+
+void FirstOrderModel::markRelevant( Node q ) {
+  if( q!=d_last_forall_rlv ){
+    Trace("fm-relevant") << "Mark relevant : " << q << std::endl;
+    if( std::find( d_forall_rlv_vec.begin(), d_forall_rlv_vec.end(), q )==d_forall_rlv_vec.end() ){
+      d_forall_rlv_vec.push_back( q );
+    }
+    d_forall_rlv[ q ] = d_rlv_count;
+    d_rlv_count++;
+    d_last_forall_rlv = q;
+  }
+}
+
+int FirstOrderModel::getRelevanceValue( Node q ) {
+  std::map< Node, unsigned >::iterator it = d_forall_rlv.find( q );
+  if( it==d_forall_rlv.end() ){
+    return -1;
+  }else{
+    return it->second;
+  }
 }
 
 //bool FirstOrderModel::isQuantifierAsserted( TNode q ) {
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 4ab1dd1c3..cbe83cfa5 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -49,6 +49,12 @@ protected:
   QuantifiersEngine * d_qe;
   /** list of quantifiers asserted in the current context */
   context::CDList<Node> d_forall_asserts;
+  /** quantified formulas marked as relevant */
+  unsigned d_rlv_count;
+  std::map< Node, unsigned > d_forall_rlv;
+  std::vector< Node > d_forall_rlv_vec;
+  Node d_last_forall_rlv;
+  std::vector< Node > d_forall_rlv_assert;
   /** is model set */
   context::CDO< bool > d_isModelSet;
   /** get variable id */
@@ -59,9 +65,9 @@ public: //for Theory Quantifiers:
   /** assert quantifier */
   void assertQuantifier( Node n );
   /** get number of asserted quantifiers */
-  int getNumAssertedQuantifiers() { return (int)d_forall_asserts.size(); }
+  unsigned getNumAssertedQuantifiers();
   /** get asserted quantifier */
-  Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; }
+  Node getAssertedQuantifier( unsigned i, bool ordered = false );
   /** initialize model for term */
   void initializeModelForTerm( Node n, std::map< Node, bool >& visited );
   virtual void processInitializeModelForTerm( Node n ) = 0;
@@ -96,8 +102,10 @@ private:
 public:
   /** reset round */
   void reset_round();
-  /** is quantified formula asserted */
-  //bool isQuantifierAsserted( TNode q );
+  /** mark quantified formula relevant */
+  void markRelevant( Node q );
+  /** get relevance value */
+  int getRelevanceValue( Node q );
   /** set quantified formula active/inactive 
    * a quantified formula may be set inactive if for instance:
    *   - it is entailed by other quantified formulas
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 0276cf7ab..6b06b9e5c 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -350,11 +350,11 @@ void FullModelChecker::preProcessBuildModel(TheoryModel* m, bool fullModel) {
     }
     //do not have to introduce terms for sorts of domains of quantified formulas if we are allowed to assume empty sorts
     if( !options::fmfEmptySorts() ){
-      for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+      for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
         Node q = fm->getAssertedQuantifier( i );
         //make sure all types are set
-        for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-          preInitializeType( fm, q[0][i].getType() );
+        for( unsigned j=0; j<q[0].getNumChildren(); j++ ){
+          preInitializeType( fm, q[0][j].getType() );
         }
       }
     }
diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp
index c6f4affc5..d4be58636 100644
--- a/src/theory/quantifiers/inst_propagator.cpp
+++ b/src/theory/quantifiers/inst_propagator.cpp
@@ -723,6 +723,9 @@ void InstPropagator::conflict( std::vector< Node >& exp ) {
       }else{
         Trace("qip-prop-debug") << it->first << " ";
       }
+    }else{
+      //mark the quantified formula as relevant
+      d_qe->markRelevant( it->second.d_q );
     }
   }
   Trace("qip-prop-debug") << std::endl;
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index cc9b56a7c..fe4867b4e 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -46,7 +46,7 @@ bool InstStrategyCbqi::needsCheck( Theory::Effort e ) {
 }
 
 unsigned InstStrategyCbqi::needsModel( Theory::Effort e ) {
-  for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+  for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
     Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
     if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
       return QuantifiersEngine::QEFFORT_STANDARD;
@@ -59,7 +59,7 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) {
   d_cbqi_set_quant_inactive = false;
   d_incomplete_check = false;
   //check if any cbqi lemma has not been added yet
-  for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+  for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
     Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
     //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
     if( doCbqi( q ) ){
@@ -115,7 +115,7 @@ void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) {
     }
     unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
     for( int ee=0; ee<=1; ee++ ){
-      for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+      for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
         Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
         if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
           process( q, e, ee );
@@ -236,7 +236,7 @@ bool InstStrategyCbqi::doCbqi( Node q ){
 
 Node InstStrategyCbqi::getNextDecisionRequest(){
   // all counterexample literals that are not asserted
-  for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+  for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
     Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
     if( hasAddedCbqiLemma( q ) ){
       Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q );
@@ -316,8 +316,10 @@ void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort
     }
   }
   //print debug
-  Debug("quant-arith-debug") << std::endl;
-  debugPrint( "quant-arith-debug" );
+  if( Debug.isOn("quant-arith-debug") ){
+    Debug("quant-arith-debug") << std::endl;
+    debugPrint( "quant-arith-debug" );
+  }
   d_counter++;
 }
 
@@ -355,10 +357,10 @@ void InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){
       bool m_point_valid = true;
       int lem = 0;
       //scan over all instantiation rows
-      for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
+      for( unsigned i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
         Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
         Debug("quant-arith-simplex") << "InstStrategySimplex check " << ic << ", rows = " << d_instRows[ic].size() << std::endl;
-        for( int j=0; j<(int)d_instRows[ic].size(); j++ ){
+        for( unsigned j=0; j<d_instRows[ic].size(); j++ ){
           ArithVar x = d_instRows[ic][j];
           if( !d_ceTableaux[ic][x].empty() ){
             if( Debug.isOn("quant-arith-simplex") ){
@@ -474,25 +476,25 @@ void InstStrategySimplex::debugPrint( const char* c ){
   }
   Debug(c) << std::endl;
 
-  for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+  for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
     Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
     Debug(c) << f << std::endl;
     Debug(c) << "   Inst constants: ";
-    for( int i=0; i<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
-      if( i>0 ){
+    for( unsigned j=0; j<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
+      if( j>0 ){
         Debug( c ) << ", ";
       }
       Debug( c ) << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
     }
     Debug(c) << std::endl;
-    for( int j=0; j<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){
+    for( unsigned j=0; j<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){
       Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );
       Debug(c) << "   Instantiation rows for " << ic << " : ";
-      for( int i=0; i<(int)d_instRows[ic].size(); i++ ){
-        if( i>0 ){
+      for( unsigned k=0; k<d_instRows[ic].size(); k++ ){
+        if( k>0 ){
           Debug(c) << ", ";
         }
-        Debug(c) << d_instRows[ic][i];
+        Debug(c) << d_instRows[ic][k];
       }
       Debug(c) << std::endl;
     }
@@ -699,7 +701,7 @@ void InstStrategyCegqi::registerCounterexampleLemma( Node q, Node lem ) {
   //must register with the instantiator
   //must explicitly remove ITEs so that we record dependencies
   std::vector< Node > ce_vars;
-  for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( q ); i++ ){
+  for( unsigned i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( q ); i++ ){
     ce_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i ) );
   }
   std::vector< Node > lems;
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 6d6991476..bb514f41b 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -573,8 +573,8 @@ void FullSaturation::check( Theory::Effort e, unsigned quant_e ) {
       Trace("fs-engine") << "---Full Saturation Round, effort = " << e << "---" << std::endl;
     }
     int addedLemmas = 0;
-    for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
-      Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+    for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+      Node q = d_quantEngine->getModel()->getAssertedQuantifier( i, true );
       if( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
         if( process( q, fullEffort ) ){
           //added lemma
@@ -627,7 +627,7 @@ bool FullSaturation::process( Node f, bool fullEffort ){
         if( r==0 ){
           ts = rd->getRDomain( f, i )->d_terms.size();
         }else{
-          ts = d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()].size();
+          ts = d_quantEngine->getTermDatabase()->getNumTypeGroundTerms( f[0][i].getType() );
         }
         max_zero.push_back( fullEffort && ts==0 );
         ts = ( fullEffort && ts==0 ) ? 1 : ts;
@@ -643,6 +643,11 @@ bool FullSaturation::process( Node f, bool fullEffort ){
         }
       }
       if( !has_zero ){
+        std::vector< TypeNode > ftypes;
+        for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
+          ftypes.push_back( f[0][i].getType() );
+        }
+      
         Trace("inst-alg-rd") << "Will do " << final_max_i << " stages of instantiation." << std::endl;
         unsigned max_i = 0;
         bool success;
@@ -660,7 +665,7 @@ bool FullSaturation::process( Node f, bool fullEffort ){
                 if( options::cbqi() && r==1 && !max_zero[index] ){
                   //skip inst constant nodes
                   while( nv<maxs[index] && nv<=max_i &&
-                          quantifiers::TermDb::hasInstConstAttr( d_quantEngine->getTermDatabase()->d_type_map[f[0][index].getType()][nv] ) ){
+                          quantifiers::TermDb::hasInstConstAttr( d_quantEngine->getTermDatabase()->getTypeGroundTerm( ftypes[index], nv ) ) ){
                     nv++;
                   }
                 }
@@ -689,7 +694,7 @@ bool FullSaturation::process( Node f, bool fullEffort ){
                 }else if( r==0 ){
                   terms.push_back( rd->getRDomain( f, i )->d_terms[childIndex[i]] );
                 }else{
-                  terms.push_back( d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()][childIndex[i]] );
+                  terms.push_back( d_quantEngine->getTermDatabase()->getTypeGroundTerm( ftypes[i], childIndex[i] ) );
                 }
               }
               if( d_quantEngine->addInstantiation( f, terms, false ) ){
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index b59734720..955dc5d86 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -123,8 +123,8 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){
     //collect all active quantified formulas belonging to this
     bool quantActive = false;
     d_quants.clear();
-    for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
-      Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+    for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+      Node q = d_quantEngine->getModel()->getAssertedQuantifier( i, true );
       if( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
         quantActive = true;
         d_quants.push_back( q );
@@ -137,7 +137,7 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){
       doInstantiationRound( e );
       if( d_quantEngine->inConflict() ){
         Assert( d_quantEngine->getNumLemmasWaiting()>lastWaiting );
-        Trace("inst-engine") << "Conflict, size = " << d_quantEngine->getNumLemmasWaiting();
+        Trace("inst-engine") << "Conflict = " << d_quantEngine->getNumLemmasWaiting() << " / " << d_quantEngine->getNumLemmasAddedThisRound();
         if( lastWaiting>0 ){
           Trace("inst-engine") << " (prev " << lastWaiting << ")";
         }
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index bdb416b6b..b0ca43cfe 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -54,10 +54,10 @@ void QModelBuilder::debugModel( FirstOrderModel* fm ){
     Trace("quant-check-model") << "Testing quantifier instantiations..." << std::endl;
     int tests = 0;
     int bad = 0;
-    for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+    for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
       Node f = fm->getAssertedQuantifier( i );
       std::vector< Node > vars;
-      for( int j=0; j<(int)f[0].getNumChildren(); j++ ){
+      for( unsigned j=0; j<f[0].getNumChildren(); j++ ){
         vars.push_back( f[0][j] );
       }
       RepSetIterator riter( d_qe, &(fm->d_rep_set) );
@@ -65,8 +65,8 @@ void QModelBuilder::debugModel( FirstOrderModel* fm ){
         while( !riter.isFinished() ){
           tests++;
           std::vector< Node > terms;
-          for( int i=0; i<riter.getNumTerms(); i++ ){
-            terms.push_back( riter.getTerm( i ) );
+          for( int k=0; k<riter.getNumTerms(); k++ ){
+            terms.push_back( riter.getTerm( k ) );
           }
           Node n = d_qe->getInstantiation( f, vars, terms );
           Node val = fm->getValue( n );
@@ -149,7 +149,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
     if( optUseModel() ){
       Trace("model-engine-debug") << "Initializing " << fm->getNumAssertedQuantifiers() << " quantifiers..." << std::endl;
       //check if any quantifiers are un-initialized
-      for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+      for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
         Node f = fm->getAssertedQuantifier( i );
         if( isQuantifierActive( f ) ){
           int lems = initializeQuantifier( f, f );
@@ -173,7 +173,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
         Trace("model-engine-debug") << "Analyzing quantifiers..." << std::endl;
         d_quant_sat.clear();
         d_uf_prefs.clear();
-        for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+        for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
           Node f = fm->getAssertedQuantifier( i );
           if( isQuantifierActive( f ) ){
             analyzeQuantifier( fm, f );
@@ -190,7 +190,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
           d_numQuantNoSelForm = 0;
           //now, see if we know that any exceptions via InstGen exist
           Trace("model-engine-debug") << "Perform InstGen techniques for quantifiers..." << std::endl;
-          for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+          for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
             Node f = fm->getAssertedQuantifier( i );
             if( isQuantifierActive( f ) ){
               int lems = doInstGen( fm, f );
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index a7e272be0..f94e947e5 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -83,8 +83,10 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){
       Trace("model-engine-debug") << "Check model..." << std::endl;
       d_incomplete_check = false;
       //print debug
-      Trace("fmf-model-complete") << std::endl;
-      debugPrint("fmf-model-complete");
+      if( Trace.isOn("fmf-model-complete") ){
+        Trace("fmf-model-complete") << std::endl;
+        debugPrint("fmf-model-complete");
+      }
       //successfully built an acceptable model, now check it
       addedLemmas += checkModel();
     }else{
@@ -99,8 +101,10 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){
     if( addedLemmas==0 ){
       Trace("model-engine-debug") << "No lemmas added, incomplete = " << d_incomplete_check << std::endl;
       //CVC4 will answer SAT or unknown
-      Trace("fmf-consistent") << std::endl;
-      debugPrint("fmf-consistent");
+      if( Trace.isOn("fmf-consistent") ){
+        Trace("fmf-consistent") << std::endl;
+        debugPrint("fmf-consistent");
+      }
     }
   }
 }
@@ -177,35 +181,30 @@ int ModelEngine::checkModel(){
   d_addedLemmas = 0;
   d_totalLemmas = 0;
   //for statistics
-  for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
-    Node f = fm->getAssertedQuantifier( i );
-    int totalInst = 1;
-    for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-      TypeNode tn = f[0][i].getType();
-      if( fm->d_rep_set.hasType( tn ) ){
-        totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size();
+  if( Trace.isOn("model-engine") ){
+    for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+      Node f = fm->getAssertedQuantifier( i );
+      int totalInst = 1;
+      for( unsigned j=0; j<f[0].getNumChildren(); j++ ){
+        TypeNode tn = f[0][j].getType();
+        if( fm->d_rep_set.hasType( tn ) ){
+          totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size();
+        }
       }
+      d_totalLemmas += totalInst;
     }
-    d_totalLemmas += totalInst;
   }
 
   Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
   // FMC uses two sub-effort levels
   int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : ( options::mbqiMode()==MBQI_TRUST ? 0 : 1 );
   for( int e=0; e<e_max; e++) {
-    for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
-      Node f = fm->getAssertedQuantifier( i );
+    for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+      Node f = fm->getAssertedQuantifier( i, true );
       Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << f << ", effort = " << e << "..." << std::endl;
       //determine if we should check this quantifier
       if( considerQuantifiedFormula( f ) ){
         exhaustiveInstantiate( f, e );
-        if( Trace.isOn("model-engine-warn") ){
-          if( d_addedLemmas>10000 ){
-            Debug("fmf-exit") << std::endl;
-            debugPrint("fmf-exit");
-            exit( 0 );
-          }
-        }
         if( d_quantEngine->inConflict() || ( optOneQuantPerRound() && d_addedLemmas>0 ) ){
           break;
         }
@@ -222,7 +221,7 @@ int ModelEngine::checkModel(){
 
   //print debug information
   if( d_quantEngine->inConflict() ){
-    Trace("model-engine") << "Conflict, size = " << d_quantEngine->getNumLemmasWaiting() << std::endl;
+    Trace("model-engine") << "Conflict = " << d_quantEngine->getNumLemmasWaiting() << " / " << d_quantEngine->getNumLemmasAddedThisRound() << std::endl;
   }else{
     Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / ";
     Trace("model-engine") << d_totalLemmas << std::endl;
@@ -320,15 +319,15 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
 
 void ModelEngine::debugPrint( const char* c ){
   Trace( c ) << "Quantifiers: " << std::endl;
-  for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
-    Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
+  for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+    Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
     Trace( c ) << "   ";
-    if( !d_quantEngine->getModelBuilder()->isQuantifierActive( f ) ){
+    if( !d_quantEngine->getModelBuilder()->isQuantifierActive( q ) ){
       Trace( c ) << "*Inactive* ";
     }else{
       Trace( c ) << "           ";
     }
-    Trace( c ) << f << std::endl;
+    Trace( c ) << q << std::endl;
   }
   //d_quantEngine->getModel()->debugPrint( c );
 }
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index e5df41510..1cbfbd99b 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -22,6 +22,7 @@
 #include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/trigger.h"
+#include "theory/quantifiers/first_order_model.h"
 #include "theory/theory_engine.h"
 
 using namespace CVC4::kind;
@@ -46,7 +47,7 @@ QuantInfo::~QuantInfo() {
 }
 
 
-void QuantInfo::initialize( Node q, Node qn ) {
+void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) {
   d_q = q;
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
     d_match.push_back( TNode::null() );
@@ -107,6 +108,59 @@ void QuantInfo::initialize( Node q, Node qn ) {
     Trace("qcf-invalid") << "QCF invalid : body of formula cannot be processed." << std::endl;
   }
   Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl;
+  
+  if( d_mg->isValid() ){
+    //optimization : record variable argument positions for terms that must be matched
+    std::vector< TNode > vars;
+    //TODO: revisit this, makes QCF faster, but misses conflicts due to caring about paths that may not be relevant (starExec jobs 14136/14137)
+    //if( options::qcfSkipRd() ){
+    //  for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){
+    //    vars.push_back( d_vars[j] );
+    //  }
+    //}
+    //get all variables that are always relevant
+    std::map< TNode, bool > visited;
+    getPropagateVars( vars, q[1], false, visited );
+    for( unsigned j=0; j<vars.size(); j++ ){
+      Node v = vars[j];
+      TNode f = p->getTermDatabase()->getMatchOperator( v );
+      if( !f.isNull() ){
+        Trace("qcf-opt") << "Record variable argument positions in " << v << ", op=" << f << "..." << std::endl;
+        for( unsigned k=0; k<v.getNumChildren(); k++ ){
+          Node n = v[k];
+          std::map< TNode, int >::iterator itv = d_var_num.find( n );
+          if( itv!=d_var_num.end() ){
+            Trace("qcf-opt") << "  arg " << k << " is var #" << itv->second << std::endl;
+            if( std::find( d_var_rel_dom[itv->second][f].begin(), d_var_rel_dom[itv->second][f].end(), k )==d_var_rel_dom[itv->second][f].end() ){
+              d_var_rel_dom[itv->second][f].push_back( k );
+            }
+          }
+        }
+      }
+    }    
+  }
+}
+
+void QuantInfo::getPropagateVars( std::vector< TNode >& vars, TNode n, bool pol, std::map< TNode, bool >& visited ){
+  std::map< TNode, bool >::iterator itv = visited.find( n );
+  if( itv==visited.end() ){
+    visited[n] = true;
+    bool rec = true;
+    bool newPol = pol;
+    if( d_var_num.find( n )!=d_var_num.end() ){
+      Assert( std::find( vars.begin(), vars.end(), n )==vars.end() );
+      vars.push_back( n );
+    }else if( MatchGen::isHandledBoolConnective( n ) ){
+      Assert( n.getKind()!=IMPLIES );
+      QuantPhaseReq::getEntailPolarity( n, 0, true, pol, rec, newPol );
+    }
+    Trace("qcf-opt-debug") << "getPropagateVars " << n << ", pol = " << pol << ", rec = " << rec << std::endl;
+    if( rec ){
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        getPropagateVars( vars, n[i], pol, visited );
+      }
+    }
+  }
 }
 
 void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant ) {
@@ -327,7 +381,7 @@ int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, boo
         return 1;
       }else{
         //std::map< int, TNode >::iterator itm = d_match.find( v );
-
+        bool isGroundRep = false;
         if( vn!=-1 ){
           Debug("qcf-match-debug") << "  ...Variable bound to variable" << std::endl;
           //std::map< int, TNode >::iterator itmn = d_match.find( vn );
@@ -373,13 +427,14 @@ int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, boo
         }else{
           Debug("qcf-match-debug") << "  ...Variable bound to ground" << std::endl;
           if( d_match[v].isNull() ){
+            //isGroundRep = true;   ??
           }else{
             //compare ground values
             Debug("qcf-match-debug") << "  -> Ground value, compare " << d_match[v] << " "<< n << std::endl;
             return p->areMatchEqual( d_match[v], n ) ? 0 : -1;
           }
         }
-        if( setMatch( p, v, n ) ){
+        if( setMatch( p, v, n, isGroundRep ) ){
           Debug("qcf-match-debug") << "  -> success" << std::endl;
           return 1;
         }else{
@@ -445,8 +500,23 @@ bool QuantInfo::isConstrainedVar( int v ) {
   }
 }
 
-bool QuantInfo::setMatch( QuantConflictFind * p, int v, TNode n ) {
+bool QuantInfo::setMatch( QuantConflictFind * p, int v, TNode n, bool isGroundRep ) {
   if( getCurrentCanBeEqual( p, v, n ) ){
+    if( isGroundRep ){
+      //fail if n does not exist in the relevant domain of each of the argument positions
+      std::map< int, std::map< TNode, std::vector< unsigned > > >::iterator it = d_var_rel_dom.find( v );
+      if( it!=d_var_rel_dom.end() ){
+        for( std::map< TNode, std::vector< unsigned > >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
+          for( unsigned j=0; j<it2->second.size(); j++ ){
+            Debug("qcf-match-debug2") << n << " in relevant domain " <<  it2->second << "." << it2->second[j] << "?" << std::endl;
+            if( !p->getTermDatabase()->inRelevantDomain( it2->first, it2->second[j], n ) ){
+              Debug("qcf-match-debug") << "  -> fail, since " << n << " is not in relevant domain of " << it2->second << "." << it2->second[j] << std::endl;
+              return false;
+            }
+          }
+        }
+      }
+    }
     Debug("qcf-match-debug") << "-- bind : " << v << " -> " << n << ", checked " <<  d_curr_var_deq[v].size() << " disequalities" << std::endl;
     d_match[v] = n;
     return true;
@@ -566,7 +636,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
                 if( !z.isNull() ){
                   Trace("qcf-tconstraint-debug") << "...set " << d_vars[vn] << " = " << z << std::endl;
                   assigned.push_back( vn );
-                  if( !setMatch( p, vn, z ) ){
+                  if( !setMatch( p, vn, z, false ) ){
                     success = false;
                     break;
                   }
@@ -608,7 +678,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
             if( !sum.isNull() ){
               assigned.push_back( slv_v );
               Trace("qcf-tconstraint-debug") << "...set " << d_vars[slv_v] << " = " << sum << std::endl;
-              if( !setMatch( p, slv_v, sum ) ){
+              if( !setMatch( p, slv_v, sum, false ) ){
                 success = false;
               }
               p->d_tempCache.push_back( sum );
@@ -694,7 +764,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
                 int currIndex = d_una_eqc_count[d_una_index];
                 d_una_eqc_count[d_una_index]++;
                 Trace("qcf-check-unassign") << d_unassigned[d_una_index] << "->" << p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex] << std::endl;
-                if( setMatch( p, d_unassigned[d_una_index], p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex] ) ){
+                if( setMatch( p, d_unassigned[d_una_index], p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex], true ) ){
                   d_match_term[d_unassigned[d_una_index]] = TNode::null();
                   Trace("qcf-check-unassign") << "Succeeded match " << d_una_index << std::endl;
                   d_una_index++;
@@ -1125,7 +1195,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
     }else{
       //unassigned, set match to true/false
       d_qni_bound[0] = vn;
-      qi->setMatch( p, vn, d_tgt ? p->d_true : p->d_false );
+      qi->setMatch( p, vn, d_tgt ? p->d_true : p->d_false, false );
       d_child_counter = 0;
     }
     if( d_child_counter==0 ){
@@ -1365,17 +1435,6 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
           d_qni_bound_cons.clear();
         }
       }
-      /*
-      if( d_type==typ_var && p->d_effort==QuantConflictFind::effort_mc && !d_matched_basis ){
-        d_matched_basis = true;
-        Node f = getMatchOperator( d_n );
-        TNode mbo = p->getTermDatabase()->getModelBasisOpTerm( f );
-        if( qi->setMatch( p, d_qni_var_num[0], mbo ) ){
-          success = true;
-          d_qni_bound[0] = d_qni_var_num[0];
-        }
-      }
-      */
     }
     Debug("qcf-match") << "    ...finished matching for " << d_n << ", success = " << success << std::endl;
     d_wasSet = success;
@@ -1595,7 +1654,7 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
               if( it != d_qn[index]->d_data.end() ) {
                 d_qni.push_back( it );
                 //set the match
-                if( it->first.getType().isComparableTo( qi->d_var_types[repVar] ) && qi->setMatch( p, d_qni_bound[index], it->first ) ){
+                if( it->first.getType().isComparableTo( qi->d_var_types[repVar] ) && qi->setMatch( p, d_qni_bound[index], it->first, true ) ){
                   Debug("qcf-match-debug") << "       Binding variable" << std::endl;
                   if( d_qn.size()<d_qni_size ){
                     d_qn.push_back( &it->second );
@@ -1640,7 +1699,7 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
             d_qni[index]++;
             if( d_qni[index]!=d_qn[index]->d_data.end() ){
               success = true;
-              if( qi->setMatch( p, itb->second, d_qni[index]->first ) ){
+              if( qi->setMatch( p, itb->second, d_qni[index]->first, true ) ){
                 Debug("qcf-match-debug") << "       Bind next variable" << std::endl;
                 if( d_qn.size()<d_qni_size ){
                   d_qn.push_back( &d_qni[index]->second );
@@ -1756,8 +1815,7 @@ bool MatchGen::isHandled( TNode n ) {
 
 QuantConflictFind::QuantConflictFind( QuantifiersEngine * qe, context::Context* c ) :
 QuantifiersModule( qe ),
-d_conflict( c, false ),
-d_qassert( c ) {
+d_conflict( c, false ) {
   d_fid_count = 0;
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
@@ -1782,7 +1840,7 @@ void QuantConflictFind::registerQuantifier( Node q ) {
     Trace("qcf-qregister") << " : " << q << std::endl;
     //make QcfNode structure
     Trace("qcf-qregister") << "- Get relevant equality/disequality pairs, calculate flattening..." << std::endl;
-    d_qinfo[q].initialize( q, q[1] );
+    d_qinfo[q].initialize( this, q, q[1] );
 
     //debug print
     Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;
@@ -1797,7 +1855,7 @@ void QuantConflictFind::registerQuantifier( Node q ) {
         Trace("qcf-qregister") << std::endl;
       }
     }
-
+    
     Trace("qcf-qregister") << "Done registering quantifier." << std::endl;
   }
 }
@@ -1805,10 +1863,8 @@ void QuantConflictFind::registerQuantifier( Node q ) {
 short QuantConflictFind::getMaxQcfEffort() {
   if( options::qcfMode()==QCF_CONFLICT_ONLY ){
     return effort_conflict;
-  }else if( options::qcfMode()==QCF_PROP_EQ ){
+  }else if( options::qcfMode()==QCF_PROP_EQ || options::qcfMode()==QCF_PARTIAL ){
     return effort_prop_eq;
-  }else if( options::qcfMode()==QCF_MC ){
-    return effort_mc;
   }else{
     return 0;
   }
@@ -1833,16 +1889,13 @@ bool QuantConflictFind::areMatchDisequal( TNode n1, TNode n2 ) {
 //-------------------------------------------------- handling assertions / eqc
 
 void QuantConflictFind::assertNode( Node q ) {
+  /*
   if( d_quantEngine->hasOwnership( q, this ) ){
     Trace("qcf-proc") << "QCF : assertQuantifier : ";
     debugPrintQuant("qcf-proc", q);
     Trace("qcf-proc") << std::endl;
-    d_qassert.push_back( q );
-    //set the eqRegistries that this depends on to true
-    //for( std::map< EqRegistry *, bool >::iterator it = d_qinfo[q].d_rel_eqr.begin(); it != d_qinfo[q].d_rel_eqr.end(); ++it ){
-    //  it->first->d_active.set( true );
-    //}
   }
+  */
 }
 
 /** new node */
@@ -1904,28 +1957,12 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
 
       //determine order for quantified formulas
       std::vector< Node > qorder;
-      std::map< Node, bool > qassert;
-      //mark which are asserted
-      for( unsigned i=0; i<d_qassert.size(); i++ ){
-        qassert[d_qassert[i]] = true;
-      }
-      //add which ones are specified in the order
-      for( unsigned i=0; i<d_quant_order.size(); i++ ){
-        Node n = d_quant_order[i];
-        if( std::find( qorder.begin(), qorder.end(), n )==qorder.end() && qassert.find( n )!=qassert.end() ){
-          qorder.push_back( n );
-        }
-      }
-      d_quant_order.clear();
-      d_quant_order.insert( d_quant_order.begin(), qorder.begin(), qorder.end() );
-      //add remaining
-      for( unsigned i=0; i<d_qassert.size(); i++ ){
-        Node n = d_qassert[i];
-        if( std::find( qorder.begin(), qorder.end(), n )==qorder.end() ){
-          qorder.push_back( n );
+      for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+        Node q = d_quantEngine->getModel()->getAssertedQuantifier( i, true );
+        if( d_quantEngine->hasOwnership( q, this ) ){
+          qorder.push_back( q );
         }
       }
-
       if( Trace.isOn("qcf-debug") ){
         Trace("qcf-debug") << std::endl;
         debugPrint("qcf-debug");
@@ -1974,7 +2011,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
                       Trace("qcf-inst") << std::endl;
                       ++addedLemmas;
                       if( e==effort_conflict ){
-                        d_quant_order.insert( d_quant_order.begin(), q );
+                        d_quantEngine->markRelevant( q );
                         ++(d_statistics.d_conflict_inst);
                         if( options::qcfAllConflict() ){
                           isConflict = true;
@@ -1983,6 +2020,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
                         }
                         break;
                       }else if( e==effort_prop_eq ){
+                        d_quantEngine->markRelevant( q );
                         ++(d_statistics.d_prop_inst);
                       }
                     }else{
@@ -2040,60 +2078,24 @@ void QuantConflictFind::computeRelevantEqr() {
     //d_uf_terms.clear();
     //d_eqc_uf_terms.clear();
     d_eqcs.clear();
-    d_model_basis.clear();
     //d_arg_reps.clear();
     //double clSet = 0;
     //if( Trace.isOn("qcf-opt") ){
     //  clSet = double(clock())/double(CLOCKS_PER_SEC);
     //}
 
-    //long nTermst = 0;
-    //long nTerms = 0;
-    //long nEqc = 0;
-
-    //which nodes are irrelevant for disequality matches
-    std::map< TNode, bool > irrelevant_dnode;
     //now, store matches
     eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );
     while( !eqcs_i.isFinished() ){
-      //nEqc++;
       Node r = (*eqcs_i);
       if( getTermDatabase()->hasTermCurrent( r ) ){
         TypeNode rtn = r.getType();
-        if( options::qcfMode()==QCF_MC ){
-          std::map< TypeNode, std::vector< TNode > >::iterator itt = d_eqcs.find( rtn );
-          if( itt==d_eqcs.end() ){
-            Node mb = getTermDatabase()->getModelBasisTerm( rtn );
-            if( !getEqualityEngine()->hasTerm( mb ) ){
-              Trace("qcf-warn") << "WARNING: Model basis term does not exist!" << std::endl;
-              Assert( false );
-            }
-            Node mbr = getRepresentative( mb );
-            if( mbr!=r ){
-              d_eqcs[rtn].push_back( mbr );
-            }
-            d_eqcs[rtn].push_back( r );
-            d_model_basis[rtn] = mb;
-          }else{
-            itt->second.push_back( r );
-          }
-        }else{
-          if( !options::cbqi() || !TermDb::hasInstConstAttr( r ) ){
-            d_eqcs[rtn].push_back( r );
-          }
+        if( !options::cbqi() || !TermDb::hasInstConstAttr( r ) ){
+          d_eqcs[rtn].push_back( r );
         }
       }
       ++eqcs_i;
     }
-    /*
-    if( Trace.isOn("qcf-opt") ){
-      double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
-      Trace("qcf-opt") << "Compute rel eqc : " << std::endl;
-      Trace("qcf-opt") << "   " << nEqc << " equivalence classes. " << std::endl;
-      Trace("qcf-opt") << "   " << nTerms << " / " << nTermst << " terms." << std::endl;
-      Trace("qcf-opt") << "   Time : " << (clSet2-clSet) << std::endl;
-    }
-    */
   }
 }
 
@@ -2120,21 +2122,6 @@ void QuantConflictFind::debugPrint( const char * c ) {
       ++eqc_i;
     }
     Trace(c) << (pr ? " " : "" ) << "}" << std::endl;
-    /*
-    EqcInfo * eqcn = getEqcInfo( n, false );
-    if( eqcn ){
-      Trace(c) << "    DEQ : {";
-      pr = false;
-      for( NodeBoolMap::iterator it = eqcn->d_diseq.begin(); it != eqcn->d_diseq.end(); ++it ){
-        if( (*it).second ){
-          Trace(c) << (pr ? "," : "" ) << " " << (*it).first;
-          pr = true;
-        }
-      }
-      Trace(c) << (pr ? " " : "" ) << "}" << std::endl;
-    }
-    //}
-    */
     ++eqcs_i;
   }
 }
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 36fcaddf5..8b42b0916 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -114,6 +114,9 @@ private: //for completing match
   int d_unassigned_nvar;
   int d_una_index;
   std::vector< int > d_una_eqc_count;
+  //optimization: track which arguments variables appear under UF terms in
+  std::map< int, std::map< TNode, std::vector< unsigned > > > d_var_rel_dom;
+  void getPropagateVars( std::vector< TNode >& vars, TNode n, bool pol, std::map< TNode, bool >& visited );
 public:
   QuantInfo();
   ~QuantInfo();
@@ -138,7 +141,7 @@ public:
   bool containsVarMg(int i) const { return var_mg_find(i) != var_mg_end(); }
 
   bool matchGeneratorIsValid() const { return d_mg->isValid(); }
-  bool getNextMatch( QuantConflictFind * p) {
+  bool getNextMatch( QuantConflictFind * p ) {
     return d_mg->getNextMatch(p, this);
   }
 
@@ -146,7 +149,7 @@ public:
   void reset_round( QuantConflictFind * p );
 public:
   //initialize
-  void initialize( Node q, Node qn );
+  void initialize( QuantConflictFind * p, Node q, Node qn );
   //current constraints
   std::vector< TNode > d_match;
   std::vector< TNode > d_match_term;
@@ -158,7 +161,7 @@ public:
   bool getCurrentCanBeEqual( QuantConflictFind * p, int v, TNode n, bool chDiseq = false );
   int addConstraint( QuantConflictFind * p, int v, TNode n, bool polarity );
   int addConstraint( QuantConflictFind * p, int v, TNode n, int vn, bool polarity, bool doRemove );
-  bool setMatch( QuantConflictFind * p, int v, TNode n );
+  bool setMatch( QuantConflictFind * p, int v, TNode n, bool isGroundRep );
   bool isMatchSpurious( QuantConflictFind * p );
   bool isTConstraintSpurious( QuantConflictFind * p, std::vector< Node >& terms );
   bool entailmentTest( QuantConflictFind * p, Node lit, bool chEnt = true );
@@ -178,7 +181,6 @@ class QuantConflictFind : public QuantifiersModule
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
 private:
   context::CDO< bool > d_conflict;
-  std::vector< Node > d_quant_order;
   std::map< Kind, Node > d_zero;
   //for storing nodes created during t-constraint solving (prevents memory leaks)
   std::vector< Node > d_tempCache;
@@ -192,18 +194,14 @@ public:  //for ground terms
   Node d_false;
   TNode getZero( Kind k );
 private:
-  //currently asserted quantifiers
-  NodeList d_qassert;
   std::map< Node, QuantInfo > d_qinfo;
 private:  //for equivalence classes
   // type -> list(eqc)
   std::map< TypeNode, std::vector< TNode > > d_eqcs;
-  std::map< TypeNode, Node > d_model_basis;
 public:
   enum {
     effort_conflict,
     effort_prop_eq,
-    effort_mc,
   };
   short d_effort;
   void setEffort( int e ) { d_effort = e; }
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 9181677ee..b353fce2f 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -95,7 +95,7 @@ void RelevantDomain::compute(){
         it2->second->reset();
       }
     }
-    for( int i=0; i<d_model->getNumAssertedQuantifiers(); i++ ){
+    for( unsigned i=0; i<d_model->getNumAssertedQuantifiers(); i++ ){
       Node q = d_model->getAssertedQuantifier( i );
       Node icf = d_qe->getTermDatabase()->getInstConstantBody( q );
       Trace("rel-dom-debug") << "compute relevant domain for " << icf << std::endl;
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index 5bf8d8a8d..07b1462c6 100644
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -285,7 +285,7 @@ void RewriteEngine::registerQuantifier( Node f ) {
       //make the quantified formula
       d_qinfo_n[f] = NodeManager::currentNM()->mkNode( FORALL, qcfn_c );
       Trace("rr-register") << "  qcf formula is : " << d_qinfo_n[f] << std::endl;
-      d_qinfo[f].initialize( d_qinfo_n[f], d_qinfo_n[f][1] );
+      d_qinfo[f].initialize( qcf, d_qinfo_n[f], d_qinfo_n[f][1] );
     }
   }
 }
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 3d3646d7d..ef301c2cf 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -78,8 +78,8 @@ TNode TermArgTrie::addOrGetTerm( TNode n, std::vector< TNode >& reps, int argInd
 
 void TermArgTrie::debugPrint( const char * c, Node n, unsigned depth ) {
   for( std::map< TNode, TermArgTrie >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
-    for( unsigned i=0; i<depth; i++ ){ Debug(c) << "  "; }
-    Debug(c) << it->first << std::endl;
+    for( unsigned i=0; i<depth; i++ ){ Trace(c) << "  "; }
+    Trace(c) << it->first << std::endl;
     it->second.debugPrint( c, n, depth+1 );
   }
 }
@@ -111,6 +111,20 @@ Node TermDb::getGroundTerm( Node f, unsigned i ) {
   return d_op_map[f][i];
 }
 
+unsigned TermDb::getNumTypeGroundTerms( TypeNode tn ) {
+  std::map< TypeNode, std::vector< Node > >::iterator it = d_type_map.find( tn );
+  if( it!=d_type_map.end() ){
+    return it->second.size();
+  }else{
+    return 0;
+  }
+}
+
+Node TermDb::getTypeGroundTerm( TypeNode tn, unsigned i ) {
+  Assert( i<d_type_map[tn].size() );
+  return d_type_map[tn][i];
+}
+
 Node TermDb::getMatchOperator( Node n ) {
   //return n.getOperator();
   Kind k = n.getKind();
@@ -205,6 +219,21 @@ void TermDb::computeUfEqcTerms( TNode f ) {
   }
 }
 
+bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) {
+  Assert( d_quantEngine->getTheoryEngine()->getMasterEqualityEngine()->getRepresentative( r )==r );
+  std::map< Node, std::map< unsigned, std::vector< Node > > >::iterator it = d_func_map_rel_dom.find( f );
+  if( it != d_func_map_rel_dom.end() ){
+    std::map< unsigned, std::vector< Node > >::iterator it2 = it->second.find( i );
+    if( it2!=it->second.end() ){
+      return std::find( it2->second.begin(), it2->second.end(), r )!=it2->second.end();
+    }else{
+      return false;
+    }
+  }else{
+    return false;
+  }
+}
+
 //return a term n' equivalent to n
 //  maximal subterms of n' are representatives in the equality engine qy
 Node TermDb::evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy ) {
@@ -533,6 +562,7 @@ bool TermDb::reset( Theory::Effort effort ){
   d_arg_reps.clear();
   d_func_map_trie.clear();
   d_func_map_eqc_trie.clear();
+  d_func_map_rel_dom.clear();
   d_consistent_ee = true;
 
   eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
@@ -596,16 +626,18 @@ bool TermDb::reset( Theory::Effort effort ){
           }
           computeArgReps( n );
 
-          if( Trace.isOn("term-db-debug") ){
-            Trace("term-db-debug") << "Adding term " << n << " with arg reps : ";
-            for( unsigned i=0; i<d_arg_reps[n].size(); i++ ){
-              Trace("term-db-debug") << d_arg_reps[n][i] << " ";
-            }
-            Trace("term-db-debug") << std::endl;
-            if( ee->hasTerm( n ) ){
-              Trace("term-db-debug") << "  and value : " << ee->getRepresentative( n ) << std::endl;
+          Trace("term-db-debug") << "Adding term " << n << " with arg reps : ";
+          for( unsigned i=0; i<d_arg_reps[n].size(); i++ ){
+            Trace("term-db-debug") << d_arg_reps[n][i] << " ";
+            if( std::find( d_func_map_rel_dom[it->first][i].begin(), 
+                           d_func_map_rel_dom[it->first][i].end(), d_arg_reps[n][i] ) == d_func_map_rel_dom[it->first][i].end() ){
+              d_func_map_rel_dom[it->first][i].push_back( d_arg_reps[n][i] );
             }
           }
+          Trace("term-db-debug") << std::endl;
+          if( ee->hasTerm( n ) ){
+            Trace("term-db-debug") << "  and value : " << ee->getRepresentative( n ) << std::endl;
+          }
           Node at = d_func_map_trie[ it->first ].addOrGetTerm( n, d_arg_reps[n] );
           if( at!=n && ee->areEqual( at, n ) ){
             NoMatchAttribute nma;
@@ -650,12 +682,12 @@ bool TermDb::reset( Theory::Effort effort ){
   Trace("term-db-stats") << "TermDb: Reset" << std::endl;
   Trace("term-db-stats") << "Non-Congruent/Congruent/Non-Relevant = ";
   Trace("term-db-stats") << nonCongruentCount << " / " << congruentCount << " (" << alreadyCongruentCount << ") / " << nonRelevantCount << std::endl;
-  if( Debug.isOn("term-db") ){
-    Debug("term-db") << "functions : " << std::endl;
+  if( Trace.isOn("term-db-index") ){
+    Trace("term-db-index") << "functions : " << std::endl;
     for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){
       if( it->second.size()>0 ){
-        Debug("term-db") << "- " << it->first << std::endl;
-        d_func_map_trie[ it->first ].debugPrint("term-db", it->second[0]);
+        Trace("term-db-index") << "- " << it->first << std::endl;
+        d_func_map_trie[ it->first ].debugPrint("term-db-index", it->second[0]);
       }
     }
   }
@@ -929,10 +961,10 @@ Node TermDb::getInstantiationConstant( Node q, int i ) const {
 }
 
 /** get number of instantiation constants for q */
-int TermDb::getNumInstantiationConstants( Node q ) const {
+unsigned 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();
+    return it->second.size();
   }else{
     return 0;
   }
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 76bd623a8..a62b343a2 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -163,11 +163,21 @@ namespace fmcheck {
 }
 
 class TermDbSygus;
+class QuantConflictFind;
+class RelevantDomain;
+class ConjectureGenerator;
+class TermGenerator;
+class TermGenEnv;
 
 class TermDb : public QuantifiersUtil {
   friend class ::CVC4::theory::QuantifiersEngine;
+  //TODO: eliminate most of these
   friend class ::CVC4::theory::inst::Trigger;
   friend class ::CVC4::theory::quantifiers::fmcheck::FullModelChecker;
+  friend class ::CVC4::theory::quantifiers::QuantConflictFind;
+  friend class ::CVC4::theory::quantifiers::RelevantDomain;
+  friend class ::CVC4::theory::quantifiers::ConjectureGenerator;
+  friend class ::CVC4::theory::quantifiers::TermGenEnv;
   typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
 private:
   /** reference to the quantifiers engine */
@@ -180,12 +190,6 @@ private:
   std::map< Node, std::map< TypeNode, Node > > d_par_op_map;
   /** whether master equality engine is UF-inconsistent */
   bool d_consistent_ee;
-  /** set has term */
-  void setHasTerm( Node n );
-  /** evaluate term */
-  Node evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy );
-  TNode getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy );
-  bool isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy );
 public:
   TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe );
   ~TermDb(){}
@@ -195,7 +199,14 @@ public:
   /** constants */
   Node d_zero;
   Node d_one;
-
+public:
+  /** presolve (called once per user check-sat) */
+  void presolve();
+  /** reset (calculate which terms are active) */
+  bool reset( Theory::Effort effort );
+  /** identify */
+  std::string identify() const { return "TermDb"; }  
+private:
   /** 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 */
@@ -208,24 +219,29 @@ public:
   /** map from operators to trie */
   std::map< Node, TermArgTrie > d_func_map_trie;
   std::map< Node, TermArgTrie > d_func_map_eqc_trie;
+  /** mapping from operators to their representative relevant domains */
+  std::map< Node, std::map< unsigned, std::vector< Node > > > d_func_map_rel_dom;
   /** 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;
-
+  std::map< Node, Node > d_term_elig_eqc;  
+  /** set has term */
+  void setHasTerm( Node n );
+  /** evaluate term */
+  Node evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy );
+  TNode getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy );
+  bool isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy );
 public:
   /** ground terms for operator */
   unsigned getNumGroundTerms( Node f );
   /** get ground term for operator */
   Node getGroundTerm( Node f, unsigned i );
+  /** get num type terms */
+  unsigned getNumTypeGroundTerms( TypeNode tn );
+  /** get type ground term */
+  Node getTypeGroundTerm( TypeNode tn, 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) */
-  bool reset( Theory::Effort effort );
-  /** identify */
-  std::string identify() const { return "TermDb"; }
   /** get match operator */
   Node getMatchOperator( Node n );
   /** get term arg index */
@@ -238,6 +254,8 @@ public:
   void computeArgReps( TNode n );
   /** compute uf eqc terms */
   void computeUfEqcTerms( TNode f );
+  /** in relevant domain */
+  bool inRelevantDomain( TNode f, unsigned i, TNode r );
   /** evaluate a term under a substitution.  Return representative in EE if possible.
    * subsRep is whether subs contains only representatives
    */
@@ -297,7 +315,7 @@ public:
   /** 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;
+  unsigned getNumInstantiationConstants( Node q ) const;
   /** get the ce body q[e/x] */
   Node getInstConstantBody( Node q );
   /** get counterexample literal (for cbqi) */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 4b95c75ed..1008d7d49 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -88,6 +88,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
   d_tr_trie = new inst::TriggerTrie;
   d_curr_effort_level = QEFFORT_NONE;
   d_conflict = false;
+  d_num_added_lemmas_round = 0;
   d_hasAddedLemma = false;
   //don't add true lemma
   d_lemmas_produced_c[d_term_db->d_true] = true;
@@ -365,6 +366,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
   }
 
   d_conflict = false;
+  d_num_added_lemmas_round = 0;
   d_hasAddedLemma = false;
   bool setIncomplete = false;
   if( e==Theory::EFFORT_LAST_CALL ){
@@ -398,7 +400,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
       }
       Trace("quant-engine-debug") << "  Theory engine finished : " << !d_te->needCheck() << std::endl;
       Trace("quant-engine-debug") << "  Needs model effort : " << needsModelE << std::endl;
-      Trace("quant-engine-debug") << "Resetting all modules..." << std::endl;
     }
     if( Trace.isOn("quant-engine-ee-pre") ){
       Trace("quant-engine-ee-pre") << "Equality engine (pre-inference): " << std::endl;
@@ -410,6 +411,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
     }
 
     //reset utilities
+    Trace("quant-engine-debug") << "Resetting all utilities..." << std::endl;
     for( unsigned i=0; i<d_util.size(); i++ ){
       Trace("quant-engine-debug2") << "Reset " << d_util[i]->identify().c_str() << "..." << std::endl;
       if( !d_util[i]->reset( e ) ){
@@ -429,9 +431,11 @@ void QuantifiersEngine::check( Theory::Effort e ){
     }
 
     //reset the model
+    Trace("quant-engine-debug") << "Reset model..." << std::endl;
     d_model->reset_round();
 
     //reset the modules
+    Trace("quant-engine-debug") << "Resetting all modules..." << std::endl;
     for( unsigned i=0; i<d_modules.size(); i++ ){
       Trace("quant-engine-debug2") << "Reset " << d_modules[i]->identify().c_str() << std::endl;
       d_modules[i]->reset_round( e );
@@ -936,6 +940,7 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){
       d_lemmas_produced_c[ lem ] = true;
       d_lemmas_waiting.push_back( lem );
       Trace("inst-add-debug") << "Added lemma" << std::endl;
+      d_num_added_lemmas_round++;
       return true;
     }else{
       Trace("inst-add-debug") << "Duplicate." << std::endl;
@@ -944,6 +949,7 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){
   }else{
     //do not need to rewrite, will be rewritten after sending
     d_lemmas_waiting.push_back( lem );
+    d_num_added_lemmas_round++;
     return true;
   }
 }
@@ -1115,6 +1121,14 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
   }
 }
 
+bool QuantifiersEngine::removeInstantiation( Node q, Node lem, std::vector< Node >& terms ) {
+  //lem must occur in d_waiting_lemmas
+  if( removeLemma( lem ) ){
+    return removeInstantiationInternal( q, terms );
+  }else{
+    return false;
+  }
+}
 
 bool QuantifiersEngine::addSplit( Node n, bool reqPhase, bool reqPhasePol ){
   n = Rewriter::rewrite( n );
@@ -1134,16 +1148,10 @@ bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool
   return addSplit( fm );
 }
 
-bool QuantifiersEngine::removeInstantiation( Node q, Node lem, std::vector< Node >& terms ) {
-  //lem must occur in d_waiting_lemmas
-  if( removeLemma( lem ) ){
-    return removeInstantiationInternal( q, terms );
-  }else{
-    return false;
-  }
+void QuantifiersEngine::markRelevant( Node q ) {
+  d_model->markRelevant( q );
 }
 
-
 bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
   Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter << ", " << d_ierCounter_lc << std::endl;
   //determine if we should perform check, based on instWhenMode
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index bad9c0169..a088dfec6 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -156,6 +156,8 @@ private:  //this information is reset during check
   unsigned d_curr_effort_level;
   /** are we in conflict */
   bool d_conflict;
+  /** number of lemmas we actually added this round (for debugging) */
+  unsigned d_num_added_lemmas_round;
   /** has added lemma this round */
   bool d_hasAddedLemma;
 private:
@@ -317,12 +319,16 @@ public:
   bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true );
   /** add split equality */
   bool addSplitEquality( Node n1, Node n2, bool reqPhase = false, bool reqPhasePol = true );
+  /** mark relevant quantified formula, this will indicate it should be checked before the others */
+  void markRelevant( Node q );
   /** has added lemma */
   bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; }
   /** is in conflict */
   bool inConflict() { return d_conflict; }
   /** get number of waiting lemmas */
   unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); }
+  /** get number of waiting lemmas */
+  unsigned getNumLemmasAddedThisRound() { return d_num_added_lemmas_round; }
   /** get needs check */
   bool getInstWhenNeedsCheck( Theory::Effort e );
   /** get user pat mode */
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 784eaf677..b51313deb 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -77,7 +77,8 @@ TESTS =	\
 	anti-sk-simp.smt2 \
 	pure_dt_cbqi.smt2 \
 	florian-case-ax.smt2 \
-	double-pattern.smt2
+	double-pattern.smt2 \
+	qcf-rel-dom-opt.smt2
 
 
 # regression can be solved with --finite-model-find --fmf-inst-engine
diff --git a/test/regress/regress0/quantifiers/qcf-rel-dom-opt.smt2 b/test/regress/regress0/quantifiers/qcf-rel-dom-opt.smt2
new file mode 100644
index 000000000..539f181af
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qcf-rel-dom-opt.smt2
@@ -0,0 +1,45 @@
+(set-logic UFLIA)
+(set-info :status unsat)
+(declare-fun P (Int) Bool)
+
+(assert (P 0))
+(assert (P 1))
+(assert (P 2))
+(assert (P 3))
+(assert (P 4))
+(assert (P 5))
+(assert (P 6))
+(assert (P 7))
+(assert (P 8))
+(assert (P 9))
+
+(assert (P 10))
+(assert (P 11))
+(assert (P 12))
+(assert (P 13))
+(assert (P 14))
+(assert (P 15))
+(assert (P 16))
+(assert (P 17))
+(assert (P 18))
+(assert (P 19))
+
+(assert (P 20))
+(assert (P 21))
+(assert (P 22))
+(assert (P 23))
+(assert (P 24))
+(assert (P 25))
+(assert (P 26))
+(assert (P 27))
+(assert (P 28))
+(assert (P 29))
+
+(declare-fun Q (Int Int Int Int Int) Bool)
+(assert (forall ((x Int) (y Int) (z Int) (w Int) (q Int)) (or (not (P x)) (not (P y)) (not (P z)) (not (P w)) (not (P q)) (Q x y z w q))))
+
+(declare-fun R (Int) Bool)
+(assert (R 0))
+(assert (forall ((x Int)) (not (R x))))
+
+(check-sat)
-- 
2.30.2