From: Andrew Reynolds Date: Thu, 29 Jul 2021 15:53:48 +0000 (-0500) Subject: Minor updates to shared terms database for central equality engine (#6929) X-Git-Tag: cvc5-1.0.0~1431 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f2672e53fae29abe40fc69b004d1df5be0ce1e8b;p=cvc5.git Minor updates to shared terms database for central equality engine (#6929) Includes proper set up of the proof equality engine it uses (which may be shared over multiple theories). Also makes its assertEquality method robust to non-equality atoms. --- diff --git a/src/theory/shared_solver.h b/src/theory/shared_solver.h index 4786d6fc9..e2cda0fbc 100644 --- a/src/theory/shared_solver.h +++ b/src/theory/shared_solver.h @@ -95,17 +95,15 @@ class SharedSolver */ virtual TrustNode explain(TNode literal, TheoryId id) = 0; /** - * Assert equality to the shared terms database. + * Assert n to the shared terms database. * * This method is called by TheoryEngine when a fact has been marked to * send to THEORY_BUILTIN, meaning that shared terms database should - * maintain this fact. This is the case when either an equality is - * asserted from the SAT solver or a theory propagates an equality between - * shared terms. + * maintain this fact. In the distributed equality engine architecture, + * this is the case when either an equality is asserted from the SAT solver + * or a theory propagates an equality between shared terms. */ - virtual void assertSharedEquality(TNode equality, - bool polarity, - TNode reason) = 0; + virtual void assertShared(TNode n, bool polarity, TNode reason) = 0; /** Is term t a shared term? */ virtual bool isShared(TNode t) const; diff --git a/src/theory/shared_solver_distributed.cpp b/src/theory/shared_solver_distributed.cpp index 58a5b4f6c..3c78a75f8 100644 --- a/src/theory/shared_solver_distributed.cpp +++ b/src/theory/shared_solver_distributed.cpp @@ -86,11 +86,9 @@ TrustNode SharedSolverDistributed::explain(TNode literal, TheoryId id) return texp; } -void SharedSolverDistributed::assertSharedEquality(TNode equality, - bool polarity, - TNode reason) +void SharedSolverDistributed::assertShared(TNode n, bool polarity, TNode reason) { - d_sharedTerms.assertEquality(equality, polarity, reason); + d_sharedTerms.assertShared(n, polarity, reason); } } // namespace theory diff --git a/src/theory/shared_solver_distributed.h b/src/theory/shared_solver_distributed.h index dab190264..f9a00230b 100644 --- a/src/theory/shared_solver_distributed.h +++ b/src/theory/shared_solver_distributed.h @@ -42,10 +42,8 @@ class SharedSolverDistributed : public SharedSolver /** Set equality engine in the shared terms database */ void setEqualityEngine(eq::EqualityEngine* ee) override; //------------------------------------- end initialization - /** Assert equality to the shared terms database. */ - void assertSharedEquality(TNode equality, - bool polarity, - TNode reason) override; + /** Assert n to the shared terms database. */ + void assertShared(TNode n, bool polarity, TNode reason) override; /** * Get equality status based on the equality engine of shared terms database */ diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index 0e17f50a9..a4a846e05 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -51,18 +51,24 @@ void SharedTermsDatabase::setEqualityEngine(eq::EqualityEngine* ee) { Assert(ee != nullptr); d_equalityEngine = ee; - // if proofs are enabled, make the proof equality engine + // if proofs are enabled, make the proof equality engine if necessary if (d_pnm != nullptr) { - d_pfee.reset( - new eq::ProofEqEngine(d_satContext, d_userContext, *ee, d_pnm)); + d_pfee = d_equalityEngine->getProofEqualityEngine(); + if (d_pfee == nullptr) + { + d_pfeeAlloc.reset( + new eq::ProofEqEngine(d_satContext, d_userContext, *ee, d_pnm)); + d_pfee = d_pfeeAlloc.get(); + d_equalityEngine->setProofEqualityEngine(d_pfee); + } } } bool SharedTermsDatabase::needsEqualityEngine(EeSetupInfo& esi) { esi.d_notify = &d_EENotify; - esi.d_name = "SharedTermsDatabase"; + esi.d_name = "shared::ee"; return true; } @@ -243,12 +249,21 @@ theory::eq::EqualityEngine* SharedTermsDatabase::getEqualityEngine() return d_equalityEngine; } -void SharedTermsDatabase::assertEquality(TNode equality, bool polarity, TNode reason) +void SharedTermsDatabase::assertShared(TNode n, bool polarity, TNode reason) { Assert(d_equalityEngine != nullptr); - Debug("shared-terms-database::assert") << "SharedTermsDatabase::assertEquality(" << equality << ", " << (polarity ? "true" : "false") << ", " << reason << ")" << endl; + Debug("shared-terms-database::assert") + << "SharedTermsDatabase::assertShared(" << n << ", " + << (polarity ? "true" : "false") << ", " << reason << ")" << endl; // Add it to the equality engine - d_equalityEngine->assertEquality(equality, polarity, reason); + if (n.getKind() == kind::EQUAL) + { + d_equalityEngine->assertEquality(n, polarity, reason); + } + else + { + d_equalityEngine->assertPredicate(n, polarity, reason); + } // Check for conflict checkForConflict(); } diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index 4e09ac23f..ddb1a4043 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -174,9 +174,9 @@ class SharedTermsDatabase : public context::ContextNotifyObj { //-------------------------------------------- end initialization /** - * Asserts the equality to the shared terms database, + * Asserts n to the shared terms database with given polarity and reason */ - void assertEquality(TNode equality, bool polarity, TNode reason); + void assertShared(TNode n, bool polarity, TNode reason); /** * Return whether the equality is alreday known to the engine @@ -271,8 +271,10 @@ class SharedTermsDatabase : public context::ContextNotifyObj { context::UserContext* d_userContext; /** Equality engine */ theory::eq::EqualityEngine* d_equalityEngine; - /** Proof equality engine */ - std::unique_ptr d_pfee; + /** Proof equality engine, if we allocated one */ + std::unique_ptr d_pfeeAlloc; + /** The proof equality engine we are using */ + theory::eq::ProofEqEngine* d_pfee; /** The proof node manager */ ProofNodeManager* d_pnm; }; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index f98f1cb6c..58014b06b 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -919,7 +919,7 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo // assert to the shared solver bool polarity = assertion.getKind() != kind::NOT; TNode atom = polarity ? assertion : assertion[0]; - d_sharedSolver->assertSharedEquality(atom, polarity, assertion); + d_sharedSolver->assertShared(atom, polarity, assertion); } return; }