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 LFSC node conversion
11 : : */
12 : :
13 : : #include "proof/lfsc/lfsc_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/skolem_manager.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/word.h"
31 : : #include "theory/uf/function_const.h"
32 : : #include "theory/uf/theory_uf_rewriter.h"
33 : : #include "util/bitvector.h"
34 : : #include "util/finite_field_value.h"
35 : : #include "util/floatingpoint.h"
36 : : #include "util/iand.h"
37 : : #include "util/rational.h"
38 : : #include "util/regexp.h"
39 : : #include "util/string.h"
40 : :
41 : : using namespace cvc5::internal::kind;
42 : :
43 : : namespace cvc5::internal {
44 : : namespace proof {
45 : :
46 : 1723 : LfscNodeConverter::LfscNodeConverter(NodeManager* nm) : NodeConverter(nm)
47 : : {
48 : 1723 : d_arrow = nm->mkSortConstructor("arrow", 2);
49 : :
50 : 1723 : d_sortType = nm->mkSort("sortType");
51 : : // the embedding of arrow into Node, which is binary constructor over sorts
52 : 6892 : TypeNode anfType = nm->mkFunctionType({d_sortType, d_sortType}, d_sortType);
53 : 1723 : d_typeAsNode[d_arrow] =
54 : 3446 : getSymbolInternal(Kind::FUNCTION_TYPE, anfType, "arrow");
55 : :
56 : 1723 : TypeNode intType = nm->integerType();
57 : 6892 : TypeNode arrType = nm->mkFunctionType({d_sortType, d_sortType}, d_sortType);
58 : 1723 : d_typeKindToNodeCons[Kind::ARRAY_TYPE] =
59 : 3446 : getSymbolInternal(Kind::FUNCTION_TYPE, arrType, "Array");
60 : 1723 : TypeNode bvType = nm->mkFunctionType(intType, d_sortType);
61 : 1723 : d_typeKindToNodeCons[Kind::BITVECTOR_TYPE] =
62 : 3446 : getSymbolInternal(Kind::FUNCTION_TYPE, bvType, "BitVec");
63 : 6892 : TypeNode fpType = nm->mkFunctionType({intType, intType}, d_sortType);
64 : 1723 : d_typeKindToNodeCons[Kind::FLOATINGPOINT_TYPE] =
65 : 3446 : getSymbolInternal(Kind::FUNCTION_TYPE, fpType, "FloatingPoint");
66 : 1723 : TypeNode setType = nm->mkFunctionType(d_sortType, d_sortType);
67 : 1723 : d_typeKindToNodeCons[Kind::SET_TYPE] =
68 : 3446 : getSymbolInternal(Kind::FUNCTION_TYPE, setType, "Set");
69 : 1723 : d_typeKindToNodeCons[Kind::BAG_TYPE] =
70 : 3446 : getSymbolInternal(Kind::FUNCTION_TYPE, setType, "Bag");
71 : 1723 : d_typeKindToNodeCons[Kind::SEQUENCE_TYPE] =
72 : 3446 : getSymbolInternal(Kind::FUNCTION_TYPE, setType, "Seq");
73 : 1723 : }
74 : :
75 : 2601590 : Node LfscNodeConverter::preConvert(Node n)
76 : : {
77 : : // match is not supported in LFSC syntax, we eliminate it at pre-order
78 : : // traversal, which avoids type-checking errors during conversion, since e.g.
79 : : // match case nodes are required but cannot be preserved
80 [ + + ]: 2601590 : if (n.getKind() == Kind::MATCH)
81 : : {
82 : 12 : return theory::datatypes::DatatypesRewriter::expandMatch(n);
83 : : }
84 : 2601578 : return n;
85 : : }
86 : :
87 : 2592555 : Node LfscNodeConverter::postConvert(Node n)
88 : : {
89 : 2592555 : Kind k = n.getKind();
90 : : // we eliminate MATCH at preConvert above
91 [ - + ][ - + ]: 2592555 : Assert(k != Kind::MATCH);
[ - - ]
92 [ + + ]: 2592555 : if (k == Kind::ASCRIPTION_TYPE)
93 : : {
94 : : // dummy node, return it
95 : 13 : return n;
96 : : }
97 : 2592542 : TypeNode tn = n.getType();
98 [ + - ]: 5185084 : Trace("lfsc-term-process-debug")
99 : 2592542 : << "postConvert " << n << " " << k << std::endl;
100 [ + + ]: 2592542 : if (k == Kind::BOUND_VARIABLE)
101 : : {
102 [ - + ]: 9713 : if (d_symbols.find(n) != d_symbols.end())
103 : : {
104 : : // ignore internally generated symbols
105 : 0 : return n;
106 : : }
107 : : // bound variable v is (bvar x T)
108 : 9713 : TypeNode intType = d_nm->integerType();
109 : 19426 : Node x = d_nm->mkConstInt(Rational(getOrAssignIndexForBVar(n)));
110 : 19426 : Node tc = typeAsNode(convertType(tn));
111 : 38852 : TypeNode ftype = d_nm->mkFunctionType({intType, d_sortType}, tn);
112 : 19426 : Node bvarOp = getSymbolInternal(k, ftype, "bvar");
113 [ + + ][ - - ]: 29139 : return mkApplyUf(bvarOp, {x, tc});
114 : 9713 : }
115 [ + + ]: 2582829 : else if (k == Kind::RAW_SYMBOL)
116 : : {
117 : : // ignore internally generated symbols
118 : 13393 : return n;
119 : : }
120 [ + + ][ + + ]: 2569436 : else if (k == Kind::SKOLEM || k == Kind::DUMMY_SKOLEM
121 [ - + ]: 2562944 : || k == Kind::DT_SYGUS_EVAL)
122 : : {
123 : : // constructors/selectors are represented by skolems, which are defined
124 : : // symbols
125 [ + + ]: 12538 : if (tn.isDatatypeConstructor() || tn.isDatatypeSelector()
126 [ + + ][ + + ]: 12538 : || tn.isDatatypeTester() || tn.isDatatypeUpdater())
[ + + ][ + + ]
127 : : {
128 : : // note these are not converted to their user named (cvc.) symbols here,
129 : : // to avoid type errors when constructing terms for postConvert
130 : 1050 : return n;
131 : : }
132 : : // skolems v print as their original forms
133 : : // v is (skolem W) where W is the original or original form of v
134 : 5442 : Node wi = SkolemManager::getUnpurifiedForm(n);
135 [ + - ][ + + ]: 5442 : if (!wi.isNull() && wi != n)
[ + + ]
136 : : {
137 [ + - ]: 8884 : Trace("lfsc-term-process-debug")
138 : 4442 : << "...original form " << wi << std::endl;
139 : 4442 : wi = convert(wi);
140 [ + - ]: 8884 : Trace("lfsc-term-process-debug")
141 : 4442 : << "...converted original for " << wi << std::endl;
142 : 4442 : TypeNode ftype = d_nm->mkFunctionType(tn, tn);
143 : 8884 : Node skolemOp = getSymbolInternal(k, ftype, "skolem");
144 : 8884 : return mkApplyUf(skolemOp, {wi});
145 : 4442 : }
146 : : // might be a skolem function
147 : 1000 : Node ns = maybeMkSkolemFun(n);
148 [ + + ]: 1000 : if (!ns.isNull())
149 : : {
150 : 100 : return ns;
151 : : }
152 : : // Otherwise, it is an uncategorized skolem, must use a fresh variable.
153 : : // This case will only apply for terms originating from places with no
154 : : // proof support. Note it is not added as a declared variable, instead it
155 : : // is used as (var N T) throughout.
156 : 900 : TypeNode intType = d_nm->integerType();
157 : 3600 : TypeNode varType = d_nm->mkFunctionType({intType, d_sortType}, tn);
158 : 1800 : Node var = mkInternalSymbol("var", varType);
159 : 1800 : Node index = d_nm->mkConstInt(Rational(getOrAssignIndexForFVar(n)));
160 : 1800 : Node tc = typeAsNode(convertType(tn));
161 [ + + ][ - - ]: 2700 : return mkApplyUf(var, {index, tc});
162 : 5442 : }
163 [ + + ]: 2562944 : else if (n.isVar())
164 : : {
165 : 16199 : d_declVars.insert(n);
166 : 32398 : return mkInternalSymbol(getNameForUserNameOf(n), tn);
167 : : }
168 [ + + ]: 2546745 : else if (k == Kind::CARDINALITY_CONSTRAINT)
169 : : {
170 [ + - ]: 16 : Trace("lfsc-term-process-debug")
171 : 8 : << "...convert cardinality constraint" << std::endl;
172 : : const CardinalityConstraint& cc =
173 : 8 : n.getOperator().getConst<CardinalityConstraint>();
174 : 16 : Node tnn = typeAsNode(convertType(cc.getType()));
175 : 8 : Node ub = d_nm->mkConstInt(Rational(cc.getUpperBound()));
176 : : // Use boolType to ensure deterministic node ID assignments
177 : 8 : TypeNode boolType = d_nm->booleanType();
178 : : TypeNode tnc =
179 : 32 : d_nm->mkFunctionType({tnn.getType(), ub.getType()}, boolType);
180 : 16 : Node fcard = getSymbolInternal(k, tnc, "fmf.card");
181 [ + + ][ - - ]: 24 : return mkApplyUf(fcard, {tnn, ub});
182 : 8 : }
183 [ + + ]: 2546737 : else if (k == Kind::APPLY_UF)
184 : : {
185 : 77164 : return convert(theory::uf::TheoryUfRewriter::getHoApplyForApplyUf(n));
186 : : }
187 [ + + ][ + + ]: 2508155 : else if (k == Kind::APPLY_CONSTRUCTOR || k == Kind::APPLY_SELECTOR
188 [ + + ][ + + ]: 2503466 : || k == Kind::APPLY_TESTER || k == Kind::APPLY_UPDATER)
189 : : {
190 : : // must add to declared types
191 : 5464 : const DType& dt = DType::datatypeOf(n.getOperator());
192 : 5464 : d_declTypes.insert(dt.getTypeNode());
193 : : // must convert other kinds of apply to functions, since we convert to
194 : : // HO_APPLY
195 : 5464 : Node opc = getOperatorOfTerm(n, true);
196 [ + + ]: 5464 : if (n.getNumChildren() == 0)
197 : : {
198 : 153 : return opc;
199 : : }
200 : 10622 : return postConvert(mkApplyUf(opc, std::vector<Node>(n.begin(), n.end())));
201 : 5464 : }
202 [ + + ]: 2502691 : else if (k == Kind::HO_APPLY)
203 : : {
204 : 677178 : std::vector<TypeNode> argTypes;
205 : 677178 : argTypes.push_back(n[0].getType());
206 : 677178 : argTypes.push_back(n[1].getType());
207 : 677178 : TypeNode tnh = d_nm->mkFunctionType(argTypes, tn);
208 : 1354356 : Node hconstf = getSymbolInternal(k, tnh, "apply");
209 [ + + ][ - - ]: 2031534 : return mkApplyUf(hconstf, {n[0], n[1]});
210 : 677178 : }
211 [ + + ][ + + ]: 1825513 : else if (k == Kind::CONST_RATIONAL || k == Kind::CONST_INTEGER)
212 : : {
213 : 22408 : TypeNode tnv = d_nm->mkFunctionType(tn, tn);
214 : 22408 : Node rconstf;
215 : 22408 : Node arg;
216 : 22408 : Rational r = n.getConst<Rational>();
217 [ + + ]: 22408 : if (tn.isInteger())
218 : : {
219 : 17769 : rconstf = getSymbolInternal(k, tnv, "int");
220 [ + + ]: 17769 : if (r.sgn() == -1)
221 : : {
222 : : // use LFSC syntax for mpz negation
223 : 3154 : Node mpzn = getSymbolInternal(k, d_nm->mkFunctionType(tn, tn), "~");
224 : 3154 : arg = mkApplyUf(mpzn, {d_nm->mkConstInt(r.abs())});
225 : 1577 : }
226 : : else
227 : : {
228 : 16192 : arg = n;
229 : : }
230 : : }
231 : : else
232 : : {
233 : 4639 : rconstf = getSymbolInternal(k, tnv, "real");
234 : : // ensure rationals are printed properly here using mpq syntax
235 : : // Note that inconvieniently, LFSC uses (non-sexpr) syntax n/m for
236 : : // constant rationals, hence we must use a string
237 : 4639 : std::stringstream ss;
238 : 4639 : ss << "__LFSC_TMP" << r.getNumerator().abs() << "/" << r.getDenominator();
239 : 4639 : arg = mkInternalSymbol(ss.str(), tn);
240 : : // negative (~ n/m)
241 [ + + ]: 4639 : if (r.sgn() == -1)
242 : : {
243 : 4444 : Node mpzn = getSymbolInternal(k, d_nm->mkFunctionType(tn, tn), "~");
244 : 4444 : arg = mkApplyUf(mpzn, {arg});
245 : 2222 : }
246 : 4639 : }
247 : 44816 : return mkApplyUf(rconstf, {arg});
248 : 22408 : }
249 [ + + ]: 1803105 : else if (k == Kind::CONST_BITVECTOR)
250 : : {
251 : 1481 : TypeNode btn = d_nm->booleanType();
252 : 1481 : TypeNode tnv = d_nm->mkFunctionType(btn, tn);
253 : 1481 : BitVector bv = n.getConst<BitVector>();
254 : 1481 : Node ret = convertBitVector(bv);
255 : 2962 : Node bconstf = getSymbolInternal(k, tnv, "bv");
256 : 2962 : return mkApplyUf(bconstf, {ret});
257 : 1481 : }
258 [ + + ]: 1801624 : else if (k == Kind::CONST_FLOATINGPOINT)
259 : : {
260 : 19 : BitVector s, e, i;
261 : 19 : n.getConst<FloatingPoint>().getIEEEBitvectors(s, e, i);
262 : 19 : Node sn = convert(d_nm->mkConst(s));
263 : 19 : Node en = convert(d_nm->mkConst(e));
264 : 19 : Node in = convert(d_nm->mkConst(i));
265 : : TypeNode tnv =
266 : 95 : d_nm->mkFunctionType({sn.getType(), en.getType(), in.getType()}, tn);
267 : 38 : Node bconstf = getSymbolInternal(k, tnv, "fp");
268 [ + + ][ - - ]: 76 : return mkApplyUf(bconstf, {sn, en, in});
269 : 19 : }
270 [ + + ]: 1801605 : else if (k == Kind::CONST_FINITE_FIELD)
271 : : {
272 : 81 : const FiniteFieldValue& ffv = n.getConst<FiniteFieldValue>();
273 : 162 : Node v = convert(d_nm->mkConstInt(ffv.getValue()));
274 : 162 : Node fs = convert(d_nm->mkConstInt(ffv.getFieldSize()));
275 : 324 : TypeNode tnv = d_nm->mkFunctionType({v.getType(), fs.getType()}, tn);
276 : 162 : Node ffconstf = getSymbolInternal(k, tnv, "ff.value");
277 [ + + ][ - - ]: 243 : return mkApplyUf(ffconstf, {v, fs});
278 : 81 : }
279 [ + + ]: 1801524 : else if (k == Kind::CONST_STRING)
280 : : {
281 : : //"" is emptystr
282 : : //"A" is (char 65)
283 : : //"ABC" is (str.++ (char 65) (str.++ (char 66) (str.++ (char 67) emptystr)))
284 : 1467 : std::vector<Node> charVec;
285 : 1467 : getCharVectorInternal(n, charVec);
286 [ - + ][ - + ]: 1467 : Assert(!charVec.empty());
[ - - ]
287 [ + + ]: 1467 : if (charVec.size() == 1)
288 : : {
289 : : // handles empty string and singleton character
290 : 1059 : return charVec[0];
291 : : }
292 : 408 : std::reverse(charVec.begin(), charVec.end());
293 : 816 : Node ret = postConvert(getNullTerminator(d_nm, Kind::STRING_CONCAT, tn));
294 [ + + ]: 3722 : for (size_t i = 0, size = charVec.size(); i < size; i++)
295 : : {
296 : 3314 : ret = d_nm->mkNode(Kind::STRING_CONCAT, charVec[i], ret);
297 : : }
298 : 408 : return ret;
299 : 1467 : }
300 [ + + ]: 1800057 : else if (k == Kind::CONST_SEQUENCE)
301 : : {
302 : 89 : const std::vector<Node>& charVec = n.getConst<Sequence>().getVec();
303 : 89 : TypeNode etype = d_nm->mkFunctionType(d_sortType, tn);
304 : 178 : Node ret = getSymbolInternal(k, etype, "seq.empty");
305 : 178 : ret = mkApplyUf(ret, {typeAsNode(convertType(tn))});
306 : 89 : std::vector<Node> vecu;
307 [ + + ]: 131 : for (size_t i = 0, size = charVec.size(); i < size; i++)
308 : : {
309 : : Node u =
310 : 174 : d_nm->mkNode(Kind::SEQ_UNIT, postConvert(charVec[size - (i + 1)]));
311 [ + + ]: 87 : if (size == 1)
312 : : {
313 : : // singleton case
314 : 45 : return u;
315 : : }
316 : 42 : ret = d_nm->mkNode(Kind::STRING_CONCAT, u, ret);
317 [ + + ]: 87 : }
318 : 44 : return ret;
319 : 89 : }
320 [ + + ]: 1799968 : else if (k == Kind::STORE_ALL)
321 : : {
322 : 38 : Node t = typeAsNode(convertType(tn));
323 : 19 : TypeNode caRetType = d_nm->mkFunctionType(tn.getArrayConstituentType(), tn);
324 : 19 : TypeNode catype = d_nm->mkFunctionType(d_sortType, caRetType);
325 : 38 : Node bconstf = getSymbolInternal(k, catype, "array_const");
326 : 57 : Node f = mkApplyUf(bconstf, {t});
327 : 19 : ArrayStoreAll storeAll = n.getConst<ArrayStoreAll>();
328 : 38 : return mkApplyUf(f, {convert(storeAll.getValue())});
329 : 19 : }
330 [ + + ][ + + ]: 1775827 : else if (k == Kind::GEQ || k == Kind::GT || k == Kind::LEQ || k == Kind::LT
[ + + ]
331 [ + + ][ + + ]: 1728615 : || k == Kind::SUB || k == Kind::DIVISION || k == Kind::DIVISION_TOTAL
[ + + ]
332 [ + + ][ + + ]: 1726207 : || k == Kind::INTS_DIVISION || k == Kind::INTS_DIVISION_TOTAL
333 [ + + ][ + + ]: 1725694 : || k == Kind::INTS_MODULUS || k == Kind::INTS_MODULUS_TOTAL
334 [ + + ][ + + ]: 1725231 : || k == Kind::NEG || k == Kind::POW
335 [ + + ]: 1724596 : || k == Kind::FLOATINGPOINT_COMPONENT_NAN
336 [ + + ]: 1724594 : || k == Kind::FLOATINGPOINT_COMPONENT_INF
337 [ + + ]: 1724593 : || k == Kind::FLOATINGPOINT_COMPONENT_ZERO
338 [ + + ]: 1724592 : || k == Kind::FLOATINGPOINT_COMPONENT_SIGN
339 [ + + ]: 1724590 : || k == Kind::FLOATINGPOINT_COMPONENT_EXPONENT
340 [ + + ]: 1724589 : || k == Kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND
341 [ + - ]: 1724588 : || k == Kind::ROUNDINGMODE_BITBLAST
342 [ + + ][ + + ]: 3575776 : || GenericOp::isIndexedOperatorKind(k))
[ + + ]
343 : : {
344 : : // must give special names to SMT-LIB operators with arithmetic subtyping
345 : : // note that SUB is not n-ary
346 : : // get the macro-apply version of the operator
347 : 87735 : Node opc = getOperatorOfTerm(n, true);
348 : 87735 : return mkApplyUf(opc, std::vector<Node>(n.begin(), n.end()));
349 : 87735 : }
350 [ + + ][ + + ]: 1712214 : else if (k == Kind::SET_EMPTY || k == Kind::SET_UNIVERSE
351 [ + + ]: 1712143 : || k == Kind::BAG_EMPTY)
352 : : {
353 : 158 : Node t = typeAsNode(convertType(tn));
354 : 79 : TypeNode etype = d_nm->mkFunctionType(d_sortType, tn);
355 : : Node ef = getSymbolInternal(
356 : : k,
357 : : etype,
358 : 79 : k == Kind::SET_EMPTY
359 : : ? "set.empty"
360 [ + + ][ + + ]: 158 : : (k == Kind::SET_UNIVERSE ? "set.universe" : "bag.empty"));
361 : 158 : return mkApplyUf(ef, {t});
362 : 79 : }
363 [ + + ]: 1712135 : else if (n.isClosure())
364 : : {
365 : : // (forall ((x1 T1) ... (xn Tk)) P) is
366 : : // ((forall x1 T1) ((forall x2 T2) ... ((forall xk Tk) P))). We use
367 : : // SEXPR to do this, which avoids the need for indexed operators.
368 : 21504 : Node ret = n[1];
369 : 21504 : Node cop = getOperatorOfClosure(n, true);
370 : 21504 : Node pcop = getOperatorOfClosure(n, true, true);
371 [ + + ]: 73729 : for (size_t i = 0, nchild = n[0].getNumChildren(); i < nchild; i++)
372 : : {
373 : 52225 : size_t ii = (nchild - 1) - i;
374 : 52225 : Node v = n[0][ii];
375 : : // use the partial operator for variables except the last one. This
376 : : // avoids type errors in internal representation of LFSC terms.
377 [ + + ]: 104450 : Node vop = getOperatorOfBoundVar(ii == 0 ? cop : pcop, v);
378 : 104450 : ret = mkApplyUf(vop, {ret});
379 : 52225 : }
380 : : // notice that intentionally we drop annotations here
381 : 21504 : return ret;
382 : 21504 : }
383 [ + + ]: 1690631 : else if (k == Kind::FUNCTION_ARRAY_CONST)
384 : : {
385 : : // must convert to lambda and then run the conversion
386 : 6 : Node lam = theory::uf::FunctionConst::toLambda(n);
387 [ - + ][ - + ]: 6 : Assert(!lam.isNull());
[ - - ]
388 : 6 : return convert(lam);
389 : 6 : }
390 [ - + ]: 1690625 : else if (k == Kind::REGEXP_LOOP)
391 : : {
392 : : // ((_ re.loop n1 n2) t) is ((re.loop n1 n2) t)
393 : 0 : TypeNode intType = d_nm->integerType();
394 : : TypeNode relType =
395 : 0 : d_nm->mkFunctionType({intType, intType}, d_nm->mkFunctionType(tn, tn));
396 : : Node rop = getSymbolInternal(
397 : 0 : k, relType, printer::smt2::Smt2Printer::smtKindString(k));
398 : 0 : RegExpLoop op = n.getOperator().getConst<RegExpLoop>();
399 : 0 : Node n1 = d_nm->mkConstInt(Rational(op.d_loopMinOcc));
400 : 0 : Node n2 = d_nm->mkConstInt(Rational(op.d_loopMaxOcc));
401 : 0 : return mkApplyUf(mkApplyUf(rop, {n1, n2}), {n[0]});
402 : 0 : }
403 [ + + ]: 1690625 : else if (k == Kind::BITVECTOR_FROM_BOOLS)
404 : : {
405 : 3744 : TypeNode btn = d_nm->booleanType();
406 : : // (from_bools t1 ... tn) is
407 : : // (from_bools t1 (from_bools t2 ... (from_bools tn emptybv)))
408 : : // where notice that each from_bools has a different type
409 : 3744 : Node curr = getNullTerminator(d_nm, Kind::BITVECTOR_CONCAT, tn);
410 [ + + ]: 27231 : for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; ++i)
411 : : {
412 : 23487 : TypeNode bvt = d_nm->mkBitVectorType(i + 1);
413 : 93948 : TypeNode ftype = d_nm->mkFunctionType({btn, curr.getType()}, bvt);
414 : 46974 : Node bbt = getSymbolInternal(k, ftype, "from_bools");
415 [ + + ][ - - ]: 70461 : curr = mkApplyUf(bbt, {n[nchild - (i + 1)], curr});
416 : 23487 : }
417 : 3744 : return curr;
418 : 3744 : }
419 [ + + ]: 1686881 : else if (k == Kind::SEP_NIL)
420 : : {
421 : 6 : Node tnn = typeAsNode(convertType(tn));
422 : 3 : TypeNode ftype = d_nm->mkFunctionType(d_sortType, tn);
423 : 6 : Node s = getSymbolInternal(k, ftype, "sep.nil");
424 : 6 : return mkApplyUf(s, {tnn});
425 : 3 : }
426 [ + + ][ + + ]: 1686878 : else if (NodeManager::isNAryKind(k) && n.getNumChildren() >= 2)
[ + + ]
427 : : {
428 : 550751 : size_t nchild = n.getNumChildren();
429 [ - + ][ - + ]: 550751 : Assert(n.getMetaKind() != metakind::PARAMETERIZED);
[ - - ]
430 : : // convert all n-ary applications to binary
431 : 550751 : std::vector<Node> children(n.begin(), n.end());
432 : : // distinct is special case
433 [ + + ]: 550751 : if (k == Kind::DISTINCT)
434 : : {
435 : : // DISTINCT(x1,...,xn) --->
436 : : // AND(DISTINCT(x1,x2), AND(,..., AND(,..,DISTINCT(x_{n-1},x_n))))
437 : 3188 : Node ret = d_nm->mkNode(k, children[0], children[1]);
438 [ + + ]: 5872 : for (unsigned i = 0; i < nchild; i++)
439 [ + + ]: 30979 : for (unsigned j = i + 1; j < nchild; j++)
440 : : {
441 [ + + ][ + - ]: 26701 : if (i != 0 && j != 1)
442 : : {
443 : 48034 : ret = d_nm->mkNode(
444 : 72051 : Kind::AND, ret, d_nm->mkNode(k, children[i], children[j]));
445 : : }
446 : : }
447 [ + - ]: 3188 : Trace("lfsc-term-process-debug") << "n: " << n << std::endl
448 : 1594 : << "ret: " << ret << std::endl;
449 : 1594 : return ret;
450 : 1594 : }
451 : 549157 : std::reverse(children.begin(), children.end());
452 : : // Add the null-terminator. This is done to disambiguate the number
453 : : // of children for term with n-ary operators. In particular note that
454 : : // (or A B C (or D E)) has representation:
455 : : // (or A (or B (or C (or (or D E) false))))
456 : : // This makes the AST above distinguishable from (or A B C D E),
457 : : // which otherwise would both have representation:
458 : : // (or A (or B (or C (or D E))))
459 : 549157 : Node nullTerm = getNullTerminator(d_nm, k, tn);
460 : : // Most operators simply get binarized
461 : 549157 : Node ret;
462 : 549157 : size_t istart = 0;
463 [ + + ]: 549157 : if (nullTerm.isNull())
464 : : {
465 : 71 : ret = children[0];
466 : 71 : istart = 1;
467 : : }
468 : : else
469 : : {
470 : : // must convert recursively, since nullTerm may have subterms.
471 : 549086 : ret = convert(nullTerm);
472 : : }
473 : : // check whether we are also changing the operator name, in which case
474 : : // we build a binary uninterpreted function opc
475 : 549157 : bool isArithOp =
476 [ + + ][ + + ]: 549157 : (k == Kind::ADD || k == Kind::MULT || k == Kind::NONLINEAR_MULT);
[ + + ]
477 : 549157 : std::stringstream arithOpName;
478 [ + + ]: 549157 : if (isArithOp)
479 : : {
480 : : // currently allow subtyping
481 : 98865 : arithOpName << "a.";
482 : 98865 : arithOpName << printer::smt2::Smt2Printer::smtKindString(k);
483 : : }
484 : : // now, iterate over children and make binary conversion
485 [ + + ]: 2702764 : for (size_t i = istart, npchild = children.size(); i < npchild; i++)
486 : : {
487 [ + + ]: 2153607 : if (isArithOp)
488 : : {
489 : : // Arithmetic operators must deal with permissive type rules for
490 : : // ADD, MULT, NONLINEAR_MULT. We use the properly typed operator to
491 : : // avoid debug failures.
492 : 285233 : TypeNode tn1 = children[i].getType();
493 : 285233 : TypeNode tn2 = ret.getType();
494 : 1140932 : TypeNode ftype = d_nm->mkFunctionType({tn1, tn2}, tn);
495 : 570466 : Node opc = getSymbolInternal(k, ftype, arithOpName.str());
496 [ + + ][ - - ]: 855699 : ret = mkApplyUf(opc, {children[i], ret});
497 : 285233 : }
498 : : else
499 : : {
500 : 1868374 : ret = d_nm->mkNode(k, children[i], ret);
501 : : }
502 : : }
503 [ + - ]: 1098314 : Trace("lfsc-term-process-debug")
504 : 549157 : << "...return n-ary conv " << ret << std::endl;
505 : 549157 : return ret;
506 : 550751 : }
507 : 1136127 : return n;
508 : 2592542 : }
509 : :
510 : 1282328 : Node LfscNodeConverter::mkApplyUf(Node op, const std::vector<Node>& args) const
511 : : {
512 : 1282328 : std::vector<Node> aargs;
513 [ + + ]: 1282328 : if (op.isVar())
514 : : {
515 : 1216935 : aargs.push_back(op);
516 : : }
517 : : else
518 : : {
519 : : // Note that dag threshold is disabled for printing operators.
520 : 65393 : std::stringstream ss;
521 : 65393 : options::ioutils::applyOutputLanguage(ss, Language::LANG_SMTLIB_V2_6);
522 : 65393 : options::ioutils::applyDagThresh(ss, 0);
523 : 65393 : ss << op;
524 : 130786 : Node opv = NodeManager::mkRawSymbol(ss.str(), op.getType());
525 : 65393 : aargs.push_back(opv);
526 : 65393 : }
527 : 1282328 : aargs.insert(aargs.end(), args.begin(), args.end());
528 : 2564656 : return d_nm->mkNode(Kind::APPLY_UF, aargs);
529 : 1282328 : }
530 : :
531 : 6847 : TypeNode LfscNodeConverter::preConvertType(TypeNode tn)
532 : : {
533 [ + + ]: 6847 : if (tn.getKind() == Kind::TUPLE_TYPE)
534 : : {
535 : : // Must collect the tuple type here, since at post-order traversal, the
536 : : // type has been modified and no longer maintains the mapping to its
537 : : // datatype encoding.
538 : 82 : d_declTypes.insert(tn);
539 : : }
540 : 6847 : return tn;
541 : : }
542 : :
543 : 6847 : TypeNode LfscNodeConverter::postConvertType(TypeNode tn)
544 : : {
545 : 6847 : TypeNode cur = tn;
546 : 6847 : Node tnn;
547 : 6847 : Kind k = tn.getKind();
548 [ + - ]: 13694 : Trace("lfsc-term-process-debug")
549 : 6847 : << "postConvertType " << tn << " " << tn.getNumChildren() << " " << k
550 : 6847 : << std::endl;
551 [ + + ]: 6847 : if (k == Kind::FUNCTION_TYPE)
552 : : {
553 : : // (-> T1 ... Tn T) is (arrow T1 .... (arrow Tn T))
554 : 2688 : std::vector<TypeNode> argTypes = tn.getArgTypes();
555 : : // also make the node embedding of the type
556 : 2688 : Node arrown = d_typeAsNode[d_arrow];
557 [ - + ][ - + ]: 2688 : Assert(!arrown.isNull());
[ - - ]
558 : 2688 : cur = tn.getRangeType();
559 : 2688 : tnn = typeAsNode(cur);
560 : 2688 : for (std::vector<TypeNode>::reverse_iterator it = argTypes.rbegin();
561 [ + + ]: 7678 : it != argTypes.rend();
562 : 4990 : ++it)
563 : : {
564 : 4990 : std::vector<TypeNode> aargs;
565 : 4990 : aargs.push_back(*it);
566 : 4990 : aargs.push_back(cur);
567 : 4990 : cur = d_nm->mkSort(d_arrow, aargs);
568 [ + + ][ - - ]: 14970 : tnn = mkApplyUf(arrown, {typeAsNode(*it), tnn});
569 : 4990 : }
570 : 2688 : }
571 [ + + ]: 4159 : else if (k == Kind::BITVECTOR_TYPE)
572 : : {
573 : 539 : tnn = d_typeKindToNodeCons[k];
574 : 539 : Node w = d_nm->mkConstInt(Rational(tn.getBitVectorSize()));
575 : 1078 : tnn = mkApplyUf(tnn, {w});
576 : 539 : }
577 [ + + ]: 3620 : else if (k == Kind::FLOATINGPOINT_TYPE)
578 : : {
579 : 6 : tnn = d_typeKindToNodeCons[k];
580 : 6 : Node e = d_nm->mkConstInt(Rational(tn.getFloatingPointExponentSize()));
581 : 6 : Node s = d_nm->mkConstInt(Rational(tn.getFloatingPointSignificandSize()));
582 [ + + ][ - - ]: 18 : tnn = mkApplyUf(tnn, {e, s});
583 : 6 : }
584 [ + + ]: 3614 : else if (k == Kind::TUPLE_TYPE)
585 : : {
586 : : // special case: tuples must be distinguished by their arity
587 : 82 : size_t nargs = tn.getNumChildren();
588 [ + + ]: 82 : if (nargs > 0)
589 : : {
590 : 81 : std::vector<TypeNode> types;
591 : 81 : std::vector<TypeNode> convTypes;
592 : 81 : std::vector<Node> targs;
593 [ + + ]: 260 : for (size_t i = 0; i < nargs; i++)
594 : : {
595 : 179 : TypeNode tnc = tn[i];
596 : 179 : types.push_back(d_sortType);
597 : 179 : convTypes.push_back(tnc);
598 : 179 : targs.push_back(typeAsNode(tnc));
599 : 179 : }
600 : 81 : TypeNode ftype = d_nm->mkFunctionType(types, d_sortType);
601 : : // must distinguish by arity
602 : 81 : std::stringstream ss;
603 : 81 : ss << "Tuple_" << nargs;
604 : 81 : tnn = mkApplyUf(getSymbolInternal(k, ftype, ss.str()), targs);
605 : : // we are changing its name, we must make a sort constructor
606 : 81 : cur = d_nm->mkSortConstructor(ss.str(), nargs);
607 : 81 : cur = d_nm->mkSort(cur, convTypes);
608 : 81 : }
609 : : else
610 : : {
611 : : // no need to convert type for tuples of size 0,
612 : : // type as node is simple
613 : 1 : tnn = getSymbolInternal(k, d_sortType, "UnitTuple");
614 : : }
615 : : }
616 [ + + ]: 3532 : else if (tn.getNumChildren() == 0)
617 : : {
618 [ - + ][ - + ]: 3131 : Assert(!tn.isTuple());
[ - - ]
619 : : // an uninterpreted sort, or an uninstantiatied (maybe parametric) datatype
620 : 3131 : d_declTypes.insert(tn);
621 : 3131 : std::stringstream ss;
622 : 3131 : options::ioutils::applyOutputLanguage(ss, Language::LANG_SMTLIB_V2_6);
623 : 3131 : tn.toStream(ss);
624 [ + + ]: 3131 : if (tn.isUninterpretedSortConstructor())
625 : : {
626 : 11 : std::string s = getNameForUserNameOfInternal(tn.getId(), ss.str());
627 : 11 : tnn = getSymbolInternal(k, d_sortType, s, false);
628 : : cur =
629 : 11 : d_nm->mkSortConstructor(s, tn.getUninterpretedSortConstructorArity());
630 : 11 : }
631 [ + + ][ + + ]: 3120 : else if (tn.isUninterpretedSort() || tn.isDatatype())
[ + + ]
632 : : {
633 : 1548 : std::string s = getNameForUserNameOfInternal(tn.getId(), ss.str());
634 : 1548 : tnn = getSymbolInternal(k, d_sortType, s, false);
635 : 1548 : cur = d_nm->mkSort(s);
636 : 1548 : }
637 : : else
638 : : {
639 : : // all other builtin type constants, e.g. Int
640 : 1572 : tnn = getSymbolInternal(k, d_sortType, ss.str());
641 : : }
642 : 3131 : }
643 : : else
644 : : {
645 : : // to build the type-as-node, must convert the component types
646 : 401 : std::vector<Node> targs;
647 : 401 : std::vector<TypeNode> types;
648 [ + + ]: 980 : for (const TypeNode& tnc : tn)
649 : : {
650 : 579 : targs.push_back(typeAsNode(tnc));
651 : 579 : types.push_back(d_sortType);
652 : 579 : }
653 : 401 : Node op;
654 [ + + ]: 401 : if (k == Kind::PARAMETRIC_DATATYPE)
655 : : {
656 : : // note we don't add to declared types here, since the parametric
657 : : // datatype is traversed and will be declared as a type constructor
658 : : // erase first child, which repeats the datatype
659 : 9 : targs.erase(targs.begin(), targs.begin() + 1);
660 : 9 : types.erase(types.begin(), types.begin() + 1);
661 : 9 : TypeNode ftype = d_nm->mkFunctionType(types, d_sortType);
662 : : // the operator has been converted; it is no longer a datatype, thus
663 : : // we must print to get its name.
664 : 9 : std::stringstream ss;
665 : 9 : ss << tn[0];
666 : 9 : op = getSymbolInternal(k, ftype, ss.str());
667 : 9 : }
668 [ + + ]: 392 : else if (k == Kind::INSTANTIATED_SORT_TYPE)
669 : : {
670 : : // We don't add to declared types here. The type constructor is already
671 : : // added to declare types when processing the children of this.
672 : : // Also, similar to PARAMETRIC_DATATYPE, the type constructor
673 : : // should be erased from children.
674 : 39 : targs.erase(targs.begin(), targs.begin() + 1);
675 : 39 : types.erase(types.begin(), types.begin() + 1);
676 : 39 : TypeNode ftype = d_nm->mkFunctionType(types, d_sortType);
677 : 39 : std::string name = tn.getUninterpretedSortConstructor().getName();
678 : 39 : op = getSymbolInternal(k, ftype, name, false);
679 : 39 : }
680 [ + + ]: 353 : else if (k == Kind::NULLABLE_TYPE)
681 : : {
682 : 2 : TypeNode ftype = d_nm->mkFunctionType(d_sortType, d_sortType);
683 : 2 : op = getSymbolInternal(k, ftype, "Nullable", false);
684 : 2 : }
685 : : else
686 : : {
687 : 351 : std::map<Kind, Node>::iterator it = d_typeKindToNodeCons.find(k);
688 [ + - ]: 351 : if (it != d_typeKindToNodeCons.end())
689 : : {
690 : 351 : op = it->second;
691 : : }
692 : : }
693 [ + - ]: 401 : if (!op.isNull())
694 : : {
695 : 401 : tnn = mkApplyUf(op, targs);
696 : : }
697 : : else
698 : : {
699 : 0 : AlwaysAssert(false);
700 : : }
701 : 401 : }
702 [ - + ][ - + ]: 6847 : Assert(!tnn.isNull());
[ - - ]
703 [ + - ]: 6847 : Trace("lfsc-term-process-debug") << "...type as node: " << tnn << std::endl;
704 : 6847 : d_typeAsNode[cur] = tnn;
705 : 13694 : return cur;
706 : 6847 : }
707 : :
708 : 26054 : std::string LfscNodeConverter::getNameForUserName(const std::string& name,
709 : : size_t variant)
710 : : {
711 : : // For user name X, we do cvc.Y, where Y contains an escaped version of X.
712 : : // Specifically, since LFSC does not allow these characters in identifier
713 : : // bodies: "() \t\n\f;", each is replaced with an escape sequence "\xXX"
714 : : // where XX is the zero-padded hex representation of the code point. "\\" is
715 : : // also escaped.
716 : : //
717 : : // See also: https://github.com/cvc5/LFSC/blob/master/src/lexer.flex#L24
718 : : //
719 : : // The "cvc." prefix ensures we do not clash with LFSC definitions.
720 : : //
721 : : // The escaping ensures that all names are valid LFSC identifiers.
722 : 26054 : std::stringstream ss;
723 : 26054 : ss << "cvc";
724 [ + + ]: 26054 : if (variant != 0)
725 : : {
726 : 46 : ss << variant;
727 : : }
728 : 26054 : ss << ".";
729 : 26054 : std::string sanitized = ss.str();
730 : 26054 : size_t found = sanitized.size();
731 : 26054 : sanitized += name;
732 : : // The following sanitizes symbols that are not allowed in LFSC identifiers
733 : : // here, e.g.
734 : : // |a b|
735 : : // is converted to:
736 : : // cvc.a\x20b
737 : : // where "20" is the hex unicode value of " ".
738 : : do
739 : : {
740 : 27301 : found = sanitized.find_first_of("() \t\n\f\\;", found);
741 [ + + ]: 27301 : if (found != std::string::npos)
742 : : {
743 : : // Emit hex sequence
744 : 1247 : std::stringstream seq;
745 : 1247 : seq << "\\x" << std::setbase(16) << std::setfill('0') << std::setw(2)
746 : 1247 : << static_cast<size_t>(sanitized[found]);
747 : 1247 : sanitized.replace(found, 1, seq.str());
748 : : // increment found over the escape
749 : 1247 : found += 3;
750 : 1247 : }
751 [ + + ]: 27301 : } while (found != std::string::npos);
752 : 52108 : return sanitized;
753 : 26054 : }
754 : :
755 : 24485 : std::string LfscNodeConverter::getNameForUserNameOf(Node v)
756 : : {
757 : 24485 : std::string name = v.getName();
758 : 48970 : return getNameForUserNameOfInternal(v.getId(), name);
759 : 24485 : }
760 : :
761 : 26044 : std::string LfscNodeConverter::getNameForUserNameOfInternal(
762 : : uint64_t id, const std::string& name)
763 : : {
764 : 26044 : std::vector<uint64_t>& syms = d_userSymbolList[name];
765 : 26044 : size_t variant = 0;
766 : 26044 : std::vector<uint64_t>::iterator itr = std::find(syms.begin(), syms.end(), id);
767 [ + + ]: 26044 : if (itr != syms.cend())
768 : : {
769 : 6798 : variant = std::distance(syms.begin(), itr);
770 : : }
771 : : else
772 : : {
773 : 19246 : variant = syms.size();
774 : 19246 : syms.push_back(id);
775 : : }
776 : 52088 : return getNameForUserName(name, variant);
777 : : }
778 : :
779 : 2601578 : bool LfscNodeConverter::shouldTraverse(Node n)
780 : : {
781 : 2601578 : Kind k = n.getKind();
782 : : // don't convert bound variable or instantiation pattern list directly
783 [ + + ][ + + ]: 2601578 : if (k == Kind::BOUND_VAR_LIST || k == Kind::INST_PATTERN_LIST)
784 : : {
785 : 10696 : return false;
786 : : }
787 : : // should not traverse internal applications
788 [ + + ]: 2590882 : if (k == Kind::APPLY_UF)
789 : : {
790 [ + + ]: 37404 : if (d_symbols.find(n.getOperator()) != d_symbols.end())
791 : : {
792 : 4133 : return false;
793 : : }
794 : : }
795 : 2586749 : return true;
796 : : }
797 : :
798 : 3255 : Node LfscNodeConverter::maybeMkSkolemFun(Node k)
799 : : {
800 : 3255 : SkolemManager* sm = d_nm->getSkolemManager();
801 : 3255 : SkolemId sfi = SkolemId::NONE;
802 : 3255 : Node cacheVal;
803 : 3255 : TypeNode tn = k.getType();
804 [ + + ]: 3255 : if (sm->isSkolemFunction(k, sfi, cacheVal))
805 : : {
806 [ + + ]: 805 : if (sfi == SkolemId::RE_UNFOLD_POS_COMPONENT)
807 : : {
808 : : // a skolem corresponding to a regular expression unfolding component
809 : : // should print as (skolem_re_unfold_pos t R n) where the skolem is the
810 : : // n^th component for the unfolding of (str.in_re t R).
811 : 100 : TypeNode strType = d_nm->stringType();
812 : 100 : TypeNode reType = d_nm->regExpType();
813 : 100 : TypeNode intType = d_nm->integerType();
814 : 500 : TypeNode reut = d_nm->mkFunctionType({strType, reType, intType}, strType);
815 : 200 : Node sk = getSymbolInternal(k.getKind(), reut, "skolem_re_unfold_pos");
816 [ + - ][ + - ]: 100 : Assert(!cacheVal.isNull() && cacheVal.getKind() == Kind::SEXPR
[ + - ][ + - ]
[ - + ][ - + ]
[ - - ]
817 : : && cacheVal.getNumChildren() == 3);
818 : : // third value is mpz, which is not converted
819 : 300 : return mkApplyUf(
820 [ + + ][ - - ]: 400 : sk, {convert(cacheVal[0]), convert(cacheVal[1]), cacheVal[2]});
821 : 100 : }
822 : : }
823 : 3155 : return Node::null();
824 : 3255 : }
825 : :
826 : 80023 : Node LfscNodeConverter::typeAsNode(TypeNode tni) const
827 : : {
828 : : // should always exist in the cache, as we always run types through
829 : : // postConvertType before calling this method.
830 : 80023 : std::map<TypeNode, Node>::const_iterator it = d_typeAsNode.find(tni);
831 [ - + ][ - + ]: 80023 : AlwaysAssert(it != d_typeAsNode.end()) << "Missing typeAsNode " << tni;
[ - - ]
832 : 160046 : return it->second;
833 : : }
834 : :
835 : 507303 : Node LfscNodeConverter::mkInternalSymbol(const std::string& name,
836 : : TypeNode tn,
837 : : bool useRawSym)
838 : : {
839 : : // use raw symbol so that it is never quoted
840 : : Node sym = useRawSym ? NodeManager::mkRawSymbol(name, tn)
841 [ + + ]: 507303 : : NodeManager::mkBoundVar(name, tn);
842 : 507303 : d_symbols.insert(sym);
843 : 507303 : return sym;
844 : 0 : }
845 : :
846 : 623 : Node LfscNodeConverter::getSymbolInternalFor(Node n,
847 : : const std::string& name,
848 : : bool useRawSym)
849 : : {
850 : 1246 : return getSymbolInternal(n.getKind(), n.getType(), name, useRawSym);
851 : : }
852 : :
853 : 1467421 : Node LfscNodeConverter::getSymbolInternal(Kind k,
854 : : TypeNode tn,
855 : : const std::string& name,
856 : : bool useRawSym)
857 : : {
858 : 1467421 : std::tuple<Kind, TypeNode, std::string> key(k, tn, name);
859 : : std::map<std::tuple<Kind, TypeNode, std::string>, Node>::iterator it =
860 : 1467421 : d_symbolsMap.find(key);
861 [ + + ]: 1467421 : if (it != d_symbolsMap.end())
862 : : {
863 : 1407437 : return it->second;
864 : : }
865 : 59984 : Node sym = mkInternalSymbol(name, tn, useRawSym);
866 : 59984 : d_symbolToBuiltinKind[sym] = k;
867 : 59984 : d_symbolsMap[key] = sym;
868 : 59984 : return sym;
869 : 1467421 : }
870 : :
871 : 1467 : void LfscNodeConverter::getCharVectorInternal(Node c, std::vector<Node>& chars)
872 : : {
873 [ - + ][ - + ]: 1467 : Assert(c.getKind() == Kind::CONST_STRING);
[ - - ]
874 : 1467 : const std::vector<unsigned>& vec = c.getConst<String>().getVec();
875 [ + + ]: 1467 : if (vec.size() == 0)
876 : : {
877 : 1246 : Node ec = getSymbolInternalFor(c, "emptystr");
878 : 623 : chars.push_back(ec);
879 : 623 : return;
880 : 623 : }
881 : : // Use intType to ensure deterministic node ID assignments
882 : 844 : TypeNode intType = d_nm->integerType();
883 : 844 : TypeNode tnc = d_nm->mkFunctionType(intType, c.getType());
884 : 1688 : Node aconstf = getSymbolInternal(Kind::CONST_STRING, tnc, "char");
885 [ + + ]: 4594 : for (unsigned i = 0, size = vec.size(); i < size; i++)
886 : : {
887 : 15000 : Node cc = mkApplyUf(aconstf, {d_nm->mkConstInt(Rational(vec[i]))});
888 : 3750 : chars.push_back(cc);
889 : 3750 : }
890 : 844 : }
891 : :
892 : 1481 : Node LfscNodeConverter::convertBitVector(const BitVector& bv)
893 : : {
894 : 1481 : TypeNode btn = d_nm->booleanType();
895 : 5924 : TypeNode btnv = d_nm->mkFunctionType({btn, btn}, btn);
896 : 1481 : size_t w = bv.getSize();
897 : 2962 : Node ret = getSymbolInternal(Kind::CONST_BITVECTOR, btn, "bvn");
898 : 2962 : Node b0 = getSymbolInternal(Kind::CONST_BITVECTOR, btn, "b0");
899 : 2962 : Node b1 = getSymbolInternal(Kind::CONST_BITVECTOR, btn, "b1");
900 : 2962 : Node bvc = getSymbolInternal(Kind::CONST_BITVECTOR, btnv, "bvc");
901 [ + + ]: 23539 : for (size_t i = 0; i < w; i++)
902 : : {
903 [ + + ]: 22058 : Node arg = bv.isBitSet((w - 1) - i) ? b1 : b0;
904 [ + + ][ - - ]: 66174 : ret = mkApplyUf(bvc, {arg, ret});
905 : 22058 : }
906 : 2962 : return ret;
907 : 1481 : }
908 : :
909 : 845164 : Node LfscNodeConverter::getNullTerminator(NodeManager* nm, Kind k, TypeNode tn)
910 : : {
911 : 845164 : Node nullTerm;
912 [ + + ][ + + ]: 845164 : switch (k)
[ + ]
913 : : {
914 : : // LFSC signature expects mixed arithmetic for null terminators
915 : 91791 : case Kind::ADD: nullTerm = nm->mkConstInt(Rational(0)); break;
916 : 27688 : case Kind::MULT:
917 : 27688 : case Kind::NONLINEAR_MULT: nullTerm = nm->mkConstInt(Rational(1)); break;
918 : 368 : case Kind::REGEXP_CONCAT:
919 : : // the language containing only the empty string, which has special
920 : : // syntax in LFSC
921 : 368 : nullTerm = getSymbolInternal(k, tn, "re.empty");
922 : 368 : break;
923 : 9282 : case Kind::BITVECTOR_CONCAT:
924 : : {
925 : : // the null terminator of bitvector concat is a dummy variable of
926 : : // bit-vector type with zero width, regardless of the type of the overall
927 : : // concat.
928 : 9282 : TypeNode bvz = d_nm->mkBitVectorType(0);
929 : 9282 : nullTerm = getSymbolInternal(k, bvz, "emptybv");
930 : 9282 : }
931 : 9282 : break;
932 : 716035 : default:
933 : : // no special handling, or not null terminated
934 : 716035 : break;
935 : : }
936 [ + + ]: 845164 : if (!nullTerm.isNull())
937 : : {
938 : 129129 : return nullTerm;
939 : : }
940 : : // otherwise, fall back to standard utility
941 : 716035 : return expr::getNullTerminator(nm, k, tn);
942 : 845164 : }
943 : :
944 : 0 : Kind LfscNodeConverter::getBuiltinKindForInternalSymbol(Node op) const
945 : : {
946 : 0 : std::map<Node, Kind>::const_iterator it = d_symbolToBuiltinKind.find(op);
947 [ - - ]: 0 : if (it != d_symbolToBuiltinKind.end())
948 : : {
949 : 0 : return it->second;
950 : : }
951 : 0 : return Kind::UNDEFINED_KIND;
952 : : }
953 : :
954 : 419047 : Node LfscNodeConverter::getOperatorOfTerm(Node n, bool macroApply)
955 : : {
956 [ - + ][ - + ]: 419047 : Assert(n.hasOperator());
[ - - ]
957 [ - + ][ - + ]: 419047 : Assert(!n.isClosure());
[ - - ]
958 : 419047 : Kind k = n.getKind();
959 : 419047 : std::stringstream opName;
960 [ + - ]: 838094 : Trace("lfsc-term-process-debug2")
961 : 0 : << "getOperatorOfTerm " << n << " " << k << " "
962 : 0 : << (n.getMetaKind() == metakind::PARAMETERIZED) << " "
963 : 419047 : << GenericOp::isIndexedOperatorKind(k) << std::endl;
964 [ + + ]: 419047 : if (n.getMetaKind() == metakind::PARAMETERIZED)
965 : : {
966 : 85724 : Node op = n.getOperator();
967 : 85724 : std::vector<Node> indices;
968 [ + + ]: 85724 : if (GenericOp::isIndexedOperatorKind(k))
969 : : {
970 : 15398 : indices = GenericOp::getIndicesForOperator(k, n.getOperator());
971 : : // we must convert the name of indices on updaters and testers
972 [ + + ][ + + ]: 15398 : if (k == Kind::APPLY_UPDATER || k == Kind::APPLY_TESTER)
973 : : {
974 [ - + ][ - + ]: 857 : Assert(indices.size() == 1);
[ - - ]
975 : : // must convert to user name
976 : 857 : TypeNode intType = d_nm->integerType();
977 : 857 : indices[0] =
978 : 1714 : getSymbolInternal(k, intType, getNameForUserNameOf(indices[0]));
979 : 857 : }
980 : : }
981 [ + + ]: 70326 : else if (op.getType().isFunction())
982 : : {
983 : 64385 : return op;
984 : : }
985 : : // note other kinds of functions (e.g. selectors and testers)
986 : 21339 : std::vector<TypeNode> argTypes;
987 [ + + ]: 46513 : for (const Node& nc : n)
988 : : {
989 : 25174 : argTypes.push_back(nc.getType());
990 : 25174 : }
991 : 21339 : TypeNode ftype = n.getType();
992 [ + + ]: 21339 : if (!argTypes.empty())
993 : : {
994 : 21186 : ftype = d_nm->mkFunctionType(argTypes, ftype);
995 : : }
996 : 21339 : Node ret;
997 [ + + ]: 21339 : if (GenericOp::isIndexedOperatorKind(k))
998 : : {
999 : 15398 : std::vector<TypeNode> itypes;
1000 [ + + ]: 34736 : for (const Node& i : indices)
1001 : : {
1002 : 19338 : itypes.push_back(i.getType());
1003 : : }
1004 [ + - ]: 15398 : if (!itypes.empty())
1005 : : {
1006 : 15398 : ftype = d_nm->mkFunctionType(itypes, ftype);
1007 : : }
1008 [ + + ]: 15398 : if (!macroApply)
1009 : : {
1010 [ + + ][ + + ]: 2249 : if (k != Kind::APPLY_UPDATER && k != Kind::APPLY_TESTER)
1011 : : {
1012 : 2167 : opName << "f_";
1013 : : }
1014 : : }
1015 : : // must avoid overloading for to_fp variants
1016 [ + + ]: 15398 : if (k == Kind::FLOATINGPOINT_TO_FP_FROM_FP)
1017 : : {
1018 : 1 : opName << "to_fp_fp";
1019 : : }
1020 [ - + ]: 15397 : else if (k == Kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV)
1021 : : {
1022 : 0 : opName << "to_fp_ieee_bv";
1023 : : }
1024 [ + + ]: 15397 : else if (k == Kind::FLOATINGPOINT_TO_FP_FROM_SBV)
1025 : : {
1026 : 10 : opName << "to_fp_sbv";
1027 : : }
1028 [ + + ]: 15387 : else if (k == Kind::FLOATINGPOINT_TO_FP_FROM_REAL)
1029 : : {
1030 : 2 : opName << "to_fp_real";
1031 : : }
1032 [ + + ]: 15385 : else if (k == Kind::BITVECTOR_BIT)
1033 : : {
1034 : 4170 : opName << "bit";
1035 : : }
1036 [ + + ]: 11215 : else if (k == Kind::DIVISIBLE)
1037 : : {
1038 : 2 : opName << "a.divisible";
1039 : : }
1040 : : else
1041 : : {
1042 : 11213 : opName << printer::smt2::Smt2Printer::smtKindString(k);
1043 : : }
1044 : 15398 : }
1045 [ + + ]: 5941 : else if (k == Kind::APPLY_CONSTRUCTOR)
1046 : : {
1047 : 3686 : unsigned index = DType::indexOf(op);
1048 : 3686 : const DType& dt = DType::datatypeOf(op);
1049 : : // get its variable name
1050 : 3686 : opName << getNameForUserNameOf(dt[index].getConstructor());
1051 : : }
1052 [ + - ]: 2255 : else if (k == Kind::APPLY_SELECTOR)
1053 : : {
1054 : 2255 : ret = maybeMkSkolemFun(op);
1055 [ + - ]: 2255 : if (ret.isNull())
1056 : : {
1057 : 2255 : unsigned index = DType::indexOf(op);
1058 : 2255 : const DType& dt = DType::datatypeOf(op);
1059 : 2255 : unsigned cindex = DType::cindexOf(op);
1060 : 2255 : opName << getNameForUserNameOf(dt[cindex][index].getSelector());
1061 : : }
1062 : : }
1063 [ - - ][ - - ]: 0 : else if (k == Kind::SET_SINGLETON || k == Kind::BAG_MAKE
1064 [ - - ]: 0 : || k == Kind::SEQ_UNIT)
1065 : : {
1066 [ - - ]: 0 : if (!macroApply)
1067 : : {
1068 : 0 : opName << "f_";
1069 : : }
1070 : 0 : opName << printer::smt2::Smt2Printer::smtKindString(k);
1071 : : }
1072 : : else
1073 : : {
1074 : 0 : opName << op;
1075 : : }
1076 [ + - ]: 21339 : if (ret.isNull())
1077 : : {
1078 [ + - ]: 21339 : Trace("lfsc-term-process-debug2") << "...default symbol" << std::endl;
1079 : 21339 : ret = getSymbolInternal(k, ftype, opName.str());
1080 : : }
1081 : : // if indexed, apply to index
1082 [ + + ]: 21339 : if (!indices.empty())
1083 : : {
1084 : 15398 : ret = mkApplyUf(ret, indices);
1085 : : }
1086 [ + - ]: 21339 : Trace("lfsc-term-process-debug2") << "...return " << ret << std::endl;
1087 : 21339 : return ret;
1088 : 85724 : }
1089 : 333323 : std::vector<TypeNode> argTypes;
1090 [ + + ]: 1126654 : for (const Node& nc : n)
1091 : : {
1092 : 793331 : argTypes.push_back(nc.getType());
1093 : 793331 : }
1094 : : // we only use binary operators
1095 [ + + ]: 333323 : if (NodeManager::isNAryKind(k))
1096 : : {
1097 : 150363 : argTypes.resize(2);
1098 : : }
1099 : 333323 : TypeNode tn = n.getType();
1100 : 333323 : TypeNode ftype = d_nm->mkFunctionType(argTypes, tn);
1101 : : // most functions are called f_X where X is the SMT-LIB name, if we are
1102 : : // getting the macroApply variant, then we don't prefix with `f_`.
1103 [ + + ]: 333323 : if (!macroApply)
1104 : : {
1105 : 257962 : opName << "f_";
1106 : : }
1107 [ + + ]: 333323 : if (k == Kind::FLOATINGPOINT_COMPONENT_NAN
1108 [ + + ]: 333321 : || k == Kind::FLOATINGPOINT_COMPONENT_INF
1109 [ + + ]: 333320 : || k == Kind::FLOATINGPOINT_COMPONENT_ZERO
1110 [ + + ]: 333319 : || k == Kind::FLOATINGPOINT_COMPONENT_SIGN
1111 [ + + ]: 333317 : || k == Kind::FLOATINGPOINT_COMPONENT_EXPONENT
1112 [ + + ]: 333316 : || k == Kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND
1113 [ - + ]: 333315 : || k == Kind::ROUNDINGMODE_BITBLAST)
1114 : : {
1115 : : // remove @fp.
1116 : 8 : std::string str = printer::smt2::Smt2Printer::smtKindString(k);
1117 : 8 : opName << str.substr(4);
1118 : 8 : }
1119 : : else
1120 : : {
1121 : : // all arithmetic kinds must explicitly deal with real vs int subtyping
1122 [ + + ][ + + ]: 333315 : if (k == Kind::ADD || k == Kind::MULT || k == Kind::NONLINEAR_MULT
[ + + ]
1123 [ + + ][ + + ]: 252126 : || k == Kind::GEQ || k == Kind::GT || k == Kind::LEQ || k == Kind::LT
[ + + ][ + + ]
1124 [ + + ][ + + ]: 169041 : || k == Kind::SUB || k == Kind::DIVISION || k == Kind::DIVISION_TOTAL
[ + + ]
1125 [ + + ][ + + ]: 166514 : || k == Kind::INTS_DIVISION || k == Kind::INTS_DIVISION_TOTAL
1126 [ + + ][ + + ]: 165902 : || k == Kind::INTS_MODULUS || k == Kind::INTS_MODULUS_TOTAL
1127 [ + + ][ + + ]: 165327 : || k == Kind::NEG || k == Kind::POW)
1128 : : {
1129 : : // currently allow subtyping
1130 : 168625 : opName << "a.";
1131 : : }
1132 [ + + ]: 333315 : if (k == Kind::NEG)
1133 : : {
1134 : 634 : opName << "u";
1135 : : }
1136 : 333315 : opName << printer::smt2::Smt2Printer::smtKindString(k);
1137 : : }
1138 : 333323 : return getSymbolInternal(k, ftype, opName.str());
1139 : 419047 : }
1140 : :
1141 : 51398 : Node LfscNodeConverter::getOperatorOfClosure(Node q,
1142 : : bool macroApply,
1143 : : bool isPartial)
1144 : : {
1145 : 51398 : TypeNode retType = isPartial ? q[1].getType() : q.getType();
1146 : 102796 : TypeNode bodyType = d_nm->mkFunctionType(q[1].getType(), retType);
1147 : : // We permit non-flat function types here
1148 : : // intType is used here for variable indices
1149 : 51398 : TypeNode intType = d_nm->integerType();
1150 : 205592 : TypeNode ftype = d_nm->mkFunctionType({intType, d_sortType}, bodyType);
1151 : 51398 : Kind k = q.getKind();
1152 : 51398 : std::stringstream opName;
1153 [ + + ]: 51398 : if (!macroApply)
1154 : : {
1155 : 8390 : opName << "f_";
1156 : : }
1157 : 51398 : opName << printer::smt2::Smt2Printer::smtKindString(k);
1158 : 102796 : return getSymbolInternal(k, ftype, opName.str());
1159 : 51398 : }
1160 : :
1161 : 60776 : Node LfscNodeConverter::getOperatorOfBoundVar(Node cop, Node v)
1162 : : {
1163 : 121552 : Node x = d_nm->mkConstInt(Rational(getOrAssignIndexForBVar(v)));
1164 : 121552 : Node tc = typeAsNode(convertType(v.getType()));
1165 [ + + ][ - - ]: 243104 : return mkApplyUf(cop, {x, tc});
1166 : 60776 : }
1167 : :
1168 : 16541 : size_t LfscNodeConverter::getOrAssignIndexForFVar(Node fv)
1169 : : {
1170 : 16541 : std::map<Node, size_t>::iterator it = d_fvarIndex.find(fv);
1171 [ - + ]: 16541 : if (it != d_fvarIndex.end())
1172 : : {
1173 : 0 : return it->second;
1174 : : }
1175 : 16541 : size_t id = d_fvarIndex.size();
1176 : 16541 : d_fvarIndex[fv] = id;
1177 : 16541 : return id;
1178 : : }
1179 : :
1180 : 70489 : size_t LfscNodeConverter::getOrAssignIndexForBVar(Node bv)
1181 : : {
1182 [ - + ][ - + ]: 70489 : Assert(bv.isVar());
[ - - ]
1183 : 70489 : std::map<Node, size_t>::iterator it = d_bvarIndex.find(bv);
1184 [ + + ]: 70489 : if (it != d_bvarIndex.end())
1185 : : {
1186 : 59949 : return it->second;
1187 : : }
1188 : 10540 : size_t id = d_bvarIndex.size();
1189 : 10540 : d_bvarIndex[bv] = id;
1190 : 10540 : return id;
1191 : : }
1192 : :
1193 : 1723 : const std::unordered_set<Node>& LfscNodeConverter::getDeclaredSymbols() const
1194 : : {
1195 : 1723 : return d_declVars;
1196 : : }
1197 : :
1198 : 1723 : const std::unordered_set<TypeNode>& LfscNodeConverter::getDeclaredTypes() const
1199 : : {
1200 : 1723 : return d_declTypes;
1201 : : }
1202 : :
1203 : : } // namespace proof
1204 : : } // namespace cvc5::internal
|
