Refactor setup of proof equality engine for central EE (#6831)

Users of an equality engine should each use the same proof equality engine that wraps it. This ensures that theory inference managers do so, by tracking the official proof equality engine for an equality engine in theory inference manager.

This is in preparation for (proper equality proofs for) central equality engine.

It also adds some debugging code that is highly useful for debugging issues related to when equalities are processed in theory inference manager.

4 files changed, 74 insertions, 12 deletions

diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index c152481b5..bfd23fb23 100644
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -39,6 +39,7 @@ TheoryInferenceManager::TheoryInferenceManager(Theory& t,
       d_out(t.getOutputChannel()),
       d_ee(nullptr),
       d_decManager(nullptr),
+      d_pfee(nullptr),
       d_pnm(pnm),
       d_cacheLemmas(cacheLemmas),
       d_keep(t.getSatContext()),
@@ -66,13 +67,21 @@ void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee)
 {
   d_ee = ee;
   // if proofs are enabled, also make a proof equality engine to wrap ee
-  // if it is non-null
+  // if it is non-null. If its proof equality engine has already been assigned,
+  // use it. This is to ensure that all theories use the same proof equality
+  // engine when in ee-mode=central.
   if (d_pnm != nullptr && d_ee != nullptr)
   {
-    d_pfee.reset(new eq::ProofEqEngine(d_theoryState.getSatContext(),
-                                       d_theoryState.getUserContext(),
-                                       *d_ee,
-                                       d_pnm));
+    d_pfee = d_ee->getProofEqualityEngine();
+    if (d_pfee == nullptr)
+    {
+      d_pfeeAlloc.reset(new eq::ProofEqEngine(d_theoryState.getSatContext(),
+                                              d_theoryState.getUserContext(),
+                                              *d_ee,
+                                              d_pnm));
+      d_pfee = d_pfeeAlloc.get();
+      d_ee->setProofEqualityEngine(d_pfee);
+    }
   }
 }
 
@@ -96,10 +105,7 @@ bool TheoryInferenceManager::hasSent() const
          || d_numCurrentFacts > 0;
 }
 
-eq::ProofEqEngine* TheoryInferenceManager::getProofEqEngine()
-{
-  return d_pfee.get();
-}
+eq::ProofEqEngine* TheoryInferenceManager::getProofEqEngine() { return d_pfee; }
 
 void TheoryInferenceManager::conflictEqConstantMerge(TNode a, TNode b)
 {
@@ -388,6 +394,41 @@ bool TheoryInferenceManager::processInternalFact(TNode atom,
   Trace("infer-manager") << "TheoryInferenceManager::assertInternalFact: "
                          << (pol ? Node(atom) : atom.notNode()) << " from "
                          << expn << std::endl;
+  if (Configuration::isAssertionBuild())
+  {
+    // check that all facts hold in the equality engine, to ensure that we
+    // aren't processing a stale fact
+    std::vector<Node> expc = exp;
+    for (size_t i = 0; i < expc.size(); i++)
+    {
+      Node e = expc[i];
+      bool epol = e.getKind() != NOT;
+      Node eatom = epol ? e : e[0];
+      Trace("infer-manager")
+          << "...check " << eatom << " " << epol << std::endl;
+      if (eatom.getKind() == AND)
+      {
+        Assert(epol);
+        for (const Node& ea : eatom)
+        {
+          expc.push_back(ea);
+        }
+        continue;
+      }
+      else if (eatom.getKind() == EQUAL)
+      {
+        Assert(d_ee->hasTerm(eatom[0]));
+        Assert(d_ee->hasTerm(eatom[1]));
+        Assert(!epol || d_ee->areEqual(eatom[0], eatom[1]));
+        Assert(epol || d_ee->areDisequal(eatom[0], eatom[1], false));
+      }
+      else
+      {
+        Assert(d_ee->hasTerm(eatom));
+        Assert(d_ee->areEqual(eatom, NodeManager::currentNM()->mkConst(epol)));
+      }
+    }
+  }
   d_numCurrentFacts++;
   // Now, assert the fact. How to do so depends on whether proofs are enabled.
   // If no proof production, or no proof rule was given
diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
index 181e67876..c61f4311b 100644
--- a/src/theory/theory_inference_manager.h
+++ b/src/theory/theory_inference_manager.h
@@ -434,7 +434,9 @@ class TheoryInferenceManager
   /** Pointer to the decision manager */
   DecisionManager* d_decManager;
   /** A proof equality engine */
-  std::unique_ptr<eq::ProofEqEngine> d_pfee;
+  eq::ProofEqEngine* d_pfee;
+  /** The proof equality engine we allocated */
+  std::unique_ptr<eq::ProofEqEngine> d_pfeeAlloc;
   /** The proof node manager of the theory */
   ProofNodeManager* d_pnm;
   /** Whether this manager caches lemmas */
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 75294621a..34704181c 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -133,7 +133,8 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify,
                                bool constantsAreTriggers,
                                bool anyTermTriggers)
     : ContextNotifyObj(context),
-      d_masterEqualityEngine(0),
+      d_masterEqualityEngine(nullptr),
+      d_proofEqualityEngine(nullptr),
       d_context(context),
       d_done(context, false),
       d_notify(&s_notifyNone),
@@ -161,10 +162,20 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify,
 }
 
 void EqualityEngine::setMasterEqualityEngine(EqualityEngine* master) {
-  Assert(d_masterEqualityEngine == 0);
+  Assert(d_masterEqualityEngine == nullptr);
   d_masterEqualityEngine = master;
 }
 
+void EqualityEngine::setProofEqualityEngine(ProofEqEngine* pfee)
+{
+  Assert(d_proofEqualityEngine == nullptr);
+  d_proofEqualityEngine = pfee;
+}
+ProofEqEngine* EqualityEngine::getProofEqualityEngine()
+{
+  return d_proofEqualityEngine;
+}
+
 void EqualityEngine::enqueue(const MergeCandidate& candidate, bool back) {
   Debug("equality") << d_name << "::eq::enqueue({" << candidate.d_t1Id << "} "
                     << d_nodes[candidate.d_t1Id] << ", {" << candidate.d_t2Id
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index aec2510f3..0710ac6c7 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -43,6 +43,7 @@ namespace eq {
 class EqClassesIterator;
 class EqClassIterator;
 class EqProof;
+class ProofEqEngine;
 
 /**
  * Class for keeping an incremental congruence closure over a set of terms. It provides
@@ -62,6 +63,9 @@ class EqualityEngine : public context::ContextNotifyObj {
    */
   EqualityEngine* d_masterEqualityEngine;
 
+  /** Proof equality engine */
+  ProofEqEngine* d_proofEqualityEngine;
+
  public:
   /**
    * Initialize the equality engine, given the notification class.
@@ -93,6 +97,10 @@ class EqualityEngine : public context::ContextNotifyObj {
    * of all the terms and equalities from this engine.
    */
   void setMasterEqualityEngine(EqualityEngine* master);
+  /** Set the proof equality engine for this one. */
+  void setProofEqualityEngine(ProofEqEngine* pfee);
+  /** Get the proof equality engine */
+  ProofEqEngine* getProofEqualityEngine();
 
   /** Print the equivalence classes for debugging */
   std::string debugPrintEqc() const;