Add quantifiers options related to model and master equality engine.

1 files changed, 54 insertions, 11 deletions

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 ){