From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 13 Oct 2014 10:11:09 +0000 (+0200)
Subject: Refactor model builder from model engine to quant engine.  Work on fairness strategy... 
X-Git-Tag: cvc5-1.0.0~6567
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c3992de261f0fa968f50349de1bdc3f9bef6ce6b;p=cvc5.git

Refactor model builder from model engine to quant engine.  Work on fairness strategy for CEGQI.  Add option for single/multi triggers.  Minor cleanup.
---

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index f4cdd1a60..babfe3f40 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -27,7 +27,8 @@ using namespace std;
 
 namespace CVC4 {
 
-CegInstantiation::CegConjecture::CegConjecture() {
+CegInstantiation::CegConjecture::CegConjecture( context::Context* c ) : d_active( c, false ), d_infeasible( c, false ), d_curr_lit( c, 0 ){
+
 }
 
 void CegInstantiation::CegConjecture::assign( Node q ) {
@@ -38,6 +39,7 @@ void CegInstantiation::CegConjecture::assign( Node q ) {
     d_candidates.push_back( NodeManager::currentNM()->mkSkolem( "e", q[0][i].getType() ) );
   }
 }
+
 void CegInstantiation::CegConjecture::initializeGuard( QuantifiersEngine * qe ){
   if( d_guard.isNull() ){
     d_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) );
@@ -47,8 +49,25 @@ void CegInstantiation::CegConjecture::initializeGuard( QuantifiersEngine * qe ){
   }
 }
 
-CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ), d_conj_active( c, false ), d_conj_infeasible( c, false ), d_guard_assertions( c ) {
+Node CegInstantiation::CegConjecture::getLiteral( QuantifiersEngine * qe, int i ) {
+  std::map< int, Node >::iterator it = d_lits.find( i );
+  if( it==d_lits.end() ){
+    Node lit = NodeManager::currentNM()->mkNode( LEQ, d_measure_term, NodeManager::currentNM()->mkConst( Rational( i + d_measure_term_size ) ) );
+    lit = Rewriter::rewrite( lit );
+    d_lits[i] = lit;
+
+    Node lem = NodeManager::currentNM()->mkNode( kind::OR, lit, lit.negate() );
+    Trace("cegqi-lemma") << "Fairness split : " << lem << std::endl;
+    qe->getOutputChannel().lemma( lem );
+    qe->getOutputChannel().requirePhase( lit, true );
+    return lit;
+  }else{
+    return it->second;
+  }
+}
 
+CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ){
+  d_conj = new CegConjecture( d_quantEngine->getSatContext() );
 }
 
 bool CegInstantiation::needsCheck( Theory::Effort e ) {
@@ -58,9 +77,10 @@ bool CegInstantiation::needsCheck( Theory::Effort e ) {
 void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) {
   if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
     Trace("cegqi-engine") << "---Countexample Guided Instantiation Engine---" << std::endl;
-    Trace("cegqi-debug") << "Current conjecture status : " << d_conj_active << " " << d_conj_infeasible << std::endl;
-    if( d_conj_active && !d_conj_infeasible ){
-      checkCegConjecture( &d_conj );
+    Trace("cegqi-engine-debug") << std::endl;
+    Trace("cegqi-engine-debug") << "Current conjecture status : active : " << d_conj->d_active << " feasible : " << !d_conj->d_infeasible << std::endl;
+    if( d_conj->d_active && !d_conj->d_infeasible ){
+      checkCegConjecture( d_conj );
     }
     Trace("cegqi-engine") << "Finished Countexample Guided Instantiation engine." << std::endl;
   }
@@ -68,24 +88,44 @@ void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) {
 
 void CegInstantiation::registerQuantifier( Node q ) {
   if( d_quantEngine->getOwner( q )==this ){
-    if( !d_conj.isAssigned() ){
+    if( !d_conj->isAssigned() ){
       Trace("cegqi") << "Register conjecture : " << q << std::endl;
-      d_conj.assign( q );
+      d_conj->assign( q );
       //construct base instantiation
-      d_conj.d_base_inst = Rewriter::rewrite( d_quantEngine->getInstantiation( q, d_conj.d_candidates ) );
-      Trace("cegqi") << "Base instantiation is : " << d_conj.d_base_inst << std::endl;
+      d_conj->d_base_inst = Rewriter::rewrite( d_quantEngine->getInstantiation( q, d_conj->d_candidates ) );
+      Trace("cegqi") << "Base instantiation is : " << d_conj->d_base_inst << std::endl;
       if( getTermDatabase()->isQAttrSygus( q ) ){
-        Assert( d_conj.d_base_inst.getKind()==NOT );
-        Assert( d_conj.d_base_inst[0].getKind()==FORALL );
-        for( unsigned j=0; j<d_conj.d_base_inst[0][0].getNumChildren(); j++ ){
-          d_conj.d_inner_vars.push_back( d_conj.d_base_inst[0][0][j] );
+        Assert( d_conj->d_base_inst.getKind()==NOT );
+        Assert( d_conj->d_base_inst[0].getKind()==FORALL );
+        for( unsigned j=0; j<d_conj->d_base_inst[0][0].getNumChildren(); j++ ){
+          d_conj->d_inner_vars.push_back( d_conj->d_base_inst[0][0][j] );
         }
       }else if( getTermDatabase()->isQAttrSynthesis( q ) ){
         //add immediate lemma
-        Node lem = NodeManager::currentNM()->mkNode( OR, d_conj.d_guard.negate(), d_conj.d_base_inst );
+        Node lem = NodeManager::currentNM()->mkNode( OR, d_conj->d_guard.negate(), d_conj->d_base_inst );
+        d_quantEngine->getOutputChannel().lemma( lem );
+      }
+      //fairness
+      std::vector< Node > mc;
+      for( unsigned j=0; j<d_conj->d_candidates.size(); j++ ){
+        TypeNode tn = d_conj->d_candidates[j].getType();
+        registerMeasuredType( tn );
+        std::map< TypeNode, Node >::iterator it = d_uf_measure.find( tn );
+        if( it!=d_uf_measure.end() ){
+          mc.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, it->second, d_conj->d_candidates[j] ) );
+        }
+      }
+      if( !mc.empty() ){
+        d_conj->d_measure_term = mc.size()==1 ? mc[0] : NodeManager::currentNM()->mkNode( PLUS, mc );
+        d_conj->d_measure_term_size = mc.size();
+        Trace("cegqi") << "Measure term is : " << d_conj->d_measure_term << std::endl;
+        //Node ax = NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkConst( Rational(0) ), d_conj->d_measure_term );
+        //ax = Rewriter::rewrite( ax );
+        //Trace("cegqi-lemma") << "Fairness non-negative axiom : " << ax << std::endl;
+        //d_quantEngine->getOutputChannel().lemma( ax );
       }
     }else{
-      Assert( d_conj.d_quant==q );
+      Assert( d_conj->d_quant==q );
     }
   }
 }
@@ -94,83 +134,113 @@ void CegInstantiation::assertNode( Node n ) {
   Trace("cegqi-debug") << "Cegqi : Assert : " << n << std::endl;
   bool pol = n.getKind()!=NOT;
   Node lit = n.getKind()==NOT ? n[0] : n;
-  if( lit==d_conj.d_guard ){
-    d_guard_assertions[lit] = pol;
-    d_conj_infeasible = !pol;
+  if( lit==d_conj->d_guard ){
+    //d_guard_assertions[lit] = pol;
+    d_conj->d_infeasible = !pol;
   }
-  if( lit==d_conj.d_quant ){
-    d_conj_active = true;
+  if( lit==d_conj->d_quant ){
+    d_conj->d_active = true;
   }
 }
 
 Node CegInstantiation::getNextDecisionRequest() {
-  d_conj.initializeGuard( d_quantEngine );
+  d_conj->initializeGuard( d_quantEngine );
   bool value;
-  if( !d_quantEngine->getValuation().hasSatValue( d_conj.d_guard, value ) ) {
-    if( d_guard_assertions.find( d_conj.d_guard )==d_guard_assertions.end() ){
-      if( d_conj.d_guard_split.isNull() ){
-        Node lem = NodeManager::currentNM()->mkNode( OR, d_conj.d_guard.negate(), d_conj.d_guard );
-        d_quantEngine->getOutputChannel().lemma( lem );
+  if( !d_quantEngine->getValuation().hasSatValue( d_conj->d_guard, value ) ) {
+    if( d_conj->d_guard_split.isNull() ){
+      Node lem = NodeManager::currentNM()->mkNode( OR, d_conj->d_guard.negate(), d_conj->d_guard );
+      d_quantEngine->getOutputChannel().lemma( lem );
+    }
+    Trace("cegqi-debug") << "CEGQI : Decide next on : " << d_conj->d_guard << "..." << std::endl;
+    return d_conj->d_guard;
+  }
+  //enforce fairness
+  if( d_conj->isAssigned() ){
+    Node lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() );
+    if( d_quantEngine->getValuation().hasSatValue( lit, value ) ) {
+      if( !value ){
+        d_conj->d_curr_lit.set( d_conj->d_curr_lit.get() + 1 );
+        lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() );
+        Trace("cegqi-debug") << "CEGQI : Decide on next lit : " << lit << "..." << std::endl;
+        return lit;
       }
-      Trace("cegqi-debug") << "Decide next on : " << d_conj.d_guard << "..." << std::endl;
-      return d_conj.d_guard;
+    }else{
+      Trace("cegqi-debug") << "CEGQI : Decide on current lit : " << lit << "..." << std::endl;
+      return lit;
     }
   }
+
   return Node::null();
 }
 
 void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
   Node q = conj->d_quant;
-  Trace("cegqi-engine-debug") << "Synthesis conjecture : " << q << std::endl;
-  Trace("cegqi-engine-debug") << "  * Candidate program/output : ";
+  Trace("cegqi-engine") << "Synthesis conjecture : " << q << std::endl;
+  Trace("cegqi-engine") << "  * Candidate program/output symbol : ";
   for( unsigned i=0; i<conj->d_candidates.size(); i++ ){
-    Trace("cegqi-engine-debug") << conj->d_candidates[i] << " ";
+    Trace("cegqi-engine") << conj->d_candidates[i] << " ";
   }
-  Trace("cegqi-engine-debug") << std::endl;
-
-  if( getTermDatabase()->isQAttrSygus( q ) ){
-    Trace("cegqi-engine-debug") << "  * Values are : ";
-    bool success = true;
-    std::vector< Node > model_values;
-    for( unsigned i=0; i<conj->d_candidates.size(); i++ ){
-      Node v = getModelValue( conj->d_candidates[i] );
-      model_values.push_back( v );
-      Trace("cegqi-engine-debug") << v << " ";
-      if( v.isNull() ){
-        success = false;
+  Trace("cegqi-engine") << std::endl;
+
+  if( conj->d_ce_sk.empty() ){
+    Trace("cegqi-engine") << "  *** Check candidate phase..." << std::endl;
+    if( getTermDatabase()->isQAttrSygus( q ) ){
+
+      std::vector< Node > model_values;
+      if( getModelValues( conj->d_candidates, model_values ) ){
+        //must get a counterexample to the value of the current candidate
+        Node inst = conj->d_base_inst.substitute( conj->d_candidates.begin(), conj->d_candidates.end(), model_values.begin(), model_values.end() );
+        inst = Rewriter::rewrite( inst );
+        //body should be an existential
+        Assert( inst.getKind()==NOT );
+        Assert( inst[0].getKind()==FORALL );
+        //immediately skolemize
+        Node inst_sk = getTermDatabase()->getSkolemizedBody( inst[0] );
+        Trace("cegqi-lemma") << "Counterexample lemma : " << inst_sk << std::endl;
+        d_quantEngine->addLemma( NodeManager::currentNM()->mkNode( OR, q.negate(), inst_sk.negate() ) );
+        conj->d_ce_sk.push_back( inst[0] );
       }
-    }
-    Trace("cegqi-engine-debug") << std::endl;
 
-    if( success ){
-      //must get a counterexample to the value of the current candidate
-      Node inst = conj->d_base_inst.substitute( conj->d_candidates.begin(), conj->d_candidates.end(), model_values.begin(), model_values.end() );
-      inst = Rewriter::rewrite( inst );
-      //body should be an existential
-      Assert( inst.getKind()==NOT );
-      Assert( inst[0].getKind()==FORALL );
-      //immediately skolemize
-      Node inst_sk = getTermDatabase()->getSkolemizedBody( inst[0] );
-      Trace("cegqi-lemma") << "Counterexample lemma : " << inst_sk << std::endl;
-      d_quantEngine->addLemma( NodeManager::currentNM()->mkNode( OR, q.negate(), inst_sk ) );
-
-      //candidate refinement : the next candidate must satisfy the counterexample found for the current model of the candidate
-      Assert( conj->d_inner_vars.size()==getTermDatabase()->d_skolem_constants[inst[0]].size() );
-      Node inst_ce_refine = conj->d_base_inst[0][1].substitute( conj->d_inner_vars.begin(), conj->d_inner_vars.end(),
-                                                                getTermDatabase()->d_skolem_constants[inst[0]].begin(), getTermDatabase()->d_skolem_constants[inst[0]].end() );
-      Node lem = NodeManager::currentNM()->mkNode( OR, conj->d_guard.negate(), inst_ce_refine.negate() );
-      Trace("cegqi-lemma") << "Candidate refinement lemma : " << lem << std::endl;
-      d_quantEngine->addLemma( lem );
+    }else if( getTermDatabase()->isQAttrSynthesis( q ) ){
+      std::vector< Node > model_terms;
+      for( unsigned i=0; i<conj->d_candidates.size(); i++ ){
+        Node t = getModelTerm( conj->d_candidates[i] );
+        model_terms.push_back( t );
+      }
+      d_quantEngine->addInstantiation( q, model_terms, false );
     }
+  }else{
+    Trace("cegqi-engine") << "  *** Refine candidate phase..." << std::endl;
+    for( unsigned j=0; j<conj->d_ce_sk.size(); j++ ){
+      Node ce_q = conj->d_ce_sk[j];
+      Assert( conj->d_inner_vars.size()==getTermDatabase()->d_skolem_constants[ce_q].size() );
+      std::vector< Node > model_values;
+      if( getModelValues( getTermDatabase()->d_skolem_constants[ce_q], model_values ) ){
+        //candidate refinement : the next candidate must satisfy the counterexample found for the current model of the candidate
+        Node inst_ce_refine = conj->d_base_inst[0][1].substitute( conj->d_inner_vars.begin(), conj->d_inner_vars.end(),
+                                                                  model_values.begin(), model_values.end() );
+        Node lem = NodeManager::currentNM()->mkNode( OR, conj->d_guard.negate(), inst_ce_refine );
+        Trace("cegqi-lemma") << "Candidate refinement lemma : " << lem << std::endl;
+        d_quantEngine->addLemma( lem );
+      }
+    }
+    conj->d_ce_sk.clear();
+  }
+}
 
-  }else if( getTermDatabase()->isQAttrSynthesis( q ) ){
-    std::vector< Node > model_terms;
-    for( unsigned i=0; i<conj->d_candidates.size(); i++ ){
-      Node t = getModelTerm( conj->d_candidates[i] );
-      model_terms.push_back( t );
+bool CegInstantiation::getModelValues( std::vector< Node >& n, std::vector< Node >& v ) {
+  bool success = true;
+  Trace("cegqi-engine") << "  * Value is : ";
+  for( unsigned i=0; i<n.size(); i++ ){
+    Node nv = getModelValue( n[i] );
+    v.push_back( nv );
+    Trace("cegqi-engine") << nv << " ";
+    if( nv.isNull() ){
+      success = false;
     }
-    d_quantEngine->addInstantiation( q, model_terms, false );
   }
+  Trace("cegqi-engine") << std::endl;
+  return success;
 }
 
 Node CegInstantiation::getModelValue( Node n ) {
@@ -210,7 +280,52 @@ Node CegInstantiation::getModelValue( Node n ) {
 }
 
 Node CegInstantiation::getModelTerm( Node n ){
+  //TODO
   return getModelValue( n );
 }
 
+void CegInstantiation::registerMeasuredType( TypeNode tn ) {
+  std::map< TypeNode, Node >::iterator it = d_uf_measure.find( tn );
+  if( it==d_uf_measure.end() ){
+    if( tn.isDatatype() ){
+      TypeNode op_tn = NodeManager::currentNM()->mkFunctionType( tn, NodeManager::currentNM()->integerType() );
+      Node op = NodeManager::currentNM()->mkSkolem( "tsize", op_tn, "was created by ceg instantiation to enforce fairness." );
+      d_uf_measure[tn] = op;
+      //cycle through constructors
+      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+      for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+        Node x = NodeManager::currentNM()->mkBoundVar( tn );
+        Node cond = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), x ).negate();
+
+        std::vector< Node > sumc;
+        sumc.push_back( NodeManager::currentNM()->mkConst( Rational(1) ) );
+        for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
+          TypeNode tnc = TypeNode::fromType( ((SelectorType)dt[i][j].getSelector().getType()).getRangeType() );
+          if( tnc.isDatatype() ){
+            registerMeasuredType( tnc );
+            sumc.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, d_uf_measure[tnc],
+                                                              NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, dt[i][j].getSelector(), x ) ) );
+          }
+        }
+        Node sum = sumc.size()==1 ? sumc[0] : NodeManager::currentNM()->mkNode( PLUS, sumc );
+        Node eq = NodeManager::currentNM()->mkNode( EQUAL, NodeManager::currentNM()->mkNode( APPLY_UF, d_uf_measure[tn], x ), sum );
+
+        Node ax = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, x ),
+                                                            NodeManager::currentNM()->mkNode( OR, cond, eq ) );
+        ax = Rewriter::rewrite( ax );
+        Trace("cegqi-lemma") << "Fairness axiom : " << ax << std::endl;
+        d_quantEngine->getOutputChannel().lemma( ax );
+      }
+      //all are non-negative
+      Node x = NodeManager::currentNM()->mkBoundVar( tn );
+      Node ax = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, x ),
+                                                          NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkConst( Rational(0) ),
+                                                                                                 NodeManager::currentNM()->mkNode( APPLY_UF, d_uf_measure[tn], x ) ) );
+      ax = Rewriter::rewrite( ax );
+      Trace("cegqi-lemma") << "Fairness non-negative axiom : " << ax << std::endl;
+      d_quantEngine->getOutputChannel().lemma( ax );
+    }
+  }
+}
+
 }
\ No newline at end of file
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 6139f8f59..c171156ce 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -25,15 +25,17 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-
-
 class CegInstantiation : public QuantifiersModule
 {
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
 private:
   class CegConjecture {
   public:
-    CegConjecture();
+    CegConjecture( context::Context* c );
+    /** is conjecture active */
+    context::CDO< bool > d_active;
+    /** is conjecture infeasible */
+    context::CDO< bool > d_infeasible;
     /** quantified formula */
     Node d_quant;
     /** guard */
@@ -46,24 +48,52 @@ private:
     std::vector< Node > d_candidates;
     /** list of variables on inner quantification */
     std::vector< Node > d_inner_vars;
-    /** is assigned */
-    bool isAssigned() { return !d_quant.isNull(); }
-    /** assign */
-    void assign( Node q );
     /** initialize guard */
     void initializeGuard( QuantifiersEngine * qe );
+    /** measure term */
+    Node d_measure_term;
+    /** measure sum size */
+    int d_measure_term_size;
+    /** assign */
+    void assign( Node q );
+    /** is assigned */
+    bool isAssigned() { return !d_quant.isNull(); }
+    /** current extential quantifeirs whose couterexamples we must refine */
+    std::vector< Node > d_ce_sk;
+  public:  //for fairness
+    /** the cardinality literals */
+    std::map< int, Node > d_lits;
+    /** current cardinality */
+    context::CDO< int > d_curr_lit;
+    /** allocate literal */
+    Node getLiteral( QuantifiersEngine * qe, int i );
+  };
+  class CegFairness {
+  public:
+    CegFairness( context::Context* c );
+    /** which conjecture we are looking at */
+    CegConjecture * d_conj;
+    /** the cardinality literals */
+    std::map< int, Node > d_lits;
+    /** current cardinality */
+    context::CDO< int > d_curr_lit;
+    /** allocate literal */
+    Node getLiteral( int i );
   };
   /** the quantified formula stating the synthesis conjecture */
-  CegConjecture d_conj;
-  /** is conjecture active */
-  context::CDO< bool > d_conj_active;
-  /** is conjecture infeasible */
-  context::CDO< bool > d_conj_infeasible;
+  CegConjecture * d_conj;
   /** assertions for guards */
-  NodeBoolMap d_guard_assertions;
+  //NodeBoolMap d_guard_assertions;
+private: //for enforcing fairness
+  /** measure functions */
+  std::map< TypeNode, Node > d_uf_measure;
+  /** register measured type */
+  void registerMeasuredType( TypeNode tn );
 private:
   /** check conjecture */
   void checkCegConjecture( CegConjecture * conj );
+  /** get model values */
+  bool getModelValues( std::vector< Node >& n, std::vector< Node >& v );
   /** get model value */
   Node getModelValue( Node n );
   /** get model term */
diff --git a/src/theory/quantifiers/inst_gen.cpp b/src/theory/quantifiers/inst_gen.cpp
index 971b3a5ee..33fcaa27a 100644
--- a/src/theory/quantifiers/inst_gen.cpp
+++ b/src/theory/quantifiers/inst_gen.cpp
@@ -51,7 +51,7 @@ void InstGenProcess::addMatchValue( QuantifiersEngine* qe, Node f, Node val, Ins
     if( d_inst_trie[val].addInstMatch( qe, f, m, true ) ){
       d_match_values.push_back( val );
       d_matches.push_back( InstMatch( &m ) );
-      ((QModelBuilderIG*)qe->getModelEngine()->getModelBuilder())->d_instGenMatches++;
+      ((QModelBuilderIG*)qe->getModelBuilder())->d_instGenMatches++;
     }
   }
 }
@@ -96,7 +96,7 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vecto
     //for each term we consider, calculate a current match
     for( size_t i=0; i<considerTerms.size(); i++ ){
       Node n = considerTerms[i];
-      bool isSelected = ((QModelBuilderIG*)qe->getModelEngine()->getModelBuilder())->isTermSelected( n );
+      bool isSelected = ((QModelBuilderIG*)qe->getModelBuilder())->isTermSelected( n );
       bool hadSuccess CVC4_UNUSED = false;
       for( int t=(isSelected ? 0 : 1); t<2; t++ ){
         if( t==0 || !n.getAttribute(NoMatchAttribute()) ){
@@ -197,7 +197,7 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vecto
     //process all values
     for( size_t i=0; i<considerTerms.size(); i++ ){
       Node n = considerTerms[i];
-      bool isSelected = ((QModelBuilderIG*)qe->getModelEngine()->getModelBuilder())->isTermSelected( n );
+      bool isSelected = ((QModelBuilderIG*)qe->getModelBuilder())->isTermSelected( n );
       for( int t=(isSelected ? 0 : 1); t<2; t++ ){
         //do not consider ground case if it is already congruent to another ground term
         if( t==0 || !n.getAttribute(NoMatchAttribute()) ){
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 5f949789a..4abdb66f6 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -110,6 +110,17 @@ void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){
   }
 }
 
+InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( QuantifiersEngine* qe, int tstrt,  int rgfr ) :
+                                                          InstStrategy( qe ), d_tr_strategy( tstrt ){
+  if( rgfr<0 ){
+    d_regenerate = false;
+  }else{
+    d_regenerate_frequency = rgfr;
+    d_regenerate = true;
+  }
+  d_generate_additional = true;
+}
+
 void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort effort ){
   //reset triggers
   for( std::map< Node, std::map< Trigger*, bool > >::iterator it = d_auto_gen_trigger.begin(); it != d_auto_gen_trigger.end(); ++it ){
@@ -199,7 +210,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effor
     d_patTerms[1][f].clear();
     std::vector< Node > patTermsF;
     Trigger::collectPatTerms( d_quantEngine, f, d_quantEngine->getTermDatabase()->getInstConstantBody( f ), patTermsF, d_tr_strategy, d_user_no_gen[f], true );
-    Trace("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getInstConstantBody( f ) << ", no-patterns : " << d_user_no_gen.size() << std::endl;
+    Trace("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getInstConstantBody( f ) << ", no-patterns : " << d_user_no_gen[f].size() << std::endl;
     Trace("auto-gen-trigger") << "   ";
     for( int i=0; i<(int)patTermsF.size(); i++ ){
       Trace("auto-gen-trigger") << patTermsF[i] << " ";
@@ -238,12 +249,12 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effor
   std::vector< Node > patTerms;
   //try to add single triggers first
   for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){
-    if( !d_single_trigger_gen[d_patTerms[0][f][i]] ){
+    if( d_single_trigger_gen.find( d_patTerms[0][f][i] )==d_single_trigger_gen.end() ){
       patTerms.push_back( d_patTerms[0][f][i] );
     }
   }
   //if no single triggers exist, add multi trigger terms
-  if( patTerms.empty() ){
+  if( patTerms.empty() && ( options::multiTriggerWhenSingle() || d_single_trigger_gen.empty() ) ){
     patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() );
   }
 
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h
index c2b4f7533..935432683 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/inst_strategy_e_matching.h
@@ -96,27 +96,13 @@ public:
   /** tstrt is the type of triggers to use (maximum depth, minimum depth, or all)
       rstrt is the relevance setting for trigger (use only relevant triggers vs. use all)
       rgfr is the frequency at which triggers are generated */
-  InstStrategyAutoGenTriggers( QuantifiersEngine* qe, int tstrt,  int rgfr = -1 ) :
-      InstStrategy( qe ), d_tr_strategy( tstrt ), d_generate_additional( false ){
-    setRegenerateFrequency( rgfr );
-  }
+  InstStrategyAutoGenTriggers( QuantifiersEngine* qe, int tstrt,  int rgfr = -1 );
   ~InstStrategyAutoGenTriggers(){}
 public:
   /** get auto-generated trigger */
   inst::Trigger* getAutoGenTrigger( Node f );
   /** identify */
   std::string identify() const { return std::string("AutoGenTriggers"); }
-  /** set regenerate frequency, if fr<0, turn off regenerate */
-  void setRegenerateFrequency( int fr ){
-    if( fr<0 ){
-      d_regenerate = false;
-    }else{
-      d_regenerate_frequency = fr;
-      d_regenerate = true;
-    }
-  }
-  /** set generate additional */
-  void setGenerateAdditional( bool val ) { d_generate_additional = val; }
   /** add pattern */
   void addUserNoPattern( Node f, Node pat );
 };/* class InstStrategyAutoGenTriggers */
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 9c3673bc2..1cb86e32f 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -61,7 +61,6 @@ void InstantiationEngine::finishInit(){
       tstrt = Trigger::TS_MAX_TRIGGER;
     }
     d_i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, tstrt, 3 );
-    d_i_ag->setGenerateAdditional( true );
     addInstStrategy( d_i_ag );
     
     //full saturation : instantiate from relevant domain, then arbitrary terms
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 9e5a8997b..92361f68a 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -42,28 +42,10 @@ d_triedLemmas(0),
 d_totalLemmas(0)
 {
 
-  Trace("model-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl;
-  if( options::mbqiMode()==MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL ||
-      options::mbqiMode()==MBQI_TRUST || options::fmfBoundInt() ){
-    Trace("model-engine-debug") << "...make fmc builder." << std::endl;
-    d_builder = new fmcheck::FullModelChecker( c, qe );
-  }else if( options::mbqiMode()==MBQI_INTERVAL ){
-    Trace("model-engine-debug") << "...make interval builder." << std::endl;
-    d_builder = new QIntervalBuilder( c, qe );
-  }else if( options::mbqiMode()==MBQI_ABS ){
-    Trace("model-engine-debug") << "...make abs mbqi builder." << std::endl;
-    d_builder = new AbsMbqiBuilder( c, qe );
-  }else if( options::mbqiMode()==MBQI_INST_GEN ){
-    Trace("model-engine-debug") << "...make inst-gen builder." << std::endl;
-    d_builder = new QModelBuilderInstGen( c, qe );
-  }else{
-    Trace("model-engine-debug") << "...make default model builder." << std::endl;
-    d_builder = new QModelBuilderDefault( c, qe );
-  }
 }
 
 ModelEngine::~ModelEngine() {
-  delete d_builder;
+
 }
 
 bool ModelEngine::needsCheck( Theory::Effort e ) {
@@ -75,6 +57,7 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){
     int addedLemmas = 0;
     bool needsBuild = true;
     FirstOrderModel* fm = d_quantEngine->getModel();
+    quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder();
     if( fm->getNumAssertedQuantifiers()>0 ){
       //the following will attempt to build a model and test that it satisfies all asserted universal quantifiers
       //quantifiers are initialized, we begin an instantiation round
@@ -83,7 +66,8 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){
         clSet = double(clock())/double(CLOCKS_PER_SEC);
       }
       ++(d_statistics.d_inst_rounds);
-      bool buildAtFullModel = d_builder->optBuildAtFullModel();
+      Assert( mb!=NULL );
+      bool buildAtFullModel = mb->optBuildAtFullModel();
       needsBuild = !buildAtFullModel;
       //two effort levels: first try exhaustive instantiation without axioms, then with.
       int startEffort = ( !fm->isAxiomAsserted() || options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT ) ? 1 : 0;
@@ -94,10 +78,10 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){
           Trace("model-engine") << "---Model Engine Round---" << std::endl;
           //initialize the model
           Trace("model-engine-debug") << "Build model..." << std::endl;
-          d_builder->d_considerAxioms = effort>=1;
-          d_builder->d_addedLemmas = 0;
-          d_builder->buildModel( fm, buildAtFullModel );
-          addedLemmas += (int)d_builder->d_addedLemmas;
+          mb->d_considerAxioms = effort>=1;
+          mb->d_addedLemmas = 0;
+          mb->buildModel( fm, buildAtFullModel );
+          addedLemmas += (int)mb->d_addedLemmas;
           //if builder has lemmas, add and return
           if( addedLemmas==0 ){
             Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl;
@@ -142,7 +126,7 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){
       debugPrint("fmf-consistent");
       if( options::produceModels() && needsBuild ){
         // finish building the model
-        d_builder->buildModel( fm, true );
+        mb->buildModel( fm, true );
       }
       //if the check was incomplete, we must set incomplete flag
       if( d_incomplete_check ){
@@ -188,6 +172,7 @@ bool ModelEngine::optOneQuantPerRound(){
 
 int ModelEngine::checkModel(){
   FirstOrderModel* fm = d_quantEngine->getModel();
+  quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder();
 
   //flatten the representatives
   //Trace("model-engine-debug") << "Flattening representatives...." << std::endl;
@@ -237,7 +222,7 @@ int ModelEngine::checkModel(){
       for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
         Node f = fm->getAssertedQuantifier( i );
         //determine if we should check this quantifier
-        if( d_builder->isQuantifierActive( f ) ){
+        if( mb->isQuantifierActive( f ) ){
           exhaustiveInstantiate( f, e );
           if( Trace.isOn("model-engine-warn") ){
             if( d_addedLemmas>10000 ){
@@ -256,7 +241,7 @@ int ModelEngine::checkModel(){
     }
   }
   //print debug information
-  Trace("model-engine-debug") << "Instantiate axioms : " << ( d_builder->d_considerAxioms ? "yes" : "no" ) << std::endl;
+  Trace("model-engine-debug") << "Instantiate axioms : " << ( mb->d_considerAxioms ? "yes" : "no" ) << std::endl;
   Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / ";
   Trace("model-engine") << d_totalLemmas << std::endl;
   return d_addedLemmas;
@@ -264,15 +249,16 @@ int ModelEngine::checkModel(){
 
 void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
   //first check if the builder can do the exhaustive instantiation
-  d_builder->d_triedLemmas = 0;
-  d_builder->d_addedLemmas = 0;
-  d_builder->d_incomplete_check = false;
-  if( d_builder->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort ) ){
+  quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder();
+  mb->d_triedLemmas = 0;
+  mb->d_addedLemmas = 0;
+  mb->d_incomplete_check = false;
+  if( mb->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort ) ){
     Trace("inst-fmf-ei") << "-> Builder determined instantiation(s)." << std::endl;
-    d_triedLemmas += d_builder->d_triedLemmas;
-    d_addedLemmas += d_builder->d_addedLemmas;
-    d_incomplete_check = d_incomplete_check || d_builder->d_incomplete_check;
-    d_statistics.d_mbqi_inst_lemmas += d_builder->d_addedLemmas;
+    d_triedLemmas += mb->d_triedLemmas;
+    d_addedLemmas += mb->d_addedLemmas;
+    d_incomplete_check = d_incomplete_check || mb->d_incomplete_check;
+    d_statistics.d_mbqi_inst_lemmas += mb->d_addedLemmas;
   }else{
     Trace("inst-fmf-ei") << "-> Exhaustive instantiate " << f << ", effort = " << effort << "..." << std::endl;
     Debug("inst-fmf-ei") << "   Instantiation Constants: ";
@@ -316,7 +302,7 @@ void ModelEngine::debugPrint( const char* c ){
   for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
     Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
     Trace( c ) << "   ";
-    if( !d_builder->isQuantifierActive( f ) ){
+    if( !d_quantEngine->getModelBuilder()->isQuantifierActive( f ) ){
       Trace( c ) << "*Inactive* ";
     }else{
       Trace( c ) << "           ";
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index 890af1643..6929188bc 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -28,9 +28,6 @@ namespace quantifiers {
 class ModelEngine : public QuantifiersModule
 {
   friend class RepSetIterator;
-private:
-  /** builder class */
-  QModelBuilder* d_builder;
 private:
   //options
   bool optOneQuantPerRound();
@@ -49,8 +46,6 @@ private:
 public:
   ModelEngine( context::Context* c, QuantifiersEngine* qe );
   virtual ~ModelEngine();
-  //get the builder
-  QModelBuilder* getModelBuilder() { return d_builder; }
 public:
   bool needsCheck( Theory::Effort e );
   void check( Theory::Effort e, unsigned quant_e );
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 5e3c66d9a..d608f0820 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -67,6 +67,8 @@ option relationalTriggers --relational-triggers bool :default false
  choose relational triggers such as x = f(y), x >= f(y)
 option purifyTriggers --purify-triggers bool :default false :read-write
  purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto y-1
+option multiTriggerWhenSingle --multi-trigger-when-single bool :default true
+ never select multi-triggers when single triggers exist
 option triggerSelMode --trigger-sel CVC4::theory::quantifiers::TriggerSelMode :default CVC4::theory::quantifiers::TRIGGER_SEL_DEFAULT :read-write :include "theory/quantifiers/modes.h" :handler  CVC4::theory::quantifiers::stringToTriggerSelMode :handler-include "theory/quantifiers/options_handlers.h"
  selection mode for triggers
 
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index d17899cf2..09cae8eca 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -25,8 +25,6 @@
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/trigger.h"
-//#include "theory/rewriterules/efficient_e_matching.h"
-//#include "theory/rewriterules/rr_trigger.h"
 #include "theory/quantifiers/bounded_integers.h"
 #include "theory/quantifiers/rewrite_engine.h"
 #include "theory/quantifiers/quant_conflict_find.h"
@@ -35,6 +33,9 @@
 #include "theory/quantifiers/relevant_domain.h"
 #include "theory/uf/options.h"
 #include "theory/uf/theory_uf.h"
+#include "theory/quantifiers/full_model_check.h"
+#include "theory/quantifiers/qinterval_builder.h"
+#include "theory/quantifiers/ambqi_builder.h"
 
 using namespace std;
 using namespace CVC4;
@@ -45,7 +46,7 @@ using namespace CVC4::theory::inst;
 
 
 eq::EqualityEngine * QuantifiersModule::getEqualityEngine() {
-  return d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
+  return d_quantEngine->getMasterEqualityEngine();
 }
 
 bool QuantifiersModule::areEqual( TNode n1, TNode n2 ) {
@@ -80,7 +81,9 @@ d_lemmas_produced_c(u){
   //d_rr_tr_trie = new rrinst::TriggerTrie;
   //d_eem = new EfficientEMatcher( this );
   d_hasAddedLemma = false;
-
+  
+  bool needsBuilder = false;
+  
   Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
 
   //the model object
@@ -135,6 +138,7 @@ d_lemmas_produced_c(u){
     }
     d_model_engine = new quantifiers::ModelEngine( c, this );
     d_modules.push_back( d_model_engine );
+    needsBuilder = true;
   }else{
     d_model_engine = NULL;
     d_bint = NULL;
@@ -151,12 +155,36 @@ d_lemmas_produced_c(u){
   }else{
     d_ceg_inst = NULL;
   }
+  
+  if( needsBuilder ){
+    Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl;
+    if( options::mbqiMode()==quantifiers::MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL ||
+        options::mbqiMode()==quantifiers::MBQI_TRUST || options::fmfBoundInt() ){
+      Trace("quant-engine-debug") << "...make fmc builder." << std::endl;
+      d_builder = new quantifiers::fmcheck::FullModelChecker( c, this );
+    }else if( options::mbqiMode()==quantifiers::MBQI_INTERVAL ){
+      Trace("quant-engine-debug") << "...make interval builder." << std::endl;
+      d_builder = new quantifiers::QIntervalBuilder( c, this );
+    }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){
+      Trace("quant-engine-debug") << "...make abs mbqi builder." << std::endl;
+      d_builder = new quantifiers::AbsMbqiBuilder( c, this );
+    }else if( options::mbqiMode()==quantifiers::MBQI_INST_GEN ){
+      Trace("quant-engine-debug") << "...make inst-gen builder." << std::endl;
+      d_builder = new quantifiers::QModelBuilderInstGen( c, this );
+    }else{
+      Trace("quant-engine-debug") << "...make default model builder." << std::endl;
+      d_builder = new quantifiers::QModelBuilderDefault( c, this );
+    }
+  }else{
+    d_builder = NULL;
+  }
 
   //options
   d_total_inst_count_debug = 0;
 }
 
 QuantifiersEngine::~QuantifiersEngine(){
+  delete d_builder;
   delete d_rr_engine;
   delete d_bint;
   delete d_model_engine;
@@ -168,6 +196,8 @@ QuantifiersEngine::~QuantifiersEngine(){
   delete d_tr_trie;
   delete d_term_db;
   delete d_eq_query;
+  delete d_sg_gen;
+  delete d_ceg_inst;
   for(std::map< Node, QuantPhaseReq* >::iterator i = d_phase_reqs.begin(); i != d_phase_reqs.end(); ++i) {
     delete (*i).second;
   }
@@ -199,7 +229,7 @@ void QuantifiersEngine::finishInit(){
   }
 }
 
-QuantifiersModule * QuantifiersEngine::getOwner( Node q ) { 
+QuantifiersModule * QuantifiersEngine::getOwner( Node q ) {
   std::map< Node, QuantifiersModule * >::iterator it = d_owner.find( q );
   if( it==d_owner.end() ){
     return NULL;
@@ -214,7 +244,7 @@ void QuantifiersEngine::setOwner( Node q, QuantifiersModule * m ) {
     if( mo!=NULL ){
       Trace("quant-warn") << "WARNING: setting owner of " << q << " to " << ( m ? m->identify() : "null" ) << ", but already has owner " << mo->identify() << "!" << std::endl;
     }
-    d_owner[q] = m; 
+    d_owner[q] = m;
   }
 }
 
@@ -247,6 +277,9 @@ void QuantifiersEngine::check( Theory::Effort e ){
     Trace("quant-engine-debug") << "  # quantified formulas = " << d_model->getNumAssertedQuantifiers() << std::endl;
     Trace("quant-engine-debug") << "  Theory engine finished : " << !d_te->needCheck() << std::endl;
 
+    Trace("quant-engine-ee") << "Equality engine : " << std::endl;
+    debugPrintEqualityEngine( "quant-engine-ee" );
+
     if( !getMasterEqualityEngine()->consistent() ){
       Trace("quant-engine") << "Master equality engine not consistent, return." << std::endl;
       return;
@@ -628,8 +661,8 @@ bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, b
       }
     }
   }
-  //also check model engine (it may contain instantiations internally)
-  if( d_model_engine->getModelBuilder()->existsInstantiation( f, m, modEq, modInst ) ){
+  //also check model builder (it may contain instantiations internally)
+  if( d_builder && d_builder->existsInstantiation( f, m, modEq, modInst ) ){
     return true;
   }
   return false;
@@ -881,7 +914,34 @@ QuantifiersEngine::Statistics::~Statistics(){
 }
 
 eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){
-  return ((quantifiers::TheoryQuantifiers*)getTheoryEngine()->theoryOf( THEORY_QUANTIFIERS ))->getMasterEqualityEngine();
+  return getTheoryEngine()->getMasterEqualityEngine();
+}
+
+void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) {
+  eq::EqualityEngine* ee = getMasterEqualityEngine();
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
+  while( !eqcs_i.isFinished() ){
+    TNode r = (*eqcs_i);
+    bool firstTime = true;
+    Trace(c) << "  " << r;
+    Trace(c) << " : { ";
+    eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
+    while( !eqc_i.isFinished() ){
+      TNode n = (*eqc_i);
+      if( r!=n ){
+        if( firstTime ){
+          Trace(c) << std::endl;
+          firstTime = false;
+        }
+        Trace(c) << "    " << n << std::endl;
+      }
+      ++eqc_i;
+    }
+    if( !firstTime ){ Trace(c) << "  "; }
+    Trace(c) << "}" << std::endl;
+    ++eqcs_i;
+  }
+  Trace(c) << std::endl;
 }
 
 void EqualityQueryQuantifiersEngine::reset(){
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index b5a02df60..ee905ad09 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -82,6 +82,7 @@ namespace quantifiers {
   class QuantConflictFind;
   class RewriteEngine;
   class RelevantDomain;
+  class QModelBuilder;
   class ConjectureGenerator;
   class CegInstantiation;
 }/* CVC4::theory::quantifiers */
@@ -111,6 +112,8 @@ private:
   QuantRelevance * d_quant_rel;
   /** relevant domain */
   quantifiers::RelevantDomain* d_rel_dom;
+  /** model builder */
+  quantifiers::QModelBuilder* d_builder;
   /** phase requirements for each quantifier for each instantiation literal */
   std::map< Node, QuantPhaseReq* > d_phase_reqs;
   /** instantiation engine */
@@ -184,6 +187,8 @@ public:
   quantifiers::RelevantDomain* getRelevantDomain() { return d_rel_dom; }
   /** get quantifier relevance */
   QuantRelevance* getQuantifierRelevance() { return d_quant_rel; }
+  /** get the model builder */
+  quantifiers::QModelBuilder* getModelBuilder() { return d_builder; }
   /** get phase requirement information */
   QuantPhaseReq* getPhaseRequirements( Node f ) { return d_phase_reqs.find( f )==d_phase_reqs.end() ? NULL : d_phase_reqs[f]; }
   /** get phase requirement terms */
@@ -284,6 +289,8 @@ public:
   void addTermToDatabase( Node n, bool withinQuant = false );
   /** get the master equality engine */
   eq::EqualityEngine* getMasterEqualityEngine() ;
+  /** debug print equality engine */
+  void debugPrintEqualityEngine( const char * c );
 public:
   /** print instantiations */
   void printInstantiations( std::ostream& out );