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