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