Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Hans-Joerg Schurr, Mathias Preiner
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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 "proof/proof_step_buffer.h"
17 : :
18 : : #include "proof/proof.h"
19 : : #include "proof/proof_checker.h"
20 : :
21 : : using namespace cvc5::internal::kind;
22 : :
23 : : namespace cvc5::internal {
24 : :
25 : 33925 : ProofStep::ProofStep() : d_rule(ProofRule::UNKNOWN) {}
26 : 17285100 : ProofStep::ProofStep(ProofRule r,
27 : : const std::vector<Node>& children,
28 : 17285100 : const std::vector<Node>& args)
29 : 17285100 : : d_rule(r), d_children(children), d_args(args)
30 : : {
31 : 17285100 : }
32 : 0 : std::ostream& operator<<(std::ostream& out, ProofStep step)
33 : : {
34 : 0 : out << "(step " << step.d_rule;
35 [ - - ]: 0 : for (const Node& c : step.d_children)
36 : : {
37 : 0 : out << " " << c;
38 : : }
39 [ - - ]: 0 : if (!step.d_args.empty())
40 : : {
41 : 0 : out << " :args";
42 [ - - ]: 0 : for (const Node& a : step.d_args)
43 : : {
44 : 0 : out << " " << a;
45 : : }
46 : : }
47 : 0 : out << ")";
48 : 0 : return out;
49 : : }
50 : :
51 : 4111240 : ProofStepBuffer::ProofStepBuffer(ProofChecker* pc,
52 : : bool ensureUnique,
53 : 4111240 : bool autoSym)
54 : 4111240 : : d_autoSym(autoSym), d_checker(pc), d_ensureUnique(ensureUnique)
55 : : {
56 : 4111240 : }
57 : :
58 : 476429 : Node ProofStepBuffer::tryStep(ProofRule id,
59 : : const std::vector<Node>& children,
60 : : const std::vector<Node>& args,
61 : : Node expected)
62 : : {
63 : : bool added;
64 : 476429 : return tryStep(added, id, children, args, expected);
65 : : }
66 : :
67 : 544210 : Node ProofStepBuffer::tryStep(bool& added,
68 : : ProofRule id,
69 : : const std::vector<Node>& children,
70 : : const std::vector<Node>& args,
71 : : Node expected)
72 : : {
73 [ - + ]: 544210 : if (d_checker == nullptr)
74 : : {
75 : 0 : added = false;
76 : 0 : Assert(false) << "ProofStepBuffer::ProofStepBuffer: no proof checker.";
77 : : return Node::null();
78 : : }
79 : : Node res =
80 : 1088420 : d_checker->checkDebug(id, children, args, expected, "pf-step-buffer");
81 [ + + ]: 544210 : if (!res.isNull())
82 : : {
83 : : // add proof step
84 : 518431 : added = addStep(id, children, args, res);
85 : : }
86 : : else
87 : : {
88 : 25779 : added = false;
89 : : }
90 : 544210 : return res;
91 : : }
92 : :
93 : 16955000 : bool ProofStepBuffer::addStep(ProofRule id,
94 : : const std::vector<Node>& children,
95 : : const std::vector<Node>& args,
96 : : Node expected)
97 : : {
98 [ + + ]: 16955000 : if (d_ensureUnique)
99 : : {
100 [ + + ]: 63707 : if (d_allSteps.find(expected) != d_allSteps.end())
101 : : {
102 [ + - ]: 10932 : Trace("psb-debug") << "Discard " << expected << " from " << id
103 : 5466 : << std::endl;
104 : 5466 : return false;
105 : : }
106 : 58241 : d_allSteps.insert(expected);
107 : : // if we are automatically considering symmetry, we also add the symmetric
108 : : // fact here
109 [ + - ]: 58241 : if (d_autoSym)
110 : : {
111 : 116482 : Node sexpected = CDProof::getSymmFact(expected);
112 [ + + ]: 58241 : if (!sexpected.isNull())
113 : : {
114 : 47506 : d_allSteps.insert(sexpected);
115 : : }
116 : : }
117 [ + - ]: 58241 : Trace("psb-debug") << "Add " << expected << " from " << id << std::endl;
118 : : }
119 : 16949500 : d_steps.push_back(
120 : 33899000 : std::pair<Node, ProofStep>(expected, ProofStep(id, children, args)));
121 : 16949500 : return true;
122 : : }
123 : 187 : bool ProofStepBuffer::addTrustedStep(TrustId id,
124 : : const std::vector<Node>& children,
125 : : const std::vector<Node>& args,
126 : : Node conc)
127 : : {
128 : 187 : std::vector<Node> sargs;
129 : 187 : sargs.push_back(mkTrustId(NodeManager::currentNM(), id));
130 : 187 : sargs.push_back(conc);
131 : 187 : sargs.insert(sargs.end(), args.begin(), args.end());
132 : 374 : return addStep(ProofRule::TRUST, children, sargs, conc);
133 : : }
134 : :
135 : 0 : void ProofStepBuffer::addSteps(ProofStepBuffer& psb)
136 : : {
137 : 0 : const std::vector<std::pair<Node, ProofStep>>& steps = psb.getSteps();
138 [ - - ]: 0 : for (const std::pair<Node, ProofStep>& step : steps)
139 : : {
140 : 0 : addStep(step.second.d_rule,
141 : 0 : step.second.d_children,
142 : 0 : step.second.d_args,
143 : 0 : step.first);
144 : : }
145 : 0 : }
146 : :
147 : 0 : void ProofStepBuffer::popStep()
148 : : {
149 : 0 : Assert(!d_steps.empty());
150 [ - - ]: 0 : if (!d_steps.empty())
151 : : {
152 [ - - ]: 0 : if (d_ensureUnique)
153 : : {
154 : 0 : d_allSteps.erase(d_steps.back().first);
155 : : }
156 : 0 : d_steps.pop_back();
157 : : }
158 : 0 : }
159 : :
160 : 0 : size_t ProofStepBuffer::getNumSteps() const { return d_steps.size(); }
161 : :
162 : 4098130 : const std::vector<std::pair<Node, ProofStep>>& ProofStepBuffer::getSteps() const
163 : : {
164 : 4098130 : return d_steps;
165 : : }
166 : :
167 : 77988 : void ProofStepBuffer::clear()
168 : : {
169 : 77988 : d_steps.clear();
170 : 77988 : d_allSteps.clear();
171 : 77988 : }
172 : :
173 : : } // namespace cvc5::internal
|
