Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Haniel Barbosa, Daniel Larraz, Andrew Reynolds
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 Alethe node conversion
14 : : */
15 : :
16 : : #include "proof/alethe/alethe_node_converter.h"
17 : :
18 : : #include "expr/dtype.h"
19 : : #include "expr/node_algorithm.h"
20 : : #include "expr/skolem_manager.h"
21 : : #include "proof/proof_rule_checker.h"
22 : : #include "util/bitvector.h"
23 : : #include "util/rational.h"
24 : :
25 : : namespace cvc5::internal {
26 : : namespace proof {
27 : :
28 : 7677130 : Node AletheNodeConverter::maybeConvert(Node n, bool isAssumption)
29 : : {
30 : 7677130 : d_error = "";
31 : 15354300 : Node res = convert(n);
32 [ + + ]: 7677130 : if (!d_error.empty())
33 : : {
34 : 921 : return Node::null();
35 : : }
36 [ + + ]: 7676210 : if (isAssumption)
37 : : {
38 : 12190 : d_convToOriginalAssumption[res] = n;
39 : : }
40 : 7676210 : return res;
41 : : }
42 : :
43 : 2930120 : Node AletheNodeConverter::postConvert(Node n)
44 : : {
45 : 2930120 : Kind k = n.getKind();
46 [ + - ]: 5860230 : Trace("alethe-conv") << "AletheNodeConverter: convert " << n << ", kind " << k
47 : 2930120 : << "\n";
48 [ + + ][ + + ]: 2930120 : switch (k)
[ + + ][ + + ]
[ + + ][ + + ]
49 : : {
50 : 9462 : case Kind::BITVECTOR_BIT:
51 : : {
52 : 18924 : std::stringstream ss;
53 : 18924 : ss << "(_ @bitOf " << n.getOperator().getConst<BitVectorBit>().d_bitIndex
54 : 9462 : << ")";
55 : 28386 : TypeNode fType = d_nm->mkFunctionType(n[0].getType(), n.getType());
56 : 28386 : Node op = mkInternalSymbol(ss.str(), fType, true);
57 : 28386 : Node converted = d_nm->mkNode(Kind::APPLY_UF, op, n[0]);
58 : 9462 : return converted;
59 : : }
60 : 4138 : case Kind::BITVECTOR_FROM_BOOLS:
61 : : {
62 : 8276 : std::vector<Node> children;
63 : 8276 : std::vector<TypeNode> childrenTypes;
64 [ + + ]: 48762 : for (const Node& c : n)
65 : : {
66 : 44624 : childrenTypes.push_back(c.getType());
67 : 44624 : children.push_back(c);
68 : : }
69 : 8276 : TypeNode fType = d_nm->mkFunctionType(childrenTypes, n.getType());
70 : 12414 : Node op = mkInternalSymbol("@bbT", fType, true);
71 : 4138 : children.insert(children.begin(), op);
72 : 8276 : Node converted = d_nm->mkNode(Kind::APPLY_UF, children);
73 : 4138 : return converted;
74 : : }
75 : 4 : case Kind::BITVECTOR_EAGER_ATOM:
76 : : {
77 : 4 : return n[0];
78 : : }
79 : 7 : case Kind::DIVISION_TOTAL:
80 : : {
81 : 7 : return d_nm->mkNode(Kind::DIVISION, n[0], n[1]);
82 : : }
83 : 289 : case Kind::INTS_DIVISION_TOTAL:
84 : : {
85 : 289 : return d_nm->mkNode(Kind::INTS_DIVISION, n[0], n[1]);
86 : : }
87 : 125 : case Kind::INTS_MODULUS_TOTAL:
88 : : {
89 : 125 : return d_nm->mkNode(Kind::INTS_MODULUS, n[0], n[1]);
90 : : }
91 : 3526 : case Kind::SKOLEM:
92 : : {
93 [ + - ]: 7052 : Trace("alethe-conv") << "AletheNodeConverter: handling skolem " << n
94 : 3526 : << "\n";
95 : 3526 : SkolemManager* sm = d_nm->getSkolemManager();
96 : 3526 : SkolemId sfi = SkolemId::NONE;
97 : 7052 : Node cacheVal;
98 : 3526 : sm->isSkolemFunction(n, sfi, cacheVal);
99 : : // skolems v print as their original forms
100 : : // v is (skolem W) where W is the original or original form of v
101 : 7052 : Node wi = SkolemManager::getUnpurifiedForm(n);
102 [ + - ][ + + ]: 3526 : if (!wi.isNull() && wi != n)
[ + + ]
103 : : {
104 [ + - ]: 6218 : Trace("alethe-conv")
105 : 3109 : << "...to convert original form " << wi << std::endl;
106 : 6218 : Node conv = convert(wi);
107 : : // ignore purification skolems
108 [ - + ]: 3109 : if (sfi != SkolemId::PURIFY)
109 : : {
110 : 0 : d_skolems[n] = conv;
111 : : }
112 : 3109 : return conv;
113 : : }
114 : : // create the witness term (witness ((x_i T_i)) (exists ((x_i+1 T_i+1)
115 : : // ... (x_n T_n)) body), where the bound variables and the body come from
116 : : // the quantifier term which must be the first element of cacheVal (which
117 : : // should be a list), and i the second.
118 [ + + ]: 417 : if (sfi == SkolemId::QUANTIFIERS_SKOLEMIZE)
119 : : {
120 [ + - ]: 522 : Trace("alethe-conv")
121 [ - - ]: 261 : << ".. to build witness with index/quant: " << cacheVal[1] << " / "
122 [ - + ][ - + ]: 261 : << cacheVal[0] << "\n";
[ - - ]
123 [ + - ][ + - ]: 522 : Assert(cacheVal.getKind() == Kind::SEXPR
[ - + ][ - - ]
124 : : && cacheVal.getNumChildren() == 2);
125 : 522 : Node quant = cacheVal[0];
126 [ - + ][ - + ]: 261 : Assert(quant.getKind() == Kind::FORALL);
[ - - ]
127 : 261 : uint32_t index = -1;
128 : 261 : ProofRuleChecker::getUInt32(cacheVal[1], index);
129 [ - + ][ - + ]: 261 : Assert(index < quant[0].getNumChildren());
[ - - ]
130 : 522 : Node var = quant[0][index];
131 : : // Since cvc5 *always* skolemize FORALLs, we generate the choice term
132 : : // assuming it is gonna be introduced via a sko_forall rule, in which
133 : : // case the body of the choice is negated, which means to have
134 : : // universal quantification of the remaining variables in the choice
135 : : // body, and the whole thing negated. Likewise, since during
136 : : // Skolemization cvc5 will have negated the body of the original
137 : : // quantifier, we need to revert that as well.
138 : : Node body =
139 : 261 : (index == quant[0].getNumChildren() - 1
140 : 1027 : ? quant[1]
141 : : : d_nm->mkNode(Kind::FORALL,
142 [ + + ][ - - ]: 383 : d_nm->mkNode(Kind::BOUND_VAR_LIST,
143 : 749 : std::vector<Node>{
144 [ + + ][ + + ]: 505 : quant[0].begin() + index + 1,
[ - - ]
145 : : quant[0].end()}),
146 : : quant[1]))
147 : 522 : .notNode();
148 : : // we need to replace in the body all the free variables (i.e., from 0
149 : : // to index) by their respective choice terms. To do this, we get
150 : : // the skolems for each of these variables, retrieve their
151 : : // conversions, and replace the variables by the conversions in body
152 [ + + ]: 261 : if (index > 0)
153 : : {
154 : 114 : std::vector<Node> subs;
155 [ + + ]: 619 : for (size_t i = 0; i < index; ++i)
156 : : {
157 : 3030 : std::vector<Node> cacheVals{quant, d_nm->mkConstInt(Rational(i))};
158 : : Node sk = sm->mkSkolemFunction(SkolemId::QUANTIFIERS_SKOLEMIZE,
159 : 505 : cacheVals);
160 [ - + ][ - + ]: 505 : Assert(!sk.isNull());
[ - - ]
161 [ - + ][ + - ]: 505 : subs.push_back(d_defineSkolems ? sk : convert(sk));
[ - - ]
162 : : }
163 : 342 : body = body.substitute(quant[0].begin(),
164 : 228 : quant[0].begin() + index,
165 : : subs.begin(),
166 : 114 : subs.end());
167 : : }
168 : : Node witness = d_nm->mkNode(
169 : 783 : Kind::WITNESS, d_nm->mkNode(Kind::BOUND_VAR_LIST, var), body);
170 [ + - ]: 261 : Trace("alethe-conv") << ".. witness: " << witness << "\n";
171 : 261 : witness = convert(witness);
172 [ - + ]: 261 : if (d_defineSkolems)
173 : : {
174 : 0 : d_skolemsAux[n] = witness;
175 [ - - ]: 0 : if (index == quant[0].getNumChildren() - 1)
176 : : {
177 [ - - ]: 0 : Trace("alethe-conv")
178 : 0 : << "....populate map from aux : " << d_skolemsAux << "\n";
179 [ - - ]: 0 : for (size_t i = index + 1; i > 0; --i)
180 : : {
181 : : std::vector<Node> cacheVals{quant,
182 : 0 : d_nm->mkConstInt(Rational(i - 1))};
183 : : Node sk = sm->mkSkolemFunction(SkolemId::QUANTIFIERS_SKOLEMIZE,
184 : 0 : cacheVals);
185 : 0 : Assert(!sk.isNull());
186 : 0 : Assert(d_skolemsAux.find(sk) != d_skolemsAux.end())
187 : 0 : << "Could not find sk " << sk;
188 : 0 : d_skolems[sk] = d_skolemsAux[sk];
189 : : }
190 : 0 : d_skolemsAux.clear();
191 : : }
192 : 0 : return n;
193 : : }
194 : 261 : d_skolems[n] = witness;
195 : 261 : return witness;
196 : : }
197 : 312 : std::stringstream ss;
198 : 156 : ss << "\"Proof unsupported by Alethe: contains Skolem (kind " << sfi
199 : 156 : << ", term " << n << "\"";
200 : 156 : d_error = ss.str();
201 : 156 : return Node::null();
202 : : }
203 : 13593 : case Kind::FORALL:
204 : : {
205 : : // remove patterns, if any
206 : 13593 : return n.getNumChildren() == 3 ? d_nm->mkNode(Kind::FORALL, n[0], n[1])
207 : 13593 : : n;
208 : : }
209 : : // we must make it to be printed with "choice", so we create an operator
210 : : // with that name and the correct type and do a function application
211 : 261 : case Kind::WITNESS:
212 : : {
213 : 522 : std::vector<TypeNode> childrenTypes;
214 [ + + ]: 783 : for (const Node& c : n)
215 : : {
216 : 522 : childrenTypes.push_back(c.getType());
217 : : }
218 : 522 : TypeNode fType = d_nm->mkFunctionType(childrenTypes, n.getType());
219 : 783 : Node choiceOp = mkInternalSymbol("choice", fType);
220 : 783 : Node converted = d_nm->mkNode(Kind::APPLY_UF, choiceOp, n[0], n[1]);
221 [ + - ]: 261 : Trace("alethe-conv") << ".. converted to choice: " << converted << "\n";
222 : 261 : return converted;
223 : : }
224 : : // other handled kinds but no-op in conversion. Everything else is
225 : : // unsupported
226 : : /* from builtin */
227 : 2872480 : case Kind::SORT_TYPE:
228 : : case Kind::INSTANTIATED_SORT_TYPE:
229 : : case Kind::UNINTERPRETED_SORT_VALUE:
230 : : case Kind::BUILTIN:
231 : : case Kind::EQUAL:
232 : : case Kind::DISTINCT:
233 : : case Kind::SEXPR:
234 : : case Kind::TYPE_CONSTANT:
235 : : case Kind::RAW_SYMBOL:
236 : : /* from booleans */
237 : : case Kind::CONST_BOOLEAN:
238 : : case Kind::NOT:
239 : : case Kind::AND:
240 : : case Kind::IMPLIES:
241 : : case Kind::OR:
242 : : case Kind::XOR:
243 : : case Kind::ITE:
244 : : /* from uf */
245 : : case Kind::APPLY_UF:
246 : : case Kind::FUNCTION_TYPE:
247 : : case Kind::LAMBDA:
248 : : case Kind::HO_APPLY:
249 : : case Kind::FUNCTION_ARRAY_CONST:
250 : : case Kind::BITVECTOR_TO_NAT:
251 : : case Kind::INT_TO_BITVECTOR_OP:
252 : : case Kind::INT_TO_BITVECTOR:
253 : : /* from arith */
254 : : case Kind::ADD:
255 : : case Kind::MULT:
256 : : case Kind::NONLINEAR_MULT:
257 : : case Kind::SUB:
258 : : case Kind::NEG:
259 : : case Kind::DIVISION:
260 : : case Kind::INTS_DIVISION:
261 : : case Kind::INTS_MODULUS:
262 : : case Kind::ABS:
263 : : case Kind::DIVISIBLE:
264 : : case Kind::DIVISIBLE_OP:
265 : : case Kind::CONST_RATIONAL:
266 : : case Kind::CONST_INTEGER:
267 : : case Kind::LT:
268 : : case Kind::LEQ:
269 : : case Kind::GT:
270 : : case Kind::GEQ:
271 : : case Kind::IS_INTEGER:
272 : : case Kind::TO_INTEGER:
273 : : case Kind::TO_REAL:
274 : : /* from BV */
275 : : case Kind::BITVECTOR_TYPE:
276 : : case Kind::CONST_BITVECTOR:
277 : : case Kind::BITVECTOR_SIZE:
278 : : case Kind::CONST_BITVECTOR_SYMBOLIC:
279 : : case Kind::BITVECTOR_CONCAT:
280 : : case Kind::BITVECTOR_AND:
281 : : case Kind::BITVECTOR_COMP:
282 : : case Kind::BITVECTOR_OR:
283 : : case Kind::BITVECTOR_XOR:
284 : : case Kind::BITVECTOR_NOT:
285 : : case Kind::BITVECTOR_NAND:
286 : : case Kind::BITVECTOR_NOR:
287 : : case Kind::BITVECTOR_XNOR:
288 : : case Kind::BITVECTOR_MULT:
289 : : case Kind::BITVECTOR_NEG:
290 : : case Kind::BITVECTOR_ADD:
291 : : case Kind::BITVECTOR_SUB:
292 : : case Kind::BITVECTOR_UDIV:
293 : : case Kind::BITVECTOR_UREM:
294 : : case Kind::BITVECTOR_SDIV:
295 : : case Kind::BITVECTOR_SMOD:
296 : : case Kind::BITVECTOR_SREM:
297 : : case Kind::BITVECTOR_ASHR:
298 : : case Kind::BITVECTOR_LSHR:
299 : : case Kind::BITVECTOR_SHL:
300 : : case Kind::BITVECTOR_ULE:
301 : : case Kind::BITVECTOR_ULT:
302 : : case Kind::BITVECTOR_UGE:
303 : : case Kind::BITVECTOR_UGT:
304 : : case Kind::BITVECTOR_SLE:
305 : : case Kind::BITVECTOR_SLT:
306 : : case Kind::BITVECTOR_SGE:
307 : : case Kind::BITVECTOR_SGT:
308 : : case Kind::BITVECTOR_ULTBV:
309 : : case Kind::BITVECTOR_SLTBV:
310 : : case Kind::BITVECTOR_ACKERMANNIZE_UDIV:
311 : : case Kind::BITVECTOR_ACKERMANNIZE_UREM:
312 : : case Kind::BITVECTOR_BIT_OP:
313 : : case Kind::BITVECTOR_EXTRACT_OP:
314 : : case Kind::BITVECTOR_EXTRACT:
315 : : case Kind::BITVECTOR_REPEAT_OP:
316 : : case Kind::BITVECTOR_REPEAT:
317 : : case Kind::BITVECTOR_ROTATE_LEFT_OP:
318 : : case Kind::BITVECTOR_ROTATE_LEFT:
319 : : case Kind::BITVECTOR_ROTATE_RIGHT_OP:
320 : : case Kind::BITVECTOR_ROTATE_RIGHT:
321 : : case Kind::BITVECTOR_SIGN_EXTEND_OP:
322 : : case Kind::BITVECTOR_SIGN_EXTEND:
323 : : case Kind::BITVECTOR_ZERO_EXTEND_OP:
324 : : case Kind::BITVECTOR_ZERO_EXTEND:
325 : : /* from arrays */
326 : : case Kind::ARRAY_TYPE:
327 : : case Kind::SELECT:
328 : : case Kind::STORE:
329 : : case Kind::STORE_ALL:
330 : : case Kind::ARRAY_LAMBDA:
331 : : /* from datatypes */
332 : : case Kind::CONSTRUCTOR_TYPE:
333 : : case Kind::SELECTOR_TYPE:
334 : : case Kind::TESTER_TYPE:
335 : : case Kind::APPLY_CONSTRUCTOR:
336 : : case Kind::APPLY_SELECTOR:
337 : : case Kind::APPLY_TESTER:
338 : : case Kind::DATATYPE_TYPE:
339 : : case Kind::PARAMETRIC_DATATYPE:
340 : : case Kind::TUPLE_TYPE:
341 : : case Kind::APPLY_TYPE_ASCRIPTION:
342 : : case Kind::ASCRIPTION_TYPE:
343 : : case Kind::DT_SIZE:
344 : : case Kind::DT_HEIGHT_BOUND:
345 : : case Kind::DT_SIZE_BOUND:
346 : : case Kind::MATCH:
347 : : case Kind::MATCH_CASE:
348 : : case Kind::MATCH_BIND_CASE:
349 : : /* from strings */
350 : : case Kind::STRING_CONCAT:
351 : : case Kind::STRING_IN_REGEXP:
352 : : case Kind::STRING_LENGTH:
353 : : case Kind::STRING_SUBSTR:
354 : : case Kind::STRING_CHARAT:
355 : : case Kind::STRING_CONTAINS:
356 : : case Kind::STRING_LT:
357 : : case Kind::STRING_LEQ:
358 : : case Kind::STRING_INDEXOF:
359 : : case Kind::STRING_REPLACE:
360 : : case Kind::STRING_REPLACE_ALL:
361 : : case Kind::STRING_REPLACE_RE:
362 : : case Kind::STRING_REPLACE_RE_ALL:
363 : : case Kind::STRING_PREFIX:
364 : : case Kind::STRING_SUFFIX:
365 : : case Kind::STRING_IS_DIGIT:
366 : : case Kind::STRING_ITOS:
367 : : case Kind::STRING_STOI:
368 : : case Kind::STRING_TO_CODE:
369 : : case Kind::STRING_FROM_CODE:
370 : : case Kind::STRING_UNIT:
371 : : case Kind::CONST_STRING:
372 : : case Kind::STRING_TO_REGEXP:
373 : : case Kind::REGEXP_CONCAT:
374 : : case Kind::REGEXP_UNION:
375 : : case Kind::REGEXP_INTER:
376 : : case Kind::REGEXP_DIFF:
377 : : case Kind::REGEXP_STAR:
378 : : case Kind::REGEXP_PLUS:
379 : : case Kind::REGEXP_OPT:
380 : : case Kind::REGEXP_RANGE:
381 : : case Kind::REGEXP_COMPLEMENT:
382 : : case Kind::REGEXP_NONE:
383 : : case Kind::REGEXP_ALL:
384 : : case Kind::REGEXP_ALLCHAR:
385 : : case Kind::REGEXP_REPEAT_OP:
386 : : case Kind::REGEXP_REPEAT:
387 : : case Kind::REGEXP_LOOP_OP:
388 : : case Kind::REGEXP_LOOP:
389 : : case Kind::REGEXP_RV:
390 : : /* from quantifiers */
391 : : case Kind::EXISTS:
392 : : case Kind::BOUND_VAR_LIST:
393 : : case Kind::INST_PATTERN:
394 : : case Kind::INST_NO_PATTERN:
395 : : case Kind::INST_ATTRIBUTE:
396 : : case Kind::INST_POOL:
397 : : case Kind::INST_ADD_TO_POOL:
398 : : case Kind::SKOLEM_ADD_TO_POOL:
399 : : case Kind::INST_PATTERN_LIST:
400 : : {
401 : 2872480 : return n;
402 : : }
403 : 24150 : case Kind::BOUND_VARIABLE:
404 : : case Kind::VARIABLE:
405 : : {
406 : : // see if variable has a supported type. We need this check because in
407 : : // some problems involving unsupported theories there are no operators,
408 : : // just variables of unsupported type
409 : 48300 : TypeNode tn = n.getType();
410 : 24150 : Kind tnk = tn.getKind();
411 [ + + ]: 24150 : switch (tnk)
412 : : {
413 : 9213 : case Kind::SORT_TYPE:
414 : : case Kind::INSTANTIATED_SORT_TYPE:
415 : : case Kind::FUNCTION_TYPE:
416 : : case Kind::BITVECTOR_TYPE:
417 : : case Kind::ARRAY_TYPE:
418 : : case Kind::CONSTRUCTOR_TYPE:
419 : : case Kind::SELECTOR_TYPE:
420 : : case Kind::TESTER_TYPE:
421 : : case Kind::ASCRIPTION_TYPE:
422 : : {
423 : 9213 : return n;
424 : : }
425 : 14937 : default:
426 : : {
427 : : // The supported constant types
428 [ + + ]: 14937 : if (tnk == Kind::TYPE_CONSTANT)
429 : : {
430 [ + + ]: 14153 : switch (tn.getConst<TypeConstant>())
431 : : {
432 : 14149 : case TypeConstant::SEXPR_TYPE:
433 : : case TypeConstant::BOOLEAN_TYPE:
434 : : case TypeConstant::REAL_TYPE:
435 : : case TypeConstant::INTEGER_TYPE:
436 : : case TypeConstant::STRING_TYPE:
437 : : case TypeConstant::REGEXP_TYPE:
438 : : {
439 : 14149 : return n;
440 : : }
441 : 4 : default: // fallthrough to the error handling below
442 : 4 : break;
443 : : }
444 : : }
445 : : // Only regular datatypes (parametric or not) are supported
446 [ + + ]: 1192 : else if (tn.isDatatype() && !tn.getDType().isCodatatype()
447 [ + + ][ + + ]: 1252 : && (tnk == Kind::DATATYPE_TYPE
[ + + ]
448 [ + + ]: 60 : || tnk == Kind::PARAMETRIC_DATATYPE))
449 : : {
450 : 356 : return n;
451 : : }
452 [ + - ]: 432 : Trace("alethe-conv") << "AletheNodeConverter: ...unsupported type\n";
453 : 864 : std::stringstream ss;
454 : 432 : ss << "\"Proof unsupported by Alethe: contains ";
455 [ + + ]: 432 : if (tnk == Kind::TYPE_CONSTANT)
456 : : {
457 : 4 : ss << tn.getConst<TypeConstant>();
458 : : }
459 [ + + ]: 428 : else if (tn.isDatatype())
460 : : {
461 : 52 : ss << "non-standard datatype";
462 : : }
463 : : else
464 : : {
465 : 376 : ss << tnk;
466 : : }
467 : 432 : ss << "\"";
468 : 432 : d_error = ss.str();
469 : 432 : return Node::null();
470 : : }
471 : : }
472 : : }
473 : 2084 : default:
474 : : {
475 [ + - ]: 2084 : Trace("alethe-conv") << "AletheNodeConverter: ...unsupported kind\n";
476 : 4168 : std::stringstream ss;
477 : 2084 : ss << "\"Proof unsupported by Alethe: contains operator " << k << "\"";
478 : 2084 : d_error = ss.str();
479 : 2084 : return Node::null();
480 : : }
481 : : }
482 : : return n;
483 : : }
484 : :
485 : 13861 : Node AletheNodeConverter::mkInternalSymbol(const std::string& name,
486 : : TypeNode tn,
487 : : bool useRawSym)
488 : : {
489 : 27722 : std::pair<TypeNode, std::string> key(tn, name);
490 : : std::map<std::pair<TypeNode, std::string>, Node>::iterator it =
491 : 13861 : d_symbolsMap.find(key);
492 [ + + ]: 13861 : if (it != d_symbolsMap.end())
493 : : {
494 : 10454 : return it->second;
495 : : }
496 : : Node sym = useRawSym ? NodeManager::mkRawSymbol(name, tn)
497 [ + - ]: 6814 : : NodeManager::mkBoundVar(name, tn);
498 : 3407 : d_symbolsMap[key] = sym;
499 : 3407 : return sym;
500 : : }
501 : :
502 : 0 : Node AletheNodeConverter::mkInternalSymbol(const std::string& name)
503 : : {
504 : 0 : return mkInternalSymbol(name, d_nm->sExprType());
505 : : }
506 : :
507 : 920 : const std::string& AletheNodeConverter::getError() { return d_error; }
508 : :
509 : 22162 : Node AletheNodeConverter::getOriginalAssumption(Node n)
510 : : {
511 : 22162 : auto it = d_convToOriginalAssumption.find(n);
512 [ + - ]: 22162 : if (it != d_convToOriginalAssumption.end())
513 : : {
514 : 22162 : return it->second;
515 : : }
516 : 0 : return n;
517 : : }
518 : :
519 : 73 : const std::map<Node, Node>& AletheNodeConverter::getSkolemDefinitions()
520 : : {
521 : 73 : return d_skolems;
522 : : }
523 : :
524 : : } // namespace proof
525 : : } // namespace cvc5::internal
|
