Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Aina Niemetz, Abdalrhman Mohamed
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * Implementation of LFSC node conversion
14 : : */
15 : :
16 : : #include "proof/lfsc/lfsc_node_converter.h"
17 : :
18 : : #include <algorithm>
19 : : #include <iomanip>
20 : : #include <sstream>
21 : :
22 : : #include "expr/array_store_all.h"
23 : : #include "expr/cardinality_constraint.h"
24 : : #include "expr/dtype.h"
25 : : #include "expr/dtype_cons.h"
26 : : #include "expr/nary_term_util.h"
27 : : #include "expr/sequence.h"
28 : : #include "expr/skolem_manager.h"
29 : : #include "printer/smt2/smt2_printer.h"
30 : : #include "theory/builtin/generic_op.h"
31 : : #include "theory/bv/theory_bv_utils.h"
32 : : #include "theory/datatypes/datatypes_rewriter.h"
33 : : #include "theory/strings/word.h"
34 : : #include "theory/uf/function_const.h"
35 : : #include "theory/uf/theory_uf_rewriter.h"
36 : : #include "util/bitvector.h"
37 : : #include "util/finite_field_value.h"
38 : : #include "util/floatingpoint.h"
39 : : #include "util/iand.h"
40 : : #include "util/rational.h"
41 : : #include "util/regexp.h"
42 : : #include "util/string.h"
43 : :
44 : : using namespace cvc5::internal::kind;
45 : :
46 : : namespace cvc5::internal {
47 : : namespace proof {
48 : :
49 : 1417 : LfscNodeConverter::LfscNodeConverter(NodeManager* nm) : NodeConverter(nm)
50 : : {
51 : 1417 : d_arrow = nm->mkSortConstructor("arrow", 2);
52 : :
53 : 1417 : d_sortType = nm->mkSort("sortType");
54 : : // the embedding of arrow into Node, which is binary constructor over sorts
55 : 7085 : TypeNode anfType = nm->mkFunctionType({d_sortType, d_sortType}, d_sortType);
56 : 1417 : d_typeAsNode[d_arrow] =
57 : 2834 : getSymbolInternal(Kind::FUNCTION_TYPE, anfType, "arrow");
58 : :
59 : 2834 : TypeNode intType = nm->integerType();
60 : 7085 : TypeNode arrType = nm->mkFunctionType({d_sortType, d_sortType}, d_sortType);
61 : 1417 : d_typeKindToNodeCons[Kind::ARRAY_TYPE] =
62 : 2834 : getSymbolInternal(Kind::FUNCTION_TYPE, arrType, "Array");
63 : 2834 : TypeNode bvType = nm->mkFunctionType(intType, d_sortType);
64 : 1417 : d_typeKindToNodeCons[Kind::BITVECTOR_TYPE] =
65 : 2834 : getSymbolInternal(Kind::FUNCTION_TYPE, bvType, "BitVec");
66 : 7085 : TypeNode fpType = nm->mkFunctionType({intType, intType}, d_sortType);
67 : 1417 : d_typeKindToNodeCons[Kind::FLOATINGPOINT_TYPE] =
68 : 2834 : getSymbolInternal(Kind::FUNCTION_TYPE, fpType, "FloatingPoint");
69 : 1417 : TypeNode setType = nm->mkFunctionType(d_sortType, d_sortType);
70 : 1417 : d_typeKindToNodeCons[Kind::SET_TYPE] =
71 : 2834 : getSymbolInternal(Kind::FUNCTION_TYPE, setType, "Set");
72 : 1417 : d_typeKindToNodeCons[Kind::BAG_TYPE] =
73 : 2834 : getSymbolInternal(Kind::FUNCTION_TYPE, setType, "Bag");
74 : 1417 : d_typeKindToNodeCons[Kind::SEQUENCE_TYPE] =
75 : 2834 : getSymbolInternal(Kind::FUNCTION_TYPE, setType, "Seq");
76 : 1417 : }
77 : :
78 : 2193070 : Node LfscNodeConverter::preConvert(Node n)
79 : : {
80 : : // match is not supported in LFSC syntax, we eliminate it at pre-order
81 : : // traversal, which avoids type-checking errors during conversion, since e.g.
82 : : // match case nodes are required but cannot be preserved
83 [ + + ]: 2193070 : if (n.getKind() == Kind::MATCH)
84 : : {
85 : 2 : return theory::datatypes::DatatypesRewriter::expandMatch(n);
86 : : }
87 : 2193070 : return n;
88 : : }
89 : :
90 : 2186060 : Node LfscNodeConverter::postConvert(Node n)
91 : : {
92 : 2186060 : Kind k = n.getKind();
93 : : // we eliminate MATCH at preConvert above
94 [ - + ][ - + ]: 2186060 : Assert(k != Kind::MATCH);
[ - - ]
95 [ + + ]: 2186060 : if (k == Kind::ASCRIPTION_TYPE)
96 : : {
97 : : // dummy node, return it
98 : 11 : return n;
99 : : }
100 : 4372110 : TypeNode tn = n.getType();
101 [ + - ]: 4372110 : Trace("lfsc-term-process-debug")
102 : 2186050 : << "postConvert " << n << " " << k << std::endl;
103 [ + + ]: 2186050 : if (k == Kind::BOUND_VARIABLE)
104 : : {
105 [ - + ]: 7790 : if (d_symbols.find(n) != d_symbols.end())
106 : : {
107 : : // ignore internally generated symbols
108 : 0 : return n;
109 : : }
110 : : // bound variable v is (bvar x T)
111 : 15580 : TypeNode intType = d_nm->integerType();
112 : 23370 : Node x = d_nm->mkConstInt(Rational(getOrAssignIndexForBVar(n)));
113 : 23370 : Node tc = typeAsNode(convertType(tn));
114 : 38950 : TypeNode ftype = d_nm->mkFunctionType({intType, d_sortType}, tn);
115 : 15580 : Node bvarOp = getSymbolInternal(k, ftype, "bvar");
116 [ + + ][ - - ]: 23370 : return mkApplyUf(bvarOp, {x, tc});
117 : : }
118 [ + + ]: 2178260 : else if (k == Kind::RAW_SYMBOL)
119 : : {
120 : : // ignore internally generated symbols
121 : 10293 : return n;
122 : : }
123 [ + + ][ + + ]: 2167970 : else if (k == Kind::SKOLEM || k == Kind::DUMMY_SKOLEM)
124 : : {
125 : : // constructors/selectors are represented by skolems, which are defined
126 : : // symbols
127 [ + + ]: 10139 : if (tn.isDatatypeConstructor() || tn.isDatatypeSelector()
128 [ + + ][ + + ]: 10139 : || tn.isDatatypeTester() || tn.isDatatypeUpdater())
[ + + ][ + + ]
129 : : {
130 : : // note these are not converted to their user named (cvc.) symbols here,
131 : : // to avoid type errors when constructing terms for postConvert
132 : 746 : return n;
133 : : }
134 : : // skolems v print as their original forms
135 : : // v is (skolem W) where W is the original or original form of v
136 : 8972 : Node wi = SkolemManager::getUnpurifiedForm(n);
137 [ + - ][ + + ]: 4486 : if (!wi.isNull() && wi != n)
[ + + ]
138 : : {
139 [ + - ]: 7286 : Trace("lfsc-term-process-debug")
140 : 3643 : << "...original form " << wi << std::endl;
141 : 3643 : wi = convert(wi);
142 [ + - ]: 7286 : Trace("lfsc-term-process-debug")
143 : 3643 : << "...converted original for " << wi << std::endl;
144 : 7286 : TypeNode ftype = d_nm->mkFunctionType(tn, tn);
145 : 7286 : Node skolemOp = getSymbolInternal(k, ftype, "skolem");
146 : 7286 : return mkApplyUf(skolemOp, {wi});
147 : : }
148 : : // might be a skolem function
149 : 1686 : Node ns = maybeMkSkolemFun(n);
150 [ + + ]: 843 : if (!ns.isNull())
151 : : {
152 : 85 : return ns;
153 : : }
154 : : // Otherwise, it is an uncategorized skolem, must use a fresh variable.
155 : : // This case will only apply for terms originating from places with no
156 : : // proof support. Note it is not added as a declared variable, instead it
157 : : // is used as (var N T) throughout.
158 : 1516 : TypeNode intType = d_nm->integerType();
159 : 3790 : TypeNode varType = d_nm->mkFunctionType({intType, d_sortType}, tn);
160 : 2274 : Node var = mkInternalSymbol("var", varType);
161 : 2274 : Node index = d_nm->mkConstInt(Rational(getOrAssignIndexForFVar(n)));
162 : 1516 : Node tc = typeAsNode(convertType(tn));
163 [ + + ][ - - ]: 2274 : return mkApplyUf(var, {index, tc});
164 : : }
165 [ + + ]: 2162740 : else if (n.isVar())
166 : : {
167 : 15467 : d_declVars.insert(n);
168 : 30934 : return mkInternalSymbol(getNameForUserNameOf(n), tn);
169 : : }
170 [ + + ]: 2147270 : else if (k == Kind::CARDINALITY_CONSTRAINT)
171 : : {
172 [ + - ]: 16 : Trace("lfsc-term-process-debug")
173 : 8 : << "...convert cardinality constraint" << std::endl;
174 : : const CardinalityConstraint& cc =
175 : 8 : n.getOperator().getConst<CardinalityConstraint>();
176 : 24 : Node tnn = typeAsNode(convertType(cc.getType()));
177 : 16 : Node ub = d_nm->mkConstInt(Rational(cc.getUpperBound()));
178 : 8 : TypeNode tnc = d_nm->mkFunctionType({tnn.getType(), ub.getType()},
179 : 48 : d_nm->booleanType());
180 : 16 : Node fcard = getSymbolInternal(k, tnc, "fmf.card");
181 [ + + ][ - - ]: 24 : return mkApplyUf(fcard, {tnn, ub});
182 : : }
183 [ + + ]: 2147260 : else if (k == Kind::APPLY_UF)
184 : : {
185 : 69554 : return convert(theory::uf::TheoryUfRewriter::getHoApplyForApplyUf(n));
186 : : }
187 [ + + ][ + + ]: 2112490 : else if (k == Kind::APPLY_CONSTRUCTOR || k == Kind::APPLY_SELECTOR
188 [ + + ][ + + ]: 2109400 : || k == Kind::APPLY_TESTER || k == Kind::APPLY_UPDATER)
189 : : {
190 : : // must add to declared types
191 : 3598 : const DType& dt = DType::datatypeOf(n.getOperator());
192 : 3598 : d_declTypes.insert(dt.getTypeNode());
193 : : // must convert other kinds of apply to functions, since we convert to
194 : : // HO_APPLY
195 : 7196 : Node opc = getOperatorOfTerm(n, true);
196 [ + + ]: 3598 : if (n.getNumChildren() == 0)
197 : : {
198 : 97 : return opc;
199 : : }
200 : 7002 : return postConvert(mkApplyUf(opc, std::vector<Node>(n.begin(), n.end())));
201 : : }
202 [ + + ]: 2108890 : else if (k == Kind::HO_APPLY)
203 : : {
204 : 1158760 : std::vector<TypeNode> argTypes;
205 : 579378 : argTypes.push_back(n[0].getType());
206 : 579378 : argTypes.push_back(n[1].getType());
207 : 1158760 : TypeNode tnh = d_nm->mkFunctionType(argTypes, tn);
208 : 1158760 : Node hconstf = getSymbolInternal(k, tnh, "apply");
209 [ + + ][ - - ]: 1738130 : return mkApplyUf(hconstf, {n[0], n[1]});
210 : : }
211 [ + + ][ + + ]: 1529510 : else if (k == Kind::CONST_RATIONAL || k == Kind::CONST_INTEGER)
212 : : {
213 : 37986 : TypeNode tnv = d_nm->mkFunctionType(tn, tn);
214 : 37986 : Node rconstf;
215 : 37986 : Node arg;
216 : 18993 : Rational r = n.getConst<Rational>();
217 [ + + ]: 18993 : if (tn.isInteger())
218 : : {
219 : 15441 : rconstf = getSymbolInternal(k, tnv, "int");
220 [ + + ]: 15441 : if (r.sgn() == -1)
221 : : {
222 : : // use LFSC syntax for mpz negation
223 : 3346 : Node mpzn = getSymbolInternal(k, d_nm->mkFunctionType(tn, tn), "~");
224 : 3346 : arg = mkApplyUf(mpzn, {d_nm->mkConstInt(r.abs())});
225 : : }
226 : : else
227 : : {
228 : 13768 : arg = n;
229 : : }
230 : : }
231 : : else
232 : : {
233 : 3552 : 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 : 7104 : std::stringstream ss;
238 : 3552 : ss << "__LFSC_TMP" << r.getNumerator().abs() << "/" << r.getDenominator();
239 : 3552 : arg = mkInternalSymbol(ss.str(), tn);
240 : : // negative (~ n/m)
241 [ + + ]: 3552 : if (r.sgn() == -1)
242 : : {
243 : 3366 : Node mpzn = getSymbolInternal(k, d_nm->mkFunctionType(tn, tn), "~");
244 : 3366 : arg = mkApplyUf(mpzn, {arg});
245 : : }
246 : : }
247 : 37986 : return mkApplyUf(rconstf, {arg});
248 : : }
249 [ + + ]: 1510520 : else if (k == Kind::CONST_BITVECTOR)
250 : : {
251 : 2274 : TypeNode btn = d_nm->booleanType();
252 : 2274 : TypeNode tnv = d_nm->mkFunctionType(btn, tn);
253 : 2274 : BitVector bv = n.getConst<BitVector>();
254 : 2274 : Node ret = convertBitVector(bv);
255 : 2274 : Node bconstf = getSymbolInternal(k, tnv, "bv");
256 : 2274 : return mkApplyUf(bconstf, {ret});
257 : : }
258 [ + + ]: 1509380 : else if (k == Kind::CONST_FLOATINGPOINT)
259 : : {
260 : 38 : BitVector s, e, i;
261 : 19 : n.getConst<FloatingPoint>().getIEEEBitvectors(s, e, i);
262 : 38 : Node sn = convert(d_nm->mkConst(s));
263 : 38 : Node en = convert(d_nm->mkConst(e));
264 : 38 : Node in = convert(d_nm->mkConst(i));
265 : : TypeNode tnv =
266 : 114 : 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 : : }
270 [ + + ]: 1509360 : else if (k == Kind::CONST_FINITE_FIELD)
271 : : {
272 : 81 : const FiniteFieldValue& ffv = n.getConst<FiniteFieldValue>();
273 : 243 : Node v = convert(d_nm->mkConstInt(ffv.getValue()));
274 : 243 : Node fs = convert(d_nm->mkConstInt(ffv.getFieldSize()));
275 : 405 : 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 : : }
279 [ + + ]: 1509280 : 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 : 1940 : std::vector<Node> charVec;
285 : 970 : getCharVectorInternal(n, charVec);
286 [ - + ][ - + ]: 970 : Assert(!charVec.empty());
[ - - ]
287 [ + + ]: 970 : if (charVec.size() == 1)
288 : : {
289 : : // handles empty string and singleton character
290 : 701 : return charVec[0];
291 : : }
292 : 269 : std::reverse(charVec.begin(), charVec.end());
293 : 807 : Node ret = postConvert(getNullTerminator(Kind::STRING_CONCAT, tn));
294 [ + + ]: 2891 : for (size_t i = 0, size = charVec.size(); i < size; i++)
295 : : {
296 : 2622 : ret = d_nm->mkNode(Kind::STRING_CONCAT, charVec[i], ret);
297 : : }
298 : 269 : return ret;
299 : : }
300 [ + + ]: 1508310 : else if (k == Kind::CONST_SEQUENCE)
301 : : {
302 : 53 : const std::vector<Node>& charVec = n.getConst<Sequence>().getVec();
303 : 106 : TypeNode etype = d_nm->mkFunctionType(d_sortType, tn);
304 : 159 : Node ret = getSymbolInternal(k, etype, "seq.empty");
305 : 106 : ret = mkApplyUf(ret, {typeAsNode(convertType(tn))});
306 : 106 : std::vector<Node> vecu;
307 [ + + ]: 83 : for (size_t i = 0, size = charVec.size(); i < size; i++)
308 : : {
309 : : Node u =
310 : 106 : d_nm->mkNode(Kind::SEQ_UNIT, postConvert(charVec[size - (i + 1)]));
311 [ + + ]: 53 : if (size == 1)
312 : : {
313 : : // singleton case
314 : 23 : return u;
315 : : }
316 : 30 : ret = d_nm->mkNode(Kind::STRING_CONCAT, u, ret);
317 : : }
318 : 30 : return ret;
319 : : }
320 [ + + ]: 1508260 : else if (k == Kind::STORE_ALL)
321 : : {
322 : 57 : Node t = typeAsNode(convertType(tn));
323 : 38 : TypeNode caRetType = d_nm->mkFunctionType(tn.getArrayConstituentType(), tn);
324 : 38 : TypeNode catype = d_nm->mkFunctionType(d_sortType, caRetType);
325 : 57 : Node bconstf = getSymbolInternal(k, catype, "array_const");
326 : 76 : Node f = mkApplyUf(bconstf, {t});
327 : 19 : ArrayStoreAll storeAll = n.getConst<ArrayStoreAll>();
328 : 38 : return mkApplyUf(f, {convert(storeAll.getValue())});
329 : : }
330 [ + + ][ + + ]: 1487430 : else if (k == Kind::GEQ || k == Kind::GT || k == Kind::LEQ || k == Kind::LT
[ + + ]
331 [ + + ][ + + ]: 1453230 : || k == Kind::SUB || k == Kind::DIVISION || k == Kind::DIVISION_TOTAL
[ + + ]
332 [ + + ][ + + ]: 1451070 : || k == Kind::INTS_DIVISION || k == Kind::INTS_DIVISION_TOTAL
333 [ + + ][ + + ]: 1450660 : || k == Kind::INTS_MODULUS || k == Kind::INTS_MODULUS_TOTAL
334 [ + + ][ + + ]: 1450390 : || k == Kind::NEG || k == Kind::POW
335 [ + + ]: 1449860 : || k == Kind::FLOATINGPOINT_COMPONENT_NAN
336 [ + + ]: 1449860 : || k == Kind::FLOATINGPOINT_COMPONENT_INF
337 [ + + ]: 1449860 : || k == Kind::FLOATINGPOINT_COMPONENT_ZERO
338 [ + + ]: 1449860 : || k == Kind::FLOATINGPOINT_COMPONENT_SIGN
339 [ + + ]: 1449860 : || k == Kind::FLOATINGPOINT_COMPONENT_EXPONENT
340 [ + + ]: 1449860 : || k == Kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND
341 [ + - ]: 1449850 : || k == Kind::ROUNDINGMODE_BITBLAST
342 [ + + ][ + + ]: 2995670 : || 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 : 67830 : Node opc = getOperatorOfTerm(n, true);
348 : 67830 : return mkApplyUf(opc, std::vector<Node>(n.begin(), n.end()));
349 : : }
350 [ + + ][ + + ]: 1440410 : else if (k == Kind::SET_EMPTY || k == Kind::SET_UNIVERSE
351 [ + + ]: 1440340 : || k == Kind::BAG_EMPTY)
352 : : {
353 : 225 : Node t = typeAsNode(convertType(tn));
354 : 150 : TypeNode etype = d_nm->mkFunctionType(d_sortType, tn);
355 : : Node ef = getSymbolInternal(
356 : : k,
357 : : etype,
358 : 75 : k == Kind::SET_EMPTY
359 : : ? "set.empty"
360 [ + + ][ + + ]: 150 : : (k == Kind::SET_UNIVERSE ? "set.universe" : "bag.empty"));
361 : 150 : return mkApplyUf(ef, {t});
362 : : }
363 [ + + ]: 1440330 : 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 : 31858 : Node ret = n[1];
369 : 31858 : Node cop = getOperatorOfClosure(n, true);
370 : 31858 : Node pcop = getOperatorOfClosure(n, true, true);
371 [ + + ]: 58599 : for (size_t i = 0, nchild = n[0].getNumChildren(); i < nchild; i++)
372 : : {
373 : 42670 : size_t ii = (nchild - 1) - i;
374 : 85340 : 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 [ + + ]: 85340 : Node vop = getOperatorOfBoundVar(ii == 0 ? cop : pcop, v);
378 : 85340 : ret = mkApplyUf(vop, {ret});
379 : : }
380 : : // notice that intentionally we drop annotations here
381 : 15929 : return ret;
382 : : }
383 [ + + ]: 1424400 : else if (k == Kind::FUNCTION_ARRAY_CONST)
384 : : {
385 : : // must convert to lambda and then run the conversion
386 : 18 : Node lam = theory::uf::FunctionConst::toLambda(n);
387 [ - + ][ - + ]: 18 : Assert(!lam.isNull());
[ - - ]
388 : 18 : return convert(lam);
389 : : }
390 [ - + ]: 1424390 : 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 : : }
403 [ + + ]: 1424390 : else if (k == Kind::BITVECTOR_FROM_BOOLS)
404 : : {
405 : 5130 : 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 : 5130 : Node curr = getNullTerminator(Kind::BITVECTOR_CONCAT, tn);
410 [ + + ]: 17412 : for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; ++i)
411 : : {
412 : 29694 : TypeNode bvt = d_nm->mkBitVectorType(i + 1);
413 : 74235 : TypeNode ftype = d_nm->mkFunctionType({btn, curr.getType()}, bvt);
414 : 29694 : Node bbt = getSymbolInternal(k, ftype, "from_bools");
415 [ + + ][ - - ]: 44541 : curr = mkApplyUf(bbt, {n[nchild - (i + 1)], curr});
416 : : }
417 : 2565 : return curr;
418 : : }
419 [ + + ]: 1421820 : else if (k == Kind::SEP_NIL)
420 : : {
421 : 9 : Node tnn = typeAsNode(convertType(tn));
422 : 6 : TypeNode ftype = d_nm->mkFunctionType(d_sortType, tn);
423 : 6 : Node s = getSymbolInternal(k, ftype, "sep.nil");
424 : 6 : return mkApplyUf(s, {tnn});
425 : : }
426 [ + + ][ + + ]: 1421820 : else if (NodeManager::isNAryKind(k) && n.getNumChildren() >= 2)
[ + + ]
427 : : {
428 : 436970 : size_t nchild = n.getNumChildren();
429 [ - + ][ - + ]: 436970 : Assert(n.getMetaKind() != metakind::PARAMETERIZED);
[ - - ]
430 : : // convert all n-ary applications to binary
431 : 873940 : std::vector<Node> children(n.begin(), n.end());
432 : : // distinct is special case
433 [ + + ]: 436970 : if (k == Kind::DISTINCT)
434 : : {
435 : : // DISTINCT(x1,...,xn) --->
436 : : // AND(DISTINCT(x1,x2), AND(,..., AND(,..,DISTINCT(x_{n-1},x_n))))
437 : 4269 : Node ret = d_nm->mkNode(k, children[0], children[1]);
438 [ + + ]: 4729 : for (unsigned i = 0; i < nchild; i++)
439 [ + + ]: 15518 : for (unsigned j = i + 1; j < nchild; j++)
440 : : {
441 [ + + ][ + - ]: 12212 : if (i != 0 && j != 1)
442 : : {
443 : 20658 : ret = d_nm->mkNode(
444 : 30987 : Kind::AND, ret, d_nm->mkNode(k, children[i], children[j]));
445 : : }
446 : : }
447 [ + - ]: 2846 : Trace("lfsc-term-process-debug") << "n: " << n << std::endl
448 : 1423 : << "ret: " << ret << std::endl;
449 : 1423 : return ret;
450 : : }
451 : 435547 : 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 : 871094 : Node nullTerm = getNullTerminator(k, tn);
460 : : // Most operators simply get binarized
461 : 871094 : Node ret;
462 : 435547 : size_t istart = 0;
463 [ + + ]: 435547 : if (nullTerm.isNull())
464 : : {
465 : 61 : ret = children[0];
466 : 61 : istart = 1;
467 : : }
468 : : else
469 : : {
470 : : // must convert recursively, since nullTerm may have subterms.
471 : 435486 : 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 : 435547 : bool isArithOp =
476 [ + + ][ + + ]: 435547 : (k == Kind::ADD || k == Kind::MULT || k == Kind::NONLINEAR_MULT);
[ + + ]
477 : 871094 : std::stringstream arithOpName;
478 [ + + ]: 435547 : if (isArithOp)
479 : : {
480 : : // currently allow subtyping
481 : 81553 : arithOpName << "a.";
482 : 81553 : arithOpName << printer::smt2::Smt2Printer::smtKindString(k);
483 : : }
484 : : // now, iterate over children and make binary conversion
485 [ + + ]: 2286580 : for (size_t i = istart, npchild = children.size(); i < npchild; i++)
486 : : {
487 [ + + ]: 1851030 : 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 : 467774 : TypeNode tn1 = children[i].getType();
493 : 467774 : TypeNode tn2 = ret.getType();
494 : 1169440 : TypeNode ftype = d_nm->mkFunctionType({tn1, tn2}, tn);
495 : 467774 : Node opc = getSymbolInternal(k, ftype, arithOpName.str());
496 [ + + ][ - - ]: 701661 : ret = mkApplyUf(opc, {children[i], ret});
497 : : }
498 : : else
499 : : {
500 : 1617150 : ret = d_nm->mkNode(k, children[i], ret);
501 : : }
502 : : }
503 [ + - ]: 871094 : Trace("lfsc-term-process-debug")
504 : 435547 : << "...return n-ary conv " << ret << std::endl;
505 : 435547 : return ret;
506 : : }
507 : 984849 : return n;
508 : : }
509 : :
510 : 1064200 : Node LfscNodeConverter::mkApplyUf(Node op, const std::vector<Node>& args) const
511 : : {
512 : 2128390 : std::vector<Node> aargs;
513 [ + + ]: 1064200 : if (op.isVar())
514 : : {
515 : 1011560 : aargs.push_back(op);
516 : : }
517 : : else
518 : : {
519 : : // Note that dag threshold is disabled for printing operators.
520 : 105282 : std::stringstream ss;
521 : 52641 : options::ioutils::applyOutputLanguage(ss, Language::LANG_SMTLIB_V2_6);
522 : 52641 : options::ioutils::applyDagThresh(ss, 0);
523 : 52641 : ss << op;
524 : 157923 : Node opv = d_nm->mkRawSymbol(ss.str(), op.getType());
525 : 52641 : aargs.push_back(opv);
526 : : }
527 : 1064200 : aargs.insert(aargs.end(), args.begin(), args.end());
528 : 2128390 : return d_nm->mkNode(Kind::APPLY_UF, aargs);
529 : : }
530 : :
531 : 6053 : TypeNode LfscNodeConverter::preConvertType(TypeNode tn)
532 : : {
533 [ + + ]: 6053 : 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 : 80 : d_declTypes.insert(tn);
539 : : }
540 : 6053 : return tn;
541 : : }
542 : :
543 : 6053 : TypeNode LfscNodeConverter::postConvertType(TypeNode tn)
544 : : {
545 : 6053 : TypeNode cur = tn;
546 : 12106 : Node tnn;
547 : 6053 : Kind k = tn.getKind();
548 [ + - ]: 12106 : Trace("lfsc-term-process-debug")
549 : 6053 : << "postConvertType " << tn << " " << tn.getNumChildren() << " " << k
550 : 6053 : << std::endl;
551 [ + + ]: 6053 : if (k == Kind::FUNCTION_TYPE)
552 : : {
553 : : // (-> T1 ... Tn T) is (arrow T1 .... (arrow Tn T))
554 : 4948 : std::vector<TypeNode> argTypes = tn.getArgTypes();
555 : : // also make the node embedding of the type
556 : 4948 : Node arrown = d_typeAsNode[d_arrow];
557 [ - + ][ - + ]: 2474 : Assert(!arrown.isNull());
[ - - ]
558 : 2474 : cur = tn.getRangeType();
559 : 2474 : tnn = typeAsNode(cur);
560 : 7145 : for (std::vector<TypeNode>::reverse_iterator it = argTypes.rbegin();
561 [ + + ]: 7145 : it != argTypes.rend();
562 : 4671 : ++it)
563 : : {
564 : 4671 : std::vector<TypeNode> aargs;
565 : 4671 : aargs.push_back(*it);
566 : 4671 : aargs.push_back(cur);
567 : 4671 : cur = d_nm->mkSort(d_arrow, aargs);
568 [ + + ][ - - ]: 14013 : tnn = mkApplyUf(arrown, {typeAsNode(*it), tnn});
569 : : }
570 : : }
571 [ + + ]: 3579 : else if (k == Kind::BITVECTOR_TYPE)
572 : : {
573 : 473 : tnn = d_typeKindToNodeCons[k];
574 : 473 : Node w = d_nm->mkConstInt(Rational(tn.getBitVectorSize()));
575 : 946 : tnn = mkApplyUf(tnn, {w});
576 : : }
577 [ + + ]: 3106 : else if (k == Kind::FLOATINGPOINT_TYPE)
578 : : {
579 : 6 : tnn = d_typeKindToNodeCons[k];
580 : 12 : 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 : : }
584 [ + + ]: 3100 : else if (k == Kind::TUPLE_TYPE)
585 : : {
586 : : // special case: tuples must be distinguished by their arity
587 : 80 : size_t nargs = tn.getNumChildren();
588 [ + + ]: 80 : if (nargs > 0)
589 : : {
590 : 158 : std::vector<TypeNode> types;
591 : 158 : std::vector<TypeNode> convTypes;
592 : 158 : std::vector<Node> targs;
593 [ + + ]: 255 : for (size_t i = 0; i < nargs; i++)
594 : : {
595 : 176 : TypeNode tnc = tn[i];
596 : 176 : types.push_back(d_sortType);
597 : 176 : convTypes.push_back(tnc);
598 : 176 : targs.push_back(typeAsNode(tnc));
599 : : }
600 : 158 : TypeNode ftype = d_nm->mkFunctionType(types, d_sortType);
601 : : // must distinguish by arity
602 : 79 : std::stringstream ss;
603 : 79 : ss << "Tuple_" << nargs;
604 : 79 : tnn = mkApplyUf(getSymbolInternal(k, ftype, ss.str()), targs);
605 : : // we are changing its name, we must make a sort constructor
606 : 79 : cur = d_nm->mkSortConstructor(ss.str(), nargs);
607 : 79 : cur = d_nm->mkSort(cur, convTypes);
608 : : }
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 [ + + ]: 3020 : else if (tn.getNumChildren() == 0)
617 : : {
618 [ - + ][ - + ]: 2657 : Assert(!tn.isTuple());
[ - - ]
619 : : // an uninterpreted sort, or an uninstantiatied (maybe parametric) datatype
620 : 2657 : d_declTypes.insert(tn);
621 : 5314 : std::stringstream ss;
622 : 2657 : options::ioutils::applyOutputLanguage(ss, Language::LANG_SMTLIB_V2_6);
623 : 2657 : tn.toStream(ss);
624 [ + + ]: 2657 : if (tn.isUninterpretedSortConstructor())
625 : : {
626 : 12 : std::string s = getNameForUserNameOfInternal(tn.getId(), ss.str());
627 : 12 : tnn = getSymbolInternal(k, d_sortType, s, false);
628 : : cur =
629 : 12 : d_nm->mkSortConstructor(s, tn.getUninterpretedSortConstructorArity());
630 : : }
631 [ + + ][ + + ]: 2645 : else if (tn.isUninterpretedSort() || tn.isDatatype())
[ + + ]
632 : : {
633 : 1396 : std::string s = getNameForUserNameOfInternal(tn.getId(), ss.str());
634 : 1396 : tnn = getSymbolInternal(k, d_sortType, s, false);
635 : 1396 : cur = d_nm->mkSort(s);
636 : : }
637 : : else
638 : : {
639 : : // all other builtin type constants, e.g. Int
640 : 1249 : tnn = getSymbolInternal(k, d_sortType, ss.str());
641 : : }
642 : : }
643 : : else
644 : : {
645 : : // to build the type-as-node, must convert the component types
646 : 726 : std::vector<Node> targs;
647 : 726 : std::vector<TypeNode> types;
648 [ + + ]: 880 : for (const TypeNode& tnc : tn)
649 : : {
650 : 517 : targs.push_back(typeAsNode(tnc));
651 : 517 : types.push_back(d_sortType);
652 : : }
653 : 726 : Node op;
654 [ + + ]: 363 : 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 : 8 : targs.erase(targs.begin(), targs.begin() + 1);
660 : 8 : types.erase(types.begin(), types.begin() + 1);
661 : 16 : 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 : 8 : std::stringstream ss;
665 : 8 : ss << tn[0];
666 : 8 : op = getSymbolInternal(k, ftype, ss.str());
667 : : }
668 [ + + ]: 355 : 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 : 40 : targs.erase(targs.begin(), targs.begin() + 1);
675 : 40 : types.erase(types.begin(), types.begin() + 1);
676 : 80 : TypeNode ftype = d_nm->mkFunctionType(types, d_sortType);
677 : 40 : std::string name = tn.getUninterpretedSortConstructor().getName();
678 : 40 : op = getSymbolInternal(k, ftype, name, false);
679 : : }
680 [ + + ]: 315 : 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 : : }
685 : : else
686 : : {
687 : 313 : std::map<Kind, Node>::iterator it = d_typeKindToNodeCons.find(k);
688 [ + - ]: 313 : if (it != d_typeKindToNodeCons.end())
689 : : {
690 : 313 : op = it->second;
691 : : }
692 : : }
693 [ + - ]: 363 : if (!op.isNull())
694 : : {
695 : 363 : tnn = mkApplyUf(op, targs);
696 : : }
697 : : else
698 : : {
699 : 0 : AlwaysAssert(false);
700 : : }
701 : : }
702 [ - + ][ - + ]: 6053 : Assert(!tnn.isNull());
[ - - ]
703 [ + - ]: 6053 : Trace("lfsc-term-process-debug") << "...type as node: " << tnn << std::endl;
704 : 6053 : d_typeAsNode[cur] = tnn;
705 : 12106 : return cur;
706 : : }
707 : :
708 : 22633 : 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 : 45266 : std::stringstream ss;
723 : 22633 : ss << "cvc";
724 [ + + ]: 22633 : if (variant != 0)
725 : : {
726 : 11 : ss << variant;
727 : : }
728 : 22633 : ss << ".";
729 : 22633 : std::string sanitized = ss.str();
730 : 22633 : size_t found = sanitized.size();
731 : 22633 : 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 : 1247 : do
739 : : {
740 : 23880 : found = sanitized.find_first_of("() \t\n\f\\;", found);
741 [ + + ]: 23880 : 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 : : }
751 [ + + ]: 23880 : } while (found != std::string::npos);
752 : 45266 : return sanitized;
753 : : }
754 : :
755 : 21215 : std::string LfscNodeConverter::getNameForUserNameOf(Node v)
756 : : {
757 : 42430 : std::string name = v.getName();
758 : 42430 : return getNameForUserNameOfInternal(v.getId(), name);
759 : : }
760 : :
761 : 22623 : std::string LfscNodeConverter::getNameForUserNameOfInternal(
762 : : uint64_t id, const std::string& name)
763 : : {
764 : 22623 : std::vector<uint64_t>& syms = d_userSymbolList[name];
765 : 22623 : size_t variant = 0;
766 : : std::vector<uint64_t>::iterator itr =
767 : 22623 : std::find(syms.begin(), syms.end(), id);
768 [ + + ]: 22623 : if (itr != syms.cend())
769 : : {
770 : 4520 : variant = std::distance(syms.begin(), itr);
771 : : }
772 : : else
773 : : {
774 : 18103 : variant = syms.size();
775 : 18103 : syms.push_back(id);
776 : : }
777 : 45246 : return getNameForUserName(name, variant);
778 : : }
779 : :
780 : 2193070 : bool LfscNodeConverter::shouldTraverse(Node n)
781 : : {
782 : 2193070 : Kind k = n.getKind();
783 : : // don't convert bound variable or instantiation pattern list directly
784 [ + + ][ + + ]: 2193070 : if (k == Kind::BOUND_VAR_LIST || k == Kind::INST_PATTERN_LIST)
785 : : {
786 : 8503 : return false;
787 : : }
788 : : // should not traverse internal applications
789 [ + + ]: 2184570 : if (k == Kind::APPLY_UF)
790 : : {
791 [ + + ]: 33600 : if (d_symbols.find(n.getOperator()) != d_symbols.end())
792 : : {
793 : 2324 : return false;
794 : : }
795 : : }
796 : 2182240 : return true;
797 : : }
798 : :
799 : 2524 : Node LfscNodeConverter::maybeMkSkolemFun(Node k, bool macroApply)
800 : : {
801 : 2524 : SkolemManager* sm = d_nm->getSkolemManager();
802 : 2524 : SkolemId sfi = SkolemId::NONE;
803 : 5048 : Node cacheVal;
804 : 5048 : TypeNode tn = k.getType();
805 [ + + ]: 2524 : if (sm->isSkolemFunction(k, sfi, cacheVal))
806 : : {
807 [ + + ]: 641 : if (sfi == SkolemId::RE_UNFOLD_POS_COMPONENT)
808 : : {
809 : : // a skolem corresponding to a regular expression unfolding component
810 : : // should print as (skolem_re_unfold_pos t R n) where the skolem is the
811 : : // n^th component for the unfolding of (str.in_re t R).
812 : 170 : TypeNode strType = d_nm->stringType();
813 : 170 : TypeNode reType = d_nm->regExpType();
814 : 170 : TypeNode intType = d_nm->integerType();
815 : 510 : TypeNode reut = d_nm->mkFunctionType({strType, reType, intType}, strType);
816 : 170 : Node sk = getSymbolInternal(k.getKind(), reut, "skolem_re_unfold_pos");
817 [ + - ][ + - ]: 170 : Assert(!cacheVal.isNull() && cacheVal.getKind() == Kind::SEXPR
[ + - ][ - + ]
[ - - ]
818 : : && cacheVal.getNumChildren() == 3);
819 : : // third value is mpz, which is not converted
820 : : return mkApplyUf(sk,
821 [ + + ][ - - ]: 340 : {convert(cacheVal[0]), convert(cacheVal[1]), cacheVal[2]});
822 : : }
823 : : }
824 : 2439 : return Node::null();
825 : : }
826 : :
827 : 64440 : Node LfscNodeConverter::typeAsNode(TypeNode tni) const
828 : : {
829 : : // should always exist in the cache, as we always run types through
830 : : // postConvertType before calling this method.
831 : 64440 : std::map<TypeNode, Node>::const_iterator it = d_typeAsNode.find(tni);
832 [ - + ][ - + ]: 64440 : AlwaysAssert(it != d_typeAsNode.end()) << "Missing typeAsNode " << tni;
[ - - ]
833 : 128880 : return it->second;
834 : : }
835 : :
836 : 431224 : Node LfscNodeConverter::mkInternalSymbol(const std::string& name,
837 : : TypeNode tn,
838 : : bool useRawSym)
839 : : {
840 : : // use raw symbol so that it is never quoted
841 : : Node sym =
842 [ + + ]: 431224 : useRawSym ? d_nm->mkRawSymbol(name, tn) : d_nm->mkBoundVar(name, tn);
843 : 431224 : d_symbols.insert(sym);
844 : 431224 : return sym;
845 : : }
846 : :
847 : 407 : Node LfscNodeConverter::getSymbolInternalFor(Node n,
848 : : const std::string& name,
849 : : bool useRawSym)
850 : : {
851 : 814 : return getSymbolInternal(n.getKind(), n.getType(), name, useRawSym);
852 : : }
853 : :
854 : 1211200 : Node LfscNodeConverter::getSymbolInternal(Kind k,
855 : : TypeNode tn,
856 : : const std::string& name,
857 : : bool useRawSym)
858 : : {
859 : 2422400 : std::tuple<Kind, TypeNode, std::string> key(k, tn, name);
860 : : std::map<std::tuple<Kind, TypeNode, std::string>, Node>::iterator it =
861 : 1211200 : d_symbolsMap.find(key);
862 [ + + ]: 1211200 : if (it != d_symbolsMap.end())
863 : : {
864 : 1162540 : return it->second;
865 : : }
866 : 97326 : Node sym = mkInternalSymbol(name, tn, useRawSym);
867 : 48663 : d_symbolToBuiltinKind[sym] = k;
868 : 48663 : d_symbolsMap[key] = sym;
869 : 48663 : return sym;
870 : : }
871 : :
872 : 970 : void LfscNodeConverter::getCharVectorInternal(Node c, std::vector<Node>& chars)
873 : : {
874 [ - + ][ - + ]: 970 : Assert(c.getKind() == Kind::CONST_STRING);
[ - - ]
875 : 970 : const std::vector<unsigned>& vec = c.getConst<String>().getVec();
876 [ + + ]: 970 : if (vec.size() == 0)
877 : : {
878 : 814 : Node ec = getSymbolInternalFor(c, "emptystr");
879 : 407 : chars.push_back(ec);
880 : 407 : return;
881 : : }
882 : 1689 : TypeNode tnc = d_nm->mkFunctionType(d_nm->integerType(), c.getType());
883 : 1689 : Node aconstf = getSymbolInternal(Kind::CONST_STRING, tnc, "char");
884 [ + + ]: 3479 : for (unsigned i = 0, size = vec.size(); i < size; i++)
885 : : {
886 : 14580 : Node cc = mkApplyUf(aconstf, {d_nm->mkConstInt(Rational(vec[i]))});
887 : 2916 : chars.push_back(cc);
888 : : }
889 : : }
890 : :
891 : 1137 : Node LfscNodeConverter::convertBitVector(const BitVector& bv)
892 : : {
893 : 2274 : TypeNode btn = d_nm->booleanType();
894 : 5685 : TypeNode btnv = d_nm->mkFunctionType({btn, btn}, btn);
895 : 1137 : size_t w = bv.getSize();
896 : 2274 : Node ret = getSymbolInternal(Kind::CONST_BITVECTOR, btn, "bvn");
897 : 3411 : Node b0 = getSymbolInternal(Kind::CONST_BITVECTOR, btn, "b0");
898 : 3411 : Node b1 = getSymbolInternal(Kind::CONST_BITVECTOR, btn, "b1");
899 : 3411 : Node bvc = getSymbolInternal(Kind::CONST_BITVECTOR, btnv, "bvc");
900 [ + + ]: 19359 : for (size_t i = 0; i < w; i++)
901 : : {
902 [ + + ]: 18222 : Node arg = bv.isBitSet((w - 1) - i) ? b1 : b0;
903 [ + + ][ - - ]: 54666 : ret = mkApplyUf(bvc, {arg, ret});
904 : : }
905 : 2274 : return ret;
906 : : }
907 : :
908 : 687742 : Node LfscNodeConverter::getNullTerminator(Kind k, TypeNode tn)
909 : : {
910 : 1375480 : Node nullTerm;
911 [ + + ][ + ]: 687742 : switch (k)
912 : : {
913 : 312 : case Kind::REGEXP_CONCAT:
914 : : // the language containing only the empty string, which has special
915 : : // syntax in LFSC
916 : 312 : nullTerm = getSymbolInternal(k, tn, "re.empty");
917 : 312 : break;
918 : 5855 : case Kind::BITVECTOR_CONCAT:
919 : : {
920 : : // the null terminator of bitvector concat is a dummy variable of
921 : : // bit-vector type with zero width, regardless of the type of the overall
922 : : // concat.
923 : 5855 : TypeNode bvz = d_nm->mkBitVectorType(0);
924 : 5855 : nullTerm = getSymbolInternal(k, bvz, "emptybv");
925 : : }
926 : 5855 : break;
927 : 681575 : default:
928 : : // no special handling, or not null terminated
929 : 681575 : break;
930 : : }
931 [ + + ]: 687742 : if (!nullTerm.isNull())
932 : : {
933 : 6167 : return nullTerm;
934 : : }
935 : : // otherwise, fall back to standard utility
936 : 681575 : return expr::getNullTerminator(k, tn);
937 : : }
938 : :
939 : 0 : Kind LfscNodeConverter::getBuiltinKindForInternalSymbol(Node op) const
940 : : {
941 : 0 : std::map<Node, Kind>::const_iterator it = d_symbolToBuiltinKind.find(op);
942 [ - - ]: 0 : if (it != d_symbolToBuiltinKind.end())
943 : : {
944 : 0 : return it->second;
945 : : }
946 : 0 : return Kind::UNDEFINED_KIND;
947 : : }
948 : :
949 : 350312 : Node LfscNodeConverter::getOperatorOfTerm(Node n, bool macroApply)
950 : : {
951 [ - + ][ - + ]: 350312 : Assert(n.hasOperator());
[ - - ]
952 [ - + ][ - + ]: 350312 : Assert(!n.isClosure());
[ - - ]
953 : 350312 : Kind k = n.getKind();
954 : 700624 : std::stringstream opName;
955 [ + - ]: 700624 : Trace("lfsc-term-process-debug2")
956 : 0 : << "getOperatorOfTerm " << n << " " << k << " "
957 : 0 : << (n.getMetaKind() == metakind::PARAMETERIZED) << " "
958 : 350312 : << GenericOp::isIndexedOperatorKind(k) << std::endl;
959 [ + + ]: 350312 : if (n.getMetaKind() == metakind::PARAMETERIZED)
960 : : {
961 : 158652 : Node op = n.getOperator();
962 : 158652 : std::vector<Node> indices;
963 [ + + ]: 79326 : if (GenericOp::isIndexedOperatorKind(k))
964 : : {
965 : 11419 : indices = GenericOp::getIndicesForOperator(k, n.getOperator());
966 : : // we must convert the name of indices on updaters and testers
967 [ + + ][ + + ]: 11419 : if (k == Kind::APPLY_UPDATER || k == Kind::APPLY_TESTER)
968 : : {
969 [ - + ][ - + ]: 582 : Assert(indices.size() == 1);
[ - - ]
970 : : // must convert to user name
971 : 582 : TypeNode intType = d_nm->integerType();
972 : 582 : indices[0] =
973 : 1164 : getSymbolInternal(k, intType, getNameForUserNameOf(indices[0]));
974 : : }
975 : : }
976 [ + + ]: 67907 : else if (op.getType().isFunction())
977 : : {
978 : 63969 : return op;
979 : : }
980 : : // note other kinds of functions (e.g. selectors and testers)
981 : 30714 : std::vector<TypeNode> argTypes;
982 [ + + ]: 32807 : for (const Node& nc : n)
983 : : {
984 : 17450 : argTypes.push_back(nc.getType());
985 : : }
986 : 30714 : TypeNode ftype = n.getType();
987 [ + + ]: 15357 : if (!argTypes.empty())
988 : : {
989 : 15260 : ftype = d_nm->mkFunctionType(argTypes, ftype);
990 : : }
991 : 30714 : Node ret;
992 [ + + ]: 15357 : if (GenericOp::isIndexedOperatorKind(k))
993 : : {
994 : 22838 : std::vector<TypeNode> itypes;
995 [ + + ]: 25424 : for (const Node& i : indices)
996 : : {
997 : 14005 : itypes.push_back(i.getType());
998 : : }
999 [ + - ]: 11419 : if (!itypes.empty())
1000 : : {
1001 : 11419 : ftype = d_nm->mkFunctionType(itypes, ftype);
1002 : : }
1003 [ + + ]: 11419 : if (!macroApply)
1004 : : {
1005 [ + + ][ + + ]: 1467 : if (k != Kind::APPLY_UPDATER && k != Kind::APPLY_TESTER)
1006 : : {
1007 : 1392 : opName << "f_";
1008 : : }
1009 : : }
1010 : : // must avoid overloading for to_fp variants
1011 [ + + ]: 11419 : if (k == Kind::FLOATINGPOINT_TO_FP_FROM_FP)
1012 : : {
1013 : 1 : opName << "to_fp_fp";
1014 : : }
1015 [ - + ]: 11418 : else if (k == Kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV)
1016 : : {
1017 : 0 : opName << "to_fp_ieee_bv";
1018 : : }
1019 [ + + ]: 11418 : else if (k == Kind::FLOATINGPOINT_TO_FP_FROM_SBV)
1020 : : {
1021 : 4 : opName << "to_fp_sbv";
1022 : : }
1023 [ + + ]: 11414 : else if (k == Kind::FLOATINGPOINT_TO_FP_FROM_REAL)
1024 : : {
1025 : 2 : opName << "to_fp_real";
1026 : : }
1027 [ + + ]: 11412 : else if (k == Kind::BITVECTOR_BIT)
1028 : : {
1029 : 3605 : opName << "bit";
1030 : : }
1031 : : else
1032 : : {
1033 : 7807 : opName << printer::smt2::Smt2Printer::smtKindString(k);
1034 : : }
1035 : : }
1036 [ + + ]: 3938 : else if (k == Kind::APPLY_CONSTRUCTOR)
1037 : : {
1038 : 2257 : unsigned index = DType::indexOf(op);
1039 : 2257 : const DType& dt = DType::datatypeOf(op);
1040 : : // get its variable name
1041 : 2257 : opName << getNameForUserNameOf(dt[index].getConstructor());
1042 : : }
1043 [ + - ]: 1681 : else if (k == Kind::APPLY_SELECTOR)
1044 : : {
1045 : 1681 : ret = maybeMkSkolemFun(op, macroApply);
1046 [ + - ]: 1681 : if (ret.isNull())
1047 : : {
1048 : 1681 : unsigned index = DType::indexOf(op);
1049 : 1681 : const DType& dt = DType::datatypeOf(op);
1050 : 1681 : unsigned cindex = DType::cindexOf(op);
1051 : 1681 : opName << getNameForUserNameOf(dt[cindex][index].getSelector());
1052 : : }
1053 : : }
1054 [ - - ][ - - ]: 0 : else if (k == Kind::SET_SINGLETON || k == Kind::BAG_MAKE
1055 [ - - ]: 0 : || k == Kind::SEQ_UNIT)
1056 : : {
1057 [ - - ]: 0 : if (!macroApply)
1058 : : {
1059 : 0 : opName << "f_";
1060 : : }
1061 : 0 : opName << printer::smt2::Smt2Printer::smtKindString(k);
1062 : : }
1063 : : else
1064 : : {
1065 : 0 : opName << op;
1066 : : }
1067 [ + - ]: 15357 : if (ret.isNull())
1068 : : {
1069 [ + - ]: 15357 : Trace("lfsc-term-process-debug2") << "...default symbol" << std::endl;
1070 : 15357 : ret = getSymbolInternal(k, ftype, opName.str());
1071 : : }
1072 : : // if indexed, apply to index
1073 [ + + ]: 15357 : if (!indices.empty())
1074 : : {
1075 : 11419 : ret = mkApplyUf(ret, indices);
1076 : : }
1077 [ + - ]: 15357 : Trace("lfsc-term-process-debug2") << "...return " << ret << std::endl;
1078 : 15357 : return ret;
1079 : : }
1080 : 541972 : std::vector<TypeNode> argTypes;
1081 [ + + ]: 934259 : for (const Node& nc : n)
1082 : : {
1083 : 663273 : argTypes.push_back(nc.getType());
1084 : : }
1085 : : // we only use binary operators
1086 [ + + ]: 270986 : if (NodeManager::isNAryKind(k))
1087 : : {
1088 : 118208 : argTypes.resize(2);
1089 : : }
1090 : 541972 : TypeNode tn = n.getType();
1091 : 270986 : TypeNode ftype = d_nm->mkFunctionType(argTypes, tn);
1092 : : // most functions are called f_X where X is the SMT-LIB name, if we are
1093 : : // getting the macroApply variant, then we don't prefix with `f_`.
1094 [ + + ]: 270986 : if (!macroApply)
1095 : : {
1096 : 212601 : opName << "f_";
1097 : : }
1098 [ + + ]: 270986 : if (k == Kind::FLOATINGPOINT_COMPONENT_NAN
1099 [ + + ]: 270984 : || k == Kind::FLOATINGPOINT_COMPONENT_INF
1100 [ + + ]: 270983 : || k == Kind::FLOATINGPOINT_COMPONENT_ZERO
1101 [ + + ]: 270982 : || k == Kind::FLOATINGPOINT_COMPONENT_SIGN
1102 [ + + ]: 270980 : || k == Kind::FLOATINGPOINT_COMPONENT_EXPONENT
1103 [ + + ]: 270979 : || k == Kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND
1104 [ - + ]: 270978 : || k == Kind::ROUNDINGMODE_BITBLAST)
1105 : : {
1106 : : // remove @fp.
1107 : 8 : std::string str = printer::smt2::Smt2Printer::smtKindString(k);
1108 : 8 : opName << str.substr(4);
1109 : : }
1110 : : else
1111 : : {
1112 : : // all arithmetic kinds must explicitly deal with real vs int subtyping
1113 [ + + ][ + + ]: 270978 : if (k == Kind::ADD || k == Kind::MULT || k == Kind::NONLINEAR_MULT
[ + + ]
1114 [ + + ][ + + ]: 202276 : || k == Kind::GEQ || k == Kind::GT || k == Kind::LEQ || k == Kind::LT
[ + + ][ + + ]
1115 [ + + ][ + + ]: 138777 : || k == Kind::SUB || k == Kind::DIVISION || k == Kind::DIVISION_TOTAL
[ + + ]
1116 [ + + ][ + + ]: 136334 : || k == Kind::INTS_DIVISION || k == Kind::INTS_DIVISION_TOTAL
1117 [ + + ][ + + ]: 135825 : || k == Kind::INTS_MODULUS || k == Kind::INTS_MODULUS_TOTAL
1118 [ + + ][ + + ]: 135482 : || k == Kind::NEG || k == Kind::POW)
1119 : : {
1120 : : // currently allow subtyping
1121 : 136023 : opName << "a.";
1122 : : }
1123 [ + + ]: 270978 : if (k == Kind::NEG)
1124 : : {
1125 : 522 : opName << "u";
1126 : : }
1127 : 270978 : opName << printer::smt2::Smt2Printer::smtKindString(k);
1128 : : }
1129 : 270986 : return getSymbolInternal(k, ftype, opName.str());
1130 : : }
1131 : :
1132 : 36510 : Node LfscNodeConverter::getOperatorOfClosure(Node q,
1133 : : bool macroApply,
1134 : : bool isPartial)
1135 : : {
1136 : 73020 : TypeNode retType = isPartial ? q[1].getType() : q.getType();
1137 : 109530 : TypeNode bodyType = d_nm->mkFunctionType(q[1].getType(), retType);
1138 : : // We permit non-flat function types here
1139 : : // intType is used here for variable indices
1140 : 73020 : TypeNode intType = d_nm->integerType();
1141 : 182550 : TypeNode ftype = d_nm->mkFunctionType({intType, d_sortType}, bodyType);
1142 : 36510 : Kind k = q.getKind();
1143 : 36510 : std::stringstream opName;
1144 [ + + ]: 36510 : if (!macroApply)
1145 : : {
1146 : 4652 : opName << "f_";
1147 : : }
1148 : 36510 : opName << printer::smt2::Smt2Printer::smtKindString(k);
1149 : 73020 : return getSymbolInternal(k, ftype, opName.str());
1150 : : }
1151 : :
1152 : 47896 : Node LfscNodeConverter::getOperatorOfBoundVar(Node cop, Node v)
1153 : : {
1154 : 143688 : Node x = d_nm->mkConstInt(Rational(getOrAssignIndexForBVar(v)));
1155 : 95792 : Node tc = typeAsNode(convertType(v.getType()));
1156 [ + + ][ - - ]: 191584 : return mkApplyUf(cop, {x, tc});
1157 : : }
1158 : :
1159 : 15733 : size_t LfscNodeConverter::getOrAssignIndexForFVar(Node fv)
1160 : : {
1161 [ - + ][ - + ]: 15733 : Assert(fv.isVar());
[ - - ]
1162 : 15733 : std::map<Node, size_t>::iterator it = d_fvarIndex.find(fv);
1163 [ - + ]: 15733 : if (it != d_fvarIndex.end())
1164 : : {
1165 : 0 : return it->second;
1166 : : }
1167 : 15733 : size_t id = d_fvarIndex.size();
1168 : 15733 : d_fvarIndex[fv] = id;
1169 : 15733 : return id;
1170 : : }
1171 : :
1172 : 55686 : size_t LfscNodeConverter::getOrAssignIndexForBVar(Node bv)
1173 : : {
1174 [ - + ][ - + ]: 55686 : Assert(bv.isVar());
[ - - ]
1175 : 55686 : std::map<Node, size_t>::iterator it = d_bvarIndex.find(bv);
1176 [ + + ]: 55686 : if (it != d_bvarIndex.end())
1177 : : {
1178 : 47722 : return it->second;
1179 : : }
1180 : 7964 : size_t id = d_bvarIndex.size();
1181 : 7964 : d_bvarIndex[bv] = id;
1182 : 7964 : return id;
1183 : : }
1184 : :
1185 : 1417 : const std::unordered_set<Node>& LfscNodeConverter::getDeclaredSymbols() const
1186 : : {
1187 : 1417 : return d_declVars;
1188 : : }
1189 : :
1190 : 1417 : const std::unordered_set<TypeNode>& LfscNodeConverter::getDeclaredTypes() const
1191 : : {
1192 : 1417 : return d_declTypes;
1193 : : }
1194 : :
1195 : : } // namespace proof
1196 : : } // namespace cvc5::internal
|
