1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Aina Niemetz |
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 |
|
* Implementation of proof step and proof step buffer utilities. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "expr/proof_step_buffer.h" |
17 |
|
|
18 |
|
#include "expr/proof_checker.h" |
19 |
|
|
20 |
|
using namespace cvc5::kind; |
21 |
|
|
22 |
|
namespace cvc5 { |
23 |
|
|
24 |
2760 |
ProofStep::ProofStep() : d_rule(PfRule::UNKNOWN) {} |
25 |
1862589 |
ProofStep::ProofStep(PfRule r, |
26 |
|
const std::vector<Node>& children, |
27 |
1862589 |
const std::vector<Node>& args) |
28 |
1862589 |
: d_rule(r), d_children(children), d_args(args) |
29 |
|
{ |
30 |
1862589 |
} |
31 |
|
std::ostream& operator<<(std::ostream& out, ProofStep step) |
32 |
|
{ |
33 |
|
out << "(step " << step.d_rule; |
34 |
|
for (const Node& c : step.d_children) |
35 |
|
{ |
36 |
|
out << " " << c; |
37 |
|
} |
38 |
|
if (!step.d_args.empty()) |
39 |
|
{ |
40 |
|
out << " :args"; |
41 |
|
for (const Node& a : step.d_args) |
42 |
|
{ |
43 |
|
out << " " << a; |
44 |
|
} |
45 |
|
} |
46 |
|
out << ")"; |
47 |
|
return out; |
48 |
|
} |
49 |
|
|
50 |
14164 |
ProofStepBuffer::ProofStepBuffer(ProofChecker* pc) : d_checker(pc) {} |
51 |
|
|
52 |
112340 |
Node ProofStepBuffer::tryStep(PfRule id, |
53 |
|
const std::vector<Node>& children, |
54 |
|
const std::vector<Node>& args, |
55 |
|
Node expected) |
56 |
|
{ |
57 |
112340 |
if (d_checker == nullptr) |
58 |
|
{ |
59 |
|
Assert(false) << "ProofStepBuffer::ProofStepBuffer: no proof checker."; |
60 |
|
return Node::null(); |
61 |
|
} |
62 |
|
Node res = |
63 |
224680 |
d_checker->checkDebug(id, children, args, expected, "pf-step-buffer"); |
64 |
112340 |
if (!res.isNull()) |
65 |
|
{ |
66 |
|
// add proof step |
67 |
224408 |
d_steps.push_back( |
68 |
224408 |
std::pair<Node, ProofStep>(res, ProofStep(id, children, args))); |
69 |
|
} |
70 |
112340 |
return res; |
71 |
|
} |
72 |
|
|
73 |
1705495 |
void ProofStepBuffer::addStep(PfRule id, |
74 |
|
const std::vector<Node>& children, |
75 |
|
const std::vector<Node>& args, |
76 |
|
Node expected) |
77 |
|
{ |
78 |
3410990 |
d_steps.push_back( |
79 |
3410990 |
std::pair<Node, ProofStep>(expected, ProofStep(id, children, args))); |
80 |
1705495 |
} |
81 |
|
|
82 |
|
void ProofStepBuffer::addSteps(ProofStepBuffer& psb) |
83 |
|
{ |
84 |
|
const std::vector<std::pair<Node, ProofStep>>& steps = psb.getSteps(); |
85 |
|
for (const std::pair<Node, ProofStep>& step : steps) |
86 |
|
{ |
87 |
|
addStep(step.second.d_rule, |
88 |
|
step.second.d_children, |
89 |
|
step.second.d_args, |
90 |
|
step.first); |
91 |
|
} |
92 |
|
} |
93 |
|
|
94 |
185 |
void ProofStepBuffer::popStep() |
95 |
|
{ |
96 |
185 |
Assert(!d_steps.empty()); |
97 |
185 |
if (!d_steps.empty()) |
98 |
|
{ |
99 |
185 |
d_steps.pop_back(); |
100 |
|
} |
101 |
185 |
} |
102 |
|
|
103 |
|
size_t ProofStepBuffer::getNumSteps() const { return d_steps.size(); } |
104 |
|
|
105 |
129262 |
const std::vector<std::pair<Node, ProofStep>>& ProofStepBuffer::getSteps() const |
106 |
|
{ |
107 |
129262 |
return d_steps; |
108 |
|
} |
109 |
|
|
110 |
125551 |
void ProofStepBuffer::clear() { d_steps.clear(); } |
111 |
|
|
112 |
28194 |
} // namespace cvc5 |