diff options
-rw-r--r-- | src/expr/node_manager.h | 25 | ||||
-rw-r--r-- | src/theory/theory_inference_manager.cpp | 120 | ||||
-rw-r--r-- | src/theory/theory_inference_manager.h | 68 | ||||
-rw-r--r-- | src/theory/uf/proof_equality_engine.cpp | 32 | ||||
-rw-r--r-- | 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 <bool ref_count> Node* mkNodePtr(Kind kind, const std::vector<NodeTemplate<ref_count> >& 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 <bool ref_count> + Node mkAnd(const std::vector<NodeTemplate<ref_count> >& children); + /** Create a node (with no children) by operator. */ Node mkNode(TNode opNode); Node* mkNodePtr(TNode opNode); @@ -1360,6 +1371,20 @@ inline Node NodeManager::mkNode(Kind kind, } template <bool ref_count> +Node NodeManager::mkAnd(const std::vector<NodeTemplate<ref_count> >& children) +{ + if (children.empty()) + { + return mkConst(true); + } + else if (children.size() == 1) + { + return children[0]; + } + return mkNode(kind::AND, children); +} + +template <bool ref_count> inline Node* NodeManager::mkNodePtr(Kind kind, const std::vector<NodeTemplate<ref_count> >& children) { 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<Node>& exp, + const std::vector<Node>& args) +{ + Assert(id != PfRule::UNKNOWN); + processInternalFact(atom, pol, id, exp, args, nullptr); +} + void TheoryInferenceManager::assertInternalFact(TNode atom, bool pol, - TNode fact) + const std::vector<Node>& 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<Node>& exp, + const std::vector<Node>& 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<TNode>& 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<TNode> 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 <memory> + #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,17 +126,72 @@ 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<Node>& exp, + const std::vector<Node>& 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<Node>& 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<Node>& exp, + const std::vector<Node>& args, + ProofGenerator* pg); + /** * Explain conflict from constants merging in the equality engine. This * method is called by conflictEqConstantMerge. By default, it returns * the explanation of the official equality engine of the theory, if it * 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<TNode>& 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<eq::ProofEqEngine> 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<Node>& 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<TNode>& 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<TNode>& 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<Node>& a); - Node mkAnd(const std::vector<TNode>& a); /** Reference to the equality engine */ eq::EqualityEngine& d_ee; /** The default proof generator (for simple facts) */ |