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