Minor refactoring of entailment tests and quantifiers util. Initial draft of instantiation propagator.

15 files changed, 1129 insertions, 318 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 610bcb305..908245e63 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -364,6 +364,8 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/anti_skolem.cpp \
 	theory/quantifiers/equality_infer.h \
 	theory/quantifiers/equality_infer.cpp \
+	theory/quantifiers/inst_propagator.h \
+	theory/quantifiers/inst_propagator.cpp \
 	theory/arith/theory_arith_type_rules.h \
 	theory/arith/type_enumerator.h \
 	theory/arith/arithvar.h \
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 8ed4f24c0..c27b21e23 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -174,6 +174,9 @@ option qcfAllConflict --qcf-all-conflict bool :read-write :default false
 
 option instNoEntail --inst-no-entail bool :read-write :default true
  do not consider instances of quantified formulas that are currently entailed
+
+option instPropagate --inst-propagate bool :read-write :default false
+ internal propagation for instantiations for selecting relevant instances
  
 ### rewrite rules options 
  
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index beec9da3b..f8a9eefcb 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -1273,7 +1273,7 @@ bool ConjectureGenerator::notifySubstitution( TNode glhs, std::map< TNode, TNode
   }
   Trace("sg-cconj-debug") << "Evaluate RHS : : " << rhs << std::endl;
   //get the representative of rhs with substitution subs
-  TNode grhs = getTermDatabase()->evaluateTerm( rhs, subs, true );
+  TNode grhs = getTermDatabase()->getEntailedTerm( rhs, subs, true );
   Trace("sg-cconj-debug") << "...done evaluating term, got : " << grhs << std::endl;
   if( !grhs.isNull() ){
     if( glhs!=grhs ){
diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp
new file mode 100644
index 000000000..d20f3fd4a
--- /dev/null
+++ b/src/theory/quantifiers/inst_propagator.cpp
@@ -0,0 +1,674 @@
+/*********************                                                        */

+/*! \file inst_propagator.cpp

+ ** \verbatim

+ ** Top contributors (to current version):

+ **   Andrew Reynolds

+ ** This file is part of the CVC4 project.

+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS

+ ** in the top-level source directory) and their institutional affiliations.

+ ** All rights reserved.  See the file COPYING in the top-level source

+ ** directory for licensing information.\endverbatim

+ **

+ ** Propagate mechanism for instantiations

+ **/

+

+#include <vector>

+

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

+#include "theory/rewriter.h"

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

+

+using namespace CVC4;

+using namespace std;

+using namespace CVC4::theory;

+using namespace CVC4::theory::quantifiers;

+using namespace CVC4::kind;

+

+

+EqualityQueryInstProp::EqualityQueryInstProp( QuantifiersEngine* qe ) : d_qe( qe ){

+  d_true = NodeManager::currentNM()->mkConst( true );

+  d_false = NodeManager::currentNM()->mkConst( false );

+}

+

+bool EqualityQueryInstProp::reset( Theory::Effort e ) {

+  d_uf.clear();

+  d_uf_exp.clear();

+  d_diseq_list.clear();

+  return true;

+}

+

+/** contains term */

+bool EqualityQueryInstProp::hasTerm( Node a ) {

+  if( getEngine()->hasTerm( a ) ){

+    return true;

+  }else{

+    std::vector< Node > exp;

+    Node ar = getUfRepresentative( a, exp );

+    return !ar.isNull() && getEngine()->hasTerm( ar );

+  }

+}

+

+/** get the representative of the equivalence class of a */

+Node EqualityQueryInstProp::getRepresentative( Node a ) {

+  if( getEngine()->hasTerm( a ) ){

+    a = getEngine()->getRepresentative( a );

+  }

+  std::vector< Node > exp;

+  Node ar = getUfRepresentative( a, exp );

+  return ar.isNull() ? a : ar;

+}

+

+/** returns true if a and b are equal in the current context */

+bool EqualityQueryInstProp::areEqual( Node a, Node b ) {

+  if( a==b ){

+    return true;

+  }else{

+    eq::EqualityEngine* ee = getEngine();

+    if( ee->hasTerm( a ) && ee->hasTerm( b ) ){

+      if( ee->areEqual( a, b ) ){

+        return true;

+      }

+    }

+    return false;

+  }

+}

+

+/** returns true is a and b are disequal in the current context */

+bool EqualityQueryInstProp::areDisequal( Node a, Node b ) {

+  if( a==b ){

+    return true;

+  }else{

+    eq::EqualityEngine* ee = getEngine();

+    if( ee->hasTerm( a ) && ee->hasTerm( b ) ){

+      if( ee->areDisequal( a, b, false ) ){

+        return true;

+      }

+    }

+    return false;

+  }

+}

+

+/** get the equality engine associated with this query */

+eq::EqualityEngine* EqualityQueryInstProp::getEngine() {

+  return d_qe->getMasterEqualityEngine();

+}

+

+/** get the equivalence class of a */

+void EqualityQueryInstProp::getEquivalenceClass( Node a, std::vector< Node >& eqc ) {

+  //TODO?

+}

+

+TNode EqualityQueryInstProp::getCongruentTerm( Node f, std::vector< TNode >& args ) {

+  TNode t = d_qe->getTermDatabase()->getCongruentTerm( f, args );

+  if( !t.isNull() ){

+    return t;

+  }else{

+    //TODO?

+    return TNode::null();

+  }

+}

+

+Node EqualityQueryInstProp::getRepresentativeExp( Node a, std::vector< Node >& exp ) {

+  bool engine_has_a = getEngine()->hasTerm( a );

+  if( engine_has_a ){

+    a = getEngine()->getRepresentative( a );

+  }

+  //get union find representative, if this occurs in the equality engine, return it

+  unsigned prev_size = exp.size();

+  Node ar = getUfRepresentative( a, exp );

+  if( !ar.isNull() ){

+    if( engine_has_a || getEngine()->hasTerm( ar ) ){

+      Assert( getEngine()->hasTerm( ar ) );

+      Assert( getEngine()->getRepresentative( ar )==ar );

+      return ar;

+    }

+  }else{

+    if( engine_has_a ){

+      return a;

+    }

+  }

+  //retract explanation

+  while( exp.size()>prev_size ){

+    exp.pop_back();

+  }

+  return Node::null();

+}

+

+bool EqualityQueryInstProp::areEqualExp( Node a, Node b, std::vector< Node >& exp ) {

+  if( areEqual( a, b ) ){

+    return true;

+  }else{

+    std::vector< Node > exp_a;

+    Node ar = getUfRepresentative( a, exp_a );

+    if( !ar.isNull() ){

+      std::vector< Node > exp_b;

+      if( ar==getUfRepresentative( b, exp_b ) ){

+        merge_exp( exp, exp_a );

+        merge_exp( exp, exp_b );

+        return true;

+      }

+    }

+    return false;

+  }

+}

+

+bool EqualityQueryInstProp::areDisequalExp( Node a, Node b, std::vector< Node >& exp ) {

+  if( areDisequal( a, b ) ){

+    return true;

+  }else{

+    //TODO?

+    return false;

+  }

+}

+

+Node EqualityQueryInstProp::getUfRepresentative( Node a, std::vector< Node >& exp ) {

+  Assert( exp.empty() );

+  std::map< Node, Node >::iterator it = d_uf.find( a );

+  if( it!=d_uf.end() ){

+    if( it->second==a ){

+      Assert( d_uf_exp[ a ].empty() );

+      return it->second;

+    }else{

+      Node m = getUfRepresentative( it->second, exp );

+      Assert( !m.isNull() );

+      if( m!=it->second ){

+        //update union find

+        d_uf[ a ] = m;

+        //update explanation : merge the explanation of the parent

+        merge_exp( d_uf_exp[ a ], exp );

+        Trace("qip-eq") << "EqualityQueryInstProp::getUfRepresentative : merge " << a << " -> " << m << ", exp size=" << d_uf_exp[ a ].size() << std::endl;

+      }

+      //add current explanation to exp: note that exp is a subset of d_uf_exp[ a ], reset

+      exp.clear();

+      exp.insert( exp.end(), d_uf_exp[ a ].begin(), d_uf_exp[ a ].end() );

+      return m;

+    }

+  }else{

+    return Node::null();

+  }

+}

+

+// set a == b with reason, return status, modify a and b to representatives pre-merge

+int EqualityQueryInstProp::setEqual( Node& a, Node& b, std::vector< Node >& reason ) {

+  int status = STATUS_MERGED_UNKNOWN;

+  Trace("qip-eq") << "EqualityQueryInstProp::setEqual " << a << ", " << b << ", reason size = " << reason.size() << std::endl;

+  //get the representative for a

+  std::vector< Node > exp_a;

+  Node ar = getUfRepresentative( a, exp_a );

+  if( ar.isNull() ){

+    Assert( exp_a.empty() );

+    ar = a;

+  }

+  if( ar==b ){

+    Trace("qip-eq") << "EqualityQueryInstProp::setEqual : already equal" << std::endl;

+    return STATUS_NONE;

+  }

+  bool swap = false;

+  //get the representative for b

+  std::vector< Node > exp_b;

+  Node br = getUfRepresentative( b, exp_b );

+  if( br.isNull() ){

+    Assert( exp_b.empty() );

+    br = b;

+    if( !getEngine()->hasTerm( br ) ){

+      if( ar!=a ){

+        swap = true;

+      }

+    }else{

+      if( getEngine()->hasTerm( ar ) ){

+        status = STATUS_MERGED_KNOWN;

+      }

+    }

+  }else{

+    if( ar==br ){

+      Trace("qip-eq") << "EqualityQueryInstProp::setEqual : already equal" << std::endl;

+      return STATUS_NONE;

+    }else if( getEngine()->hasTerm( ar ) ){

+      if( getEngine()->hasTerm( br ) ){

+        status = STATUS_MERGED_KNOWN;

+      }else{

+        swap = true;

+      }

+    }

+  }

+  if( swap ){

+    //swap

+    Node temp_r = ar;

+    ar = br;

+    br = temp_r;

+  }

+

+  Assert( ar!=br );

+  Assert( !getEngine()->hasTerm( ar ) || getEngine()->hasTerm( br ) );

+

+  //update the union find

+  Assert( d_uf_exp[ar].empty() );

+  Assert( d_uf_exp[br].empty() );

+

+  d_uf[ar] = br;

+  merge_exp( d_uf_exp[ar], exp_a );

+  merge_exp( d_uf_exp[ar], exp_b );

+  merge_exp( d_uf_exp[ar], reason );

+

+  d_uf[br] = br;

+  d_uf_exp[br].clear();

+

+  Trace("qip-eq") << "EqualityQueryInstProp::setEqual : merge " << ar << " -> " << br << ", exp size = " << d_uf_exp[ar].size() << ", status = " << status << std::endl;

+  a = ar;

+  b = br;

+  return status;

+}

+

+

+void EqualityQueryInstProp::addArgument( std::vector< TNode >& args, std::vector< TNode >& props, Node n, bool is_prop, bool pol ) {

+  if( is_prop ){

+    if( isLiteral( n ) ){

+      props.push_back( pol ? n : n.negate() );

+      return;

+    }

+  }

+  args.push_back( n );

+}

+

+bool EqualityQueryInstProp::isLiteral( Node n ) {

+  Kind ak = n.getKind()==NOT ? n[0].getKind() : n.getKind();

+  Assert( ak!=NOT );

+  return ak!=AND && ak!=OR && ak!=IFF && ak!=ITE;

+}

+

+//this is identical to TermDb::evaluateTerm2, but tracks more information

+Node EqualityQueryInstProp::evaluateTermExp( TNode n, std::vector< Node >& exp, std::map< TNode, Node >& visited, bool hasPol, bool pol,

+                                             std::map< Node, bool >& watch_list_out, std::vector< TNode >& props ) {

+  std::map< TNode, Node >::iterator itv = visited.find( n );

+  if( itv != visited.end() ){

+    return itv->second;

+  }else{

+    Trace("term-db-eval") << "evaluate term : " << n << std::endl;

+    std::vector< Node > exp_n;

+    Node ret = getRepresentativeExp( n, exp_n );

+    if( ret.isNull() ){

+      //term is not known to be equal to a representative in equality engine, evaluate it

+      Kind k = n.getKind();

+      if( k==FORALL ){

+        ret = Node::null();

+      }else{

+        std::map< Node, bool > watch_list_out_curr;

+        TNode f = d_qe->getTermDatabase()->getMatchOperator( n );

+        std::vector< TNode > args;

+        bool ret_set = false;

+        bool childChanged = false;

+        int abort_i = -1;

+        //get the child entailed polarity

+        Assert( n.getKind()!=IMPLIES );

+        bool newHasPol, newPol;

+        QuantPhaseReq::getEntailPolarity( n, 0, hasPol, pol, newHasPol, newPol );

+        //for each child

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

+          TNode c = evaluateTermExp( n[i], exp, visited, newHasPol, newPol, watch_list_out_curr, props );

+          if( c.isNull() ){

+            ret = Node::null();

+            ret_set = true;

+            break;

+          }else if( c==d_true || c==d_false ){

+            //short-circuiting

+            if( k==kind::AND || k==kind::OR ){

+              if( (k==kind::AND)==(c==d_false) ){

+                ret = c;

+                ret_set = true;

+                break;

+              }else{

+                //redundant

+                c = Node::null();

+                childChanged = true;

+              }

+            }else if( k==kind::ITE && i==0 ){

+              Assert( watch_list_out_curr.empty() );

+              ret = evaluateTermExp( n[ c==d_true ? 1 : 2], exp, visited, hasPol, pol, watch_list_out_curr, props );

+              ret_set = true;

+              break;

+            }else if( k==kind::NOT ){

+              ret = c==d_true ? d_false : d_true;

+              ret_set = true;

+              break;

+            }

+          }

+          if( !c.isNull() ){

+            childChanged = childChanged || n[i]!=c;

+            if( !f.isNull() && !watch_list_out_curr.empty() ){

+              // we are done if this is an UF application and an argument is unevaluated

+              args.push_back( c );

+              abort_i = i;

+              break;

+            }else if( ( k==kind::AND || k==kind::OR ) ){

+              if( c.getKind()==k ){

+                //flatten

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

+                  addArgument( args, props, c[j], newHasPol, newPol );

+                }

+              }else{

+                addArgument( args, props, c, newHasPol, newPol );

+              }

+              //if we are in a branching position

+              if( hasPol && !newHasPol && args.size()>=2 ){

+                //we are done if at least two args are unevaluated

+                abort_i = i;

+                break;

+              }

+            }else if( k==kind::ITE ){

+              //we are done if we are ITE and condition is unevaluated

+              Assert( i==0 );

+              args.push_back( c );

+              abort_i = i;

+              break;

+            }else{

+              args.push_back( c );

+            }

+          }

+        }

+        //add remaining children if we aborted

+        if( abort_i!=-1 ){

+          for( int i=(abort_i+1); i<(int)n.getNumChildren(); i++ ){

+            args.push_back( n[i] );

+          }

+        }

+        //copy over the watch list

+        for( std::map< Node, bool >::iterator itc = watch_list_out_curr.begin(); itc != watch_list_out_curr.end(); ++itc ){

+          watch_list_out[itc->first] = itc->second;

+        }

+

+        //if we have not short-circuited evaluation

+        if( !ret_set ){

+          //if it is an indexed term, return the congruent term

+          if( !f.isNull() && watch_list_out.empty() ){

+            Assert( args.size()==n.getNumChildren() );

+            //args contains terms known by the equality engine

+            TNode nn = getCongruentTerm( f, args );

+            Trace("term-db-eval") << "  got congruent term " << nn << " from DB for " << n << std::endl;

+            if( !nn.isNull() ){

+              //successfully constructed representative in EE

+              Assert( exp_n.empty() );

+              ret = getRepresentativeExp( nn, exp_n );

+              Trace("term-db-eval") << "return rep, exp size = " << exp_n.size() << std::endl;

+              merge_exp( exp, exp_n );

+              ret_set = true;

+              Assert( !ret.isNull() );

+            }

+          }

+          if( !ret_set ){

+            if( childChanged ){

+              Trace("term-db-eval") << "return rewrite" << std::endl;

+              if( ( k==kind::AND || k==kind::OR ) ){

+                if( args.empty() ){

+                  ret = k==kind::AND ? d_true : d_false;

+                  ret_set = true;

+                }else if( args.size()==1 ){

+                  ret = args[0];

+                  ret_set = true;

+                }

+              }

+              if( !ret_set ){

+                Assert( args.size()==n.getNumChildren() );

+                if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){

+                  args.insert( args.begin(), n.getOperator() );

+                }

+                ret = NodeManager::currentNM()->mkNode( k, args );

+                ret = Rewriter::rewrite( ret );

+                watch_list_out[ret] = true;

+              }

+            }else{

+              ret = n;

+              watch_list_out[ret] = true;

+            }

+          }

+        }

+      }

+    }else{

+      Trace("term-db-eval") << "...exists in ee, return rep, exp size = " << exp_n.size() << std::endl;

+      merge_exp( exp, exp_n );

+    }

+    Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret << ", exp size = " << exp.size() << std::endl;

+    visited[n] = ret;

+    return ret;

+  }

+}

+

+void EqualityQueryInstProp::merge_exp( std::vector< Node >& v, std::vector< Node >& v_to_merge, int up_to_size ) {

+  //TODO : optimize

+  if( v.empty() ){

+    Assert( up_to_size==-1 || up_to_size==(int)v_to_merge.size() );

+    v.insert( v.end(), v_to_merge.begin(), v_to_merge.end() );

+  }else{

+    //std::vector< Node >::iterator v_end = v.end();

+    up_to_size = up_to_size==-1 ? (int)v_to_merge.size() : up_to_size;

+    for( int j=0; j<up_to_size; j++ ){

+      if( std::find( v.begin(), v.end(), v_to_merge[j] )==v.end() ){

+        v.push_back( v_to_merge[j] );

+      }

+    }

+  }

+}

+

+

+void InstPropagator::InstInfo::init( Node q, Node lem, std::vector< Node >& terms, Node body ) {

+  d_active = true;

+  //information about the instance

+  d_q = q;

+  d_lem = lem;

+  Assert( d_terms.empty() );

+  d_terms.insert( d_terms.end(), terms.begin(), terms.end() );

+  //the current lemma

+  d_curr = body;

+  d_curr_exp.push_back( body );

+}

+

+InstPropagator::InstPropagator( QuantifiersEngine* qe ) :

+d_qe( qe ), d_notify(*this), d_qy( qe ){

+}

+

+bool InstPropagator::reset( Theory::Effort e ) {

+  d_icount = 0;

+  d_ii.clear();

+  for( unsigned i=0; i<2; i++ ){

+    d_conc_to_id[i].clear();

+  }

+  d_conflict = false;

+  d_watch_list.clear();

+  d_relevant_inst.clear();

+  return d_qy.reset( e );

+}

+

+void InstPropagator::notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) {

+  if( !d_conflict ){

+    if( Trace.isOn("qip-prop") ){

+      Trace("qip-prop") << "InstPropagator:: Notify instantiation " << q << " : " << std::endl;

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

+        Trace("qip-prop") << "  " << terms[i] << std::endl;

+      }

+    }

+    unsigned id = d_icount;

+    d_icount++;

+    Trace("qip-prop") << "...assign id=" << id << std::endl;

+    d_ii[id].init( q, lem, terms, body );

+    //initialize the information

+    if( cacheConclusion( id, body ) ){

+      Assert( d_update_list.empty() );

+      d_update_list.push_back( id );

+      bool firstTime = true;

+      //update infos in the update list until empty 

+      do {

+        unsigned uid = d_update_list.back();

+        d_update_list.pop_back();

+        if( d_ii[uid].d_active ){

+          update( uid, d_ii[uid], firstTime );

+        }

+        firstTime = false;

+      }while( !d_update_list.empty() );

+    }else{

+      d_ii[id].d_active = false;

+      Trace("qip-prop") << "...duplicate." << std::endl;

+    }

+  }

+}

+

+bool InstPropagator::update( unsigned id, InstInfo& ii, bool firstTime ) {

+  Assert( !d_conflict );

+  Assert( ii.d_active );

+  Trace("qip-prop-debug") << "Update info [" << id << "]..." << std::endl;

+  //update the evaluation of the current lemma

+  std::map< TNode, Node > visited;

+  std::map< Node, bool > watch_list;

+  std::vector< TNode > props;

+  Node eval = d_qy.evaluateTermExp( ii.d_curr, ii.d_curr_exp, visited, true, true, watch_list, props );

+  if( eval.isNull() ){

+    ii.d_active = false;

+  }else if( firstTime || eval!=ii.d_curr ){

+    if( EqualityQueryInstProp::isLiteral( eval ) ){

+      props.push_back( eval );

+      eval = d_qy.d_true;

+      watch_list.clear();

+    }

+    if( Trace.isOn("qip-prop") ){

+      Trace("qip-prop") << "Update info [" << id << "]..." << std::endl;

+      Trace("qip-prop") << "...updated lemma " << ii.d_curr << " -> " << eval << ", exp = ";

+      debugPrintExplanation( ii.d_curr_exp, "qip-prop" );

+      Trace("qip-prop") << std::endl;

+      Trace("qip-prop") << "...watch list: " << std::endl;

+      for( std::map< Node, bool >::iterator itw = watch_list.begin(); itw!=watch_list.end(); ++itw ){

+        Trace("qip-prop") << "  " << itw->first << std::endl;

+      }

+      Trace("qip-prop") << "...new propagations: " << std::endl;

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

+        Trace("qip-prop") << "  " << props[i] << std::endl;

+      }

+      Trace("qip-prop") << std::endl;

+    }

+    //determine the status of eval

+    if( eval==d_qy.d_false ){

+      Assert( props.empty() );

+      //we have inferred a conflict

+      conflict( ii.d_curr_exp );

+      return false;

+    }else{

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

+        //if we haven't propagated this literal yet

+        if( cacheConclusion( id, props[i], 1 ) ){

+          Node lit = props[i].getKind()==NOT ? props[i][0] : props[i];

+          bool pol = props[i].getKind()!=NOT;

+          if( lit.getKind()==EQUAL ){

+            propagate( lit[0], lit[1], pol, ii.d_curr_exp );

+          }else{

+            propagate( lit, pol ? d_qy.d_true : d_qy.d_false, true, ii.d_curr_exp );

+          }

+          if( d_conflict ){

+            return false;

+          }

+        }

+      }

+      //if we have not inferred this conclusion yet

+      if( cacheConclusion( id, eval ) ){

+        ii.d_curr = eval;

+        //update the watch list

+        Trace("qip-prop-debug") << "...updating watch list for [" << id << "], curr is " << ii.d_curr << std::endl;

+        //Here, we need to be notified of enough terms such that if we are not notified, then update( ii ) will return no propagations.

+        //  Similar to two-watched literals, but since we are in UF, we need to watch all terms on a complete path of two terms.

+        for( std::map< Node, bool >::iterator itw = watch_list.begin(); itw != watch_list.end(); ++itw ){

+          d_watch_list[ itw->first ][ id ] = true;

+        }

+      }else{

+        Trace("qip-prop-debug") << "...conclusion is duplicate." << std::endl;

+        ii.d_active = false;

+      }

+    }

+  }else{

+    Trace("qip-prop-debug") << "...did not update." << std::endl;

+  }

+  Assert( !d_conflict );

+  return true;

+}

+

+void InstPropagator::propagate( Node a, Node b, bool pol, std::vector< Node >& exp ) {

+  if( Trace.isOn("qip-propagate") ){

+    Trace("qip-propagate") << "* Propagate " << a << ( pol ? " == " : " != " ) << b << ", exp = ";

+    debugPrintExplanation( exp, "qip-propagate" );

+    Trace("qip-propagate") << "..." << std::endl;

+  }

+  if( pol ){

+    std::vector< Node > exp_d;

+    if( d_qy.areDisequalExp( a, b, exp_d ) ){

+      Trace("qip-prop-debug") << "...conflict." << std::endl;

+      EqualityQueryInstProp::merge_exp( exp, exp_d );

+      conflict( exp );

+    }else{

+      //set equal

+      int status = d_qy.setEqual( a, b, exp );

+      if( status==EqualityQueryInstProp::STATUS_NONE ){

+        Trace("qip-prop-debug") << "...already equal." << std::endl;

+        return;

+      }else if( status==EqualityQueryInstProp::STATUS_MERGED_KNOWN ){

+        Assert( d_qy.getEngine()->hasTerm( a ) );

+        Assert( d_qy.getEngine()->hasTerm( b ) );

+        Trace("qip-prop-debug") << "...equality between known terms." << std::endl;

+        addRelevantInstances( exp, "qip-propagate" );

+      }

+      Trace("qip-prop-debug") << "...merging " << a << " and " << b << std::endl;

+      for( unsigned i=0; i<2; i++ ){

+        //update terms from watched lists

+        Node c = i==0 ? a : b;

+        std::map< Node, std::map< unsigned, bool > >::iterator it = d_watch_list.find( c );

+        if( it!=d_watch_list.end() ){

+          Trace("qip-prop-debug") << "...update ids from watch list of " << c << ", size=" << it->second.size() << "..." << std::endl;

+          for( std::map< unsigned, bool >::iterator itw = it->second.begin(); itw != it->second.end(); ++itw ){

+            unsigned idw = itw->first;

+            if( std::find( d_update_list.begin(), d_update_list.end(), idw )==d_update_list.end() ){

+              Trace("qip-prop-debug") << "...will update " << idw << std::endl;

+              d_update_list.push_back( idw );

+            }

+          }

+          d_watch_list.erase( c );

+        }

+      }

+    }

+  }else{

+    std::vector< Node > exp_e;

+    if( d_qy.areEqualExp( a, b, exp_e ) ){

+      EqualityQueryInstProp::merge_exp( exp, exp_e );

+      conflict( exp );

+    }else{

+      //TODO?

+    }

+  }

+}

+

+void InstPropagator::conflict( std::vector< Node >& exp ) {

+  Trace("qip-propagate") << "Conflict, exp size =" << exp.size() << std::endl;

+  d_conflict = true;

+  d_relevant_inst.clear();

+  addRelevantInstances( exp, "qip-propagate" );

+}

+

+bool InstPropagator::cacheConclusion( unsigned id, Node body, int prop_index ) {

+  Assert( prop_index==0 || prop_index==1 );

+  //check if the conclusion is non-redundant

+  if( d_conc_to_id[prop_index].find( body )==d_conc_to_id[prop_index].end() ){

+    d_conc_to_id[prop_index][body] = id;

+    return true;

+  }else{

+    return false;

+  }

+}

+

+void InstPropagator::addRelevantInstances( std::vector< Node >& exp, const char * c ) {

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

+    Assert( d_conc_to_id[0].find( exp[i] )!=d_conc_to_id[0].end() );

+    Trace(c) << "  relevant instance id : " << d_conc_to_id[0][ exp[i] ] << std::endl;

+    d_relevant_inst[ d_conc_to_id[0][ exp[i] ] ] = true;

+  }

+}

+

+void InstPropagator::debugPrintExplanation( std::vector< Node >& exp, const char * c ) {

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

+    Assert( d_conc_to_id[0].find( exp[i] )!=d_conc_to_id[0].end() );

+    Trace(c) << d_conc_to_id[0][ exp[i] ] << " ";

+  }

+}

+

diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h
new file mode 100644
index 000000000..0e21dc0d4
--- /dev/null
+++ b/src/theory/quantifiers/inst_propagator.h
@@ -0,0 +1,160 @@
+/*********************                                                        */

+/*! \file inst_propagator.h

+ ** \verbatim

+ ** Top contributors (to current version):

+ **   Andrew Reynolds

+ ** This file is part of the CVC4 project.

+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS

+ ** in the top-level source directory) and their institutional affiliations.

+ ** All rights reserved.  See the file COPYING in the top-level source

+ ** directory for licensing information.\endverbatim

+ **

+ ** \brief Propagate mechanism for instantiations

+ **/

+

+#include "cvc4_private.h"

+

+#ifndef __CVC4__QUANTIFIERS_INST_PROPAGATOR_H

+#define __CVC4__QUANTIFIERS_INST_PROPAGATOR_H

+

+#include <iostream>

+#include <string>

+#include <vector>

+#include <map>

+#include "expr/node.h"

+#include "expr/type_node.h"

+#include "theory/quantifiers_engine.h"

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

+

+namespace CVC4 {

+namespace theory {

+namespace quantifiers {

+

+class EqualityQueryInstProp : public EqualityQuery {

+private:

+  /** pointer to quantifiers engine */

+  QuantifiersEngine* d_qe;

+public:

+  EqualityQueryInstProp( QuantifiersEngine* qe );

+  ~EqualityQueryInstProp(){};

+  /** reset */

+  bool reset( Theory::Effort e );

+  /** identify */

+  std::string identify() const { return "EqualityQueryInstProp"; }

+  /** extends engine */

+  bool extendsEngine() { return true; }

+  /** contains term */

+  bool hasTerm( Node a );

+  /** get the representative of the equivalence class of a */

+  Node getRepresentative( Node a );

+  /** returns true if a and b are equal in the current context */

+  bool areEqual( Node a, Node b );

+  /** returns true is a and b are disequal in the current context */

+  bool areDisequal( Node a, Node b );

+  /** get the equality engine associated with this query */

+  eq::EqualityEngine* getEngine();

+  /** get the equivalence class of a */

+  void getEquivalenceClass( Node a, std::vector< Node >& eqc );

+  /** get congruent term */

+  TNode getCongruentTerm( Node f, std::vector< TNode >& args );

+public:

+  /** get the representative of the equivalence class of a, with explanation */

+  Node getRepresentativeExp( Node a, std::vector< Node >& exp );

+  /** returns true if a and b are equal in the current context */

+  bool areEqualExp( Node a, Node b, std::vector< Node >& exp );

+  /** returns true is a and b are disequal in the current context */

+  bool areDisequalExp( Node a, Node b, std::vector< Node >& exp );

+private:

+  /** term index */

+  std::map< Node, TermArgTrie > d_func_map_trie;

+  /** union find for terms beyond what is stored in equality engine */

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

+  std::map< Node, std::vector< Node > > d_uf_exp;

+  Node getUfRepresentative( Node a, std::vector< Node >& exp );

+  /** disequality list, stores explanations */

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

+  /** add arg */

+  void addArgument( std::vector< TNode >& args, std::vector< TNode >& props, Node n, bool is_prop, bool pol );

+public:

+  enum {

+    STATUS_MERGED_KNOWN,

+    STATUS_MERGED_UNKNOWN,

+    STATUS_NONE,

+  };

+  /** set equal */

+  int setEqual( Node& a, Node& b, std::vector< Node >& reason );

+  Node d_true;

+  Node d_false;

+public:

+  //for explanations

+  static void merge_exp( std::vector< Node >& v, std::vector< Node >& v_to_merge, int up_to_size = -1 );

+

+  Node evaluateTermExp( TNode n, std::vector< Node >& exp, std::map< TNode, Node >& visited, bool hasPol, bool pol,

+                        std::map< Node, bool >& watch_list_out, std::vector< TNode >& props );

+  static bool isLiteral( Node n );

+};

+

+class InstPropagator : public QuantifiersUtil {

+private:

+  /** pointer to quantifiers engine */

+  QuantifiersEngine* d_qe;

+  /** notify class */

+  class InstantiationNotifyInstPropagator : public InstantiationNotify {

+    InstPropagator& d_ip;

+  public:

+    InstantiationNotifyInstPropagator(InstPropagator& ip): d_ip(ip) {}

+    virtual void notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) { d_ip.notifyInstantiation( quant_e, q, lem, terms, body ); }

+  };

+  InstantiationNotifyInstPropagator d_notify;

+  /** notify instantiation method */

+  void notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body );

+  /** equality query */

+  EqualityQueryInstProp d_qy;

+  class InstInfo {

+  public:

+    bool d_active;

+    Node d_q;

+    Node d_lem;

+    std::vector< Node > d_terms;

+    // the current entailed body

+    Node d_curr;

+    //explanation for current entailed body

+    std::vector< Node > d_curr_exp;

+    void init( Node q, Node lem, std::vector< Node >& terms, Node body );

+  };

+  /** instantiation count/info */

+  unsigned d_icount;

+  std::map< unsigned, InstInfo > d_ii;

+  std::map< TNode, unsigned > d_conc_to_id[2];

+  /** are we in conflict */

+  bool d_conflict;

+  /** watch list */

+  std::map< Node, std::map< unsigned, bool > > d_watch_list;

+  /** update list */

+  std::vector< unsigned > d_update_list;

+  /** relevant instances */

+  std::map< unsigned, bool > d_relevant_inst;

+private:

+  bool update( unsigned id, InstInfo& i, bool firstTime = false );

+  void propagate( Node a, Node b, bool pol, std::vector< Node >& exp );

+  void conflict( std::vector< Node >& exp );

+  bool cacheConclusion( unsigned id, Node body, int prop_index = 0 );

+  void addRelevantInstances( std::vector< Node >& exp, const char * c );

+

+  void debugPrintExplanation( std::vector< Node >& exp, const char * c );

+public:

+  InstPropagator( QuantifiersEngine* qe );

+  ~InstPropagator(){}

+  /** reset */

+  bool reset( Theory::Effort e );

+  /** identify */

+  std::string identify() const { return "InstPropagator"; }

+  /** get the notify mechanism */

+  InstantiationNotify* getInstantiationNotify() { return &d_notify; }

+};

+

+}

+}

+}

+

+#endif

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index e1cbbcfe3..e5df41510 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1061,16 +1061,27 @@ void MatchGen::reset_round( QuantConflictFind * p ) {
     d_qni_gterm_rep[it->first] = p->getRepresentative( it->second );
   }
   if( d_type==typ_ground ){
-    int e = p->evaluate( d_n );
-    if( e==1 ){
-      d_ground_eval[0] = p->d_true;
-    }else if( e==-1 ){
-      d_ground_eval[0] = p->d_false;
+    //int e = p->evaluate( d_n );
+    //if( e==1 ){
+    //  d_ground_eval[0] = p->d_true;
+    //}else if( e==-1 ){
+    //  d_ground_eval[0] = p->d_false;
+    //}
+    //modified 
+    for( unsigned i=0; i<2; i++ ){ 
+      if( p->getTermDatabase()->isEntailed( d_n, i==0 ) ){
+        d_ground_eval[0] = i==0 ? p->d_true : p->d_false;
+      }
     }
   }else if( d_type==typ_eq ){
     for( unsigned i=0; i<d_n.getNumChildren(); i++ ){
       if( !d_n[i].hasBoundVar() ){
-        d_ground_eval[i] = p->evaluateTerm( d_n[i] );
+        TNode t = p->getTermDatabase()->getEntailedTerm( d_n[i] );
+        if( t.isNull() ){
+          d_ground_eval[i] = d_n[i];
+        }else{
+          d_ground_eval[i] = t;
+        }
       }
     }
   }
@@ -1103,8 +1114,12 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
     int vn = qi->getCurrentRepVar( qi->getVarNum( n ) );
     if( vn==-1 ){
       //evaluate the value, see if it is compatible
-      int e = p->evaluate( n );
-      if( ( e==1 && d_tgt ) || ( e==0 && !d_tgt ) ){
+      //int e = p->evaluate( n );
+      //if( ( e==1 && d_tgt ) || ( e==0 && !d_tgt ) ){
+      //  d_child_counter = 0;
+      //}
+      //modified 
+      if( p->getTermDatabase()->isEntailed( n, d_tgt ) ){ 
         d_child_counter = 0;
       }
     }else{
@@ -1787,84 +1802,6 @@ void QuantConflictFind::registerQuantifier( Node q ) {
   }
 }
 
-int QuantConflictFind::evaluate( Node n, bool pref, bool hasPref ) {
-  int ret = 0;
-  if( n.getKind()==EQUAL ){
-    Node n1 = evaluateTerm( n[0] );
-    Node n2 = evaluateTerm( n[1] );
-    Debug("qcf-eval") << "Evaluate : Normalize " << n << " to " << n1 << " = " << n2 << std::endl;
-    if( areEqual( n1, n2 ) ){
-      ret = 1;
-    }else if( areDisequal( n1, n2 ) ){
-      ret = -1;
-    }
-    //else if( d_effort>QuantConflictFind::effort_conflict ){
-    //  ret = -1;
-    //}
-  }else if( MatchGen::isHandledUfTerm( n ) ){  //predicate
-    Node nn = evaluateTerm( n );
-    Debug("qcf-eval") << "Evaluate : Normalize " << nn << " to " << n << std::endl;
-    if( areEqual( nn, d_true ) ){
-      ret = 1;
-    }else if( areEqual( nn, d_false ) ){
-      ret = -1;
-    }
-    //else if( d_effort>QuantConflictFind::effort_conflict ){
-    //  ret = -1;
-    //}
-  }else if( n.getKind()==NOT ){
-    return -evaluate( n[0] );
-  }else if( n.getKind()==ITE ){
-    int cev1 = evaluate( n[0] );
-    int cevc[2] = { 0, 0 };
-    for( unsigned i=0; i<2; i++ ){
-      if( ( i==0 && cev1!=-1 ) || ( i==1 && cev1!=1 ) ){
-        cevc[i] = evaluate( n[i+1] );
-        if( cev1!=0 ){
-          ret = cevc[i];
-          break;
-        }else if( cevc[i]==0 ){
-          break;
-        }
-      }
-    }
-    if( ret==0 && cevc[0]!=0 && cevc[0]==cevc[1] ){
-      ret = cevc[0];
-    }
-  }else if( n.getKind()==IFF ){
-    int cev1 = evaluate( n[0] );
-    if( cev1!=0 ){
-      int cev2 = evaluate( n[1] );
-      if( cev2!=0 ){
-        ret = cev1==cev2 ? 1 : -1;
-      }
-    }
-
-  }else{
-    int ssval = 0;
-    if( n.getKind()==OR ){
-      ssval = 1;
-    }else if( n.getKind()==AND ){
-      ssval = -1;
-    }
-    bool isUnk = false;
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      int cev = evaluate( n[i] );
-      if( cev==ssval ){
-        ret = ssval;
-        break;
-      }else if( cev==0 ){
-        isUnk = true;
-      }
-    }
-    if( ret==0 && !isUnk ){
-      ret = -ssval;
-    }
-  }
-  Debug("qcf-eval") << "Evaluate " << n << " to " << ret << std::endl;
-  return ret;
-}
-
 short QuantConflictFind::getMaxQcfEffort() {
   if( options::qcfMode()==QCF_CONFLICT_ONLY ){
     return effort_conflict;
@@ -1908,38 +1845,6 @@ void QuantConflictFind::assertNode( Node q ) {
   }
 }
 
-Node QuantConflictFind::evaluateTerm( Node n ) {
-  if( MatchGen::isHandledUfTerm( n ) ){
-    Node f = MatchGen::getMatchOperator( this, n );
-    Node nn;
-    if( getEqualityEngine()->hasTerm( n ) ){
-      nn = getTermDatabase()->existsTerm( f, n );
-    }else{
-      std::vector< TNode > args;
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        Node c = evaluateTerm( n[i] );
-        args.push_back( c );
-      }
-      nn = getTermDatabase()->d_func_map_trie[f].existsTerm( args );
-    }
-    if( !nn.isNull() ){
-      Debug("qcf-eval") << "GT: Term " << nn << " for " << n << " hasTerm = " << getEqualityEngine()->hasTerm( n )  << std::endl;
-      return getRepresentative( nn );
-    }else{
-      Debug("qcf-eval") << "GT: No term for " << n << " hasTerm = " << getEqualityEngine()->hasTerm( n )  << std::endl;
-      return n;
-    }
-  }else if( n.getKind()==ITE ){
-    int v = evaluate( n[0], false, false );
-    if( v==1 ){
-      return evaluateTerm( n[1] );
-    }else if( v==-1 ){
-      return evaluateTerm( n[2] );
-    }
-  }
-  return getRepresentative( n );
-}
-
 /** new node */
 void QuantConflictFind::newEqClass( Node n ) {
 
@@ -2055,13 +1960,12 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
                   std::vector< Node > terms;
                   qi->getMatch( terms );
                   if( !qi->isTConstraintSpurious( this, terms ) ){
+                    //for debugging
                     if( Debug.isOn("qcf-check-inst") ){
-                      //if( e==effort_conflict ){
                       Node inst = d_quantEngine->getInstantiation( q, terms );
                       Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;
-                      Assert( evaluate( inst )!=1 );
-                      Assert( evaluate( inst )==-1 || e>effort_conflict );
-                      //}
+                      Assert( !getTermDatabase()->isEntailed( inst, true ) );
+                      Assert( getTermDatabase()->isEntailed( inst, false ) || e>effort_conflict );
                     }
                     if( d_quantEngine->addInstantiation( q, terms, false ) ){
                       Trace("qcf-check") << "   ... Added instantiation" << std::endl;
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 0e0e78100..36fcaddf5 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -192,9 +192,6 @@ public:  //for ground terms
   Node d_false;
   TNode getZero( Kind k );
 private:
-  Node evaluateTerm( Node n );
-  int evaluate( Node n, bool pref = false, bool hasPref = false );
-private:
   //currently asserted quantifiers
   NodeList d_qassert;
   std::map< Node, QuantInfo > d_qinfo;
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 5fbc46954..3b7787a20 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -23,6 +23,38 @@ using namespace CVC4::kind;
 using namespace CVC4::context;
 using namespace CVC4::theory;
 
+
+unsigned QuantifiersModule::needsModel( Theory::Effort e ) {
+  return QuantifiersEngine::QEFFORT_NONE;
+}
+
+eq::EqualityEngine * QuantifiersModule::getEqualityEngine() {
+  return d_quantEngine->getMasterEqualityEngine();
+}
+
+bool QuantifiersModule::areEqual( TNode n1, TNode n2 ) {
+  eq::EqualityEngine * ee = getEqualityEngine();
+  return n1==n2 || ( ee->hasTerm( n1 ) && ee->hasTerm( n2 ) && ee->areEqual( n1, n2 ) );
+}
+
+bool QuantifiersModule::areDisequal( TNode n1, TNode n2 ) {
+  eq::EqualityEngine * ee = getEqualityEngine();
+  return n1!=n2 && ee->hasTerm( n1 ) && ee->hasTerm( n2 ) && ee->areDisequal( n1, n2, false );
+}
+
+TNode QuantifiersModule::getRepresentative( TNode n ) {
+  eq::EqualityEngine * ee = getEqualityEngine();
+  if( ee->hasTerm( n ) ){
+    return ee->getRepresentative( n );
+  }else{
+    return n;
+  }
+}
+
+quantifiers::TermDb * QuantifiersModule::getTermDatabase() {
+  return d_quantEngine->getTermDatabase();
+}
+
 bool QuantArith::getMonomial( Node n, Node& c, Node& v ){
   if( n.getKind()==MULT && n.getNumChildren()==2 && n[0].isConst() ){
     c = n[0];
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 8db79db9c..79cdae437 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -29,6 +29,58 @@ namespace theory {
 
 class QuantifiersEngine;
 
+namespace quantifiers {
+  class TermDb;
+}
+
+class QuantifiersModule {
+protected:
+  QuantifiersEngine* d_quantEngine;
+public:
+  QuantifiersModule( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
+  virtual ~QuantifiersModule(){}
+  //get quantifiers engine
+  QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; }
+  /** presolve */
+  virtual void presolve() {}
+  /* whether this module needs to check this round */
+  virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; }
+  /* whether this module needs a model built */
+  virtual unsigned needsModel( Theory::Effort e );
+  /* reset at a round */
+  virtual void reset_round( Theory::Effort e ){}
+  /* Call during quantifier engine's check */
+  virtual void check( Theory::Effort e, unsigned quant_e ) = 0;
+  /* check was complete (e.g. no lemmas implies a model) */
+  virtual bool checkComplete() { return true; }
+  /* Called for new quantified formulas */
+  virtual void preRegisterQuantifier( Node q ) { }
+  /* Called for new quantifiers after owners are finalized */
+  virtual void registerQuantifier( Node q ) = 0;
+  virtual void assertNode( Node n ) {}
+  virtual void propagate( Theory::Effort level ){}
+  virtual Node getNextDecisionRequest() { return TNode::null(); }
+  /** Identify this module (for debugging, dynamic configuration, etc..) */
+  virtual std::string identify() const = 0;
+public:
+  eq::EqualityEngine * getEqualityEngine();
+  bool areDisequal( TNode n1, TNode n2 );
+  bool areEqual( TNode n1, TNode n2 );
+  TNode getRepresentative( TNode n );
+  quantifiers::TermDb * getTermDatabase();
+};/* class QuantifiersModule */
+
+class QuantifiersUtil {
+public:
+  QuantifiersUtil(){}
+  virtual ~QuantifiersUtil(){}
+  /* reset at a round */
+  virtual bool reset( Theory::Effort e ) = 0;
+  /** Identify this module (for debugging, dynamic configuration, etc..) */
+  virtual std::string identify() const = 0;
+};
+
+
 class QuantArith
 {
 public:
@@ -97,7 +149,7 @@ public:
 };
 
 
-class EqualityQuery {
+class EqualityQuery : public QuantifiersUtil{
 public:
   EqualityQuery(){}
   virtual ~EqualityQuery(){};
@@ -115,6 +167,8 @@ public:
   virtual eq::EqualityEngine* getEngine() = 0;
   /** get the equivalence class of a */
   virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0;
+  /** get the term that exists in EE that is congruent to f with args (f is returned by TermDb::getMatchOperator(...) */
+  virtual TNode getCongruentTerm( Node f, std::vector< TNode >& args ) = 0;
 };/* class EqualityQuery */
 
 
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 6cc14c023..9181677ee 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -82,8 +82,9 @@ RelevantDomain::RDomain * RelevantDomain::getRDomain( Node n, int i, bool getPar
   return getParent ? d_rel_doms[n][i]->getParent() : d_rel_doms[n][i];
 }
 
-void RelevantDomain::reset(){
+bool RelevantDomain::reset( Theory::Effort e ) {
   d_is_computed = false;
+  return true;
 }
 
 void RelevantDomain::compute(){
diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h
index 819e0e7b6..2b90520fd 100644
--- a/src/theory/quantifiers/relevant_domain.h
+++ b/src/theory/quantifiers/relevant_domain.h
@@ -23,7 +23,7 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-class RelevantDomain
+class RelevantDomain : public QuantifiersUtil
 {
 private:
   class RDomain
@@ -62,7 +62,10 @@ private:
 public:
   RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m );
   virtual ~RelevantDomain(){}
-  void reset();
+  /* reset */
+  bool reset( Theory::Effort e );
+  /** identify */
+  std::string identify() const { return "RelevantDomain"; }
   //compute the relevant domain
   void compute();
 
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 763a80af3..3d3646d7d 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -205,67 +205,59 @@ void TermDb::computeUfEqcTerms( TNode f ) {
   }
 }
 
-//returns a term n' equivalent to n
-//  - if hasSubs = true, then n is consider under substitution subs
-//  - if mkNewTerms = true, then n' is either null, or a term in the master equality engine
-Node TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, std::map< TNode, Node >& visited, EqualityQuery * qy ) {
+//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 ) {
   std::map< TNode, Node >::iterator itv = visited.find( n );
   if( itv != visited.end() ){
     return itv->second;
   }
-  Node ret;
+  Assert( n.getKind()!=BOUND_VARIABLE );
   Trace("term-db-eval") << "evaluate term : " << n << std::endl;
-  if( qy->hasTerm( n ) ){
-    Trace("term-db-eval") << "...exists in ee, return rep " << std::endl;
-    ret = qy->getRepresentative( n );
-  }else if( n.getKind()==BOUND_VARIABLE ){
-    if( hasSubs ){
-      Assert( subs.find( n )!=subs.end() );
-      Trace("term-db-eval") << "...substitution is : " << subs[n] << std::endl;
-      if( subsRep ){
-        Assert( qy->hasTerm( subs[n] ) );
-        Assert( qy->getRepresentative( subs[n] )==subs[n] );
-        ret = subs[n];
-      }else{
-        ret = evaluateTerm2( subs[n], subs, subsRep, hasSubs, visited, qy );
-      }
-    }
-  }else if( n.getKind()==FORALL ){
-    ret = n;
-  }else{
-    if( n.hasOperator() ){
+  Node ret;
+  if( !qy->hasTerm( n ) ){
+    //term is not known to be equal to a representative in equality engine, evaluate it
+    if( n.getKind()==FORALL ){
+      ret = Node::null();
+    }else if( n.hasOperator() ){
       TNode f = getMatchOperator( n );
       std::vector< TNode > args;
       bool ret_set = false;
       for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        TNode c = evaluateTerm2( n[i], subs, subsRep, hasSubs, visited, qy );
+        TNode c = evaluateTerm2( n[i], visited, qy );
         if( c.isNull() ){
-          ret = TNode::null();
+          ret = Node::null();
           ret_set = true;
           break;
+        }else if( c==d_true || c==d_false ){
+          //short-circuiting
+          if( ( n.getKind()==kind::AND && c==d_false ) || ( n.getKind()==kind::OR && c==d_true ) ){
+            ret = c;
+            ret_set = true;
+            break;
+          }else if( n.getKind()==kind::ITE && i==0 ){
+            ret = evaluateTerm2( n[ c==d_true ? 1 : 2], visited, qy ); 
+            ret_set = true;
+            break;
+          }
         }
-        Trace("term-db-eval") << "Child " << i << " : " << c << std::endl;
-        //short-circuit and/or
-        if( ( n.getKind()==kind::AND && c==d_false ) || ( n.getKind()==kind::OR && c==d_true ) ){
-          ret = c;
-          ret_set = true;
-          break;
-        }else{
-          args.push_back( c );
-        }
+        Trace("term-db-eval") << "  child " << i << " : " << c << std::endl;
+        args.push_back( c );
       }
       if( !ret_set ){
+        //if it is an indexed term, return the congruent term
         if( !f.isNull() ){
-          Trace("term-db-eval") << "Get term from DB" << std::endl;
-          TNode nn = d_func_map_trie[f].existsTerm( args );
-          Trace("term-db-eval") << "Got term " << nn << std::endl;
-          if( !nn.isNull() && qy->hasTerm( nn ) ){
-            Trace("term-db-eval") << "return rep " << std::endl;
+          TNode nn = qy->getCongruentTerm( f, args );
+          Trace("term-db-eval") << "  got congruent term " << nn << " from DB for " << n << std::endl;
+          if( !nn.isNull() ){
             ret = qy->getRepresentative( nn );
+            Trace("term-db-eval") << "return rep" << std::endl;
             ret_set = true;
+            Assert( !ret.isNull() );
           }
         }
         if( !ret_set ){
+          Trace("term-db-eval") << "return rewrite" << std::endl;
           //a theory symbol or a new UF term
           if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
             args.insert( args.begin(), n.getOperator() );
@@ -275,6 +267,9 @@ Node TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRe
         }
       }
     }
+  }else{
+    Trace("term-db-eval") << "...exists in ee, return rep" << std::endl;
+    ret = qy->getRepresentative( n );
   }
   Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret << std::endl;
   visited[n] = ret;
@@ -282,22 +277,28 @@ Node TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRe
 }
 
 
-TNode TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ) {
+TNode TermDb::getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ) {
   Assert( !qy->extendsEngine() );
-  Trace("term-db-eval") << "evaluate term : " << n << std::endl;
+  Trace("term-db-entail") << "get entailed term : " << n << std::endl;
   if( qy->getEngine()->hasTerm( n ) ){
-    Trace("term-db-eval") << "...exists in ee, return rep " << std::endl;
+    Trace("term-db-entail") << "...exists in ee, return rep " << std::endl;
     return n;
   }else if( n.getKind()==BOUND_VARIABLE ){
     if( hasSubs ){
       Assert( subs.find( n )!=subs.end() );
-      Trace("term-db-eval") << "...substitution is : " << subs[n] << std::endl;
+      Trace("term-db-entail") << "...substitution is : " << subs[n] << std::endl;
       if( subsRep ){
         Assert( qy->getEngine()->hasTerm( subs[n] ) );
         Assert( qy->getEngine()->getRepresentative( subs[n] )==subs[n] );
         return subs[n];
       }else{
-        return evaluateTerm2( subs[n], subs, subsRep, hasSubs, qy );
+        return getEntailedTerm2( subs[n], subs, subsRep, hasSubs, qy );
+      }
+    }
+  }else if( n.getKind()==ITE ){
+    for( unsigned i=0; i<2; i++ ){
+      if( isEntailed2( n[0], subs, subsRep, hasSubs, i==0, qy ) ){
+        return getEntailedTerm2( n[ i==0 ? 1 : 2 ], subs, subsRep, hasSubs, qy );
       }
     }
   }else{
@@ -306,17 +307,16 @@ TNode TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsR
       if( !f.isNull() ){
         std::vector< TNode > args;
         for( unsigned i=0; i<n.getNumChildren(); i++ ){
-          TNode c = evaluateTerm2( n[i], subs, subsRep, hasSubs, qy );
+          TNode c = getEntailedTerm2( n[i], subs, subsRep, hasSubs, qy );
           if( c.isNull() ){
             return TNode::null();
           }
           c = qy->getEngine()->getRepresentative( c );
-          Trace("term-db-eval") << "Got child : " << c << std::endl;
+          Trace("term-db-entail") << "  child " << i << " : " << c << std::endl;
           args.push_back( c );
         }
-        Trace("term-db-eval") << "Get term from DB" << std::endl;
-        TNode nn = d_func_map_trie[f].existsTerm( args );
-        Trace("term-db-eval") << "Got term " << nn << std::endl;
+        TNode nn = qy->getCongruentTerm( f, args );
+        Trace("term-db-entail") << "  got congruent term " << nn << " for " << n << std::endl;
         return nn;
       }
     }
@@ -324,39 +324,37 @@ TNode TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsR
   return TNode::null();
 }
 
-Node TermDb::evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool mkNewTerms, EqualityQuery * qy ) {
+Node TermDb::evaluateTerm( TNode n, EqualityQuery * qy ) {
   if( qy==NULL ){
     qy = d_quantEngine->getEqualityQuery();
   }
-  if( mkNewTerms ){
-    std::map< TNode, Node > visited;
-    return evaluateTerm2( n, subs, subsRep, true, visited, qy );
-  }else{
-    return evaluateTerm2( n, subs, subsRep, true, qy );
+  std::map< TNode, Node > visited;
+  return evaluateTerm2( n, visited, qy );
+}
+
+TNode TermDb::getEntailedTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, EqualityQuery * qy ) {
+  if( qy==NULL ){
+    qy = d_quantEngine->getEqualityQuery();
   }
+  return getEntailedTerm2( n, subs, subsRep, true, qy );
 }
 
-Node TermDb::evaluateTerm( TNode n, bool mkNewTerms, EqualityQuery * qy ) {
+TNode TermDb::getEntailedTerm( TNode n, EqualityQuery * qy ) {
   if( qy==NULL ){
     qy = d_quantEngine->getEqualityQuery();
   }
   std::map< TNode, TNode > subs;
-  if( mkNewTerms ){
-    std::map< TNode, Node > visited;
-    return evaluateTerm2( n, subs, false, false, visited, qy );
-  }else{
-    return evaluateTerm2( n, subs, false, false, qy );
-  }
+  return getEntailedTerm2( n, subs, false, false, qy );
 }
 
-bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy ) {
+bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy ) {
   Assert( !qy->extendsEngine() );
-  Trace("term-db-eval") << "Check entailed : " << n << ", pol = " << pol << std::endl;
+  Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol << std::endl;
   Assert( n.getType().isBoolean() );
   if( n.getKind()==EQUAL ){
-    TNode n1 = evaluateTerm2( n[0], subs, subsRep, hasSubs, qy );
+    TNode n1 = getEntailedTerm2( n[0], subs, subsRep, hasSubs, qy );
     if( !n1.isNull() ){
-      TNode n2 = evaluateTerm2( n[1], subs, subsRep, hasSubs, qy );
+      TNode n2 = getEntailedTerm2( n[1], subs, subsRep, hasSubs, qy );
       if( !n2.isNull() ){
         if( n1==n2 ){
           return pol;
@@ -372,11 +370,11 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep,
       }
     }
   }else if( n.getKind()==NOT ){
-    return isEntailed( n[0], subs, subsRep, hasSubs, !pol, qy );
+    return isEntailed2( n[0], subs, subsRep, hasSubs, !pol, qy );
   }else if( n.getKind()==OR || n.getKind()==AND ){
     bool simPol = ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND );
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if( isEntailed( n[i], subs, subsRep, hasSubs, pol, qy ) ){
+      if( isEntailed2( n[i], subs, subsRep, hasSubs, pol, qy ) ){
         if( simPol ){
           return true;
         }
@@ -389,14 +387,14 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep,
     return !simPol;
   }else if( n.getKind()==IFF || n.getKind()==ITE ){
     for( unsigned i=0; i<2; i++ ){
-      if( isEntailed( n[0], subs, subsRep, hasSubs, i==0, qy ) ){
+      if( isEntailed2( n[0], subs, subsRep, hasSubs, i==0, qy ) ){
         unsigned ch = ( n.getKind()==IFF || i==0 ) ? 1 : 2;
         bool reqPol = ( n.getKind()==ITE || i==0 ) ? pol : !pol;
-        return isEntailed( n[ch], subs, subsRep, hasSubs, reqPol, qy );
+        return isEntailed2( n[ch], subs, subsRep, hasSubs, reqPol, qy );
       }
     }
   }else if( n.getKind()==APPLY_UF ){
-    TNode n1 = evaluateTerm2( n, subs, subsRep, hasSubs, qy );
+    TNode n1 = getEntailedTerm2( n, subs, subsRep, hasSubs, qy );
     if( !n1.isNull() ){
       Assert( qy->hasTerm( n1 ) );
       if( n1==d_true ){
@@ -411,16 +409,21 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep,
   return false;
 }
 
-bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy ) {
+bool TermDb::isEntailed( TNode n, bool pol, EqualityQuery * qy ) {
   if( qy==NULL ){
+    Assert( d_consistent_ee );
     qy = d_quantEngine->getEqualityQuery();
   }
-  if( d_consistent_ee ){
-    return isEntailed( n, subs, subsRep, true, pol, qy );
-  }else{
-    //don't check entailment wrt an inconsistent ee
-    return false;
+  std::map< TNode, TNode > subs;
+  return isEntailed2( n, subs, false, false, pol, qy );
+}
+
+bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy ) {
+  if( qy==NULL ){
+    Assert( d_consistent_ee );
+    qy = d_quantEngine->getEqualityQuery();
   }
+  return isEntailed2( n, subs, subsRep, true, pol, qy );
 }
 
 bool TermDb::hasTermCurrent( Node n, bool useMode ) {
@@ -571,7 +574,13 @@ bool TermDb::reset( Theory::Effort effort ){
       }
     }
   }
-
+  //explicitly add inst closure terms to the equality engine to ensure only EE terms are indexed
+  for( std::hash_set< Node, NodeHashFunction >::iterator it = d_iclosure_processed.begin(); it !=d_iclosure_processed.end(); ++it ){
+    Node n = *it;
+    if( !ee->hasTerm( n ) ){
+      ee->addTerm( n );
+    }
+  }
 
   //rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms
   for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){
@@ -579,8 +588,8 @@ bool TermDb::reset( Theory::Effort effort ){
     Trace("term-db-debug") << "Adding terms for operator " << it->first << std::endl;
     for( unsigned i=0; i<it->second.size(); i++ ){
       Node n = it->second[i];
-      //to be added to term index, term must be relevant, and either exist in EE or be an inst closure term
-      if( hasTermCurrent( n ) && ( ee->hasTerm( n ) || d_iclosure_processed.find( n )!=d_iclosure_processed.end() ) ){
+      //to be added to term index, term must be relevant, and exist in EE
+      if( hasTermCurrent( n ) && ee->hasTerm( n ) ){
         if( !n.getAttribute(NoMatchAttribute()) ){
           if( options::finiteModelFind() ){
             computeModelBasisArgAttribute( n );
@@ -681,11 +690,15 @@ TermArgTrie * TermDb::getTermArgTrie( Node eqc, Node f ) {
   }
 }
 
-TNode TermDb::existsTerm( Node f, Node n ) {
+TNode TermDb::getCongruentTerm( Node f, Node n ) {
   computeArgReps( n );
   return d_func_map_trie[f].existsTerm( d_arg_reps[n] );
 }
 
+TNode TermDb::getCongruentTerm( Node f, std::vector< TNode >& args ) {
+  return d_func_map_trie[f].existsTerm( args );
+}
+
 Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
   if( d_model_basis_term.find( tn )==d_model_basis_term.end() ){
     Node mbt;
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 9177d3a1a..76bd623a8 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -164,7 +164,7 @@ namespace fmcheck {
 
 class TermDbSygus;
 
-class TermDb {
+class TermDb : public QuantifiersUtil {
   friend class ::CVC4::theory::QuantifiersEngine;
   friend class ::CVC4::theory::inst::Trigger;
   friend class ::CVC4::theory::quantifiers::fmcheck::FullModelChecker;
@@ -183,9 +183,9 @@ private:
   /** set has term */
   void setHasTerm( Node n );
   /** evaluate term */
-  TNode evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy );
-  Node evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, std::map< TNode, Node >& visited, EqualityQuery * qy );
-  bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy );
+  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(){}
@@ -224,13 +224,16 @@ public:
   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 */
   TermArgTrie * getTermArgTrie( Node f );
   TermArgTrie * getTermArgTrie( Node eqc, Node f );
   /** exists term */
-  TNode existsTerm( Node f, Node n );
+  TNode getCongruentTerm( Node f, Node n );
+  TNode getCongruentTerm( Node f, std::vector< TNode >& args );
   /** compute arg reps */
   void computeArgReps( TNode n );
   /** compute uf eqc terms */
@@ -238,10 +241,12 @@ public:
   /** evaluate a term under a substitution.  Return representative in EE if possible.
    * subsRep is whether subs contains only representatives
    */
-  Node evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool mkNewTerms = false, EqualityQuery * qy = NULL );
-  /** same as above, but without substitution */
-  Node evaluateTerm( TNode n, bool mkNewTerms = false, EqualityQuery * qy = NULL );
+  Node evaluateTerm( TNode n, EqualityQuery * qy = NULL );
+  /** get entailed term, does not construct new terms, less aggressive */
+  TNode getEntailedTerm( TNode n, EqualityQuery * qy = NULL );
+  TNode getEntailedTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, EqualityQuery * qy = NULL );
   /** is entailed (incomplete check) */
+  bool isEntailed( TNode n, bool pol, EqualityQuery * qy = NULL );
   bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy = NULL );
   /** has term */
   bool hasTermCurrent( Node n, bool useMode = true );
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index d31865f35..839077a40 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -42,6 +42,7 @@
 #include "theory/quantifiers/quant_split.h"
 #include "theory/quantifiers/anti_skolem.h"
 #include "theory/quantifiers/equality_infer.h"
+#include "theory/quantifiers/inst_propagator.h"
 #include "theory/theory_engine.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf.h"
@@ -54,37 +55,6 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::inst;
 
-unsigned QuantifiersModule::needsModel( Theory::Effort e ) {
-  return QuantifiersEngine::QEFFORT_NONE;
-}
-
-eq::EqualityEngine * QuantifiersModule::getEqualityEngine() {
-  return d_quantEngine->getMasterEqualityEngine();
-}
-
-bool QuantifiersModule::areEqual( TNode n1, TNode n2 ) {
-  eq::EqualityEngine * ee = getEqualityEngine();
-  return n1==n2 || ( ee->hasTerm( n1 ) && ee->hasTerm( n2 ) && ee->areEqual( n1, n2 ) );
-}
-
-bool QuantifiersModule::areDisequal( TNode n1, TNode n2 ) {
-  eq::EqualityEngine * ee = getEqualityEngine();
-  return n1!=n2 && ee->hasTerm( n1 ) && ee->hasTerm( n2 ) && ee->areDisequal( n1, n2, false );
-}
-
-TNode QuantifiersModule::getRepresentative( TNode n ) {
-  eq::EqualityEngine * ee = getEqualityEngine();
-  if( ee->hasTerm( n ) ){
-    return ee->getRepresentative( n );
-  }else{
-    return n;
-  }
-}
-
-quantifiers::TermDb * QuantifiersModule::getTermDatabase() {
-  return d_quantEngine->getTermDatabase();
-}
-
 QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te):
     d_te( te ),
     d_lemmas_produced_c(u),
@@ -98,8 +68,21 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
     d_presolve_cache(u),
     d_presolve_cache_wq(u),
     d_presolve_cache_wic(u){
+  //utilities
   d_eq_query = new EqualityQueryQuantifiersEngine( c, this );
+  d_util.push_back( d_eq_query );
+  
   d_term_db = new quantifiers::TermDb( c, u, this );
+  d_util.push_back( d_term_db );
+  
+  if( options::instPropagate() ){
+    d_inst_prop = new quantifiers::InstPropagator( this );
+    d_util.push_back( d_inst_prop );
+    d_inst_notify.push_back( d_inst_prop->getInstantiationNotify() );
+  }else{
+    d_inst_prop = NULL;
+  }
+
   d_tr_trie = new inst::TriggerTrie;
   d_hasAddedLemma = false;
   //don't add true lemma
@@ -183,6 +166,7 @@ QuantifiersEngine::~QuantifiersEngine(){
   delete d_i_cbqi;
   delete d_qsplit;
   delete d_anti_skolem;
+  delete d_inst_prop;
 }
 
 EqualityQueryQuantifiersEngine* QuantifiersEngine::getEqualityQuery() {
@@ -288,6 +272,7 @@ void QuantifiersEngine::finishInit(){
 
   if( needsRelDom ){
     d_rel_dom = new quantifiers::RelevantDomain( this, d_model );
+    d_util.push_back( d_rel_dom );
   }
 
   if( needsBuilder ){
@@ -389,6 +374,12 @@ void QuantifiersEngine::check( Theory::Effort e ){
 
   Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e << ", needsCheck=" << needsCheck << std::endl;
   if( needsCheck ){
+    //flush previous lemmas (for instance, if was interupted), or other lemmas to process
+    flushLemmas();
+    if( d_hasAddedLemma ){
+      return;
+    }
+    
     if( Trace.isOn("quant-engine-debug") ){
       Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e << std::endl;
       Trace("quant-engine-debug") << "  depth : " << d_ierCounter_c << std::endl;
@@ -405,44 +396,38 @@ void QuantifiersEngine::check( Theory::Effort e ){
       Trace("quant-engine-debug") << "  Needs model effort : " << needsModelE << std::endl;
       Trace("quant-engine-debug") << "Resetting all modules..." << std::endl;
     }
-
-    //reset relevant information
-
-    //flush previous lemmas (for instance, if was interupted), or other lemmas to process
-    flushLemmas();
-    if( d_hasAddedLemma ){
-      return;
-    }
-
     if( Trace.isOn("quant-engine-ee-pre") ){
       Trace("quant-engine-ee-pre") << "Equality engine (pre-inference): " << std::endl;
       debugPrintEqualityEngine( "quant-engine-ee-pre" );
     }
-    Trace("quant-engine-debug2") << "Reset equality engine..." << std::endl;
-    if( !d_eq_query->reset( e ) ){
-      flushLemmas();
-      return;
-    }
-    
     if( Trace.isOn("quant-engine-assert") ){
       Trace("quant-engine-assert") << "Assertions : " << std::endl;
       getTheoryEngine()->printAssertions("quant-engine-assert");
     }
+    
+    //reset utilities
+    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 ) ){
+        flushLemmas();
+        if( d_hasAddedLemma ){
+          return;
+        }else{
+          //should only fail reset if added a lemma
+          Assert( false );
+        }
+      }
+    }
+
     if( Trace.isOn("quant-engine-ee") ){
       Trace("quant-engine-ee") << "Equality engine : " << std::endl;
       debugPrintEqualityEngine( "quant-engine-ee" );
     }
-    
-    Trace("quant-engine-debug2") << "Reset term database..." << std::endl;
-    if( !d_term_db->reset( e ) ){
-      flushLemmas();
-      return;
-    }
-    if( d_rel_dom ){
-      d_rel_dom->reset();
-    }
+
+    //reset the model
     d_model->reset_round();
     
+    //reset the modules
     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 );
@@ -1007,6 +992,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
   
   //check for positive entailment
   if( options::instNoEntail() ){
+    //TODO: check consistency of equality engine (if not aborting on utility's reset)
     std::map< TNode, TNode > subs;
     for( unsigned i=0; i<terms.size(); i++ ){
       subs[q[0][i]] = terms[i];
@@ -1069,9 +1055,11 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
       }
       setInstantiationLevelAttr( body, q[1], maxInstLevel+1 );
     }
-    //notify listeners
-    for( unsigned j=0; j<d_inst_notify.size(); j++ ){
-      d_inst_notify[j]->notifyInstantiation( q, lem, terms, body );
+    if( d_curr_effort_level>QEFFORT_CONFLICT ){
+      //notify listeners
+      for( unsigned j=0; j<d_inst_notify.size(); j++ ){
+        d_inst_notify[j]->notifyInstantiation( d_curr_effort_level, q, lem, terms, body );
+      }
     }
     Trace("inst-add-debug") << " -> Success." << std::endl;
     ++(d_statistics.d_instantiations);
@@ -1571,6 +1559,10 @@ void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< N
   Assert( std::find( eqc.begin(), eqc.end(), a )!=eqc.end() );
 }
 
+TNode EqualityQueryQuantifiersEngine::getCongruentTerm( Node f, std::vector< TNode >& args ) {
+  return d_qe->getTermDatabase()->getCongruentTerm( f, args );
+}
+
 //helper functions
 
 Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache ){
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index cdf7c3b89..9ee967eb0 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -44,47 +44,10 @@ namespace quantifiers {
   class TermDbSygus;
 }
 
-class QuantifiersModule {
-protected:
-  QuantifiersEngine* d_quantEngine;
-public:
-  QuantifiersModule( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
-  virtual ~QuantifiersModule(){}
-  //get quantifiers engine
-  QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; }
-  /** presolve */
-  virtual void presolve() {}
-  /* whether this module needs to check this round */
-  virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; }
-  /* whether this module needs a model built */
-  virtual unsigned needsModel( Theory::Effort e );
-  /* reset at a round */
-  virtual void reset_round( Theory::Effort e ){}
-  /* Call during quantifier engine's check */
-  virtual void check( Theory::Effort e, unsigned quant_e ) = 0;
-  /* check was complete (e.g. no lemmas implies a model) */
-  virtual bool checkComplete() { return true; }
-  /* Called for new quantified formulas */
-  virtual void preRegisterQuantifier( Node q ) { }
-  /* Called for new quantifiers after owners are finalized */
-  virtual void registerQuantifier( Node q ) = 0;
-  virtual void assertNode( Node n ) {}
-  virtual void propagate( Theory::Effort level ){}
-  virtual Node getNextDecisionRequest() { return TNode::null(); }
-  /** Identify this module (for debugging, dynamic configuration, etc..) */
-  virtual std::string identify() const = 0;
-public:
-  eq::EqualityEngine * getEqualityEngine();
-  bool areDisequal( TNode n1, TNode n2 );
-  bool areEqual( TNode n1, TNode n2 );
-  TNode getRepresentative( TNode n );
-  quantifiers::TermDb * getTermDatabase();
-};/* class QuantifiersModule */
-
 class InstantiationNotify {
 public:
   InstantiationNotify(){}
-  virtual void notifyInstantiation( Node q, Node lem, std::vector< Node >& terms, Node body ) = 0;
+  virtual void notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) = 0;
 };
 
 namespace quantifiers {
@@ -109,6 +72,7 @@ namespace quantifiers {
   class QuantDSplit;
   class QuantAntiSkolem;
   class EqualityInference;
+  class InstPropagator;
 }/* CVC4::theory::quantifiers */
 
 namespace inst {
@@ -132,6 +96,8 @@ class QuantifiersEngine {
 private:
   /** reference to theory engine object */
   TheoryEngine* d_te;
+  /** vector of utilities for quantifiers */
+  std::vector< QuantifiersUtil* > d_util;
   /** vector of modules for quantifiers */
   std::vector< QuantifiersModule* > d_modules;
   /** instantiation notify */
@@ -174,6 +140,8 @@ private:
   quantifiers::QuantDSplit * d_qsplit;
   /** quantifiers anti-skolemization */
   quantifiers::QuantAntiSkolem * d_anti_skolem;
+  /** quantifiers instantiation propagtor */
+  quantifiers::InstPropagator * d_inst_prop;
 public: //effort levels
   enum {
     QEFFORT_CONFLICT,
@@ -427,11 +395,15 @@ private:
   Node getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache );
   /** get score */
   int getRepScore( Node n, Node f, int index, TypeNode v_tn );
+  /** flatten representatives */
+  void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps );
 public:
   EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe );
   virtual ~EqualityQueryQuantifiersEngine();
   /** reset */
   bool reset( Theory::Effort e );
+  /** identify */
+  std::string identify() const { return "EqualityQueryQE"; }
   /** general queries about equality */
   bool hasTerm( Node a );
   Node getRepresentative( Node a );
@@ -439,13 +411,12 @@ public:
   bool areDisequal( Node a, Node b );
   eq::EqualityEngine* getEngine();
   void getEquivalenceClass( Node a, std::vector< Node >& eqc );
+  TNode getCongruentTerm( Node f, std::vector< TNode >& args );
   /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria.
       If cbqi is active, this will return a term in the equivalence class of "a" that does
       not contain instantiation constants, if such a term exists.
    */
   Node getInternalRepresentative( Node a, Node f, int index );
-  /** flatten representatives */
-  void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps );
   /** get quantifiers equality inference */
   quantifiers::EqualityInference * getEqualityInference() { return d_eq_inference; }
 }; /* EqualityQueryQuantifiersEngine */