diff options
-rw-r--r-- | src/preprocessing/assertion_pipeline.cpp | 92 | ||||
-rw-r--r-- | src/preprocessing/assertion_pipeline.h | 41 | ||||
-rw-r--r-- | src/smt/preprocess_proof_generator.cpp | 117 | ||||
-rw-r--r-- | src/smt/preprocess_proof_generator.h | 24 | ||||
-rw-r--r-- | src/smt/proof_manager.cpp | 4 | ||||
-rw-r--r-- | src/smt/proof_manager.h | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 2 | ||||
-rw-r--r-- | src/theory/trust_node.cpp | 2 | ||||
-rw-r--r-- | src/theory/trust_node.h | 2 |
9 files changed, 205 insertions, 81 deletions
diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp index 99e22b28f..cd92e5f3d 100644 --- a/src/preprocessing/assertion_pipeline.cpp +++ b/src/preprocessing/assertion_pipeline.cpp @@ -18,6 +18,7 @@ #include "expr/node_manager.h" #include "options/smt_options.h" #include "proof/proof_manager.h" +#include "theory/builtin/proof_checker.h" #include "theory/rewriter.h" namespace CVC4 { @@ -61,10 +62,17 @@ void AssertionPipeline::push_back(Node n, Assert(d_assumptionsStart + d_numAssumptions == d_nodes.size() - 1); d_numAssumptions++; } - if (!isInput && isProofEnabled()) + if (isProofEnabled()) { - // notice this is always called, regardless of whether pgen is nullptr - d_pppg->notifyNewAssert(n, pgen); + if (!isInput) + { + // notice this is always called, regardless of whether pgen is nullptr + d_pppg->notifyNewAssert(n, pgen); + } + else + { + Trace("smt-pppg") << "...input assertion " << n << std::endl; + } } } @@ -77,6 +85,13 @@ void AssertionPipeline::pushBackTrusted(theory::TrustNode trn) void AssertionPipeline::replace(size_t i, Node n, ProofGenerator* pgen) { + if (n == d_nodes[i]) + { + // no change, skip + return; + } + Trace("smt-pppg-repl") << "Replace " << d_nodes[i] << " with " << n + << std::endl; if (options::unsatCores()) { ProofManager::currentPM()->addDependence(n, d_nodes[i]); @@ -94,26 +109,6 @@ void AssertionPipeline::replaceTrusted(size_t i, theory::TrustNode trn) replace(i, trn.getNode(), trn.getGenerator()); } -void AssertionPipeline::replace(size_t i, - Node n, - const std::vector<Node>& addnDeps, - ProofGenerator* pgen) -{ - if (options::unsatCores()) - { - ProofManager::currentPM()->addDependence(n, d_nodes[i]); - for (const auto& addnDep : addnDeps) - { - ProofManager::currentPM()->addDependence(n, addnDep); - } - } - if (isProofEnabled()) - { - d_pppg->notifyPreprocessed(d_nodes[i], n, pgen); - } - d_nodes[i] = n; -} - void AssertionPipeline::setProofGenerator(smt::PreprocessProofGenerator* pppg) { d_pppg = pppg; @@ -133,14 +128,55 @@ void AssertionPipeline::disableStoreSubstsInAsserts() d_storeSubstsInAsserts = false; } -void AssertionPipeline::addSubstitutionNode(Node n) +void AssertionPipeline::addSubstitutionNode(Node n, ProofGenerator* pg) { Assert(d_storeSubstsInAsserts); Assert(n.getKind() == kind::EQUAL); - d_nodes[d_substsIndex] = theory::Rewriter::rewrite( - NodeManager::currentNM()->mkNode(kind::AND, n, d_nodes[d_substsIndex])); - Assert(theory::Rewriter::rewrite(d_nodes[d_substsIndex]) - == d_nodes[d_substsIndex]); + conjoin(d_substsIndex, n, pg); +} + +void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg) +{ + NodeManager* nm = NodeManager::currentNM(); + Node newConj = nm->mkNode(kind::AND, d_nodes[i], n); + Node newConjr = theory::Rewriter::rewrite(newConj); + if (newConjr == d_nodes[i]) + { + // trivial, skip + return; + } + if (isProofEnabled()) + { + // ---------- from pppg --------- from pg + // d_nodes[i] n + // -------------------------------- AND_INTRO + // d_nodes[i] ^ n + // -------------------------------- MACRO_SR_PRED_TRANSFORM + // rewrite( d_nodes[i] ^ n ) + // allocate a fresh proof which will act as the proof generator + LazyCDProof* lcp = d_pppg->allocateHelperProof(); + lcp->addLazyStep(d_nodes[i], d_pppg, false); + lcp->addLazyStep( + n, pg, false, "AssertionPipeline::conjoin", false, PfRule::PREPROCESS); + lcp->addStep(newConj, PfRule::AND_INTRO, {d_nodes[i], n}, {}); + if (newConjr != newConj) + { + lcp->addStep( + newConjr, PfRule::MACRO_SR_PRED_TRANSFORM, {newConj}, {newConjr}); + } + // Notice we have constructed a proof of a new assertion, where d_pppg + // is referenced in the lazy proof above. If alternatively we had + // constructed a proof of d_nodes[i] = rewrite( d_nodes[i] ^ n ), we would + // have used notifyPreprocessed. However, it is simpler to make the + // above proof. + d_pppg->notifyNewAssert(newConjr, lcp); + } + if (options::unsatCores()) + { + ProofManager::currentPM()->addDependence(newConjr, d_nodes[i]); + } + d_nodes[i] = newConjr; + Assert(theory::Rewriter::rewrite(newConjr) == newConjr); } } // namespace preprocessing diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h index 63e2bdd2a..6ca430ac4 100644 --- a/src/preprocessing/assertion_pipeline.h +++ b/src/preprocessing/assertion_pipeline.h @@ -49,7 +49,9 @@ class AssertionPipeline */ void clear(); + /** TODO (projects #75): remove this */ Node& operator[](size_t i) { return d_nodes[i]; } + /** Get the assertion at index i */ const Node& operator[](size_t i) const { return d_nodes[i]; } /** @@ -70,7 +72,13 @@ class AssertionPipeline /** Same as above, with TrustNode */ void pushBackTrusted(theory::TrustNode trn); + /** TODO (projects #75): remove this */ std::vector<Node>& ref() { return d_nodes; } + + /** + * Get the constant reference to the underlying assertions. It is only + * possible to modify these via the replace methods below. + */ const std::vector<Node>& ref() const { return d_nodes; } std::vector<Node>::const_iterator begin() const { return d_nodes.cbegin(); } @@ -89,22 +97,6 @@ class AssertionPipeline /** Same as above, with TrustNode */ void replaceTrusted(size_t i, theory::TrustNode trn); - /* - * Replaces assertion i with node n and records that this replacement depends - * on assertion i and the nodes listed in addnDeps. The dependency - * information is used for unsat cores and proofs. - * - * @param i The position of the assertion to replace. - * @param n The replacement assertion. - * @param addnDeps The dependencies. - * @param pg The proof generator who can provide a proof of d_nodes[i] == n, - * where d_nodes[i] is the assertion at position i prior to this call. - */ - void replace(size_t i, - Node n, - const std::vector<Node>& addnDeps, - ProofGenerator* pg = nullptr); - IteSkolemMap& getIteSkolemMap() { return d_iteSkolemMap; } const IteSkolemMap& getIteSkolemMap() const { return d_iteSkolemMap; } @@ -136,8 +128,23 @@ class AssertionPipeline /** * Adds a substitution node of the form (= lhs rhs) to the assertions. + * This conjoins n to assertions at a distinguished index given by + * d_substsIndex. + * + * @param n The substitution node + * @param pg The proof generator that can provide a proof of n. + */ + void addSubstitutionNode(Node n, ProofGenerator* pgen = nullptr); + + /** + * Conjoin n to the assertion vector at position i. This replaces + * d_nodes[i] with the rewritten form of (AND d_nodes[i] n). + * + * @param i The assertion to replace + * @param n The formula to conjoin at position i + * @param pg The proof generator that can provide a proof of n */ - void addSubstitutionNode(Node n); + void conjoin(size_t i, Node n, ProofGenerator* pg = nullptr); /** * Checks whether the assertion at a given index represents substitutions. diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp index 5c7ed0356..1739a4e7d 100644 --- a/src/smt/preprocess_proof_generator.cpp +++ b/src/smt/preprocess_proof_generator.cpp @@ -21,15 +21,24 @@ namespace CVC4 { namespace smt { -PreprocessProofGenerator::PreprocessProofGenerator(ProofNodeManager* pnm) - : d_pnm(pnm) +PreprocessProofGenerator::PreprocessProofGenerator(context::UserContext* u, + ProofNodeManager* pnm) + : d_pnm(pnm), d_src(u), d_helperProofs(u) { } void PreprocessProofGenerator::notifyNewAssert(Node n, ProofGenerator* pg) { - Trace("smt-proof-pp-debug") << "- notifyNewAssert: " << n << std::endl; - d_src[n] = theory::TrustNode::mkTrustLemma(n, pg); + Trace("smt-proof-pp-debug") + << "PreprocessProofGenerator::notifyNewAssert: " << n << std::endl; + if (d_src.find(n) == d_src.end()) + { + d_src[n] = theory::TrustNode::mkTrustLemma(n, pg); + } + else + { + Trace("smt-proof-pp-debug") << "...already proven" << std::endl; + } } void PreprocessProofGenerator::notifyPreprocessed(Node n, @@ -40,14 +49,22 @@ void PreprocessProofGenerator::notifyPreprocessed(Node n, if (n != np) { Trace("smt-proof-pp-debug") - << "- notifyPreprocessed: " << n << "..." << np << std::endl; - d_src[np] = theory::TrustNode::mkTrustRewrite(n, np, pg); + << "PreprocessProofGenerator::notifyPreprocessed: " << n << "..." << np + << std::endl; + if (d_src.find(np) == d_src.end()) + { + d_src[np] = theory::TrustNode::mkTrustRewrite(n, np, pg); + } + else + { + Trace("smt-proof-pp-debug") << "...already proven" << std::endl; + } } } std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f) { - std::map<Node, theory::TrustNode>::iterator it = d_src.find(f); + NodeTrustNodeMap::iterator it = d_src.find(f); if (it == d_src.end()) { // could be an assumption, return nullptr @@ -56,67 +73,102 @@ std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f) // make CDProof to construct the proof below CDProof cdp(d_pnm); + Trace("smt-pppg") << "PreprocessProofGenerator::getProofFor: input " << f + << std::endl; Node curr = f; std::vector<Node> transChildren; + std::unordered_set<Node, NodeHashFunction> processed; bool success; + // we connect the proof of f to its source via the map d_src until we + // discover that its source is a preprocessing lemma (a lemma stored in d_src) + // or otherwise it is assumed to be an input assumption. do { success = false; if (it != d_src.end()) { - Assert(it->second.getNode() == curr); + Assert((*it).second.getNode() == curr); + // get the proven node + Node proven = (*it).second.getProven(); + Assert(!proven.isNull()); + Trace("smt-pppg") << "...process proven " << proven << std::endl; + if (processed.find(proven) != processed.end()) + { + Unhandled() << "Cyclic steps in preprocess proof generator"; + continue; + } + processed.insert(proven); bool proofStepProcessed = false; - std::shared_ptr<ProofNode> pfr = it->second.toProofNode(); + + // if a generator for the step was provided, it is stored in the proof + Trace("smt-pppg") << "...get provided proof" << std::endl; + std::shared_ptr<ProofNode> pfr = (*it).second.toProofNode(); if (pfr != nullptr) { - Assert(pfr->getResult() == it->second.getProven()); + Trace("smt-pppg") << "...add provided" << std::endl; + Assert(pfr->getResult() == proven); cdp.addProof(pfr); proofStepProcessed = true; } - if (it->second.getKind() == theory::TrustNodeKind::REWRITE) + Trace("smt-pppg") << "...update" << std::endl; + theory::TrustNodeKind tnk = (*it).second.getKind(); + if (tnk == theory::TrustNodeKind::REWRITE) { - Node eq = it->second.getProven(); - Assert(eq.getKind() == kind::EQUAL); + Trace("smt-pppg") << "...rewritten from " << proven[0] << std::endl; + Assert(proven.getKind() == kind::EQUAL); if (!proofStepProcessed) { // maybe its just a simple rewrite? - if (eq[1] == theory::Rewriter::rewrite(eq[0])) + if (proven[1] == theory::Rewriter::rewrite(proven[0])) { - cdp.addStep(eq, PfRule::REWRITE, {}, {eq[0]}); + cdp.addStep(proven, PfRule::REWRITE, {}, {proven[0]}); proofStepProcessed = true; } } - transChildren.push_back(eq); + transChildren.push_back(proven); // continue with source - curr = eq[0]; + curr = proven[0]; success = true; // find the next node it = d_src.find(curr); } else { - Assert(it->second.getKind() == theory::TrustNodeKind::LEMMA); + Trace("smt-pppg") << "...lemma" << std::endl; + Assert(tnk == theory::TrustNodeKind::LEMMA); } if (!proofStepProcessed) { - // add trusted step - Node proven = it->second.getProven(); - cdp.addStep(proven, PfRule::PREPROCESS, {}, {proven}); + Trace("smt-pppg") << "...add missing step" << std::endl; + // add trusted step, the rule depends on the kind of trust node + cdp.addStep(proven, + tnk == theory::TrustNodeKind::LEMMA + ? PfRule::PREPROCESS_LEMMA + : PfRule::PREPROCESS, + {}, + {proven}); } } } while (success); - Assert(curr != f); - // prove ( curr == f ) - Node fullRewrite = curr.eqNode(f); - if (transChildren.size() >= 2) + // prove ( curr == f ), which is not necessary if they are the same + // modulo symmetry. + if (!CDProof::isSame(f, curr)) { - cdp.addStep(fullRewrite, PfRule::TRANS, transChildren, {}); + Node fullRewrite = curr.eqNode(f); + if (transChildren.size() >= 2) + { + Trace("smt-pppg") << "...apply trans to get " << fullRewrite << std::endl; + std::reverse(transChildren.begin(), transChildren.end()); + cdp.addStep(fullRewrite, PfRule::TRANS, transChildren, {}); + } + Trace("smt-pppg") << "...eq_resolve to prove" << std::endl; + // prove f + cdp.addStep(f, PfRule::EQ_RESOLVE, {curr, fullRewrite}, {}); + Trace("smt-pppg") << "...finished" << std::endl; } - // prove f - cdp.addStep(f, PfRule::EQ_RESOLVE, {curr, fullRewrite}, {}); // overall, proof is: // --------- from proof generator ---------- from proof generator @@ -130,6 +182,15 @@ std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f) return cdp.getProofFor(f); } +ProofNodeManager* PreprocessProofGenerator::getManager() { return d_pnm; } + +LazyCDProof* PreprocessProofGenerator::allocateHelperProof() +{ + std::shared_ptr<LazyCDProof> helperPf = std::make_shared<LazyCDProof>(d_pnm); + d_helperProofs.push_back(helperPf); + return helperPf.get(); +} + std::string PreprocessProofGenerator::identify() const { return "PreprocessProofGenerator"; diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h index 5319071f0..b71187188 100644 --- a/src/smt/preprocess_proof_generator.h +++ b/src/smt/preprocess_proof_generator.h @@ -19,8 +19,12 @@ #include <map> +#include "context/cdhashmap.h" +#include "context/cdlist.h" +#include "expr/lazy_proof.h" #include "expr/proof_generator.h" #include "expr/proof_node_manager.h" +#include "theory/eager_proof_generator.h" #include "theory/trust_node.h" namespace CVC4 { @@ -41,8 +45,11 @@ namespace smt { */ class PreprocessProofGenerator : public ProofGenerator { + typedef context::CDHashMap<Node, theory::TrustNode, NodeHashFunction> + NodeTrustNodeMap; + public: - PreprocessProofGenerator(ProofNodeManager* pnm); + PreprocessProofGenerator(context::UserContext* u, ProofNodeManager* pnm); ~PreprocessProofGenerator() {} /** * Notify that n is a new assertion, where pg can provide a proof of n. @@ -61,6 +68,17 @@ class PreprocessProofGenerator : public ProofGenerator std::shared_ptr<ProofNode> getProofFor(Node f) override; /** Identify */ std::string identify() const override; + /** Get the proof manager */ + ProofNodeManager* getManager(); + /** + * Allocate a helper proof. This returns a fresh lazy proof object that + * remains alive in this user context. This feature is used to construct + * helper proofs for preprocessing, e.g. to support the skeleton of proofs + * that connect AssertionPipeline::conjoin steps. + * + * Internally, this adds a LazyCDProof to the list d_helperProofs below. + */ + LazyCDProof* allocateHelperProof(); private: /** The proof node manager */ @@ -72,7 +90,9 @@ class PreprocessProofGenerator : public ProofGenerator * (1) A trust node REWRITE proving (n_src = n) for some n_src, or * (2) A trust node LEMMA proving n. */ - std::map<Node, theory::TrustNode> d_src; + NodeTrustNodeMap d_src; + /** A context-dependent list of LazyCDProof, allocated for conjoin steps */ + context::CDList<std::shared_ptr<LazyCDProof> > d_helperProofs; }; } // namespace smt diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index f51a116b7..df7b6bf4d 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -22,10 +22,10 @@ namespace CVC4 { namespace smt { -PfManager::PfManager(SmtEngine* smte) +PfManager::PfManager(context::UserContext* u, SmtEngine* smte) : d_pchecker(new ProofChecker(options::proofNewPedantic())), d_pnm(new ProofNodeManager(d_pchecker.get())), - d_pppg(new PreprocessProofGenerator(d_pnm.get())), + d_pppg(new PreprocessProofGenerator(u, d_pnm.get())), d_pfpp(new ProofPostproccess(d_pnm.get(), smte, d_pppg.get())), d_finalProof(nullptr) { diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h index bda741a05..118b82bec 100644 --- a/src/smt/proof_manager.h +++ b/src/smt/proof_manager.h @@ -41,7 +41,7 @@ class Assertions; class PfManager { public: - PfManager(SmtEngine* smte); + PfManager(context::UserContext* u, SmtEngine* smte); ~PfManager(); /** * Print the proof on the output channel of the current options in scope. diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3caf03946..755822d2a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -270,7 +270,7 @@ void SmtEngine::finishInit() ProofNodeManager* pnm = nullptr; if (options::proofNew()) { - d_pfManager.reset(new PfManager(this)); + d_pfManager.reset(new PfManager(getUserContext(), this)); // use this proof node manager pnm = d_pfManager->getProofNodeManager(); // enable proof support in the rewriter diff --git a/src/theory/trust_node.cpp b/src/theory/trust_node.cpp index fe66fc3cb..b0c8f3b79 100644 --- a/src/theory/trust_node.cpp +++ b/src/theory/trust_node.cpp @@ -101,7 +101,7 @@ ProofGenerator* TrustNode::getGenerator() const { return d_gen; } bool TrustNode::isNull() const { return d_proven.isNull(); } -std::shared_ptr<ProofNode> TrustNode::toProofNode() +std::shared_ptr<ProofNode> TrustNode::toProofNode() const { if (d_gen == nullptr) { diff --git a/src/theory/trust_node.h b/src/theory/trust_node.h index 0e0bfddf5..a0586bd0c 100644 --- a/src/theory/trust_node.h +++ b/src/theory/trust_node.h @@ -132,7 +132,7 @@ class TrustNode * Gets the proof node for this trust node, which is obtained by * calling the generator's getProofFor method on the proven node. */ - std::shared_ptr<ProofNode> toProofNode(); + std::shared_ptr<ProofNode> toProofNode() const; /** Get the proven formula corresponding to a conflict call */ static Node getConflictProven(Node conf); |