Remove instantiation model true option (#4861)

This was an option that rejected instantiations that are true according to the current
model's equality engine.

This option was never helpful and will be burdensome to maintain with new updates
 to equality engine infrastructure.

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index b62468cddea12ac2a8413f15421286a1a885c723..4b130158ca8fb63d8c40ce4c1df0db9d988919d4 100644 (file)
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -492,15 +492,6 @@ header = "options/quantifiers_options.h"
   default    = "true"
   help       = "allow theory combination to happen once initially, before quantifier strategies are run"
 
-[[option]]
-  name       = "quantModelEe"
-  category   = "regular"
-  long       = "quant-model-ee"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "use equality engine of model for last call effort"
-
 [[option]]
   name       = "instMaxLevel"
   category   = "regular"
@@ -823,14 +814,6 @@ header = "options/quantifiers_options.h"
   default    = "true"
   help       = "do not consider instances of quantified formulas that are currently entailed"
 
-[[option]]
-  name       = "instNoModelTrue"
-  category   = "regular"
-  long       = "inst-no-model-true"
-  type       = "bool"
-  default    = "false"
-  help       = "do not consider instances of quantified formulas that are currently true in model, if it is available"
-
 [[option]]
   name       = "qcfEagerTest"
   category   = "regular"

diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp
index 94e60513c5c038570c414a55b677621b0effd83b..feaa0f223da19d315dcea045a722120a8a882a0b 100644 (file)
--- a/src/theory/quantifiers/equality_query.cpp
+++ b/src/theory/quantifiers/equality_query.cpp
@@ -182,7 +182,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a,
 }
 
 eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){
-  return d_qe->getActiveEqualityEngine();
+  return d_qe->getMasterEqualityEngine();
 }
 
 void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< Node >& eqc ){

diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index c9048fc951c9ee5cbf2a71426f61b878121a6c70..77b61e9dd9f27e3143369739806e7990e805cdce 100644 (file)
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -242,17 +242,6 @@ bool Instantiate::addInstantiation(
   // construct the lemma
   Trace("inst-assert") << "(assert " << body << ")" << std::endl;
 
-  if (d_qe->usingModelEqualityEngine() && options::instNoModelTrue())
-  {
-    Node val_body = d_qe->getModel()->getValue(body);
-    if (val_body.isConst() && val_body.getConst<bool>())
-    {
-      Trace("inst-add-debug") << " --> True in model." << std::endl;
-      ++(d_statistics.d_inst_duplicate_model_true);
-      return false;
-    }
-  }
-
   Node lem = NodeManager::currentNM()->mkNode(kind::OR, q.negate(), body);
   lem = Rewriter::rewrite(lem);
 
@@ -845,14 +834,12 @@ Instantiate::Statistics::Statistics()
     : d_instantiations("Instantiate::Instantiations_Total", 0),
       d_inst_duplicate("Instantiate::Duplicate_Inst", 0),
       d_inst_duplicate_eq("Instantiate::Duplicate_Inst_Eq", 0),
-      d_inst_duplicate_ent("Instantiate::Duplicate_Inst_Entailed", 0),
-      d_inst_duplicate_model_true("Instantiate::Duplicate_Inst_Model_True", 0)
+      d_inst_duplicate_ent("Instantiate::Duplicate_Inst_Entailed", 0)
 {
   smtStatisticsRegistry()->registerStat(&d_instantiations);
   smtStatisticsRegistry()->registerStat(&d_inst_duplicate);
   smtStatisticsRegistry()->registerStat(&d_inst_duplicate_eq);
   smtStatisticsRegistry()->registerStat(&d_inst_duplicate_ent);
-  smtStatisticsRegistry()->registerStat(&d_inst_duplicate_model_true);
 }
 
 Instantiate::Statistics::~Statistics()
@@ -861,7 +848,6 @@ Instantiate::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);
 }
 
 } /* CVC4::theory::quantifiers namespace */

diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index 16ff1f2c3db7187fbfa47ad7ec3b65abb5f29975..cb40bbbbc099bdec0522b17cf2d2090d9161896e 100644 (file)
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -305,7 +305,6 @@ class Instantiate : public QuantifiersUtil
     IntStat d_inst_duplicate;
     IntStat d_inst_duplicate_eq;
     IntStat d_inst_duplicate_ent;
-    IntStat d_inst_duplicate_model_true;
     Statistics();
     ~Statistics();
   }; /* class Instantiate::Statistics */

diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index a8eda10bb438c4dbbab547ff2fe26c93a03541fa..cb1207912baa90cd2095dc8aed341cbcc326df7d 100644 (file)
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -32,7 +32,7 @@ QuantifiersModule::QEffort QuantifiersModule::needsModel(Theory::Effort e)
 
 eq::EqualityEngine* QuantifiersModule::getEqualityEngine() const
 {
-  return d_quantEngine->getActiveEqualityEngine();
+  return d_quantEngine->getMasterEqualityEngine();
 }
 
 bool QuantifiersModule::areEqual(TNode n1, TNode n2) const

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 7caa103a07cd8640044a18cd02be40d8c4e15931..6e5dca4ef37880f989b143b84e02d64d883e2ac8 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -249,7 +249,7 @@ void TermDb::addTerm(Node n,
 void TermDb::computeArgReps( TNode n ) {
   if (d_arg_reps.find(n) == d_arg_reps.end())
   {
-    eq::EqualityEngine * ee = d_quantEngine->getActiveEqualityEngine();
+    eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
     for (const TNode& nc : n)
     {
       TNode r = ee->hasTerm(nc) ? ee->getRepresentative(nc) : nc;
@@ -272,7 +272,7 @@ void TermDb::computeUfEqcTerms( TNode f ) {
   {
     ops.insert(ops.end(), d_ho_op_slaves[f].begin(), d_ho_op_slaves[f].end());
   }
-  eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine();
+  eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
   for (const Node& ff : ops)
   {
     for (const TNode& n : d_op_map[ff])
@@ -307,7 +307,7 @@ void TermDb::computeUfTerms( TNode f ) {
   unsigned nonCongruentCount = 0;
   unsigned alreadyCongruentCount = 0;
   unsigned relevantCount = 0;
-  eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine();
+  eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
   NodeManager* nm = NodeManager::currentNM();
   for (const Node& ff : ops)
   {
@@ -503,8 +503,8 @@ bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) {
     f = getOperatorRepresentative( f );
   }
   computeUfTerms( f );
-  Assert(!d_quantEngine->getActiveEqualityEngine()->hasTerm(r)
-         || d_quantEngine->getActiveEqualityEngine()->getRepresentative(r)
+  Assert(!d_quantEngine->getMasterEqualityEngine()->hasTerm(r)
+         || d_quantEngine->getMasterEqualityEngine()->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() ){
@@ -905,22 +905,18 @@ void TermDb::setTermInactive( Node n ) {
 bool TermDb::hasTermCurrent( Node n, bool useMode ) {
   if( !useMode ){
     return d_has_map.find( n )!=d_has_map.end();
-  }else{
-    //return d_quantEngine->getActiveEqualityEngine()->hasTerm( n ); //some assertions are not sent to EE
-    if (options::termDbMode() == options::TermDbMode::ALL)
-    {
-      return true;
-    }
-    else if (options::termDbMode() == options::TermDbMode::RELEVANT)
-    {
-      return d_has_map.find( n )!=d_has_map.end();
-    }
-    else
-    {
-      Assert(false);
-      return false;
-    }
   }
+  //some assertions are not sent to EE
+  if (options::termDbMode() == options::TermDbMode::ALL)
+  {
+    return true;
+  }
+  else if (options::termDbMode() == options::TermDbMode::RELEVANT)
+  {
+    return d_has_map.find( n )!=d_has_map.end();
+  }
+  Assert(false) << "TermDb::hasTermCurrent: Unknown termDbMode : " << options::termDbMode();
+  return false;
 }
 
 bool TermDb::isTermEligibleForInstantiation(TNode n, TNode f)
@@ -966,7 +962,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->getActiveEqualityEngine();
+      eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
       eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
       while (!eqc_i.isFinished())
       {
@@ -1021,7 +1017,7 @@ bool TermDb::reset( Theory::Effort effort ){
   d_func_map_rel_dom.clear();
   d_consistent_ee = true;
 
-  eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine();
+  eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
 
   Assert(ee->consistent());
   // if higher-order, add equalities for the purification terms now

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index bb5950c5e8561fc9f126896123557bd06a8f481b..eafcc1e851a8f1f32cce660a0a6b4262983d34d3 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -223,7 +223,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
   d_curr_effort_level = QuantifiersModule::QEFFORT_NONE;
   d_conflict = false;
   d_hasAddedLemma = false;
-  d_useModelEe = false;
   //don't add true lemma
   d_lemmas_produced_c[d_term_util->d_true] = true;
 
@@ -513,22 +512,9 @@ void QuantifiersEngine::ppNotifyAssertions(
 
 void QuantifiersEngine::check( Theory::Effort e ){
   CodeTimer codeTimer(d_statistics.d_time);
-  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.get()))
-    {
-      //we are done if model building was unsuccessful
-      flushLemmas();
-      if( d_hasAddedLemma ){
-        Trace("quant-engine-debug") << "...failed." << std::endl;
-        return;
-      }
-    }
-  }
-  
-  if( !getActiveEqualityEngine()->consistent() ){
+
+  if (!getMasterEqualityEngine()->consistent())
+  {
     Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl;
     return;
   }
@@ -1275,20 +1261,8 @@ eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine() const
   return d_te->getMasterEqualityEngine();
 }
 
-eq::EqualityEngine* QuantifiersEngine::getActiveEqualityEngine() const
-{
-  if( d_useModelEe ){
-    return d_model->getEqualityEngine();
-  }
-  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;
+  return d_eq_query->getInternalRepresentative(a, q, index);
 }
 
 bool QuantifiersEngine::getSynthSolutions(
@@ -1298,7 +1272,7 @@ bool QuantifiersEngine::getSynthSolutions(
 }
 
 void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) {
-  eq::EqualityEngine* ee = getActiveEqualityEngine();
+  eq::EqualityEngine* ee = getMasterEqualityEngine();
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
   std::map< TypeNode, int > typ_num;
   while( !eqcs_i.isFinished() ){

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index a4d858b16093b97146d973d9d748f12cced7b7a8..dd86c0db9239e0e12c876b992073976706a4159a 100644 (file)
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -74,8 +74,6 @@ public:
   //---------------------- utilities
   /** get the master equality engine */
   eq::EqualityEngine* getMasterEqualityEngine() const;
-  /** get the active equality engine */
-  eq::EqualityEngine* getActiveEqualityEngine() const;
   /** get equality query */
   EqualityQuery* getEqualityQuery() const;
   /** get the model builder */
@@ -228,8 +226,6 @@ public:
   void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false );
   /** notification when master equality engine is updated */
   void eqNotifyNewClass(TNode t);
-  /** use model equality engine */
-  bool usingModelEqualityEngine() const { return d_useModelEe; }
   /** debug print equality engine */
   void debugPrintEqualityEngine( const char * c );
   /** get internal representative
@@ -364,8 +360,6 @@ public:
   context::CDO<bool> d_conflict_c;
   /** has added lemma this round */
   bool d_hasAddedLemma;
-  /** whether to use model equality engine */
-  bool d_useModelEe;
   //------------- end temporary information during check
  private:
   /** list of all quantifiers seen */