Add quantifiers options related to model and master equality engine.

11 files changed, 80 insertions, 33 deletions

diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 7c9a6196f..17c8e0300 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -284,7 +284,7 @@ Node CandidateGeneratorQEAll::getNextCandidate() {
       TNode nh = d_qe->getTermDatabase()->getEligibleTermInEqc( n );
       if( !nh.isNull() ){
         if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){
-          nh = d_qe->getEqualityQuery()->getInternalRepresentative( nh, d_f, d_index );
+          nh = d_qe->getInternalRepresentative( nh, d_f, d_index );
           //don't consider this if already the instantiation is ineligible
           if( !d_qe->getTermDatabase()->isTermEligibleForInstantiation( nh, d_f, false ) ){
             nh = Node::null();
diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index 703dc6928..7ce299864 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -711,6 +711,7 @@ void CegInstantiator::processAssertions() {
   d_curr_eqc.clear();
   d_curr_type_eqc.clear();
 
+  // must use master equality engine to avoid value instantiations
   eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine();
   //to eliminate identified illegal terms
   std::map< Node, Node > aux_subs;
diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp
index 28b92cc5e..6457de145 100644
--- a/src/theory/quantifiers/inst_propagator.cpp
+++ b/src/theory/quantifiers/inst_propagator.cpp
@@ -91,7 +91,7 @@ bool EqualityQueryInstProp::areDisequal( Node a, Node b ) {
 
 /** get the equality engine associated with this query */
 eq::EqualityEngine* EqualityQueryInstProp::getEngine() {
-  return d_qe->getMasterEqualityEngine();
+  return d_qe->getActiveEqualityEngine();
 }
 
 /** get the equivalence class of a */
diff --git a/src/theory/quantifiers/local_theory_ext.cpp b/src/theory/quantifiers/local_theory_ext.cpp
index ada28c084..09ed99735 100644
--- a/src/theory/quantifiers/local_theory_ext.cpp
+++ b/src/theory/quantifiers/local_theory_ext.cpp
@@ -143,7 +143,7 @@ void LtePartialInst::check( Theory::Effort e, unsigned quant_e ) {
 
 void LtePartialInst::reset() {
   d_reps.clear();
-  eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
+  eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine();
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
   while( !eqcs_i.isFinished() ){
     TNode r = (*eqcs_i);
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index f529a9a27..2faf13f1a 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -155,7 +155,7 @@ int ModelEngine::checkModel(){
   //Trace("model-engine-debug") << "Flattening representatives...." << std::endl;
   //d_quantEngine->getEqualityQuery()->flattenRepresentatives( fm->d_rep_set.d_type_reps );
 
-  //for debugging
+  //for debugging, setup
   for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
        it != fm->d_rep_set.d_type_reps.end(); ++it ){
     if( it->first.isSort() ){
@@ -167,7 +167,7 @@ int ModelEngine::checkModel(){
       Trace("model-engine-debug") << std::endl;
       Trace("model-engine-debug") << "   Term reps : ";
       for( size_t i=0; i<it->second.size(); i++ ){
-        Node r = d_quantEngine->getEqualityQuery()->getInternalRepresentative( it->second[i], Node::null(), 0 );
+        Node r = d_quantEngine->getInternalRepresentative( it->second[i], Node::null(), 0 );
         Trace("model-engine-debug") << r << " ";
       }
       Trace("model-engine-debug") << std::endl;
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 163c576f7..8fecaa78d 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -29,7 +29,7 @@ unsigned QuantifiersModule::needsModel( Theory::Effort e ) {
 }
 
 eq::EqualityEngine * QuantifiersModule::getEqualityEngine() {
-  return d_quantEngine->getMasterEqualityEngine();
+  return d_quantEngine->getActiveEqualityEngine();
 }
 
 bool QuantifiersModule::areEqual( TNode n1, TNode n2 ) {
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 28423259b..4f58f7a2e 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -204,7 +204,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi
 
 void TermDb::computeArgReps( TNode n ) {
   if( d_arg_reps.find( n )==d_arg_reps.end() ){
-    eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
+    eq::EqualityEngine * ee = d_quantEngine->getActiveEqualityEngine();
     for( unsigned j=0; j<n.getNumChildren(); j++ ){
       TNode r = ee->hasTerm( n[j] ) ? ee->getRepresentative( n[j] ) : n[j];
       d_arg_reps[n].push_back( r );
@@ -215,7 +215,7 @@ void TermDb::computeArgReps( TNode n ) {
 void TermDb::computeUfEqcTerms( TNode f ) {
   if( d_func_map_eqc_trie.find( f )==d_func_map_eqc_trie.end() ){
     d_func_map_eqc_trie[f].clear();
-    eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
+    eq::EqualityEngine * ee = d_quantEngine->getActiveEqualityEngine();
     for( unsigned i=0; i<d_op_map[f].size(); i++ ){
       TNode n = d_op_map[f][i];
       if( hasTermCurrent( n ) ){
@@ -234,7 +234,7 @@ void TermDb::computeUfTerms( TNode f ) {
     d_op_nonred_count[ f ] = 0;
     std::map< Node, std::vector< Node > >::iterator it = d_op_map.find( f );
     if( it!=d_op_map.end() ){
-      eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
+      eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine();
       Trace("term-db-debug") << "Adding terms for operator " << f << std::endl;
       unsigned congruentCount = 0;
       unsigned nonCongruentCount = 0;
@@ -307,7 +307,8 @@ void TermDb::computeUfTerms( TNode f ) {
 
 bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) {
   computeUfTerms( f );
-  Assert( d_quantEngine->getTheoryEngine()->getMasterEqualityEngine()->getRepresentative( r )==r );
+  Assert( !d_quantEngine->getActiveEqualityEngine()->hasTerm( r ) || 
+          d_quantEngine->getActiveEqualityEngine()->getRepresentative( r )==r );
   std::map< Node, std::map< unsigned, std::vector< Node > > >::iterator it = d_func_map_rel_dom.find( f );
   if( it != d_func_map_rel_dom.end() ){
     std::map< unsigned, std::vector< Node > >::iterator it2 = it->second.find( i );
@@ -578,7 +579,7 @@ bool TermDb::hasTermCurrent( Node n, bool useMode ) {
   if( !useMode ){
     return d_has_map.find( n )!=d_has_map.end();
   }else{
-    //return d_quantEngine->getMasterEqualityEngine()->hasTerm( n ); //some assertions are not sent to EE
+    //return d_quantEngine->getActiveEqualityEngine()->hasTerm( n ); //some assertions are not sent to EE
     if( options::termDbMode()==TERM_DB_ALL ){
       return true;
     }else if( options::termDbMode()==TERM_DB_RELEVANT ){
@@ -630,7 +631,7 @@ Node TermDb::getEligibleTermInEqc( TNode r ) {
     std::map< Node, Node >::iterator it = d_term_elig_eqc.find( r );
     if( it==d_term_elig_eqc.end() ){
       Node h;
-      eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
+      eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine();
       eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
       while( h.isNull() && !eqc_i.isFinished() ){
         TNode n = (*eqc_i);
@@ -680,7 +681,7 @@ bool TermDb::reset( Theory::Effort effort ){
   d_func_map_rel_dom.clear();
   d_consistent_ee = true;
 
-  eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
+  eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine();
   //compute has map
   if( options::termDbMode()==TERM_DB_RELEVANT || options::lteRestrictInstClosure() ){
     d_has_map.clear();
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 94a11a09e..4d3e584b4 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -35,8 +35,7 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
 TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
-    Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo),
-  d_masterEqualityEngine(0)
+    Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo)
 {
   d_numInstantiations = 0;
   d_baseDecLevel = -1;
@@ -55,7 +54,7 @@ TheoryQuantifiers::~TheoryQuantifiers() {
 }
 
 void TheoryQuantifiers::setMasterEqualityEngine(eq::EqualityEngine* eq) {
-  d_masterEqualityEngine = eq;
+
 }
 
 void TheoryQuantifiers::addSharedTerm(TNode t) {
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index f52381011..462dcb339 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -44,9 +44,6 @@ private:
   /** number of instantiations */
   int d_numInstantiations;
   int d_baseDecLevel;
-
-  eq::EqualityEngine* d_masterEqualityEngine;
-
 private:
   void computeCareGraph();
 
@@ -69,7 +66,6 @@ public:
   void shutdown() { }
   std::string identify() const { return std::string("TheoryQuantifiers"); }
   void setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value);
-  eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; }
   bool ppDontRewriteSubterm(TNode atom) { return atom.getKind() == kind::FORALL || atom.getKind() == kind::EXISTS; }
 private:
   void assertUniversal( Node n );
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index b369e30b7..db0efd988 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -91,6 +91,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
   d_curr_effort_level = QEFFORT_NONE;
   d_conflict = false;
   d_hasAddedLemma = false;
+  d_useModelEe = false;
   //don't add true lemma
   d_lemmas_produced_c[d_term_db->d_true] = true;
 
@@ -383,7 +384,21 @@ void QuantifiersEngine::ppNotifyAssertions(
 
 void QuantifiersEngine::check( Theory::Effort e ){
   CodeTimer codeTimer(d_statistics.d_time);
-  if( !getMasterEqualityEngine()->consistent() ){
+  d_useModelEe = options::quantModelEe() && ( e>=Theory::EFFORT_LAST_CALL );
+  // if we want to use the model's equality engine, build the model now
+  if( d_useModelEe && !d_model->isBuilt() ){
+    Trace("quant-engine-debug") << "Build the model." << std::endl;
+    if( !d_te->getModelBuilder()->buildModel( d_model ) ){
+      //we are done if model building was unsuccessful
+      flushLemmas();
+      if( d_hasAddedLemma ){
+        Trace("quant-engine-debug") << "...failed." << std::endl;
+        return;
+      }
+    }
+  }
+  
+  if( !getActiveEqualityEngine()->consistent() ){
     Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl;
     return;
   }
@@ -505,7 +520,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
     Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl;
     for( unsigned quant_e = QEFFORT_CONFLICT; quant_e<=QEFFORT_LAST_CALL; quant_e++ ){
       d_curr_effort_level = quant_e;
-      bool success = true;
       //build the model if any module requested it
       if( needsModelE==quant_e && !d_model->isBuilt() ){
         // theory engine's model builder is quantifier engine's builder if it has one
@@ -513,11 +527,11 @@ void QuantifiersEngine::check( Theory::Effort e ){
         Trace("quant-engine-debug") << "Build model..." << std::endl;
         if( !d_te->getModelBuilder()->buildModel( d_model ) ){
           //we are done if model building was unsuccessful
-          Trace("quant-engine-debug") << "...failed." << std::endl;
-          success = false;
+          Trace("quant-engine-debug") << "...added lemmas." << std::endl;
+          flushLemmas();
         }
       }
-      if( success ){
+      if( !d_hasAddedLemma ){
         //check each module
         for( unsigned i=0; i<qm.size(); i++ ){
           Trace("quant-engine-debug") << "Check " << qm[i]->identify().c_str() << " at effort " << quant_e << "..." << std::endl;
@@ -527,9 +541,9 @@ void QuantifiersEngine::check( Theory::Effort e ){
             break;
           }
         }
+        //flush all current lemmas
+        flushLemmas();
       }
-      //flush all current lemmas
-      flushLemmas();
       //if we have added one, stop
       if( d_hasAddedLemma ){
         break;
@@ -1084,7 +1098,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
     }
     if( mkRep ){
       //pick the best possible representative for instantiation, based on past use and simplicity of term
-      terms[i] = d_eq_query->getInternalRepresentative( terms[i], q, i );
+      terms[i] = getInternalRepresentative( terms[i], q, i );
     }else{
       //ensure the type is correct
       terms[i] = quantifiers::TermDb::ensureType( terms[i], q[0][i].getType() );
@@ -1178,6 +1192,16 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
   //construct the lemma
   Trace("inst-assert") << "(assert " << body << ")" << std::endl;
   body = Rewriter::rewrite(body);
+  
+  if( d_useModelEe && options::instNoModelTrue() ){
+    Node val_body = d_model->getValue( body );
+    if( val_body==d_term_db->d_true ){
+      Trace("inst-add-debug") << " --> True in model." << std::endl;
+      ++(d_statistics.d_inst_duplicate_model_true);
+      return false;
+    }
+  }
+  
   Node lem;
   if( rlv_cond.empty() ){
     lem = NodeManager::currentNM()->mkNode( kind::OR, q.negate(), body );
@@ -1571,6 +1595,7 @@ QuantifiersEngine::Statistics::Statistics()
       d_inst_duplicate("QuantifiersEngine::Duplicate_Inst", 0),
       d_inst_duplicate_eq("QuantifiersEngine::Duplicate_Inst_Eq", 0),
       d_inst_duplicate_ent("QuantifiersEngine::Duplicate_Inst_Entailed", 0),
+      d_inst_duplicate_model_true("QuantifiersEngine::Duplicate_Inst_Model_True", 0),
       d_triggers("QuantifiersEngine::Triggers", 0),
       d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
       d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
@@ -1596,6 +1621,7 @@ QuantifiersEngine::Statistics::Statistics()
   smtStatisticsRegistry()->registerStat(&d_inst_duplicate);
   smtStatisticsRegistry()->registerStat(&d_inst_duplicate_eq);
   smtStatisticsRegistry()->registerStat(&d_inst_duplicate_ent);
+  smtStatisticsRegistry()->registerStat(&d_inst_duplicate_model_true);
   smtStatisticsRegistry()->registerStat(&d_triggers);
   smtStatisticsRegistry()->registerStat(&d_simple_triggers);
   smtStatisticsRegistry()->registerStat(&d_multi_triggers);
@@ -1623,6 +1649,7 @@ QuantifiersEngine::Statistics::~Statistics(){
   smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate);
   smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_eq);
   smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_ent);
+  smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_model_true);
   smtStatisticsRegistry()->unregisterStat(&d_triggers);
   smtStatisticsRegistry()->unregisterStat(&d_simple_triggers);
   smtStatisticsRegistry()->unregisterStat(&d_multi_triggers);
@@ -1640,11 +1667,27 @@ QuantifiersEngine::Statistics::~Statistics(){
 }
 
 eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){
-  return getTheoryEngine()->getMasterEqualityEngine();
+  return d_te->getMasterEqualityEngine();
+}
+
+eq::EqualityEngine* QuantifiersEngine::getActiveEqualityEngine() {
+  if( d_useModelEe ){
+    return d_model->d_equalityEngine;
+  }else{
+    return d_te->getMasterEqualityEngine();
+  }
+}
+
+Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){
+  bool prevModelEe = d_useModelEe;
+  d_useModelEe = false;
+  Node ret = d_eq_query->getInternalRepresentative( a, q, index );
+  d_useModelEe = prevModelEe;
+  return ret;
 }
 
 void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) {
-  eq::EqualityEngine* ee = getMasterEqualityEngine();
+  eq::EqualityEngine* ee = getActiveEqualityEngine();
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
   std::map< TypeNode, int > typ_num;
   while( !eqcs_i.isFinished() ){
@@ -1922,7 +1965,7 @@ void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map< TypeNode,
 }
 
 eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){
-  return d_qe->getMasterEqualityEngine();
+  return d_qe->getActiveEqualityEngine();
 }
 
 void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< Node >& eqc ){
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 5d7c25cde..bb38e5e4a 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -165,6 +165,8 @@ private:  //this information is reset during check
   context::CDO< bool > d_conflict_c;
   /** has added lemma this round */
   bool d_hasAddedLemma;
+  /** whether to use model equality engine */
+  bool d_useModelEe;
 private:
   /** list of all quantifiers seen */
   std::map< Node, bool > d_quants;
@@ -306,9 +308,9 @@ private:
   bool removeInstantiationInternal( Node q, std::vector< Node >& terms );
   /** set instantiation level attr */
   static void setInstantiationLevelAttr( Node n, Node qn, uint64_t level );
-public:
   /** flush lemmas */
   void flushLemmas();
+public:
   /** get instantiation */
   Node getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts = false );
   /** get instantiation */
@@ -366,9 +368,13 @@ public:
   void eqNotifyPostMerge(TNode t1, TNode t2);
   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
   /** get the master equality engine */
-  eq::EqualityEngine* getMasterEqualityEngine() ;
+  eq::EqualityEngine* getMasterEqualityEngine();
+  /** get the active equality engine */
+  eq::EqualityEngine* getActiveEqualityEngine();
   /** debug print equality engine */
   void debugPrintEqualityEngine( const char * c );
+  /** get internal representative */
+  Node getInternalRepresentative( Node a, Node q, int index );
 public:
   /** print instantiations */
   void printInstantiations( std::ostream& out );
@@ -402,6 +408,7 @@ public:
     IntStat d_inst_duplicate;
     IntStat d_inst_duplicate_eq;
     IntStat d_inst_duplicate_ent;
+    IntStat d_inst_duplicate_model_true;
     IntStat d_triggers;
     IntStat d_simple_triggers;
     IntStat d_multi_triggers;