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 : 4442597 : Node AletheNodeConverter::maybeConvert(Node n, bool isAssumption)
27 : : {
28 : 4442597 : d_error = "";
29 : 4442597 : Node res = convert(n);
30 [ + + ]: 4442597 : if (!d_error.empty())
31 : : {
32 : 1949 : return Node::null();
33 : : }
34 [ + + ]: 4440648 : if (isAssumption)
35 : : {
36 : 11548 : d_convToOriginalAssumption[res] = n;
37 : : }
38 : 4440648 : return res;
39 : 4442597 : }
40 : :
41 : 21988 : void collectTypes(std::vector<TypeNode>& allTypesVec,
42 : : std::unordered_set<TypeNode>& allTypes)
43 : : {
44 [ + + ]: 50651 : for (size_t i = 0, size = allTypesVec.size(); i < size; ++i)
45 : : {
46 : 28663 : TypeNode tn = allTypesVec[i];
47 : : // Must additionally get the subfield types from datatypes.
48 [ + + ]: 28663 : if (tn.isDatatype())
49 : : {
50 : 766 : const DType& dt = tn.getDType();
51 : 766 : std::unordered_set<TypeNode> sftypes = dt.getSubfieldTypes();
52 : 766 : std::unordered_set<TypeNode> sfctypes;
53 : : // get the component types of each of the subfield types
54 [ + + ]: 1827 : for (const TypeNode& sft : sftypes)
55 : : {
56 : : // as an optimization, if we've already considered this type, don't
57 : : // have to find its component types
58 [ + + ]: 1061 : if (allTypes.find(sft) == allTypes.end())
59 : : {
60 : 477 : expr::getComponentTypes(sft, sfctypes);
61 : : }
62 : : }
63 [ + + ]: 1283 : for (const TypeNode& sft : sfctypes)
64 : : {
65 [ + + ]: 517 : if (allTypes.find(sft) == allTypes.end())
66 : : {
67 : 507 : allTypesVec.emplace_back(sft);
68 : 507 : allTypes.insert(sft);
69 : : }
70 : : }
71 : 766 : }
72 : 28663 : }
73 : 21988 : }
74 : :
75 : 22003 : Node AletheNodeConverter::recordUnsupportedKind(Kind k)
76 : : {
77 [ + - ]: 22003 : Trace("alethe-conv") << "AletheNodeConverter: ...unsupported kind\n";
78 : 22003 : std::stringstream ss;
79 : 22003 : ss << "\"Proof unsupported by Alethe: contains operator " << k << "\"";
80 : 22003 : d_error = ss.str();
81 : 44006 : return Node::null();
82 : 22003 : }
83 : :
84 : 1910426 : Node AletheNodeConverter::postConvert(Node n)
85 : : {
86 : 1910426 : Kind k = n.getKind();
87 [ + - ]: 3820852 : Trace("alethe-conv") << "AletheNodeConverter: convert " << n << ", kind " << k
88 : 1910426 : << "\n";
89 [ + - ][ - + ]: 1910426 : switch (k)
[ + + ][ + + ]
[ + + ][ + + ]
[ + ]
90 : : {
91 : 352 : case Kind::BITVECTOR_BIT:
92 : : {
93 [ + - ]: 352 : if (d_isTesting)
94 : : {
95 : 352 : return recordUnsupportedKind(k);
96 : : }
97 : 0 : std::stringstream ss;
98 : 0 : ss << "(_ @bit_of " << n.getOperator().getConst<BitVectorBit>().d_bitIndex
99 : 0 : << ")";
100 : : // Use n0Type to ensure deterministic node ID assignments
101 : 0 : TypeNode n0Type = n[0].getType();
102 : 0 : TypeNode fType = d_nm->mkFunctionType(n0Type, n.getType());
103 : 0 : Node op = mkInternalSymbol(ss.str(), fType, true);
104 : 0 : Node converted = d_nm->mkNode(Kind::APPLY_UF, op, n[0]);
105 : 0 : return converted;
106 : 0 : }
107 : 0 : case Kind::BITVECTOR_FROM_BOOLS:
108 : : {
109 [ - - ]: 0 : if (d_isTesting)
110 : : {
111 : 0 : return recordUnsupportedKind(k);
112 : : }
113 : 0 : std::vector<Node> children;
114 : 0 : std::vector<TypeNode> childrenTypes;
115 [ - - ]: 0 : for (const Node& c : n)
116 : : {
117 : 0 : childrenTypes.push_back(c.getType());
118 : 0 : children.push_back(c);
119 : 0 : }
120 : 0 : TypeNode fType = d_nm->mkFunctionType(childrenTypes, n.getType());
121 : 0 : Node op = mkInternalSymbol("@bbterm", fType, true);
122 : 0 : children.insert(children.begin(), op);
123 : 0 : Node converted = d_nm->mkNode(Kind::APPLY_UF, children);
124 : 0 : return converted;
125 : 0 : }
126 : 0 : case Kind::BITVECTOR_EAGER_ATOM:
127 : : {
128 [ - - ]: 0 : if (d_isTesting)
129 : : {
130 : 0 : return recordUnsupportedKind(k);
131 : : }
132 : 0 : return n[0];
133 : : }
134 : 14 : case Kind::DIVISION_TOTAL:
135 : : {
136 : 14 : return d_nm->mkNode(Kind::DIVISION, n[0], n[1]);
137 : : }
138 : 117 : case Kind::INTS_DIVISION_TOTAL:
139 : : {
140 : 117 : return d_nm->mkNode(Kind::INTS_DIVISION, n[0], n[1]);
141 : : }
142 : 67 : case Kind::INTS_MODULUS_TOTAL:
143 : : {
144 : 67 : return d_nm->mkNode(Kind::INTS_MODULUS, n[0], n[1]);
145 : : }
146 : 1681 : case Kind::SKOLEM:
147 : : {
148 [ + - ]: 3362 : Trace("alethe-conv") << "AletheNodeConverter: handling skolem " << n
149 : 1681 : << "\n";
150 : 1681 : SkolemManager* sm = d_nm->getSkolemManager();
151 : 1681 : SkolemId sfi = SkolemId::NONE;
152 : 1681 : Node cacheVal;
153 : 1681 : sm->isSkolemFunction(n, sfi, cacheVal);
154 : : // skolems v print as their original forms
155 : : // v is (skolem W) where W is the original or original form of v
156 : 1681 : Node wi = SkolemManager::getUnpurifiedForm(n);
157 [ + - ][ + + ]: 1681 : if (!wi.isNull() && wi != n)
[ + + ]
158 : : {
159 [ + - ]: 2552 : Trace("alethe-conv")
160 : 1276 : << "...to convert original form " << wi << std::endl;
161 : 1276 : Node conv = convert(wi);
162 : : // ignore purification skolems
163 [ - + ]: 1276 : if (sfi != SkolemId::PURIFY)
164 : : {
165 : 0 : d_skolemsList.push_back(n);
166 : 0 : d_skolems[n] = conv;
167 : : }
168 : 1276 : return conv;
169 : 1276 : }
170 [ + + ]: 405 : if (sfi == SkolemId::QUANTIFIERS_SKOLEMIZE)
171 : : {
172 : : // create the witness term
173 : : //
174 : : // (witness ((x_i T_i)) (exists ((x_i+1 T_i+1) ... (x_n T_n)) body))
175 : : //
176 : : // where the bound variables and the body come from the quantifier term
177 : : // which must be the first element of cacheVal (which should be a list),
178 : : // and i the second.
179 [ + - ]: 520 : Trace("alethe-conv")
180 [ - - ]: 260 : << ".. to build witness with index/quant: " << cacheVal[1] << " / "
181 [ - + ][ - + ]: 260 : << cacheVal[0] << "\n";
[ - - ]
182 [ + - ][ + - ]: 260 : Assert(cacheVal.getKind() == Kind::SEXPR
[ - + ][ - + ]
[ - - ]
183 : : && cacheVal.getNumChildren() == 2);
184 : 260 : Node quant = cacheVal[0];
185 [ - + ][ - + ]: 260 : Assert(quant.getKind() == Kind::FORALL);
[ - - ]
186 : 260 : uint32_t index = -1;
187 : 260 : ProofRuleChecker::getUInt32(cacheVal[1], index);
188 [ - + ][ - + ]: 260 : Assert(index < quant[0].getNumChildren());
[ - - ]
189 : 260 : Node var = quant[0][index];
190 : : // Since cvc5 *always* skolemize FORALLs, we generate the choice term
191 : : // assuming it is gonna be introduced via a sko_forall rule, in which
192 : : // case the body of the choice is negated, which means to have
193 : : // universal quantification of the remaining variables in the choice
194 : : // body, and the whole thing negated. Likewise, since during
195 : : // Skolemization cvc5 will have negated the body of the original
196 : : // quantifier, we need to revert that as well.
197 : : Node body =
198 : 260 : (index == quant[0].getNumChildren() - 1
199 : 1034 : ? quant[1]
200 : : : d_nm->mkNode(Kind::FORALL,
201 [ + + ][ - - ]: 387 : d_nm->mkNode(Kind::BOUND_VAR_LIST,
202 : 901 : std::vector<Node>{
203 [ + + ][ + + ]: 514 : quant[0].begin() + index + 1,
[ - - ]
204 [ + + ][ - - ]: 514 : quant[0].end()}),
205 : : quant[1]))
206 : 260 : .notNode();
207 : : // we need to replace in the body all the free variables (i.e., from 0
208 : : // to index) by their respective choice terms. To do this, we get
209 : : // the skolems for each of these variables, retrieve their
210 : : // conversions, and replace the variables by the conversions in body
211 [ + + ]: 260 : if (index > 0)
212 : : {
213 : 120 : std::vector<Node> subs;
214 [ + + ]: 638 : for (size_t i = 0; i < index; ++i)
215 : : {
216 : 2590 : std::vector<Node> cacheVals{quant, d_nm->mkConstInt(Rational(i))};
217 : : Node sk = sm->mkSkolemFunction(SkolemId::QUANTIFIERS_SKOLEMIZE,
218 : 518 : cacheVals);
219 [ - + ][ - + ]: 518 : Assert(!sk.isNull());
[ - - ]
220 [ - + ][ + - ]: 518 : subs.push_back(d_defineSkolems ? sk : convert(sk));
[ - - ]
221 : 518 : }
222 : 360 : body = body.substitute(quant[0].begin(),
223 : 240 : quant[0].begin() + index,
224 : : subs.begin(),
225 : 120 : subs.end());
226 : 120 : }
227 : : Node witness = d_nm->mkNode(
228 : 520 : Kind::WITNESS, d_nm->mkNode(Kind::BOUND_VAR_LIST, var), body);
229 [ + - ]: 260 : Trace("alethe-conv") << ".. witness: " << witness << "\n";
230 : 260 : witness = convert(witness);
231 : 260 : d_skolems[n] = witness;
232 [ - + ]: 260 : if (d_defineSkolems)
233 : : {
234 : 0 : if (std::find(d_skolemsList.begin(), d_skolemsList.end(), n)
235 [ - - ]: 0 : == d_skolemsList.end())
236 : : {
237 : 0 : d_skolemsList.push_back(n);
238 : : }
239 : 0 : return n;
240 : : }
241 : 260 : return witness;
242 : 260 : }
243 [ + + ]: 145 : if (sfi == SkolemId::ARRAY_DEQ_DIFF)
244 : : {
245 : : // create the witness term
246 : : //
247 : : // (witness ((x T)) (or (= a b) (not (= (select a x) (select b x)))))
248 : : //
249 : : // where a and b come from cache and T is the index type of a (which
250 : : // must be the same of b).
251 [ + - ]: 34 : Trace("alethe-conv")
252 [ - - ]: 17 : << ".. to build array diff choice with arrays: " << cacheVal[0]
253 [ - + ][ - + ]: 17 : << " / " << cacheVal[1] << "\n";
[ - - ]
254 [ + - ][ + - ]: 17 : Assert(cacheVal.getKind() == Kind::SEXPR
[ - + ][ - + ]
[ - - ]
255 : : && cacheVal.getNumChildren() == 2);
256 : 17 : Node a = cacheVal[0];
257 [ - + ][ - + ]: 17 : Assert(a.getType().isArray());
[ - - ]
258 : 17 : Node b = cacheVal[1];
259 [ - + ][ - + ]: 17 : Assert(b.getType().isArray());
[ - - ]
260 : 17 : TypeNode indexType = a.getType().getArrayIndexType();
261 : : // get index element of array
262 : 34 : Node var = NodeManager::mkBoundVar("x", indexType);
263 : 17 : Node eq = a.eqNode(b);
264 : : Node select =
265 : : d_nm->mkNode(Kind::NOT,
266 : 102 : d_nm->mkNode(Kind::EQUAL,
267 : 34 : {d_nm->mkNode(Kind::SELECT, a, var),
268 : 68 : d_nm->mkNode(Kind::SELECT, b, var)}));
269 : 34 : Node body = d_nm->mkNode(Kind::OR, eq, select);
270 : : Node choice = d_nm->mkNode(
271 : 34 : Kind::WITNESS, d_nm->mkNode(Kind::BOUND_VAR_LIST, var), body);
272 : 17 : choice = convert(choice);
273 : 17 : d_skolems[n] = choice;
274 : 17 : return choice;
275 : 17 : }
276 [ + + ]: 128 : if (sfi == SkolemId::GROUND_TERM)
277 : : {
278 : : // create the witness term (witness ((x T)) true) where T is the type of
279 : : // the skolem. This skolem is introduced for example by enumerative
280 : : // quantifier instantiation when no ground term exists in the formula of
281 : : // the same type as the variable being instantiated. This is done only
282 : : // once per type, so the formula in the body of the witness term is
283 : : // nonrestrictive.
284 : 4 : TypeNode tn = n.getType();
285 [ + - ]: 8 : Trace("alethe-conv")
286 : 0 : << ".. to build stand-in for arbitrary ground term of type: " << tn
287 : 4 : << "\n";
288 : 8 : Node var = NodeManager::mkBoundVar("x", tn);
289 : 4 : Node trueNode = d_nm->mkConst(true);
290 : : Node choice = d_nm->mkNode(
291 : 8 : Kind::WITNESS, d_nm->mkNode(Kind::BOUND_VAR_LIST, var), trueNode);
292 : 4 : choice = convert(choice);
293 : 4 : d_skolems[n] = choice;
294 : 4 : return choice;
295 : 4 : }
296 : 124 : std::stringstream ss;
297 : 124 : ss << "\"Proof unsupported by Alethe: contains Skolem (kind " << sfi
298 : 124 : << ", term " << n << "\"";
299 : 124 : d_error = ss.str();
300 : 124 : return Node::null();
301 : 1681 : }
302 : 8424 : case Kind::FORALL:
303 : : {
304 : : // remove patterns, if any
305 : 8424 : return n.getNumChildren() == 3 ? d_nm->mkNode(Kind::FORALL, n[0], n[1])
306 : 8424 : : n;
307 : : }
308 : : // we must make it to be printed with "choice", so we create an operator
309 : : // with that name and the correct type and do a function application
310 : 281 : case Kind::WITNESS:
311 : : {
312 : 281 : std::vector<TypeNode> childrenTypes;
313 [ + + ]: 843 : for (const Node& c : n)
314 : : {
315 : 562 : childrenTypes.push_back(c.getType());
316 : 562 : }
317 : 281 : TypeNode fType = d_nm->mkFunctionType(childrenTypes, n.getType());
318 : 562 : Node choiceOp = mkInternalSymbol("choice", fType);
319 : 562 : Node converted = d_nm->mkNode(Kind::APPLY_UF, choiceOp, n[0], n[1]);
320 [ + - ]: 281 : Trace("alethe-conv") << ".. converted to choice: " << converted << "\n";
321 : 281 : return converted;
322 : 281 : }
323 : : // other handled kinds but no-op in conversion. Everything else is
324 : : // unsupported
325 : : /* from builtin */
326 : 1855851 : case Kind::SORT_TYPE:
327 : : case Kind::INSTANTIATED_SORT_TYPE:
328 : : case Kind::UNINTERPRETED_SORT_VALUE:
329 : : case Kind::BUILTIN:
330 : : case Kind::EQUAL:
331 : : case Kind::DISTINCT:
332 : : case Kind::SEXPR:
333 : : case Kind::TYPE_CONSTANT:
334 : : case Kind::RAW_SYMBOL:
335 : : case Kind::APPLY_INDEXED_SYMBOLIC:
336 : : case Kind::APPLY_INDEXED_SYMBOLIC_OP:
337 : : /* from booleans */
338 : : case Kind::CONST_BOOLEAN:
339 : : case Kind::NOT:
340 : : case Kind::AND:
341 : : case Kind::IMPLIES:
342 : : case Kind::OR:
343 : : case Kind::XOR:
344 : : case Kind::ITE:
345 : : /* from uf */
346 : : case Kind::APPLY_UF:
347 : : case Kind::FUNCTION_TYPE:
348 : : case Kind::LAMBDA:
349 : : case Kind::HO_APPLY:
350 : : case Kind::FUNCTION_ARRAY_CONST:
351 : : /* from arith */
352 : : case Kind::ADD:
353 : : case Kind::MULT:
354 : : case Kind::NONLINEAR_MULT:
355 : : case Kind::SUB:
356 : : case Kind::NEG:
357 : : case Kind::DIVISION:
358 : : case Kind::INTS_DIVISION:
359 : : case Kind::INTS_MODULUS:
360 : : case Kind::ABS:
361 : : case Kind::DIVISIBLE:
362 : : case Kind::DIVISIBLE_OP:
363 : : case Kind::CONST_RATIONAL:
364 : : case Kind::CONST_INTEGER:
365 : : case Kind::LT:
366 : : case Kind::LEQ:
367 : : case Kind::GT:
368 : : case Kind::GEQ:
369 : : case Kind::IS_INTEGER:
370 : : case Kind::TO_INTEGER:
371 : : case Kind::TO_REAL:
372 : : case Kind::INTS_ISPOW2:
373 : : case Kind::INTS_LOG2:
374 : : case Kind::POW2:
375 : : /* from arrays */
376 : : case Kind::ARRAY_TYPE:
377 : : case Kind::SELECT:
378 : : case Kind::STORE:
379 : : case Kind::ARRAY_LAMBDA:
380 : : /* from quantifiers */
381 : : case Kind::EXISTS:
382 : : case Kind::BOUND_VAR_LIST:
383 : : case Kind::INST_PATTERN:
384 : : case Kind::INST_NO_PATTERN:
385 : : case Kind::INST_ATTRIBUTE:
386 : : case Kind::INST_POOL:
387 : : case Kind::INST_ADD_TO_POOL:
388 : : case Kind::SKOLEM_ADD_TO_POOL:
389 : : case Kind::INST_PATTERN_LIST:
390 : : {
391 : 1855851 : return n;
392 : : }
393 : : // BV, datatypes, strings, and constant array kinds are no-op in
394 : : // conversion but are reported as unsupported when running in Alethe
395 : : // testing mode.
396 : : /* from arrays (constant arrays) */
397 : 19665 : case Kind::STORE_ALL:
398 : : /* from uf (BV-related) */
399 : : case Kind::BITVECTOR_UBV_TO_INT:
400 : : case Kind::INT_TO_BITVECTOR_OP:
401 : : case Kind::INT_TO_BITVECTOR:
402 : : /* from BV */
403 : : case Kind::BITVECTOR_TYPE:
404 : : case Kind::CONST_BITVECTOR:
405 : : case Kind::BITVECTOR_SIZE:
406 : : case Kind::CONST_BITVECTOR_SYMBOLIC:
407 : : case Kind::BITVECTOR_CONCAT:
408 : : case Kind::BITVECTOR_AND:
409 : : case Kind::BITVECTOR_COMP:
410 : : case Kind::BITVECTOR_OR:
411 : : case Kind::BITVECTOR_XOR:
412 : : case Kind::BITVECTOR_NOT:
413 : : case Kind::BITVECTOR_NAND:
414 : : case Kind::BITVECTOR_NOR:
415 : : case Kind::BITVECTOR_XNOR:
416 : : case Kind::BITVECTOR_MULT:
417 : : case Kind::BITVECTOR_NEG:
418 : : case Kind::BITVECTOR_ADD:
419 : : case Kind::BITVECTOR_SUB:
420 : : case Kind::BITVECTOR_UDIV:
421 : : case Kind::BITVECTOR_UREM:
422 : : case Kind::BITVECTOR_SDIV:
423 : : case Kind::BITVECTOR_SMOD:
424 : : case Kind::BITVECTOR_SREM:
425 : : case Kind::BITVECTOR_ASHR:
426 : : case Kind::BITVECTOR_LSHR:
427 : : case Kind::BITVECTOR_SHL:
428 : : case Kind::BITVECTOR_ULE:
429 : : case Kind::BITVECTOR_ULT:
430 : : case Kind::BITVECTOR_UGE:
431 : : case Kind::BITVECTOR_UGT:
432 : : case Kind::BITVECTOR_SLE:
433 : : case Kind::BITVECTOR_SLT:
434 : : case Kind::BITVECTOR_SGE:
435 : : case Kind::BITVECTOR_SGT:
436 : : case Kind::BITVECTOR_ULTBV:
437 : : case Kind::BITVECTOR_SLTBV:
438 : : case Kind::BITVECTOR_ACKERMANNIZE_UDIV:
439 : : case Kind::BITVECTOR_ACKERMANNIZE_UREM:
440 : : case Kind::BITVECTOR_BIT_OP:
441 : : case Kind::BITVECTOR_EXTRACT_OP:
442 : : case Kind::BITVECTOR_EXTRACT:
443 : : case Kind::BITVECTOR_REPEAT_OP:
444 : : case Kind::BITVECTOR_REPEAT:
445 : : case Kind::BITVECTOR_ROTATE_LEFT_OP:
446 : : case Kind::BITVECTOR_ROTATE_LEFT:
447 : : case Kind::BITVECTOR_ROTATE_RIGHT_OP:
448 : : case Kind::BITVECTOR_ROTATE_RIGHT:
449 : : case Kind::BITVECTOR_SIGN_EXTEND_OP:
450 : : case Kind::BITVECTOR_SIGN_EXTEND:
451 : : case Kind::BITVECTOR_ZERO_EXTEND_OP:
452 : : case Kind::BITVECTOR_ZERO_EXTEND:
453 : : case Kind::BITVECTOR_ITE:
454 : : /* from datatypes */
455 : : case Kind::CONSTRUCTOR_TYPE:
456 : : case Kind::SELECTOR_TYPE:
457 : : case Kind::TESTER_TYPE:
458 : : case Kind::APPLY_CONSTRUCTOR:
459 : : case Kind::APPLY_SELECTOR:
460 : : case Kind::APPLY_TESTER:
461 : : case Kind::DATATYPE_TYPE:
462 : : case Kind::PARAMETRIC_DATATYPE:
463 : : case Kind::TUPLE_TYPE:
464 : : case Kind::APPLY_TYPE_ASCRIPTION:
465 : : case Kind::ASCRIPTION_TYPE:
466 : : case Kind::DT_SIZE:
467 : : case Kind::DT_HEIGHT_BOUND:
468 : : case Kind::DT_SIZE_BOUND:
469 : : case Kind::MATCH:
470 : : case Kind::MATCH_CASE:
471 : : case Kind::MATCH_BIND_CASE:
472 : : /* from strings */
473 : : case Kind::STRING_CONCAT:
474 : : case Kind::STRING_IN_REGEXP:
475 : : case Kind::STRING_LENGTH:
476 : : case Kind::STRING_SUBSTR:
477 : : case Kind::STRING_CHARAT:
478 : : case Kind::STRING_CONTAINS:
479 : : case Kind::STRING_LT:
480 : : case Kind::STRING_LEQ:
481 : : case Kind::STRING_INDEXOF:
482 : : case Kind::STRING_REPLACE:
483 : : case Kind::STRING_REPLACE_ALL:
484 : : case Kind::STRING_REPLACE_RE:
485 : : case Kind::STRING_REPLACE_RE_ALL:
486 : : case Kind::STRING_PREFIX:
487 : : case Kind::STRING_SUFFIX:
488 : : case Kind::STRING_IS_DIGIT:
489 : : case Kind::STRING_ITOS:
490 : : case Kind::STRING_STOI:
491 : : case Kind::STRING_TO_CODE:
492 : : case Kind::STRING_FROM_CODE:
493 : : case Kind::STRING_UNIT:
494 : : case Kind::CONST_STRING:
495 : : case Kind::STRING_TO_REGEXP:
496 : : case Kind::REGEXP_CONCAT:
497 : : case Kind::REGEXP_UNION:
498 : : case Kind::REGEXP_INTER:
499 : : case Kind::REGEXP_DIFF:
500 : : case Kind::REGEXP_STAR:
501 : : case Kind::REGEXP_PLUS:
502 : : case Kind::REGEXP_OPT:
503 : : case Kind::REGEXP_RANGE:
504 : : case Kind::REGEXP_COMPLEMENT:
505 : : case Kind::REGEXP_NONE:
506 : : case Kind::REGEXP_ALL:
507 : : case Kind::REGEXP_ALLCHAR:
508 : : case Kind::REGEXP_REPEAT_OP:
509 : : case Kind::REGEXP_REPEAT:
510 : : case Kind::REGEXP_LOOP_OP:
511 : : case Kind::REGEXP_LOOP:
512 : : case Kind::REGEXP_RV:
513 : : {
514 [ + - ]: 19665 : if (d_isTesting)
515 : : {
516 : 19665 : return recordUnsupportedKind(k);
517 : : }
518 : 0 : return n;
519 : : }
520 : 21988 : case Kind::BOUND_VARIABLE:
521 : : case Kind::VARIABLE:
522 : : {
523 : : // see if variable has a supported type. We need this check because in
524 : : // some problems involving unsupported theories there are no operators,
525 : : // just variables of unsupported type. Note that we need to consider the
526 : : // subtypes of a given type as well.
527 : 21988 : std::unordered_set<TypeNode> allTypes;
528 : 21988 : TypeNode tn = n.getType();
529 : 21988 : expr::getComponentTypes(tn, allTypes);
530 : 21988 : std::vector<TypeNode> allTypesVec(allTypes.begin(), allTypes.end());
531 : 21988 : collectTypes(allTypesVec, allTypes);
532 : 21988 : TypeNode unsupported = TypeNode::null();
533 [ + + ]: 51158 : for (const TypeNode& ttn : allTypes)
534 : : {
535 : 29170 : Kind tnk = ttn.getKind();
536 [ + - ]: 29170 : Trace("test") << "Test " << ttn << ", kind " << tnk << "\n";
537 [ + + ][ + ]: 29170 : switch (tnk)
538 : : {
539 : 9913 : case Kind::SORT_TYPE:
540 : : case Kind::INSTANTIATED_SORT_TYPE:
541 : : case Kind::FUNCTION_TYPE:
542 : : case Kind::ARRAY_TYPE:
543 : : {
544 : 25877 : continue;
545 : : }
546 : : // BV and datatypes type kinds are unsupported under testing mode.
547 : 1425 : case Kind::BITVECTOR_TYPE:
548 : : case Kind::CONSTRUCTOR_TYPE:
549 : : case Kind::SELECTOR_TYPE:
550 : : case Kind::TESTER_TYPE:
551 : : case Kind::ASCRIPTION_TYPE:
552 : : {
553 [ + - ]: 1425 : if (d_isTesting)
554 : : {
555 : 1425 : unsupported = ttn;
556 : 1425 : break;
557 : : }
558 : 0 : continue;
559 : : }
560 : 17832 : default:
561 : : {
562 : : // The supported constant types
563 [ + + ]: 17832 : if (tnk == Kind::TYPE_CONSTANT)
564 : : {
565 [ + + ][ + ]: 16417 : switch (ttn.getConst<TypeConstant>())
566 : : {
567 : 15964 : case TypeConstant::SEXPR_TYPE:
568 : : case TypeConstant::BOOLEAN_TYPE:
569 : : case TypeConstant::REAL_TYPE:
570 : : case TypeConstant::INTEGER_TYPE:
571 : : {
572 : 15964 : continue;
573 : : }
574 : : // String and regexp types are unsupported under testing mode.
575 : 444 : case TypeConstant::STRING_TYPE:
576 : : case TypeConstant::REGEXP_TYPE:
577 : : {
578 [ - + ]: 444 : if (!d_isTesting)
579 : : {
580 : 0 : continue;
581 : : }
582 : 444 : break; // fallthrough to the error handling below
583 : : }
584 : 9 : default: // fallthrough to the error handling below
585 : 9 : break;
586 : : }
587 : : }
588 : : // Only regular datatypes (parametric or not) are supported, and
589 : : // only outside testing mode.
590 [ - - ]: 0 : else if (!d_isTesting && ttn.isDatatype()
591 [ - - ]: 0 : && !ttn.getDType().isCodatatype()
592 [ - + ][ - - ]: 1415 : && (tnk == Kind::DATATYPE_TYPE
[ - + ]
593 [ - - ]: 0 : || tnk == Kind::PARAMETRIC_DATATYPE))
594 : : {
595 : 0 : continue;
596 : : }
597 [ + - ]: 1868 : Trace("test") << "\tBad: " << ttn << ", kind " << tnk << "\n";
598 : 1868 : unsupported = ttn;
599 : 1868 : break;
600 : : }
601 : : }
602 : : }
603 [ + + ]: 21988 : if (unsupported.isNull())
604 : : {
605 : 19211 : return n;
606 : : }
607 [ + - ]: 2777 : Trace("alethe-conv") << "AletheNodeConverter: ...unsupported type\n";
608 : 5554 : std::stringstream ss;
609 : 2777 : ss << "\"Proof unsupported by Alethe: contains ";
610 : 2777 : Kind utnk = unsupported.getKind();
611 [ + + ]: 2777 : if (utnk == Kind::TYPE_CONSTANT)
612 : : {
613 : 441 : ss << unsupported.getConst<TypeConstant>();
614 : : }
615 [ + + ]: 2336 : else if (unsupported.isDatatype())
616 : : {
617 : 586 : ss << "non-standard datatype";
618 : : }
619 : : else
620 : : {
621 : 1750 : ss << utnk;
622 : : }
623 : 2777 : ss << "\"";
624 : 2777 : d_error = ss.str();
625 : 2777 : return Node::null();
626 : 21988 : }
627 : 1986 : default:
628 : : {
629 : 1986 : return recordUnsupportedKind(k);
630 : : }
631 : : }
632 : : return n;
633 : : }
634 : :
635 : 281 : Node AletheNodeConverter::mkInternalSymbol(const std::string& name,
636 : : TypeNode tn,
637 : : bool useRawSym)
638 : : {
639 : 281 : std::pair<TypeNode, std::string> key(tn, name);
640 : : std::map<std::pair<TypeNode, std::string>, Node>::iterator it =
641 : 281 : d_symbolsMap.find(key);
642 [ + + ]: 281 : if (it != d_symbolsMap.end())
643 : : {
644 : 128 : return it->second;
645 : : }
646 : : Node sym = useRawSym ? NodeManager::mkRawSymbol(name, tn)
647 [ + - ]: 153 : : NodeManager::mkBoundVar(name, tn);
648 : 153 : d_symbolsMap[key] = sym;
649 : 153 : return sym;
650 : 281 : }
651 : :
652 : 0 : Node AletheNodeConverter::mkInternalSymbol(const std::string& name)
653 : : {
654 : 0 : return mkInternalSymbol(name, d_nm->sExprType());
655 : : }
656 : :
657 : 1948 : const std::string& AletheNodeConverter::getError() { return d_error; }
658 : :
659 : 21170 : Node AletheNodeConverter::getOriginalAssumption(Node n)
660 : : {
661 : 21170 : auto it = d_convToOriginalAssumption.find(n);
662 [ + - ]: 21170 : if (it != d_convToOriginalAssumption.end())
663 : : {
664 : 21170 : return it->second;
665 : : }
666 : 0 : return n;
667 : : }
668 : :
669 : 66 : const std::map<Node, Node>& AletheNodeConverter::getSkolemDefinitions()
670 : : {
671 : 66 : return d_skolems;
672 : : }
673 : :
674 : 0 : const std::vector<Node>& AletheNodeConverter::getSkolemList()
675 : : {
676 : 0 : return d_skolemsList;
677 : : }
678 : :
679 : : } // namespace proof
680 : : } // namespace cvc5::internal
|
