From 704127085e5ba2deb19e41337908a340e1b191dd Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 14 Jul 2021 09:15:25 -0500 Subject: [PATCH] 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. --- src/theory/theory_inference_manager.cpp | 59 +++++++++++++++++++++---- src/theory/theory_inference_manager.h | 4 +- src/theory/uf/equality_engine.cpp | 15 ++++++- src/theory/uf/equality_engine.h | 8 ++++ 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 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 d_pfee; + eq::ProofEqEngine* d_pfee; + /** The proof equality engine we allocated */ + std::unique_ptr 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; -- 2.30.2