diff options
| -rw-r--r-- | src/proof/alethe/alethe_post_processor.cpp | 111 | ||||
| -rw-r--r-- | src/proof/alethe/alethe_post_processor.h | 15 |
2 files changed, 122 insertions, 4 deletions
diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp new file mode 100644 index 000000000..738497ece --- /dev/null +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -0,0 +1,111 @@ +/****************************************************************************** + * Top contributors (to current version): + * Hanna Lachnitt, Haniel Barbosa + * + * 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 module for processing proof nodes into Alethe proof nodes + */ + +#include "proof/alethe/alethe_post_processor.h" + +#include "expr/node_algorithm.h" +#include "proof/proof.h" +#include "proof/proof_checker.h" +#include "util/rational.h" + +namespace cvc5 { + +namespace proof { + +AletheProofPostprocessCallback::AletheProofPostprocessCallback( + ProofNodeManager* pnm, AletheNodeConverter& anc) + : d_pnm(pnm), d_anc(anc) +{ + NodeManager* nm = NodeManager::currentNM(); + d_cl = nm->mkBoundVar("cl", nm->sExprType()); +} + +bool AletheProofPostprocessCallback::shouldUpdate(std::shared_ptr<ProofNode> pn, + const std::vector<Node>& fa, + bool& continueUpdate) +{ + return pn->getRule() != PfRule::ALETHE_RULE; +} + +bool AletheProofPostprocessCallback::update(Node res, + PfRule id, + const std::vector<Node>& children, + const std::vector<Node>& args, + CDProof* cdp, + bool& continueUpdate) +{ + Trace("alethe-proof") << "- Alethe post process callback " << res << " " << id + << " " << children << " / " << args << std::endl; + + NodeManager* nm = NodeManager::currentNM(); + std::vector<Node> new_args = std::vector<Node>(); + + switch (id) + { + default: + { + return addAletheStep(AletheRule::UNDEFINED, + res, + nm->mkNode(kind::SEXPR, d_cl, res), + children, + args, + *cdp); + } + } +} + +bool AletheProofPostprocessCallback::addAletheStep( + AletheRule rule, + Node res, + Node conclusion, + const std::vector<Node>& children, + const std::vector<Node>& args, + CDProof& cdp) +{ + // delete attributes + Node sanitized_conclusion = conclusion; + if (expr::hasClosure(conclusion)) + { + sanitized_conclusion = d_anc.convert(conclusion); + } + + std::vector<Node> new_args = std::vector<Node>(); + new_args.push_back( + NodeManager::currentNM()->mkConst<Rational>(static_cast<unsigned>(rule))); + new_args.push_back(res); + new_args.push_back(sanitized_conclusion); + new_args.insert(new_args.end(), args.begin(), args.end()); + Trace("alethe-proof") << "... add Alethe step " << res << " / " << conclusion + << " " << rule << " " << children << " / " << new_args + << std::endl; + return cdp.addStep(res, PfRule::ALETHE_RULE, children, new_args); +} + +bool AletheProofPostprocessCallback::addAletheStepFromOr( + Node res, + AletheRule rule, + const std::vector<Node>& children, + const std::vector<Node>& args, + CDProof& cdp) +{ + std::vector<Node> subterms = {d_cl}; + subterms.insert(subterms.end(), res.begin(), res.end()); + Node conclusion = NodeManager::currentNM()->mkNode(kind::SEXPR, subterms); + return addAletheStep(rule, res, conclusion, children, args, cdp); +} + +} // namespace proof + +} // namespace cvc5 diff --git a/src/proof/alethe/alethe_post_processor.h b/src/proof/alethe/alethe_post_processor.h index a19903f12..d8fae8a55 100644 --- a/src/proof/alethe/alethe_post_processor.h +++ b/src/proof/alethe/alethe_post_processor.h @@ -16,8 +16,9 @@ #ifndef CVC4__PROOF__ALETHE_PROOF_PROCESSOR_H #define CVC4__PROOF__ALETHE_PROOF_PROCESSOR_H -#include "proof/alethe/alethe_proof_rule.h" #include "proof/proof_node_updater.h" +#include "proof/alethe/alethe_node_converter.h" +#include "proof/alethe/alethe_proof_rule.h" namespace cvc5 { @@ -30,7 +31,8 @@ namespace proof { class AletheProofPostprocessCallback : public ProofNodeUpdaterCallback { public: - AletheProofPostprocessCallback(ProofNodeManager* pnm); + AletheProofPostprocessCallback(ProofNodeManager* pnm, + AletheNodeConverter& anc); ~AletheProofPostprocessCallback() {} /** Should proof pn be updated? Only if its top-level proof rule is not an * Alethe proof rule. @@ -52,6 +54,8 @@ class AletheProofPostprocessCallback : public ProofNodeUpdaterCallback private: /** The proof node manager */ ProofNodeManager* d_pnm; + /** The Alethe node converter */ + AletheNodeConverter& d_anc; /** The cl operator * For every step the conclusion is a clause. But since the or operator *requires at least two arguments it is extended by the cl operator. In case @@ -114,7 +118,8 @@ class AletheProofPostprocessCallback : public ProofNodeUpdaterCallback class AletheProofPostprocessFinalCallback : public ProofNodeUpdaterCallback { public: - AletheProofPostprocessFinalCallback(ProofNodeManager* pnm); + AletheProofPostprocessFinalCallback(ProofNodeManager* pnm, + AletheNodeConverter& anc); ~AletheProofPostprocessFinalCallback() {} /** Should proof pn be updated? It should, if the last step is printed as (cl * false) or if it is an assumption (in that case it is printed as false). @@ -139,6 +144,8 @@ class AletheProofPostprocessFinalCallback : public ProofNodeUpdaterCallback private: /** The proof node manager */ ProofNodeManager* d_pnm; + /** The Alethe node converter */ + AletheNodeConverter& d_anc; /** The cl operator is defined as described in the * AletheProofPostprocessCallback class above **/ @@ -152,7 +159,7 @@ class AletheProofPostprocessFinalCallback : public ProofNodeUpdaterCallback class AletheProofPostprocess { public: - AletheProofPostprocess(ProofNodeManager* pnm); + AletheProofPostprocess(ProofNodeManager* pnm, AletheNodeConverter& anc); ~AletheProofPostprocess(); /** post-process */ void process(std::shared_ptr<ProofNode> pf); |