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 : 1724 : LfscNodeConverter::LfscNodeConverter(NodeManager* nm) : NodeConverter(nm)
47 : : {
48 : 1724 : d_arrow = nm->mkSortConstructor("arrow", 2);
49 : :
50 : 1724 : d_sortType = nm->mkSort("sortType");
51 : : // the embedding of arrow into Node, which is binary constructor over sorts
52 : 6896 : TypeNode anfType = nm->mkFunctionType({d_sortType, d_sortType}, d_sortType);
53 : 1724 : d_typeAsNode[d_arrow] =
54 : 3448 : getSymbolInternal(Kind::FUNCTION_TYPE, anfType, "arrow");
55 : :
56 : 1724 : TypeNode intType = nm->integerType();
57 : 6896 : TypeNode arrType = nm->mkFunctionType({d_sortType, d_sortType}, d_sortType);
58 : 1724 : d_typeKindToNodeCons[Kind::ARRAY_TYPE] =
59 : 3448 : getSymbolInternal(Kind::FUNCTION_TYPE, arrType, "Array");
60 : 1724 : TypeNode bvType = nm->mkFunctionType(intType, d_sortType);
61 : 1724 : d_typeKindToNodeCons[Kind::BITVECTOR_TYPE] =
62 : 3448 : getSymbolInternal(Kind::FUNCTION_TYPE, bvType, "BitVec");
63 : 6896 : TypeNode fpType = nm->mkFunctionType({intType, intType}, d_sortType);
64 : 1724 : d_typeKindToNodeCons[Kind::FLOATINGPOINT_TYPE] =
65 : 3448 : getSymbolInternal(Kind::FUNCTION_TYPE, fpType, "FloatingPoint");
66 : 1724 : TypeNode setType = nm->mkFunctionType(d_sortType, d_sortType);
67 : 1724 : d_typeKindToNodeCons[Kind::SET_TYPE] =
68 : 3448 : getSymbolInternal(Kind::FUNCTION_TYPE, setType, "Set");
69 : 1724 : d_typeKindToNodeCons[Kind::BAG_TYPE] =
70 : 3448 : getSymbolInternal(Kind::FUNCTION_TYPE, setType, "Bag");
71 : 1724 : d_typeKindToNodeCons[Kind::SEQUENCE_TYPE] =
72 : 3448 : getSymbolInternal(Kind::FUNCTION_TYPE, setType, "Seq");
73 : 1724 : }
74 : :
75 : 2596918 : 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 [ + + ]: 2596918 : if (n.getKind() == Kind::MATCH)
81 : : {
82 : 12 : return theory::datatypes::DatatypesRewriter::expandMatch(n);
83 : : }
84 : 2596906 : return n;
85 : : }
86 : :
87 : 2587890 : Node LfscNodeConverter::postConvert(Node n)
88 : : {
89 : 2587890 : Kind k = n.getKind();
90 : : // we eliminate MATCH at preConvert above
91 [ - + ][ - + ]: 2587890 : Assert(k != Kind::MATCH);
[ - - ]
92 [ + + ]: 2587890 : if (k == Kind::ASCRIPTION_TYPE)
93 : : {
94 : : // dummy node, return it
95 : 13 : return n;
96 : : }
97 : 2587877 : TypeNode tn = n.getType();
98 [ + - ]: 5175754 : Trace("lfsc-term-process-debug")
99 : 2587877 : << "postConvert " << n << " " << k << std::endl;
100 [ + + ]: 2587877 : if (k == Kind::BOUND_VARIABLE)
101 : : {
102 [ - + ]: 9795 : 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 : 9795 : TypeNode intType = d_nm->integerType();
109 : 19590 : Node x = d_nm->mkConstInt(Rational(getOrAssignIndexForBVar(n)));
110 : 19590 : Node tc = typeAsNode(convertType(tn));
111 : 39180 : TypeNode ftype = d_nm->mkFunctionType({intType, d_sortType}, tn);
112 : 19590 : Node bvarOp = getSymbolInternal(k, ftype, "bvar");
113 [ + + ][ - - ]: 29385 : return mkApplyUf(bvarOp, {x, tc});
114 : 9795 : }
115 [ + + ]: 2578082 : else if (k == Kind::RAW_SYMBOL)
116 : : {
117 : : // ignore internally generated symbols
118 : 13358 : return n;
119 : : }
120 [ + + ][ + + ]: 2564724 : else if (k == Kind::SKOLEM || k == Kind::DUMMY_SKOLEM
121 [ - + ]: 2558216 : || k == Kind::DT_SYGUS_EVAL)
122 : : {
123 : : // constructors/selectors are represented by skolems, which are defined
124 : : // symbols
125 [ + + ]: 12567 : if (tn.isDatatypeConstructor() || tn.isDatatypeSelector()
126 [ + + ][ + + ]: 12567 : || 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 : 1058 : 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 : 5450 : Node wi = SkolemManager::getUnpurifiedForm(n);
135 [ + - ][ + + ]: 5450 : if (!wi.isNull() && wi != n)
[ + + ]
136 : : {
137 [ + - ]: 8900 : Trace("lfsc-term-process-debug")
138 : 4450 : << "...original form " << wi << std::endl;
139 : 4450 : wi = convert(wi);
140 [ + - ]: 8900 : Trace("lfsc-term-process-debug")
141 : 4450 : << "...converted original for " << wi << std::endl;
142 : 4450 : TypeNode ftype = d_nm->mkFunctionType(tn, tn);
143 : 8900 : Node skolemOp = getSymbolInternal(k, ftype, "skolem");
144 : 8900 : return mkApplyUf(skolemOp, {wi});
145 : 4450 : }
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 : 5450 : }
163 [ + + ]: 2558216 : else if (n.isVar())
164 : : {
165 : 16220 : d_declVars.insert(n);
166 : 32440 : return mkInternalSymbol(getNameForUserNameOf(n), tn);
167 : : }
168 [ + + ]: 2541996 : 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 : 16 : TypeNode tnc = d_nm->mkFunctionType({tnn.getType(), ub.getType()},
177 : 24 : d_nm->booleanType());
178 : 16 : Node fcard = getSymbolInternal(k, tnc, "fmf.card");
179 [ + + ][ - - ]: 24 : return mkApplyUf(fcard, {tnn, ub});
180 : 8 : }
181 [ + + ]: 2541988 : else if (k == Kind::APPLY_UF)
182 : : {
183 : 77434 : return convert(theory::uf::TheoryUfRewriter::getHoApplyForApplyUf(n));
184 : : }
185 [ + + ][ + + ]: 2503271 : else if (k == Kind::APPLY_CONSTRUCTOR || k == Kind::APPLY_SELECTOR
186 [ + + ][ + + ]: 2498544 : || k == Kind::APPLY_TESTER || k == Kind::APPLY_UPDATER)
187 : : {
188 : : // must add to declared types
189 : 5512 : const DType& dt = DType::datatypeOf(n.getOperator());
190 : 5512 : d_declTypes.insert(dt.getTypeNode());
191 : : // must convert other kinds of apply to functions, since we convert to
192 : : // HO_APPLY
193 : 5512 : Node opc = getOperatorOfTerm(n, true);
194 [ + + ]: 5512 : if (n.getNumChildren() == 0)
195 : : {
196 : 154 : return opc;
197 : : }
198 : 10716 : return postConvert(mkApplyUf(opc, std::vector<Node>(n.begin(), n.end())));
199 : 5512 : }
200 [ + + ]: 2497759 : else if (k == Kind::HO_APPLY)
201 : : {
202 : 675317 : std::vector<TypeNode> argTypes;
203 : 675317 : argTypes.push_back(n[0].getType());
204 : 675317 : argTypes.push_back(n[1].getType());
205 : 675317 : TypeNode tnh = d_nm->mkFunctionType(argTypes, tn);
206 : 1350634 : Node hconstf = getSymbolInternal(k, tnh, "apply");
207 [ + + ][ - - ]: 2025951 : return mkApplyUf(hconstf, {n[0], n[1]});
208 : 675317 : }
209 [ + + ][ + + ]: 1822442 : else if (k == Kind::CONST_RATIONAL || k == Kind::CONST_INTEGER)
210 : : {
211 : 22344 : TypeNode tnv = d_nm->mkFunctionType(tn, tn);
212 : 22344 : Node rconstf;
213 : 22344 : Node arg;
214 : 22344 : Rational r = n.getConst<Rational>();
215 [ + + ]: 22344 : if (tn.isInteger())
216 : : {
217 : 17789 : rconstf = getSymbolInternal(k, tnv, "int");
218 [ + + ]: 17789 : if (r.sgn() == -1)
219 : : {
220 : : // use LFSC syntax for mpz negation
221 : 3156 : Node mpzn = getSymbolInternal(k, d_nm->mkFunctionType(tn, tn), "~");
222 : 3156 : arg = mkApplyUf(mpzn, {d_nm->mkConstInt(r.abs())});
223 : 1578 : }
224 : : else
225 : : {
226 : 16211 : arg = n;
227 : : }
228 : : }
229 : : else
230 : : {
231 : 4555 : rconstf = getSymbolInternal(k, tnv, "real");
232 : : // ensure rationals are printed properly here using mpq syntax
233 : : // Note that inconvieniently, LFSC uses (non-sexpr) syntax n/m for
234 : : // constant rationals, hence we must use a string
235 : 4555 : std::stringstream ss;
236 : 4555 : ss << "__LFSC_TMP" << r.getNumerator().abs() << "/" << r.getDenominator();
237 : 4555 : arg = mkInternalSymbol(ss.str(), tn);
238 : : // negative (~ n/m)
239 [ + + ]: 4555 : if (r.sgn() == -1)
240 : : {
241 : 4348 : Node mpzn = getSymbolInternal(k, d_nm->mkFunctionType(tn, tn), "~");
242 : 4348 : arg = mkApplyUf(mpzn, {arg});
243 : 2174 : }
244 : 4555 : }
245 : 44688 : return mkApplyUf(rconstf, {arg});
246 : 22344 : }
247 [ + + ]: 1800098 : else if (k == Kind::CONST_BITVECTOR)
248 : : {
249 : 1440 : TypeNode btn = d_nm->booleanType();
250 : 1440 : TypeNode tnv = d_nm->mkFunctionType(btn, tn);
251 : 1440 : BitVector bv = n.getConst<BitVector>();
252 : 1440 : Node ret = convertBitVector(bv);
253 : 2880 : Node bconstf = getSymbolInternal(k, tnv, "bv");
254 : 2880 : return mkApplyUf(bconstf, {ret});
255 : 1440 : }
256 [ + + ]: 1798658 : else if (k == Kind::CONST_FLOATINGPOINT)
257 : : {
258 : 19 : BitVector s, e, i;
259 : 19 : n.getConst<FloatingPoint>().getIEEEBitvectors(s, e, i);
260 : 19 : Node sn = convert(d_nm->mkConst(s));
261 : 19 : Node en = convert(d_nm->mkConst(e));
262 : 19 : Node in = convert(d_nm->mkConst(i));
263 : : TypeNode tnv =
264 : 95 : d_nm->mkFunctionType({sn.getType(), en.getType(), in.getType()}, tn);
265 : 38 : Node bconstf = getSymbolInternal(k, tnv, "fp");
266 [ + + ][ - - ]: 76 : return mkApplyUf(bconstf, {sn, en, in});
267 : 19 : }
268 [ + + ]: 1798639 : else if (k == Kind::CONST_FINITE_FIELD)
269 : : {
270 : 81 : const FiniteFieldValue& ffv = n.getConst<FiniteFieldValue>();
271 : 162 : Node v = convert(d_nm->mkConstInt(ffv.getValue()));
272 : 162 : Node fs = convert(d_nm->mkConstInt(ffv.getFieldSize()));
273 : 324 : TypeNode tnv = d_nm->mkFunctionType({v.getType(), fs.getType()}, tn);
274 : 162 : Node ffconstf = getSymbolInternal(k, tnv, "ff.value");
275 [ + + ][ - - ]: 243 : return mkApplyUf(ffconstf, {v, fs});
276 : 81 : }
277 [ + + ]: 1798558 : else if (k == Kind::CONST_STRING)
278 : : {
279 : : //"" is emptystr
280 : : //"A" is (char 65)
281 : : //"ABC" is (str.++ (char 65) (str.++ (char 66) (str.++ (char 67) emptystr)))
282 : 1467 : std::vector<Node> charVec;
283 : 1467 : getCharVectorInternal(n, charVec);
284 [ - + ][ - + ]: 1467 : Assert(!charVec.empty());
[ - - ]
285 [ + + ]: 1467 : if (charVec.size() == 1)
286 : : {
287 : : // handles empty string and singleton character
288 : 1059 : return charVec[0];
289 : : }
290 : 408 : std::reverse(charVec.begin(), charVec.end());
291 : 816 : Node ret = postConvert(getNullTerminator(d_nm, Kind::STRING_CONCAT, tn));
292 [ + + ]: 3722 : for (size_t i = 0, size = charVec.size(); i < size; i++)
293 : : {
294 : 3314 : ret = d_nm->mkNode(Kind::STRING_CONCAT, charVec[i], ret);
295 : : }
296 : 408 : return ret;
297 : 1467 : }
298 [ + + ]: 1797091 : else if (k == Kind::CONST_SEQUENCE)
299 : : {
300 : 89 : const std::vector<Node>& charVec = n.getConst<Sequence>().getVec();
301 : 89 : TypeNode etype = d_nm->mkFunctionType(d_sortType, tn);
302 : 178 : Node ret = getSymbolInternal(k, etype, "seq.empty");
303 : 178 : ret = mkApplyUf(ret, {typeAsNode(convertType(tn))});
304 : 89 : std::vector<Node> vecu;
305 [ + + ]: 131 : for (size_t i = 0, size = charVec.size(); i < size; i++)
306 : : {
307 : : Node u =
308 : 174 : d_nm->mkNode(Kind::SEQ_UNIT, postConvert(charVec[size - (i + 1)]));
309 [ + + ]: 87 : if (size == 1)
310 : : {
311 : : // singleton case
312 : 45 : return u;
313 : : }
314 : 42 : ret = d_nm->mkNode(Kind::STRING_CONCAT, u, ret);
315 [ + + ]: 87 : }
316 : 44 : return ret;
317 : 89 : }
318 [ + + ]: 1797002 : else if (k == Kind::STORE_ALL)
319 : : {
320 : 38 : Node t = typeAsNode(convertType(tn));
321 : 19 : TypeNode caRetType = d_nm->mkFunctionType(tn.getArrayConstituentType(), tn);
322 : 19 : TypeNode catype = d_nm->mkFunctionType(d_sortType, caRetType);
323 : 38 : Node bconstf = getSymbolInternal(k, catype, "array_const");
324 : 57 : Node f = mkApplyUf(bconstf, {t});
325 : 19 : ArrayStoreAll storeAll = n.getConst<ArrayStoreAll>();
326 : 38 : return mkApplyUf(f, {convert(storeAll.getValue())});
327 : 19 : }
328 [ + + ][ + + ]: 1772770 : else if (k == Kind::GEQ || k == Kind::GT || k == Kind::LEQ || k == Kind::LT
[ + + ]
329 [ + + ][ + + ]: 1725364 : || k == Kind::SUB || k == Kind::DIVISION || k == Kind::DIVISION_TOTAL
[ + + ]
330 [ + + ][ + + ]: 1722955 : || k == Kind::INTS_DIVISION || k == Kind::INTS_DIVISION_TOTAL
331 [ + + ][ + + ]: 1722442 : || k == Kind::INTS_MODULUS || k == Kind::INTS_MODULUS_TOTAL
332 [ + + ][ + + ]: 1721979 : || k == Kind::NEG || k == Kind::POW
333 [ + + ]: 1721343 : || k == Kind::FLOATINGPOINT_COMPONENT_NAN
334 [ + + ]: 1721341 : || k == Kind::FLOATINGPOINT_COMPONENT_INF
335 [ + + ]: 1721340 : || k == Kind::FLOATINGPOINT_COMPONENT_ZERO
336 [ + + ]: 1721339 : || k == Kind::FLOATINGPOINT_COMPONENT_SIGN
337 [ + + ]: 1721337 : || k == Kind::FLOATINGPOINT_COMPONENT_EXPONENT
338 [ + + ]: 1721336 : || k == Kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND
339 [ + - ]: 1721335 : || k == Kind::ROUNDINGMODE_BITBLAST
340 [ + + ][ + + ]: 3569753 : || GenericOp::isIndexedOperatorKind(k))
[ + + ]
341 : : {
342 : : // must give special names to SMT-LIB operators with arithmetic subtyping
343 : : // note that SUB is not n-ary
344 : : // get the macro-apply version of the operator
345 : 87944 : Node opc = getOperatorOfTerm(n, true);
346 : 87944 : return mkApplyUf(opc, std::vector<Node>(n.begin(), n.end()));
347 : 87944 : }
348 [ + + ][ + + ]: 1709039 : else if (k == Kind::SET_EMPTY || k == Kind::SET_UNIVERSE
349 [ + + ]: 1708968 : || k == Kind::BAG_EMPTY)
350 : : {
351 : 158 : Node t = typeAsNode(convertType(tn));
352 : 79 : TypeNode etype = d_nm->mkFunctionType(d_sortType, tn);
353 : : Node ef = getSymbolInternal(
354 : : k,
355 : : etype,
356 : 79 : k == Kind::SET_EMPTY
357 : : ? "set.empty"
358 [ + + ][ + + ]: 158 : : (k == Kind::SET_UNIVERSE ? "set.universe" : "bag.empty"));
359 : 158 : return mkApplyUf(ef, {t});
360 : 79 : }
361 [ + + ]: 1708960 : else if (n.isClosure())
362 : : {
363 : : // (forall ((x1 T1) ... (xn Tk)) P) is
364 : : // ((forall x1 T1) ((forall x2 T2) ... ((forall xk Tk) P))). We use
365 : : // SEXPR to do this, which avoids the need for indexed operators.
366 : 21563 : Node ret = n[1];
367 : 21563 : Node cop = getOperatorOfClosure(n, true);
368 : 21563 : Node pcop = getOperatorOfClosure(n, true, true);
369 [ + + ]: 73935 : for (size_t i = 0, nchild = n[0].getNumChildren(); i < nchild; i++)
370 : : {
371 : 52372 : size_t ii = (nchild - 1) - i;
372 : 52372 : Node v = n[0][ii];
373 : : // use the partial operator for variables except the last one. This
374 : : // avoids type errors in internal representation of LFSC terms.
375 [ + + ]: 104744 : Node vop = getOperatorOfBoundVar(ii == 0 ? cop : pcop, v);
376 : 104744 : ret = mkApplyUf(vop, {ret});
377 : 52372 : }
378 : : // notice that intentionally we drop annotations here
379 : 21563 : return ret;
380 : 21563 : }
381 [ + + ]: 1687397 : else if (k == Kind::FUNCTION_ARRAY_CONST)
382 : : {
383 : : // must convert to lambda and then run the conversion
384 : 6 : Node lam = theory::uf::FunctionConst::toLambda(n);
385 [ - + ][ - + ]: 6 : Assert(!lam.isNull());
[ - - ]
386 : 6 : return convert(lam);
387 : 6 : }
388 [ - + ]: 1687391 : else if (k == Kind::REGEXP_LOOP)
389 : : {
390 : : // ((_ re.loop n1 n2) t) is ((re.loop n1 n2) t)
391 : 0 : TypeNode intType = d_nm->integerType();
392 : : TypeNode relType =
393 : 0 : d_nm->mkFunctionType({intType, intType}, d_nm->mkFunctionType(tn, tn));
394 : : Node rop = getSymbolInternal(
395 : 0 : k, relType, printer::smt2::Smt2Printer::smtKindString(k));
396 : 0 : RegExpLoop op = n.getOperator().getConst<RegExpLoop>();
397 : 0 : Node n1 = d_nm->mkConstInt(Rational(op.d_loopMinOcc));
398 : 0 : Node n2 = d_nm->mkConstInt(Rational(op.d_loopMaxOcc));
399 : 0 : return mkApplyUf(mkApplyUf(rop, {n1, n2}), {n[0]});
400 : 0 : }
401 [ + + ]: 1687391 : else if (k == Kind::BITVECTOR_FROM_BOOLS)
402 : : {
403 : 3551 : TypeNode btn = d_nm->booleanType();
404 : : // (from_bools t1 ... tn) is
405 : : // (from_bools t1 (from_bools t2 ... (from_bools tn emptybv)))
406 : : // where notice that each from_bools has a different type
407 : 3551 : Node curr = getNullTerminator(d_nm, Kind::BITVECTOR_CONCAT, tn);
408 [ + + ]: 26014 : for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; ++i)
409 : : {
410 : 22463 : TypeNode bvt = d_nm->mkBitVectorType(i + 1);
411 : 89852 : TypeNode ftype = d_nm->mkFunctionType({btn, curr.getType()}, bvt);
412 : 44926 : Node bbt = getSymbolInternal(k, ftype, "from_bools");
413 [ + + ][ - - ]: 67389 : curr = mkApplyUf(bbt, {n[nchild - (i + 1)], curr});
414 : 22463 : }
415 : 3551 : return curr;
416 : 3551 : }
417 [ + + ]: 1683840 : else if (k == Kind::SEP_NIL)
418 : : {
419 : 6 : Node tnn = typeAsNode(convertType(tn));
420 : 3 : TypeNode ftype = d_nm->mkFunctionType(d_sortType, tn);
421 : 6 : Node s = getSymbolInternal(k, ftype, "sep.nil");
422 : 6 : return mkApplyUf(s, {tnn});
423 : 3 : }
424 [ + + ][ + + ]: 1683837 : else if (NodeManager::isNAryKind(k) && n.getNumChildren() >= 2)
[ + + ]
425 : : {
426 : 550082 : size_t nchild = n.getNumChildren();
427 [ - + ][ - + ]: 550082 : Assert(n.getMetaKind() != metakind::PARAMETERIZED);
[ - - ]
428 : : // convert all n-ary applications to binary
429 : 550082 : std::vector<Node> children(n.begin(), n.end());
430 : : // distinct is special case
431 [ + + ]: 550082 : if (k == Kind::DISTINCT)
432 : : {
433 : : // DISTINCT(x1,...,xn) --->
434 : : // AND(DISTINCT(x1,x2), AND(,..., AND(,..,DISTINCT(x_{n-1},x_n))))
435 : 3188 : Node ret = d_nm->mkNode(k, children[0], children[1]);
436 [ + + ]: 5872 : for (unsigned i = 0; i < nchild; i++)
437 [ + + ]: 30979 : for (unsigned j = i + 1; j < nchild; j++)
438 : : {
439 [ + + ][ + - ]: 26701 : if (i != 0 && j != 1)
440 : : {
441 : 48034 : ret = d_nm->mkNode(
442 : 72051 : Kind::AND, ret, d_nm->mkNode(k, children[i], children[j]));
443 : : }
444 : : }
445 [ + - ]: 3188 : Trace("lfsc-term-process-debug") << "n: " << n << std::endl
446 : 1594 : << "ret: " << ret << std::endl;
447 : 1594 : return ret;
448 : 1594 : }
449 : 548488 : std::reverse(children.begin(), children.end());
450 : : // Add the null-terminator. This is done to disambiguate the number
451 : : // of children for term with n-ary operators. In particular note that
452 : : // (or A B C (or D E)) has representation:
453 : : // (or A (or B (or C (or (or D E) false))))
454 : : // This makes the AST above distinguishable from (or A B C D E),
455 : : // which otherwise would both have representation:
456 : : // (or A (or B (or C (or D E))))
457 : 548488 : Node nullTerm = getNullTerminator(d_nm, k, tn);
458 : : // Most operators simply get binarized
459 : 548488 : Node ret;
460 : 548488 : size_t istart = 0;
461 [ + + ]: 548488 : if (nullTerm.isNull())
462 : : {
463 : 71 : ret = children[0];
464 : 71 : istart = 1;
465 : : }
466 : : else
467 : : {
468 : : // must convert recursively, since nullTerm may have subterms.
469 : 548417 : ret = convert(nullTerm);
470 : : }
471 : : // check whether we are also changing the operator name, in which case
472 : : // we build a binary uninterpreted function opc
473 : 548488 : bool isArithOp =
474 [ + + ][ + + ]: 548488 : (k == Kind::ADD || k == Kind::MULT || k == Kind::NONLINEAR_MULT);
[ + + ]
475 : 548488 : std::stringstream arithOpName;
476 [ + + ]: 548488 : if (isArithOp)
477 : : {
478 : : // currently allow subtyping
479 : 99056 : arithOpName << "a.";
480 : 99056 : arithOpName << printer::smt2::Smt2Printer::smtKindString(k);
481 : : }
482 : : // now, iterate over children and make binary conversion
483 [ + + ]: 2699906 : for (size_t i = istart, npchild = children.size(); i < npchild; i++)
484 : : {
485 [ + + ]: 2151418 : if (isArithOp)
486 : : {
487 : : // Arithmetic operators must deal with permissive type rules for
488 : : // ADD, MULT, NONLINEAR_MULT. We use the properly typed operator to
489 : : // avoid debug failures.
490 : 285265 : TypeNode tn1 = children[i].getType();
491 : 285265 : TypeNode tn2 = ret.getType();
492 : 1141060 : TypeNode ftype = d_nm->mkFunctionType({tn1, tn2}, tn);
493 : 570530 : Node opc = getSymbolInternal(k, ftype, arithOpName.str());
494 [ + + ][ - - ]: 855795 : ret = mkApplyUf(opc, {children[i], ret});
495 : 285265 : }
496 : : else
497 : : {
498 : 1866153 : ret = d_nm->mkNode(k, children[i], ret);
499 : : }
500 : : }
501 [ + - ]: 1096976 : Trace("lfsc-term-process-debug")
502 : 548488 : << "...return n-ary conv " << ret << std::endl;
503 : 548488 : return ret;
504 : 550082 : }
505 : 1133755 : return n;
506 : 2587877 : }
507 : :
508 : 1279586 : Node LfscNodeConverter::mkApplyUf(Node op, const std::vector<Node>& args) const
509 : : {
510 : 1279586 : std::vector<Node> aargs;
511 [ + + ]: 1279586 : if (op.isVar())
512 : : {
513 : 1214114 : aargs.push_back(op);
514 : : }
515 : : else
516 : : {
517 : : // Note that dag threshold is disabled for printing operators.
518 : 65472 : std::stringstream ss;
519 : 65472 : options::ioutils::applyOutputLanguage(ss, Language::LANG_SMTLIB_V2_6);
520 : 65472 : options::ioutils::applyDagThresh(ss, 0);
521 : 65472 : ss << op;
522 : 130944 : Node opv = NodeManager::mkRawSymbol(ss.str(), op.getType());
523 : 65472 : aargs.push_back(opv);
524 : 65472 : }
525 : 1279586 : aargs.insert(aargs.end(), args.begin(), args.end());
526 : 2559172 : return d_nm->mkNode(Kind::APPLY_UF, aargs);
527 : 1279586 : }
528 : :
529 : 6861 : TypeNode LfscNodeConverter::preConvertType(TypeNode tn)
530 : : {
531 [ + + ]: 6861 : if (tn.getKind() == Kind::TUPLE_TYPE)
532 : : {
533 : : // Must collect the tuple type here, since at post-order traversal, the
534 : : // type has been modified and no longer maintains the mapping to its
535 : : // datatype encoding.
536 : 82 : d_declTypes.insert(tn);
537 : : }
538 : 6861 : return tn;
539 : : }
540 : :
541 : 6861 : TypeNode LfscNodeConverter::postConvertType(TypeNode tn)
542 : : {
543 : 6861 : TypeNode cur = tn;
544 : 6861 : Node tnn;
545 : 6861 : Kind k = tn.getKind();
546 [ + - ]: 13722 : Trace("lfsc-term-process-debug")
547 : 6861 : << "postConvertType " << tn << " " << tn.getNumChildren() << " " << k
548 : 6861 : << std::endl;
549 [ + + ]: 6861 : if (k == Kind::FUNCTION_TYPE)
550 : : {
551 : : // (-> T1 ... Tn T) is (arrow T1 .... (arrow Tn T))
552 : 2695 : std::vector<TypeNode> argTypes = tn.getArgTypes();
553 : : // also make the node embedding of the type
554 : 2695 : Node arrown = d_typeAsNode[d_arrow];
555 [ - + ][ - + ]: 2695 : Assert(!arrown.isNull());
[ - - ]
556 : 2695 : cur = tn.getRangeType();
557 : 2695 : tnn = typeAsNode(cur);
558 : 2695 : for (std::vector<TypeNode>::reverse_iterator it = argTypes.rbegin();
559 [ + + ]: 7702 : it != argTypes.rend();
560 : 5007 : ++it)
561 : : {
562 : 5007 : std::vector<TypeNode> aargs;
563 : 5007 : aargs.push_back(*it);
564 : 5007 : aargs.push_back(cur);
565 : 5007 : cur = d_nm->mkSort(d_arrow, aargs);
566 [ + + ][ - - ]: 15021 : tnn = mkApplyUf(arrown, {typeAsNode(*it), tnn});
567 : 5007 : }
568 : 2695 : }
569 [ + + ]: 4166 : else if (k == Kind::BITVECTOR_TYPE)
570 : : {
571 : 539 : tnn = d_typeKindToNodeCons[k];
572 : 539 : Node w = d_nm->mkConstInt(Rational(tn.getBitVectorSize()));
573 : 1078 : tnn = mkApplyUf(tnn, {w});
574 : 539 : }
575 [ + + ]: 3627 : else if (k == Kind::FLOATINGPOINT_TYPE)
576 : : {
577 : 6 : tnn = d_typeKindToNodeCons[k];
578 : 6 : Node e = d_nm->mkConstInt(Rational(tn.getFloatingPointExponentSize()));
579 : 6 : Node s = d_nm->mkConstInt(Rational(tn.getFloatingPointSignificandSize()));
580 [ + + ][ - - ]: 18 : tnn = mkApplyUf(tnn, {e, s});
581 : 6 : }
582 [ + + ]: 3621 : else if (k == Kind::TUPLE_TYPE)
583 : : {
584 : : // special case: tuples must be distinguished by their arity
585 : 82 : size_t nargs = tn.getNumChildren();
586 [ + + ]: 82 : if (nargs > 0)
587 : : {
588 : 81 : std::vector<TypeNode> types;
589 : 81 : std::vector<TypeNode> convTypes;
590 : 81 : std::vector<Node> targs;
591 [ + + ]: 260 : for (size_t i = 0; i < nargs; i++)
592 : : {
593 : 179 : TypeNode tnc = tn[i];
594 : 179 : types.push_back(d_sortType);
595 : 179 : convTypes.push_back(tnc);
596 : 179 : targs.push_back(typeAsNode(tnc));
597 : 179 : }
598 : 81 : TypeNode ftype = d_nm->mkFunctionType(types, d_sortType);
599 : : // must distinguish by arity
600 : 81 : std::stringstream ss;
601 : 81 : ss << "Tuple_" << nargs;
602 : 81 : tnn = mkApplyUf(getSymbolInternal(k, ftype, ss.str()), targs);
603 : : // we are changing its name, we must make a sort constructor
604 : 81 : cur = d_nm->mkSortConstructor(ss.str(), nargs);
605 : 81 : cur = d_nm->mkSort(cur, convTypes);
606 : 81 : }
607 : : else
608 : : {
609 : : // no need to convert type for tuples of size 0,
610 : : // type as node is simple
611 : 1 : tnn = getSymbolInternal(k, d_sortType, "UnitTuple");
612 : : }
613 : : }
614 [ + + ]: 3539 : else if (tn.getNumChildren() == 0)
615 : : {
616 [ - + ][ - + ]: 3135 : Assert(!tn.isTuple());
[ - - ]
617 : : // an uninterpreted sort, or an uninstantiatied (maybe parametric) datatype
618 : 3135 : d_declTypes.insert(tn);
619 : 3135 : std::stringstream ss;
620 : 3135 : options::ioutils::applyOutputLanguage(ss, Language::LANG_SMTLIB_V2_6);
621 : 3135 : tn.toStream(ss);
622 [ + + ]: 3135 : if (tn.isUninterpretedSortConstructor())
623 : : {
624 : 11 : std::string s = getNameForUserNameOfInternal(tn.getId(), ss.str());
625 : 11 : tnn = getSymbolInternal(k, d_sortType, s, false);
626 : : cur =
627 : 11 : d_nm->mkSortConstructor(s, tn.getUninterpretedSortConstructorArity());
628 : 11 : }
629 [ + + ][ + + ]: 3124 : else if (tn.isUninterpretedSort() || tn.isDatatype())
[ + + ]
630 : : {
631 : 1551 : std::string s = getNameForUserNameOfInternal(tn.getId(), ss.str());
632 : 1551 : tnn = getSymbolInternal(k, d_sortType, s, false);
633 : 1551 : cur = d_nm->mkSort(s);
634 : 1551 : }
635 : : else
636 : : {
637 : : // all other builtin type constants, e.g. Int
638 : 1573 : tnn = getSymbolInternal(k, d_sortType, ss.str());
639 : : }
640 : 3135 : }
641 : : else
642 : : {
643 : : // to build the type-as-node, must convert the component types
644 : 404 : std::vector<Node> targs;
645 : 404 : std::vector<TypeNode> types;
646 [ + + ]: 989 : for (const TypeNode& tnc : tn)
647 : : {
648 : 585 : targs.push_back(typeAsNode(tnc));
649 : 585 : types.push_back(d_sortType);
650 : 585 : }
651 : 404 : Node op;
652 [ + + ]: 404 : if (k == Kind::PARAMETRIC_DATATYPE)
653 : : {
654 : : // note we don't add to declared types here, since the parametric
655 : : // datatype is traversed and will be declared as a type constructor
656 : : // erase first child, which repeats the datatype
657 : 9 : targs.erase(targs.begin(), targs.begin() + 1);
658 : 9 : types.erase(types.begin(), types.begin() + 1);
659 : 9 : TypeNode ftype = d_nm->mkFunctionType(types, d_sortType);
660 : : // the operator has been converted; it is no longer a datatype, thus
661 : : // we must print to get its name.
662 : 9 : std::stringstream ss;
663 : 9 : ss << tn[0];
664 : 9 : op = getSymbolInternal(k, ftype, ss.str());
665 : 9 : }
666 [ + + ]: 395 : else if (k == Kind::INSTANTIATED_SORT_TYPE)
667 : : {
668 : : // We don't add to declared types here. The type constructor is already
669 : : // added to declare types when processing the children of this.
670 : : // Also, similar to PARAMETRIC_DATATYPE, the type constructor
671 : : // should be erased from children.
672 : 39 : targs.erase(targs.begin(), targs.begin() + 1);
673 : 39 : types.erase(types.begin(), types.begin() + 1);
674 : 39 : TypeNode ftype = d_nm->mkFunctionType(types, d_sortType);
675 : 39 : std::string name = tn.getUninterpretedSortConstructor().getName();
676 : 39 : op = getSymbolInternal(k, ftype, name, false);
677 : 39 : }
678 [ + + ]: 356 : else if (k == Kind::NULLABLE_TYPE)
679 : : {
680 : 2 : TypeNode ftype = d_nm->mkFunctionType(d_sortType, d_sortType);
681 : 2 : op = getSymbolInternal(k, ftype, "Nullable", false);
682 : 2 : }
683 : : else
684 : : {
685 : 354 : std::map<Kind, Node>::iterator it = d_typeKindToNodeCons.find(k);
686 [ + - ]: 354 : if (it != d_typeKindToNodeCons.end())
687 : : {
688 : 354 : op = it->second;
689 : : }
690 : : }
691 [ + - ]: 404 : if (!op.isNull())
692 : : {
693 : 404 : tnn = mkApplyUf(op, targs);
694 : : }
695 : : else
696 : : {
697 : 0 : AlwaysAssert(false);
698 : : }
699 : 404 : }
700 [ - + ][ - + ]: 6861 : Assert(!tnn.isNull());
[ - - ]
701 [ + - ]: 6861 : Trace("lfsc-term-process-debug") << "...type as node: " << tnn << std::endl;
702 : 6861 : d_typeAsNode[cur] = tnn;
703 : 13722 : return cur;
704 : 6861 : }
705 : :
706 : 26144 : std::string LfscNodeConverter::getNameForUserName(const std::string& name,
707 : : size_t variant)
708 : : {
709 : : // For user name X, we do cvc.Y, where Y contains an escaped version of X.
710 : : // Specifically, since LFSC does not allow these characters in identifier
711 : : // bodies: "() \t\n\f;", each is replaced with an escape sequence "\xXX"
712 : : // where XX is the zero-padded hex representation of the code point. "\\" is
713 : : // also escaped.
714 : : //
715 : : // See also: https://github.com/cvc5/LFSC/blob/master/src/lexer.flex#L24
716 : : //
717 : : // The "cvc." prefix ensures we do not clash with LFSC definitions.
718 : : //
719 : : // The escaping ensures that all names are valid LFSC identifiers.
720 : 26144 : std::stringstream ss;
721 : 26144 : ss << "cvc";
722 [ + + ]: 26144 : if (variant != 0)
723 : : {
724 : 46 : ss << variant;
725 : : }
726 : 26144 : ss << ".";
727 : 26144 : std::string sanitized = ss.str();
728 : 26144 : size_t found = sanitized.size();
729 : 26144 : sanitized += name;
730 : : // The following sanitizes symbols that are not allowed in LFSC identifiers
731 : : // here, e.g.
732 : : // |a b|
733 : : // is converted to:
734 : : // cvc.a\x20b
735 : : // where "20" is the hex unicode value of " ".
736 : : do
737 : : {
738 : 27391 : found = sanitized.find_first_of("() \t\n\f\\;", found);
739 [ + + ]: 27391 : if (found != std::string::npos)
740 : : {
741 : : // Emit hex sequence
742 : 1247 : std::stringstream seq;
743 : 1247 : seq << "\\x" << std::setbase(16) << std::setfill('0') << std::setw(2)
744 : 1247 : << static_cast<size_t>(sanitized[found]);
745 : 1247 : sanitized.replace(found, 1, seq.str());
746 : : // increment found over the escape
747 : 1247 : found += 3;
748 : 1247 : }
749 [ + + ]: 27391 : } while (found != std::string::npos);
750 : 52288 : return sanitized;
751 : 26144 : }
752 : :
753 : 24572 : std::string LfscNodeConverter::getNameForUserNameOf(Node v)
754 : : {
755 : 24572 : std::string name = v.getName();
756 : 49144 : return getNameForUserNameOfInternal(v.getId(), name);
757 : 24572 : }
758 : :
759 : 26134 : std::string LfscNodeConverter::getNameForUserNameOfInternal(
760 : : uint64_t id, const std::string& name)
761 : : {
762 : 26134 : std::vector<uint64_t>& syms = d_userSymbolList[name];
763 : 26134 : size_t variant = 0;
764 : : std::vector<uint64_t>::iterator itr =
765 : 26134 : std::find(syms.begin(), syms.end(), id);
766 [ + + ]: 26134 : if (itr != syms.cend())
767 : : {
768 : 6857 : variant = std::distance(syms.begin(), itr);
769 : : }
770 : : else
771 : : {
772 : 19277 : variant = syms.size();
773 : 19277 : syms.push_back(id);
774 : : }
775 : 52268 : return getNameForUserName(name, variant);
776 : : }
777 : :
778 : 2596906 : bool LfscNodeConverter::shouldTraverse(Node n)
779 : : {
780 : 2596906 : Kind k = n.getKind();
781 : : // don't convert bound variable or instantiation pattern list directly
782 [ + + ][ + + ]: 2596906 : if (k == Kind::BOUND_VAR_LIST || k == Kind::INST_PATTERN_LIST)
783 : : {
784 : 10741 : return false;
785 : : }
786 : : // should not traverse internal applications
787 [ + + ]: 2586165 : if (k == Kind::APPLY_UF)
788 : : {
789 [ + + ]: 37487 : if (d_symbols.find(n.getOperator()) != d_symbols.end())
790 : : {
791 : 4128 : return false;
792 : : }
793 : : }
794 : 2582037 : return true;
795 : : }
796 : :
797 : 3270 : Node LfscNodeConverter::maybeMkSkolemFun(Node k)
798 : : {
799 : 3270 : SkolemManager* sm = d_nm->getSkolemManager();
800 : 3270 : SkolemId sfi = SkolemId::NONE;
801 : 3270 : Node cacheVal;
802 : 3270 : TypeNode tn = k.getType();
803 [ + + ]: 3270 : if (sm->isSkolemFunction(k, sfi, cacheVal))
804 : : {
805 [ + + ]: 805 : if (sfi == SkolemId::RE_UNFOLD_POS_COMPONENT)
806 : : {
807 : : // a skolem corresponding to a regular expression unfolding component
808 : : // should print as (skolem_re_unfold_pos t R n) where the skolem is the
809 : : // n^th component for the unfolding of (str.in_re t R).
810 : 100 : TypeNode strType = d_nm->stringType();
811 : 100 : TypeNode reType = d_nm->regExpType();
812 : 100 : TypeNode intType = d_nm->integerType();
813 : 500 : TypeNode reut = d_nm->mkFunctionType({strType, reType, intType}, strType);
814 : 200 : Node sk = getSymbolInternal(k.getKind(), reut, "skolem_re_unfold_pos");
815 [ + - ][ + - ]: 100 : Assert(!cacheVal.isNull() && cacheVal.getKind() == Kind::SEXPR
[ + - ][ + - ]
[ - + ][ - + ]
[ - - ]
816 : : && cacheVal.getNumChildren() == 3);
817 : : // third value is mpz, which is not converted
818 : 300 : return mkApplyUf(sk,
819 [ + + ][ - - ]: 400 : {convert(cacheVal[0]), convert(cacheVal[1]), cacheVal[2]});
820 : 100 : }
821 : : }
822 : 3170 : return Node::null();
823 : 3270 : }
824 : :
825 : 80312 : Node LfscNodeConverter::typeAsNode(TypeNode tni) const
826 : : {
827 : : // should always exist in the cache, as we always run types through
828 : : // postConvertType before calling this method.
829 : 80312 : std::map<TypeNode, Node>::const_iterator it = d_typeAsNode.find(tni);
830 [ - + ][ - + ]: 80312 : AlwaysAssert(it != d_typeAsNode.end()) << "Missing typeAsNode " << tni;
[ - - ]
831 : 160624 : return it->second;
832 : : }
833 : :
834 : 508380 : Node LfscNodeConverter::mkInternalSymbol(const std::string& name,
835 : : TypeNode tn,
836 : : bool useRawSym)
837 : : {
838 : : // use raw symbol so that it is never quoted
839 : : Node sym = useRawSym ? NodeManager::mkRawSymbol(name, tn)
840 [ + + ]: 508380 : : NodeManager::mkBoundVar(name, tn);
841 : 508380 : d_symbols.insert(sym);
842 : 508380 : return sym;
843 : 0 : }
844 : :
845 : 623 : Node LfscNodeConverter::getSymbolInternalFor(Node n,
846 : : const std::string& name,
847 : : bool useRawSym)
848 : : {
849 : 1246 : return getSymbolInternal(n.getKind(), n.getType(), name, useRawSym);
850 : : }
851 : :
852 : 1463935 : Node LfscNodeConverter::getSymbolInternal(Kind k,
853 : : TypeNode tn,
854 : : const std::string& name,
855 : : bool useRawSym)
856 : : {
857 : 1463935 : std::tuple<Kind, TypeNode, std::string> key(k, tn, name);
858 : : std::map<std::tuple<Kind, TypeNode, std::string>, Node>::iterator it =
859 : 1463935 : d_symbolsMap.find(key);
860 [ + + ]: 1463935 : if (it != d_symbolsMap.end())
861 : : {
862 : 1404099 : return it->second;
863 : : }
864 : 59836 : Node sym = mkInternalSymbol(name, tn, useRawSym);
865 : 59836 : d_symbolToBuiltinKind[sym] = k;
866 : 59836 : d_symbolsMap[key] = sym;
867 : 59836 : return sym;
868 : 1463935 : }
869 : :
870 : 1467 : void LfscNodeConverter::getCharVectorInternal(Node c, std::vector<Node>& chars)
871 : : {
872 [ - + ][ - + ]: 1467 : Assert(c.getKind() == Kind::CONST_STRING);
[ - - ]
873 : 1467 : const std::vector<unsigned>& vec = c.getConst<String>().getVec();
874 [ + + ]: 1467 : if (vec.size() == 0)
875 : : {
876 : 1246 : Node ec = getSymbolInternalFor(c, "emptystr");
877 : 623 : chars.push_back(ec);
878 : 623 : return;
879 : 623 : }
880 : 1688 : TypeNode tnc = d_nm->mkFunctionType(d_nm->integerType(), c.getType());
881 : 1688 : Node aconstf = getSymbolInternal(Kind::CONST_STRING, tnc, "char");
882 [ + + ]: 4594 : for (unsigned i = 0, size = vec.size(); i < size; i++)
883 : : {
884 : 15000 : Node cc = mkApplyUf(aconstf, {d_nm->mkConstInt(Rational(vec[i]))});
885 : 3750 : chars.push_back(cc);
886 : 3750 : }
887 : 844 : }
888 : :
889 : 1440 : Node LfscNodeConverter::convertBitVector(const BitVector& bv)
890 : : {
891 : 1440 : TypeNode btn = d_nm->booleanType();
892 : 5760 : TypeNode btnv = d_nm->mkFunctionType({btn, btn}, btn);
893 : 1440 : size_t w = bv.getSize();
894 : 2880 : Node ret = getSymbolInternal(Kind::CONST_BITVECTOR, btn, "bvn");
895 : 2880 : Node b0 = getSymbolInternal(Kind::CONST_BITVECTOR, btn, "b0");
896 : 2880 : Node b1 = getSymbolInternal(Kind::CONST_BITVECTOR, btn, "b1");
897 : 2880 : Node bvc = getSymbolInternal(Kind::CONST_BITVECTOR, btnv, "bvc");
898 [ + + ]: 23159 : for (size_t i = 0; i < w; i++)
899 : : {
900 [ + + ]: 21719 : Node arg = bv.isBitSet((w - 1) - i) ? b1 : b0;
901 [ + + ][ - - ]: 65157 : ret = mkApplyUf(bvc, {arg, ret});
902 : 21719 : }
903 : 2880 : return ret;
904 : 1440 : }
905 : :
906 : 843904 : Node LfscNodeConverter::getNullTerminator(NodeManager* nm, Kind k, TypeNode tn)
907 : : {
908 : 843904 : Node nullTerm;
909 [ + + ][ + + ]: 843904 : switch (k)
[ + ]
910 : : {
911 : : // LFSC signature expects mixed arithmetic for null terminators
912 : 92067 : case Kind::ADD:
913 : 92067 : nullTerm = nm->mkConstInt(Rational(0));
914 : 92067 : break;
915 : 27715 : case Kind::MULT:
916 : : case Kind::NONLINEAR_MULT:
917 : 27715 : nullTerm = nm->mkConstInt(Rational(1));
918 : 27715 : break;
919 : 368 : case Kind::REGEXP_CONCAT:
920 : : // the language containing only the empty string, which has special
921 : : // syntax in LFSC
922 : 368 : nullTerm = getSymbolInternal(k, tn, "re.empty");
923 : 368 : break;
924 : 9027 : case Kind::BITVECTOR_CONCAT:
925 : : {
926 : : // the null terminator of bitvector concat is a dummy variable of
927 : : // bit-vector type with zero width, regardless of the type of the overall
928 : : // concat.
929 : 9027 : TypeNode bvz = d_nm->mkBitVectorType(0);
930 : 9027 : nullTerm = getSymbolInternal(k, bvz, "emptybv");
931 : 9027 : }
932 : 9027 : break;
933 : 714727 : default:
934 : : // no special handling, or not null terminated
935 : 714727 : break;
936 : : }
937 [ + + ]: 843904 : if (!nullTerm.isNull())
938 : : {
939 : 129177 : return nullTerm;
940 : : }
941 : : // otherwise, fall back to standard utility
942 : 714727 : return expr::getNullTerminator(nm, k, tn);
943 : 843904 : }
944 : :
945 : 0 : Kind LfscNodeConverter::getBuiltinKindForInternalSymbol(Node op) const
946 : : {
947 : 0 : std::map<Node, Kind>::const_iterator it = d_symbolToBuiltinKind.find(op);
948 [ - - ]: 0 : if (it != d_symbolToBuiltinKind.end())
949 : : {
950 : 0 : return it->second;
951 : : }
952 : 0 : return Kind::UNDEFINED_KIND;
953 : : }
954 : :
955 : 418723 : Node LfscNodeConverter::getOperatorOfTerm(Node n, bool macroApply)
956 : : {
957 [ - + ][ - + ]: 418723 : Assert(n.hasOperator());
[ - - ]
958 [ - + ][ - + ]: 418723 : Assert(!n.isClosure());
[ - - ]
959 : 418723 : Kind k = n.getKind();
960 : 418723 : std::stringstream opName;
961 [ + - ]: 837446 : Trace("lfsc-term-process-debug2")
962 : 0 : << "getOperatorOfTerm " << n << " " << k << " "
963 : 0 : << (n.getMetaKind() == metakind::PARAMETERIZED) << " "
964 : 418723 : << GenericOp::isIndexedOperatorKind(k) << std::endl;
965 [ + + ]: 418723 : if (n.getMetaKind() == metakind::PARAMETERIZED)
966 : : {
967 : 85686 : Node op = n.getOperator();
968 : 85686 : std::vector<Node> indices;
969 [ + + ]: 85686 : if (GenericOp::isIndexedOperatorKind(k))
970 : : {
971 : 15310 : indices = GenericOp::getIndicesForOperator(k, n.getOperator());
972 : : // we must convert the name of indices on updaters and testers
973 [ + + ][ + + ]: 15310 : if (k == Kind::APPLY_UPDATER || k == Kind::APPLY_TESTER)
974 : : {
975 [ - + ][ - + ]: 869 : Assert(indices.size() == 1);
[ - - ]
976 : : // must convert to user name
977 : 869 : TypeNode intType = d_nm->integerType();
978 : 869 : indices[0] =
979 : 1738 : getSymbolInternal(k, intType, getNameForUserNameOf(indices[0]));
980 : 869 : }
981 : : }
982 [ + + ]: 70376 : else if (op.getType().isFunction())
983 : : {
984 : 64388 : return op;
985 : : }
986 : : // note other kinds of functions (e.g. selectors and testers)
987 : 21298 : std::vector<TypeNode> argTypes;
988 [ + + ]: 46423 : for (const Node& nc : n)
989 : : {
990 : 25125 : argTypes.push_back(nc.getType());
991 : 25125 : }
992 : 21298 : TypeNode ftype = n.getType();
993 [ + + ]: 21298 : if (!argTypes.empty())
994 : : {
995 : 21144 : ftype = d_nm->mkFunctionType(argTypes, ftype);
996 : : }
997 : 21298 : Node ret;
998 [ + + ]: 21298 : if (GenericOp::isIndexedOperatorKind(k))
999 : : {
1000 : 15310 : std::vector<TypeNode> itypes;
1001 [ + + ]: 34496 : for (const Node& i : indices)
1002 : : {
1003 : 19186 : itypes.push_back(i.getType());
1004 : : }
1005 [ + - ]: 15310 : if (!itypes.empty())
1006 : : {
1007 : 15310 : ftype = d_nm->mkFunctionType(itypes, ftype);
1008 : : }
1009 [ + + ]: 15310 : if (!macroApply)
1010 : : {
1011 [ + + ][ + + ]: 2229 : if (k != Kind::APPLY_UPDATER && k != Kind::APPLY_TESTER)
1012 : : {
1013 : 2145 : opName << "f_";
1014 : : }
1015 : : }
1016 : : // must avoid overloading for to_fp variants
1017 [ + + ]: 15310 : if (k == Kind::FLOATINGPOINT_TO_FP_FROM_FP)
1018 : : {
1019 : 1 : opName << "to_fp_fp";
1020 : : }
1021 [ - + ]: 15309 : else if (k == Kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV)
1022 : : {
1023 : 0 : opName << "to_fp_ieee_bv";
1024 : : }
1025 [ + + ]: 15309 : else if (k == Kind::FLOATINGPOINT_TO_FP_FROM_SBV)
1026 : : {
1027 : 4 : opName << "to_fp_sbv";
1028 : : }
1029 [ + + ]: 15305 : else if (k == Kind::FLOATINGPOINT_TO_FP_FROM_REAL)
1030 : : {
1031 : 2 : opName << "to_fp_real";
1032 : : }
1033 [ + + ]: 15303 : else if (k == Kind::BITVECTOR_BIT)
1034 : : {
1035 : 4137 : opName << "bit";
1036 : : }
1037 [ + + ]: 11166 : else if (k==Kind::DIVISIBLE)
1038 : : {
1039 : 2 : opName << "a.divisible";
1040 : : }
1041 : : else
1042 : : {
1043 : 11164 : opName << printer::smt2::Smt2Printer::smtKindString(k);
1044 : : }
1045 : 15310 : }
1046 [ + + ]: 5988 : else if (k == Kind::APPLY_CONSTRUCTOR)
1047 : : {
1048 : 3718 : unsigned index = DType::indexOf(op);
1049 : 3718 : const DType& dt = DType::datatypeOf(op);
1050 : : // get its variable name
1051 : 3718 : opName << getNameForUserNameOf(dt[index].getConstructor());
1052 : : }
1053 [ + - ]: 2270 : else if (k == Kind::APPLY_SELECTOR)
1054 : : {
1055 : 2270 : ret = maybeMkSkolemFun(op);
1056 [ + - ]: 2270 : if (ret.isNull())
1057 : : {
1058 : 2270 : unsigned index = DType::indexOf(op);
1059 : 2270 : const DType& dt = DType::datatypeOf(op);
1060 : 2270 : unsigned cindex = DType::cindexOf(op);
1061 : 2270 : opName << getNameForUserNameOf(dt[cindex][index].getSelector());
1062 : : }
1063 : : }
1064 [ - - ][ - - ]: 0 : else if (k == Kind::SET_SINGLETON || k == Kind::BAG_MAKE
1065 [ - - ]: 0 : || k == Kind::SEQ_UNIT)
1066 : : {
1067 [ - - ]: 0 : if (!macroApply)
1068 : : {
1069 : 0 : opName << "f_";
1070 : : }
1071 : 0 : opName << printer::smt2::Smt2Printer::smtKindString(k);
1072 : : }
1073 : : else
1074 : : {
1075 : 0 : opName << op;
1076 : : }
1077 [ + - ]: 21298 : if (ret.isNull())
1078 : : {
1079 [ + - ]: 21298 : Trace("lfsc-term-process-debug2") << "...default symbol" << std::endl;
1080 : 21298 : ret = getSymbolInternal(k, ftype, opName.str());
1081 : : }
1082 : : // if indexed, apply to index
1083 [ + + ]: 21298 : if (!indices.empty())
1084 : : {
1085 : 15310 : ret = mkApplyUf(ret, indices);
1086 : : }
1087 [ + - ]: 21298 : Trace("lfsc-term-process-debug2") << "...return " << ret << std::endl;
1088 : 21298 : return ret;
1089 : 85686 : }
1090 : 333037 : std::vector<TypeNode> argTypes;
1091 [ + + ]: 1125985 : for (const Node& nc : n)
1092 : : {
1093 : 792948 : argTypes.push_back(nc.getType());
1094 : 792948 : }
1095 : : // we only use binary operators
1096 [ + + ]: 333037 : if (NodeManager::isNAryKind(k))
1097 : : {
1098 : 149741 : argTypes.resize(2);
1099 : : }
1100 : 333037 : TypeNode tn = n.getType();
1101 : 333037 : TypeNode ftype = d_nm->mkFunctionType(argTypes, tn);
1102 : : // most functions are called f_X where X is the SMT-LIB name, if we are
1103 : : // getting the macroApply variant, then we don't prefix with `f_`.
1104 [ + + ]: 333037 : if (!macroApply)
1105 : : {
1106 : 257389 : opName << "f_";
1107 : : }
1108 [ + + ]: 333037 : if (k == Kind::FLOATINGPOINT_COMPONENT_NAN
1109 [ + + ]: 333035 : || k == Kind::FLOATINGPOINT_COMPONENT_INF
1110 [ + + ]: 333034 : || k == Kind::FLOATINGPOINT_COMPONENT_ZERO
1111 [ + + ]: 333033 : || k == Kind::FLOATINGPOINT_COMPONENT_SIGN
1112 [ + + ]: 333031 : || k == Kind::FLOATINGPOINT_COMPONENT_EXPONENT
1113 [ + + ]: 333030 : || k == Kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND
1114 [ - + ]: 333029 : || k == Kind::ROUNDINGMODE_BITBLAST)
1115 : : {
1116 : : // remove @fp.
1117 : 8 : std::string str = printer::smt2::Smt2Printer::smtKindString(k);
1118 : 8 : opName << str.substr(4);
1119 : 8 : }
1120 : : else
1121 : : {
1122 : : // all arithmetic kinds must explicitly deal with real vs int subtyping
1123 [ + + ][ + + ]: 333029 : if (k == Kind::ADD || k == Kind::MULT || k == Kind::NONLINEAR_MULT
[ + + ]
1124 [ + + ][ + + ]: 251667 : || k == Kind::GEQ || k == Kind::GT || k == Kind::LEQ || k == Kind::LT
[ + + ][ + + ]
1125 [ + + ][ + + ]: 168224 : || k == Kind::SUB || k == Kind::DIVISION || k == Kind::DIVISION_TOTAL
[ + + ]
1126 [ + + ][ + + ]: 165695 : || k == Kind::INTS_DIVISION || k == Kind::INTS_DIVISION_TOTAL
1127 [ + + ][ + + ]: 165083 : || k == Kind::INTS_MODULUS || k == Kind::INTS_MODULUS_TOTAL
1128 [ + + ][ + + ]: 164508 : || k == Kind::NEG || k == Kind::POW)
1129 : : {
1130 : : // currently allow subtyping
1131 : 169159 : opName << "a.";
1132 : : }
1133 [ + + ]: 333029 : if (k == Kind::NEG)
1134 : : {
1135 : 635 : opName << "u";
1136 : : }
1137 : 333029 : opName << printer::smt2::Smt2Printer::smtKindString(k);
1138 : : }
1139 : 333037 : return getSymbolInternal(k, ftype, opName.str());
1140 : 418723 : }
1141 : :
1142 : 51550 : Node LfscNodeConverter::getOperatorOfClosure(Node q,
1143 : : bool macroApply,
1144 : : bool isPartial)
1145 : : {
1146 : 51550 : TypeNode retType = isPartial ? q[1].getType() : q.getType();
1147 : 103100 : TypeNode bodyType = d_nm->mkFunctionType(q[1].getType(), retType);
1148 : : // We permit non-flat function types here
1149 : : // intType is used here for variable indices
1150 : 51550 : TypeNode intType = d_nm->integerType();
1151 : 206200 : TypeNode ftype = d_nm->mkFunctionType({intType, d_sortType}, bodyType);
1152 : 51550 : Kind k = q.getKind();
1153 : 51550 : std::stringstream opName;
1154 [ + + ]: 51550 : if (!macroApply)
1155 : : {
1156 : 8424 : opName << "f_";
1157 : : }
1158 : 51550 : opName << printer::smt2::Smt2Printer::smtKindString(k);
1159 : 103100 : return getSymbolInternal(k, ftype, opName.str());
1160 : 51550 : }
1161 : :
1162 : 60953 : Node LfscNodeConverter::getOperatorOfBoundVar(Node cop, Node v)
1163 : : {
1164 : 121906 : Node x = d_nm->mkConstInt(Rational(getOrAssignIndexForBVar(v)));
1165 : 121906 : Node tc = typeAsNode(convertType(v.getType()));
1166 [ + + ][ - - ]: 243812 : return mkApplyUf(cop, {x, tc});
1167 : 60953 : }
1168 : :
1169 : 16562 : size_t LfscNodeConverter::getOrAssignIndexForFVar(Node fv)
1170 : : {
1171 : 16562 : std::map<Node, size_t>::iterator it = d_fvarIndex.find(fv);
1172 [ - + ]: 16562 : if (it != d_fvarIndex.end())
1173 : : {
1174 : 0 : return it->second;
1175 : : }
1176 : 16562 : size_t id = d_fvarIndex.size();
1177 : 16562 : d_fvarIndex[fv] = id;
1178 : 16562 : return id;
1179 : : }
1180 : :
1181 : 70748 : size_t LfscNodeConverter::getOrAssignIndexForBVar(Node bv)
1182 : : {
1183 [ - + ][ - + ]: 70748 : Assert(bv.isVar());
[ - - ]
1184 : 70748 : std::map<Node, size_t>::iterator it = d_bvarIndex.find(bv);
1185 [ + + ]: 70748 : if (it != d_bvarIndex.end())
1186 : : {
1187 : 60125 : return it->second;
1188 : : }
1189 : 10623 : size_t id = d_bvarIndex.size();
1190 : 10623 : d_bvarIndex[bv] = id;
1191 : 10623 : return id;
1192 : : }
1193 : :
1194 : 1724 : const std::unordered_set<Node>& LfscNodeConverter::getDeclaredSymbols() const
1195 : : {
1196 : 1724 : return d_declVars;
1197 : : }
1198 : :
1199 : 1724 : const std::unordered_set<TypeNode>& LfscNodeConverter::getDeclaredTypes() const
1200 : : {
1201 : 1724 : return d_declTypes;
1202 : : }
1203 : :
1204 : : } // namespace proof
1205 : : } // namespace cvc5::internal
|
