1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* 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 |
|
* Proof step and proof step buffer utilities. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5_private.h" |
17 |
|
|
18 |
|
#ifndef CVC5__PROOF__PROOF_STEP_BUFFER_H |
19 |
|
#define CVC5__PROOF__PROOF_STEP_BUFFER_H |
20 |
|
|
21 |
|
#include <vector> |
22 |
|
|
23 |
|
#include "expr/node.h" |
24 |
|
#include "proof/proof_rule.h" |
25 |
|
|
26 |
|
namespace cvc5 { |
27 |
|
|
28 |
|
class ProofChecker; |
29 |
|
|
30 |
|
/** |
31 |
|
* Information for constructing a step in a CDProof. Notice that the conclusion |
32 |
|
* of the proof step is intentionally not included in this data structure. |
33 |
|
* Instead, it is intended that conclusions may be associated with proof steps |
34 |
|
* based on e.g. the result of proof checking. |
35 |
|
*/ |
36 |
18838205 |
class ProofStep |
37 |
|
{ |
38 |
|
public: |
39 |
|
ProofStep(); |
40 |
|
ProofStep(PfRule r, |
41 |
|
const std::vector<Node>& children, |
42 |
|
const std::vector<Node>& args); |
43 |
|
/** The proof rule */ |
44 |
|
PfRule d_rule; |
45 |
|
/** The proof children */ |
46 |
|
std::vector<Node> d_children; |
47 |
|
/** The proof arguments */ |
48 |
|
std::vector<Node> d_args; |
49 |
|
}; |
50 |
|
std::ostream& operator<<(std::ostream& out, ProofStep step); |
51 |
|
|
52 |
|
/** |
53 |
|
* Class used to speculatively try and buffer a set of proof steps before |
54 |
|
* sending them to a proof object. |
55 |
|
*/ |
56 |
|
class ProofStepBuffer |
57 |
|
{ |
58 |
|
public: |
59 |
|
ProofStepBuffer(ProofChecker* pc = nullptr); |
60 |
16317 |
~ProofStepBuffer() {} |
61 |
|
/** |
62 |
|
* Returns the conclusion of the proof step, as determined by the proof |
63 |
|
* checker of the given proof. If this is non-null, then the given step |
64 |
|
* is added to the buffer maintained by this class. |
65 |
|
* |
66 |
|
* If expected is non-null, then this method returns null if the result of |
67 |
|
* checking is not equal to expected. |
68 |
|
*/ |
69 |
|
Node tryStep(PfRule id, |
70 |
|
const std::vector<Node>& children, |
71 |
|
const std::vector<Node>& args, |
72 |
|
Node expected = Node::null()); |
73 |
|
/** Same as above, without checking */ |
74 |
|
void addStep(PfRule id, |
75 |
|
const std::vector<Node>& children, |
76 |
|
const std::vector<Node>& args, |
77 |
|
Node expected); |
78 |
|
/** Multi-step version */ |
79 |
|
void addSteps(ProofStepBuffer& psb); |
80 |
|
/** pop step */ |
81 |
|
void popStep(); |
82 |
|
/** Get num steps */ |
83 |
|
size_t getNumSteps() const; |
84 |
|
/** Get steps */ |
85 |
|
const std::vector<std::pair<Node, ProofStep>>& getSteps() const; |
86 |
|
/** Clear */ |
87 |
|
void clear(); |
88 |
|
|
89 |
|
private: |
90 |
|
/** The proof checker*/ |
91 |
|
ProofChecker* d_checker; |
92 |
|
/** the queued proof steps */ |
93 |
|
std::vector<std::pair<Node, ProofStep>> d_steps; |
94 |
|
}; |
95 |
|
|
96 |
|
} // namespace cvc5 |
97 |
|
|
98 |
|
#endif /* CVC5__PROOF__PROOF_STEP_BUFFER_H */ |