Use standard equality engine information in quantifiers state (#5824)

This refactors quantifiers so that it uses the standard interfaces for setting up an equality engine and using it via TheoryState.

This eliminates the need for several special interfaces including getMasterEqualityEngine, CombinationEngine::getCoreEqualityEngine, and most uses of EqualityQuery.

8 files changed, 48 insertions, 38 deletions

diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index 0fd5249e8..cdee268d6 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -59,7 +59,7 @@ void CandidateGeneratorQE::resetForOperator(Node eqc, Node op)
     if( isExcludedEqc( eqc ) ){
       d_mode = cand_term_none;
     }else{
-      eq::EqualityEngine* ee = d_qe->getEqualityQuery()->getEngine();
+      eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine();
       if( ee->hasTerm( eqc ) ){
         TNodeTrie* tat = d_qe->getTermDatabase()->getTermArgTrie(eqc, op);
         if( tat ){
@@ -93,6 +93,7 @@ Node CandidateGeneratorQE::getNextCandidate(){
 Node CandidateGeneratorQE::getNextCandidateInternal()
 {
   if( d_mode==cand_term_db ){
+    eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine();
     Debug("cand-gen-qe") << "...get next candidate in tbd" << std::endl;
     //get next candidate term in the uf term database
     while( d_term_iter<d_term_iter_limit ){
@@ -103,7 +104,7 @@ Node CandidateGeneratorQE::getNextCandidateInternal()
           if( d_exclude_eqc.empty() ){
             return n;
           }else{
-            Node r = d_qe->getEqualityQuery()->getRepresentative( n );
+            Node r = ee->getRepresentative(n);
             if( d_exclude_eqc.find( r )==d_exclude_eqc.end() ){
               Debug("cand-gen-qe") << "...returning " << n << std::endl;
               return n;
@@ -143,8 +144,9 @@ CandidateGenerator( qe ), d_match_pattern( mpat ){
 }
 
 void CandidateGeneratorQELitDeq::reset( Node eqc ){
-  Node false_term = d_qe->getEqualityQuery()->getEngine()->getRepresentative( NodeManager::currentNM()->mkConst<bool>(false) );
-  d_eqc_false = eq::EqClassIterator( false_term, d_qe->getEqualityQuery()->getEngine() );
+  eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine();
+  Node falset = NodeManager::currentNM()->mkConst(false);
+  d_eqc_false = eq::EqClassIterator(falset, ee);
 }
 
 Node CandidateGeneratorQELitDeq::getNextCandidate(){
@@ -177,7 +179,7 @@ CandidateGeneratorQEAll::CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mp
 }
 
 void CandidateGeneratorQEAll::reset( Node eqc ) {
-  d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() );
+  d_eq = eq::EqClassesIterator(d_qe->getState().getEqualityEngine());
   d_firstTime = true;
 }
 
diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp
index cdfb9c85c..6d13ef2ee 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.cpp
+++ b/src/theory/quantifiers/ematching/ho_trigger.cpp
@@ -231,7 +231,7 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m)
     d_lchildren.clear();
     d_arg_to_arg_rep.clear();
     d_arg_vector.clear();
-    EqualityQuery* eq = d_quantEngine->getEqualityQuery();
+    quantifiers::QuantifiersState& qs = d_quantEngine->getState();
     for (std::pair<const TNode, std::vector<Node> >& ha : ho_var_apps_subs)
     {
       TNode var = ha.first;
@@ -283,10 +283,10 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m)
           }
           else if (!itf->second.isNull())
           {
-            if (!eq->areEqual(itf->second, args[k]))
+            if (!qs.areEqual(itf->second, args[k]))
             {
               if (!d_quantEngine->getTermDatabase()->isEntailed(
-                      itf->second.eqNode(args[k]), true, eq))
+                      itf->second.eqNode(args[k]), true))
               {
                 fixed_vals[k] = Node::null();
               }
@@ -318,7 +318,7 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m)
         {
           if (!itf->second.isNull())
           {
-            Node r = eq->getRepresentative(itf->second);
+            Node r = qs.getRepresentative(itf->second);
             std::map<Node, unsigned>::iterator itfr = arg_to_rep.find(r);
             if (itfr != arg_to_rep.end())
             {
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index 63731c444..4cdb207f3 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -24,6 +24,7 @@
 #include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/ematching/var_match_generator.h"
 #include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
@@ -285,7 +286,7 @@ int InstMatchGenerator::getMatch(
     Trace("matching-fail") << "Internal error for match generator." << std::endl;
     return -2;
   }
-  EqualityQuery* q = qe->getEqualityQuery();
+  quantifiers::QuantifiersState& qs = qe->getState();
   bool success = true;
   std::vector<int> prev;
   // if t is null
@@ -303,7 +304,7 @@ int InstMatchGenerator::getMatch(
       Trace("matching-debug2")
           << "Setting " << ct << " to " << t[i] << "..." << std::endl;
       bool addToPrev = m.get(ct).isNull();
-      if (!m.set(q, ct, t[i]))
+      if (!m.set(qs, ct, t[i]))
       {
         // match is in conflict
         Trace("matching-fail")
@@ -319,7 +320,7 @@ int InstMatchGenerator::getMatch(
     }
     else if (ct == -1)
     {
-      if (!q->areEqual(d_match_pattern[i], t[i]))
+      if (!qs.areEqual(d_match_pattern[i], t[i]))
       {
         Trace("matching-fail") << "Match fail arg: " << d_match_pattern[i]
                                << " and " << t[i] << std::endl;
@@ -335,7 +336,7 @@ int InstMatchGenerator::getMatch(
   if (d_match_pattern.getKind() == INST_CONSTANT)
   {
     bool addToPrev = m.get(d_children_types[0]).isNull();
-    if (!m.set(q, d_children_types[0], t))
+    if (!m.set(qs, d_children_types[0], t))
     {
       success = false;
     }
@@ -371,7 +372,7 @@ int InstMatchGenerator::getMatch(
       {
         if (t.getType().isBoolean())
         {
-          t_match = nm->mkConst(!q->areEqual(nm->mkConst(true), t));
+          t_match = nm->mkConst(!qs.areEqual(nm->mkConst(true), t));
         }
         else
         {
@@ -391,7 +392,7 @@ int InstMatchGenerator::getMatch(
     if (!t_match.isNull())
     {
       bool addToPrev = m.get(v).isNull();
-      if (!m.set(q, v, t_match))
+      if (!m.set(qs, v, t_match))
       {
         success = false;
       }
@@ -467,7 +468,7 @@ bool InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){
     // we did not properly initialize the candidate generator, thus we fail
     return false;
   }
-  eqc = qe->getEqualityQuery()->getRepresentative( eqc );
+  eqc = qe->getState().getRepresentative(eqc);
   Trace("matching-debug2") << this << " reset " << eqc << "." << std::endl;
   if( !d_eq_class_rel.isNull() && d_eq_class_rel.getKind()!=INST_CONSTANT ){
     d_eq_class = d_eq_class_rel;
@@ -509,7 +510,7 @@ int InstMatchGenerator::getNextMatch(Node f,
   Node t = d_curr_first_candidate;
   do{
     Trace("matching-debug2") << "Matching candidate : " << t << std::endl;
-    Assert(!qe->inConflict());
+    Assert(!qe->getState().isInConflict());
     //if t not null, try to fit it into match m
     if( !t.isNull() ){
       if( d_curr_exclude_match.find( t )==d_curr_exclude_match.end() ){
@@ -523,7 +524,8 @@ int InstMatchGenerator::getNextMatch(Node f,
       }
       //get the next candidate term t
       if( success<0 ){
-        t = qe->inConflict() ? Node::null() : d_cg->getNextCandidate();
+        t = qe->getState().isInConflict() ? Node::null()
+                                          : d_cg->getNextCandidate();
       }else{
         d_curr_first_candidate = d_cg->getNextCandidate();
       }
@@ -554,13 +556,15 @@ uint64_t InstMatchGenerator::addInstantiations(Node f,
       if (sendInstantiation(tparent, m))
       {
         addedLemmas++;
-        if( qe->inConflict() ){
+        if (qe->getState().isInConflict())
+        {
           break;
         }
       }
     }else{
       addedLemmas++;
-      if( qe->inConflict() ){
+      if (qe->getState().isInConflict())
+      {
         break;
       }
     }
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
index b4a7457a3..371bc3378 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/ematching/inst_match_generator_multi.h"
 
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers_engine.h"
 
 using namespace CVC4::kind;
@@ -174,7 +175,7 @@ uint64_t InstMatchGeneratorMulti::addInstantiations(Node q,
           << "...processing " << j << " / " << newMatches.size()
           << ", #lemmas = " << addedLemmas << std::endl;
       processNewMatch(qe, tparent, newMatches[j], i, addedLemmas);
-      if (qe->inConflict())
+      if (qe->getState().isInConflict())
       {
         return addedLemmas;
       }
@@ -221,7 +222,7 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe,
                                                        size_t endChildIndex,
                                                        bool modEq)
 {
-  Assert(!qe->inConflict());
+  Assert(!qe->getState().isInConflict());
   if (childIndex == endChildIndex)
   {
     // m is an instantiation
@@ -256,7 +257,7 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe,
                                  childIndex,
                                  endChildIndex,
                                  modEq);
-        if (qe->inConflict())
+        if (qe->getState().isInConflict())
         {
           break;
         }
@@ -280,13 +281,13 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe,
     {
       return;
     }
-    eq::EqualityEngine* ee = qe->getEqualityQuery()->getEngine();
+    quantifiers::QuantifiersState& qs = qe->getState();
     // check modulo equality for other possible instantiations
-    if (!ee->hasTerm(n))
+    if (!qs.hasTerm(n))
     {
       return;
     }
-    eq::EqClassIterator eqc(ee->getRepresentative(n), ee);
+    eq::EqClassIterator eqc(qs.getRepresentative(n), qs.getEqualityEngine());
     while (!eqc.isFinished())
     {
       Node en = (*eqc);
@@ -304,7 +305,7 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe,
                                    childIndex,
                                    endChildIndex,
                                    modEq);
-          if (qe->inConflict())
+          if (qe->getState().isInConflict())
           {
             break;
           }
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
index 8c3de21a9..b5ef7792d 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
@@ -67,6 +67,7 @@ uint64_t InstMatchGeneratorSimple::addInstantiations(Node q,
                                                      QuantifiersEngine* qe,
                                                      Trigger* tparent)
 {
+  quantifiers::QuantifiersState& qs = qe->getState();
   uint64_t addedLemmas = 0;
   TNodeTrie* tat;
   if (d_eqc.isNull())
@@ -83,16 +84,16 @@ uint64_t InstMatchGeneratorSimple::addInstantiations(Node q,
     {
       // iterate over all classes except r
       tat = qe->getTermDatabase()->getTermArgTrie(Node::null(), d_op);
-      if (tat && !qe->inConflict())
+      if (tat && !qs.isInConflict())
       {
-        Node r = qe->getEqualityQuery()->getRepresentative(d_eqc);
+        Node r = qs.getRepresentative(d_eqc);
         for (std::pair<const TNode, TNodeTrie>& t : tat->d_data)
         {
           if (t.first != r)
           {
             InstMatch m(q);
             addInstantiations(m, qe, addedLemmas, 0, &(t.second));
-            if (qe->inConflict())
+            if (qs.isInConflict())
             {
               break;
             }
@@ -105,7 +106,7 @@ uint64_t InstMatchGeneratorSimple::addInstantiations(Node q,
   Debug("simple-trigger-debug")
       << "Adding instantiations based on " << tat << " from " << d_op << " "
       << d_eqc << std::endl;
-  if (tat && !qe->inConflict())
+  if (tat && !qs.isInConflict())
   {
     InstMatch m(q);
     addInstantiations(m, qe, addedLemmas, 0, tat);
@@ -146,6 +147,7 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
     }
     return;
   }
+  quantifiers::QuantifiersState& qs = qe->getState();
   if (d_match_pattern[argIndex].getKind() == INST_CONSTANT)
   {
     int v = d_var_num[argIndex];
@@ -162,7 +164,7 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
           m.setValue(v, t);
           addInstantiations(m, qe, addedLemmas, argIndex + 1, &(tt.second));
           m.setValue(v, prev);
-          if (qe->inConflict())
+          if (qs.isInConflict())
           {
             break;
           }
@@ -172,7 +174,7 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
     }
     // inst constant from another quantified formula, treat as ground term?
   }
-  Node r = qe->getEqualityQuery()->getRepresentative(d_match_pattern[argIndex]);
+  Node r = qs.getRepresentative(d_match_pattern[argIndex]);
   std::map<TNode, TNodeTrie>::iterator it = tat->d_data.find(r);
   if (it != tat->d_data.end())
   {
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index cd0ab7976..48c02f288 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -98,8 +98,9 @@ void InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
           Trace("inst-engine-debug")
               << " -> unfinished= "
               << (quantStatus == InstStrategyStatus::STATUS_UNFINISHED)
-              << ", conflict=" << d_quantEngine->inConflict() << std::endl;
-          if( d_quantEngine->inConflict() ){
+              << ", conflict=" << d_qstate.isInConflict() << std::endl;
+          if (d_qstate.isInConflict())
+          {
             return;
           }
           else if (quantStatus == InstStrategyStatus::STATUS_UNFINISHED)
@@ -165,7 +166,7 @@ void InstantiationEngine::check(Theory::Effort e, QEffort quant_e)
   {
     unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
     doInstantiationRound(e);
-    if (d_quantEngine->inConflict())
+    if (d_qstate.isInConflict())
     {
       Assert(d_quantEngine->getNumLemmasWaiting() > lastWaiting);
       Trace("inst-engine") << "Conflict, added lemmas = "
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 470120be2..b1caa739e 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -109,7 +109,7 @@ uint64_t Trigger::addInstantiations()
   {
     // for each ground term t that does not exist in the equality engine, we
     // add a purification lemma of the form (k = t).
-    eq::EqualityEngine* ee = d_quantEngine->getEqualityQuery()->getEngine();
+    eq::EqualityEngine* ee = d_quantEngine->getState().getEqualityEngine();
     for (const Node& gt : d_groundTerms)
     {
       if (!ee->hasTerm(gt))
diff --git a/src/theory/quantifiers/ematching/var_match_generator.cpp b/src/theory/quantifiers/ematching/var_match_generator.cpp
index 0553c1745..4edacb827 100644
--- a/src/theory/quantifiers/ematching/var_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/var_match_generator.cpp
@@ -52,7 +52,7 @@ int VarMatchGeneratorTermSubs::getNextMatch(Node q,
     d_eq_class = Node::null();
     // if( s.getType().isSubtypeOf( d_var_type ) ){
     d_rm_prev = m.get(d_children_types[0]).isNull();
-    if (!m.set(qe->getEqualityQuery(), d_children_types[0], s))
+    if (!m.set(qe->getState(), d_children_types[0], s))
     {
       return -1;
     }