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