diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-09-15 23:36:21 -0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-15 23:36:21 -0300 |
commit | 8a126d59141d2889e3b10b07ece4b10f48511a71 (patch) | |
tree | b4d5f303a120fbf5eeba3c7cfb0c8ea81eff9555 /src/expr/buffered_proof_generator.h | |
parent | 33f51490a9df73d8fee25fb88b19a87339b28e95 (diff) |
[proof-new] A simple proof generator for buffered proof steps (#5069)
This commit also modifies proof equality engine to use this new proof generator rather than the FactProofGenerator, on which this new one is based.
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Diffstat (limited to 'src/expr/buffered_proof_generator.h')
-rw-r--r-- | src/expr/buffered_proof_generator.h | 65 |
1 files changed, 65 insertions, 0 deletions
diff --git a/src/expr/buffered_proof_generator.h b/src/expr/buffered_proof_generator.h new file mode 100644 index 000000000..987bd2465 --- /dev/null +++ b/src/expr/buffered_proof_generator.h @@ -0,0 +1,65 @@ +/********************* */ +/*! \file buffered_proof_generator.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Haniel Barbosa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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 A proof generator for buffered proof steps + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H +#define CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H + +#include <map> +#include <vector> + +#include "context/cdhashmap.h" +#include "context/cdhashset.h" +#include "expr/proof_generator.h" +#include "expr/proof_node_manager.h" +#include "expr/proof_step_buffer.h" + +namespace CVC4 { + +/** + * The proof generator for buffered steps. This class is a context-dependent + * mapping from formulas to proof steps. It does not generate ProofNodes until it + * is asked to provide a proof for a given fact. + */ +class BufferedProofGenerator : public ProofGenerator +{ + typedef context::CDHashMap<Node, std::shared_ptr<ProofStep>, NodeHashFunction> + NodeProofStepMap; + + public: + BufferedProofGenerator(context::Context* c, ProofNodeManager* pnm); + ~BufferedProofGenerator() {} + /** add step + * Unless the overwrite policy is ALWAYS it does not replace previously + * registered steps (modulo (dis)equality symmetry). + */ + bool addStep(Node fact, + ProofStep ps, + CDPOverwrite opolicy = CDPOverwrite::NEVER); + /** Get proof for. It is robust to (dis)equality symmetry. */ + std::shared_ptr<ProofNode> getProofFor(Node f) override; + /** identify */ + std::string identify() const override { return "BufferedProofGenerator"; } + + private: + /** maps expected to ProofStep */ + NodeProofStepMap d_facts; + /** the proof node manager */ + ProofNodeManager* d_pnm; +}; + +} // namespace CVC4 + +#endif /* CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H */ |