From 1cb249c9dd06a049953f001cd6d82c0e6f1246f2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 13 Jul 2020 17:42:57 -0500 Subject: [PATCH] (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. --- src/CMakeLists.txt | 2 + src/expr/proof_node_updater.cpp | 14 +-- src/expr/proof_rule.cpp | 2 + src/expr/proof_rule.h | 17 +++ src/smt/preprocess_proof_generator.cpp | 139 +++++++++++++++++++++++++ src/smt/preprocess_proof_generator.h | 81 ++++++++++++++ src/theory/booleans/proof_checker.cpp | 11 ++ src/theory/builtin/proof_checker.cpp | 7 ++ src/theory/trust_node.cpp | 12 ++- src/theory/trust_node.h | 6 ++ 10 files changed, 283 insertions(+), 8 deletions(-) create mode 100644 src/smt/preprocess_proof_generator.cpp create mode 100644 src/smt/preprocess_proof_generator.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 9ef154246..930bf2370 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -239,6 +239,8 @@ libcvc4_add_sources( smt/model_core_builder.h smt/model_blocker.cpp smt/model_blocker.h + smt/preprocess_proof_generator.cpp + smt/preprocess_proof_generator.h smt/process_assertions.cpp smt/process_assertions.h smt/set_defaults.cpp diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp index 227be2122..1e8fe4e7d 100644 --- a/src/expr/proof_node_updater.cpp +++ b/src/expr/proof_node_updater.cpp @@ -16,7 +16,6 @@ #include "expr/lazy_proof.h" - namespace CVC4 { ProofNodeUpdaterCallback::ProofNodeUpdaterCallback() {} @@ -39,6 +38,7 @@ void ProofNodeUpdater::process(std::shared_ptr pf) do { cur = visit.back(); + visit.pop_back(); it = visited.find(cur); if (it == visited.end()) { @@ -67,12 +67,12 @@ void ProofNodeUpdater::process(std::shared_ptr pf) // then, update the original proof node based on this one d_pnm->updateNode(cur, npn.get()); } - const std::vector>& ccp = cur->getChildren(); - // now, process children - for (const std::shared_ptr& cp : ccp) - { - visit.push_back(cp.get()); - } + } + const std::vector>& ccp = cur->getChildren(); + // now, process children + for (const std::shared_ptr& cp : ccp) + { + visit.push_back(cp.get()); } } } while (!visit.empty()); diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index d00f1658b..08998e66e 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -31,8 +31,10 @@ const char* toString(PfRule id) case PfRule::MACRO_SR_PRED_INTRO: return "MACRO_SR_PRED_INTRO"; case PfRule::MACRO_SR_PRED_ELIM: return "MACRO_SR_PRED_ELIM"; case PfRule::MACRO_SR_PRED_TRANSFORM: return "MACRO_SR_PRED_TRANSFORM"; + case PfRule::PREPROCESS: return "PREPROCESS"; //================================================= Boolean rules case PfRule::SPLIT: return "SPLIT"; + case PfRule::EQ_RESOLVE: return "EQ_RESOLVE"; case PfRule::AND_ELIM: return "AND_ELIM"; case PfRule::AND_INTRO: return "AND_INTRO"; case PfRule::NOT_OR_ELIM: return "NOT_OR_ELIM"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index a15d8a2d2..87e8565ca 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -164,6 +164,16 @@ enum class PfRule : uint32_t // MACRO_SR_PRED_INTRO. MACRO_SR_PRED_TRANSFORM, + //================================================= Processing rules + // ======== Preprocess + // Children: none + // Arguments: (F) + // --------------------------------------------------------------- + // Conclusion: F + // where F is an equality of the form t = t' where t was replaced by t' + // based on some preprocessing pass, or otherwise F was added as a new + // assertion by some preprocessing pass. + PREPROCESS, //================================================= Boolean rules // ======== Split // Children: none @@ -171,6 +181,13 @@ enum class PfRule : uint32_t // --------------------- // Conclusion: (or F (not F)) SPLIT, + // ======== Equality resolution + // Children: (P1:F1, P2:(= F1 F2)) + // Arguments: none + // --------------------- + // Conclusion: (F2) + // Note this can optionally be seen as a macro for EQUIV_ELIM1+RESOLUTION. + EQ_RESOLVE, // ======== And elimination // Children: (P:(and F1 ... Fn)) // Arguments: (i) 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 PreprocessProofGenerator::getProofFor(Node f) +{ + std::map::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 transChildren; + bool success; + do + { + success = false; + if (it != d_src.end()) + { + Assert(it->second.getNode() == curr); + bool proofStepProcessed = false; + std::shared_ptr 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 + +#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 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 d_src; +}; + +} // namespace smt +} // namespace CVC4 + +#endif diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp index 6e7cabccd..6a8244ce0 100644 --- a/src/theory/booleans/proof_checker.cpp +++ b/src/theory/booleans/proof_checker.cpp @@ -21,6 +21,7 @@ namespace booleans { void BoolProofRuleChecker::registerTo(ProofChecker* pc) { pc->registerChecker(PfRule::SPLIT, this); + pc->registerChecker(PfRule::EQ_RESOLVE, this); pc->registerChecker(PfRule::AND_ELIM, this); pc->registerChecker(PfRule::AND_INTRO, this); pc->registerChecker(PfRule::NOT_OR_ELIM, this); @@ -74,6 +75,16 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, return NodeManager::currentNM()->mkNode( kind::OR, args[0], args[0].notNode()); } + if (id == PfRule::EQ_RESOLVE) + { + Assert(children.size() == 2); + Assert(args.empty()); + if (children[1].getKind() != kind::EQUAL || children[0] != children[1][0]) + { + return Node::null(); + } + return children[1][1]; + } // natural deduction rules if (id == PfRule::AND_ELIM) { diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index f6b41104a..a8249ae7c 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -59,6 +59,7 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::MACRO_SR_PRED_INTRO, this); pc->registerChecker(PfRule::MACRO_SR_PRED_ELIM, this); pc->registerChecker(PfRule::MACRO_SR_PRED_TRANSFORM, this); + pc->registerChecker(PfRule::PREPROCESS, this); } Node BuiltinProofRuleChecker::applySubstitutionRewrite( @@ -309,6 +310,12 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, } return args[0]; } + else if (id == PfRule::PREPROCESS) + { + Assert(children.empty()); + Assert(args.size() == 1); + return args[0]; + } // no rule return Node::null(); } diff --git a/src/theory/trust_node.cpp b/src/theory/trust_node.cpp index af2d60241..25aef5a72 100644 --- a/src/theory/trust_node.cpp +++ b/src/theory/trust_node.cpp @@ -96,10 +96,20 @@ Node TrustNode::getNode() const } Node TrustNode::getProven() const { return d_proven; } + ProofGenerator* TrustNode::getGenerator() const { return d_gen; } bool TrustNode::isNull() const { return d_proven.isNull(); } +std::shared_ptr TrustNode::toProofNode() +{ + if (d_gen == nullptr) + { + return nullptr; + } + return d_gen->getProofFor(d_proven); +} + Node TrustNode::getConflictProven(Node conf) { return conf.notNode(); } Node TrustNode::getLemmaProven(Node lem) { return lem; } @@ -113,7 +123,7 @@ Node TrustNode::getRewriteProven(TNode n, Node nr) { return n.eqNode(nr); } std::ostream& operator<<(std::ostream& out, TrustNode n) { - out << "(trust " << n.getNode() << ")"; + out << "(" << n.getKind() << " " << n.getProven() << ")"; return out; } diff --git a/src/theory/trust_node.h b/src/theory/trust_node.h index a3c0fbec5..ff174b63e 100644 --- a/src/theory/trust_node.h +++ b/src/theory/trust_node.h @@ -18,6 +18,7 @@ #define CVC4__THEORY__TRUST_NODE_H #include "expr/node.h" +#include "expr/proof_node.h" namespace CVC4 { @@ -127,6 +128,11 @@ class TrustNode ProofGenerator* getGenerator() const; /** is null? */ bool isNull() const; + /** + * 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 toProofNode(); /** Get the proven formula corresponding to a conflict call */ static Node getConflictProven(Node conf); -- 2.30.2