From fc784f0273099b84581862b8587940c6db3459ed Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 31 Aug 2020 06:46:42 -0500 Subject: [PATCH] Basic proof support in inference manager (#4975) This adds basic support for asserting internal facts with proofs in the inference manager class. The purpose of this PR is twofold: (1) From the point of view of proofs, this PR standardizes the management of proof equality engine within inference manager. Theories no longer have to manually construct proof equality engines, and instead are recommended to create inference managers. (2) From the point of view of the new approach to theory combination, this PR ensures standard theory callbacks (preNotifyFact / notifyFact) are used for internal facts, regardless of whether proofs are enabled. This will simplify several of the current (unmerged) changes for proof production in theory solvers on proof-new. Notice this PR adds the utility method NodeManager::mkAnd, which is arguably long overdue. Also notice this code is not yet active, but will be used on proof-new after this PR is merged. --- src/expr/node_manager.h | 25 +++++ src/theory/theory_inference_manager.cpp | 120 +++++++++++++++++++++--- src/theory/theory_inference_manager.h | 68 +++++++++++++- src/theory/uf/proof_equality_engine.cpp | 32 +------ src/theory/uf/proof_equality_engine.h | 6 -- 5 files changed, 200 insertions(+), 51 deletions(-) diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 592b5e7e9..abbe998b5 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -473,6 +473,17 @@ class NodeManager { template Node* mkNodePtr(Kind kind, const std::vector >& children); + /** + * Create an AND node with arbitrary number of children. This returns the + * true node if children is empty, or the single node in children if + * it contains only one node. + * + * We define construction of AND as a special case here since it is widely + * used for e.g. constructing explanations. + */ + template + Node mkAnd(const std::vector >& children); + /** Create a node (with no children) by operator. */ Node mkNode(TNode opNode); Node* mkNodePtr(TNode opNode); @@ -1359,6 +1370,20 @@ inline Node NodeManager::mkNode(Kind kind, return nb.constructNode(); } +template +Node NodeManager::mkAnd(const std::vector >& children) +{ + if (children.empty()) + { + return mkConst(true); + } + else if (children.size() == 1) + { + return children[0]; + } + return mkNode(kind::AND, children); +} + template inline Node* NodeManager::mkNodePtr(Kind kind, const std::vector >& diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index b2da91e16..a42c33814 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -37,6 +37,14 @@ TheoryInferenceManager::TheoryInferenceManager(Theory& t, void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee) { d_ee = ee; + // if proofs are enabled, also make a proof equality engine to wrap ee + if (d_pnm != nullptr) + { + d_pfee.reset(new eq::ProofEqEngine(d_theoryState.getSatContext(), + d_theoryState.getUserContext(), + *d_ee, + d_pnm)); + } } void TheoryInferenceManager::conflictEqConstantMerge(TNode a, TNode b) @@ -85,7 +93,10 @@ bool TheoryInferenceManager::propagateLit(TNode lit) TrustNode TheoryInferenceManager::explainLit(TNode lit) { - // TODO (project #37): use proof equality engine if it exists + if (d_pfee != nullptr) + { + return d_pfee->explain(lit); + } if (d_ee != nullptr) { Node exp = d_ee->mkExplainLit(lit); @@ -100,10 +111,13 @@ TrustNode TheoryInferenceManager::explainLit(TNode lit) TrustNode TheoryInferenceManager::explainConflictEqConstantMerge(TNode a, TNode b) { - // TODO (project #37): use proof equality engine if it exists + Node lit = a.eqNode(b); + if (d_pfee != nullptr) + { + return d_pfee->explain(lit); + } if (d_ee != nullptr) { - Node lit = a.eqNode(b); Node conf = d_ee->mkExplainLit(lit); return TrustNode::mkTrustConflict(conf, nullptr); } @@ -122,36 +136,112 @@ LemmaStatus TheoryInferenceManager::trustedLemma(const TrustNode& tlem, return d_out.trustedLemma(tlem, p); } +void TheoryInferenceManager::assertInternalFact(TNode atom, bool pol, TNode exp) +{ + processInternalFact(atom, pol, PfRule::UNKNOWN, {exp}, {}, nullptr); +} + +void TheoryInferenceManager::assertInternalFact(TNode atom, + bool pol, + PfRule id, + const std::vector& exp, + const std::vector& args) +{ + Assert(id != PfRule::UNKNOWN); + processInternalFact(atom, pol, id, exp, args, nullptr); +} + void TheoryInferenceManager::assertInternalFact(TNode atom, bool pol, - TNode fact) + const std::vector& exp, + ProofGenerator* pg) { + Assert(pg != nullptr); + processInternalFact(atom, pol, PfRule::ASSUME, exp, {}, pg); +} + +void TheoryInferenceManager::processInternalFact(TNode atom, + bool pol, + PfRule id, + const std::vector& exp, + const std::vector& args, + ProofGenerator* pg) +{ + // make the node corresponding to the explanation + Node expn = NodeManager::currentNM()->mkAnd(exp); // call the pre-notify fact method with preReg = false, isInternal = true - if (d_theory.preNotifyFact(atom, pol, fact, false, true)) + if (d_theory.preNotifyFact(atom, pol, expn, false, true)) { // handled in a theory-specific way that doesn't require equality engine return; } Assert(d_ee != nullptr); Trace("infer-manager") << "TheoryInferenceManager::assertInternalFact: " - << fact << std::endl; - if (atom.getKind() == kind::EQUAL) + << expn << std::endl; + // Now, assert the fact. How to do so depends on whether proofs are enabled. + // If no proof production, or no proof rule was given + if (d_pfee == nullptr || id == PfRule::UNKNOWN) { - d_ee->assertEquality(atom, pol, fact); + if (atom.getKind() == kind::EQUAL) + { + d_ee->assertEquality(atom, pol, expn); + } + else + { + d_ee->assertPredicate(atom, pol, expn); + } + // Must reference count the equality and its explanation, which is not done + // by the equality engine. Notice that we do *not* need to do this for + // external assertions, which enter as facts in theory check. This is also + // not done if we are asserting to the proof equality engine, which does + // this caching itself within ProofEqEngine::assertFact. + d_keep.insert(atom); + d_keep.insert(expn); } else { - d_ee->assertPredicate(atom, pol, fact); + // Note that we reconstruct the original literal lit here, since both the + // original literal is needed for bookkeeping proofs. It is possible to + // optimize this so that a few less nodes are created, but at the cost + // of a more verbose interface to proof equality engine. + Node lit = pol ? Node(atom) : atom.notNode(); + if (pg != nullptr) + { + // use the proof generator interface + d_pfee->assertFact(lit, expn, pg); + } + else + { + // use the explict proof step interface + d_pfee->assertFact(lit, id, expn, args); + } } // call the notify fact method with isInternal = true - d_theory.notifyFact(atom, pol, fact, true); + d_theory.notifyFact(atom, pol, expn, true); Trace("infer-manager") << "TheoryInferenceManager::finished assertInternalFact" << std::endl; - // Must reference count the equality and its explanation, which is not done - // by the equality engine. Notice that we do *not* need to do this for - // external assertions, which enter as facts in theory check. - d_keep.insert(atom); - d_keep.insert(fact); +} + +void TheoryInferenceManager::explain(TNode n, std::vector& assumptions) +{ + if (n.getKind() == kind::AND) + { + for (const Node& nc : n) + { + d_ee->explainLit(nc, assumptions); + } + } + else + { + d_ee->explainLit(n, assumptions); + } +} + +Node TheoryInferenceManager::mkExplain(TNode n) +{ + std::vector assumptions; + explain(n, assumptions); + return NodeManager::currentNM()->mkAnd(assumptions); } } // namespace theory diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index e52afe124..af8e817b4 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -17,11 +17,14 @@ #ifndef CVC4__THEORY__THEORY_INFERENCE_MANAGER_H #define CVC4__THEORY__THEORY_INFERENCE_MANAGER_H +#include + #include "context/cdhashset.h" #include "expr/node.h" #include "theory/output_channel.h" #include "theory/theory_state.h" #include "theory/trust_node.h" +#include "theory/uf/proof_equality_engine.h" namespace CVC4 { @@ -51,6 +54,12 @@ class EqualityEngine; * (with isInternal = true) whenever we assert internal facts using * assertFactInernal below, mirroring what is done for facts from the fact * queue (where isInternal = false). + * + * (3) The proof equality engine is used whenever proofs are enabled (when + * the proof node manager provided to this class is non-null). Notice this + * class automatically will construct a proof equality engine during + * setEqualityEngine, and use it for handling variants of assertInternalFact + * below that involve proofs. */ class TheoryInferenceManager { @@ -117,10 +126,55 @@ class TheoryInferenceManager * output channel as a propagation or lemma. This method ensures that the * Theory's preNotifyFact and notifyFact method have been called with * isInternal = true. + * + * @param atom The atom of the fact to assert + * @param pol Its polarity + * @param exp Its explanation, i.e. ( exp => (~) atom ) is valid. + */ + void assertInternalFact(TNode atom, bool pol, TNode exp); + /** + * Assert internal fact, with a proof step justification. Notice that if + * proofs are not enabled in this inference manager, then this asserts + * a fact to the equality engine in the normal way. + * + * @param atom The atom of the fact to assert + * @param pol Its polarity + * @param id The proof rule identifier of the proof step + * @param exp Its explanation, interpreted as a conjunction + * @param args The arguments of the proof step */ - void assertInternalFact(TNode atom, bool pol, TNode fact); + void assertInternalFact(TNode atom, + bool pol, + PfRule id, + const std::vector& exp, + const std::vector& args); + /** + * Assert internal fact, with a proof generator justification. Same as above, + * but with a proof generator instead of an explicit step. + * + * @param atom The atom of the fact to assert + * @param pol Its polarity + * @param exp Its explanation, interpreted as a conjunction + * @param pg The proof generator for this step. It must be the case that pf + * can provide a proof concluding (~) atom from free asumptions in exp in + * the remainder of the current SAT context. + */ + void assertInternalFact(TNode atom, + bool pol, + const std::vector& exp, + ProofGenerator* pg); protected: + /** + * Process internal fact. This is a common helper method for the + * assertInternalFact variants above. + */ + void processInternalFact(TNode atom, + bool pol, + PfRule id, + const std::vector& exp, + const std::vector& args, + ProofGenerator* pg); /** * Explain conflict from constants merging in the equality engine. This * method is called by conflictEqConstantMerge. By default, it returns @@ -128,6 +182,16 @@ class TheoryInferenceManager * exists. */ virtual TrustNode explainConflictEqConstantMerge(TNode a, TNode b); + /** + * Explain formula n (which is possibly a conjunction with no nested + * conjunctions), add its explanation to assumptions. + */ + void explain(TNode n, std::vector& assumptions); + /** + * Explain formula n (which is possibly a conjunction with no nested + * conjunctions), return the explanation as a conjunction. + */ + Node mkExplain(TNode n); /** The theory object */ Theory& d_theory; /** Reference to the state of theory */ @@ -136,6 +200,8 @@ class TheoryInferenceManager OutputChannel& d_out; /** Pointer to equality engine of the theory. */ eq::EqualityEngine* d_ee; + /** A proof equality engine */ + std::unique_ptr d_pfee; /** The proof node manager of the theory */ ProofNodeManager* d_pnm; /** diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp index 274a46b26..021a737c0 100644 --- a/src/theory/uf/proof_equality_engine.cpp +++ b/src/theory/uf/proof_equality_engine.cpp @@ -126,7 +126,7 @@ bool ProofEqEngine::assertFact(Node lit, d_proof.addLazyStep(lit, &d_factPg, false); } // second, assert it to the equality engine - Node reason = mkAnd(exp); + Node reason = NodeManager::currentNM()->mkAnd(exp); return assertFactInternal(atom, polarity, reason); } @@ -494,11 +494,11 @@ TrustNode ProofEqEngine::ensureProofForFact(Node conc, // scope the proof constructed above, and connect the formula with the proof // minimize the assumptions pf = d_pnm->mkScope(pfBody, scopeAssumps, true, true); - exp = mkAnd(scopeAssumps); + exp = nm->mkAnd(scopeAssumps); } else { - exp = mkAnd(assumps); + exp = nm->mkAnd(assumps); } // Make the lemma or conflict node. This must exactly match the conclusion // of SCOPE below. @@ -668,32 +668,6 @@ void ProofEqEngine::explainWithProof(Node lit, Trace("pfee-proof") << "pfee::explainWithProof: finished" << std::endl; } -Node ProofEqEngine::mkAnd(const std::vector& a) -{ - if (a.empty()) - { - return d_true; - } - else if (a.size() == 1) - { - return a[0]; - } - return NodeManager::currentNM()->mkNode(AND, a); -} - -Node ProofEqEngine::mkAnd(const std::vector& a) -{ - if (a.empty()) - { - return d_true; - } - else if (a.size() == 1) - { - return a[0]; - } - return NodeManager::currentNM()->mkNode(AND, a); -} - ProofEqEngine::FactProofGenerator::FactProofGenerator(context::Context* c, ProofNodeManager* pnm) : ProofGenerator(), d_facts(c), d_pnm(pnm) diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h index b71f72c53..314353131 100644 --- a/src/theory/uf/proof_equality_engine.h +++ b/src/theory/uf/proof_equality_engine.h @@ -307,12 +307,6 @@ class ProofEqEngine : public EagerProofGenerator const std::vector& assumps, TrustNodeKind tnk, LazyCDProof* curr); - /** - * Make the conjunction of nodes in a. Returns true if a is empty, and a - * single literal if a has size 1. - */ - Node mkAnd(const std::vector& a); - Node mkAnd(const std::vector& a); /** Reference to the equality engine */ eq::EqualityEngine& d_ee; /** The default proof generator (for simple facts) */ -- 2.30.2