diff options
Diffstat (limited to 'src/expr/proof_step_buffer.h')
-rw-r--r-- | src/expr/proof_step_buffer.h | 96 |
1 files changed, 96 insertions, 0 deletions
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 <vector> + +#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<Node>& children, + const std::vector<Node>& args); + /** The proof rule */ + PfRule d_rule; + /** The proof children */ + std::vector<Node> d_children; + /** The proof arguments */ + std::vector<Node> 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<Node>& children, + const std::vector<Node>& args, + Node expected = Node::null()); + /** Same as above, without checking */ + void addStep(PfRule id, + const std::vector<Node>& children, + const std::vector<Node>& 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<std::pair<Node, ProofStep>>& getSteps() const; + /** Clear */ + void clear(); + + private: + /** The proof checker*/ + ProofChecker* d_checker; + /** the queued proof steps */ + std::vector<std::pair<Node, ProofStep>> d_steps; +}; + +} // namespace CVC4 + +#endif /* CVC4__EXPR__PROOF_STEP_BUFFER_H */ |