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 Eunoia node conversion
11 : : */
12 : :
13 : : #include "proof/eo/eo_node_converter.h"
14 : :
15 : : #include <algorithm>
16 : : #include <iomanip>
17 : : #include <sstream>
18 : :
19 : : #include "expr/aci_norm.h"
20 : : #include "expr/array_store_all.h"
21 : : #include "expr/cardinality_constraint.h"
22 : : #include "expr/dtype.h"
23 : : #include "expr/dtype_cons.h"
24 : : #include "expr/sequence.h"
25 : : #include "expr/sort_to_term.h"
26 : : #include "printer/smt2/smt2_printer.h"
27 : : #include "theory/builtin/generic_op.h"
28 : : #include "theory/bv/theory_bv_utils.h"
29 : : #include "theory/datatypes/datatypes_rewriter.h"
30 : : #include "theory/strings/theory_strings_utils.h"
31 : : #include "theory/strings/word.h"
32 : : #include "theory/uf/function_const.h"
33 : : #include "theory/uf/theory_uf_rewriter.h"
34 : : #include "util/bitvector.h"
35 : : #include "util/finite_field_value.h"
36 : : #include "util/floatingpoint.h"
37 : : #include "util/iand.h"
38 : : #include "util/indexed_root_predicate.h"
39 : : #include "util/rational.h"
40 : : #include "util/regexp.h"
41 : : #include "util/string.h"
42 : :
43 : : using namespace cvc5::internal::kind;
44 : :
45 : : namespace cvc5::internal {
46 : : namespace proof {
47 : :
48 : 3526 : BaseEoNodeConverter::BaseEoNodeConverter(NodeManager* nm) : NodeConverter(nm) {}
49 : :
50 : 1792 : EoNodeConverter::EoNodeConverter(NodeManager* nm) : BaseEoNodeConverter(nm)
51 : : {
52 : : // use builtin operator type as the type of sorts, which makes a difference
53 : : // e.g. for converting terms of kind SORT_TO_TERM.
54 : 1792 : d_sortType = nm->builtinOperatorType();
55 : 1792 : }
56 : :
57 : 1792 : EoNodeConverter::~EoNodeConverter() {}
58 : :
59 : 2238283 : Node EoNodeConverter::preConvert(Node n)
60 : : {
61 : : // match is not supported in Eunoia syntax, we eliminate it at pre-order
62 : : // traversal, which avoids type-checking errors during conversion, since e.g.
63 : : // match case nodes are required but cannot be preserved
64 [ + + ]: 2238283 : if (n.getKind() == Kind::MATCH)
65 : : {
66 : 12 : return theory::datatypes::DatatypesRewriter::expandMatch(n);
67 : : }
68 : 2238271 : return n;
69 : : }
70 : :
71 : 2234640 : Node EoNodeConverter::postConvert(Node n)
72 : : {
73 : 2234640 : Kind k = n.getKind();
74 : : // we eliminate MATCH at preConvert above
75 [ - + ][ - + ]: 2234640 : Assert(k != Kind::MATCH);
[ - - ]
76 [ + - ]: 4469280 : Trace("eo-term-process-debug")
77 : 2234640 : << "postConvert " << n << " " << k << std::endl;
78 [ + + ][ - + ]: 2234640 : if (k == Kind::ASCRIPTION_TYPE || k == Kind::RAW_SYMBOL)
79 : : {
80 : : // dummy node, return it
81 : 13 : return n;
82 : : }
83 : : // case for skolems, unhandled variables, and other unhandled terms
84 : : // These should print as @const, or otherwise be printed as a skolem,
85 : : // which may need further processing below. In the case of unhandled
86 : : // terms (e.g. DT_SYGUS_EVAL), we prefer printing them as @const instead
87 : : // of using their smt2 printer, which would lead to undeclared identifiers in
88 : : // the proof.
89 [ + + ][ + + ]: 2234627 : if (k == Kind::SKOLEM || k == Kind::DUMMY_SKOLEM || k == Kind::INST_CONSTANT
[ + + ]
90 [ - + ]: 2227582 : || k == Kind::DT_SYGUS_EVAL)
91 : : {
92 : 7045 : TypeNode tn = n.getType();
93 : : // constructors/selectors are represented by skolems, which are defined
94 : : // symbols
95 [ + + ]: 13634 : if (tn.isDatatypeConstructor() || tn.isDatatypeSelector()
96 [ + + ][ + + ]: 13634 : || tn.isDatatypeTester() || tn.isDatatypeUpdater())
[ + + ][ + + ]
97 : : {
98 : : // note these are not converted to their user named (cvc.) symbols here,
99 : : // to avoid type errors when constructing terms for postConvert
100 : 1071 : return n;
101 : : }
102 [ + + ]: 5974 : if (k == Kind::SKOLEM)
103 : : {
104 : : // might be a skolem function
105 : 5771 : Node ns = maybeMkSkolemFun(n);
106 [ + + ]: 5771 : if (!ns.isNull())
107 : : {
108 : 5701 : return ns;
109 : : }
110 [ + + ]: 5771 : }
111 : : // Otherwise, it is an uncategorized skolem, must use a fresh variable.
112 : : // This case will only apply for terms originating from places with no
113 : : // proof support. Note it is not added as a declared variable, instead it
114 : : // is used as (var N T) throughout.
115 : 546 : Node index = d_nm->mkConstInt(Rational(getOrAssignIndexForConst(n)));
116 : 273 : Node tc = typeAsNode(tn);
117 [ + + ][ - - ]: 819 : return mkInternalApp("@const", {index, tc}, tn);
118 : 7045 : }
119 [ + + ]: 2227582 : else if (k == Kind::BOUND_VARIABLE)
120 : : {
121 : 10508 : std::string sname;
122 [ + + ]: 10508 : if (n.hasName())
123 : : {
124 : : // get its name if it has one
125 : 7618 : sname = n.getName();
126 : : }
127 : : else
128 : : {
129 : : // otherwise invoke the printer to get its name
130 : 2890 : std::stringstream ss;
131 : 2890 : ss << n;
132 : 2890 : sname = ss.str();
133 : 2890 : }
134 : : // A variable x of type T can unambiguously referred to as (@var "x" T),
135 : : // which is a macro for (eo::var "x" T) in the cpc signature.
136 : : // We convert to this representation here, which will often be letified.
137 : 10508 : TypeNode tn = n.getType();
138 : 10508 : std::vector<Node> args;
139 : 10508 : Node nn = d_nm->mkConst(String(sname));
140 : 10508 : args.push_back(nn);
141 : 10508 : Node tnn = typeAsNode(tn);
142 : 10508 : args.push_back(tnn);
143 : 10508 : return mkInternalApp("@var", args, tn);
144 : 10508 : }
145 [ + + ]: 2217074 : else if (k == Kind::VARIABLE)
146 : : {
147 : : // note that we do not handle overloading here
148 : 16990 : return n;
149 : : }
150 [ + + ]: 2200084 : else if (k == Kind::APPLY_UF)
151 : : {
152 : : // must ensure we print higher-order function applications with "_"
153 [ + + ]: 31500 : if (!n.getOperator().isVar())
154 : : {
155 : 964 : TypeNode tn = n.getType();
156 : 964 : std::vector<Node> args;
157 : 964 : args.push_back(n.getOperator());
158 : 964 : args.insert(args.end(), n.begin(), n.end());
159 : 964 : return mkInternalApp("_", args, tn);
160 : 964 : }
161 : : }
162 [ + + ]: 2168584 : else if (k == Kind::HO_APPLY)
163 : : {
164 : 4860 : TypeNode tn = n.getType();
165 [ + + ][ - - ]: 14580 : return mkInternalApp("_", {n[0], n[1]}, tn);
166 : 4860 : }
167 [ + + ]: 2163724 : else if (n.isClosure())
168 : : {
169 : 22610 : TypeNode tn = n.getType();
170 : 22610 : Node vl = n[0];
171 : : // Notice that intentionally we drop annotations here.
172 : : // Additionally, it is important that we convert the closure to a
173 : : // non-closure operator here, since we will be traversing over it
174 : : // during letification.
175 : 22610 : std::vector<Node> args;
176 : 22610 : args.insert(args.end(),
177 : : n.begin(),
178 : 22610 : n.begin() + getNumChildrenToProcessForClosure(k));
179 : 22610 : return mkInternalApp(
180 : 45220 : printer::smt2::Smt2Printer::smtKindString(k), args, tn);
181 : 22610 : }
182 [ + + ]: 2141114 : else if (k == Kind::SET_INSERT)
183 : : {
184 : 6 : TypeNode tn = n.getType();
185 : 6 : std::vector<Node> iargs(n.begin(), n.begin() + n.getNumChildren() - 1);
186 : 6 : Node list = mkTypedList(iargs);
187 [ + + ][ - - ]: 18 : return mkInternalApp("set.insert", {list, n[n.getNumChildren() - 1]}, tn);
188 : 6 : }
189 [ + + ]: 2141108 : else if (k == Kind::CONST_SEQUENCE)
190 : : {
191 [ + + ]: 92 : if (!n.getConst<Sequence>().empty())
192 : : {
193 : : // if non-empty, must convert to term representation and convert
194 : 69 : Node cc = theory::strings::utils::mkConcatForConstSequence(n);
195 : 69 : return convert(cc);
196 : 69 : }
197 : : }
198 [ + + ]: 2141016 : else if (k == Kind::CONST_FINITE_FIELD)
199 : : {
200 : 68 : TypeNode tn = n.getType();
201 : 68 : const FiniteFieldValue& ffv = n.getConst<FiniteFieldValue>();
202 : 136 : Node v = convert(d_nm->mkConstInt(ffv.getValue()));
203 : 136 : Node fs = convert(d_nm->mkConstInt(ffv.getFieldSize()));
204 [ + + ][ - - ]: 204 : return mkInternalApp("ff.value", {fs, v}, tn);
205 : 68 : }
206 [ + + ]: 2140948 : else if (k == Kind::FUNCTION_ARRAY_CONST)
207 : : {
208 : : // must convert to lambda and then run the conversion
209 : 7 : Node lam = theory::uf::FunctionConst::toLambda(n);
210 [ - + ][ - + ]: 7 : Assert(!lam.isNull());
[ - - ]
211 : 7 : return convert(lam);
212 : 7 : }
213 [ + + ]: 2140941 : else if (k == Kind::APPLY_CONSTRUCTOR)
214 : : {
215 : 2732 : Node opc = getOperatorOfTerm(n);
216 [ + + ]: 2732 : if (n.getNumChildren() == 0)
217 : : {
218 : 157 : return opc;
219 : : }
220 : 2575 : std::vector<Node> newArgs;
221 : 2575 : newArgs.push_back(opc);
222 : 2575 : newArgs.insert(newArgs.end(), n.begin(), n.end());
223 : 2575 : Node ret = d_nm->mkNode(Kind::APPLY_UF, newArgs);
224 : 2575 : return convert(ret);
225 : 2732 : }
226 [ + + ][ + + ]: 2138209 : else if (k == Kind::APPLY_TESTER || k == Kind::APPLY_UPDATER || k == Kind::NEG
[ + + ]
227 [ + + ][ + + ]: 2136750 : || k == Kind::DIVISION_TOTAL || k == Kind::INTS_DIVISION_TOTAL
228 [ + + ][ + + ]: 2136287 : || k == Kind::INTS_MODULUS_TOTAL || k == Kind::APPLY_SELECTOR
229 [ - + ]: 2134099 : || k == Kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV)
230 : : {
231 : : // kinds where the operator may be different
232 : 4110 : Node opc = getOperatorOfTerm(n);
233 [ - + ]: 4110 : if (n.getNumChildren() == 0)
234 : : {
235 : 0 : return opc;
236 : : }
237 : 4110 : std::vector<Node> newArgs;
238 [ + + ]: 4110 : if (opc.getNumChildren() > 0)
239 : : {
240 : 900 : TypeNode tn = n.getType();
241 : 900 : newArgs.insert(newArgs.end(), opc.begin(), opc.end());
242 : 900 : newArgs.insert(newArgs.end(), n.begin(), n.end());
243 : 900 : opc = opc.getOperator();
244 : 900 : std::stringstream ss;
245 : 900 : ss << opc;
246 : 1800 : return mkInternalApp(ss.str(), newArgs, tn);
247 : 900 : }
248 : 3210 : newArgs.push_back(opc);
249 : 3210 : newArgs.insert(newArgs.end(), n.begin(), n.end());
250 : 3210 : return d_nm->mkNode(Kind::APPLY_UF, newArgs);
251 : 4110 : }
252 [ + + ]: 2134099 : else if (k == Kind::INDEXED_ROOT_PREDICATE)
253 : : {
254 : 37 : TypeNode tn = n.getType();
255 : : const IndexedRootPredicate& irp =
256 : 37 : n.getOperator().getConst<IndexedRootPredicate>();
257 : 37 : std::vector<Node> newArgs;
258 : 37 : newArgs.push_back(d_nm->mkConstInt(irp.d_index));
259 : 37 : newArgs.insert(newArgs.end(), n.begin(), n.end());
260 : 37 : return mkInternalApp("@indexed_root_predicate", newArgs, tn);
261 : 37 : }
262 [ + + ]: 2134062 : else if (k == Kind::FLOATINGPOINT_COMPONENT_NAN
263 [ + + ]: 2134058 : || k == Kind::FLOATINGPOINT_COMPONENT_INF
264 [ + + ]: 2134055 : || k == Kind::FLOATINGPOINT_COMPONENT_ZERO
265 [ + + ]: 2134052 : || k == Kind::FLOATINGPOINT_COMPONENT_SIGN
266 [ + + ]: 2134048 : || k == Kind::FLOATINGPOINT_COMPONENT_EXPONENT
267 [ + + ]: 2134045 : || k == Kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND)
268 : : {
269 : 20 : TypeNode tn = n.getType();
270 : : // dummy symbol, provide the return type
271 : 20 : Node tnn = typeAsNode(tn);
272 : 20 : std::stringstream ss;
273 : 20 : ss << printer::smt2::Smt2Printer::smtKindString(k);
274 : 60 : return mkInternalApp(ss.str(), {tnn}, tn);
275 : 20 : }
276 [ + + ][ + + ]: 2134042 : else if (k == Kind::SEXPR || k == Kind::BOUND_VAR_LIST)
277 : : {
278 : 99499 : TypeNode tn = n.getType();
279 : : // use generic list
280 : 99499 : std::vector<Node> args;
281 : 99499 : args.insert(args.end(), n.begin(), n.end());
282 : 99499 : return mkInternalApp("@list", args, tn);
283 : 99499 : }
284 [ + + ]: 2034543 : else if (k == Kind::APPLY_INDEXED_SYMBOLIC)
285 : : {
286 : 2871 : Kind okind = n.getOperator().getConst<GenericOp>().getKind();
287 [ - + ]: 2871 : if (okind == Kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV)
288 : : {
289 : 0 : TypeNode tn = n.getType();
290 : : // This does not take a rounding mode, we change the smt2 syntax
291 : : // to distinguish this case, similar to the case in getOperatorOfTerm
292 : : // where it is processed as an indexed operator.
293 : 0 : std::vector<Node> children(n.begin(), n.end());
294 : 0 : return mkInternalApp("to_fp_bv", children, tn);
295 : 0 : }
296 : : }
297 [ + + ]: 2031672 : else if (k == Kind::BITVECTOR_EAGER_ATOM)
298 : : {
299 : : // For now, we explicity remove the application.
300 : : // https://github.com/cvc5/cvc5-wishues/issues/156: if the smt2 printer
301 : : // is refactored to silently ignore this kind, this case can be deleted.
302 : 4 : return n[0];
303 : : }
304 [ + + ]: 2031668 : else if (k == Kind::SORT_TO_TERM)
305 : : {
306 : 1 : return typeAsNode(n.getConst<SortToTerm>().getType());
307 : : }
308 [ + + ]: 2031667 : else if (GenericOp::isIndexedOperatorKind(k))
309 : : {
310 : 15613 : TypeNode tn = n.getType();
311 : : // return app of?
312 : : std::vector<Node> args =
313 : 15613 : GenericOp::getIndicesForOperator(k, n.getOperator());
314 [ + + ][ + + ]: 15613 : if (k == Kind::RELATION_GROUP || k == Kind::TABLE_GROUP)
315 : : {
316 : 6 : Node list = mkList(args);
317 : 6 : std::vector<Node> children;
318 : 6 : children.push_back(list);
319 : 6 : children.insert(children.end(), n.begin(), n.end());
320 : 6 : return mkInternalApp(
321 : 12 : printer::smt2::Smt2Printer::smtKindString(k), children, tn);
322 : 6 : }
323 : 15607 : args.insert(args.end(), n.begin(), n.end());
324 : 15607 : return mkInternalApp(
325 : 31214 : printer::smt2::Smt2Printer::smtKindString(k), args, tn);
326 : 15613 : }
327 : 2049484 : return n;
328 : : }
329 : :
330 : 2238271 : bool EoNodeConverter::shouldTraverse(Node n)
331 : : {
332 : 2238271 : Kind k = n.getKind();
333 : : // don't convert instantiation pattern list directly
334 [ + + ]: 2238271 : if (k == Kind::INST_PATTERN_LIST)
335 : : {
336 : 1056 : return false;
337 : : }
338 : : // should not traverse internal applications
339 [ + + ]: 2237215 : if (k == Kind::APPLY_UF)
340 : : {
341 [ + + ]: 34075 : if (d_symbols.find(n.getOperator()) != d_symbols.end())
342 : : {
343 : 2575 : return false;
344 : : }
345 : : }
346 : 2234640 : return true;
347 : : }
348 : :
349 : 5771 : Node EoNodeConverter::maybeMkSkolemFun(Node k)
350 : : {
351 : 5771 : SkolemManager* sm = d_nm->getSkolemManager();
352 : 5771 : SkolemId sfi = SkolemId::NONE;
353 : 5771 : Node cacheVal;
354 : 5771 : TypeNode tn = k.getType();
355 [ + - ]: 5771 : if (sm->isSkolemFunction(k, sfi, cacheVal))
356 : : {
357 [ + + ]: 5771 : if (isHandledSkolemId(sfi))
358 : : {
359 [ + + ]: 5701 : if (!cacheVal.isNull())
360 : : {
361 : 5575 : std::vector<Node> vals;
362 [ + + ]: 5575 : if (cacheVal.getKind() == Kind::SEXPR)
363 : : {
364 : 687 : vals.insert(vals.end(), cacheVal.begin(), cacheVal.end());
365 : : }
366 : : else
367 : : {
368 : 4888 : vals.push_back(cacheVal);
369 : : }
370 : 5575 : bool hasChanged = false;
371 [ + + ]: 11966 : for (Node& v : vals)
372 : : {
373 : 6391 : Node orig = v;
374 : 6391 : v = convert(v);
375 [ + + ][ + + ]: 6391 : hasChanged = hasChanged || v != orig;
376 : 6391 : }
377 : : // if an index term changed, we have to construct a new skolem
378 [ + + ]: 5575 : if (hasChanged)
379 : : {
380 : : // construct an internal app instead
381 : 1780 : std::stringstream ss;
382 : 1780 : ss << "@" << sfi;
383 : 3560 : return mkInternalApp(ss.str(), vals, k.getType());
384 : 1780 : }
385 [ + + ]: 5575 : }
386 : : // otherwise we return itself, this will be printed in its full
387 : : // definition since applyPrintSkolemDefinitions is set to true
388 : 3921 : return k;
389 : : }
390 : : }
391 : 70 : return Node::null();
392 : 5771 : }
393 : :
394 : 11334 : Node EoNodeConverter::typeAsNode(TypeNode tn)
395 : : {
396 : : // should always exist in the cache, as we always run types through
397 : : // postConvertType before calling this method.
398 : 11334 : std::map<TypeNode, Node>::const_iterator it = d_typeAsNode.find(tn);
399 [ + + ]: 11334 : if (it != d_typeAsNode.end())
400 : : {
401 : 9902 : return it->second;
402 : : }
403 : : // dummy symbol whose name is the type printed
404 : : // this suffices since Eunoia faithfully represents all types.
405 : : // note we cannot letify types (same as in SMT-LIB)
406 : 1432 : std::stringstream ss;
407 : 1432 : ss << tn;
408 : 2864 : Node ret = mkInternalSymbol(ss.str(), d_sortType, true);
409 : 1432 : d_typeAsNode[tn] = ret;
410 : 1432 : return ret;
411 : 1432 : }
412 : :
413 : 22610 : size_t EoNodeConverter::getNumChildrenToProcessForClosure(Kind k) const
414 : : {
415 [ + + ]: 22610 : return k == Kind::SET_COMPREHENSION ? 3 : 2;
416 : : }
417 : :
418 : 6 : Node EoNodeConverter::mkList(const std::vector<Node>& args)
419 : : {
420 [ - + ][ - + ]: 6 : Assert(!args.empty());
[ - - ]
421 : 6 : TypeNode tn = d_nm->booleanType();
422 : : // singleton lists are handled due to (@list x) ---> (@list x eo::nil)
423 : 12 : return mkInternalApp("@list", args, tn);
424 : 6 : }
425 : :
426 : 6 : Node EoNodeConverter::mkTypedList(const std::vector<Node>& args)
427 : : {
428 [ - + ][ - + ]: 6 : Assert(!args.empty());
[ - - ]
429 : 6 : TypeNode tn = d_nm->booleanType();
430 : 12 : return mkInternalApp("@tlist", args, tn);
431 : 6 : }
432 : :
433 : 173919 : Node EoNodeConverter::mkInternalSymbol(const std::string& name,
434 : : TypeNode tn,
435 : : bool useRawSym)
436 : : {
437 : : // use raw symbol so that it is never quoted
438 : : Node sym = useRawSym ? NodeManager::mkRawSymbol(name, tn)
439 [ + - ]: 173919 : : NodeManager::mkBoundVar(name, tn);
440 : 173919 : d_symbols.insert(sym);
441 : 173919 : return sym;
442 : 0 : }
443 : :
444 : 172477 : Node EoNodeConverter::mkInternalApp(const std::string& name,
445 : : const std::vector<Node>& args,
446 : : TypeNode ret,
447 : : bool useRawSym)
448 : : {
449 [ + + ]: 172477 : if (!args.empty())
450 : : {
451 : 172320 : std::vector<TypeNode> argTypes;
452 [ + + ]: 3318645 : for (const Node& a : args)
453 : : {
454 [ - + ][ - + ]: 3146325 : Assert(!a.isNull());
[ - - ]
455 : 3146325 : argTypes.push_back(a.getType());
456 : : }
457 : 172320 : TypeNode atype = d_nm->mkFunctionType(argTypes, ret);
458 : 172320 : Node op = mkInternalSymbol(name, atype, useRawSym);
459 : 172320 : std::vector<Node> aargs;
460 : 172320 : aargs.push_back(op);
461 : 172320 : aargs.insert(aargs.end(), args.begin(), args.end());
462 : 172320 : return d_nm->mkNode(Kind::APPLY_UF, aargs);
463 : 172320 : }
464 : 157 : return mkInternalSymbol(name, ret, useRawSym);
465 : : }
466 : :
467 : 6842 : Node EoNodeConverter::getOperatorOfTerm(Node n)
468 : : {
469 [ - + ][ - + ]: 6842 : Assert(n.hasOperator());
[ - - ]
470 : 6842 : Kind k = n.getKind();
471 : 6842 : std::stringstream opName;
472 [ + - ]: 13684 : Trace("eo-term-process-debug2")
473 : 0 : << "getOperatorOfTerm " << n << " " << k << " "
474 : 0 : << (n.getMetaKind() == metakind::PARAMETERIZED) << " "
475 : 6842 : << GenericOp::isIndexedOperatorKind(k) << std::endl;
476 : 6842 : std::vector<Node> indices;
477 [ + + ]: 6842 : if (n.getMetaKind() == metakind::PARAMETERIZED)
478 : : {
479 : 5434 : Node op = n.getOperator();
480 : 5434 : bool isIndexed = GenericOp::isIndexedOperatorKind(k);
481 [ + + ]: 5434 : if (isIndexed)
482 : : {
483 : 817 : indices = GenericOp::getIndicesForOperator(k, n.getOperator());
484 : : }
485 [ - + ]: 4617 : else if (op.getType().isFunction())
486 : : {
487 : 0 : return op;
488 : : }
489 : : // note other kinds of functions (e.g. selectors and testers)
490 : 5434 : Node ret;
491 [ + + ]: 5434 : if (isIndexed)
492 : : {
493 [ + + ]: 817 : if (k == Kind::APPLY_TESTER)
494 : : {
495 : 802 : indices.clear();
496 : 802 : size_t cindex = DType::indexOf(op);
497 : 802 : const DType& dt = DType::datatypeOf(op);
498 : 802 : opName << "is";
499 [ + + ]: 802 : if (dt.isTuple())
500 : : {
501 [ + + ]: 10 : std::string tname = dt[0].getNumArgs() == 0 ? "tuple.unit" : "tuple";
502 : 20 : Node tsym = mkInternalSymbol(tname, dt[0].getConstructor().getType());
503 : 10 : indices.push_back(tsym);
504 : 10 : }
505 : : else
506 : : {
507 : 792 : indices.push_back(dt[cindex].getConstructor());
508 : : }
509 : : }
510 [ + - ]: 15 : else if (k == Kind::APPLY_UPDATER)
511 : : {
512 : 15 : indices.clear();
513 : 15 : size_t index = DType::indexOf(op);
514 : 15 : const DType& dt = DType::datatypeOf(op);
515 : 15 : size_t cindex = DType::cindexOf(op);
516 [ + + ]: 15 : if (dt.isTuple())
517 : : {
518 : 6 : opName << "tuple.update";
519 : 6 : indices.push_back(d_nm->mkConstInt(index));
520 : : }
521 : : else
522 : : {
523 : 9 : opName << "update";
524 : 9 : indices.push_back(dt[cindex][index].getSelector());
525 : : }
526 : : }
527 [ - - ]: 0 : else if (k == Kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV)
528 : : {
529 : : // this does not take a rounding mode, we change the smt2 syntax
530 : : // to distinguish this case.
531 : 0 : opName << "to_fp_bv";
532 : : }
533 : : else
534 : : {
535 : 0 : opName << printer::smt2::Smt2Printer::smtKindString(k);
536 : : }
537 : : }
538 [ + + ]: 4617 : else if (k == Kind::APPLY_CONSTRUCTOR)
539 : : {
540 : 2732 : unsigned index = DType::indexOf(op);
541 : 2732 : const DType& dt = DType::datatypeOf(op);
542 : : // get its variable name
543 [ + + ]: 2732 : if (dt.isTuple())
544 : : {
545 [ + + ]: 452 : if (n.getNumChildren() == 0)
546 : : {
547 : 1 : opName << "tuple.unit";
548 : : }
549 : : else
550 : : {
551 : 451 : opName << "tuple";
552 : : }
553 : : }
554 [ + + ]: 7 : else if ((dt.isNullable() && index == 0)
555 [ + + ][ + + ]: 2320 : || (dt.isParametric()
556 [ + + ][ + + ]: 2313 : && isAmbiguousDtConstructor(dt[index].getConstructor())))
[ + + ][ - - ]
557 : : {
558 : : // ambiguous if nullable.null or a user provided ambiguous datatype
559 : : // constructor
560 : 6 : opName << "as";
561 : 6 : indices.push_back(dt[index].getConstructor());
562 : : // tn is the return type
563 : 6 : TypeNode tn = n.getType();
564 : 6 : indices.push_back(typeAsNode(tn));
565 : 6 : }
566 : : else
567 : : {
568 : 2274 : opName << dt[index].getConstructor();
569 : : }
570 : : }
571 [ + - ]: 1885 : else if (k == Kind::APPLY_SELECTOR)
572 : : {
573 : : // maybe a shared selector
574 [ - + ]: 1885 : if (op.getSkolemId() == SkolemId::SHARED_SELECTOR)
575 : : {
576 : 0 : std::vector<Node> kindices = op.getSkolemIndices();
577 : 0 : opName << "@shared_selector";
578 : 0 : indices.push_back(
579 : 0 : typeAsNode(kindices[0].getConst<SortToTerm>().getType()));
580 : 0 : indices.push_back(
581 : 0 : typeAsNode(kindices[1].getConst<SortToTerm>().getType()));
582 : 0 : indices.push_back(kindices[2]);
583 : 0 : }
584 : : else
585 : : {
586 : 1885 : unsigned index = DType::indexOf(op);
587 : 1885 : const DType& dt = DType::datatypeOf(op);
588 [ + + ]: 1885 : if (dt.isTuple())
589 : : {
590 : 83 : indices.push_back(d_nm->mkConstInt(index));
591 : 83 : opName << "tuple.select";
592 : : }
593 : : else
594 : : {
595 : 1802 : unsigned cindex = DType::cindexOf(op);
596 : 1802 : opName << dt[cindex][index].getSelector();
597 : : }
598 : : }
599 : : }
600 : : else
601 : : {
602 : 0 : opName << op;
603 : : }
604 [ + - ]: 5434 : }
605 : : else
606 : : {
607 : 1408 : opName << printer::smt2::Smt2Printer::smtKindString(k);
608 : : }
609 : 6842 : std::vector<Node> args(n.begin(), n.end());
610 : 13684 : Node app = mkInternalApp(opName.str(), args, n.getType());
611 : 6842 : Node ret;
612 [ + + ]: 6842 : if (!indices.empty())
613 : : {
614 [ + + ]: 906 : Node op = args.empty() ? app : app.getOperator();
615 : 906 : ret = mkInternalApp(opName.str(), indices, op.getType());
616 : 906 : }
617 [ - + ]: 5936 : else if (n.isClosure())
618 : : {
619 : : // The operator of a closure by convention includes its variable list.
620 : : // This is required for cong over binders. We do not convert the variable
621 : : // list here, for the same reason as why it is not converted in convert(..).
622 : 0 : Node vl = n[0];
623 : : // the type of this term is irrelevant, just use vl's type
624 : 0 : ret = mkInternalApp(
625 : 0 : printer::smt2::Smt2Printer::smtKindString(k), {vl}, vl.getType());
626 : 0 : }
627 : : else
628 : : {
629 [ + + ]: 5936 : ret = args.empty() ? app : app.getOperator();
630 : : }
631 [ + - ]: 6842 : Trace("eo-term-process-debug2") << "...return " << ret << std::endl;
632 : 6842 : return ret;
633 : 6842 : }
634 : :
635 : 273 : size_t EoNodeConverter::getOrAssignIndexForConst(Node v)
636 : : {
637 : 273 : std::map<Node, size_t>::iterator it = d_constIndex.find(v);
638 [ - + ]: 273 : if (it != d_constIndex.end())
639 : : {
640 : 0 : return it->second;
641 : : }
642 : 273 : size_t id = d_constIndex.size();
643 : 273 : d_constIndex[v] = id;
644 : 273 : return id;
645 : : }
646 : :
647 : 33 : bool EoNodeConverter::isAmbiguousDtConstructor(const Node& op)
648 : : {
649 : 33 : std::map<Node, bool>::iterator it = d_ambDt.find(op);
650 [ + + ]: 33 : if (it != d_ambDt.end())
651 : : {
652 : 22 : return it->second;
653 : : }
654 : 11 : bool ret = false;
655 : 11 : TypeNode tn = op.getType();
656 [ + - ]: 22 : Trace("eo-amb-dt") << "Ambiguous datatype constructor? " << op << " " << tn
657 : 11 : << std::endl;
658 : 11 : size_t nchild = tn.getNumChildren();
659 [ - + ][ - + ]: 11 : Assert(nchild > 0);
[ - - ]
660 : 11 : std::unordered_set<TypeNode> atypes;
661 [ + + ]: 24 : for (size_t i = 0; i < nchild - 1; i++)
662 : : {
663 : 13 : expr::getComponentTypes(tn[i], atypes);
664 : : }
665 : 11 : const DType& dt = DType::datatypeOf(op);
666 : 11 : std::vector<TypeNode> params = dt.getParameters();
667 [ + + ]: 20 : for (const TypeNode& p : params)
668 : : {
669 [ + + ]: 13 : if (atypes.find(p) == atypes.end())
670 : : {
671 [ + - ]: 8 : Trace("eo-amb-dt") << "...yes since " << p << " not contained"
672 : 4 : << std::endl;
673 : 4 : ret = true;
674 : 4 : break;
675 : : }
676 : : }
677 [ + - ]: 11 : Trace("eo-amb-dt") << "...returns " << ret << std::endl;
678 : 11 : d_ambDt[op] = ret;
679 : 11 : return ret;
680 : 11 : }
681 : :
682 : 5771 : bool EoNodeConverter::isHandledSkolemId(SkolemId id)
683 : : {
684 : : // Note we don't handle skolems that take types as arguments yet.
685 [ + + ]: 5771 : switch (id)
686 : : {
687 : 5701 : case SkolemId::PURIFY:
688 : : case SkolemId::ARRAY_DEQ_DIFF:
689 : : case SkolemId::BV_EMPTY:
690 : : case SkolemId::DIV_BY_ZERO:
691 : : case SkolemId::INT_DIV_BY_ZERO:
692 : : case SkolemId::MOD_BY_ZERO:
693 : : case SkolemId::TRANSCENDENTAL_PURIFY:
694 : : case SkolemId::TRANSCENDENTAL_PURIFY_ARG:
695 : : case SkolemId::ARITH_VTS_DELTA:
696 : : case SkolemId::ARITH_VTS_DELTA_FREE:
697 : : case SkolemId::QUANTIFIERS_SKOLEMIZE:
698 : : case SkolemId::SETS_DEQ_DIFF:
699 : : case SkolemId::STRINGS_NUM_OCCUR:
700 : : case SkolemId::STRINGS_NUM_OCCUR_RE:
701 : : case SkolemId::STRINGS_OCCUR_INDEX:
702 : : case SkolemId::STRINGS_OCCUR_INDEX_RE:
703 : : case SkolemId::STRINGS_DEQ_DIFF:
704 : : case SkolemId::STRINGS_REPLACE_ALL_RESULT:
705 : : case SkolemId::STRINGS_ITOS_RESULT:
706 : : case SkolemId::STRINGS_STOI_RESULT:
707 : : case SkolemId::STRINGS_STOI_NON_DIGIT:
708 : : case SkolemId::RE_UNFOLD_POS_COMPONENT:
709 : : case SkolemId::BAGS_DEQ_DIFF:
710 : : case SkolemId::BAGS_DISTINCT_ELEMENTS:
711 : : case SkolemId::BAGS_MAP_PREIMAGE_INJECTIVE:
712 : : case SkolemId::BAGS_DISTINCT_ELEMENTS_SIZE:
713 : : case SkolemId::BAGS_MAP_SUM:
714 : : case SkolemId::TABLES_GROUP_PART:
715 : : case SkolemId::TABLES_GROUP_PART_ELEMENT:
716 : 5701 : case SkolemId::WITNESS_STRING_LENGTH: return true;
717 : 70 : default: break;
718 : : }
719 : 70 : return false;
720 : : }
721 : :
722 : : } // namespace proof
723 : : } // namespace cvc5::internal
|
