Remove equality inference option for quantifiers (#3282)

6 files changed, 17 insertions, 111 deletions

diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp
index 22d6a3782..bb0306c06 100644
--- a/src/theory/quantifiers/equality_query.cpp
+++ b/src/theory/quantifiers/equality_query.cpp
@@ -32,8 +32,10 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe ) : d_qe( qe ), d_eqi_counter( c ), d_reset_count( 0 ){
-
+EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine(
+    context::Context* c, QuantifiersEngine* qe)
+    : d_qe(qe), d_eqi_counter(c), d_reset_count(0)
+{
 }
 
 EqualityQueryQuantifiersEngine::~EqualityQueryQuantifiersEngine(){
@@ -42,43 +44,6 @@ EqualityQueryQuantifiersEngine::~EqualityQueryQuantifiersEngine(){
 bool EqualityQueryQuantifiersEngine::reset( Theory::Effort e ){
   d_int_rep.clear();
   d_reset_count++;
-  return processInferences( e );
-}
-
-bool EqualityQueryQuantifiersEngine::processInferences( Theory::Effort e ) {
-  if( options::inferArithTriggerEq() ){
-    eq::EqualityEngine* ee = getEngine();
-    //updated implementation
-    EqualityInference * ei = d_qe->getEqualityInference();
-    while( d_eqi_counter.get()<ei->getNumPendingMerges() ){
-      Node eq = ei->getPendingMerge( d_eqi_counter.get() );
-      Node eq_exp = ei->getPendingMergeExplanation( d_eqi_counter.get() );
-      Trace("quant-engine-ee-proc") << "processInferences : Infer : " << eq << std::endl;
-      Trace("quant-engine-ee-proc") << "      explanation : " << eq_exp << std::endl;
-      Assert( ee->hasTerm( eq[0] ) );
-      Assert( ee->hasTerm( eq[1] ) );
-      if( areDisequal( eq[0], eq[1] ) ){
-        Trace("quant-engine-ee-proc") << "processInferences : Conflict : " << eq << std::endl;
-        if( Trace.isOn("term-db-lemma") ){
-          Trace("term-db-lemma") << "Disequal terms, equal by normalization : " << eq[0] << " " << eq[1] << "!!!!" << std::endl;
-          if( !d_qe->getTheoryEngine()->needCheck() ){
-            Trace("term-db-lemma") << "  all theories passed with no lemmas." << std::endl;
-            //this should really never happen (implies arithmetic is incomplete when sharing is enabled)
-            Assert( false );
-          }
-          Trace("term-db-lemma") << "  add split on : " << eq << std::endl;
-        }
-        eq = Rewriter::rewrite(eq);
-        Node split = NodeManager::currentNM()->mkNode(OR, eq, eq.negate());
-        d_qe->addLemma(split);
-        return false;
-      }else{
-        ee->assertEquality( eq, true, eq_exp );
-        d_eqi_counter = d_eqi_counter.get() + 1;
-      }
-    }
-    Assert( ee->consistent() );
-  }
   return true;
 }
 
diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h
index 1000b97e9..7766a335a 100644
--- a/src/theory/quantifiers/equality_query.h
+++ b/src/theory/quantifiers/equality_query.h
@@ -27,22 +27,19 @@ namespace theory {
 namespace quantifiers {
 
 /** EqualityQueryQuantifiersEngine class
-* This is a wrapper class around an equality engine that is used for
-* queries required by algorithms in the quantifiers theory.
-* It uses an equality engine, as determined by the quantifiers engine it points
-* to.
-*
-* The main extension of this class wrt EqualityQuery is the function
-* getInternalRepresentative, which is used by instantiation-based methods
-* that are agnostic with respect to choosing terms within an equivalence class.
-* Examples of such methods are finite model finding and enumerative
-* instantiation.
-* Method getInternalRepresentative returns the "best" representative based on
-* the internal heuristic,
-* which is currently based on choosing the term that was previously chosen as a
-* representative
-* earliest.
-*/
+ *
+ * This is a wrapper class around an equality engine that is used for
+ * queries required by algorithms in the quantifiers theory. It uses an equality
+ * engine, as determined by the quantifiers engine it points to.
+ *
+ * The main extension of this class wrt EqualityQuery is the function
+ * getInternalRepresentative, which is used by instantiation-based methods
+ * that are agnostic with respect to choosing terms within an equivalence class.
+ * Examples of such methods are finite model finding and enumerative
+ * instantiation. Method getInternalRepresentative returns the "best"
+ * representative based on the internal heuristic, which is currently based on
+ * choosing the term that was previously chosen as a representative earliest.
+ */
 class EqualityQueryQuantifiersEngine : public EqualityQuery
 {
  public:
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index a6ec1c077..507d938b4 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -188,7 +188,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
                                      TheoryEngine* te)
     : d_te(te),
       d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(c, this)),
-      d_eq_inference(nullptr),
       d_tr_trie(new inst::TriggerTrie),
       d_model(nullptr),
       d_rel_dom(nullptr),
@@ -237,9 +236,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
     d_instantiate->addNotify(d_private->d_inst_prop->getInstantiationNotify());
   }
   
-  if( options::inferArithTriggerEq() ){
-    d_eq_inference.reset(new quantifiers::EqualityInference(c, false));
-  }
 
   d_util.push_back(d_instantiate.get());
 
@@ -328,10 +324,6 @@ EqualityQuery* QuantifiersEngine::getEqualityQuery() const
 {
   return d_eq_query.get();
 }
-quantifiers::EqualityInference* QuantifiersEngine::getEqualityInference() const
-{
-  return d_eq_inference.get();
-}
 quantifiers::RelevantDomain* QuantifiersEngine::getRelevantDomain() const
 {
   return d_rel_dom.get();
@@ -1040,25 +1032,6 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool within
 
 void QuantifiersEngine::eqNotifyNewClass(TNode t) {
   addTermToDatabase( t );
-  if( d_eq_inference ){
-    d_eq_inference->eqNotifyNewClass( t );
-  }
-}
-
-void QuantifiersEngine::eqNotifyPreMerge(TNode t1, TNode t2) {
-  if( d_eq_inference ){
-    d_eq_inference->eqNotifyMerge( t1, t2 );
-  }
-}
-
-void QuantifiersEngine::eqNotifyPostMerge(TNode t1, TNode t2) {
-
-}
-
-void QuantifiersEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
-  //if( d_qcf ){
-  //  d_qcf->assertDisequal( t1, t2 );
-  //}
 }
 
 bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 0a534d090..e1fc742af 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -25,7 +25,6 @@
 #include "expr/attribute.h"
 #include "expr/term_canonize.h"
 #include "theory/quantifiers/ematching/trigger.h"
-#include "theory/quantifiers/equality_infer.h"
 #include "theory/quantifiers/equality_query.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/fmf/model_builder.h"
@@ -106,8 +105,6 @@ public:
   inst::TriggerTrie* getTriggerDatabase() const;
   //---------------------- end utilities
   //---------------------- utilities (TODO move these utilities #1163)
-  /** get the equality inference */
-  quantifiers::EqualityInference* getEqualityInference() const;
   /** get relevant domain */
   quantifiers::RelevantDomain* getRelevantDomain() const;
   //---------------------- end utilities
@@ -228,9 +225,6 @@ public:
   void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false );
   /** notification when master equality engine is updated */
   void eqNotifyNewClass(TNode t);
-  void eqNotifyPreMerge(TNode t1, TNode t2);
-  void eqNotifyPostMerge(TNode t1, TNode t2);
-  void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
   /** use model equality engine */
   bool usingModelEqualityEngine() const { return d_useModelEe; }
   /** debug print equality engine */
@@ -316,8 +310,6 @@ public:
   //------------- quantifiers utilities
   /** equality query class */
   std::unique_ptr<quantifiers::EqualityQueryQuantifiersEngine> d_eq_query;
-  /** equality inference class */
-  std::unique_ptr<quantifiers::EqualityInference> d_eq_inference;
   /** all triggers will be stored in this trie */
   std::unique_ptr<inst::TriggerTrie> d_tr_trie;
   /** extended model object */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index b8f6bf15c..8348c24d5 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -260,24 +260,6 @@ void TheoryEngine::eqNotifyNewClass(TNode t){
   }
 }
 
-void TheoryEngine::eqNotifyPreMerge(TNode t1, TNode t2){
-  if (d_logicInfo.isQuantified()) {
-    d_quantEngine->eqNotifyPreMerge( t1, t2 );
-  }
-}
-
-void TheoryEngine::eqNotifyPostMerge(TNode t1, TNode t2){
-  if (d_logicInfo.isQuantified()) {
-    d_quantEngine->eqNotifyPostMerge( t1, t2 );
-  }
-}
-
-void TheoryEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){
-  if (d_logicInfo.isQuantified()) {
-    d_quantEngine->eqNotifyDisequal( t1, t2, reason );
-  }
-}
-
 TheoryEngine::TheoryEngine(context::Context* context,
                            context::UserContext* userContext,
                            RemoveTermFormulas& iteRemover,
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 23d3282de..587d3693c 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -174,15 +174,12 @@ class TheoryEngine {
     void eqNotifyNewClass(TNode t) override { d_te.eqNotifyNewClass(t); }
     void eqNotifyPreMerge(TNode t1, TNode t2) override
     {
-      d_te.eqNotifyPreMerge(t1, t2);
     }
     void eqNotifyPostMerge(TNode t1, TNode t2) override
     {
-      d_te.eqNotifyPostMerge(t1, t2);
     }
     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override
     {
-      d_te.eqNotifyDisequal(t1, t2, reason);
     }
   };/* class TheoryEngine::NotifyClass */
   NotifyClass d_masterEENotify;