diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-13 17:42:57 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-13 17:42:57 -0500 |
commit | 1cb249c9dd06a049953f001cd6d82c0e6f1246f2 (patch) | |
tree | 000398841f1869d9911e1e496623520ffb6de21a /src/smt | |
parent | a34f29798b3f4d1f83e1ced57fe53db53b9956f0 (diff) |
(proof-new) SMT Preprocess proof generator (#4708)
This adds the proof generator for storing proofs of preprocessing. It stores assertions added via preprocessing passes and their rewrites. This utility will eventually live in SmtEngine.
It also adds 2 new proof rules, and fixes an issue in ProofNodeUpdater.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/preprocess_proof_generator.cpp | 139 | ||||
-rw-r--r-- | src/smt/preprocess_proof_generator.h | 81 |
2 files changed, 220 insertions, 0 deletions
diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp new file mode 100644 index 000000000..969ffa9bb --- /dev/null +++ b/src/smt/preprocess_proof_generator.cpp @@ -0,0 +1,139 @@ +/********************* */ +/*! \file preprocess_proof_generator.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The implementation of the module for proofs for preprocessing in an + ** SMT engine. + **/ + +#include "smt/preprocess_proof_generator.h" + +#include "expr/proof.h" +#include "theory/rewriter.h" + +namespace CVC4 { +namespace smt { + +PreprocessProofGenerator::PreprocessProofGenerator(ProofNodeManager* pnm) + : d_pnm(pnm) +{ +} + +void PreprocessProofGenerator::notifyNewAssert(Node n, ProofGenerator* pg) +{ + Trace("smt-proof-pp-debug") << "- notifyNewAssert: " << n << std::endl; + d_src[n] = theory::TrustNode::mkTrustLemma(n, pg); +} + +void PreprocessProofGenerator::notifyPreprocessed(Node n, + Node np, + ProofGenerator* pg) +{ + // only keep if indeed it rewrote + if (n != np) + { + Trace("smt-proof-pp-debug") + << "- notifyPreprocessed: " << n << "..." << np << std::endl; + d_src[np] = theory::TrustNode::mkTrustRewrite(n, np, pg); + } +} + +std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f) +{ + std::map<Node, theory::TrustNode>::iterator it = d_src.find(f); + if (it == d_src.end()) + { + // could be an assumption, return nullptr + return nullptr; + } + // make CDProof to construct the proof below + CDProof cdp(d_pnm); + + Node curr = f; + std::vector<Node> transChildren; + bool success; + do + { + success = false; + if (it != d_src.end()) + { + Assert(it->second.getNode() == curr); + bool proofStepProcessed = false; + std::shared_ptr<ProofNode> pfr = it->second.toProofNode(); + if (pfr != nullptr) + { + Assert(pfr->getResult() == it->second.getProven()); + cdp.addProof(pfr); + proofStepProcessed = true; + } + + if (it->second.getKind() == theory::TrustNodeKind::REWRITE) + { + Node eq = it->second.getProven(); + Assert(eq.getKind() == kind::EQUAL); + if (!proofStepProcessed) + { + // maybe its just a simple rewrite? + if (eq[1] == theory::Rewriter::rewrite(eq[0])) + { + cdp.addStep(eq, PfRule::REWRITE, {}, {eq[0]}); + proofStepProcessed = true; + } + } + transChildren.push_back(eq); + // continue with source + curr = eq[0]; + success = true; + // find the next node + it = d_src.find(curr); + } + else + { + Assert(it->second.getKind() == theory::TrustNodeKind::LEMMA); + } + + if (!proofStepProcessed) + { + // add trusted step + Node proven = it->second.getProven(); + cdp.addStep(proven, PfRule::PREPROCESS, {}, {proven}); + } + } + } while (success); + + Assert(curr != f); + // prove ( curr == f ) + Node fullRewrite = curr.eqNode(f); + if (transChildren.size() >= 2) + { + cdp.addStep(fullRewrite, PfRule::TRANS, transChildren, {}); + } + // prove f + cdp.addStep(f, PfRule::EQ_RESOLVE, {curr, fullRewrite}, {}); + + // overall, proof is: + // --------- from proof generator ---------- from proof generator + // F_1 = F_2 ... F_{n-1} = F_n + // ---? -------------------------------------------------- TRANS + // F_1 F_1 = F_n + // ---------------- EQ_RESOLVE + // F_n + // Note F_1 may have been given a proof if it was not an input assumption. + + return cdp.getProofFor(f); +} + +std::string PreprocessProofGenerator::identify() const +{ + return "PreprocessProofGenerator"; +} + +} // namespace smt +} // namespace CVC4 diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h new file mode 100644 index 000000000..3b960b051 --- /dev/null +++ b/src/smt/preprocess_proof_generator.h @@ -0,0 +1,81 @@ +/********************* */ +/*! \file preprocess_proof_generator.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The module for proofs for preprocessing in an SMT engine. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__SMT__PREPROCESS_PROOF_GENERATOR_H +#define CVC4__SMT__PREPROCESS_PROOF_GENERATOR_H + +#include <map> + +#include "expr/proof_generator.h" +#include "expr/proof_node_manager.h" +#include "theory/trust_node.h" + +namespace CVC4 { +namespace smt { + +/** + * A proof generator storing proofs of preprocessing. This has two main + * interfaces during solving: + * (1) notifyNewAssert, for assertions that are not part of the input and are + * added by preprocessing passes, + * (2) notifyPreprocessed, which is called when a preprocessing pass rewrites + * an assertion into another. + * Notice that input assertions do not need to be provided to this class. + * + * Its getProofFor method produces a proof for a preprocessed assertion + * whose free assumptions are intended to be input assertions, which are + * implictly all assertions that are not notified to this class. + */ +class PreprocessProofGenerator : public ProofGenerator +{ + public: + PreprocessProofGenerator(ProofNodeManager* pnm); + ~PreprocessProofGenerator() {} + /** + * Notify that n is a new assertion, where pg can provide a proof of n. + */ + void notifyNewAssert(Node n, ProofGenerator* pg); + /** + * Notify that n was replaced by np due to preprocessing, where pg can + * provide a proof of the equality n=np. + */ + void notifyPreprocessed(Node n, Node np, ProofGenerator* pg); + /** + * Get proof for f, which returns a proof based on proving an equality based + * on transitivity of preprocessing steps, and then using the original + * assertion with EQ_RESOLVE to obtain the proof of the ending assertion f. + */ + std::shared_ptr<ProofNode> getProofFor(Node f) override; + /** Identify */ + std::string identify() const override; + + private: + /** The proof node manager */ + ProofNodeManager* d_pnm; + /** + * The trust node that was the source of each node constructed during + * preprocessing. For each n, d_src[n] is a trust node whose node is n. This + * can either be: + * (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; +}; + +} // namespace smt +} // namespace CVC4 + +#endif |