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.

diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index c152481b59b9790ec02644c7d59d87a4b147ebca..bfd23fb2304154501edeaff8c412e6bcb47ef767 100644 (file)
--- 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 181e678765755622b9fc7d49834757eb1936e25d..c61f4311b39de861b5d26a7ae9adafb08c88fa13 100644 (file)
--- 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 75294621a5ffbe4ad0f65b2c20b1d31b5e5ac2c4..34704181cb84efa3c2bd4cf5384e452e54f59cb0 100644 (file)
--- 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 aec2510f353d81ec1ab41cd6c40e234de4d17e06..0710ac6c7fd1d5d54a49bd9dd415d30287cadc6a 100644 (file)
--- 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;