summaryrefslogtreecommitdiff
path: root/src/proof
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof')
-rw-r--r--src/proof/alethe/alethe_post_processor.cpp339
-rw-r--r--src/proof/annotation_proof_generator.cpp87
-rw-r--r--src/proof/annotation_proof_generator.h102
-rw-r--r--src/proof/lazy_proof_chain.cpp44
-rw-r--r--src/proof/lazy_proof_chain.h18
-rw-r--r--src/proof/lfsc/lfsc_node_converter.cpp59
-rw-r--r--src/proof/lfsc/lfsc_util.cpp4
-rw-r--r--src/proof/method_id.cpp4
-rw-r--r--src/proof/proof_checker.cpp4
-rw-r--r--src/proof/proof_node_manager.cpp12
-rw-r--r--src/proof/proof_node_manager.h7
-rw-r--r--src/proof/proof_node_to_sexpr.cpp6
-rw-r--r--src/proof/proof_rule.cpp1
-rw-r--r--src/proof/proof_rule.h8
-rw-r--r--src/proof/unsat_core.cpp3
15 files changed, 606 insertions, 92 deletions
diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
index 2254c025f..af683ffc6 100644
--- a/src/proof/alethe/alethe_post_processor.cpp
+++ b/src/proof/alethe/alethe_post_processor.cpp
@@ -20,6 +20,7 @@
#include "proof/proof.h"
#include "proof/proof_checker.h"
#include "proof/proof_node_algorithm.h"
+#include "proof/proof_node_manager.h"
#include "theory/builtin/proof_checker.h"
#include "util/rational.h"
@@ -465,7 +466,7 @@ bool AletheProofPostprocessCallback::update(Node res,
res,
nm->mkNode(kind::SEXPR, d_cl, res),
children,
- {nm->mkConst(CONST_RATIONAL, Rational(1))},
+ {nm->mkConstInt(Rational(1))},
*cdp);
}
default:
@@ -1351,7 +1352,7 @@ bool AletheProofPostprocessCallback::update(Node res,
{
Node vp1 = nm->mkNode(kind::SEXPR, d_cl, children[0], res);
std::vector<Node> new_children = {vp1, children[0]};
- new_args.push_back(nm->mkConst<Rational>(CONST_RATIONAL, 1));
+ new_args.push_back(nm->mkConstInt(Rational(1)));
return addAletheStep(AletheRule::LA_GENERIC, vp1, vp1, {}, new_args, *cdp)
&& addAletheStep(AletheRule::RESOLUTION,
res,
@@ -1374,7 +1375,7 @@ bool AletheProofPostprocessCallback::update(Node res,
{
Node vp1 = nm->mkNode(kind::SEXPR, d_cl, children[0], res);
std::vector<Node> new_children = {vp1, children[0]};
- new_args.push_back(nm->mkConst<Rational>(CONST_RATIONAL, 1));
+ new_args.push_back(nm->mkConstInt(Rational(1)));
return addAletheStep(AletheRule::LA_GENERIC, vp1, vp1, {}, new_args, *cdp)
&& addAletheStep(AletheRule::RESOLUTION,
res,
@@ -1383,6 +1384,232 @@ bool AletheProofPostprocessCallback::update(Node res,
{},
*cdp);
}
+ // ======== Trichotomy of the reals
+ // See proof_rule.h for documentation on the ARITH_TRICHOTOMY rule. This
+ // comment uses variable names as introduced there.
+ //
+ // If C = (= x c) or C = (> x c) pre-processing has to transform (>= x c)
+ // into (<= c x)
+ //
+ // ------------------------------------------------------ LA_DISEQUALITY
+ // (VP1: (cl (or (= x c) (not (<= x c)) (not (<= c x)))))
+ // -------------------------------------------------------- OR
+ // (VP2: (cl (= x c) (not (<= x c)) (not (<= c x))))
+ //
+ // If C = (> x c) or C = (< x c) post-processing has to be added. In these
+ // cases resolution on VP2 A B yields (not (<=x c)) or (not (<= c x)) and
+ // comp_simplify is used to transform it into C. Otherwise,
+ //
+ // VP2 A B
+ // ---------------- RESOLUTION
+ // (cl C)*
+ //
+ // * the corresponding proof node is C
+ case PfRule::ARITH_TRICHOTOMY:
+ {
+ bool success = true;
+ Node equal, lesser, greater;
+
+ Kind k = res.getKind();
+ if (k == kind::EQUAL)
+ {
+ equal = res;
+ if (children[0].getKind() == kind::LEQ)
+ {
+ greater = children[0];
+ lesser = children[1];
+ }
+ else
+ {
+ greater = children[1];
+ lesser = children[0];
+ }
+ }
+ // Add case where res is not =
+ else if (res.getKind() == kind::GT)
+ {
+ greater = res;
+ if (children[0].getKind() == kind::NOT)
+ {
+ equal = children[0];
+ lesser = children[1];
+ }
+ else
+ {
+ equal = children[1];
+ lesser = children[0];
+ }
+ }
+ else
+ {
+ lesser = res;
+ if (children[0].getKind() == kind::NOT)
+ {
+ equal = children[0];
+ greater = children[1];
+ }
+ else
+ {
+ equal = children[1];
+ greater = children[0];
+ }
+ }
+
+ Node x, c;
+ if (equal.getKind() == kind::NOT)
+ {
+ x = equal[0][0];
+ c = equal[0][1];
+ }
+ else
+ {
+ x = equal[0];
+ c = equal[1];
+ }
+ Node vp_child1 = children[0], vp_child2 = children[1];
+
+ // Preprocessing
+ if (res == equal || res == greater)
+ { // C = (= x c) or C = (> x c)
+ // lesser = (>= x c)
+ Node vpc2 = nm->mkNode(
+ kind::SEXPR,
+ d_cl,
+ nm->mkNode(kind::GEQ, x, c).eqNode(nm->mkNode(kind::LEQ, c, x)));
+ // (cl (= (>= x c) (<= c x)))
+ Node vpc1 = nm->mkNode(kind::SEXPR,
+ {d_cl,
+ vpc2[1].notNode(),
+ nm->mkNode(kind::GEQ, x, c).notNode(),
+ nm->mkNode(kind::LEQ, c, x)});
+ // (cl (not(= (>= x c) (<= c x))) (not (>= x c)) (<= c x))
+ vp_child1 = nm->mkNode(
+ kind::SEXPR, d_cl, nm->mkNode(kind::LEQ, c, x)); // (cl (<= c x))
+
+ success &=
+ addAletheStep(AletheRule::EQUIV_POS2, vpc1, vpc1, {}, {}, *cdp)
+ && addAletheStep(
+ AletheRule::COMP_SIMPLIFY, vpc2, vpc2, {}, {}, *cdp)
+ && addAletheStep(AletheRule::RESOLUTION,
+ vp_child1,
+ vp_child1,
+ {vpc1, vpc2, lesser},
+ {},
+ *cdp);
+ // greater = (<= x c) or greater = (not (= x c)) -> no preprocessing
+ // necessary
+ vp_child2 = res == equal ? greater : equal;
+ }
+
+ // Process
+ Node vp1 = nm->mkNode(kind::SEXPR,
+ d_cl,
+ nm->mkNode(kind::OR,
+ nm->mkNode(kind::EQUAL, x, c),
+ nm->mkNode(kind::LEQ, x, c).notNode(),
+ nm->mkNode(kind::LEQ, c, x).notNode()));
+ // (cl (or (= x c) (not (<= x c)) (not (<= c x))))
+ Node vp2 = nm->mkNode(kind::SEXPR,
+ {d_cl,
+ nm->mkNode(kind::EQUAL, x, c),
+ nm->mkNode(kind::LEQ, x, c).notNode(),
+ nm->mkNode(kind::LEQ, c, x).notNode()});
+ // (cl (= x c) (not (<= x c)) (not (<= c x)))
+ success &=
+ addAletheStep(AletheRule::LA_DISEQUALITY, vp1, vp1, {}, {}, *cdp)
+ && addAletheStep(AletheRule::OR, vp2, vp2, {vp1}, {}, *cdp);
+
+ // Postprocessing
+ if (res == equal)
+ { // no postprocessing necessary
+ return success
+ && addAletheStep(AletheRule::RESOLUTION,
+ res,
+ nm->mkNode(kind::SEXPR, d_cl, res),
+ {vp2, vp_child1, vp_child2},
+ {},
+ *cdp);
+ }
+ if (res == greater)
+ { // have (not (<= x c)) but result should be (> x c)
+ Node vp3 = nm->mkNode(
+ kind::SEXPR,
+ d_cl,
+ nm->mkNode(kind::LEQ, x, c).notNode()); // (cl (not (<= x c)))
+ Node vp4 = nm->mkNode(
+ kind::SEXPR,
+ {d_cl,
+ nm->mkNode(kind::EQUAL,
+ nm->mkNode(kind::GT, x, c),
+ nm->mkNode(kind::LEQ, x, c).notNode())
+ .notNode(),
+ nm->mkNode(kind::GT, x, c),
+ nm->mkNode(kind::LEQ, x, c)
+ .notNode()
+ .notNode()}); // (cl (not(= (> x c) (not (<= x c)))) (> x c)
+ // (not (not (<= x c))))
+ Node vp5 =
+ nm->mkNode(kind::SEXPR,
+ d_cl,
+ nm->mkNode(kind::GT, x, c)
+ .eqNode(nm->mkNode(kind::LEQ, x, c).notNode()));
+ // (cl (= (> x c) (not (<= x c))))
+
+ return success
+ && addAletheStep(AletheRule::RESOLUTION,
+ vp3,
+ vp3,
+ {vp2, vp_child1, vp_child2},
+ {},
+ *cdp)
+ && addAletheStep(AletheRule::EQUIV_POS1, vp4, vp4, {}, {}, *cdp)
+ && addAletheStep(
+ AletheRule::COMP_SIMPLIFY, vp5, vp5, {}, {}, *cdp)
+ && addAletheStep(AletheRule::RESOLUTION,
+ res,
+ nm->mkNode(kind::SEXPR, d_cl, res),
+ {vp3, vp4, vp5},
+ {},
+ *cdp);
+ }
+ // have (not (<= c x)) but result should be (< x c)
+ Node vp3 = nm->mkNode(
+ kind::SEXPR,
+ d_cl,
+ nm->mkNode(kind::LEQ, c, x).notNode()); // (cl (not (<= c x)))
+ Node vp4 =
+ nm->mkNode(kind::SEXPR,
+ {d_cl,
+ nm->mkNode(kind::LT, x, c)
+ .eqNode(nm->mkNode(kind::LEQ, c, x).notNode())
+ .notNode(),
+ nm->mkNode(kind::LT, x, c),
+ nm->mkNode(kind::LEQ, c, x)
+ .notNode()
+ .notNode()}); // (cl (not(= (< x c) (not (<= c x))))
+ // (< x c) (not (not (<= c x))))
+ Node vp5 = nm->mkNode(
+ kind::SEXPR,
+ d_cl,
+ nm->mkNode(kind::LT, x, c)
+ .eqNode(nm->mkNode(kind::LEQ, c, x)
+ .notNode())); // (cl (= (< x c) (not (<= c x))))
+ return success
+ && addAletheStep(AletheRule::RESOLUTION,
+ vp3,
+ vp3,
+ {vp2, vp_child1, vp_child2},
+ {},
+ *cdp)
+ && addAletheStep(AletheRule::EQUIV_POS1, vp4, vp4, {}, {}, *cdp)
+ && addAletheStep(AletheRule::COMP_SIMPLIFY, vp5, vp5, {}, {}, *cdp)
+ && addAletheStep(AletheRule::RESOLUTION,
+ res,
+ nm->mkNode(kind::SEXPR, d_cl, res),
+ {vp3, vp4, vp5},
+ {},
+ *cdp);
+ }
default:
{
return addAletheStep(AletheRule::UNDEFINED,
@@ -1445,17 +1672,28 @@ bool AletheProofPostprocessCallback::finalize(Node res,
{
std::shared_ptr<ProofNode> childPf = cdp->getProofFor(children[0]);
Node childConclusion = childPf->getArguments()[2];
+ AletheRule childRule = getAletheRule(childPf->getArguments()[0]);
// if child conclusion is of the form (sexpr cl (or ...)), then we need
// to add an OR step, since this child must not be a singleton
- if (childConclusion.getNumChildren() == 2 && childConclusion[0] == d_cl
- && childConclusion[1].getKind() == kind::OR)
+ if ((childConclusion.getNumChildren() == 2 && childConclusion[0] == d_cl
+ && childConclusion[1].getKind() == kind::OR)
+ || (childRule == AletheRule::ASSUME
+ && childConclusion.getKind() == kind::OR))
{
hasUpdated = true;
// Add or step
std::vector<Node> subterms{d_cl};
- subterms.insert(subterms.end(),
- childConclusion[1].begin(),
- childConclusion[1].end());
+ if (childRule == AletheRule::ASSUME)
+ {
+ subterms.insert(
+ subterms.end(), childConclusion.begin(), childConclusion.end());
+ }
+ else
+ {
+ subterms.insert(subterms.end(),
+ childConclusion[1].begin(),
+ childConclusion[1].end());
+ }
Node newConclusion = nm->mkNode(kind::SEXPR, subterms);
addAletheStep(AletheRule::OR,
newConclusion,
@@ -1484,16 +1722,27 @@ bool AletheProofPostprocessCallback::finalize(Node res,
{
std::shared_ptr<ProofNode> childPf = cdp->getProofFor(children[i]);
Node childConclusion = childPf->getArguments()[2];
+ AletheRule childRule = getAletheRule(childPf->getArguments()[0]);
// Add or step
- if (childConclusion.getNumChildren() == 2
- && childConclusion[0] == d_cl
- && childConclusion[1].getKind() == kind::OR)
+ if ((childConclusion.getNumChildren() == 2
+ && childConclusion[0] == d_cl
+ && childConclusion[1].getKind() == kind::OR)
+ || (childRule == AletheRule::ASSUME
+ && childConclusion.getKind() == kind::OR))
{
hasUpdated = true;
std::vector<Node> lits{d_cl};
- lits.insert(lits.end(),
- childConclusion[1].begin(),
- childConclusion[1].end());
+ if (childRule == AletheRule::ASSUME)
+ {
+ lits.insert(
+ lits.end(), childConclusion.begin(), childConclusion.end());
+ }
+ else
+ {
+ lits.insert(lits.end(),
+ childConclusion[1].begin(),
+ childConclusion[1].end());
+ }
Node conclusion = nm->mkNode(kind::SEXPR, lits);
addAletheStep(AletheRule::OR,
conclusion,
@@ -1547,14 +1796,25 @@ bool AletheProofPostprocessCallback::finalize(Node res,
{
std::shared_ptr<ProofNode> childPf = cdp->getProofFor(children[0]);
Node childConclusion = childPf->getArguments()[2];
- if (childConclusion.getNumChildren() == 2 && childConclusion[0] == d_cl
- && childConclusion[1].getKind() == kind::OR)
+ AletheRule childRule = getAletheRule(childPf->getArguments()[0]);
+ if ((childConclusion.getNumChildren() == 2 && childConclusion[0] == d_cl
+ && childConclusion[1].getKind() == kind::OR)
+ || (childRule == AletheRule::ASSUME
+ && childConclusion.getKind() == kind::OR))
{
// Add or step for child
std::vector<Node> subterms{d_cl};
- subterms.insert(subterms.end(),
- childConclusion[1].begin(),
- childConclusion[1].end());
+ if (getAletheRule(childPf->getArguments()[0]) == AletheRule::ASSUME)
+ {
+ subterms.insert(
+ subterms.end(), childConclusion.begin(), childConclusion.end());
+ }
+ else
+ {
+ subterms.insert(subterms.end(),
+ childConclusion[1].begin(),
+ childConclusion[1].end());
+ }
Node newChild = nm->mkNode(kind::SEXPR, subterms);
addAletheStep(
AletheRule::OR, newChild, newChild, {children[0]}, {}, *cdp);
@@ -1614,10 +1874,7 @@ bool AletheProofPostprocessCallback::finalStep(
if (id != PfRule::ALETHE_RULE)
{
std::vector<Node> sanitized_args{
- res,
- res,
- nm->mkConst<Rational>(CONST_RATIONAL,
- static_cast<unsigned>(AletheRule::ASSUME))};
+ res, res, nm->mkConstInt(static_cast<uint32_t>(AletheRule::ASSUME))};
for (const Node& arg : args)
{
sanitized_args.push_back(d_anc.convert(arg));
@@ -1680,8 +1937,8 @@ bool AletheProofPostprocessCallback::addAletheStep(
}
std::vector<Node> new_args = std::vector<Node>();
- new_args.push_back(NodeManager::currentNM()->mkConst(
- CONST_RATIONAL, Rational(static_cast<unsigned>(rule))));
+ new_args.push_back(NodeManager::currentNM()->mkConstInt(
+ Rational(static_cast<uint32_t>(rule))));
new_args.push_back(res);
new_args.push_back(sanitized_conclusion);
new_args.insert(new_args.end(), args.begin(), args.end());
@@ -1712,7 +1969,37 @@ AletheProofPostprocess::AletheProofPostprocess(ProofNodeManager* pnm,
AletheProofPostprocess::~AletheProofPostprocess() {}
-void AletheProofPostprocess::process(std::shared_ptr<ProofNode> pf) {}
+void AletheProofPostprocess::process(std::shared_ptr<ProofNode> pf) {
+ // Translate proof node
+ ProofNodeUpdater updater(d_pnm, d_cb,true,false);
+ updater.process(pf->getChildren()[0]);
+
+ // In the Alethe proof format the final step has to be (cl). However, after
+ // the translation it might be (cl false). In that case additional steps are
+ // required.
+ // The function has the additional purpose of sanitizing the attributes of the
+ // first SCOPE
+ CDProof cpf(d_pnm, nullptr, "ProofNodeUpdater::CDProof", true);
+ const std::vector<std::shared_ptr<ProofNode>>& cc = pf->getChildren();
+ std::vector<Node> ccn;
+ for (const std::shared_ptr<ProofNode>& cp : cc)
+ {
+ Node cpres = cp->getResult();
+ ccn.push_back(cpres);
+ // store in the proof
+ cpf.addProof(cp);
+ }
+ if (d_cb.finalStep(
+ pf->getResult(), pf->getRule(), ccn, pf->getArguments(), &cpf))
+ {
+ std::shared_ptr<ProofNode> npn = cpf.getProofFor(pf->getResult());
+
+ // then, update the original proof node based on this one
+ Trace("pf-process-debug") << "Update node..." << std::endl;
+ d_pnm->updateNode(pf.get(), npn.get());
+ Trace("pf-process-debug") << "...update node finished." << std::endl;
+ }
+}
} // namespace proof
diff --git a/src/proof/annotation_proof_generator.cpp b/src/proof/annotation_proof_generator.cpp
new file mode 100644
index 000000000..e9467276b
--- /dev/null
+++ b/src/proof/annotation_proof_generator.cpp
@@ -0,0 +1,87 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Implementation of the annotation proof generator class.
+ */
+
+#include "proof/annotation_proof_generator.h"
+
+#include "proof/proof.h"
+#include "proof/proof_node.h"
+#include "proof/proof_node_manager.h"
+
+namespace cvc5 {
+
+AnnotationProofGenerator::AnnotationProofGenerator(ProofNodeManager* pnm,
+ context::Context* c,
+ std::string name)
+ : d_pnm(pnm),
+ d_name(name),
+ d_exps(c == nullptr ? &d_context : c),
+ d_proofs(c == nullptr ? &d_context : c)
+{
+}
+
+void AnnotationProofGenerator::setExplanationFor(Node f,
+ ProofGenerator* pg,
+ Annotator* a)
+{
+ Assert(pg != nullptr);
+ d_exps[f] = std::pair<ProofGenerator*, Annotator*>(pg, a);
+}
+
+std::shared_ptr<ProofNode> AnnotationProofGenerator::getProofFor(Node f)
+{
+ // is the proof already cached?
+ NodeProofNodeMap::iterator it = d_proofs.find(f);
+ if (it != d_proofs.end())
+ {
+ return (*it).second;
+ }
+ // make it into an actual proof now
+ NodeExpMap::iterator itx = d_exps.find(f);
+ if (itx == d_exps.end())
+ {
+ return nullptr;
+ }
+ // get the proof from the proof generator
+ std::shared_ptr<ProofNode> pf = itx->second.first->getProofFor(f);
+ if (pf == nullptr)
+ {
+ d_proofs[f] = nullptr;
+ return nullptr;
+ }
+ // now anntoate it if an annotator was provided
+ std::shared_ptr<ProofNode> pfa = pf;
+ if (itx->second.second != nullptr)
+ {
+ pfa = itx->second.second->annotate(pf);
+ }
+ d_proofs[f] = pfa;
+ return pfa;
+}
+
+TrustNode AnnotationProofGenerator::transform(const TrustNode& trn,
+ Annotator* a)
+{
+ setExplanationFor(trn.getProven(), trn.getGenerator(), a);
+ return TrustNode::mkReplaceGenTrustNode(trn, this);
+}
+
+bool AnnotationProofGenerator::hasProofFor(Node f)
+{
+ return d_exps.find(f) != d_exps.end();
+}
+
+std::string AnnotationProofGenerator::identify() const { return d_name; }
+
+} // namespace cvc5
diff --git a/src/proof/annotation_proof_generator.h b/src/proof/annotation_proof_generator.h
new file mode 100644
index 000000000..fb737dc44
--- /dev/null
+++ b/src/proof/annotation_proof_generator.h
@@ -0,0 +1,102 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * The annotation proof generator class.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__PROOF__ANNOTATION_PROOF_GENERATOR_H
+#define CVC5__PROOF__ANNOTATION_PROOF_GENERATOR_H
+
+#include "context/cdhashmap.h"
+#include "expr/node.h"
+#include "proof/proof_generator.h"
+#include "proof/trust_node.h"
+
+namespace cvc5 {
+
+class ProofNodeManager;
+
+/**
+ * Base class for annotators. An annotator is a utility that implements a
+ * simple transformation on proofs: `annotate` below.
+ */
+class Annotator
+{
+ public:
+ Annotator() {}
+ virtual ~Annotator() {}
+ /**
+ * Annotate the proof node. This must return a proof node that concludes the
+ * same thing as p.
+ */
+ virtual std::shared_ptr<ProofNode> annotate(std::shared_ptr<ProofNode> p) = 0;
+};
+
+/**
+ * Annotation proof generator, used to "wrap" proofs of other proof generators
+ * via the annotate method above.
+ */
+class AnnotationProofGenerator : public ProofGenerator
+{
+ typedef context::CDHashMap<Node, std::pair<ProofGenerator*, Annotator*>>
+ NodeExpMap;
+ typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>> NodeProofNodeMap;
+
+ public:
+ AnnotationProofGenerator(ProofNodeManager* pnm,
+ context::Context* c = nullptr,
+ std::string name = "AnnotationProofGenerator");
+ ~AnnotationProofGenerator() {}
+ /** Get the proof for formula f. */
+ std::shared_ptr<ProofNode> getProofFor(Node f) override;
+ /** Can we give the proof for formula f? */
+ bool hasProofFor(Node f) override;
+ /**
+ * Set explanation for fact f, called when pg has a proof for f.
+ *
+ * @param f The fact proven by pg,
+ * @param pg The proof generator that can prove f.
+ * @param a The annotator that will annotate the proof of f, if necessary.
+ */
+ void setExplanationFor(Node f, ProofGenerator* pg, Annotator* a);
+ /**
+ * Transform trust node, will be annotated by the given annotator.
+ */
+ TrustNode transform(const TrustNode& trn, Annotator* a);
+ /** identify */
+ std::string identify() const override;
+
+ protected:
+ /** The proof node manager */
+ ProofNodeManager* d_pnm;
+ /** Name identifier */
+ std::string d_name;
+ /** A dummy context used by this class if none is provided */
+ context::Context d_context;
+ /**
+ * A context-dependent map from formulas to a generator + annotation
+ * pair, which will be used to generate the proof of formulas if asked.
+ * We use the context provided to this class or otherwise d_context above.
+ */
+ NodeExpMap d_exps;
+ /**
+ * A context-dependent map from formulas to the proof nodes we have
+ * returned in calls to getProofFor.
+ */
+ NodeProofNodeMap d_proofs;
+};
+
+} // namespace cvc5
+
+#endif /* CVC5__PROOF__ANNOTATION_PROOF_GENERATOR_H */
diff --git a/src/proof/lazy_proof_chain.cpp b/src/proof/lazy_proof_chain.cpp
index 0de5673ab..3280626ad 100644
--- a/src/proof/lazy_proof_chain.cpp
+++ b/src/proof/lazy_proof_chain.cpp
@@ -30,7 +30,8 @@ LazyCDProofChain::LazyCDProofChain(ProofNodeManager* pnm,
ProofGenerator* defGen,
bool defRec,
const std::string& name)
- : d_manager(pnm),
+ : CDProof(pnm, c, name, false),
+ d_manager(pnm),
d_cyclic(cyclic),
d_defRec(defRec),
d_context(),
@@ -85,21 +86,10 @@ std::shared_ptr<ProofNode> LazyCDProofChain::getProofFor(Node fact)
Trace("lazy-cdproofchain")
<< "LazyCDProofChain::getProofFor: check " << cur << "\n";
Assert(toConnect.find(cur) == toConnect.end());
+ // The current fact may be justified by concrete steps added to this
+ // proof, in which case we do not use the generators.
bool rec = true;
- ProofGenerator* pg = getGeneratorForInternal(cur, rec);
- if (!pg)
- {
- Trace("lazy-cdproofchain")
- << "LazyCDProofChain::getProofFor: nothing to do\n";
- // nothing to do for this fact, it'll be a leaf in the final proof
- // node, don't post-traverse.
- visited[cur] = true;
- continue;
- }
- Trace("lazy-cdproofchain")
- << "LazyCDProofChain::getProofFor: Call generator " << pg->identify()
- << " for chain link " << cur << "\n";
- std::shared_ptr<ProofNode> curPfn = pg->getProofFor(cur);
+ std::shared_ptr<ProofNode> curPfn = getProofForInternal(cur, rec);
if (curPfn == nullptr)
{
Trace("lazy-cdproofchain")
@@ -107,7 +97,8 @@ std::shared_ptr<ProofNode> LazyCDProofChain::getProofFor(Node fact)
visited[cur] = true;
continue;
}
- // map node whose proof node must be expanded to the respective poof node
+ // map node whose proof node must be expanded to the respective poof
+ // node
toConnect[cur] = curPfn;
// We may not want to recursively connect this proof so we skip.
if (!rec)
@@ -368,6 +359,27 @@ ProofGenerator* LazyCDProofChain::getGeneratorForInternal(Node fact, bool& rec)
return nullptr;
}
+std::shared_ptr<ProofNode> LazyCDProofChain::getProofForInternal(Node fact,
+ bool& rec)
+{
+ std::shared_ptr<ProofNode> pfn = CDProof::getProofFor(fact);
+ Assert(pfn != nullptr);
+ // If concrete proof, save it, otherwise try generators.
+ if (pfn->getRule() != PfRule::ASSUME)
+ {
+ return pfn;
+ }
+ ProofGenerator* pg = getGeneratorForInternal(fact, rec);
+ if (!pg)
+ {
+ return nullptr;
+ }
+ Trace("lazy-cdproofchain")
+ << "LazyCDProofChain::getProofFor: Call generator " << pg->identify()
+ << " for chain link " << fact << "\n";
+ return pg->getProofFor(fact);
+}
+
std::string LazyCDProofChain::identify() const { return d_name; }
} // namespace cvc5
diff --git a/src/proof/lazy_proof_chain.h b/src/proof/lazy_proof_chain.h
index d15b8f9e2..114e2310e 100644
--- a/src/proof/lazy_proof_chain.h
+++ b/src/proof/lazy_proof_chain.h
@@ -20,8 +20,7 @@
#include <vector>
-#include "context/cdhashmap.h"
-#include "proof/proof_generator.h"
+#include "proof/proof.h"
namespace cvc5 {
@@ -36,7 +35,7 @@ class ProofNodeManager;
* connecting, for the proof generated to one fact, assumptions to the proofs
* generated for those assumptinos that are registered in the chain.
*/
-class LazyCDProofChain : public ProofGenerator
+class LazyCDProofChain : public CDProof
{
public:
/** Constructor
@@ -92,6 +91,11 @@ class LazyCDProofChain : public ProofGenerator
* it is required to do so. This mapping is maintained in the remainder of
* the current context (according to the context c provided to this class).
*
+ * It is important to note that pg is asked to provide a proof for expected
+ * only when no other call for the fact expected is provided via the addStep
+ * method of this class. In particular, pg is asked to prove expected when it
+ * appears as the conclusion of an ASSUME leaf within CDProof::getProofFor.
+ *
* Moreover the lazy steps of this class are expected to fulfill the
* requirement that pg.getProofFor(expected) generates a proof node closed
* with relation to
@@ -136,6 +140,14 @@ class LazyCDProofChain : public ProofGenerator
* true if we should recurse on its proof.
*/
ProofGenerator* getGeneratorForInternal(Node fact, bool& rec);
+ /**
+ * Get internal proof for fact from the underlying CDProof, if any, otherwise
+ * via a call to the above method.
+ *
+ * Returns a nullptr when no internal proof stored.
+ */
+ std::shared_ptr<ProofNode> getProofForInternal(Node fact, bool& rec);
+
/** The proof manager, used for allocating new ProofNode objects */
ProofNodeManager* d_manager;
/** Whether this instance is robust to cycles in the chain. */
diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp
index 6eab9b036..5af1c2b7e 100644
--- a/src/proof/lfsc/lfsc_node_converter.cpp
+++ b/src/proof/lfsc/lfsc_node_converter.cpp
@@ -89,7 +89,7 @@ Node LfscNodeConverter::postConvert(Node n)
}
// bound variable v is (bvar x T)
TypeNode intType = nm->integerType();
- Node x = nm->mkConst(CONST_RATIONAL, Rational(getOrAssignIndexForVar(n)));
+ Node x = nm->mkConstInt(Rational(getOrAssignIndexForVar(n)));
Node tc = typeAsNode(convertType(tn));
TypeNode ftype = nm->mkFunctionType({intType, d_sortType}, tn);
Node bvarOp = getSymbolInternal(k, ftype, "bvar");
@@ -136,8 +136,7 @@ Node LfscNodeConverter::postConvert(Node n)
TypeNode intType = nm->integerType();
TypeNode varType = nm->mkFunctionType({intType, d_sortType}, tn);
Node var = mkInternalSymbol("var", varType);
- Node index =
- nm->mkConst(CONST_RATIONAL, Rational(getOrAssignIndexForVar(n)));
+ Node index = nm->mkConstInt(Rational(getOrAssignIndexForVar(n)));
Node tc = typeAsNode(convertType(tn));
return nm->mkNode(APPLY_UF, var, index, tc);
}
@@ -176,7 +175,7 @@ Node LfscNodeConverter::postConvert(Node n)
Node hconstf = getSymbolInternal(k, tnh, "apply");
return nm->mkNode(APPLY_UF, hconstf, n[0], n[1]);
}
- else if (k == CONST_RATIONAL || k == CAST_TO_REAL)
+ else if (k == CONST_RATIONAL || k == CONST_INTEGER || k == CAST_TO_REAL)
{
if (k == CAST_TO_REAL)
{
@@ -184,8 +183,9 @@ Node LfscNodeConverter::postConvert(Node n)
do
{
n = n[0];
- Assert(n.getKind() == APPLY_UF || n.getKind() == CONST_RATIONAL);
- } while (n.getKind() != CONST_RATIONAL);
+ Assert(n.getKind() == APPLY_UF || n.getKind() == CONST_RATIONAL
+ || n.getKind() == CONST_INTEGER);
+ } while (n.getKind() != CONST_RATIONAL && n.getKind() != CONST_INTEGER);
}
TypeNode tnv = nm->mkFunctionType(tn, tn);
Node rconstf;
@@ -198,7 +198,7 @@ Node LfscNodeConverter::postConvert(Node n)
{
// use LFSC syntax for mpz negation
Node mpzn = getSymbolInternal(k, nm->mkFunctionType(tn, tn), "~");
- arg = nm->mkNode(APPLY_UF, mpzn, nm->mkConst(CONST_RATIONAL, r.abs()));
+ arg = nm->mkNode(APPLY_UF, mpzn, nm->mkConstInt(r.abs()));
}
else
{
@@ -344,8 +344,8 @@ Node LfscNodeConverter::postConvert(Node n)
Node rop = getSymbolInternal(
k, relType, printer::smt2::Smt2Printer::smtKindString(k));
RegExpLoop op = n.getOperator().getConst<RegExpLoop>();
- Node n1 = nm->mkConst(CONST_RATIONAL, Rational(op.d_loopMinOcc));
- Node n2 = nm->mkConst(CONST_RATIONAL, Rational(op.d_loopMaxOcc));
+ Node n1 = nm->mkConstInt(Rational(op.d_loopMinOcc));
+ Node n2 = nm->mkConstInt(Rational(op.d_loopMaxOcc));
return nm->mkNode(APPLY_UF, nm->mkNode(APPLY_UF, rop, n1, n2), n[0]);
}
else if (k == MATCH)
@@ -485,16 +485,14 @@ TypeNode LfscNodeConverter::postConvertType(TypeNode tn)
else if (k == BITVECTOR_TYPE)
{
tnn = d_typeKindToNodeCons[k];
- Node w = nm->mkConst(CONST_RATIONAL, Rational(tn.getBitVectorSize()));
+ Node w = nm->mkConstInt(Rational(tn.getBitVectorSize()));
tnn = nm->mkNode(APPLY_UF, tnn, w);
}
else if (k == FLOATINGPOINT_TYPE)
{
tnn = d_typeKindToNodeCons[k];
- Node e = nm->mkConst(CONST_RATIONAL,
- Rational(tn.getFloatingPointExponentSize()));
- Node s = nm->mkConst(CONST_RATIONAL,
- Rational(tn.getFloatingPointSignificandSize()));
+ Node e = nm->mkConstInt(Rational(tn.getFloatingPointExponentSize()));
+ Node s = nm->mkConstInt(Rational(tn.getFloatingPointSignificandSize()));
tnn = nm->mkNode(APPLY_UF, tnn, e, s);
}
else if (tn.getNumChildren() == 0)
@@ -723,8 +721,7 @@ void LfscNodeConverter::getCharVectorInternal(Node c, std::vector<Node>& chars)
Node aconstf = getSymbolInternal(CONST_STRING, tnc, "char");
for (unsigned i = 0, size = vec.size(); i < size; i++)
{
- Node cc = nm->mkNode(
- APPLY_UF, aconstf, nm->mkConst(CONST_RATIONAL, Rational(vec[i])));
+ Node cc = nm->mkNode(APPLY_UF, aconstf, nm->mkConstInt(Rational(vec[i])));
chars.push_back(cc);
}
}
@@ -747,42 +744,36 @@ std::vector<Node> LfscNodeConverter::getOperatorIndices(Kind k, Node n)
case BITVECTOR_EXTRACT:
{
BitVectorExtract p = n.getConst<BitVectorExtract>();
- indices.push_back(nm->mkConst(CONST_RATIONAL, Rational(p.d_high)));
- indices.push_back(nm->mkConst(CONST_RATIONAL, Rational(p.d_low)));
+ indices.push_back(nm->mkConstInt(Rational(p.d_high)));
+ indices.push_back(nm->mkConstInt(Rational(p.d_low)));
break;
}
case BITVECTOR_REPEAT:
- indices.push_back(
- nm->mkConst(CONST_RATIONAL,
- Rational(n.getConst<BitVectorRepeat>().d_repeatAmount)));
+ indices.push_back(nm->mkConstInt(
+ Rational(n.getConst<BitVectorRepeat>().d_repeatAmount)));
break;
case BITVECTOR_ZERO_EXTEND:
- indices.push_back(nm->mkConst(
- CONST_RATIONAL,
+ indices.push_back(nm->mkConstInt(
Rational(n.getConst<BitVectorZeroExtend>().d_zeroExtendAmount)));
break;
case BITVECTOR_SIGN_EXTEND:
- indices.push_back(nm->mkConst(
- CONST_RATIONAL,
+ indices.push_back(nm->mkConstInt(
Rational(n.getConst<BitVectorSignExtend>().d_signExtendAmount)));
break;
case BITVECTOR_ROTATE_LEFT:
- indices.push_back(nm->mkConst(
- CONST_RATIONAL,
+ indices.push_back(nm->mkConstInt(
Rational(n.getConst<BitVectorRotateLeft>().d_rotateLeftAmount)));
break;
case BITVECTOR_ROTATE_RIGHT:
- indices.push_back(nm->mkConst(
- CONST_RATIONAL,
+ indices.push_back(nm->mkConstInt(
Rational(n.getConst<BitVectorRotateRight>().d_rotateRightAmount)));
break;
case INT_TO_BITVECTOR:
- indices.push_back(nm->mkConst(
- CONST_RATIONAL, Rational(n.getConst<IntToBitVector>().d_size)));
+ indices.push_back(
+ nm->mkConstInt(Rational(n.getConst<IntToBitVector>().d_size)));
break;
case IAND:
- indices.push_back(
- nm->mkConst(CONST_RATIONAL, Rational(n.getConst<IntAnd>().d_size)));
+ indices.push_back(nm->mkConstInt(Rational(n.getConst<IntAnd>().d_size)));
break;
case APPLY_TESTER:
{
@@ -1023,7 +1014,7 @@ Node LfscNodeConverter::getOperatorOfClosure(Node q, bool macroApply)
Node LfscNodeConverter::getOperatorOfBoundVar(Node cop, Node v)
{
NodeManager* nm = NodeManager::currentNM();
- Node x = nm->mkConst(CONST_RATIONAL, Rational(getOrAssignIndexForVar(v)));
+ Node x = nm->mkConstInt(Rational(getOrAssignIndexForVar(v)));
Node tc = typeAsNode(convertType(v.getType()));
return nm->mkNode(APPLY_UF, cop, x, tc);
}
diff --git a/src/proof/lfsc/lfsc_util.cpp b/src/proof/lfsc/lfsc_util.cpp
index 06bedb895..aca884ddc 100644
--- a/src/proof/lfsc/lfsc_util.cpp
+++ b/src/proof/lfsc/lfsc_util.cpp
@@ -68,8 +68,8 @@ LfscRule getLfscRule(Node n)
Node mkLfscRuleNode(LfscRule r)
{
- return NodeManager::currentNM()->mkConst(CONST_RATIONAL,
- Rational(static_cast<uint32_t>(r)));
+ return NodeManager::currentNM()->mkConstInt(
+ Rational(static_cast<uint32_t>(r)));
}
bool LfscProofLetifyTraverseCallback::shouldTraverse(const ProofNode* pn)
diff --git a/src/proof/method_id.cpp b/src/proof/method_id.cpp
index 9567590a8..042df92bb 100644
--- a/src/proof/method_id.cpp
+++ b/src/proof/method_id.cpp
@@ -51,8 +51,8 @@ std::ostream& operator<<(std::ostream& out, MethodId id)
Node mkMethodId(MethodId id)
{
- return NodeManager::currentNM()->mkConst(CONST_RATIONAL,
- Rational(static_cast<uint32_t>(id)));
+ return NodeManager::currentNM()->mkConstInt(
+ Rational(static_cast<uint32_t>(id)));
}
bool getMethodId(TNode n, MethodId& i)
diff --git a/src/proof/proof_checker.cpp b/src/proof/proof_checker.cpp
index 5289d77ff..b688a28f3 100644
--- a/src/proof/proof_checker.cpp
+++ b/src/proof/proof_checker.cpp
@@ -74,8 +74,8 @@ Node ProofRuleChecker::mkKindNode(Kind k)
// UNDEFINED_KIND is negative, hence return null to avoid cast
return Node::null();
}
- return NodeManager::currentNM()->mkConst(CONST_RATIONAL,
- Rational(static_cast<uint32_t>(k)));
+ return NodeManager::currentNM()->mkConstInt(
+ Rational(static_cast<uint32_t>(k)));
}
ProofCheckerStatistics::ProofCheckerStatistics()
diff --git a/src/proof/proof_node_manager.cpp b/src/proof/proof_node_manager.cpp
index e0a7f81c0..c832ac3fa 100644
--- a/src/proof/proof_node_manager.cpp
+++ b/src/proof/proof_node_manager.cpp
@@ -28,8 +28,10 @@ using namespace cvc5::kind;
namespace cvc5 {
-ProofNodeManager::ProofNodeManager(theory::Rewriter* rr, ProofChecker* pc)
- : d_rewriter(rr), d_checker(pc)
+ProofNodeManager::ProofNodeManager(const Options& opts,
+ theory::Rewriter* rr,
+ ProofChecker* pc)
+ : d_opts(opts), d_rewriter(rr), d_checker(pc)
{
d_true = NodeManager::currentNM()->mkConst(true);
// we always allocate a proof checker, regardless of the proof checking mode
@@ -329,8 +331,8 @@ Node ProofNodeManager::checkInternal(
// a proof checking mode that does not eagerly check rule applications
if (!expected.isNull())
{
- if (options::proofCheck() == options::ProofCheckMode::LAZY
- || options::proofCheck() == options::ProofCheckMode::NONE)
+ if (d_opts.proof.proofCheck == options::ProofCheckMode::LAZY
+ || d_opts.proof.proofCheck == options::ProofCheckMode::NONE)
{
return expected;
}
@@ -435,7 +437,7 @@ bool ProofNodeManager::updateNodeInternal(
{
Assert(pn != nullptr);
// ---------------- check for cyclic
- if (options::proofCheck() == options::ProofCheckMode::EAGER)
+ if (d_opts.proof.proofCheck == options::ProofCheckMode::EAGER)
{
std::unordered_set<const ProofNode*> visited;
for (const std::shared_ptr<ProofNode>& cpc : children)
diff --git a/src/proof/proof_node_manager.h b/src/proof/proof_node_manager.h
index 533f6d173..5926a5f2e 100644
--- a/src/proof/proof_node_manager.h
+++ b/src/proof/proof_node_manager.h
@@ -27,6 +27,7 @@ namespace cvc5 {
class ProofChecker;
class ProofNode;
+class Options;
namespace theory {
class Rewriter;
@@ -58,7 +59,9 @@ class Rewriter;
class ProofNodeManager
{
public:
- ProofNodeManager(theory::Rewriter* rr, ProofChecker* pc = nullptr);
+ ProofNodeManager(const Options& opts,
+ theory::Rewriter* rr,
+ ProofChecker* pc = nullptr);
~ProofNodeManager() {}
/**
* This constructs a ProofNode with the given arguments. The expected
@@ -188,6 +191,8 @@ class ProofNodeManager
static ProofNode* cancelDoubleSymm(ProofNode* pn);
private:
+ /** Reference to the options */
+ const Options& d_opts;
/** The rewriter */
theory::Rewriter* d_rewriter;
/** The (optional) proof checker */
diff --git a/src/proof/proof_node_to_sexpr.cpp b/src/proof/proof_node_to_sexpr.cpp
index e8871af34..910af3d90 100644
--- a/src/proof/proof_node_to_sexpr.cpp
+++ b/src/proof/proof_node_to_sexpr.cpp
@@ -297,6 +297,12 @@ ProofNodeToSExpr::ArgFormat ProofNodeToSExpr::getArgumentFormat(
}
}
break;
+ case PfRule::ANNOTATION:
+ if (i == 0)
+ {
+ return ArgFormat::INFERENCE_ID;
+ }
+ break;
default: break;
}
return ArgFormat::DEFAULT;
diff --git a/src/proof/proof_rule.cpp b/src/proof/proof_rule.cpp
index c82928dc5..9bd714161 100644
--- a/src/proof/proof_rule.cpp
+++ b/src/proof/proof_rule.cpp
@@ -33,6 +33,7 @@ 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::ANNOTATION: return "ANNOTATION";
case PfRule::REMOVE_TERM_FORMULA_AXIOM: return "REMOVE_TERM_FORMULA_AXIOM";
//================================================= Trusted rules
case PfRule::THEORY_LEMMA: return "THEORY_LEMMA";
diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h
index d9e92fa92..eaa92c02c 100644
--- a/src/proof/proof_rule.h
+++ b/src/proof/proof_rule.h
@@ -185,6 +185,14 @@ enum class PfRule : uint32_t
// where F' and G' are the result of each side of the equation above. Here,
// original forms are used in a similar manner to MACRO_SR_PRED_INTRO above.
MACRO_SR_PRED_TRANSFORM,
+ // ======== Annotation
+ // Children: (P1:F)
+ // Arguments: (a1 ... an)
+ // ----------------------------------------
+ // Conclusion: F
+ // The terms a1 ... an can be anything used to annotate the proof node, one
+ // example is where a1 is a theory::InferenceId.
+ ANNOTATION,
//================================================= Processing rules
// ======== Remove Term Formulas Axiom
// Children: none
diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp
index 68e0f9a85..419dda9e2 100644
--- a/src/proof/unsat_core.cpp
+++ b/src/proof/unsat_core.cpp
@@ -52,7 +52,8 @@ UnsatCore::const_iterator UnsatCore::end() const {
void UnsatCore::toStream(std::ostream& out) const {
options::ioutils::Scope scope(out);
options::ioutils::applyDagThresh(out, 0);
- Printer::getPrinter(options::outputLanguage())->toStream(out, *this);
+ auto language = options::ioutils::getOutputLang(out);
+ Printer::getPrinter(language)->toStream(out, *this);
}
std::ostream& operator<<(std::ostream& out, const UnsatCore& core) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback