From a5b834d5af88e372d9c6340653f831a09daf1d39 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 3 Sep 2020 19:15:30 -0500 Subject: Add interfaces for making trust nodes in TheoryInferenceManager. (#5016) This gives theories a finer grained control over explained lemmas and conflicts. A theory may now use an inference manager to construct "explained" lemmas/conflicts e.g. via mkLemmaExp, subsequently do any theory-specific debugging or modification to that lemma before sending it via trustedLemma. This is required for the new strings inference manager on proof-new. This also adds a missing variant of conflicts for the proof equality engine. It also does a minor simplification of a previous variant for constructing conflicts from proof equality engine based on a proof step buffer. --- src/theory/theory_inference_manager.cpp | 94 ++++++++++++++++++++++++++------- src/theory/theory_inference_manager.h | 52 ++++++++++++++++-- src/theory/uf/proof_equality_engine.cpp | 23 ++++---- src/theory/uf/proof_equality_engine.h | 2 + 4 files changed, 136 insertions(+), 35 deletions(-) (limited to 'src/theory') diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index 330613e2e..40fa9c5ae 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -50,6 +50,8 @@ void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee) } } +bool TheoryInferenceManager::isProofEnabled() const { return d_pnm != nullptr; } + void TheoryInferenceManager::reset() { d_numCurrentLemmas = 0; @@ -96,21 +98,52 @@ void TheoryInferenceManager::conflictExp(PfRule id, { if (!d_theoryState.isInConflict()) { - if (d_pfee != nullptr) - { - // use proof equality engine to construct the trust node - TrustNode tconf = d_pfee->assertConflict(id, exp, args); - d_out.trustedConflict(tconf); - } - else - { - // version without proofs - Node conf = mkExplainPartial(exp, {}); - conflict(conf); - } + // make the trust node + TrustNode tconf = mkConflictExp(id, exp, args); + // send it on the output channel + trustedConflict(tconf); } } +TrustNode TheoryInferenceManager::mkConflictExp(PfRule id, + const std::vector& exp, + const std::vector& args) +{ + if (d_pfee != nullptr) + { + // use proof equality engine to construct the trust node + return d_pfee->assertConflict(id, exp, args); + } + // version without proofs + Node conf = mkExplainPartial(exp, {}); + return TrustNode::mkTrustConflict(conf, nullptr); +} + +void TheoryInferenceManager::conflictExp(const std::vector& exp, + ProofGenerator* pg) +{ + if (!d_theoryState.isInConflict()) + { + // make the trust node + TrustNode tconf = mkConflictExp(exp, pg); + // send it on the output channel + trustedConflict(tconf); + } +} + +TrustNode TheoryInferenceManager::mkConflictExp(const std::vector& exp, + ProofGenerator* pg) +{ + if (d_pfee != nullptr) + { + // use proof equality engine to construct the trust node + return d_pfee->assertConflict(exp, pg); + } + // version without proofs + Node conf = mkExplainPartial(exp, {}); + return TrustNode::mkTrustConflict(conf, nullptr); +} + bool TheoryInferenceManager::propagateLit(TNode lit) { // If already in conflict, no more propagation @@ -190,17 +223,28 @@ bool TheoryInferenceManager::lemmaExp(Node conc, const std::vector& args, LemmaProperty p, bool doCache) +{ + // make the trust node + TrustNode trn = mkLemmaExp(conc, id, exp, noExplain, args); + // send it on the output channel + return trustedLemma(trn, p, doCache); +} + +TrustNode TheoryInferenceManager::mkLemmaExp(Node conc, + PfRule id, + const std::vector& exp, + const std::vector& noExplain, + const std::vector& args) { if (d_pfee != nullptr) { // make the trust node from the proof equality engine - TrustNode trn = d_pfee->assertLemma(conc, id, exp, noExplain, args); - return trustedLemma(trn, p, doCache); + return d_pfee->assertLemma(conc, id, exp, noExplain, args); } - // otherwise, not using proofs, explain and send lemma + // otherwise, not using proofs, explain and make trust node Node ant = mkExplainPartial(exp, noExplain); Node lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, ant, conc); - return lemma(lem, p, doCache); + return TrustNode::mkTrustLemma(lem, nullptr); } bool TheoryInferenceManager::lemmaExp(Node conc, @@ -209,17 +253,27 @@ bool TheoryInferenceManager::lemmaExp(Node conc, ProofGenerator* pg, LemmaProperty p, bool doCache) +{ + // make the trust node + TrustNode trn = mkLemmaExp(conc, exp, noExplain, pg); + // send it on the output channel + return trustedLemma(trn, p, doCache); +} + +TrustNode TheoryInferenceManager::mkLemmaExp(Node conc, + const std::vector& exp, + const std::vector& noExplain, + ProofGenerator* pg) { if (d_pfee != nullptr) { // make the trust node from the proof equality engine - TrustNode trn = d_pfee->assertLemma(conc, exp, noExplain, pg); - return trustedLemma(trn, p, doCache); + return d_pfee->assertLemma(conc, exp, noExplain, pg); } - // otherwise, not using proofs, explain and send lemma + // otherwise, not using proofs, explain and make trust node Node ant = mkExplainPartial(exp, noExplain); Node lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, ant, conc); - return lemma(lem, p, doCache); + return TrustNode::mkTrustLemma(lem, nullptr); } bool TheoryInferenceManager::hasCachedLemma(TNode lem, LemmaProperty p) diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index 080a09ba8..92116648e 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -76,6 +76,11 @@ class TheoryInferenceManager * of theory. */ void setEqualityEngine(eq::EqualityEngine* ee); + /** + * Are proofs enabled in this inference manager? Returns true if the proof + * node manager pnm provided to the constructor of this class was non-null. + */ + bool isProofEnabled() const; /** * Reset, which resets counters regarding the number of added lemmas and * internal facts. This method should be manually called by the theory at @@ -127,7 +132,7 @@ class TheoryInferenceManager void conflict(TNode conf); /** * Raise trusted conflict tconf (of any form) where a proof generator has - * been provided in a custom way. + * been provided (as part of the trust node) in a custom way. */ void trustedConflict(TrustNode tconf); /** @@ -140,6 +145,29 @@ class TheoryInferenceManager void conflictExp(PfRule id, const std::vector& exp, const std::vector& args); + /** + * Make the trust node corresponding to the conflict of the above form. It is + * the responsibility of the caller to subsequently call trustedConflict with + * the returned trust node. + */ + TrustNode mkConflictExp(PfRule id, + const std::vector& exp, + const std::vector& args); + /** + * Explain and send conflict from contradictory facts. This method is called + * when proof generator pg has a proof of false from free assumptions exp. + * This method sends a trusted conflict corresponding to the official + * equality engine's explanation of literals in exp, with the proof equality + * engine as the proof generator (if it exists), where pg provides the + * final step(s) of this proof during this call. + */ + void conflictExp(const std::vector& exp, ProofGenerator* pg); + /** + * Make the trust node corresponding to the conflict of the above form. It is + * the responsibility of the caller to subsequently call trustedConflict with + * the returned trust node. + */ + TrustNode mkConflictExp(const std::vector& exp, ProofGenerator* pg); //--------------------------------------- lemmas /** * Send (trusted) lemma lem with property p on the output channel. @@ -190,10 +218,20 @@ class TheoryInferenceManager const std::vector& args, LemmaProperty p = LemmaProperty::NONE, bool doCache = true); + /** + * Make the trust node for the above method. It is responsibility of the + * caller to subsequently call trustedLemma with the returned trust node. + */ + TrustNode mkLemmaExp(Node conc, + PfRule id, + const std::vector& exp, + const std::vector& noExplain, + const std::vector& args); /** * Same as above, but where pg can provide a proof of conc from free - * assumptions in exp. It is required to do so in the remainder of the user - * context when this method returns true. + * assumptions in exp. This sends a trusted lemma on the output channel where + * the proof equality engine is the proof generator. The generator pg + * is asked to provide the final step(s) of this proof during this call. * * @param conc The conclusion of the lemma * @param exp The set of (all) literals that imply conc @@ -210,6 +248,14 @@ class TheoryInferenceManager ProofGenerator* pg = nullptr, LemmaProperty p = LemmaProperty::NONE, bool doCache = true); + /** + * Make the trust node for the above method. It is responsibility of the + * caller to subsequently call trustedLemma with the returned trust node. + */ + TrustNode mkLemmaExp(Node conc, + const std::vector& exp, + const std::vector& noExplain, + ProofGenerator* pg = nullptr); /** * Has this inference manager cached and sent the given lemma (in this user * context)? This method can be overridden by the particular manager. If not, diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp index 021a737c0..66c36ed95 100644 --- a/src/theory/uf/proof_equality_engine.cpp +++ b/src/theory/uf/proof_equality_engine.cpp @@ -260,9 +260,8 @@ TrustNode ProofEqEngine::assertConflict(PfRule id, { Trace("pfee") << "pfee::assertConflict " << id << ", exp = " << exp << ", args = " << args << std::endl; - // conflict is same as proof of false - std::vector empVec; - return assertLemma(d_false, id, exp, empVec, args); + // conflict is same as lemma concluding false + return assertLemma(d_false, id, exp, {}, args); } TrustNode ProofEqEngine::assertConflict(const std::vector& exp, @@ -270,15 +269,15 @@ TrustNode ProofEqEngine::assertConflict(const std::vector& exp, { Trace("pfee") << "pfee::assertConflict " << exp << " via buffer with " << psb.getNumSteps() << " steps" << std::endl; - if (d_pfEnabled) - { - if (!d_proof.addSteps(psb)) - { - return TrustNode::null(); - } - } - std::vector empVec; - return assertLemmaInternal(d_false, exp, empVec, &d_proof); + return assertLemma(d_false, exp, {}, psb); +} + +TrustNode ProofEqEngine::assertConflict(const std::vector& exp, + ProofGenerator* pg) +{ + Trace("pfee") << "pfee::assertConflict " << exp << " via generator" + << std::endl; + return assertLemma(d_false, exp, {}, pg); } TrustNode ProofEqEngine::assertLemma(Node conc, diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h index 314353131..e1105623a 100644 --- a/src/theory/uf/proof_equality_engine.h +++ b/src/theory/uf/proof_equality_engine.h @@ -180,6 +180,8 @@ class ProofEqEngine : public EagerProofGenerator const std::vector& args); /** Multi-step version */ TrustNode assertConflict(const std::vector& exp, ProofStepBuffer& psb); + /** Generator version, where pg has a proof of false from assumptions exp */ + TrustNode assertConflict(const std::vector& exp, ProofGenerator* pg); //-------------------------- assert lemma /** * Called when we have concluded conc, typically via theory specific -- cgit v1.2.3