more cleanup of quantifiers code

27 files changed, 514 insertions, 595 deletions

diff --git a/src/theory/arith/theory_arith_instantiator.cpp b/src/theory/arith/theory_arith_instantiator.cpp
index 2135f9064..b6c85b7eb 100644
--- a/src/theory/arith/theory_arith_instantiator.cpp
+++ b/src/theory/arith/theory_arith_instantiator.cpp
@@ -107,9 +107,9 @@ void InstantiatorTheoryArith::assertNode( Node assertion ){
   d_quantEngine->addTermToDatabase( assertion );
   if( options::cbqi() ){
     if( assertion.hasAttribute(InstConstantAttribute()) ){
-      setHasConstraintsFrom( assertion.getAttribute(InstConstantAttribute()) );
+      setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) );
     }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
-      setHasConstraintsFrom( assertion[0].getAttribute(InstConstantAttribute()) );
+      setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) );
     }
   }
 }
@@ -140,7 +140,7 @@ void InstantiatorTheoryArith::processResetInstantiationRound( Theory::Effort eff
           d_instRows[f].push_back( x );
           //this theory has constraints from f
           Debug("quant-arith") << "Has constraints from " << f << std::endl;
-          setHasConstraintsFrom( f );
+          setQuantifierActive( f );
           //set tableaux term
           if( t.getNumChildren()==0 ){
             d_tableaux_term[x] = NodeManager::currentNM()->mkConst( Rational(0) );
diff --git a/src/theory/arrays/theory_arrays_instantiator.cpp b/src/theory/arrays/theory_arrays_instantiator.cpp
index b53496f22..a93a01322 100644
--- a/src/theory/arrays/theory_arrays_instantiator.cpp
+++ b/src/theory/arrays/theory_arrays_instantiator.cpp
@@ -39,9 +39,9 @@ void InstantiatorTheoryArrays::assertNode( Node assertion ){
   d_quantEngine->addTermToDatabase( assertion );
   if( options::cbqi() ){
     if( assertion.hasAttribute(InstConstantAttribute()) ){
-      setHasConstraintsFrom( assertion.getAttribute(InstConstantAttribute()) );
+      setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) );
     }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
-      setHasConstraintsFrom( assertion[0].getAttribute(InstConstantAttribute()) );
+      setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) );
     }
   }
 }
diff --git a/src/theory/datatypes/theory_datatypes_instantiator.cpp b/src/theory/datatypes/theory_datatypes_instantiator.cpp
index cc8d9fa30..e9f255c65 100644
--- a/src/theory/datatypes/theory_datatypes_instantiator.cpp
+++ b/src/theory/datatypes/theory_datatypes_instantiator.cpp
@@ -36,9 +36,9 @@ void InstantiatorTheoryDatatypes::assertNode( Node assertion ){
   d_quantEngine->addTermToDatabase( assertion );
   if( options::cbqi() ){
     if( assertion.hasAttribute(InstConstantAttribute()) ){
-      setHasConstraintsFrom( assertion.getAttribute(InstConstantAttribute()) );
+      setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) );
     }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
-      setHasConstraintsFrom( assertion[0].getAttribute(InstConstantAttribute()) );
+      setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) );
     }
   }
 }
diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am
index db0eed31e..57b99c59b 100644
--- a/src/theory/quantifiers/Makefile.am
+++ b/src/theory/quantifiers/Makefile.am
@@ -38,7 +38,9 @@ libquantifiers_la_SOURCES = \
 	quantifiers_attributes.h \
 	quantifiers_attributes.cpp \
 	inst_gen.h \
-	inst_gen.cpp
+	inst_gen.cpp \
+	quant_util.h \
+	quant_util.cpp
 
 EXTRA_DIST = \
 	kinds \
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 685898515..28eeca624 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -27,7 +27,7 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
 FirstOrderModel::FirstOrderModel( context::Context* c, std::string name ) : TheoryModel( c, name, true ),
-d_axiom_asserted( c, false ), d_forall_asserts( c ){
+d_axiom_asserted( c, false ), d_forall_asserts( c ), d_isModelSet( c, false ){
 
 }
 
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index df9b55582..c8fcb7c44 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -48,6 +48,8 @@ private:
   context::CDO< bool > d_axiom_asserted;
   /** list of quantifiers asserted in the current context */
   context::CDList<Node> d_forall_asserts;
+  /** is model set */
+  context::CDO< bool > d_isModelSet;
 public: //for Theory UF:
   //models for each UF operator
   std::map< Node, uf::UfModelTree > d_uf_model_tree;
@@ -78,9 +80,12 @@ public:
   virtual ~FirstOrderModel(){}
   // reset the model
   void reset();
-public:
   // initialize the model
   void initialize( bool considerAxioms = true );
+  /** mark model set */
+  void markModelSet() { d_isModelSet = true; }
+  /** is model set */
+  bool isModelSet() { return d_isModelSet; }
 //the following functions are for evaluating quantifier bodies
 public:
   /** reset evaluation */
diff --git a/src/theory/quantifiers/inst_gen.cpp b/src/theory/quantifiers/inst_gen.cpp
index 324165692..ea58840f5 100755
--- a/src/theory/quantifiers/inst_gen.cpp
+++ b/src/theory/quantifiers/inst_gen.cpp
@@ -44,8 +44,8 @@ InstGenProcess::InstGenProcess( Node n ) : d_node( n ){
 }

 

 void InstGenProcess::addMatchValue( QuantifiersEngine* qe, Node f, Node val, InstMatch& m ){

-  if( !qe->existsInstantiation( f, m, true, true ) ){

-    //if( d_inst_trie[val].addInstMatch( qe, f, m, true, NULL, true ) ){

+  if( !qe->existsInstantiation( f, m, true ) ){

+    //if( d_inst_trie[val].addInstMatch( qe, f, m, true ) ){

       d_match_values.push_back( val );

       d_matches.push_back( InstMatch( &m ) );

     //}

diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index a74bf0fd5..d00885abf 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -100,8 +100,8 @@ void InstMatch::debugPrint( const char* c ){
 }
 
 void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){
-  for( int i=0; i<(int)qe->getTermDatabase()->d_inst_constants[f].size(); i++ ){
-    Node ic = qe->getTermDatabase()->d_inst_constants[f][i];
+  for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+    Node ic = qe->getTermDatabase()->getInstantiationConstant( f, i );
     if( d_map.find( ic )==d_map.end() ){
       d_map[ ic ] = qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
     }
@@ -145,26 +145,6 @@ Node InstMatch::getValue( Node var ){
     return Node::null();
   }
 }
-/*
-void InstMatch::computeTermVec( QuantifiersEngine* qe, const std::vector< Node >& vars, std::vector< Node >& match ){
-  for( int i=0; i<(int)vars.size(); i++ ){
-    std::map< Node, Node >::iterator it = d_map.find( vars[i] );
-    if( it!=d_map.end() && !it->second.isNull() ){
-      match.push_back( it->second );
-    }else{
-      match.push_back( qe->getTermDatabase()->getFreeVariableForInstConstant( vars[i] ) );
-    }
-  }
-}
-
-void InstMatch::computeTermVec( const std::vector< Node >& vars, std::vector< Node >& match ){
-  for( int i=0; i<(int)vars.size(); i++ ){
-    if( d_map.find( vars[i] )!=d_map.end() && !d_map[ vars[i] ].isNull() ){
-      match.push_back( d_map[ vars[i] ] );
-    }
-  }
-}
-*/
 
 /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
 void InstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio ){
@@ -176,7 +156,7 @@ void InstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m,
 }
 
 /** exists match */
-bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, int index, ImtIndexOrder* imtio, bool modInst ){
+bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio ){
   if( long(index)==long(f[0].getNumChildren()) || ( imtio && long(index)==long(imtio->d_order.size()) ) ){
     return true;
   }else{
@@ -184,7 +164,7 @@ bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch&
     Node n = m.get( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) );
     std::map< Node, InstMatchTrie >::iterator it = d_data.find( n );
     if( it!=d_data.end() ){
-      if( it->second.existsInstMatch2( qe, f, m, modEq, index+1, imtio, modInst ) ){
+      if( it->second.existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){
         return true;
       }
     }
@@ -194,7 +174,7 @@ bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch&
         Node nl;
         it = d_data.find( nl );
         if( it!=d_data.end() ){
-          if( it->second.existsInstMatch2( qe, f, m, modEq, index+1, imtio, modInst ) ){
+          if( it->second.existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){
             return true;
           }
         }
@@ -210,7 +190,7 @@ bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch&
           if( en!=n ){
             std::map< Node, InstMatchTrie >::iterator itc = d_data.find( en );
             if( itc!=d_data.end() ){
-              if( itc->second.existsInstMatch2( qe, f, m, modEq, index+1, imtio, modInst ) ){
+              if( itc->second.existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){
                 return true;
               }
             }
@@ -223,12 +203,12 @@ bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch&
   }
 }
 
-bool InstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, ImtIndexOrder* imtio, bool modInst ){
-  return existsInstMatch2( qe, f, m, modEq, 0, imtio, modInst );
+bool InstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, ImtIndexOrder* imtio ){
+  return existsInstMatch2( qe, f, m, modEq, modInst, 0, imtio );
 }
 
-bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, ImtIndexOrder* imtio, bool modInst ){
-  if( !existsInstMatch( qe, f, m, modEq, imtio, modInst ) ){
+bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, ImtIndexOrder* imtio ){
+  if( !existsInstMatch( qe, f, m, modEq, modInst, imtio ) ){
     addInstMatch2( qe, f, m, 0, imtio );
     return true;
   }else{
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index feab91837..a0db1336f 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -122,10 +122,6 @@ public:
   void makeInternal( QuantifiersEngine* qe );
   /** make representative */
   void makeRepresentative( QuantifiersEngine* qe );
-  /** compute d_match */
-  //void computeTermVec( QuantifiersEngine* qe, const std::vector< Node >& vars, std::vector< Node >& match );
-  /** compute d_match */
-  //void computeTermVec( const std::vector< Node >& vars, std::vector< Node >& match );
   /** get value */
   Node getValue( Node var );
   /** clear */
@@ -191,7 +187,7 @@ private:
   /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
   void addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio );
   /** exists match */
-  bool existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, int index, ImtIndexOrder* imtio, bool modInst );
+  bool existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio );
 public:
   /** the data */
   std::map< Node, InstMatchTrie > d_data;
@@ -204,16 +200,16 @@ public:
         modInst is if we return true if m is an instance of a match that exists
    */
   bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
-                        ImtIndexOrder* imtio = NULL, bool modInst = false );
+                        bool modInst = false, ImtIndexOrder* imtio = NULL );
   /** add match m for quantifier f, take into account equalities if modEq = true,
       if imtio is non-null, this is the order to add to trie
       return true if successful
   */
   bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
-                     ImtIndexOrder* imtio = NULL, bool modInst = false );
+                     bool modInst = false, ImtIndexOrder* imtio = NULL );
 };/* class InstMatchTrie */
 
-class InstMatchTrieOrdered {
+class InstMatchTrieOrdered{
 private:
   InstMatchTrie::ImtIndexOrder* d_imtio;
   InstMatchTrie d_imt;
@@ -226,8 +222,11 @@ public:
   InstMatchTrie* getTrie() { return &d_imt; }
 public:
   /** add match m, return true if successful */
-  bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false ){
-    return d_imt.addInstMatch( qe, f, m, modEq, d_imtio );
+  bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){
+    return d_imt.addInstMatch( qe, f, m, modEq, modInst, d_imtio );
+  }
+  bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){
+    return d_imt.existsInstMatch( qe, f, m, modEq, modInst, d_imtio );
   }
 };/* class InstMatchTrieOrdered */
 
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index b402638b1..027ac67eb 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -32,35 +32,6 @@ QuantifiersModule( qe ), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ){
 
 }
 
-bool InstantiationEngine::hasAddedCbqiLemma( Node f ) {
-  return d_ce_lit.find( f ) != d_ce_lit.end();
-}
-
-void InstantiationEngine::addCbqiLemma( Node f ){
-  Assert( doCbqi( f ) && !hasAddedCbqiLemma( f ) );
-  //code for counterexample-based quantifier instantiation
-  Debug("cbqi") << "Do cbqi for " << f << std::endl;
-  //make the counterexample body
-  //Node ceBody = f[1].substitute( d_quantEngine->d_vars[f].begin(), d_quantEngine->d_vars[f].end(),
-  //                              d_quantEngine->d_inst_constants[f].begin(),
-  //                              d_quantEngine->d_inst_constants[f].end() );
-  //get the counterexample literal
-  Node ceBody = d_quantEngine->getTermDatabase()->getCounterexampleBody( f );
-  Node ceLit = d_quantEngine->getValuation().ensureLiteral( ceBody.notNode() );
-  d_ce_lit[ f ] = ceLit;
-  d_quantEngine->getTermDatabase()->setInstantiationConstantAttr( ceLit, f );
-  // set attributes, mark all literals in the body of n as dependent on cel
-  //registerLiterals( ceLit, f );
-  //require any decision on cel to be phase=true
-  d_quantEngine->getOutputChannel().requirePhase( ceLit, true );
-  Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl;
-  //add counterexample lemma
-  NodeBuilder<> nb(kind::OR);
-  nb << f << ceLit;
-  Node lem = nb;
-  Debug("cbqi-debug") << "Counterexample lemma : " << lem << std::endl;
-  d_quantEngine->getOutputChannel().lemma( lem );
-}
 
 bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
   //if counterexample-based quantifier instantiation is active
@@ -70,8 +41,20 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
     for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
       Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
       if( doCbqi( f ) && !hasAddedCbqiLemma( f ) ){
+        d_added_cbqi_lemma[f] = true;
+        Debug("cbqi") << "Do cbqi for " << f << std::endl;
         //add cbqi lemma
-        addCbqiLemma( f );
+        //get the counterexample literal
+        Node ceLit = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( f );
+        //require any decision on cel to be phase=true
+        d_quantEngine->getOutputChannel().requirePhase( ceLit, true );
+        Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl;
+        //add counterexample lemma
+        NodeBuilder<> nb(kind::OR);
+        nb << f << ceLit;
+        Node lem = nb;
+        Debug("cbqi-debug") << "Counterexample lemma : " << lem << std::endl;
+        d_quantEngine->getOutputChannel().lemma( lem );
         addedLemma = true;
       }
     }
@@ -98,7 +81,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
       Node f = d_quantEngine->getModel()->getAssertedQuantifier( q );
       Debug("inst-engine-debug") << "IE: Instantiate " << f << "..." << std::endl;
       //if this quantifier is active
-      if( d_quantEngine->getActive( f ) ){
+      if( d_quant_active[ f ] ){
         //int e_use = d_quantEngine->getRelevance( f )==-1 ? e - 1 : e;
         int e_use = e;
         if( e_use>=0 ){
@@ -165,16 +148,12 @@ void InstantiationEngine::check( Theory::Effort e ){
       Trace("inst-engine") << "---Instantiation Engine Round, effort = " << e << "---" << std::endl;
     }
     bool quantActive = false;
-    //for each quantifier currently asserted,
-    // such that the counterexample literal is not in positive in d_counterexample_asserts
-   // for( BoolMap::iterator i = d_forall_asserts.begin(); i != d_forall_asserts.end(); i++ ) {
-    //  if( (*i).second ) {
     Debug("quantifiers") << "quantifiers:  check:  asserted quantifiers size"
                          << d_quantEngine->getModel()->getNumAssertedQuantifiers() << std::endl;
     for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
       Node n = d_quantEngine->getModel()->getAssertedQuantifier( i );
       if( options::cbqi() && hasAddedCbqiLemma( n ) ){
-        Node cel = d_ce_lit[ n ];
+        Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( n );
         bool active, value;
         bool ceValue = false;
         if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){
@@ -183,7 +162,7 @@ void InstantiationEngine::check( Theory::Effort e ){
         }else{
           active = true;
         }
-        d_quantEngine->setActive( n, active );
+        d_quant_active[n] = active;
         if( active ){
           Debug("quantifiers") << "  Active : " << n;
           quantActive = true;
@@ -203,15 +182,14 @@ void InstantiationEngine::check( Theory::Effort e ){
         }
         Debug("quantifiers") << std::endl;
       }else{
-        d_quantEngine->setActive( n, true );
+        d_quant_active[n] = true;
         quantActive = true;
         Debug("quantifiers") << "  Active : " << n << ", no ce assigned." << std::endl;
       }
       Debug("quantifiers-relevance")  << "Quantifier : " << n << std::endl;
-      Debug("quantifiers-relevance")  << "   Relevance : " << d_quantEngine->getRelevance( n ) << std::endl;
-      Debug("quantifiers") << "   Relevance : " << d_quantEngine->getRelevance( n ) << std::endl;
+      Debug("quantifiers-relevance")  << "   Relevance : " << d_quantEngine->getQuantifierRelevance()->getRelevance( n ) << std::endl;
+      Debug("quantifiers") << "   Relevance : " << d_quantEngine->getQuantifierRelevance()->getRelevance( n ) << std::endl;
     }
-    //}
     if( quantActive ){
       bool addedLemmas = doInstantiationRound( e );
       //Debug("quantifiers-dec") << "Do instantiation, level = " << d_quantEngine->getValuation().getDecisionLevel() << std::endl;
@@ -248,17 +226,17 @@ void InstantiationEngine::check( Theory::Effort e ){
 
 void InstantiationEngine::registerQuantifier( Node f ){
   //Notice() << "do cbqi " << f << " ? " << std::endl;
-  Node ceBody = d_quantEngine->getTermDatabase()->getCounterexampleBody( f );
+  Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
   if( !doCbqi( f ) ){
     d_quantEngine->addTermToDatabase( ceBody, true );
     //need to tell which instantiators will be responsible
     //by default, just chose the UF instantiator
-    d_quantEngine->getInstantiator( theory::THEORY_UF )->setHasConstraintsFrom( f );
+    d_quantEngine->getInstantiator( theory::THEORY_UF )->setQuantifierActive( f );
   }
 
   //take into account user patterns
   if( f.getNumChildren()==3 ){
-    Node subsPat = d_quantEngine->getTermDatabase()->getSubstitutedNode( f[2], f );
+    Node subsPat = d_quantEngine->getTermDatabase()->getInstConstantNode( f[2], f );
     //add patterns
     for( int i=0; i<(int)subsPat.getNumChildren(); i++ ){
       //Notice() << "Add pattern " << subsPat[i] << " for " << f << std::endl;
@@ -320,22 +298,6 @@ bool InstantiationEngine::doCbqi( Node f ){
 
 
 
-//void InstantiationEngine::registerLiterals( Node n, Node f ){
-//  if( n.getAttribute(InstConstantAttribute())==f ){
-//    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-//      registerLiterals( n[i], f );
-//    }
-//    if( !d_ce_lit[ f ].isNull() ){
-//      if( d_quantEngine->d_te->getPropEngine()->isSatLiteral( n ) && n.getKind()!=NOT ){
-//        if( n!=d_ce_lit[ f ] && n.notNode()!=d_ce_lit[ f ] ){
-//          Debug("quant-dep-dec") << "Make " << n << " dependent on ";
-//          Debug("quant-dep-dec") << d_ce_lit[ f ] << std::endl;
-//          d_quantEngine->getOutputChannel().dependentDecision( d_ce_lit[ f ], n );
-//        }
-//      }
-//    }
-//  }
-//}
 
 void InstantiationEngine::debugSat( int reason ){
   if( reason==SAT_CBQI ){
@@ -347,7 +309,7 @@ void InstantiationEngine::debugSat( int reason ){
     //  if( (*i).second ) {
     for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
       Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
-      Node cel = d_ce_lit[ f ];
+      Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( f );
       Assert( !cel.isNull() );
       bool value;
       if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){
@@ -371,26 +333,20 @@ void InstantiationEngine::debugSat( int reason ){
   }
 }
 
-void InstantiationEngine::propagate( Theory::Effort level ){
-  //propagate as decision all counterexample literals that are not asserted
-  for( std::map< Node, Node >::iterator it = d_ce_lit.begin(); it != d_ce_lit.end(); ++it ){
-    bool value;
-    if( !d_quantEngine->getValuation().hasSatValue( it->second, value ) ){
-      //if not already set, propagate as decision
-      //d_quantEngine->getOutputChannel().propagateAsDecision( it->second );
-      Debug("cbqi-prop-as-dec") << "CBQI: propagate as decision " << it->second << std::endl;
-    }
-  }
-}
-
 Node InstantiationEngine::getNextDecisionRequest(){
   //propagate as decision all counterexample literals that are not asserted
-  for( std::map< Node, Node >::iterator it = d_ce_lit.begin(); it != d_ce_lit.end(); ++it ){
-    bool value;
-    if( !d_quantEngine->getValuation().hasSatValue( it->second, value ) ){
-      //if not already set, propagate as decision
-      Debug("cbqi-prop-as-dec") << "CBQI: propagate as decision " << it->second << std::endl;
-      return it->second;
+  if( options::cbqi() ){
+    for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+      Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
+      if( hasAddedCbqiLemma( f ) ){
+        Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( f );
+        bool value;
+        if( !d_quantEngine->getValuation().hasSatValue( cel, value ) ){
+          //if not already set, propagate as decision
+          Debug("cbqi-prop-as-dec") << "CBQI: propagate as decision " << cel << std::endl;
+          return cel;
+        }
+      }
     }
   }
   return Node::null();
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 896e17ac8..6d995097a 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -30,16 +30,17 @@ private:
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
   /** status of instantiation round (one of InstStrategy::STATUS_*) */
   int d_inst_round_status;
-  /** map from universal quantifiers to their counterexample literals */
-  std::map< Node, Node > d_ce_lit;
   /** whether the instantiation engine should set incomplete if it cannot answer SAT */
   bool d_setIncomplete;
   /** inst round counter */
   int d_ierCounter;
+  /** whether each quantifier is active */
+  std::map< Node, bool > d_quant_active;
+  /** whether we have added cbqi lemma */
+  std::map< Node, bool > d_added_cbqi_lemma;
 private:
-  bool hasAddedCbqiLemma( Node f );
-  void addCbqiLemma( Node f );
-private:
+  /** has added cbqi lemma */
+  bool hasAddedCbqiLemma( Node f ) { return d_added_cbqi_lemma.find( f )!=d_added_cbqi_lemma.end(); }
   /** helper functions */
   bool hasNonArithmeticVariable( Node f );
   bool hasApplyUf( Node f );
@@ -65,11 +66,7 @@ public:
   void registerQuantifier( Node f );
   void assertNode( Node f );
   Node explain(TNode n){ return Node::null(); }
-  void propagate( Theory::Effort level );
   Node getNextDecisionRequest();
-public:
-  /** get the corresponding counterexample literal for quantified formula node n */
-  Node getCounterexampleLiteralFor( Node f ) { return d_ce_lit.find( f )==d_ce_lit.end() ? Node::null() : d_ce_lit[ f ]; }
 };/* class InstantiationEngine */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 6fa02a8d3..3d1ca8f0d 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -51,6 +51,8 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) {
       fm->d_uf_models[ it->first ] = it->second.getFunctionValue( "$x" );
     }
     TheoryEngineModelBuilder::processBuildModel( m, fullModel );
+    //mark that the model has been set
+    fm->markModelSet();
   }else{
     d_curr_model = fm;
     //build model for relevant symbols contained in quantified formulas
@@ -338,8 +340,8 @@ void ModelEngineBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f )
   //for each asserted quantifier f,
   // - determine selection literals
   // - check which function/predicates have good and bad definitions for satisfying f
-  for( std::map< Node, bool >::iterator it = d_qe->d_phase_reqs[f].begin();
-       it != d_qe->d_phase_reqs[f].end(); ++it ){
+  QuantPhaseReq* qpr = d_qe->getPhaseRequirements( f );
+  for( std::map< Node, bool >::iterator it = qpr->d_phase_reqs.begin(); it != qpr->d_phase_reqs.end(); ++it ){
     //the literal n is phase-required for quantifier f
     Node n = it->first;
     Node gn = d_qe->getTermDatabase()->getModelBasis( f, n );
@@ -465,8 +467,10 @@ int ModelEngineBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){
       std::vector< Node > tr_terms;
       if( lit.getKind()==APPLY_UF ){
         //only match predicates that are contrary to this one, use literal matching
-        Node eq = NodeManager::currentNM()->mkNode( IFF, lit, !phase ? fm->d_true : fm->d_false );
-        d_qe->getTermDatabase()->setInstantiationConstantAttr( eq, f );
+        std::vector< Node > children;
+        children.push_back( lit );
+        children.push_back( !phase ? fm->d_true : fm->d_false );
+        Node eq = d_qe->getTermDatabase()->mkNodeInstConstant( IFF, children, f );
         tr_terms.push_back( eq );
       }else if( lit.getKind()==EQUAL ){
         //collect trigger terms
@@ -532,7 +536,7 @@ void ModelEngineBuilderInstGen::analyzeQuantifiers( FirstOrderModel* fm ){
 
 void ModelEngineBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f ){
   //determine selection formula, set terms in selection formula as being selected
-  Node s = getSelectionFormula( d_qe->getTermDatabase()->getCounterexampleBody( f ),
+  Node s = getSelectionFormula( d_qe->getTermDatabase()->getInstConstantBody( f ),
                                 d_qe->getTermDatabase()->getModelBasisBody( f ), true, 0 );
   Trace("sel-form") << "Selection formula for " << f << " is " << s << std::endl;
   if( !s.isNull() ){
@@ -580,7 +584,7 @@ int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){
             if( !m.isComplete( f ) ){
               Trace("inst-gen-debug") << "- partial inst" << std::endl;
               //if the instantiation does not yet exist
-              if( d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, mp, true, NULL ) ){
+              if( d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, mp, true ) ){
                 //get the partial instantiation pf
                 Node pf = d_qe->getInstantiation( fp, mp );
                 Trace("inst-gen-pi") << "Partial instantiation of " << f << std::endl;
@@ -732,10 +736,10 @@ bool ModelEngineBuilderInstGen::isUsableSelectionLiteral( Node n, int useOption
 
 Node ModelEngineBuilderInstGen::getParentQuantifier( Node f ){
   std::map< Node, Node >::iterator it = d_sub_quant_parent.find( f );
-  if( it==d_sub_quant_parent.end() ){
+  if( it==d_sub_quant_parent.end() || it->second.isNull() ){
     return f;
   }else{
-    return getParentQuantifier( it->second );
+    return it->second;
   }
 }
 
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 0b73f3c8b..7952d3c21 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -115,7 +115,6 @@ void ModelEngine::check( Theory::Effort e ){
       if( options::produceModels() ){
         // finish building the model in the standard way
         d_builder->buildModel( fm, true );
-        d_quantEngine->d_model_set = true;
       }
       //if the check was incomplete, we must set incomplete flag
       if( d_incomplete_check ){
@@ -256,7 +255,7 @@ int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){
         //if evaluate(...)==1, then the instantiation is already true in the model
         //  depIndex is the index of the least significant variable that this evaluation relies upon
         depIndex = riter.getNumTerms()-1;
-        eval = d_quantEngine->getModel()->evaluate( d_quantEngine->getTermDatabase()->getCounterexampleBody( f ), depIndex, &riter );
+        eval = d_quantEngine->getModel()->evaluate( d_quantEngine->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter );
         if( eval==1 ){
           Debug("fmf-model-eval") << "  Returned success with depIndex = " << depIndex << std::endl;
         }else{
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index f930fbec7..377fe9aa9 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -64,7 +64,6 @@ public:
   void registerQuantifier( Node f );
   void assertNode( Node f );
   Node explain(TNode n){ return Node::null(); }
-  void propagate( Theory::Effort level ){}
   void debugPrint( const char* c );
 public:
   /** statistics class */
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
new file mode 100755
index 000000000..7a2d965b8
--- /dev/null
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -0,0 +1,144 @@
+/*********************                                                        */

+/*! \file quant_util.cpp

+ ** \verbatim

+ ** Original author: ajreynol

+ ** Major contributors: bobot, mdeters

+ ** Minor contributors (to current version): none

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

+ ** Copyright (c) 2009-2012  New York University and The University of Iowa

+ ** See the file COPYING in the top-level source directory for licensing

+ ** information.\endverbatim

+ **

+ ** \brief Implementation of quantifier utilities

+ **/

+

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

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

+

+using namespace std;

+using namespace CVC4;

+using namespace CVC4::kind;

+using namespace CVC4::context;

+using namespace CVC4::theory;

+

+void QuantRelevance::registerQuantifier( Node f ){

+  //compute symbols in f

+  std::vector< Node > syms;

+  computeSymbols( f[1], syms );

+  d_syms[f].insert( d_syms[f].begin(), syms.begin(), syms.end() );

+  //set initial relevance

+  int minRelevance = -1;

+  for( int i=0; i<(int)syms.size(); i++ ){

+    d_syms_quants[ syms[i] ].push_back( f );

+    int r = getRelevance( syms[i] );

+    if( r!=-1 && ( minRelevance==-1 || r<minRelevance ) ){

+      minRelevance = r;

+    }

+  }

+  if( minRelevance!=-1 ){

+    setRelevance( f, minRelevance+1 );

+  }

+}

+

+

+/** compute symbols */

+void QuantRelevance::computeSymbols( Node n, std::vector< Node >& syms ){

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

+    Node op = n.getOperator();

+    if( std::find( syms.begin(), syms.end(), op )==syms.end() ){

+      syms.push_back( op );

+    }

+  }

+  if( n.getKind()!=FORALL ){

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

+      computeSymbols( n[i], syms );

+    }

+  }

+}

+

+/** set relevance */

+void QuantRelevance::setRelevance( Node s, int r ){

+  if( d_computeRel ){

+    int rOld = getRelevance( s );

+    if( rOld==-1 || r<rOld ){

+      d_relevance[s] = r;

+      if( s.getKind()==FORALL ){

+        for( int i=0; i<(int)d_syms[s].size(); i++ ){

+          setRelevance( d_syms[s][i], r );

+        }

+      }else{

+        for( int i=0; i<(int)d_syms_quants[s].size(); i++ ){

+          setRelevance( d_syms_quants[s][i], r+1 );

+        }

+      }

+    }

+  }

+}

+

+

+QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){

+  std::map< Node, int > phaseReqs2;

+  computePhaseReqs( n, false, phaseReqs2 );

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

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

+      d_phase_reqs[ it->first ] = true;

+    }else if( it->second==-1 ){

+      d_phase_reqs[ it->first ] = false;

+    }

+  }

+  Debug("inst-engine-phase-req") << "Phase requirements for " << n << ":" << std::endl;

+  //now, compute if any patterns are equality required

+  if( computeEq ){

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

+      Debug("inst-engine-phase-req") << "   " << it->first << " -> " << it->second << std::endl;

+      if( it->first.getKind()==EQUAL ){

+        if( it->first[0].hasAttribute(InstConstantAttribute()) ){

+          if( !it->first[1].hasAttribute(InstConstantAttribute()) ){

+            d_phase_reqs_equality_term[ it->first[0] ] = it->first[1];

+            d_phase_reqs_equality[ it->first[0] ] = it->second;

+            Debug("inst-engine-phase-req") << "      " << it->first[0] << ( it->second ? " == " : " != " ) << it->first[1] << std::endl;

+          }

+        }else if( it->first[1].hasAttribute(InstConstantAttribute()) ){

+          d_phase_reqs_equality_term[ it->first[1] ] = it->first[0];

+          d_phase_reqs_equality[ it->first[1] ] = it->second;

+          Debug("inst-engine-phase-req") << "      " << it->first[1] << ( it->second ? " == " : " != " ) << it->first[0] << std::endl;

+        }

+      }

+    }

+  }

+}

+

+void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int >& phaseReqs ){

+  bool newReqPol = false;

+  bool newPolarity;

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

+    newReqPol = true;

+    newPolarity = !polarity;

+  }else if( n.getKind()==OR || n.getKind()==IMPLIES ){

+    if( !polarity ){

+      newReqPol = true;

+      newPolarity = false;

+    }

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

+    if( polarity ){

+      newReqPol = true;

+      newPolarity = true;

+    }

+  }else{

+    int val = polarity ? 1 : -1;

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

+      phaseReqs[n] = val;

+    }else if( val!=phaseReqs[n] ){

+      phaseReqs[n] = 0;

+    }

+  }

+  if( newReqPol ){

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

+      if( n.getKind()==IMPLIES && i==0 ){

+        computePhaseReqs( n[i], !newPolarity, phaseReqs );

+      }else{

+        computePhaseReqs( n[i], newPolarity, phaseReqs );

+      }

+    }

+  }

+}

diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
new file mode 100755
index 000000000..1479f910e
--- /dev/null
+++ b/src/theory/quantifiers/quant_util.h
@@ -0,0 +1,77 @@
+/*********************                                                        */

+/*! \file quant_util.h

+ ** \verbatim

+ ** Original author: ajreynol

+ ** Major contributors: none

+ ** Minor contributors (to current version): mdeters, bobot

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

+ ** Copyright (c) 2009-2012  New York University and The University of Iowa

+ ** See the file COPYING in the top-level source directory for licensing

+ ** information.\endverbatim

+ **

+ ** \brief quantifier util

+ **/

+

+#include "cvc4_private.h"

+

+#ifndef __CVC4__THEORY__QUANT_UTIL_H

+#define __CVC4__THEORY__QUANT_UTIL_H

+

+#include "theory/theory.h"

+

+#include <ext/hash_set>

+#include <iostream>

+#include <map>

+

+namespace CVC4 {

+namespace theory {

+

+

+class QuantRelevance

+{

+private:

+  /** for computing relavance */

+  bool d_computeRel;

+  /** map from quantifiers to symbols they contain */

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

+  /** map from symbols to quantifiers */

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

+  /** relevance for quantifiers and symbols */

+  std::map< Node, int > d_relevance;

+  /** compute symbols */

+  void computeSymbols( Node n, std::vector< Node >& syms );

+public:

+  QuantRelevance( bool cr ) : d_computeRel( cr ){}

+  ~QuantRelevance(){}

+  /** register quantifier */

+  void registerQuantifier( Node f );

+  /** set relevance */

+  void setRelevance( Node s, int r );

+  /** get relevance */

+  int getRelevance( Node s ) { return d_relevance.find( s )==d_relevance.end() ? -1 : d_relevance[s]; }

+  /** get number of quantifiers for symbol s */

+  int getNumQuantifiersForSymbol( Node s ) { return (int)d_syms_quants[s].size(); }

+};

+

+class QuantPhaseReq

+{

+private:

+  /** helper functions compute phase requirements */

+  void computePhaseReqs( Node n, bool polarity, std::map< Node, int >& phaseReqs );

+public:

+  QuantPhaseReq( Node n, bool computeEq = false );

+  ~QuantPhaseReq(){}

+  /** is phase required */

+  bool isPhaseReq( Node lit ) { return d_phase_reqs.find( lit )!=d_phase_reqs.end(); }

+  /** get phase requirement */

+  bool getPhaseReq( Node lit ) { return d_phase_reqs.find( lit )==d_phase_reqs.end() ? false : d_phase_reqs[ lit ]; }

+  /** phase requirements for each quantifier for each instantiation literal */

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

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

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

+};

+

+}

+}

+

+#endif

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index d21ea252c..7bf1f30e9 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -281,11 +281,10 @@ Node QuantifiersRewriter::computeNNF( Node body ){
 
 Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){
   //Notice() << "Compute var elimination for " << f << std::endl;
-  std::map< Node, bool > litPhaseReq;
-  QuantifiersEngine::computePhaseReqs( body, false, litPhaseReq );
+  QuantPhaseReq qpr( body );
   std::vector< Node > vars;
   std::vector< Node > subs;
-  for( std::map< Node, bool >::iterator it = litPhaseReq.begin(); it != litPhaseReq.end(); ++it ){
+  for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){
     //Notice() << "   " << it->first << " -> " << ( it->second ? "true" : "false" ) << std::endl;
     if( it->first.getKind()==EQUAL ){
       if( it->second ){
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 5261e6876..7b4440c31 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -72,12 +72,12 @@ void RelevantDomain::compute(){
     for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){
       Node f = d_model->getAssertedQuantifier( i );
       //compute the domain of relevant instantiations (rule 3 of complete instantiation, essentially uf fragment)
-      if( computeRelevantInstantiationDomain( d_qe->getTermDatabase()->getCounterexampleBody( f ), Node::null(), -1, f ) ){
+      if( computeRelevantInstantiationDomain( d_qe->getTermDatabase()->getInstConstantBody( f ), Node::null(), -1, f ) ){
         success = false;
       }
       //extend the possible domain for functions (rule 2 of complete instantiation, essentially uf fragment)
       RepDomain range;
-      if( extendFunctionDomains( d_qe->getTermDatabase()->getCounterexampleBody( f ), range ) ){
+      if( extendFunctionDomains( d_qe->getTermDatabase()->getInstConstantBody( f ), range ) ){
         success = false;
       }
     }
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 0614bb22a..c8c884974 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -259,7 +259,7 @@ Node TermDb::getModelBasis( Node f, Node n ){
 
 Node TermDb::getModelBasisBody( Node f ){
   if( d_model_basis_body.find( f )==d_model_basis_body.end() ){
-    Node n = getCounterexampleBody( f );
+    Node n = getInstConstantBody( f );
     d_model_basis_body[f] = getModelBasis( f, n );
   }
   return d_model_basis_body[f];
@@ -301,17 +301,6 @@ void TermDb::makeInstantiationConstantsFor( Node f ){
   }
 }
 
-void TermDb::setInstantiationLevelAttr( Node n, uint64_t level ){
-  if( !n.hasAttribute(InstLevelAttribute()) ){
-    InstLevelAttribute ila;
-    n.setAttribute(ila,level);
-  }
-  for( int i=0; i<(int)n.getNumChildren(); i++ ){
-    setInstantiationLevelAttr( n[i], level );
-  }
-}
-
-
 void TermDb::setInstantiationConstantAttr( Node n, Node f ){
   if( !n.hasAttribute(InstConstantAttribute()) ){
     bool setAttr = false;
@@ -336,18 +325,49 @@ void TermDb::setInstantiationConstantAttr( Node n, Node f ){
 }
 
 
-Node TermDb::getCounterexampleBody( Node f ){
-  std::map< Node, Node >::iterator it = d_counterexample_body.find( f );
-  if( it==d_counterexample_body.end() ){
+Node TermDb::getInstConstantBody( Node f ){
+  std::map< Node, Node >::iterator it = d_inst_const_body.find( f );
+  if( it==d_inst_const_body.end() ){
     makeInstantiationConstantsFor( f );
-    Node n = getSubstitutedNode( f[1], f );
-    d_counterexample_body[ f ] = n;
+    Node n = getInstConstantNode( f[1], f );
+    d_inst_const_body[ f ] = n;
     return n;
   }else{
     return it->second;
   }
 }
 
+Node TermDb::getCounterexampleLiteral( Node f ){
+  if( d_ce_lit.find( f )==d_ce_lit.end() ){
+    Node ceBody = getInstConstantBody( f );
+    Node ceLit = d_quantEngine->getValuation().ensureLiteral( ceBody.notNode() );
+    d_ce_lit[ f ] = ceLit;
+    setInstantiationConstantAttr( ceLit, f );
+  }
+  return d_ce_lit[ f ];
+}
+
+Node TermDb::getInstConstantNode( Node n, Node f ){
+  return convertNodeToPattern(n,f,d_vars[f],d_inst_constants[ f ]);
+}
+
+Node TermDb::convertNodeToPattern( Node n, Node f, const std::vector<Node> & vars,
+                                              const std::vector<Node> & inst_constants){
+  Node n2 = n.substitute( vars.begin(), vars.end(),
+                          inst_constants.begin(),
+                          inst_constants.end() );
+  setInstantiationConstantAttr( n2, f );
+  return n2;
+}
+
+Node TermDb::mkNodeInstConstant( Kind k, std::vector< Node >& children, Node f ){
+  Node n = NodeManager::currentNM()->mkNode( k, children );
+  setInstantiationConstantAttr( n, f );
+  return n;
+}
+
+
+
 Node TermDb::getSkolemizedBody( Node f ){
   Assert( f.getKind()==FORALL );
   if( d_skolem_body.find( f )==d_skolem_body.end() ){
@@ -367,17 +387,14 @@ Node TermDb::getSkolemizedBody( Node f ){
 }
 
 
-Node TermDb::getSubstitutedNode( Node n, Node f ){
-  return convertNodeToPattern(n,f,d_vars[f],d_inst_constants[ f ]);
-}
-
-Node TermDb::convertNodeToPattern( Node n, Node f, const std::vector<Node> & vars,
-                                              const std::vector<Node> & inst_constants){
-  Node n2 = n.substitute( vars.begin(), vars.end(),
-                          inst_constants.begin(),
-                          inst_constants.end() );
-  setInstantiationConstantAttr( n2, f );
-  return n2;
+void TermDb::setInstantiationLevelAttr( Node n, uint64_t level ){
+  if( !n.hasAttribute(InstLevelAttribute()) ){
+    InstLevelAttribute ila;
+    n.setAttribute(ila,level);
+  }
+  for( int i=0; i<(int)n.getNumChildren(); i++ ){
+    setInstantiationLevelAttr( n[i], level );
+  }
 }
 
 Node TermDb::getFreeVariableForInstConstant( Node n ){
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 64f3d4980..d63eebf7e 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -109,6 +109,8 @@ public:
   /* Todo replace int by size_t */
   std::hash_map< Node, std::hash_map< Node, std::hash_map< int, std::vector< Node >  >, NodeHashFunction  > , NodeHashFunction > d_parents;
   const std::vector<Node> & getParents(TNode n, TNode f, int arg);
+
+//for model basis
 private:
   //map from types to model basis terms
   std::map< TypeNode, Node > d_model_basis_term;
@@ -116,6 +118,8 @@ private:
   std::map< Node, Node > d_model_basis_op_term;
   //map from instantiation terms to their model basis equivalent
   std::map< Node, Node > d_model_basis_body;
+  /** map from universal quantifiers to model basis terms */
+  std::map< Node, std::vector< Node > > d_model_basis_terms;
   // compute model basis arg
   void computeModelBasisArgAttribute( Node n );
 public:
@@ -127,46 +131,37 @@ public:
   Node getModelBasis( Node f, Node n );
   //get model basis body
   Node getModelBasisBody( Node f );
+
+//for inst constant
 private:
-  /** map from universal quantifiers to the list of variables */
-  std::map< Node, std::vector< Node > > d_vars;
-  /** map from universal quantifiers to the list of skolem constants */
-  std::map< Node, std::vector< Node > > d_skolem_constants;
-  /** model basis terms */
-  std::map< Node, std::vector< Node > > d_model_basis_terms;
-  /** map from universal quantifiers to their skolemized body */
-  std::map< Node, Node > d_skolem_body;
+  /** map from universal quantifiers to the list of instantiation constants */
+  std::map< Node, std::vector< Node > > d_inst_constants;
+  /** map from universal quantifiers to their inst constant body */
+  std::map< Node, Node > d_inst_const_body;
+  /** map from universal quantifiers to their counterexample literals */
+  std::map< Node, Node > d_ce_lit;
   /** instantiation constants to universal quantifiers */
   std::map< Node, Node > d_inst_constants_map;
-  /** map from universal quantifiers to their counterexample body */
-  std::map< Node, Node > d_counterexample_body;
-  /** free variable for instantiation constant type */
-  std::map< TypeNode, Node > d_free_vars;
-private:
   /** make instantiation constants for */
   void makeInstantiationConstantsFor( Node f );
-public:
-  /** map from universal quantifiers to the list of instantiation constants */
-  std::map< Node, std::vector< Node > > d_inst_constants;
-  /** set instantiation level attr */
-  void setInstantiationLevelAttr( Node n, uint64_t level );
   /** set instantiation constant attr */
   void setInstantiationConstantAttr( Node n, Node f );
+public:
   /** get the i^th instantiation constant of f */
   Node getInstantiationConstant( Node f, int i ) { return d_inst_constants[f][i]; }
   /** get number of instantiation constants for f */
   int getNumInstantiationConstants( Node f ) { return (int)d_inst_constants[f].size(); }
   /** get the ce body f[e/x] */
-  Node getCounterexampleBody( Node f );
-  /** get the skolemized body f[e/x] */
-  Node getSkolemizedBody( Node f );
+  Node getInstConstantBody( Node f );
+  /** get counterexample literal (for cbqi) */
+  Node getCounterexampleLiteral( Node f );
   /** returns node n with bound vars of f replaced by instantiation constants of f
       node n : is the futur pattern
       node f : is the quantifier containing which bind the variable
       return a pattern where the variable are replaced by variable for
       instantiation.
    */
-  Node getSubstitutedNode( Node n, Node f );
+  Node getInstConstantNode( Node n, Node f );
   /** same as before but node f is just linked to the new pattern by the
       applied attribute
       vars the bind variable
@@ -175,15 +170,37 @@ public:
   Node convertNodeToPattern( Node n, Node f,
                              const std::vector<Node> & vars,
                              const std::vector<Node> & nvars);
+  /** get iff term */
+  Node getInstConstantIffTerm( Node n, bool pol );
+  /** make node, validating the inst constant attribute */
+  Node mkNodeInstConstant( Kind k, std::vector< Node >& children, Node f );
+
+//for skolem
+private:
+  /** map from universal quantifiers to the list of skolem constants */
+  std::map< Node, std::vector< Node > > d_skolem_constants;
+  /** map from universal quantifiers to their skolemized body */
+  std::map< Node, Node > d_skolem_body;
+public:
+  /** get the skolemized body f[e/x] */
+  Node getSkolemizedBody( Node f );
+
+//miscellaneous
+private:
+  /** map from universal quantifiers to the list of variables */
+  std::map< Node, std::vector< Node > > d_vars;
+  /** free variable for instantiation constant type */
+  std::map< TypeNode, Node > d_free_vars;
+public:
   /** get free variable for instantiation constant */
   Node getFreeVariableForInstConstant( Node n );
+  /** set instantiation level attr */
+  void setInstantiationLevelAttr( Node n, uint64_t level );
 
 //for triggers
 private:
   /** helper function for compute var contains */
   void computeVarContains2( Node n, Node parent );
-  /** all triggers will be stored in this trie */
-  TrTrie d_tr_trie;
   /** var contains */
   std::map< TNode, std::vector< TNode > > d_var_contains;
 public:
@@ -195,6 +212,10 @@ public:
   void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains );
   /** get var contains for node n */
   void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains );
+private:
+  /** all triggers will be stored in this trie */
+  TrTrie d_tr_trie;
+public:
   /** get trigger */
   inst::Trigger* getTrigger( std::vector< Node >& nodes ){ return d_tr_trie.getTrigger( nodes ); }
   /** add trigger */
diff --git a/src/theory/quantifiers/theory_quantifiers_instantiator.cpp b/src/theory/quantifiers/theory_quantifiers_instantiator.cpp
index fc5c66b94..eabb4ceda 100644
--- a/src/theory/quantifiers/theory_quantifiers_instantiator.cpp
+++ b/src/theory/quantifiers/theory_quantifiers_instantiator.cpp
@@ -34,10 +34,10 @@ void InstantiatorTheoryQuantifiers::assertNode( Node assertion ){
   if( options::cbqi() ){
     if( assertion.hasAttribute(InstConstantAttribute()) ){
       Debug("quant-quant-assert") << "   -> has constraints from " << assertion.getAttribute(InstConstantAttribute()) << std::endl;
-      setHasConstraintsFrom( assertion.getAttribute(InstConstantAttribute()) );
+      setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) );
     }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
       Debug("quant-quant-assert") << "   -> has constraints from " << assertion[0].getAttribute(InstConstantAttribute()) << std::endl;
-      setHasConstraintsFrom( assertion[0].getAttribute(InstConstantAttribute()) );
+      setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) );
     }
   }
 }
@@ -53,11 +53,9 @@ int InstantiatorTheoryQuantifiers::process( Node f, Theory::Effort effort, int e
     return InstStrategy::STATUS_UNFINISHED;
   }else if( e==5 ){
     //add random addition
-    if( isOwnerOf( f ) ){
-      InstMatch m;
-      if( d_quantEngine->addInstantiation( f, m ) ){
-        ++(d_statistics.d_instantiations);
-      }
+    InstMatch m;
+    if( d_quantEngine->addInstantiation( f, m ) ){
+      ++(d_statistics.d_instantiations);
     }
   }
   return InstStrategy::STATUS_UNKNOWN;
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 4d7e93ef2..9d7c8e315 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -34,35 +34,9 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::inst;
 
-//#define COMPUTE_RELEVANCE
-//#define REWRITE_ASSERTED_QUANTIFIERS
-
-  /** reset instantiation */
-void InstStrategy::resetInstantiationRound( Theory::Effort effort ){
-  d_no_instantiate_temp.clear();
-  d_no_instantiate_temp.insert( d_no_instantiate_temp.begin(), d_no_instantiate.begin(), d_no_instantiate.end() );
-  processResetInstantiationRound( effort );
-}
-
-/** do instantiation round method */
-int InstStrategy::doInstantiation( Node f, Theory::Effort effort, int e ){
-  if( shouldInstantiate( f ) ){
-    int origLemmas = d_quantEngine->getNumLemmasWaiting();
-    int retVal = process( f, effort, e );
-    if( d_quantEngine->getNumLemmasWaiting()!=origLemmas ){
-      for( int i=0; i<(int)d_priority_over.size(); i++ ){
-        d_priority_over[i]->d_no_instantiate_temp.push_back( f );
-      }
-    }
-    return retVal;
-  }else{
-    return STATUS_UNKNOWN;
-  }
-}
-
 QuantifiersEngine::QuantifiersEngine(context::Context* c, TheoryEngine* te):
 d_te( te ),
-d_active( c ){
+d_quant_rel( false ){ //currently do not care about relevance
   d_eq_query = new EqualityQueryQuantifiersEngine( this );
   d_term_db = new quantifiers::TermDb( this );
   d_hasAddedLemma = false;
@@ -122,8 +96,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
   CodeTimer codeTimer(d_time);
 
   d_hasAddedLemma = false;
-  d_model_set = false;
-  d_resetInstRound = false;
   if( e==Theory::EFFORT_LAST_CALL ){
     ++(d_statistics.d_instantiation_rounds_lc);
   }else if( e==Theory::EFFORT_FULL ){
@@ -141,7 +113,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
   }
   //build the model if not done so already
   //  this happens if no quantifiers are currently asserted and no model-building module is enabled
-  if( options::produceModels() && e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma && !d_model_set ){
+  if( options::produceModels() && e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma && !d_model->isModelSet() ){
     d_te->getModelBuilder()->buildModel( d_model, true );
   }
 }
@@ -161,68 +133,23 @@ std::vector<Node> QuantifiersEngine::createInstVariable( std::vector<Node> & var
 void QuantifiersEngine::registerQuantifier( Node f ){
   if( std::find( d_quants.begin(), d_quants.end(), f )==d_quants.end() ){
     d_quants.push_back( f );
-    std::vector< Node > quants;
-#ifdef REWRITE_ASSERTED_QUANTIFIERS
-    //do assertion-time rewriting of quantifier
-    Node nf = quantifiers::QuantifiersRewriter::rewriteQuant( f, false, false );
-    if( nf!=f ){
-      Debug("quantifiers-rewrite") << "*** assert-rewrite " << f << std::endl;
-      Debug("quantifiers-rewrite") << " to " << std::endl;
-      Debug("quantifiers-rewrite") << nf << std::endl;
-      //we will instead register all the rewritten quantifiers
-      if( nf.getKind()==FORALL ){
-        quants.push_back( nf );
-      }else if( nf.getKind()==AND ){
-        for( int i=0; i<(int)nf.getNumChildren(); i++ ){
-          quants.push_back( nf[i] );
-        }
-      }else{
-        //unhandled: rewrite must go to a quantifier, or conjunction of quantifiers
-        Assert( false );
-      }
-    }else{
-      quants.push_back( f );
+
+    ++(d_statistics.d_num_quant);
+    Assert( f.getKind()==FORALL );
+    //make instantiation constants for f
+    d_term_db->makeInstantiationConstantsFor( f );
+    //register with quantifier relevance
+    d_quant_rel.registerQuantifier( f );
+    //register with each module
+    for( int i=0; i<(int)d_modules.size(); i++ ){
+      d_modules[i]->registerQuantifier( f );
     }
-#else
-    quants.push_back( f );
-#endif
-    for( int q=0; q<(int)quants.size(); q++ ){
-      d_quant_rewritten[f].push_back( quants[q] );
-      d_rewritten_quant[ quants[q] ] = f;
-      ++(d_statistics.d_num_quant);
-      Assert( quants[q].getKind()==FORALL );
-      //register quantifier
-      d_r_quants.push_back( quants[q] );
-      //make instantiation constants for quants[q]
-      d_term_db->makeInstantiationConstantsFor( quants[q] );
-      //compute symbols in quants[q]
-      std::vector< Node > syms;
-      computeSymbols( quants[q][1], syms );
-      d_syms[quants[q]].insert( d_syms[quants[q]].begin(), syms.begin(), syms.end() );
-      //set initial relevance
-      int minRelevance = -1;
-      for( int i=0; i<(int)syms.size(); i++ ){
-        d_syms_quants[ syms[i] ].push_back( quants[q] );
-        int r = getRelevance( syms[i] );
-        if( r!=-1 && ( minRelevance==-1 || r<minRelevance ) ){
-          minRelevance = r;
-        }
-      }
-#ifdef COMPUTE_RELEVANCE
-      if( minRelevance!=-1 ){
-        setRelevance( quants[q], minRelevance+1 );
-      }
-#endif
-      //register with each module
-      for( int i=0; i<(int)d_modules.size(); i++ ){
-        d_modules[i]->registerQuantifier( quants[q] );
-      }
-      Node ceBody = d_term_db->getCounterexampleBody( quants[q] );
-      generatePhaseReqs( quants[q], ceBody );
-      //also register it with the strong solver
-      if( options::finiteModelFind() ){
-        ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( quants[q] );
-      }
+    Node ceBody = d_term_db->getInstConstantBody( f );
+    //generate the phase requirements
+    d_phase_reqs[f] = new QuantPhaseReq( ceBody, true );
+    //also register it with the strong solver
+    if( options::finiteModelFind() ){
+      ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f );
     }
   }
 }
@@ -236,11 +163,9 @@ void QuantifiersEngine::registerPattern( std::vector<Node> & pattern) {
 
 void QuantifiersEngine::assertNode( Node f ){
   Assert( f.getKind()==FORALL );
-  for( int j=0; j<(int)d_quant_rewritten[f].size(); j++ ){
-    d_model->assertQuantifier( d_quant_rewritten[f][j] );
-    for( int i=0; i<(int)d_modules.size(); i++ ){
-      d_modules[i]->assertNode( d_quant_rewritten[f][j] );
-    }
+  d_model->assertQuantifier( f );
+  for( int i=0; i<(int)d_modules.size(); i++ ){
+    d_modules[i]->assertNode( f );
   }
 }
 
@@ -263,15 +188,12 @@ Node QuantifiersEngine::getNextDecisionRequest(){
 }
 
 void QuantifiersEngine::resetInstantiationRound( Theory::Effort level ){
-  //if( !d_resetInstRound ){
-  d_resetInstRound = true;
   for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){
     if( getInstantiator( i ) ){
       getInstantiator( i )->resetInstantiationRound( level );
     }
   }
   getTermDatabase()->reset( level );
-  //}
 }
 
 void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){
@@ -281,16 +203,12 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){
     uf::InstantiatorTheoryUf* d_ith = (uf::InstantiatorTheoryUf*)getInstantiator( THEORY_UF );
     d_ith->newTerms(added);
   }
-#ifdef COMPUTE_RELEVANCE
   //added contains also the Node that just have been asserted in this branch
-  for( std::set< Node >::iterator i=added.begin(), end=added.end();
-       i!=end; i++ ){
+  for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){
     if( !withinQuant ){
-      setRelevance( i->getOperator(), 0 );
+      d_quant_rel.setRelevance( i->getOperator(), 0 );
     }
   }
-#endif
-
 }
 
 void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms ){
@@ -316,7 +234,7 @@ Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& vars, std
     }
     Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, uninst_vars );
     body = NodeManager::currentNM()->mkNode( FORALL, bvl, body );
-    Trace("partial-inst") << "Partial instantiation : " << d_rewritten_quant[f] << std::endl;
+    Trace("partial-inst") << "Partial instantiation : " << f << std::endl;
     Trace("partial-inst") << "                      : " << body << std::endl;
   }
   return body;
@@ -330,7 +248,7 @@ Node QuantifiersEngine::getInstantiation( Node f, InstMatch& m ){
 }
 
 bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){
-  return d_inst_match_trie[f].existsInstMatch( this, f, m, modEq, NULL, modInst );
+  return d_inst_match_trie[f].existsInstMatch( this, f, m, modEq, modInst );
 }
 
 bool QuantifiersEngine::addLemma( Node lem ){
@@ -355,7 +273,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std
   Node body = getInstantiation( f, vars, terms );
   //make the lemma
   NodeBuilder<> nb(kind::OR);
-  nb << d_rewritten_quant[f].notNode() << body;
+  nb << f.notNode() << body;
   Node lem = nb;
   //check for duplication
   if( addLemma( lem ) ){
@@ -462,15 +380,17 @@ void QuantifiersEngine::flushLemmas( OutputChannel* out ){
 }
 
 void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){
-  if( options::literalMatchMode()!=quantifiers::LITERAL_MATCH_NONE ){
-    bool printed = false;
+  if( options::literalMatchMode()!=quantifiers::LITERAL_MATCH_NONE && d_phase_reqs.find( f )!=d_phase_reqs.end() ){
     // doing literal-based matching (consider polarity of literals)
     for( int i=0; i<(int)nodes.size(); i++ ){
       Node prev = nodes[i];
       bool nodeChanged = false;
-      if( isPhaseReq( f, nodes[i] ) ){
-        bool preq = getPhaseReq( f, nodes[i] );
-        nodes[i] = NodeManager::currentNM()->mkNode( IFF, nodes[i], NodeManager::currentNM()->mkConst<bool>(preq) );
+      if( d_phase_reqs[f]->isPhaseReq( nodes[i] ) ){
+        bool preq = d_phase_reqs[f]->getPhaseReq( nodes[i] );
+        std::vector< Node > children;
+        children.push_back( nodes[i] );
+        children.push_back( NodeManager::currentNM()->mkConst<bool>(preq) );
+        nodes[i] = d_term_db->mkNodeInstConstant( IFF, children, f );
         nodeChanged = true;
       }
       //else if( qe->isPhaseReqEquality( f, trNodes[i] ) ){
@@ -478,13 +398,7 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){
       //  trNodes[i] = NodeManager::currentNM()->mkNode( EQUAL, trNodes[i], req );
       //}
       if( nodeChanged ){
-        if( !printed ){
-          Debug("literal-matching") << "LitMatch for " << f << ":" << std::endl;
-          printed = true;
-        }
         Debug("literal-matching") << "  Make " << prev << " -> " << nodes[i] << std::endl;
-        Assert( prev.hasAttribute(InstConstantAttribute()) );
-        d_term_db->setInstantiationConstantAttr( nodes[i], prev.getAttribute(InstConstantAttribute()) );
         ++(d_statistics.d_lit_phase_req);
       }else{
         ++(d_statistics.d_lit_phase_nreq);
@@ -495,76 +409,6 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){
   }
 }
 
-void QuantifiersEngine::computePhaseReqs2( Node n, bool polarity, std::map< Node, int >& phaseReqs ){
-  bool newReqPol = false;
-  bool newPolarity;
-  if( n.getKind()==NOT ){
-    newReqPol = true;
-    newPolarity = !polarity;
-  }else if( n.getKind()==OR || n.getKind()==IMPLIES ){
-    if( !polarity ){
-      newReqPol = true;
-      newPolarity = false;
-    }
-  }else if( n.getKind()==AND ){
-    if( polarity ){
-      newReqPol = true;
-      newPolarity = true;
-    }
-  }else{
-    int val = polarity ? 1 : -1;
-    if( phaseReqs.find( n )==phaseReqs.end() ){
-      phaseReqs[n] = val;
-    }else if( val!=phaseReqs[n] ){
-      phaseReqs[n] = 0;
-    }
-  }
-  if( newReqPol ){
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      if( n.getKind()==IMPLIES && i==0 ){
-        computePhaseReqs2( n[i], !newPolarity, phaseReqs );
-      }else{
-        computePhaseReqs2( n[i], newPolarity, phaseReqs );
-      }
-    }
-  }
-}
-
-void QuantifiersEngine::computePhaseReqs( Node n, bool polarity, std::map< Node, bool >& phaseReqs ){
-  std::map< Node, int > phaseReqs2;
-  computePhaseReqs2( n, polarity, phaseReqs2 );
-  for( std::map< Node, int >::iterator it = phaseReqs2.begin(); it != phaseReqs2.end(); ++it ){
-    if( it->second==1 ){
-      phaseReqs[ it->first ] = true;
-    }else if( it->second==-1 ){
-      phaseReqs[ it->first ] = false;
-    }
-  }
-}
-
-void QuantifiersEngine::generatePhaseReqs( Node f, Node n ){
-  computePhaseReqs( n, false, d_phase_reqs[f] );
-  Debug("inst-engine-phase-req") << "Phase requirements for " << f << ":" << std::endl;
-  //now, compute if any patterns are equality required
-  for( std::map< Node, bool >::iterator it = d_phase_reqs[f].begin(); it != d_phase_reqs[f].end(); ++it ){
-    Debug("inst-engine-phase-req") << "   " << it->first << " -> " << it->second << std::endl;
-    if( it->first.getKind()==EQUAL ){
-      if( it->first[0].hasAttribute(InstConstantAttribute()) ){
-        if( !it->first[1].hasAttribute(InstConstantAttribute()) ){
-          d_phase_reqs_equality_term[f][ it->first[0] ] = it->first[1];
-          d_phase_reqs_equality[f][ it->first[0] ] = it->second;
-          Debug("inst-engine-phase-req") << "      " << it->first[0] << ( it->second ? " == " : " != " ) << it->first[1] << std::endl;
-        }
-      }else if( it->first[1].hasAttribute(InstConstantAttribute()) ){
-        d_phase_reqs_equality_term[f][ it->first[1] ] = it->first[0];
-        d_phase_reqs_equality[f][ it->first[1] ] = it->second;
-        Debug("inst-engine-phase-req") << "      " << it->first[1] << ( it->second ? " == " : " != " ) << it->first[0] << std::endl;
-      }
-    }
-  }
-
-}
-
 QuantifiersEngine::Statistics::Statistics():
   d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
   d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
@@ -644,39 +488,6 @@ QuantifiersEngine::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_multi_candidates_cache_miss);
 }
 
-/** compute symbols */
-void QuantifiersEngine::computeSymbols( Node n, std::vector< Node >& syms ){
-  if( n.getKind()==APPLY_UF ){
-    Node op = n.getOperator();
-    if( std::find( syms.begin(), syms.end(), op )==syms.end() ){
-      syms.push_back( op );
-    }
-  }
-  if( n.getKind()!=FORALL ){
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      computeSymbols( n[i], syms );
-    }
-  }
-}
-
-/** set relevance */
-void QuantifiersEngine::setRelevance( Node s, int r ){
-  int rOld = getRelevance( s );
-  if( rOld==-1 || r<rOld ){
-    d_relevance[s] = r;
-    if( s.getKind()==FORALL ){
-      for( int i=0; i<(int)d_syms[s].size(); i++ ){
-        setRelevance( d_syms[s][i], r );
-      }
-    }else{
-      for( int i=0; i<(int)d_syms_quants[s].size(); i++ ){
-        setRelevance( d_syms_quants[s][i], r+1 );
-      }
-    }
-  }
-}
-
-
 
 bool EqualityQueryQuantifiersEngine::hasTerm( Node a ){
   eq::EqualityEngine* ee = d_qe->getTheoryEngine()->getSharedTermsDatabase()->getEqualityEngine();
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index d0c5832ff..62e5d983e 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -21,6 +21,7 @@
 #include "util/hash.h"
 #include "theory/quantifiers/inst_match.h"
 #include "theory/rewriterules/rr_inst_match.h"
+#include "theory/quantifiers/quant_util.h"
 
 #include "util/statistics_registry.h"
 
@@ -36,57 +37,6 @@ namespace theory {
 
 class QuantifiersEngine;
 
-class InstStrategy {
-public:
-  enum Status {
-    STATUS_UNFINISHED,
-    STATUS_UNKNOWN,
-    STATUS_SAT,
-  };/* enum Status */
-protected:
-  /** reference to the instantiation engine */
-  QuantifiersEngine* d_quantEngine;
-protected:
-  /** giving priorities */
-  std::vector< InstStrategy* > d_priority_over;
-  /** do not instantiate list */
-  std::vector< Node > d_no_instantiate;
-  std::vector< Node > d_no_instantiate_temp;
-  /** reset instantiation */
-  virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
-  /** process method */
-  virtual int process( Node f, Theory::Effort effort, int e ) = 0;
-public:
-  InstStrategy( QuantifiersEngine* ie ) : d_quantEngine( ie ){}
-  virtual ~InstStrategy(){}
-
-  /** reset instantiation */
-  void resetInstantiationRound( Theory::Effort effort );
-  /** do instantiation round method */
-  int doInstantiation( Node f, Theory::Effort effort, int e );
-  /** update status */
-  static void updateStatus( int& currStatus, int addStatus ){
-    if( addStatus==STATUS_UNFINISHED ){
-      currStatus = STATUS_UNFINISHED;
-    }else if( addStatus==STATUS_UNKNOWN ){
-      if( currStatus==STATUS_SAT ){
-        currStatus = STATUS_UNKNOWN;
-      }
-    }
-  }
-  /** identify */
-  virtual std::string identify() const { return std::string("Unknown"); }
-public:
-  /** set priority */
-  void setPriorityOver( InstStrategy* is ) { d_priority_over.push_back( is ); }
-  /** set no instantiate */
-  void setNoInstantiate( Node n ) { d_no_instantiate.push_back( n ); }
-  /** should instantiate */
-  bool shouldInstantiate( Node n ) {
-    return std::find( d_no_instantiate_temp.begin(), d_no_instantiate_temp.end(), n )==d_no_instantiate_temp.end();
-  }
-};/* class InstStrategy */
-
 class QuantifiersModule {
 protected:
   QuantifiersEngine* d_quantEngine;
@@ -129,13 +79,13 @@ private:
   quantifiers::ModelEngine* d_model_engine;
   /** equality query class */
   EqualityQuery* d_eq_query;
-public:
+  /** for computing relevance of quantifiers */
+  QuantRelevance d_quant_rel;
+  /** phase requirements for each quantifier for each instantiation literal */
+  std::map< Node, QuantPhaseReq* > d_phase_reqs;
+private:
   /** list of all quantifiers (pre-rewrite) */
   std::vector< Node > d_quants;
-  /** list of all quantifiers (post-rewrite) */
-  std::vector< Node > d_r_quants;
-  /** map from quantifiers to whether they are active */
-  BoolMap d_active;
   /** lemmas produced */
   std::map< Node, bool > d_lemmas_produced;
   /** lemmas waiting */
@@ -150,30 +100,8 @@ public:
   quantifiers::TermDb* d_term_db;
   /** extended model object */
   quantifiers::FirstOrderModel* d_model;
-  /** has the model been set? */
-  bool d_model_set;
-  /** has resetInstantiationRound() been called on this check(...) */
-  bool d_resetInstRound;
-  /** universal quantifiers that have been rewritten */
-  std::map< Node, std::vector< Node > > d_quant_rewritten;
-  /** map from rewritten universal quantifiers to the quantifier they are the consequence of */
-  std::map< Node, Node > d_rewritten_quant;
 private:
-  /** for computing relavance */
-  /** map from quantifiers to symbols they contain */
-  std::map< Node, std::vector< Node > > d_syms;
-  /** map from symbols to quantifiers */
-  std::map< Node, std::vector< Node > > d_syms_quants;
-  /** relevance for quantifiers and symbols */
-  std::map< Node, int > d_relevance;
-  /** compute symbols */
-  void computeSymbols( Node n, std::vector< Node >& syms );
-private:
-  /** helper functions compute phase requirements */
-  static void computePhaseReqs2( Node n, bool polarity, std::map< Node, int >& phaseReqs );
-
   KEEP_STATISTIC(TimerStat, d_time, "theory::QuantifiersEngine::time");
-
 public:
   QuantifiersEngine(context::Context* c, TheoryEngine* te);
   ~QuantifiersEngine();
@@ -184,9 +112,7 @@ public:
   /** get equality query object for the given type. The default is the
       generic one */
   inst::EqualityQuery* getEqualityQuery(TypeNode t);
-  inst::EqualityQuery* getEqualityQuery() {
-    return d_eq_query;
-  }
+  inst::EqualityQuery* getEqualityQuery() { return d_eq_query; }
   /** get equality query object for the given type. The default is the
       one of UF */
   rrinst::CandidateGenerator* getRRCanGenClasses(TypeNode t);
@@ -204,14 +130,20 @@ public:
   OutputChannel& getOutputChannel();
   /** get default valuation for the quantifiers engine */
   Valuation& getValuation();
+  /** get quantifier relevance */
+  QuantRelevance* getQuantifierRelevance() { return &d_quant_rel; }
+  /** 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 */
+  void getPhaseReqTerms( Node f, std::vector< Node >& nodes );
 public:
   /** check at level */
   void check( Theory::Effort e );
-  /** register (non-rewritten) quantifier */
+  /** register quantifier */
   void registerQuantifier( Node f );
-  /** register (non-rewritten) quantifier */
+  /** register quantifier */
   void registerPattern( std::vector<Node> & pattern);
-  /** assert (universal) quantifier */
+  /** assert universal quantifier */
   void assertNode( Node f );
   /** propagate */
   void propagate( Theory::Effort level );
@@ -253,33 +185,6 @@ public:
   int getNumQuantifiers() { return (int)d_quants.size(); }
   /** get quantifier */
   Node getQuantifier( int i ) { return d_quants[i]; }
-  /** set active */
-  void setActive( Node n, bool val ) { d_active[n] = val; }
-  /** get active */
-  bool getActive( Node n ) { return d_active.find( n )!=d_active.end() && d_active[n]; }
-public:
-  /** phase requirements for each quantifier for each instantiation literal */
-  std::map< Node, std::map< Node, bool > > d_phase_reqs;
-  std::map< Node, std::map< Node, bool > > d_phase_reqs_equality;
-  std::map< Node, std::map< Node, Node > > d_phase_reqs_equality_term;
-public:
-  /** is phase required */
-  bool isPhaseReq( Node f, Node lit ) { return d_phase_reqs[f].find( lit )!=d_phase_reqs[f].end(); }
-  /** get phase requirement */
-  bool getPhaseReq( Node f, Node lit ) { return d_phase_reqs[f].find( lit )==d_phase_reqs[f].end() ? false : d_phase_reqs[f][ lit ]; }
-  /** get term req terms */
-  void getPhaseReqTerms( Node f, std::vector< Node >& nodes );
-  /** helper functions compute phase requirements */
-  static void computePhaseReqs( Node n, bool polarity, std::map< Node, bool >& phaseReqs );
-  /** compute phase requirements */
-  void generatePhaseReqs( Node f, Node n );
-public:
-  /** has owner */
-  bool hasOwner( Node f ) { return d_owner.find( f )!=d_owner.end(); }
-  /** get owner */
-  Theory* getOwner( Node f ) { return d_owner[f]; }
-  /** set owner */
-  void setOwner( Node f, Theory* t ) { d_owner[f] = t; }
 public:
   /** get model */
   quantifiers::FirstOrderModel* getModel() { return d_model; }
@@ -287,14 +192,6 @@ public:
   quantifiers::TermDb* getTermDatabase() { return d_term_db; }
   /** add term to database */
   void addTermToDatabase( Node n, bool withinQuant = false );
-private:
-  /** set relevance */
-  void setRelevance( Node s, int r );
-public:
-  /** get relevance */
-  int getRelevance( Node s ) { return d_relevance.find( s )==d_relevance.end() ? -1 : d_relevance[s]; }
-  /** get number of quantifiers for symbol s */
-  int getNumQuantifiersForSymbol( Node s ) { return (int)d_syms_quants[s].size(); }
 public:
   /** statistics class */
   class Statistics {
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 63a493b07..cdad1e19c 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -186,14 +186,14 @@ Instantiator::~Instantiator() {
 void Instantiator::resetInstantiationRound(Theory::Effort effort) {
   for(int i = 0; i < (int) d_instStrategies.size(); ++i) {
     if(isActiveStrategy(d_instStrategies[i])) {
-      d_instStrategies[i]->resetInstantiationRound(effort);
+      d_instStrategies[i]->processResetInstantiationRound(effort);
     }
   }
   processResetInstantiationRound(effort);
 }
 
 int Instantiator::doInstantiation(Node f, Theory::Effort effort, int e ) {
-  if(hasConstraintsFrom(f)) {
+  if( getQuantifierActive(f) ) {
     int status = process(f, effort, e );
     if(d_instStrategies.empty()) {
       Debug("inst-engine-inst") << "There are no instantiation strategies allocated." << endl;
@@ -202,7 +202,7 @@ int Instantiator::doInstantiation(Node f, Theory::Effort effort, int e ) {
         if(isActiveStrategy(d_instStrategies[i])) {
           Debug("inst-engine-inst") << d_instStrategies[i]->identify() << " process " << effort << endl;
           //call the instantiation strategy's process method
-          int s_status = d_instStrategies[i]->doInstantiation( f, effort, e );
+          int s_status = d_instStrategies[i]->process( f, effort, e );
           Debug("inst-engine-inst") << "  -> status is " << s_status << endl;
           InstStrategy::updateStatus(status, s_status);
         } else {
@@ -237,22 +237,6 @@ int Instantiator::doInstantiation(Node f, Theory::Effort effort, int e ) {
 //  }
 //}
 
-void Instantiator::setHasConstraintsFrom(Node f) {
-  d_hasConstraints[f] = true;
-  if(! d_quantEngine->hasOwner(f)) {
-    d_quantEngine->setOwner(f, getTheory());
-  } else if(d_quantEngine->getOwner(f) != getTheory()) {
-    d_quantEngine->setOwner(f, NULL);
-  }
-}
-
-bool Instantiator::hasConstraintsFrom(Node f) {
-  return d_hasConstraints.find(f) != d_hasConstraints.end() && d_hasConstraints[f];
-}
-
-bool Instantiator::isOwnerOf(Node f) {
-  return d_quantEngine->hasOwner(f) && d_quantEngine->getOwner(f) == getTheory();
-}
 
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 44ee06f91..a57f7646d 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -46,7 +46,6 @@ class TheoryEngine;
 namespace theory {
 
 class Instantiator;
-class InstStrategy;
 class QuantifiersEngine;
 class TheoryModel;
 
@@ -794,6 +793,40 @@ namespace eq{
   class EqualityEngine;
 }
 
+/** instantiation strategy class */
+class InstStrategy {
+public:
+  enum Status {
+    STATUS_UNFINISHED,
+    STATUS_UNKNOWN,
+    STATUS_SAT,
+  };/* enum Status */
+protected:
+  /** reference to the instantiation engine */
+  QuantifiersEngine* d_quantEngine;
+public:
+  InstStrategy( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
+  virtual ~InstStrategy(){}
+
+  /** reset instantiation */
+  virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
+  /** process method, returns a status */
+  virtual int process( Node f, Theory::Effort effort, int e ) = 0;
+  /** update status */
+  static void updateStatus( int& currStatus, int addStatus ){
+    if( addStatus==STATUS_UNFINISHED ){
+      currStatus = STATUS_UNFINISHED;
+    }else if( addStatus==STATUS_UNKNOWN ){
+      if( currStatus==STATUS_SAT ){
+        currStatus = STATUS_UNKNOWN;
+      }
+    }
+  }
+  /** identify */
+  virtual std::string identify() const { return std::string("Unknown"); }
+};/* class InstStrategy */
+
+/** instantiator class */
 class Instantiator {
   friend class QuantifiersEngine;
 protected:
@@ -806,7 +839,7 @@ protected:
   /** instantiation strategies active */
   std::map< InstStrategy*, bool > d_instStrategyActive;
   /** has constraints from quantifier */
-  std::map< Node, bool > d_hasConstraints;
+  std::map< Node, bool > d_quantActive;
   /** is instantiation strategy active */
   bool isActiveStrategy( InstStrategy* is ) {
     return d_instStrategyActive.find( is )!=d_instStrategyActive.end() && d_instStrategyActive[is];
@@ -821,13 +854,6 @@ protected:
   /** process quantifier */
   virtual int process( Node f, Theory::Effort effort, int e ) = 0;
 public:
-  /** set has constraints from quantifier f */
-  void setHasConstraintsFrom( Node f );
-  /** has constraints from */
-  bool hasConstraintsFrom( Node f );
-  /** is full owner of quantifier f? */
-  bool isOwnerOf( Node f );
-public:
   Instantiator(context::Context* c, QuantifiersEngine* qe, Theory* th);
   virtual ~Instantiator();
 
@@ -844,6 +870,10 @@ public:
   /** print debug information */
   virtual void debugPrint( const char* c ) {}
 public:
+  /** set has constraints from quantifier f */
+  void setQuantifierActive( Node f ) { d_quantActive[f] = true; }
+  /** has constraints from */
+  bool getQuantifierActive( Node f ) { return d_quantActive.find(f) != d_quantActive.end() && d_quantActive[f]; }
   /** reset instantiation round */
   void resetInstantiationRound( Theory::Effort effort );
   /** do instantiation method*/
diff --git a/src/theory/uf/inst_strategy.cpp b/src/theory/uf/inst_strategy.cpp
index 38211ae28..eef2dac79 100644
--- a/src/theory/uf/inst_strategy.cpp
+++ b/src/theory/uf/inst_strategy.cpp
@@ -36,8 +36,8 @@ using namespace CVC4::theory::inst;
 struct sortQuantifiersForSymbol {
   QuantifiersEngine* d_qe;
   bool operator() (Node i, Node j) {
-    int nqfsi = d_qe->getNumQuantifiersForSymbol( i.getOperator() );
-    int nqfsj = d_qe->getNumQuantifiersForSymbol( j.getOperator() );
+    int nqfsi = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( i.getOperator() );
+    int nqfsj = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( j.getOperator() );
     if( nqfsi<nqfsj ){
       return true;
     }else if( nqfsi>nqfsj ){
@@ -223,14 +223,14 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
     d_patTerms[0][f].clear();
     d_patTerms[1][f].clear();
     std::vector< Node > patTermsF;
-    Trigger::collectPatTerms( d_quantEngine, f, d_quantEngine->getTermDatabase()->getCounterexampleBody( f ), patTermsF, d_tr_strategy, true );
-    Debug("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getCounterexampleBody( f ) << std::endl;
+    Trigger::collectPatTerms( d_quantEngine, f, d_quantEngine->getTermDatabase()->getInstConstantBody( f ), patTermsF, d_tr_strategy, true );
+    Debug("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getInstConstantBody( f ) << std::endl;
     Debug("auto-gen-trigger") << "   ";
     for( int i=0; i<(int)patTermsF.size(); i++ ){
       Debug("auto-gen-trigger") << patTermsF[i] << " ";
     }
     Debug("auto-gen-trigger") << std::endl;
-    //extend to literal matching
+    //extend to literal matching (if applicable)
     d_quantEngine->getPhaseReqTerms( f, patTermsF );
     //sort into single/multi triggers
     std::map< Node, std::vector< Node > > varContains;
@@ -288,7 +288,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
       Debug("relevant-trigger") << "Terms based on relevance: " << std::endl;
       for( int i=0; i<(int)patTerms.size(); i++ ){
         Debug("relevant-trigger") << "   " << patTerms[i] << " (";
-        Debug("relevant-trigger") << d_quantEngine->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl;
+        Debug("relevant-trigger") << d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl;
       }
       //Notice() << "Terms based on relevance: " << std::endl;
       //for( int i=0; i<(int)patTerms.size(); i++ ){
@@ -338,12 +338,12 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
         if( index<(int)patTerms.size() ){
           //Notice() << "check add additional" << std::endl;
           //check if similar patterns exist, and if so, add them additionally
-          int nqfs_curr = d_quantEngine->getNumQuantifiersForSymbol( patTerms[0].getOperator() );
+          int nqfs_curr = d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[0].getOperator() );
           index++;
           bool success = true;
           while( success && index<(int)patTerms.size() && d_is_single_trigger[ patTerms[index] ] ){
             success = false;
-            if( d_quantEngine->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){
+            if( d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){
               d_single_trigger_gen[ patTerms[index] ] = true;
               Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], matchOption, false, Trigger::TR_RETURN_NULL,
                                                  options::smartTriggers() );
diff --git a/src/theory/uf/theory_uf_instantiator.cpp b/src/theory/uf/theory_uf_instantiator.cpp
index 40ac4940b..24da83786 100644
--- a/src/theory/uf/theory_uf_instantiator.cpp
+++ b/src/theory/uf/theory_uf_instantiator.cpp
@@ -126,9 +126,9 @@ void InstantiatorTheoryUf::assertNode( Node assertion )
   d_quantEngine->addTermToDatabase( assertion );
   if( options::cbqi() ){
     if( assertion.hasAttribute(InstConstantAttribute()) ){
-      setHasConstraintsFrom( assertion.getAttribute(InstConstantAttribute()) );
+      setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) );
     }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
-      setHasConstraintsFrom( assertion[0].getAttribute(InstConstantAttribute()) );
+      setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) );
     }
   }
 }
@@ -136,8 +136,8 @@ void InstantiatorTheoryUf::assertNode( Node assertion )
 void InstantiatorTheoryUf::addUserPattern( Node f, Node pat ){
   if( d_isup ){
     d_isup->addUserPattern( f, pat );
+    setQuantifierActive( f );
   }
-  setHasConstraintsFrom( f );
 }