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.
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
#include "expr/lazy_proof.h"
-
namespace CVC4 {
ProofNodeUpdaterCallback::ProofNodeUpdaterCallback() {}
do
{
cur = visit.back();
+ visit.pop_back();
it = visited.find(cur);
if (it == visited.end())
{
// then, update the original proof node based on this one
d_pnm->updateNode(cur, npn.get());
}
- const std::vector<std::shared_ptr<ProofNode>>& ccp = cur->getChildren();
- // now, process children
- for (const std::shared_ptr<ProofNode>& cp : ccp)
- {
- visit.push_back(cp.get());
- }
+ }
+ const std::vector<std::shared_ptr<ProofNode>>& ccp = cur->getChildren();
+ // now, process children
+ for (const std::shared_ptr<ProofNode>& cp : ccp)
+ {
+ visit.push_back(cp.get());
}
}
} while (!visit.empty());
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";
// 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
// ---------------------
// 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)
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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
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);
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)
{
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(
}
return args[0];
}
+ else if (id == PfRule::PREPROCESS)
+ {
+ Assert(children.empty());
+ Assert(args.size() == 1);
+ return args[0];
+ }
// no rule
return Node::null();
}
}
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<ProofNode> 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; }
std::ostream& operator<<(std::ostream& out, TrustNode n)
{
- out << "(trust " << n.getNode() << ")";
+ out << "(" << n.getKind() << " " << n.getProven() << ")";
return out;
}
#define CVC4__THEORY__TRUST_NODE_H
#include "expr/node.h"
+#include "expr/proof_node.h"
namespace CVC4 {
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<ProofNode> toProofNode();
/** Get the proven formula corresponding to a conflict call */
static Node getConflictProven(Node conf);
projects / cvc5.git / commitdiff