Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Hans-Joerg Schurr, Haniel Barbosa
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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 node to s-expression.
14 : : */
15 : :
16 : : #include "proof/proof_node_to_sexpr.h"
17 : :
18 : : #include <iostream>
19 : : #include <sstream>
20 : :
21 : : #include "options/proof_options.h"
22 : : #include "proof/proof_checker.h"
23 : : #include "proof/proof_node.h"
24 : : #include "theory/builtin/proof_checker.h"
25 : :
26 : : using namespace cvc5::internal::kind;
27 : :
28 : : namespace cvc5::internal {
29 : :
30 : 239 : ProofNodeToSExpr::ProofNodeToSExpr()
31 : : {
32 : 239 : NodeManager* nm = NodeManager::currentNM();
33 : : // use raw symbols so that `:args` is not converted to `|:args|`
34 : 239 : d_conclusionMarker = nm->mkRawSymbol(":conclusion", nm->sExprType());
35 : 239 : d_argsMarker = nm->mkRawSymbol(":args", nm->sExprType());
36 : 239 : }
37 : :
38 : 239 : Node ProofNodeToSExpr::convertToSExpr(const ProofNode* pn, bool printConclusion)
39 : : {
40 : 239 : NodeManager* nm = NodeManager::currentNM();
41 : 239 : std::map<const ProofNode*, Node>::iterator it;
42 : 478 : std::vector<const ProofNode*> visit;
43 : 478 : std::vector<const ProofNode*> traversing;
44 : : const ProofNode* cur;
45 : 239 : visit.push_back(pn);
46 : 2273 : do
47 : : {
48 : 2512 : cur = visit.back();
49 : 2512 : visit.pop_back();
50 : 2512 : it = d_pnMap.find(cur);
51 : :
52 [ + + ]: 2512 : if (it == d_pnMap.end())
53 : : {
54 : 1256 : d_pnMap[cur] = Node::null();
55 : 1256 : traversing.push_back(cur);
56 : 1256 : visit.push_back(cur);
57 : 1256 : const std::vector<std::shared_ptr<ProofNode>>& pc = cur->getChildren();
58 [ + + ]: 2273 : for (const std::shared_ptr<ProofNode>& cp : pc)
59 : : {
60 : 1017 : if (std::find(traversing.begin(), traversing.end(), cp.get())
61 [ - + ]: 2034 : != traversing.end())
62 : : {
63 : 0 : Unhandled() << "ProofNodeToSExpr::convertToSExpr: cyclic proof! (use "
64 : 0 : "--proof-check=eager)"
65 : 0 : << std::endl;
66 : : return Node::null();
67 : : }
68 : 1017 : visit.push_back(cp.get());
69 : : }
70 : : }
71 [ + - ]: 1256 : else if (it->second.isNull())
72 : : {
73 [ - + ][ - + ]: 1256 : Assert(!traversing.empty());
[ - - ]
74 : 1256 : traversing.pop_back();
75 : 1256 : std::vector<Node> children;
76 : : // add proof rule
77 : 1256 : ProofRule r = cur->getRule();
78 : 1256 : children.push_back(getOrMkProofRuleVariable(r));
79 [ - + ]: 1256 : if (printConclusion)
80 : : {
81 : 0 : children.push_back(d_conclusionMarker);
82 : 0 : children.push_back(cur->getResult());
83 : : }
84 : 1256 : const std::vector<std::shared_ptr<ProofNode>>& pc = cur->getChildren();
85 [ + + ]: 2273 : for (const std::shared_ptr<ProofNode>& cp : pc)
86 : : {
87 : 1017 : it = d_pnMap.find(cp.get());
88 [ - + ][ - + ]: 1017 : Assert(it != d_pnMap.end());
[ - - ]
89 [ - + ][ - + ]: 1017 : Assert(!it->second.isNull());
[ - - ]
90 : 1017 : children.push_back(it->second);
91 : : }
92 : : // add arguments
93 : 1256 : const std::vector<Node>& args = cur->getArguments();
94 [ + + ]: 1256 : if (!args.empty())
95 : : {
96 : 1207 : children.push_back(d_argsMarker);
97 : : // needed to ensure builtin operators are not treated as operators
98 : : // this can be the case for CONG where d_args may contain a builtin
99 : : // operator
100 : 2414 : std::vector<Node> argsPrint;
101 [ + + ]: 3672 : for (size_t i = 0, nargs = args.size(); i < nargs; i++)
102 : : {
103 : 2465 : ArgFormat f = getArgumentFormat(cur, i);
104 : 4930 : Node av = getArgument(args[i], f);
105 : 2465 : argsPrint.push_back(av);
106 : : }
107 : 2414 : Node argsC = nm->mkNode(Kind::SEXPR, argsPrint);
108 : 1207 : children.push_back(argsC);
109 : : }
110 : 1256 : d_pnMap[cur] = nm->mkNode(Kind::SEXPR, children);
111 : : }
112 [ + + ]: 2512 : } while (!visit.empty());
113 [ - + ][ - + ]: 239 : Assert(d_pnMap.find(pn) != d_pnMap.end());
[ - - ]
114 [ - + ][ - + ]: 239 : Assert(!d_pnMap.find(pn)->second.isNull());
[ - - ]
115 : 239 : return d_pnMap[pn];
116 : : }
117 : :
118 : 1256 : Node ProofNodeToSExpr::getOrMkProofRuleVariable(ProofRule r)
119 : : {
120 : 1256 : std::map<ProofRule, Node>::iterator it = d_pfrMap.find(r);
121 [ + + ]: 1256 : if (it != d_pfrMap.end())
122 : : {
123 : 665 : return it->second;
124 : : }
125 : 1182 : std::stringstream ss;
126 : 591 : ss << r;
127 : 591 : NodeManager* nm = NodeManager::currentNM();
128 : 1773 : Node var = nm->mkBoundVar(ss.str(), nm->sExprType());
129 : 591 : d_pfrMap[r] = var;
130 : 591 : return var;
131 : : }
132 : 54 : Node ProofNodeToSExpr::getOrMkKindVariable(TNode n)
133 : : {
134 : : Kind k;
135 [ - + ]: 54 : if (!ProofRuleChecker::getKind(n, k))
136 : : {
137 : : // just use self if we failed to get the node, throw a debug failure
138 : 0 : Assert(false) << "Expected kind node, got " << n;
139 : : return n;
140 : : }
141 : 54 : std::map<Kind, Node>::iterator it = d_kindMap.find(k);
142 [ + + ]: 54 : if (it != d_kindMap.end())
143 : : {
144 : 13 : return it->second;
145 : : }
146 : 82 : std::stringstream ss;
147 : 41 : ss << k;
148 : 41 : NodeManager* nm = NodeManager::currentNM();
149 : 123 : Node var = nm->mkBoundVar(ss.str(), nm->sExprType());
150 : 41 : d_kindMap[k] = var;
151 : 41 : return var;
152 : : }
153 : :
154 : 42 : Node ProofNodeToSExpr::getOrMkTheoryIdVariable(TNode n)
155 : : {
156 : : theory::TheoryId tid;
157 [ - + ]: 42 : if (!theory::builtin::BuiltinProofRuleChecker::getTheoryId(n, tid))
158 : : {
159 : : // just use self if we failed to get the node, throw a debug failure
160 : 0 : Assert(false) << "Expected theory id node, got " << n;
161 : : return n;
162 : : }
163 : 42 : std::map<theory::TheoryId, Node>::iterator it = d_tidMap.find(tid);
164 [ + + ]: 42 : if (it != d_tidMap.end())
165 : : {
166 : 12 : return it->second;
167 : : }
168 : 60 : std::stringstream ss;
169 : 30 : ss << tid;
170 : 30 : NodeManager* nm = NodeManager::currentNM();
171 : 90 : Node var = nm->mkBoundVar(ss.str(), nm->sExprType());
172 : 30 : d_tidMap[tid] = var;
173 : 30 : return var;
174 : : }
175 : :
176 : 42 : Node ProofNodeToSExpr::getOrMkMethodIdVariable(TNode n)
177 : : {
178 : : MethodId mid;
179 [ - + ]: 42 : if (!getMethodId(n, mid))
180 : : {
181 : : // just use self if we failed to get the node, throw a debug failure
182 : 0 : Assert(false) << "Expected method id node, got " << n;
183 : : return n;
184 : : }
185 : 42 : std::map<MethodId, Node>::iterator it = d_midMap.find(mid);
186 [ + + ]: 42 : if (it != d_midMap.end())
187 : : {
188 : 12 : return it->second;
189 : : }
190 : 60 : std::stringstream ss;
191 : 30 : ss << mid;
192 : 30 : NodeManager* nm = NodeManager::currentNM();
193 : 90 : Node var = nm->mkBoundVar(ss.str(), nm->sExprType());
194 : 30 : d_midMap[mid] = var;
195 : 30 : return var;
196 : : }
197 : 0 : Node ProofNodeToSExpr::getOrMkTrustIdVariable(TNode n)
198 : : {
199 : : TrustId tid;
200 [ - - ]: 0 : if (!getTrustId(n, tid))
201 : : {
202 : : // just use self if we failed to get the node, throw a debug failure
203 : 0 : Assert(false) << "Expected trust id node, got " << n;
204 : : return n;
205 : : }
206 : 0 : std::map<TrustId, Node>::iterator it = d_tridMap.find(tid);
207 [ - - ]: 0 : if (it != d_tridMap.end())
208 : : {
209 : 0 : return it->second;
210 : : }
211 : 0 : std::stringstream ss;
212 : 0 : ss << tid;
213 : 0 : NodeManager* nm = NodeManager::currentNM();
214 : 0 : Node var = nm->mkBoundVar(ss.str(), nm->sExprType());
215 : 0 : d_tridMap[tid] = var;
216 : 0 : return var;
217 : : }
218 : 0 : Node ProofNodeToSExpr::getOrMkInferenceIdVariable(TNode n)
219 : : {
220 : : theory::InferenceId iid;
221 [ - - ]: 0 : if (!theory::getInferenceId(n, iid))
222 : : {
223 : : // just use self if we failed to get the node, throw a debug failure
224 : 0 : Assert(false) << "Expected inference id node, got " << n;
225 : : return n;
226 : : }
227 : 0 : std::map<theory::InferenceId, Node>::iterator it = d_iidMap.find(iid);
228 [ - - ]: 0 : if (it != d_iidMap.end())
229 : : {
230 : 0 : return it->second;
231 : : }
232 : 0 : std::stringstream ss;
233 : 0 : ss << iid;
234 : 0 : NodeManager* nm = NodeManager::currentNM();
235 : 0 : Node var = nm->mkBoundVar(ss.str(), nm->sExprType());
236 : 0 : d_iidMap[iid] = var;
237 : 0 : return var;
238 : : }
239 : :
240 : 12 : Node ProofNodeToSExpr::getOrMkDslRewriteVariable(TNode n)
241 : : {
242 : : ProofRewriteRule rid;
243 [ - + ]: 12 : if (!rewriter::getRewriteRule(n, rid))
244 : : {
245 : : // just use self if we failed to get the node, throw a debug failure
246 : 0 : Assert(false) << "Expected inference id node, got " << n;
247 : : return n;
248 : : }
249 : 12 : std::map<ProofRewriteRule, Node>::iterator it = d_dslrMap.find(rid);
250 [ + + ]: 12 : if (it != d_dslrMap.end())
251 : : {
252 : 3 : return it->second;
253 : : }
254 : 18 : std::stringstream ss;
255 : 9 : ss << rid;
256 : 9 : NodeManager* nm = NodeManager::currentNM();
257 : 27 : Node var = nm->mkBoundVar(ss.str(), nm->sExprType());
258 : 9 : d_dslrMap[rid] = var;
259 : 9 : return var;
260 : : }
261 : :
262 : 0 : Node ProofNodeToSExpr::getOrMkNodeVariable(TNode n)
263 : : {
264 : 0 : std::map<TNode, Node>::iterator it = d_nodeMap.find(n);
265 [ - - ]: 0 : if (it != d_nodeMap.end())
266 : : {
267 : 0 : return it->second;
268 : : }
269 : 0 : std::stringstream ss;
270 : 0 : ss << n;
271 : 0 : NodeManager* nm = NodeManager::currentNM();
272 : 0 : Node var = nm->mkBoundVar(ss.str(), nm->sExprType());
273 : 0 : d_nodeMap[n] = var;
274 : 0 : return var;
275 : : }
276 : :
277 : 2465 : Node ProofNodeToSExpr::getArgument(Node arg, ArgFormat f)
278 : : {
279 [ + + ][ + - ]: 2465 : switch (f)
[ - + ][ - + ]
280 : : {
281 : 54 : case ArgFormat::KIND: return getOrMkKindVariable(arg);
282 : 42 : case ArgFormat::THEORY_ID: return getOrMkTheoryIdVariable(arg);
283 : 42 : case ArgFormat::METHOD_ID: return getOrMkMethodIdVariable(arg);
284 : 0 : case ArgFormat::TRUST_ID: return getOrMkTrustIdVariable(arg);
285 : 0 : case ArgFormat::INFERENCE_ID: return getOrMkInferenceIdVariable(arg);
286 : 12 : case ArgFormat::DSL_REWRITE_ID: return getOrMkDslRewriteVariable(arg);
287 : 0 : case ArgFormat::NODE_VAR: return getOrMkNodeVariable(arg);
288 : 2315 : default: return arg;
289 : : }
290 : : }
291 : :
292 : 2465 : ProofNodeToSExpr::ArgFormat ProofNodeToSExpr::getArgumentFormat(
293 : : const ProofNode* pn, size_t i)
294 : : {
295 : 2465 : ProofRule r = pn->getRule();
296 [ + - ][ - + ]: 2465 : switch (r)
[ + - ][ - + ]
297 : : {
298 : 54 : case ProofRule::CONG:
299 : : case ProofRule::NARY_CONG:
300 : : {
301 [ + - ]: 54 : if (i == 0)
302 : : {
303 : 54 : return ArgFormat::KIND;
304 : : }
305 : 0 : const std::vector<Node>& args = pn->getArguments();
306 : 0 : Assert(i < args.size());
307 : 0 : if (args[i].getNumChildren() == 0
308 : 0 : && NodeManager::operatorToKind(args[i]) != Kind::UNDEFINED_KIND)
309 : : {
310 : 0 : return ArgFormat::NODE_VAR;
311 : : }
312 : : }
313 : 0 : break;
314 : 0 : case ProofRule::SUBS:
315 : : case ProofRule::MACRO_REWRITE:
316 : : case ProofRule::MACRO_SR_EQ_INTRO:
317 : : case ProofRule::MACRO_SR_PRED_INTRO:
318 : : case ProofRule::MACRO_SR_PRED_TRANSFORM:
319 [ - - ]: 0 : if (i > 0)
320 : : {
321 : 0 : return ArgFormat::METHOD_ID;
322 : : }
323 : 0 : break;
324 : 0 : case ProofRule::MACRO_SR_PRED_ELIM: return ArgFormat::METHOD_ID; break;
325 : 126 : case ProofRule::TRUST_THEORY_REWRITE:
326 [ + + ]: 126 : if (i == 1)
327 : : {
328 : 42 : return ArgFormat::THEORY_ID;
329 : : }
330 [ + + ]: 84 : else if (i == 2)
331 : : {
332 : 42 : return ArgFormat::METHOD_ID;
333 : : }
334 : 42 : break;
335 : 32 : case ProofRule::DSL_REWRITE:
336 : : case ProofRule::THEORY_REWRITE:
337 [ + + ]: 32 : if (i == 0)
338 : : {
339 : 12 : return ArgFormat::DSL_REWRITE_ID;
340 : : }
341 : 20 : break;
342 : 0 : case ProofRule::INSTANTIATE:
343 : : {
344 [ - - ]: 0 : if (i == 1)
345 : : {
346 : 0 : return ArgFormat::INFERENCE_ID;
347 : : }
348 : : }
349 : 0 : break;
350 : 0 : case ProofRule::TRUST:
351 : : {
352 [ - - ]: 0 : if (i == 0)
353 : : {
354 : 0 : return ArgFormat::TRUST_ID;
355 : : }
356 [ - - ]: 0 : else if (i == 2)
357 : : {
358 : : TrustId tid;
359 : 0 : getTrustId(pn->getArguments()[0], tid);
360 [ - - ][ - - ]: 0 : if (tid == TrustId::THEORY_LEMMA || tid == TrustId::THEORY_INFERENCE)
361 : : {
362 : 0 : return ArgFormat::THEORY_ID;
363 : : }
364 : : }
365 : : }
366 : 0 : break;
367 : 2253 : default: break;
368 : : }
369 : 2315 : return ArgFormat::DEFAULT;
370 : : }
371 : :
372 : : } // namespace cvc5::internal
|
