1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Haniel Barbosa, Andrew Reynolds, Gereon Kremer |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* A proof generator for buffered proof steps. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5_private.h" |
17 |
|
|
18 |
|
#ifndef CVC5__EXPR__BUFFERED_PROOF_GENERATOR_H |
19 |
|
#define CVC5__EXPR__BUFFERED_PROOF_GENERATOR_H |
20 |
|
|
21 |
|
#include "context/cdhashmap.h" |
22 |
|
#include "expr/proof_generator.h" |
23 |
|
|
24 |
|
namespace cvc5 { |
25 |
|
|
26 |
|
class ProofNodeManager; |
27 |
|
class ProofStep; |
28 |
|
|
29 |
|
/** |
30 |
|
* The proof generator for buffered steps. This class is a context-dependent |
31 |
|
* mapping from formulas to proof steps. It does not generate ProofNodes until it |
32 |
|
* is asked to provide a proof for a given fact. |
33 |
|
*/ |
34 |
|
class BufferedProofGenerator : public ProofGenerator |
35 |
|
{ |
36 |
|
typedef context::CDHashMap<Node, std::shared_ptr<ProofStep>> NodeProofStepMap; |
37 |
|
|
38 |
|
public: |
39 |
|
BufferedProofGenerator(context::Context* c, ProofNodeManager* pnm); |
40 |
10246 |
~BufferedProofGenerator() {} |
41 |
|
/** add step |
42 |
|
* Unless the overwrite policy is ALWAYS it does not replace previously |
43 |
|
* registered steps (modulo (dis)equality symmetry). |
44 |
|
*/ |
45 |
|
bool addStep(Node fact, |
46 |
|
ProofStep ps, |
47 |
|
CDPOverwrite opolicy = CDPOverwrite::NEVER); |
48 |
|
/** Get proof for. It is robust to (dis)equality symmetry. */ |
49 |
|
std::shared_ptr<ProofNode> getProofFor(Node f) override; |
50 |
|
/** Whether a step has been registered for f. */ |
51 |
|
bool hasProofFor(Node f) override; |
52 |
|
/** identify */ |
53 |
206449 |
std::string identify() const override { return "BufferedProofGenerator"; } |
54 |
|
|
55 |
|
private: |
56 |
|
/** maps expected to ProofStep */ |
57 |
|
NodeProofStepMap d_facts; |
58 |
|
/** the proof node manager */ |
59 |
|
ProofNodeManager* d_pnm; |
60 |
|
}; |
61 |
|
|
62 |
|
} // namespace cvc5 |
63 |
|
|
64 |
|
#endif /* CVC5__EXPR__BUFFERED_PROOF_GENERATOR_H */ |