more cleanup of quantifiers code

18 files changed, 405 insertions, 208 deletions

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;