From: Andrew Reynolds Date: Mon, 1 Jun 2020 23:34:21 +0000 (-0500) Subject: (proof-new) Proof step buffer utilities (#4533) X-Git-Tag: cvc5-1.0.0~3274 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b826fc8ae95fc13c4e2be45e39961199392a4dda;p=cvc5.git (proof-new) Proof step buffer utilities (#4533) This class is used for delaying proof node creation until it is necessary. --- diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 413041213..3d41b7a72 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -51,6 +51,8 @@ libcvc4_add_sources( proof_rule.h proof_skolem_cache.cpp proof_skolem_cache.h + proof_step_buffer.cpp + proof_step_buffer.h symbol_table.cpp symbol_table.h term_canonize.cpp diff --git a/src/expr/proof_step_buffer.cpp b/src/expr/proof_step_buffer.cpp new file mode 100644 index 000000000..800efa2c0 --- /dev/null +++ b/src/expr/proof_step_buffer.cpp @@ -0,0 +1,109 @@ +/********************* */ +/*! \file proof_step_buffer.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 Implementation of proof step and proof step buffer utilities. + **/ + +#include "expr/proof_step_buffer.h" + +using namespace CVC4::kind; + +namespace CVC4 { + +ProofStep::ProofStep() : d_rule(PfRule::UNKNOWN) {} +ProofStep::ProofStep(PfRule r, + const std::vector& children, + const std::vector& args) + : d_rule(r), d_children(children), d_args(args) +{ +} +std::ostream& operator<<(std::ostream& out, ProofStep step) +{ + out << "(step " << step.d_rule; + for (const Node& c : step.d_children) + { + out << " " << c; + } + if (!step.d_args.empty()) + { + out << " :args"; + for (const Node& a : step.d_args) + { + out << " " << a; + } + } + out << ")"; + return out; +} + +ProofStepBuffer::ProofStepBuffer(ProofChecker* pc) : d_checker(pc) {} + +Node ProofStepBuffer::tryStep(PfRule id, + const std::vector& children, + const std::vector& args, + Node expected) +{ + if (d_checker == nullptr) + { + Assert(false) << "ProofStepBuffer::ProofStepBuffer: no proof checker."; + return Node::null(); + } + Node res = + d_checker->checkDebug(id, children, args, expected, "pf-step-buffer"); + if (!res.isNull()) + { + // add proof step + d_steps.push_back( + std::pair(res, ProofStep(id, children, args))); + } + return res; +} + +void ProofStepBuffer::addStep(PfRule id, + const std::vector& children, + const std::vector& args, + Node expected) +{ + d_steps.push_back( + std::pair(expected, ProofStep(id, children, args))); +} + +void ProofStepBuffer::addSteps(ProofStepBuffer& psb) +{ + const std::vector>& steps = psb.getSteps(); + for (const std::pair& step : steps) + { + addStep(step.second.d_rule, + step.second.d_children, + step.second.d_args, + step.first); + } +} + +void ProofStepBuffer::popStep() +{ + Assert(!d_steps.empty()); + if (!d_steps.empty()) + { + d_steps.pop_back(); + } +} + +size_t ProofStepBuffer::getNumSteps() const { return d_steps.size(); } + +const std::vector>& ProofStepBuffer::getSteps() const +{ + return d_steps; +} + +void ProofStepBuffer::clear() { d_steps.clear(); } + +} // namespace CVC4 diff --git a/src/expr/proof_step_buffer.h b/src/expr/proof_step_buffer.h new file mode 100644 index 000000000..005aee399 --- /dev/null +++ b/src/expr/proof_step_buffer.h @@ -0,0 +1,96 @@ +/********************* */ +/*! \file proof_step_buffer.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 Proof step and proof step buffer utilities. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__EXPR__PROOF_STEP_BUFFER_H +#define CVC4__EXPR__PROOF_STEP_BUFFER_H + +#include + +#include "expr/node.h" +#include "expr/proof_checker.h" +#include "expr/proof_rule.h" + +namespace CVC4 { + +/** + * Information for constructing a step in a CDProof. Notice that the conclusion + * of the proof step is intentionally not included in this data structure. + * Instead, it is intended that conclusions may be associated with proof steps + * based on e.g. the result of proof checking. + */ +class ProofStep +{ + public: + ProofStep(); + ProofStep(PfRule r, + const std::vector& children, + const std::vector& args); + /** The proof rule */ + PfRule d_rule; + /** The proof children */ + std::vector d_children; + /** The proof arguments */ + std::vector d_args; +}; +std::ostream& operator<<(std::ostream& out, ProofStep step); + +/** + * Class used to speculatively try and buffer a set of proof steps before + * sending them to a proof object. + */ +class ProofStepBuffer +{ + public: + ProofStepBuffer(ProofChecker* pc = nullptr); + ~ProofStepBuffer() {} + /** + * Returns the conclusion of the proof step, as determined by the proof + * checker of the given proof. If this is non-null, then the given step + * is added to the buffer maintained by this class. + * + * If expected is non-null, then this method returns null if the result of + * checking is not equal to expected. + */ + Node tryStep(PfRule id, + const std::vector& children, + const std::vector& args, + Node expected = Node::null()); + /** Same as above, without checking */ + void addStep(PfRule id, + const std::vector& children, + const std::vector& args, + Node expected); + /** Multi-step version */ + void addSteps(ProofStepBuffer& psb); + /** pop step */ + void popStep(); + /** Get num steps */ + size_t getNumSteps() const; + /** Get steps */ + const std::vector>& getSteps() const; + /** Clear */ + void clear(); + + private: + /** The proof checker*/ + ProofChecker* d_checker; + /** the queued proof steps */ + std::vector> d_steps; +}; + +} // namespace CVC4 + +#endif /* CVC4__EXPR__PROOF_STEP_BUFFER_H */