cleaning up some of the equality query stuff, implemented a new representative selection strategy for quantifier instantiation

18 files changed, 234 insertions, 174 deletions

diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 36f265c30..4a89a4dd3 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -91,7 +91,7 @@ void InstMatch::debugPrint( const char* c ){
   //  Debug( c ) << std::endl;
   //}
 }
-
+/*
 void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){
   for( size_t i=0; i<f[0].getNumChildren(); i++ ){
     Node ic = qe->getTermDatabase()->getInstantiationConstant( f, i );
@@ -113,13 +113,15 @@ void InstMatch::makeInternal( QuantifiersEngine* qe ){
     }
   }
 }
-
+*/
 void InstMatch::makeRepresentative( QuantifiersEngine* qe ){
   for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
-    d_map[ it->first ] = qe->getEqualityQuery()->getInternalRepresentative( it->second );
-    if( options::cbqi() && it->second.hasAttribute(InstConstantAttribute()) ){
-      d_map[ it->first ] = qe->getTermDatabase()->getFreeVariableForInstConstant( it->first );
+    if( qe->getEqualityQuery()->getEngine()->hasTerm( it->second ) ){
+      d_map[ it->first ] = qe->getEqualityQuery()->getEngine()->getRepresentative( it->second );
     }
+    //if( options::cbqi() && it->second.hasAttribute(InstConstantAttribute()) ){
+    //  d_map[ it->first ] = qe->getTermDatabase()->getFreeVariableForInstConstant( it->first );
+    //}
   }
 }
 
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index 426adc02d..43c0d26c7 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -55,9 +55,9 @@ public:
   /** is complete? */
   bool isComplete( Node f ) { return d_map.size()==f[0].getNumChildren(); }
   /** make complete */
-  void makeComplete( Node f, QuantifiersEngine* qe );
+  //void makeComplete( Node f, QuantifiersEngine* qe );
   /** make internal: ensure that no term in d_map contains instantiation constants */
-  void makeInternal( QuantifiersEngine* qe );
+  //void makeInternal( QuantifiersEngine* qe );
   /** make representative */
   void makeRepresentative( QuantifiersEngine* qe );
   /** get value */
@@ -96,7 +96,8 @@ public:
     //std::cout << "var.getType() " << var.getType() << "n.getType() " << n.getType() << std::endl ;
     Assert( !var.isNull() );
     Assert( n.isNull() ||// For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations
-            var.getType() == n.getType() );
+            //var.getType() == n.getType()
+            n.getType().isSubtypeOf( var.getType() ) );
     d_map[var] = n;
   }
   size_t size(){ return d_map.size(); }
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 027ac67eb..8d935a323 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -28,7 +28,7 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
 InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete ) :
-QuantifiersModule( qe ), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ){
+QuantifiersModule( qe ), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ), d_performCheck( false ){
 
 }
 
@@ -67,7 +67,12 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
   Debug("inst-engine-ctrl") << "IE: Instantiation Round." << std::endl;
   //reset the quantifiers engine
   Debug("inst-engine-ctrl") << "Reset IE" << std::endl;
-  d_quantEngine->resetInstantiationRound( effort );
+  //reset the instantiators
+  for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){
+    if( d_quantEngine->getInstantiator( i ) ){
+      d_quantEngine->getInstantiator( i )->resetInstantiationRound( effort );
+    }
+  }
   //iterate over an internal effort level e
   int e = 0;
   int eLimit = effort==Theory::EFFORT_LAST_CALL ? 10 : 2;
@@ -125,22 +130,26 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
   }
 }
 
-void InstantiationEngine::check( Theory::Effort e ){
+bool InstantiationEngine::needsCheck( Theory::Effort e ){
   if( e==Theory::EFFORT_FULL ){
     d_ierCounter++;
   }
   //determine if we should perform check, based on instWhenMode
-  bool performCheck = false;
+  d_performCheck = false;
   if( options::instWhenMode()==INST_WHEN_FULL ){
-    performCheck = ( e >= Theory::EFFORT_FULL );
+    d_performCheck = ( e >= Theory::EFFORT_FULL );
   }else if( options::instWhenMode()==INST_WHEN_FULL_LAST_CALL ){
-    performCheck = ( ( e==Theory::EFFORT_FULL  && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL );
+    d_performCheck = ( ( e==Theory::EFFORT_FULL  && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL );
   }else if( options::instWhenMode()==INST_WHEN_LAST_CALL ){
-    performCheck = ( e >= Theory::EFFORT_LAST_CALL );
+    d_performCheck = ( e >= Theory::EFFORT_LAST_CALL );
   }else{
-    performCheck = true;
+    d_performCheck = true;
   }
-  if( performCheck ){
+  return d_performCheck;
+}
+
+void InstantiationEngine::check( Theory::Effort e ){
+  if( d_performCheck ){
     Debug("inst-engine") << "IE: Check " << e << " " << d_ierCounter << std::endl;
     double clSet = 0;
     if( Trace.isOn("inst-engine") ){
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 6d995097a..b3bbbce4a 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -34,6 +34,7 @@ private:
   bool d_setIncomplete;
   /** inst round counter */
   int d_ierCounter;
+  bool d_performCheck;
   /** whether each quantifier is active */
   std::map< Node, bool > d_quant_active;
   /** whether we have added cbqi lemma */
@@ -62,6 +63,7 @@ public:
   InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete = true );
   ~InstantiationEngine(){}
 
+  bool needsCheck( Theory::Effort e );
   void check( Theory::Effort e );
   void registerQuantifier( Node f );
   void assertNode( Node f );
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index f2e195d2e..8b34a3a12 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -33,20 +33,20 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
-bool TermArgBasisTrie::addTerm2( QuantifiersEngine* qe, Node n, int argIndex ){
+bool TermArgBasisTrie::addTerm2( FirstOrderModel* fm, Node n, int argIndex ){
   if( argIndex<(int)n.getNumChildren() ){
     Node r;
     if( n[ argIndex ].getAttribute(ModelBasisAttribute()) ){
       r = n[ argIndex ];
     }else{
-      r = qe->getEqualityQuery()->getRepresentative( n[ argIndex ] );
+      r = fm->getRepresentative( n[ argIndex ] );
     }
     std::map< Node, TermArgBasisTrie >::iterator it = d_data.find( r );
     if( it==d_data.end() ){
-      d_data[r].addTerm2( qe, n, argIndex+1 );
+      d_data[r].addTerm2( fm, n, argIndex+1 );
       return true;
     }else{
-      return it->second.addTerm2( qe, n, argIndex+1 );
+      return it->second.addTerm2( fm, n, argIndex+1 );
     }
   }else{
     return false;
@@ -99,6 +99,7 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) {
         }
       }
     }
+    //END FOR DEBUGGING
   }else{
     d_curr_model = fm;
     d_addedLemmas = 0;
@@ -162,6 +163,8 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) {
               if( optOneQuantPerRoundInstGen() && addedLemmas>0 ){
                 break;
               }
+            }else if( d_quant_sat.find( f )!=d_quant_sat.end() ){
+              d_numQuantSat++;
             }
           }
           Trace("model-engine-debug") << "Quantifiers sat/ig/n-ig/null " << d_numQuantSat << " / " << d_numQuantInstGen << " / ";
@@ -267,7 +270,7 @@ void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){
       if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){
         if( !n.getAttribute(BasisNoMatchAttribute()) ){
           //need to consider if it is not congruent modulo model basis
-          if( !tabt.addTerm( d_qe, n ) ){
+          if( !tabt.addTerm( fm, n ) ){
              BasisNoMatchAttribute bnma;
              n.setAttribute(bnma,true);
           }
@@ -311,7 +314,7 @@ bool ModelEngineBuilder::optOneQuantPerRoundInstGen(){
 }
 
 bool ModelEngineBuilder::optExhInstNonInstGenQuant(){
-  return true;
+  return options::fmfNewInstGen();
 }
 
 void ModelEngineBuilder::setEffort( int effort ){
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index d0348dff8..7331daf8e 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -23,6 +23,7 @@
 
 namespace CVC4 {
 namespace theory {
+namespace quantifiers {
 
 /** Attribute true for nodes that should not be used when considered for inst-gen basis */
 struct BasisNoMatchAttributeId {};
@@ -35,17 +36,14 @@ typedef expr::Attribute< BasisNoMatchAttributeId,
 
 class TermArgBasisTrie {
 private:
-  bool addTerm2( QuantifiersEngine* qe, Node n, int argIndex );
+  bool addTerm2( FirstOrderModel* fm, Node n, int argIndex );
 public:
   /** the data */
   std::map< Node, TermArgBasisTrie > d_data;
 public:
-  bool addTerm( QuantifiersEngine* qe, Node n ) { return addTerm2( qe, n, 0 ); }
+  bool addTerm( FirstOrderModel* fm, Node n ) { return addTerm2( fm, n, 0 ); }
 };/* class TermArgBasisTrie */
 
-
-namespace quantifiers {
-
 /** model builder class
   *  This class is capable of building candidate models based on the current quantified formulas
   *  that are asserted.  Use:
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 40a61f7c5..87f842862 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -52,21 +52,19 @@ void ModelEngine::check( Theory::Effort e ){
     FirstOrderModel* fm = d_quantEngine->getModel();
     //the following will attempt to build a model and test that it satisfies all asserted universal quantifiers
     int addedLemmas = 0;
-    Trace("model-engine") << "---Model Engine Round---" << std::endl;
+    //quantifiers are initialized, we begin an instantiation round
+    double clSet = 0;
+    if( Trace.isOn("model-engine") ){
+      clSet = double(clock())/double(CLOCKS_PER_SEC);
+    }
+    ++(d_statistics.d_inst_rounds);
     //two effort levels: first try exhaustive instantiation without axioms, then with.
     int startEffort = ( !fm->isAxiomAsserted() || options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT ) ? 1 : 0;
     for( int effort=startEffort; effort<2; effort++ ){
       // for effort = 0, we only instantiate non-axioms
       // for effort = 1, we instantiate everything
       if( addedLemmas==0 ){
-        //quantifiers are initialized, we begin an instantiation round
-        double clSet = 0;
-        if( Trace.isOn("model-engine") ){
-          clSet = double(clock())/double(CLOCKS_PER_SEC);
-        }
-        ++(d_statistics.d_inst_rounds);
-        //reset the quantifiers engine
-        d_quantEngine->resetInstantiationRound( e );
+        Trace("model-engine") << "---Model Engine Round---" << std::endl;
         //initialize the model
         Trace("model-engine-debug") << "Build model..." << std::endl;
         d_builder->setEffort( effort );
@@ -91,10 +89,6 @@ void ModelEngine::check( Theory::Effort e ){
           //check quantifiers that inst-gen didn't apply to
           addedLemmas += checkModel( check_model_no_inst_gen );
         }
-        if( Trace.isOn("model-engine") ){
-          double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
-          Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl;
-        }
       }
       if( addedLemmas==0 ){
         //if we have not added lemmas yet and axiomInstMode=trust, then we are done
@@ -107,6 +101,10 @@ void ModelEngine::check( Theory::Effort e ){
         }
       }
     }
+    if( Trace.isOn("model-engine") ){
+      double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
+      Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl;
+    }
     if( addedLemmas==0 ){
       Trace("model-engine-debug") << "No lemmas added, incomplete = " << d_incomplete_check << std::endl;
       //CVC4 will answer SAT or unknown
@@ -155,6 +153,19 @@ bool ModelEngine::optExhInstEvalSkipMultiple(){
 #endif
 }
 
+bool containsNN( Node n, Node nc ){
+  if( n==nc ){
+    return true;
+  }else{
+    for( int i=0; i<(int)n.getNumChildren(); i++ ){
+      if( containsNN( n[i], nc ) ){
+        return true;
+      }
+    }
+    return false;
+  }
+}
+
 int ModelEngine::checkModel( int checkOption ){
   int addedLemmas = 0;
   FirstOrderModel* fm = d_quantEngine->getModel();
@@ -169,6 +180,17 @@ int ModelEngine::checkModel( int checkOption ){
           Trace("model-engine-debug") << it->second[i] << "  ";
         }
         Trace("model-engine-debug") << std::endl;
+        for( size_t i=0; i<it->second.size(); i++ ){
+          std::vector< Node > eqc;
+          d_quantEngine->getEqualityQuery()->getEquivalenceClass( it->second[i], eqc );
+          Trace("model-engine-debug-eqc") << "      " << it->second[i] << " : { ";
+          for( size_t j=0; j<eqc.size(); j++ ){
+            if( it->second[i]!=eqc[j] && containsNN( it->second[i], eqc[j] ) ){
+              Trace("model-engine-debug-eqc") << eqc[j] << " ";
+            }
+          }
+          Trace("model-engine-debug-eqc") << "}" << std::endl;
+        }
       }
     }
   }
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 724c76e82..5802a05cd 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -61,9 +61,12 @@ option cbqi --enable-cbqi/--disable-cbqi bool :default false
 option userPatternsQuant /--ignore-user-patterns bool :default true
  ignore user-provided patterns for quantifier instantiation
 
-option flipDecision --enable-flip-decision/ bool :default false
+option flipDecision --flip-decision/ bool :default false
  turns on flip decision heuristic
 
+option internalReps --disable-quant-internal-reps/ bool :default true
+ disables instantiating with representatives chosen by quantifiers engine
+
 option finiteModelFind --finite-model-find bool :default false
  use finite model finding heuristic for quantifier instantiation
 
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 18aaab01f..bb6855c47 100755
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -77,6 +77,8 @@ class EqualityQuery {
 public:

   EqualityQuery(){}

   virtual ~EqualityQuery(){};

+  /** reset */

+  virtual void reset() = 0;

   /** contains term */

   virtual bool hasTerm( Node a ) = 0;

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

@@ -85,11 +87,6 @@ public:
   virtual bool areEqual( Node a, Node b ) = 0;

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

   virtual bool areDisequal( Node a, Node b ) = 0;

-  /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria.

-      If cbqi is active, this will return a term in the equivalence class of "a" that does

-      not contain instantiation constants, if such a term exists.

-   */

-  virtual Node getInternalRepresentative( Node a ) = 0;

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

   virtual eq::EqualityEngine* getEngine() = 0;

   /** get the equivalence class of a */

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 493b9e931..d637fa25f 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -144,7 +144,6 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
            computeModelBasisArgAttribute( n );
            if( !n.getAttribute(NoMatchAttribute()) ){
              if( !d_func_map_trie[ it->first ].addTerm( d_quantEngine, n ) ){
-               //only set no match if not a model basis argument term
                NoMatchAttribute nma;
                n.setAttribute(nma,true);
                congruentCount++;
@@ -171,7 +170,6 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
          if( !en.getAttribute(NoMatchAttribute()) ){
            Node op = en.getOperator();
            if( !d_pred_map_trie[i][op].addTerm( d_quantEngine, en ) ){
-             //only set no match if not a model basis argument term
              NoMatchAttribute nma;
              en.setAttribute(nma,true);
              congruentCount++;
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 902eebe01..ebd6d32ea 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -78,6 +78,10 @@ QuantifiersEngine::~QuantifiersEngine(){
   delete d_eq_query;
 }
 
+EqualityQuery* QuantifiersEngine::getEqualityQuery() {
+  return d_eq_query;
+}
+
 Instantiator* QuantifiersEngine::getInstantiator( theory::TheoryId id ){
   return d_te->theoryOf( id )->getInstantiator();
 }
@@ -96,32 +100,39 @@ Valuation& QuantifiersEngine::getValuation(){
 
 void QuantifiersEngine::check( Theory::Effort e ){
   CodeTimer codeTimer(d_time);
-  if( e>=Theory::EFFORT_FULL ){
-    Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl;
+  bool needsCheck = e>=Theory::EFFORT_LAST_CALL;  //always need to check at or above last call
+  for( int i=0; i<(int)d_modules.size(); i++ ){
+    if( d_modules[i]->needsCheck( e ) ){
+      needsCheck = true;
+    }
   }
-
-  d_hasAddedLemma = false;
-  if( e==Theory::EFFORT_LAST_CALL ){
-    //if effort is last call, try to minimize model first
-    if( options::finiteModelFind() ){
-      //first, check if we can minimize the model further
-      if( !((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->minimize() ){
-        return;
+  if( needsCheck ){
+    Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl;
+    //reset relevant information
+    d_hasAddedLemma = false;
+    d_term_db->reset( e );
+    d_eq_query->reset();
+    if( e==Theory::EFFORT_LAST_CALL ){
+      //if effort is last call, try to minimize model first
+      if( options::finiteModelFind() ){
+        //first, check if we can minimize the model further
+        if( !((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->minimize() ){
+          return;
+        }
       }
+      ++(d_statistics.d_instantiation_rounds_lc);
+    }else if( e==Theory::EFFORT_FULL ){
+      ++(d_statistics.d_instantiation_rounds);
     }
-    ++(d_statistics.d_instantiation_rounds_lc);
-  }else if( e==Theory::EFFORT_FULL ){
-    ++(d_statistics.d_instantiation_rounds);
-  }
-  for( int i=0; i<(int)d_modules.size(); i++ ){
-    d_modules[i]->check( 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->isModelSet() ){
-    d_te->getModelBuilder()->buildModel( d_model, true );
-  }
-  if( e>=Theory::EFFORT_FULL ){
+    for( int i=0; i<(int)d_modules.size(); i++ ){
+      d_modules[i]->check( 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->isModelSet() ){
+      d_te->getModelBuilder()->buildModel( d_model, true );
+    }
+
     Trace("quant-engine") << "Finished quantifiers engine check." << std::endl;
   }
 }
@@ -183,15 +194,6 @@ Node QuantifiersEngine::getNextDecisionRequest(){
   return Node::null();
 }
 
-void QuantifiersEngine::resetInstantiationRound( Theory::Effort level ){
-  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 ){
   std::set< Node > added;
   getTermDatabase()->addTerm( n, added, withinQuant );
@@ -326,13 +328,24 @@ bool QuantifiersEngine::addLemma( Node lem ){
 }
 
 bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool modEq, bool modInst, bool mkRep ){
+  Trace("inst-add") << "Add instantiation: " << m << std::endl;
   //make sure there are values for each variable we are instantiating
-  m.makeComplete( f, this );
-  //make it representative, this is helpful for recognizing duplication
-  if( mkRep ){
-    m.makeRepresentative( this );
+  for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+    Node ic = d_term_db->getInstantiationConstant( f, i );
+    Node val = m.getValue( ic );
+    if( val.isNull() ){
+      val = d_term_db->getFreeVariableForInstConstant( ic );
+      Trace("inst-add-debug") << "mkComplete " << val << std::endl;
+      m.set( ic, val );
+    }
+    //make it representative, this is helpful for recognizing duplication
+    if( mkRep ){
+      //pick the best possible representative for instantiation, based on past use and simplicity of term
+      Node r = d_eq_query->getInternalRepresentative( val );
+      Trace("inst-add-debug") << "mkRep " << r << " " << val << std::endl;
+      m.set( ic, r );
+    }
   }
-  Trace("inst-add") << "Add instantiation: " << m << std::endl;
   //check for duplication modulo equality
   if( !d_inst_match_trie[f].addInstMatch( this, f, m, modEq, modInst ) ){
     Trace("inst-add") << " -> Already exists." << std::endl;
@@ -552,6 +565,10 @@ QuantifiersEngine::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_multi_candidates_cache_miss);
 }
 
+void EqualityQueryQuantifiersEngine::reset(){
+  d_int_rep.clear();
+  d_reset_count++;
+}
 
 bool EqualityQueryQuantifiersEngine::hasTerm( Node a ){
   eq::EqualityEngine* ee = d_qe->getTheoryEngine()->getSharedTermsDatabase()->getEqualityEngine();
@@ -624,15 +641,40 @@ bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){
 }
 
 Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a ){
-  //for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){
-  //  if( d_qe->getInstantiator( i ) ){
-  //    if( d_qe->getInstantiator( i )->hasTerm( a ) ){
-  //      return d_qe->getInstantiator( i )->getInternalRepresentative( a );
-  //    }
-  //  }
-  //}
-  //return a;
-  return d_qe->getInstantiator( THEORY_UF )->getInternalRepresentative( a );
+  if( !options::internalReps() ){
+    return d_qe->getInstantiator( THEORY_UF )->getRepresentative( a );
+  }else{
+    Node r = d_qe->getInstantiator( THEORY_UF )->getRepresentative( a );
+    if( d_int_rep.find( r )==d_int_rep.end() ){
+      std::vector< Node > eqc;
+      getEquivalenceClass( r, eqc );
+      //find best selection for representative
+      Node r_best = r;
+      int r_best_score = getRepScore( r );
+      for( size_t i=0; i<eqc.size(); i++ ){
+        int score = getRepScore( eqc[i] );
+        //score prefers earliest use of this term as a representative
+        if( score>=0 && ( r_best_score<0 || score<r_best_score ) ){
+          r_best = eqc[i];
+          r_best_score = score;
+        }
+      }
+      //now, make sure that no other member of the class is an instance
+      r_best = getInstance( r_best, eqc );
+      //store that this representative was chosen at this point
+      if( d_rep_score.find( r_best )==d_rep_score.end() ){
+        d_rep_score[ r_best ] = d_reset_count;
+      }
+      d_int_rep[r] = r_best;
+      if( r_best!=a ){
+        Trace("internal-rep-debug") << "rep( " << a << " ) = " << r << ", " << std::endl;
+        Trace("internal-rep-debug") << "int_rep( " << a << " ) = " << r_best << ", " << std::endl;
+      }
+      return r_best;
+    }else{
+      return d_int_rep[r];
+    }
+  }
 }
 
 eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){
@@ -657,4 +699,26 @@ void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< N
   if( eqc.empty() ){
     eqc.push_back( a );
   }
+  //a should be in its equivalence class
+  Assert( std::find( eqc.begin(), eqc.end(), a )!=eqc.end() );
+}
+
+//helper functions
+
+Node EqualityQueryQuantifiersEngine::getInstance( Node n, std::vector< Node >& eqc ){
+  for( size_t i=0; i<n.getNumChildren(); i++ ){
+    Node nn = getInstance( n[i], eqc );
+    if( !nn.isNull() ){
+      return nn;
+    }
+  }
+  if( std::find( eqc.begin(), eqc.end(), n )!=eqc.end() ){
+    return n;
+  }else{
+    return Node::null();
+  }
+}
+
+int EqualityQueryQuantifiersEngine::getRepScore( Node n ){
+  return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n];
 }
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index f9c016cb9..8fc6253ac 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -45,7 +45,9 @@ public:
   virtual ~QuantifiersModule(){}
   //get quantifiers engine
   QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; }
-  /* Call during check registerQuantifier has already been called */
+  /* whether this module needs to check this round */
+  virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; }
+  /* Call during quantifier engine's check */
   virtual void check( Theory::Effort e ) = 0;
   /* Called for new quantifiers */
   virtual void registerQuantifier( Node n ) = 0;
@@ -67,6 +69,7 @@ namespace inst {
 }/* CVC4::theory::inst */
 
 class EfficientEMatcher;
+class EqualityQueryQuantifiersEngine;
 
 class QuantifiersEngine {
   friend class quantifiers::InstantiationEngine;
@@ -83,7 +86,7 @@ private:
   /** model engine */
   quantifiers::ModelEngine* d_model_engine;
   /** equality query class */
-  EqualityQuery* d_eq_query;
+  EqualityQueryQuantifiersEngine* d_eq_query;
   /** for computing relevance of quantifiers */
   QuantRelevance d_quant_rel;
   /** phase requirements for each quantifier for each instantiation literal */
@@ -118,7 +121,7 @@ public:
   TheoryEngine* getTheoryEngine() { return d_te; }
   /** get equality query object for the given type. The default is the
       generic one */
-  EqualityQuery* getEqualityQuery() { return d_eq_query; }
+  EqualityQuery* getEqualityQuery();
   /** get instantiation engine */
   quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; }
   /** get model engine */
@@ -150,8 +153,6 @@ public:
   void propagate( Theory::Effort level );
   /** get next decision request */
   Node getNextDecisionRequest();
-  /** reset instantiation round */
-  void resetInstantiationRound( Theory::Effort level );
 private:
   /** compute term vector */
   void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms );
@@ -244,17 +245,34 @@ class EqualityQueryQuantifiersEngine : public EqualityQuery
 private:
   /** pointer to theory engine */
   QuantifiersEngine* d_qe;
+  /** internal representatives */
+  std::map< Node, Node > d_int_rep;
+  /** rep score */
+  std::map< Node, int > d_rep_score;
+  /** reset count */
+  int d_reset_count;
+private:
+  /** node contains */
+  Node getInstance( Node n, std::vector< Node >& eqc );
+  /** get score */
+  int getRepScore( Node n );
 public:
-  EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ){}
+  EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ){}
   ~EqualityQueryQuantifiersEngine(){}
+  /** reset */
+  void reset();
   /** general queries about equality */
   bool hasTerm( Node a );
   Node getRepresentative( Node a );
   bool areEqual( Node a, Node b );
   bool areDisequal( Node a, Node b );
-  Node getInternalRepresentative( Node a );
   eq::EqualityEngine* getEngine();
   void getEquivalenceClass( Node a, std::vector< Node >& eqc );
+  /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria.
+      If cbqi is active, this will return a term in the equivalence class of "a" that does
+      not contain instantiation constants, if such a term exists.
+   */
+  Node getInternalRepresentative( Node a );
 }; /* EqualityQueryQuantifiersEngine */
 
 }/* CVC4::theory namespace */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index e51b8594e..195e37154 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -789,7 +789,7 @@ public:
 
   /**
    * This is a utility function for constructing a copy of the currently shared terms
-   * in a queriable form.  As this is 
+   * in a queriable form.  As this is
    */
   std::hash_set<TNode, TNodeHashFunction> currentlySharedTerms() const;
 };/* class Theory */
@@ -893,7 +893,6 @@ public:
   virtual bool areEqual( Node a, Node b ) { return false; }
   virtual bool areDisequal( Node a, Node b ) { return false; }
   virtual Node getRepresentative( Node a ) { return a; }
-  virtual Node getInternalRepresentative( Node a ) { return getRepresentative( a ); }
   virtual eq::EqualityEngine* getEqualityEngine() { return NULL; }
   virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) {}
 public:
diff --git a/src/theory/uf/inst_strategy.cpp b/src/theory/uf/inst_strategy.cpp
index eef2dac79..4fe5772de 100644
--- a/src/theory/uf/inst_strategy.cpp
+++ b/src/theory/uf/inst_strategy.cpp
@@ -48,48 +48,6 @@ struct sortQuantifiersForSymbol {
   }
 };
 
-
-void InstStrategyCheckCESolved::processResetInstantiationRound( Theory::Effort effort ){
-  for( std::map< Node, bool >::iterator it = d_solved.begin(); it != d_solved.end(); ++it ){
-    calcSolved( it->first );
-  }
-}
-
-int InstStrategyCheckCESolved::process( Node f, Theory::Effort effort, int e ){
-  if( e==0 ){
-    //calc solved if not done so already
-    if( d_solved.find( f )==d_solved.end() ){
-      calcSolved( f );
-    }
-    //check if f is counterexample-solved
-    Debug("quant-uf-strategy") << "Try CE-solved.." << std::endl;
-    if( d_solved[ f ] ){
-      if( d_quantEngine->addInstantiation( f, d_th->d_baseMatch[f] ) ){
-        ++(d_th->d_statistics.d_instantiations_ce_solved);
-        //d_quantEngine->d_hasInstantiated[f] = true;
-      }
-      d_solved[f] = false;
-    }
-    Debug("quant-uf-strategy") << "done." << std::endl;
-  }
-  return STATUS_UNKNOWN;
-}
-
-void InstStrategyCheckCESolved::calcSolved( Node f ){
-  d_th->d_baseMatch[f].clear();
-  d_solved[ f ]= true;
-  //check if instantiation constants are solved for
-  for( int j = 0; j<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){
-    Node i = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );
-    Node rep = d_th->getInternalRepresentative( i );
-    if( !rep.hasAttribute(InstConstantAttribute()) ){
-      d_th->d_baseMatch[f].set(i,rep);
-    }else{
-      d_solved[ f ] = false;
-    }
-  }
-}
-
 void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort effort ){
   //reset triggers
   for( std::map< Node, std::vector< Trigger* > >::iterator it = d_user_gen.begin(); it != d_user_gen.end(); ++it ){
diff --git a/src/theory/uf/inst_strategy.h b/src/theory/uf/inst_strategy.h
index 6baa5b147..5a3b9cc3d 100644
--- a/src/theory/uf/inst_strategy.h
+++ b/src/theory/uf/inst_strategy.h
@@ -34,25 +34,6 @@ class InstantiatorTheoryUf;
 
 //instantiation strategies
 
-class InstStrategyCheckCESolved : public InstStrategy{
-private:
-  /** InstantiatorTheoryUf class */
-  InstantiatorTheoryUf* d_th;
-  /** is solved? */
-  std::map< Node, bool > d_solved;
-  /** calc if f is solved */
-  void calcSolved( Node f );
-  /** process functions */
-  void processResetInstantiationRound( Theory::Effort effort );
-  int process( Node f, Theory::Effort effort, int e );
-public:
-  InstStrategyCheckCESolved( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) :
-      InstStrategy( ie ), d_th( th ){}
-  ~InstStrategyCheckCESolved(){}
-  /** identify */
-  std::string identify() const { return std::string("CheckCESolved"); }
-};/* class InstStrategyCheckCESolved */
-
 class InstStrategyUserPatterns : public InstStrategy{
 private:
   /** InstantiatorTheoryUf class */
diff --git a/src/theory/uf/theory_uf_instantiator.cpp b/src/theory/uf/theory_uf_instantiator.cpp
index 0cc32d420..099eb5b5e 100644
--- a/src/theory/uf/theory_uf_instantiator.cpp
+++ b/src/theory/uf/theory_uf_instantiator.cpp
@@ -38,9 +38,9 @@ InstantiatorTheoryUf::InstantiatorTheoryUf(context::Context* c, CVC4::theory::Qu
 Instantiator( c, qe, th )
 {
   if( !options::finiteModelFind() || options::fmfInstEngine() ){
-    if( options::cbqi() ){
-      addInstStrategy( new InstStrategyCheckCESolved( this, qe ) );
-    }
+    //if( options::cbqi() ){
+    //  addInstStrategy( new InstStrategyCheckCESolved( this, qe ) );
+    //}
     if( options::userPatternsQuant() ){
       d_isup = new InstStrategyUserPatterns( this, qe );
       addInstStrategy( d_isup );
@@ -88,7 +88,7 @@ void InstantiatorTheoryUf::addUserPattern( Node f, Node pat ){
 
 
 void InstantiatorTheoryUf::processResetInstantiationRound( Theory::Effort effort ){
-  d_ground_reps.clear();
+  //d_ground_reps.clear();
 }
 
 int InstantiatorTheoryUf::process( Node f, Theory::Effort effort, int e ){
@@ -132,7 +132,7 @@ Node InstantiatorTheoryUf::getRepresentative( Node a ){
     return a;
   }
 }
-
+/*
 Node InstantiatorTheoryUf::getInternalRepresentative( Node a ){
   if( d_ground_reps.find( a )==d_ground_reps.end() ){
     if( !hasTerm( a ) ){
@@ -160,7 +160,7 @@ Node InstantiatorTheoryUf::getInternalRepresentative( Node a ){
   }
   return d_ground_reps[a];
 }
-
+*/
 eq::EqualityEngine* InstantiatorTheoryUf::getEqualityEngine(){
   return &((TheoryUF*)d_th)->d_equalityEngine;
 }
diff --git a/src/theory/uf/theory_uf_instantiator.h b/src/theory/uf/theory_uf_instantiator.h
index 324fa6386..3cb4f97cc 100644
--- a/src/theory/uf/theory_uf_instantiator.h
+++ b/src/theory/uf/theory_uf_instantiator.h
@@ -48,7 +48,7 @@ protected:
   typedef context::CDChunkList<Node> NodeList;
   typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeLists;
   /** map to representatives used */
-  std::map< Node, Node > d_ground_reps;
+  //std::map< Node, Node > d_ground_reps;
 protected:
   /** instantiation strategies */
   InstStrategyUserPatterns* d_isup;
@@ -132,7 +132,6 @@ public:
   Node getRepresentative( Node a ) { return d_ith->getRepresentative( a ); }
   bool areEqual( Node a, Node b ) { return d_ith->areEqual( a, b ); }
   bool areDisequal( Node a, Node b ) { return d_ith->areDisequal( a, b ); }
-  Node getInternalRepresentative( Node a ) { return d_ith->getInternalRepresentative( a ); }
   eq::EqualityEngine* getEngine() { return d_ith->getEqualityEngine(); }
   void getEquivalenceClass( Node a, std::vector< Node >& eqc ) { d_ith->getEquivalenceClass( a, eqc ); }
 }; /* EqualityQueryInstantiatorTheoryUf */
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index d037c374d..548d6f2f0 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -919,7 +919,13 @@ void StrongSolverTheoryUf::SortRepModel::allocateCardinality( OutputChannel* out
       //must generate new cardinality lemma term
       std::stringstream ss;
       ss << "_c_" << d_aloc_cardinality;
-      Node var = NodeManager::currentNM()->mkSkolem( ss.str(), d_type, "is a cardinality lemma term" );
+      Node var;
+      if( d_totality_terms[0].empty() ){
+        //get arbitrary ground term
+        var = d_cardinality_term;
+      }else{
+        var = NodeManager::currentNM()->mkSkolem( ss.str(), d_type, "is a cardinality lemma term" );
+      }
       d_totality_terms[0].push_back( var );
       Trace("mkVar") << "allocateCardinality, mkVar : " << var << " : " << d_type << std::endl;
       //must be distinct from all other cardinality terms