diff options
| -rw-r--r-- | src/theory/theory_inference_manager.cpp | 59 | ||||
| -rw-r--r-- | src/theory/theory_inference_manager.h | 4 | ||||
| -rw-r--r-- | src/theory/uf/equality_engine.cpp | 15 | ||||
| -rw-r--r-- | 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<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; |