diff options
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/alethe/alethe_post_processor.cpp | 339 | ||||
-rw-r--r-- | src/proof/annotation_proof_generator.cpp | 87 | ||||
-rw-r--r-- | src/proof/annotation_proof_generator.h | 102 | ||||
-rw-r--r-- | src/proof/lazy_proof_chain.cpp | 44 | ||||
-rw-r--r-- | src/proof/lazy_proof_chain.h | 18 | ||||
-rw-r--r-- | src/proof/lfsc/lfsc_node_converter.cpp | 59 | ||||
-rw-r--r-- | src/proof/lfsc/lfsc_util.cpp | 4 | ||||
-rw-r--r-- | src/proof/method_id.cpp | 4 | ||||
-rw-r--r-- | src/proof/proof_checker.cpp | 4 | ||||
-rw-r--r-- | src/proof/proof_node_manager.cpp | 12 | ||||
-rw-r--r-- | src/proof/proof_node_manager.h | 7 | ||||
-rw-r--r-- | src/proof/proof_node_to_sexpr.cpp | 6 | ||||
-rw-r--r-- | src/proof/proof_rule.cpp | 1 | ||||
-rw-r--r-- | src/proof/proof_rule.h | 8 | ||||
-rw-r--r-- | src/proof/unsat_core.cpp | 3 |
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) { |