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-2025 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 : : * The pretty-printer interface for the SMT2 output language.
14 : : */
15 : :
16 : : #include "printer/smt2/smt2_printer.h"
17 : :
18 : : #include <cvc5/cvc5.h>
19 : :
20 : : #include <iostream>
21 : : #include <list>
22 : : #include <string>
23 : : #include <typeinfo>
24 : : #include <vector>
25 : :
26 : : #include "expr/array_store_all.h"
27 : : #include "expr/ascription_type.h"
28 : : #include "expr/cardinality_constraint.h"
29 : : #include "expr/dtype.h"
30 : : #include "expr/dtype_cons.h"
31 : : #include "expr/emptybag.h"
32 : : #include "expr/emptyset.h"
33 : : #include "expr/function_array_const.h"
34 : : #include "expr/node_visitor.h"
35 : : #include "expr/sequence.h"
36 : : #include "expr/skolem_manager.h"
37 : : #include "options/io_utils.h"
38 : : #include "options/language.h"
39 : : #include "printer/let_binding.h"
40 : : #include "proof/unsat_core.h"
41 : : #include "smt/model.h"
42 : : #include "theory/arrays/theory_arrays_rewriter.h"
43 : : #include "theory/builtin/abstract_type.h"
44 : : #include "theory/builtin/generic_op.h"
45 : : #include "theory/datatypes/project_op.h"
46 : : #include "theory/datatypes/sygus_datatype_utils.h"
47 : : #include "theory/quantifiers/quantifiers_attributes.h"
48 : : #include "theory/strings/theory_strings_utils.h"
49 : : #include "theory/theory_model.h"
50 : : #include "theory/uf/function_const.h"
51 : : #include "theory/uf/theory_uf_rewriter.h"
52 : : #include "util/bitvector.h"
53 : : #include "util/divisible.h"
54 : : #include "util/finite_field_value.h"
55 : : #include "util/floatingpoint.h"
56 : : #include "util/iand.h"
57 : : #include "util/indexed_root_predicate.h"
58 : : #include "util/real_algebraic_number.h"
59 : : #include "util/regexp.h"
60 : : #include "util/smt2_quote_string.h"
61 : : #include "util/string.h"
62 : : #include "util/uninterpreted_sort_value.h"
63 : :
64 : : using namespace std;
65 : :
66 : : namespace cvc5::internal {
67 : : namespace printer {
68 : : namespace smt2 {
69 : :
70 : 2180326 : static void toStreamRational(std::ostream& out,
71 : : const Rational& r,
72 : : bool isReal,
73 : : Variant v)
74 : : {
75 : 2180326 : bool neg = r.sgn() < 0;
76 : 2180326 : bool arithTokens = options::ioutils::getPrintArithLitToken(out);
77 : : // Print the rational, possibly as a real.
78 : : // Notice that we print (/ (- 5) 3) instead of (- (/ 5 3)),
79 : : // the former is compliant with real values in the smt lib standard.
80 [ + + ]: 2180326 : if (r.isIntegral())
81 : : {
82 [ + + ]: 2122207 : if (arithTokens)
83 : : {
84 [ + + ]: 1670101 : if (neg)
85 : : {
86 : 198487 : out << "-" << -r;
87 : : }
88 : : else
89 : : {
90 : 1471614 : out << r;
91 : : }
92 [ + + ]: 1670101 : if (isReal)
93 : : {
94 : 220123 : out << "/1";
95 : : }
96 : : }
97 : : else
98 : : {
99 [ + + ]: 452106 : if (neg)
100 : : {
101 : 24637 : out << "(- " << -r;
102 : : }
103 : : else
104 : : {
105 : 427469 : out << r;
106 : : }
107 [ + + ]: 452106 : if (isReal)
108 : : {
109 : 67821 : out << ".0";
110 : : }
111 [ + + ]: 452106 : if (neg)
112 : : {
113 : 24637 : out << ")";
114 : : }
115 : : }
116 : : }
117 : : else
118 : : {
119 [ - + ][ - + ]: 58119 : Assert(isReal);
[ - - ]
120 [ + + ]: 58119 : if (arithTokens)
121 : : {
122 [ + + ]: 25791 : if (neg)
123 : : {
124 : 13223 : Rational abs_r = (-r);
125 : 13223 : out << '-' << abs_r.getNumerator() << '/' << abs_r.getDenominator();
126 : 13223 : }
127 : : else
128 : : {
129 : 12568 : out << r.getNumerator() << '/' << r.getDenominator();
130 : : }
131 : : }
132 : : else
133 : : {
134 : 32328 : out << "(/ ";
135 [ + + ]: 32328 : if (neg)
136 : : {
137 : 16343 : Rational abs_r = (-r);
138 : 16343 : out << "(- " << abs_r.getNumerator() << ") " << abs_r.getDenominator();
139 : 16343 : }
140 : : else
141 : : {
142 : 15985 : out << r.getNumerator() << ' ' << r.getDenominator();
143 : : }
144 : 32328 : out << ')';
145 : : }
146 : : }
147 : 2180326 : }
148 : :
149 : 10830462 : void Smt2Printer::toStream(std::ostream& out,
150 : : TNode n,
151 : : int toDepth,
152 : : size_t dag) const
153 : : {
154 [ + + ]: 10830462 : if (dag == 0)
155 : : {
156 : 6107220 : toStream(out, n, nullptr, toDepth);
157 : 6107220 : return;
158 : : }
159 : 9446484 : LetBinding lbind("_let_", dag + 1);
160 : :
161 : 4723242 : std::string cparen;
162 : 4723242 : std::vector<Node> letList;
163 : 4723242 : lbind.letify(n, letList);
164 [ + + ]: 4723242 : if (!letList.empty())
165 : : {
166 : 25485 : std::stringstream cparens;
167 : 25485 : std::map<Node, uint32_t>::const_iterator it;
168 [ + + ]: 256314 : for (size_t i = 0, nlets = letList.size(); i < nlets; i++)
169 : : {
170 : 230829 : Node nl = letList[i];
171 : 230829 : out << "(let ((";
172 : 230829 : uint32_t id = lbind.getId(nl);
173 : 230829 : out << "_let_" << id << " ";
174 : 230829 : toStream(out, nl, &lbind, toDepth, false);
175 : 230829 : out << ")) ";
176 : 230829 : cparens << ")";
177 : 230829 : }
178 : 25485 : cparen = cparens.str();
179 : 25485 : }
180 : : // Print the body, passing the lbind object. Note that we don't convert
181 : : // n here, and instead rely on the printing method to lookup ids in the
182 : : // given let binding.
183 : 4723242 : toStream(out, n, &lbind, toDepth);
184 : 4723242 : out << cparen;
185 : 4723242 : lbind.popScope();
186 : 4723242 : }
187 : :
188 : 4360185 : void Smt2Printer::toStream(std::ostream& out,
189 : : TNode n,
190 : : const LetBinding* lbind,
191 : : bool lbindTop) const
192 : : {
193 : 4360185 : int toDepth = options::ioutils::getNodeDepth(out);
194 : 4360185 : toStream(out, n, lbind, toDepth, lbindTop);
195 : 4360185 : }
196 : :
197 : 10695348 : void Smt2Printer::toStream(std::ostream& out, TNode n) const
198 : : {
199 : 10695348 : size_t dag = options::ioutils::getDagThresh(out);
200 : 10695348 : int toDepth = options::ioutils::getNodeDepth(out);
201 : 10695348 : toStream(out, n, toDepth, dag);
202 : 10695348 : }
203 : :
204 : 350526 : void Smt2Printer::toStream(std::ostream& out, Kind k) const
205 : : {
206 : 350526 : out << smtKindString(k);
207 : 350526 : }
208 : :
209 : 39353006 : bool Smt2Printer::toStreamBase(std::ostream& out,
210 : : TNode n,
211 : : const LetBinding* lbind,
212 : : int toDepth) const
213 : : {
214 : : // null
215 [ + + ]: 39353006 : if (n.getKind() == Kind::NULL_EXPR)
216 : : {
217 : 14 : out << "null";
218 : 14 : return true;
219 : : }
220 : :
221 : 39352992 : NodeManager* nm = n.getNodeManager();
222 : : // constant
223 [ + + ]: 39352992 : if (n.getMetaKind() == kind::metakind::CONSTANT)
224 : : {
225 [ + + ][ + + ]: 5401316 : switch (n.getKind())
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ - + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
226 : : {
227 : 573655 : case Kind::TYPE_CONSTANT:
228 [ + + ][ + + ]: 573655 : switch (n.getConst<TypeConstant>())
[ + + ][ - ]
229 : : {
230 : 152172 : case BOOLEAN_TYPE: out << "Bool"; break;
231 : 30071 : case REAL_TYPE: out << "Real"; break;
232 : 315070 : case INTEGER_TYPE: out << "Int"; break;
233 : 49422 : case STRING_TYPE: out << "String"; break;
234 : 26590 : case REGEXP_TYPE: out << "RegLan"; break;
235 : 330 : case ROUNDINGMODE_TYPE: out << "RoundingMode"; break;
236 : 0 : default:
237 : : // fall back on whatever operator<< does on underlying type; we
238 : : // might luck out and be SMT-LIB v2 compliant
239 : 0 : n.constToStream(out);
240 : : }
241 : 573655 : break;
242 : 146102 : case Kind::ABSTRACT_TYPE:
243 : : {
244 : 146102 : const AbstractType& at = n.getConst<AbstractType>();
245 : 146102 : Kind atk = at.getKind();
246 : 146102 : out << "?";
247 : : // note that the fully abstract type (where atk is ABSTRACT_TYPE) is
248 : : // printed simply as "?", not, e.g., "?Abstract"
249 [ + + ]: 146102 : if (atk != Kind::ABSTRACT_TYPE)
250 : : {
251 : 46487 : out << smtKindString(atk);
252 : : }
253 : 146102 : break;
254 : : }
255 : 2842 : case Kind::APPLY_INDEXED_SYMBOLIC_OP:
256 : 2842 : out << smtKindString(n.getConst<GenericOp>().getKind());
257 : 2842 : break;
258 : 68436 : case Kind::BITVECTOR_TYPE:
259 : 68436 : out << "(_ BitVec " << n.getConst<BitVectorSize>().d_size << ")";
260 : 68436 : break;
261 : 579 : case Kind::FINITE_FIELD_TYPE:
262 : 579 : out << "(_ FiniteField " << n.getConst<FfSize>().d_val << ")";
263 : 579 : break;
264 : 192 : case Kind::FLOATINGPOINT_TYPE:
265 : 192 : out << "(_ FloatingPoint "
266 : 192 : << n.getConst<FloatingPointSize>().exponentWidth() << " "
267 : 192 : << n.getConst<FloatingPointSize>().significandWidth() << ")";
268 : 192 : break;
269 : 171976 : case Kind::CONST_BITVECTOR:
270 : : {
271 : 171976 : const BitVector& bv = n.getConst<BitVector>();
272 [ + + ]: 171976 : if (options::ioutils::getBvPrintConstsAsIndexedSymbols(out))
273 : : {
274 : 10 : out << "(_ bv" << bv.getValue() << " " << bv.getSize() << ")";
275 : : }
276 : : else
277 : : {
278 : 171966 : out << "#b" << bv.toString();
279 : : }
280 : 171976 : break;
281 : : }
282 : 1070 : case Kind::CONST_FINITE_FIELD:
283 : : {
284 : 1070 : const FiniteFieldValue& ff = n.getConst<FiniteFieldValue>();
285 : 1070 : out << "#f" << ff.getValue() << "m" << ff.getFieldSize();
286 : 1070 : break;
287 : : }
288 : 496 : case Kind::CONST_FLOATINGPOINT:
289 : : {
290 : 992 : out << n.getConst<FloatingPoint>().toString(
291 : 496 : options::ioutils::getBvPrintConstsAsIndexedSymbols(out));
292 : 496 : break;
293 : : }
294 : 1151 : case Kind::CONST_ROUNDINGMODE:
295 [ + + ][ + + ]: 1151 : switch (n.getConst<RoundingMode>()) {
[ + - ]
296 : 345 : case RoundingMode::ROUND_NEAREST_TIES_TO_EVEN:
297 : 345 : out << "roundNearestTiesToEven";
298 : 345 : break;
299 : 181 : case RoundingMode::ROUND_NEAREST_TIES_TO_AWAY:
300 : 181 : out << "roundNearestTiesToAway";
301 : 181 : break;
302 : 173 : case RoundingMode::ROUND_TOWARD_POSITIVE:
303 : 173 : out << "roundTowardPositive";
304 : 173 : break;
305 : 173 : case RoundingMode::ROUND_TOWARD_NEGATIVE:
306 : 173 : out << "roundTowardNegative";
307 : 173 : break;
308 : 279 : case RoundingMode::ROUND_TOWARD_ZERO: out << "roundTowardZero"; break;
309 : 0 : default:
310 : 0 : Unreachable() << "Invalid value of rounding mode constant ("
311 : 0 : << n.getConst<RoundingMode>() << ")";
312 : : }
313 : 1151 : break;
314 : 2146849 : case Kind::CONST_BOOLEAN:
315 : : // the default would print "1" or "0" for bool, that's not correct
316 : : // for our purposes
317 [ + + ]: 2146849 : out << (n.getConst<bool>() ? "true" : "false");
318 : 2146849 : break;
319 : 36 : case Kind::BUILTIN: out << smtKindString(n.getConst<Kind>()); break;
320 : 346063 : case Kind::CONST_RATIONAL:
321 : : {
322 : 346063 : const Rational& r = n.getConst<Rational>();
323 : 346063 : toStreamRational(out, r, true, d_variant);
324 : 346063 : break;
325 : : }
326 : 1834263 : case Kind::CONST_INTEGER:
327 : : {
328 : 1834263 : const Rational& r = n.getConst<Rational>();
329 : 1834263 : toStreamRational(out, r, false, d_variant);
330 : 1834263 : break;
331 : : }
332 : :
333 : 66658 : case Kind::CONST_STRING:
334 : : {
335 : 66658 : std::string s = n.getConst<String>().toString();
336 : 66658 : out << '"';
337 [ + + ]: 270552 : for(size_t i = 0; i < s.size(); ++i) {
338 : 203894 : char c = s[i];
339 [ + + ]: 203894 : if(c == '"') {
340 : 39 : out << "\"\"";
341 : : } else {
342 : 203855 : out << c;
343 : : }
344 : : }
345 : 66658 : out << '"';
346 : 66658 : break;
347 : 66658 : }
348 : 674 : case Kind::CONST_SEQUENCE:
349 : : {
350 : 674 : const Sequence& sn = n.getConst<Sequence>();
351 : 674 : const std::vector<Node>& snvec = sn.getVec();
352 [ + + ]: 674 : if (snvec.empty())
353 : : {
354 : 474 : out << "(as seq.empty ";
355 : 474 : toStreamType(out, n.getType());
356 : 474 : out << ")";
357 : : }
358 : : else
359 : : {
360 : : // prints as the corresponding concatenation of seq.unit
361 : 200 : Node cc = theory::strings::utils::mkConcatForConstSequence(n);
362 : 200 : toStream(out, cc, lbind, toDepth);
363 : 200 : }
364 : 674 : break;
365 : : }
366 : :
367 : 204 : case Kind::STORE_ALL:
368 : : {
369 : 204 : ArrayStoreAll asa = n.getConst<ArrayStoreAll>();
370 : 204 : out << "((as const ";
371 : 204 : toStreamType(out, asa.getType());
372 : 204 : out << ") ";
373 [ - + ]: 204 : toStream(out, asa.getValue(), lbind, toDepth < 0 ? toDepth : toDepth - 1);
374 : 204 : out << ")";
375 : 204 : break;
376 : 204 : }
377 : 4476 : case Kind::FUNCTION_ARRAY_CONST:
378 : : {
379 : : // prints as the equivalent lambda
380 : 4476 : Node lam = theory::uf::FunctionConst::toLambda(n);
381 : 4476 : toStream(out, lam, lbind, toDepth);
382 : 4476 : break;
383 : 4476 : }
384 : :
385 : 1637 : case Kind::UNINTERPRETED_SORT_VALUE:
386 : : {
387 : 1637 : const UninterpretedSortValue& v = n.getConst<UninterpretedSortValue>();
388 : 3274 : out << "(as " << cvc5::internal::quoteSymbol(v.getSymbol()) << " "
389 : 1637 : << n.getType() << ")";
390 : 1637 : break;
391 : : }
392 : 91 : case Kind::CARDINALITY_CONSTRAINT_OP:
393 : : {
394 : : const CardinalityConstraint& cc =
395 : 91 : n.getConst<CardinalityConstraint>();
396 : 91 : TypeNode tn = cc.getType();
397 : 91 : out << "(_ fmf.card " << tn << " " << cc.getUpperBound() << ")";
398 : 91 : }
399 : 91 : break;
400 : 0 : case Kind::COMBINED_CARDINALITY_CONSTRAINT_OP:
401 : : {
402 : : const CombinedCardinalityConstraint& cc =
403 : 0 : n.getConst<CombinedCardinalityConstraint>();
404 : 0 : out << "(_ fmf.combined_card " << cc.getUpperBound() << ")";
405 : : }
406 : 0 : break;
407 : 30 : case Kind::DIVISIBLE_OP:
408 : 30 : out << "(_ divisible " << n.getConst<Divisible>().k << ")";
409 : 30 : break;
410 : 1120 : case Kind::SET_EMPTY:
411 : 1120 : out << "(as set.empty ";
412 : 1120 : toStreamType(out, n.getConst<EmptySet>().getType());
413 : 1120 : out << ")";
414 : 1120 : break;
415 : :
416 : 184 : case Kind::BAG_EMPTY:
417 : 184 : out << "(as bag.empty ";
418 : 184 : toStreamType(out, n.getConst<EmptyBag>().getType());
419 : 184 : out << ")";
420 : 184 : break;
421 : 8005 : case Kind::BITVECTOR_EXTRACT_OP:
422 : : {
423 : 8005 : BitVectorExtract p = n.getConst<BitVectorExtract>();
424 : 8005 : out << "(_ extract " << p.d_high << ' ' << p.d_low << ")";
425 : 8005 : break;
426 : : }
427 : 462 : case Kind::BITVECTOR_REPEAT_OP:
428 : 462 : out << "(_ repeat " << n.getConst<BitVectorRepeat>().d_repeatAmount
429 : 462 : << ")";
430 : 462 : break;
431 : 8917 : case Kind::BITVECTOR_ZERO_EXTEND_OP:
432 : 8917 : out << "(_ zero_extend "
433 : 8917 : << n.getConst<BitVectorZeroExtend>().d_zeroExtendAmount << ")";
434 : 8917 : break;
435 : 12594 : case Kind::BITVECTOR_SIGN_EXTEND_OP:
436 : 12594 : out << "(_ sign_extend "
437 : 12594 : << n.getConst<BitVectorSignExtend>().d_signExtendAmount << ")";
438 : 12594 : break;
439 : 314 : case Kind::BITVECTOR_ROTATE_LEFT_OP:
440 : 314 : out << "(_ rotate_left "
441 : 314 : << n.getConst<BitVectorRotateLeft>().d_rotateLeftAmount << ")";
442 : 314 : break;
443 : 375 : case Kind::BITVECTOR_ROTATE_RIGHT_OP:
444 : 375 : out << "(_ rotate_right "
445 : 375 : << n.getConst<BitVectorRotateRight>().d_rotateRightAmount << ")";
446 : 375 : break;
447 : 701 : case Kind::INT_TO_BITVECTOR_OP:
448 : 701 : out << "(_ int_to_bv " << n.getConst<IntToBitVector>().d_size << ")";
449 : 701 : break;
450 : 200 : case Kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV_OP:
451 : 200 : out << "(_ to_fp "
452 : 200 : << n.getConst<FloatingPointToFPIEEEBitVector>()
453 : 200 : .getSize()
454 : 200 : .exponentWidth()
455 : 200 : << ' '
456 : 200 : << n.getConst<FloatingPointToFPIEEEBitVector>()
457 : 200 : .getSize()
458 : 200 : .significandWidth()
459 : 200 : << ")";
460 : 200 : break;
461 : 10 : case Kind::FLOATINGPOINT_TO_FP_FROM_FP_OP:
462 : 10 : out << "(_ to_fp "
463 : 10 : << n.getConst<FloatingPointToFPFloatingPoint>()
464 : 10 : .getSize()
465 : 10 : .exponentWidth()
466 : 10 : << ' '
467 : 10 : << n.getConst<FloatingPointToFPFloatingPoint>()
468 : 10 : .getSize()
469 : 10 : .significandWidth()
470 : 10 : << ")";
471 : 10 : break;
472 : 37 : case Kind::FLOATINGPOINT_TO_FP_FROM_REAL_OP:
473 : 37 : out << "(_ to_fp "
474 : 37 : << n.getConst<FloatingPointToFPReal>().getSize().exponentWidth()
475 : 37 : << ' '
476 : 37 : << n.getConst<FloatingPointToFPReal>().getSize().significandWidth()
477 : 37 : << ")";
478 : 37 : break;
479 : 5 : case Kind::FLOATINGPOINT_TO_FP_FROM_SBV_OP:
480 : 5 : out << "(_ to_fp "
481 : 5 : << n.getConst<FloatingPointToFPSignedBitVector>()
482 : 5 : .getSize()
483 : 5 : .exponentWidth()
484 : 5 : << ' '
485 : 5 : << n.getConst<FloatingPointToFPSignedBitVector>()
486 : 5 : .getSize()
487 : 5 : .significandWidth()
488 : 5 : << ")";
489 : 5 : break;
490 : 3 : case Kind::FLOATINGPOINT_TO_FP_FROM_UBV_OP:
491 : 3 : out << "(_ to_fp_unsigned "
492 : 3 : << n.getConst<FloatingPointToFPUnsignedBitVector>()
493 : 3 : .getSize()
494 : 3 : .exponentWidth()
495 : 3 : << ' '
496 : 3 : << n.getConst<FloatingPointToFPUnsignedBitVector>()
497 : 3 : .getSize()
498 : 3 : .significandWidth()
499 : 3 : << ")";
500 : 3 : break;
501 : 28 : case Kind::FLOATINGPOINT_TO_UBV_OP:
502 : 28 : out << "(_ fp.to_ubv "
503 : 28 : << n.getConst<FloatingPointToUBV>().d_bv_size.d_size << ")";
504 : 28 : break;
505 : 11 : case Kind::FLOATINGPOINT_TO_SBV_OP:
506 : 11 : out << "(_ fp.to_sbv "
507 : 11 : << n.getConst<FloatingPointToSBV>().d_bv_size.d_size << ")";
508 : 11 : break;
509 : 30 : case Kind::FLOATINGPOINT_TO_UBV_TOTAL_OP:
510 : 30 : out << "(_ fp.to_ubv_total "
511 : 30 : << n.getConst<FloatingPointToUBVTotal>().d_bv_size.d_size << ")";
512 : 30 : break;
513 : 12 : case Kind::FLOATINGPOINT_TO_SBV_TOTAL_OP:
514 : 12 : out << "(_ fp.to_sbv_total "
515 : 12 : << n.getConst<FloatingPointToSBVTotal>().d_bv_size.d_size << ")";
516 : 12 : break;
517 : 14 : case Kind::REGEXP_REPEAT_OP:
518 : 14 : out << "(_ re.^ " << n.getConst<RegExpRepeat>().d_repeatAmount << ")";
519 : 14 : break;
520 : 48 : case Kind::REGEXP_LOOP_OP:
521 : 48 : out << "(_ re.loop " << n.getConst<RegExpLoop>().d_loopMinOcc << " "
522 : 48 : << n.getConst<RegExpLoop>().d_loopMaxOcc << ")";
523 : 48 : break;
524 : 225 : case Kind::TUPLE_PROJECT_OP:
525 : : case Kind::TABLE_PROJECT_OP:
526 : : case Kind::TABLE_AGGREGATE_OP:
527 : : case Kind::TABLE_JOIN_OP:
528 : : case Kind::TABLE_GROUP_OP:
529 : : case Kind::RELATION_GROUP_OP:
530 : : case Kind::RELATION_AGGREGATE_OP:
531 : : case Kind::RELATION_PROJECT_OP:
532 : : case Kind::RELATION_TABLE_JOIN_OP:
533 : : {
534 : 225 : ProjectOp op = n.getConst<ProjectOp>();
535 : 225 : const std::vector<uint32_t>& indices = op.getIndices();
536 : 225 : Kind k = NodeManager::operatorToKind(n);
537 [ + + ]: 225 : if (indices.empty())
538 : : {
539 : 32 : out << smtKindString(k);
540 : : }
541 : : else
542 : : {
543 : 193 : out << "(_ " << smtKindString(k);
544 [ + + ]: 759 : for (uint32_t i : indices)
545 : : {
546 : 566 : out << " " << i;
547 : : }
548 : 193 : out << ")";
549 : : }
550 : 225 : }
551 : 225 : break;
552 : 541 : default:
553 : : // fall back on whatever operator<< does on underlying type; we
554 : : // might luck out and be SMT-LIB v2 compliant
555 : 541 : n.constToStream(out);
556 : : }
557 : :
558 : 5401316 : return true;
559 : : }
560 : :
561 : 33951676 : Kind k = n.getKind();
562 [ + + ][ + + ]: 33951676 : if (k == Kind::DATATYPE_TYPE || k == Kind::TUPLE_TYPE
563 [ + + ]: 33923387 : || k == Kind::NULLABLE_TYPE)
564 : : {
565 : 28585 : const DType& dt = n.getNodeManager()->getDTypeFor(n);
566 [ + + ]: 28585 : if (dt.isTuple())
567 : : {
568 : 2340 : unsigned int nargs = dt[0].getNumArgs();
569 [ + + ]: 2340 : if (nargs == 0)
570 : : {
571 : 18 : out << "UnitTuple";
572 : : }
573 : : else
574 : : {
575 : 2322 : out << "(Tuple";
576 [ + + ]: 7644 : for (unsigned int i = 0; i < nargs; i++)
577 : : {
578 : 5322 : out << " ";
579 : 5322 : toStreamType(out, dt[0][i].getRangeType());
580 : : }
581 : 2322 : out << ")";
582 : : }
583 : 2340 : return true;
584 : : }
585 [ + + ]: 26245 : if (dt.isNullable())
586 : : {
587 : 296 : out << "(Nullable " << dt[1][0].getRangeType() << ")";
588 : : }
589 : : else
590 : : {
591 : 25949 : out << cvc5::internal::quoteSymbol(dt.getName());
592 : : }
593 : 26245 : return true;
594 : : }
595 [ + + ]: 33923091 : else if (k == Kind::APPLY_TYPE_ASCRIPTION)
596 : : {
597 : 60 : TypeNode typeAsc = n.getOperator().getConst<AscriptionType>().getType();
598 : : // use type ascription
599 : 60 : out << "(as ";
600 [ - + ]: 60 : toStream(out, n[0], lbind, toDepth < 0 ? toDepth : toDepth - 1);
601 : 60 : out << " " << typeAsc << ")";
602 : 60 : return true;
603 : 60 : }
604 [ + + ]: 33923031 : else if (n.isVar())
605 : : {
606 : 22013759 : bool printed = false;
607 [ + + ]: 22013759 : if (k == Kind::SKOLEM)
608 : : {
609 : 6498 : SkolemManager* sm = nm->getSkolemManager();
610 : : SkolemId id;
611 : 6498 : Node cacheVal;
612 [ + - ]: 6498 : if (sm->isSkolemFunction(n, id, cacheVal))
613 : : {
614 [ + + ]: 6498 : if (id == SkolemId::INTERNAL)
615 : : {
616 [ + + ]: 238 : if (sm->isAbstractValue(n))
617 : : {
618 : : // abstract value
619 : 8 : std::string s = n.getName();
620 : 16 : out << "(as " << cvc5::internal::quoteSymbol(s) << " " << n.getType()
621 : 8 : << ")";
622 : 8 : printed = true;
623 : 8 : }
624 : : }
625 [ + + ]: 6260 : else if (options::ioutils::getPrintSkolemDefinitions(out))
626 : : {
627 : 3707 : toStreamSkolem(
628 : : out, cacheVal, id, /*isApplied=*/false, toDepth, lbind);
629 : 3707 : printed = true;
630 : : }
631 : : }
632 : 6498 : }
633 [ + + ]: 22013759 : if (!printed)
634 : : {
635 : : // variable
636 [ + + ]: 22010044 : if (n.hasName())
637 : : {
638 : 21692071 : std::string s = n.getName();
639 [ + + ]: 21692071 : if (k == Kind::RAW_SYMBOL)
640 : : {
641 : : // raw symbols are never quoted
642 : 3831357 : out << s;
643 : : }
644 : : else
645 : : {
646 : 17860714 : out << cvc5::internal::quoteSymbol(s);
647 : : }
648 : 21692071 : }
649 : : else
650 : : {
651 [ + + ]: 317973 : if (k == Kind::VARIABLE)
652 : : {
653 : 4 : out << "var_";
654 : : }
655 : : else
656 : : {
657 : 317969 : out << k << '_';
658 : : }
659 : 317973 : out << n.getId();
660 : : }
661 : : }
662 : 22013759 : return true;
663 : : }
664 [ + + ]: 11909272 : else if (k == Kind::APPLY_UF)
665 : : {
666 [ + + ]: 1420425 : if (!n.getOperator().isVar())
667 : : {
668 : : // Must print as HO apply instead. This ensures un-beta-reduced function
669 : : // applications can be reparsed.
670 : 4292 : Node hoa = theory::uf::TheoryUfRewriter::getHoApplyForApplyUf(n);
671 : 4292 : toStream(out, hoa, lbind, toDepth);
672 : 4292 : return true;
673 : 4292 : }
674 [ + + ]: 1416133 : else if (n.getOperator().getKind() == Kind::SKOLEM)
675 : : {
676 : 999 : SkolemManager* sm = nm->getSkolemManager();
677 : : SkolemId id;
678 : 999 : Node cacheVal;
679 [ + - ]: 999 : if (sm->isSkolemFunction(n.getOperator(), id, cacheVal))
680 : : {
681 [ + + ]: 999 : if (options::ioutils::getPrintSkolemDefinitions(out))
682 : : {
683 [ + - ]: 267 : if (n.getNumChildren() != 0)
684 : : {
685 : 267 : out << '(';
686 : : }
687 : 267 : toStreamSkolem(out, cacheVal, id, /*isApplied=*/true, toDepth, lbind);
688 : 267 : return false;
689 : : }
690 : : }
691 [ + + ]: 999 : }
692 : : }
693 [ + + ]: 10488847 : else if (k == Kind::CONSTRUCTOR_TYPE)
694 : : {
695 : 60 : Node range = n[n.getNumChildren() - 1];
696 : 60 : toStream(out, range, lbind, toDepth);
697 : 60 : return true;
698 : 60 : }
699 [ + + ][ + + ]: 10488787 : else if (k == Kind::HO_APPLY && options::ioutils::getFlattenHOChains(out))
[ + + ]
700 : : {
701 : 301 : out << "(";
702 : : // collapse "@" chains, i.e.
703 : : //
704 : : // ((a b) c) --> (a b c)
705 : : //
706 : : // (((a b) ((c d) e)) f) --> (a b (c d e) f)
707 : : {
708 : 301 : Node head = n;
709 : 301 : std::vector<Node> args;
710 [ + + ]: 845 : while (head.getKind() == Kind::HO_APPLY)
711 : : {
712 : 544 : args.insert(args.begin(), head[1]);
713 : 544 : head = head[0];
714 : : }
715 : 301 : toStream(out, head, lbind, toDepth);
716 [ + + ]: 845 : for (unsigned i = 0, size = args.size(); i < size; ++i)
717 : : {
718 : 544 : out << " ";
719 : 544 : toStream(out, args[i], lbind, toDepth);
720 : : }
721 : 301 : out << ")";
722 : 301 : }
723 : 301 : return true;
724 : : }
725 [ + + ]: 10488486 : else if (k == Kind::MATCH)
726 : : {
727 : 34 : out << '(' << smtKindString(k) << " ";
728 : 34 : toStream(out, n[0], lbind, toDepth);
729 : 34 : out << " (";
730 [ + + ]: 108 : for (size_t i = 1, nchild = n.getNumChildren(); i < nchild; i++)
731 : : {
732 [ + + ]: 74 : if (i > 1)
733 : : {
734 : 40 : out << " ";
735 : : }
736 : 74 : toStream(out, n[i], lbind, toDepth);
737 : : }
738 : 34 : out << "))";
739 : 34 : return true;
740 : : }
741 [ + + ][ + + ]: 10488452 : else if (k == Kind::MATCH_BIND_CASE || k == Kind::MATCH_CASE)
742 : : {
743 : 76 : out << '(';
744 : : // ignore the binder for MATCH_BIND_CASE
745 [ + + ]: 76 : size_t patIndex = (k == Kind::MATCH_BIND_CASE ? 1 : 0);
746 : : // The pattern should be printed as a pattern (symbol applied to symbols),
747 : : // not as a term. In particular, this means we should not print any
748 : : // type ascriptions (if any).
749 [ + + ]: 76 : if (n[patIndex].getKind() == Kind::APPLY_CONSTRUCTOR)
750 : : {
751 [ + + ]: 72 : if (n[patIndex].getNumChildren() > 0)
752 : : {
753 : 40 : out << "(";
754 : : }
755 : 72 : Node op = n[patIndex].getOperator();
756 : 72 : const DType& dt = DType::datatypeOf(op);
757 : 72 : size_t index = DType::indexOf(op);
758 : 72 : out << dt[index].getConstructor();
759 [ + + ]: 133 : for (const Node& nc : n[patIndex])
760 : : {
761 : 61 : out << " ";
762 : 61 : toStream(out, nc, lbind, toDepth);
763 : 133 : }
764 [ + + ]: 72 : if (n[patIndex].getNumChildren() > 0)
765 : : {
766 : 40 : out << ")";
767 : : }
768 : 72 : }
769 : : else
770 : : {
771 : : // otherwise, a variable, just print
772 [ - + ][ - + ]: 4 : Assert(n[patIndex].isVar());
[ - - ]
773 : 4 : toStream(out, n[patIndex], lbind, toDepth);
774 : : }
775 : 76 : out << " ";
776 : 76 : toStream(out, n[patIndex + 1], lbind, toDepth);
777 : 76 : out << ")";
778 : 76 : return true;
779 : : }
780 [ + + ]: 10488376 : else if (k == Kind::BOUND_VAR_LIST)
781 : : {
782 : 149831 : out << '(';
783 [ + + ]: 434745 : for (TNode::iterator i = n.begin(), iend = n.end(); i != iend;)
784 : : {
785 : 284914 : out << '(';
786 [ - + ]: 284914 : toStream(out, *i, nullptr, toDepth < 0 ? toDepth : toDepth - 1);
787 : 284914 : out << ' ' << (*i).getType() << ')';
788 [ + + ]: 284914 : if (++i != iend)
789 : : {
790 : 135083 : out << ' ';
791 : : }
792 : : }
793 : 149831 : out << ')';
794 : 149831 : return true;
795 : : }
796 [ + + ]: 10338545 : else if (k == Kind::SET_UNIVERSE)
797 : : {
798 : 438 : out << "(as set.universe " << n.getType() << ")";
799 : 438 : return true;
800 : : }
801 [ + + ]: 10338107 : else if (k == Kind::SEP_NIL)
802 : : {
803 : 49 : out << "(as sep.nil " << n.getType() << ")";
804 : 49 : return true;
805 : : }
806 [ + + ][ + + ]: 10338058 : else if (k == Kind::FORALL || k == Kind::EXISTS || k == Kind::LAMBDA
[ + + ]
807 [ + + ]: 10205346 : || k == Kind::WITNESS)
808 : : {
809 : 133164 : out << '(' << smtKindString(k) << " ";
810 : : // do not letify the bound variable list
811 : 133164 : toStream(out, n[0], nullptr, toDepth);
812 : 133164 : out << " ";
813 : 133164 : bool needsPrintAnnot = false;
814 : 133164 : size_t dag = options::ioutils::getDagThresh(out);
815 [ - + ]: 133164 : size_t newDepth = (toDepth < 0 ? toDepth : toDepth - 1);
816 : 133164 : std::stringstream annot;
817 [ + + ]: 133164 : if (n.getNumChildren() == 3)
818 : : {
819 [ + + ]: 3726 : for (const Node& nc : n[2])
820 : : {
821 : 1910 : Kind nck = nc.getKind();
822 [ + + ]: 1910 : if (nck == Kind::INST_PATTERN)
823 : : {
824 : 1286 : needsPrintAnnot = true;
825 : 1286 : annot << " :pattern (";
826 [ + + ]: 2662 : for (size_t i = 0, nchild = nc.getNumChildren(); i < nchild; i++)
827 : : {
828 [ + + ]: 1376 : if (i > 0)
829 : : {
830 : 90 : annot << " ";
831 : : }
832 : 1376 : toStream(annot, nc[i], newDepth, dag);
833 : : }
834 : 1286 : annot << ")";
835 : : }
836 [ + + ]: 624 : else if (nck == Kind::INST_NO_PATTERN)
837 : : {
838 : 2 : needsPrintAnnot = true;
839 : 2 : annot << " :no-pattern ";
840 : 2 : toStream(annot, nc[0], newDepth, dag);
841 : : }
842 [ + + ][ + + ]: 622 : else if (nck == Kind::INST_POOL || nck == Kind::INST_ADD_TO_POOL
843 [ + + ]: 612 : || nck == Kind::SKOLEM_ADD_TO_POOL)
844 : : {
845 : 12 : needsPrintAnnot = true;
846 [ + + ][ + - ]: 12 : switch (nck)
847 : : {
848 : 6 : case Kind::INST_POOL: annot << " :pool"; break;
849 : 4 : case Kind::INST_ADD_TO_POOL: annot << " :inst-add-to-pool"; break;
850 : 2 : case Kind::SKOLEM_ADD_TO_POOL:
851 : 2 : annot << " :skolem-add-to-pool";
852 : 2 : break;
853 : 0 : default: break;
854 : : }
855 : 12 : annot << " (";
856 [ + + ]: 31 : for (size_t i = 0, nchild = nc.getNumChildren(); i < nchild; i++)
857 : : {
858 [ + + ]: 19 : if (i > 0)
859 : : {
860 : 7 : annot << " ";
861 : : }
862 : 19 : toStream(annot, nc[i], newDepth, dag);
863 : : }
864 : 12 : annot << ")";
865 : 12 : }
866 [ + - ]: 610 : else if (nck == Kind::INST_ATTRIBUTE)
867 : : {
868 : : // notice that INST_ATTRIBUTES either have an "internal" form,
869 : : // where the argument is a variable with an internal attribute set
870 : : // on it, or an "external" form where it is of the form
871 : : // (INST_ATTRIBUTE "keyword" [nodeValues]). We print the latter
872 : : // here only.
873 [ + + ]: 610 : if (nc[0].getKind() == Kind::CONST_STRING)
874 : : {
875 : 553 : needsPrintAnnot = true;
876 : : // print out as string to avoid quotes
877 : 553 : annot << " :" << nc[0].getConst<String>().toString();
878 [ + + ]: 1106 : for (size_t j = 1, nchild = nc.getNumChildren(); j < nchild; j++)
879 : : {
880 : 553 : annot << " ";
881 : 553 : toStream(annot, nc[j], newDepth, dag);
882 : : }
883 : : }
884 : : }
885 : 3726 : }
886 : : }
887 : : // Use a fresh let binder, since using existing let symbols may violate
888 : : // scoping issues for let-bound variables, see explanation in let_binding.h.
889 [ + + ]: 133164 : if (needsPrintAnnot)
890 : : {
891 : 1759 : out << "(! ";
892 : 1759 : annot << ")";
893 : : }
894 : 133164 : toStream(out, n[1], newDepth, dag);
895 : 133164 : out << annot.str() << ")";
896 : 133164 : return true;
897 : 133164 : }
898 : :
899 : 11620760 : bool stillNeedToPrintParams = true;
900 : 11620760 : bool printed = true;
901 : : // operator
902 [ + + ]: 11620760 : if (n.getNumChildren() != 0)
903 : : {
904 : 11613588 : out << '(';
905 : : }
906 [ + - ][ - + ]: 11620760 : switch (k)
[ + + ][ + + ]
[ + + ]
907 : : {
908 : 4 : case Kind::REAL_ALGEBRAIC_NUMBER:
909 : : {
910 : : const RealAlgebraicNumber& ran =
911 : 4 : n.getOperator().getConst<RealAlgebraicNumber>();
912 : 4 : out << "(_ real_algebraic_number " << ran << ")";
913 : 4 : stillNeedToPrintParams = false;
914 : 4 : break;
915 : : }
916 : 0 : case Kind::INDEXED_ROOT_PREDICATE_OP:
917 : : {
918 : 0 : const IndexedRootPredicate& irp = n.getConst<IndexedRootPredicate>();
919 : 0 : out << "(_ root_predicate " << irp.d_index << ")";
920 : 0 : stillNeedToPrintParams = false;
921 : 0 : break;
922 : : }
923 : 0 : case Kind::BITVECTOR_BIT:
924 : 0 : out << "(_ @bit " << n.getOperator().getConst<BitVectorBit>().d_bitIndex
925 : 0 : << ")";
926 : 0 : stillNeedToPrintParams = false;
927 : 0 : break;
928 : 8788 : case Kind::APPLY_CONSTRUCTOR:
929 : : {
930 : 8788 : const DType& dt = DType::datatypeOf(n.getOperator());
931 [ + + ]: 8788 : if (dt.isTuple())
932 : : {
933 : 2649 : stillNeedToPrintParams = false;
934 [ + + ]: 2649 : if (dt[0].getNumArgs() == 0)
935 : : {
936 : 16 : out << "tuple.unit";
937 : : }
938 : : else
939 : : {
940 : 2633 : out << "tuple";
941 : : }
942 : : }
943 [ + + ]: 8788 : if (dt.isNullable())
944 : : {
945 : 156 : stillNeedToPrintParams = false;
946 [ + + ]: 156 : if (n.getNumChildren() == 0)
947 : : {
948 : 94 : out << "(as nullable.null " << n.getType() << ")";
949 : : }
950 : : else
951 : : {
952 : 62 : out << "nullable.some";
953 : : }
954 : : }
955 : 8788 : break;
956 : : }
957 : 29835 : case Kind::APPLY_SELECTOR:
958 : : {
959 : 29835 : Node op = n.getOperator();
960 : 29835 : const DType& dt = DType::datatypeOf(op);
961 [ + + ]: 29835 : if (dt.isTuple())
962 : : {
963 : 492 : stillNeedToPrintParams = false;
964 : 492 : out << "(_ tuple.select " << DType::indexOf(op) << ")";
965 : : }
966 [ + + ]: 29343 : else if (dt.isNullable())
967 : : {
968 : 76 : stillNeedToPrintParams = false;
969 : 76 : out << "nullable.val";
970 : : }
971 : 29835 : }
972 : 29835 : break;
973 : 1059 : case Kind::APPLY_TESTER:
974 : : {
975 : 1059 : Node op = n.getOperator();
976 : 1059 : size_t cindex = DType::indexOf(op);
977 : 1059 : const DType& dt = DType::datatypeOf(op);
978 [ + + ]: 1059 : if (dt.isNullable())
979 : : {
980 : 19 : stillNeedToPrintParams = false;
981 [ + + ]: 19 : if (cindex == 0)
982 : : {
983 : 11 : out << "nullable.is_null";
984 : : }
985 : : else
986 : : {
987 : 8 : out << "nullable.is_some";
988 : : }
989 : : }
990 : : else
991 : : {
992 : 1040 : stillNeedToPrintParams = false;
993 : 1040 : out << "(_ is ";
994 [ - + ]: 2080 : toStream(out,
995 : 2080 : dt[cindex].getConstructor(),
996 : : lbind,
997 : : toDepth < 0 ? toDepth : toDepth - 1);
998 : 1040 : out << ")";
999 : : }
1000 : 1059 : }
1001 : 1059 : break;
1002 : 52 : case Kind::APPLY_UPDATER:
1003 : : {
1004 : 52 : stillNeedToPrintParams = false;
1005 : 52 : Node op = n.getOperator();
1006 : 52 : size_t index = DType::indexOf(op);
1007 : 52 : const DType& dt = DType::datatypeOf(op);
1008 : 52 : size_t cindex = DType::cindexOf(op);
1009 [ + + ]: 52 : if (dt.isTuple())
1010 : : {
1011 : 10 : out << "(_ tuple.update " << index << ")";
1012 : : }
1013 : : else
1014 : : {
1015 : 42 : out << "(_ update ";
1016 [ - + ]: 84 : toStream(out,
1017 : 84 : dt[cindex][index].getSelector(),
1018 : : lbind,
1019 : : toDepth < 0 ? toDepth : toDepth - 1);
1020 : 42 : out << ")";
1021 : : }
1022 : 52 : }
1023 : 52 : break;
1024 : : // kinds that don't print their operator
1025 : 2653642 : case Kind::SEXPR:
1026 : : case Kind::INSTANTIATED_SORT_TYPE:
1027 : : case Kind::PARAMETRIC_DATATYPE:
1028 : : case Kind::INST_PATTERN:
1029 : : case Kind::INST_NO_PATTERN:
1030 : 2653642 : case Kind::INST_PATTERN_LIST: printed = false; break;
1031 : 53581 : case Kind::STRING_CONCAT:
1032 : : case Kind::STRING_LENGTH:
1033 : : case Kind::STRING_SUBSTR:
1034 : : case Kind::STRING_UPDATE:
1035 : : case Kind::STRING_CHARAT:
1036 : : case Kind::STRING_CONTAINS:
1037 : : case Kind::STRING_INDEXOF:
1038 : : case Kind::STRING_REPLACE:
1039 : : case Kind::STRING_REPLACE_ALL:
1040 : : case Kind::STRING_REV:
1041 : : case Kind::STRING_PREFIX:
1042 : : case Kind::STRING_SUFFIX:
1043 : : // maybe print seq. instead of str.
1044 : 53581 : out << smtKindStringOf(n);
1045 : 53581 : break;
1046 : 8873799 : default:
1047 : : // by default, print the kind using the smtKindString utility
1048 [ + + ]: 8873799 : if (n.getMetaKind() != kind::metakind::PARAMETERIZED)
1049 : : {
1050 : 7422886 : out << smtKindString(k);
1051 : : }
1052 : 8873799 : break;
1053 : : }
1054 : 11620760 : if (n.getMetaKind() == kind::metakind::PARAMETERIZED
1055 [ + + ][ + + ]: 11620760 : && stillNeedToPrintParams)
[ + + ]
1056 : : {
1057 [ + - ]: 1486163 : if (toDepth != 0)
1058 : : {
1059 [ - + ]: 2972326 : toStream(
1060 : 2972326 : out, n.getOperator(), lbind, toDepth < 0 ? toDepth : toDepth - 1);
1061 : : }
1062 : : else
1063 : : {
1064 : 0 : out << "(...)";
1065 : : }
1066 : : }
1067 : : // finished if we have no children
1068 [ + + ]: 11620760 : if (n.getNumChildren() == 0)
1069 : : {
1070 : 7172 : return true;
1071 : : }
1072 [ + + ]: 11613588 : if (printed)
1073 : : {
1074 : : // if printed anything, now add a space
1075 : 8959946 : out << ' ';
1076 : : }
1077 : 11613588 : return false;
1078 : : }
1079 : :
1080 : 17341307 : void Smt2Printer::toStream(std::ostream& out,
1081 : : TNode n,
1082 : : const LetBinding* lbind,
1083 : : int toDepth,
1084 : : bool lbindTop) const
1085 : : {
1086 : 17341307 : std::vector<std::tuple<TNode, size_t, int>> visit;
1087 : 17341307 : TNode cur;
1088 : : size_t curChild;
1089 : : int cdepth;
1090 : 17341307 : visit.emplace_back(n, 0, toDepth);
1091 : : do
1092 : : {
1093 : 79438297 : cur = std::get<0>(visit.back());
1094 : 79438297 : curChild = std::get<1>(visit.back());
1095 : 79438297 : cdepth = std::get<2>(visit.back());
1096 [ + + ]: 79438297 : if (curChild == 0)
1097 : : {
1098 [ + + ]: 48389802 : if (lbind != nullptr)
1099 : : {
1100 [ + + ]: 26255500 : if (lbindTop)
1101 : : {
1102 : : // see if its letified
1103 : 24964530 : uint32_t lid = lbind->getId(cur);
1104 [ + + ]: 24964530 : if (lid != 0)
1105 : : {
1106 : 9036796 : out << lbind->getPrefix() << lid;
1107 : 9036796 : visit.pop_back();
1108 : 9036796 : continue;
1109 : : }
1110 : : }
1111 : : else
1112 : : {
1113 : 1290970 : lbindTop = true;
1114 : : }
1115 : : }
1116 : : // print the operator
1117 : : // if printed as standalone, we are done
1118 [ + + ]: 39353006 : if (toStreamBase(out, cur, lbind, cdepth))
1119 : : {
1120 : 27739151 : visit.pop_back();
1121 : 27739151 : continue;
1122 : : }
1123 [ - + ]: 11613855 : else if (cdepth == 0)
1124 : : {
1125 : 0 : visit.pop_back();
1126 : 0 : out << "(...)";
1127 [ - - ]: 0 : if (cur.getNumChildren() > 0)
1128 : : {
1129 : 0 : out << ')';
1130 : : }
1131 : 0 : continue;
1132 : : }
1133 : : }
1134 [ + + ]: 42662350 : if (curChild < cur.getNumChildren())
1135 : : {
1136 : 31048495 : std::get<1>(visit.back())++;
1137 : : // toStreamBase akready adds space, skip adding space before first child
1138 [ + + ]: 31048495 : if (curChild > 0)
1139 : : {
1140 : 19434640 : out << ' ';
1141 : : }
1142 [ - + ]: 31048495 : visit.emplace_back(cur[curChild], 0, cdepth < 0 ? cdepth : cdepth - 1);
1143 : : }
1144 : : else
1145 : : {
1146 [ - + ][ - + ]: 11613855 : Assert(cur.getNumChildren() > 0);
[ - - ]
1147 : 11613855 : out << ')';
1148 : 11613855 : visit.pop_back();
1149 : : }
1150 [ + + ]: 79438297 : } while (!visit.empty());
1151 : 17341307 : }
1152 : :
1153 : 8505932 : std::string Smt2Printer::smtKindString(Kind k)
1154 : : {
1155 [ + + ][ + - ]: 8505932 : switch(k) {
[ - + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ - - ]
[ - + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ - - ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + - ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + - ][ + + ]
[ + + ][ + + ]
[ - + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ - + ][ + + ]
[ + - ][ - - ]
[ - + ][ + + ]
[ + + ][ + + ]
[ + - ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ - + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ - + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + ]
1156 : : // builtin theory
1157 : 10665 : case Kind::FUNCTION_TYPE: return "->";
1158 : 2421411 : case Kind::EQUAL: return "=";
1159 : 25846 : case Kind::DISTINCT: return "distinct";
1160 : 0 : case Kind::SEXPR: break;
1161 : :
1162 : 0 : case Kind::TYPE_OF: return "@type_of";
1163 : :
1164 : : // bool theory
1165 : 1102269 : case Kind::NOT: return "not";
1166 : 851298 : case Kind::AND: return "and";
1167 : 169483 : case Kind::IMPLIES: return "=>";
1168 : 1441239 : case Kind::OR: return "or";
1169 : 36117 : case Kind::XOR: return "xor";
1170 : 241602 : case Kind::ITE: return "ite";
1171 : :
1172 : : // uf theory
1173 : 408 : case Kind::APPLY_UF: break;
1174 : :
1175 : 9139 : case Kind::LAMBDA: return "lambda";
1176 : 35 : case Kind::MATCH: return "match";
1177 : 452 : case Kind::WITNESS: return "witness";
1178 : :
1179 : : // arith theory
1180 : 367574 : case Kind::ADD: return "+";
1181 : 297019 : case Kind::MULT:
1182 : 297019 : case Kind::NONLINEAR_MULT: return "*";
1183 : 83 : case Kind::IAND: return "iand";
1184 : 109 : case Kind::PIAND: return "piand";
1185 : 394 : case Kind::POW2: return "int.pow2";
1186 : 585 : case Kind::EXPONENTIAL: return "exp";
1187 : 627 : case Kind::SINE: return "sin";
1188 : 102 : case Kind::COSINE: return "cos";
1189 : 15 : case Kind::TANGENT: return "tan";
1190 : 8 : case Kind::COSECANT: return "csc";
1191 : 16 : case Kind::SECANT: return "sec";
1192 : 9 : case Kind::COTANGENT: return "cot";
1193 : 34 : case Kind::ARCSINE: return "arcsin";
1194 : 33 : case Kind::ARCCOSINE: return "arccos";
1195 : 20 : case Kind::ARCTANGENT: return "arctan";
1196 : 0 : case Kind::ARCCOSECANT: return "arccsc";
1197 : 0 : case Kind::ARCSECANT: return "arcsec";
1198 : 0 : case Kind::ARCCOTANGENT: return "arccot";
1199 : 1637 : case Kind::PI: return "real.pi";
1200 : 60 : case Kind::SQRT: return "sqrt";
1201 : 68670 : case Kind::SUB: return "-";
1202 : 34430 : case Kind::NEG: return "-";
1203 : 50551 : case Kind::LT: return "<";
1204 : 87487 : case Kind::LEQ: return "<=";
1205 : 17167 : case Kind::GT: return ">";
1206 : 257455 : case Kind::GEQ: return ">=";
1207 : 3353 : case Kind::DIVISION: return "/";
1208 : 363 : case Kind::DIVISION_TOTAL: return "/_total";
1209 : 2597 : case Kind::INTS_DIVISION: return "div";
1210 : 1051 : case Kind::INTS_DIVISION_TOTAL: return "div_total";
1211 : 2816 : case Kind::INTS_MODULUS: return "mod";
1212 : 891 : case Kind::INTS_MODULUS_TOTAL: return "mod_total";
1213 : 67 : case Kind::INTS_LOG2: return "int.log2";
1214 : 35 : case Kind::INTS_ISPOW2: return "int.ispow2";
1215 : 1858 : case Kind::ABS: return "abs";
1216 : 196 : case Kind::IS_INTEGER: return "is_int";
1217 : 526 : case Kind::TO_INTEGER: return "to_int";
1218 : 8207 : case Kind::TO_REAL: return "to_real";
1219 : 39 : case Kind::POW: return "^";
1220 : 6 : case Kind::DIVISIBLE: return "divisible";
1221 : :
1222 : : // arrays theory
1223 : 17493 : case Kind::SELECT: return "select";
1224 : 5413 : case Kind::STORE: return "store";
1225 : 15280 : case Kind::ARRAY_TYPE: return "Array";
1226 : 23 : case Kind::EQ_RANGE: return "eqrange";
1227 : :
1228 : : // ff theory
1229 : 1154 : case Kind::FINITE_FIELD_ADD: return "ff.add";
1230 : 59 : case Kind::FINITE_FIELD_BITSUM: return "ff.bitsum";
1231 : 1413 : case Kind::FINITE_FIELD_MULT: return "ff.mul";
1232 : 183 : case Kind::FINITE_FIELD_NEG: return "ff.neg";
1233 : :
1234 : : // bv theory
1235 : 23244 : case Kind::BITVECTOR_CONCAT: return "concat";
1236 : 9554 : case Kind::BITVECTOR_AND: return "bvand";
1237 : 5333 : case Kind::BITVECTOR_OR: return "bvor";
1238 : 3909 : case Kind::BITVECTOR_XOR: return "bvxor";
1239 : 5059 : case Kind::BITVECTOR_NOT: return "bvnot";
1240 : 478 : case Kind::BITVECTOR_NAND: return "bvnand";
1241 : 619 : case Kind::BITVECTOR_NOR: return "bvnor";
1242 : 719 : case Kind::BITVECTOR_XNOR: return "bvxnor";
1243 : 3530 : case Kind::BITVECTOR_COMP: return "bvcomp";
1244 : 11445 : case Kind::BITVECTOR_MULT: return "bvmul";
1245 : 17687 : case Kind::BITVECTOR_ADD: return "bvadd";
1246 : 6212 : case Kind::BITVECTOR_SUB: return "bvsub";
1247 : 3481 : case Kind::BITVECTOR_NEG: return "bvneg";
1248 : 657 : case Kind::BITVECTOR_UDIV: return "bvudiv";
1249 : 477 : case Kind::BITVECTOR_UREM: return "bvurem";
1250 : 228 : case Kind::BITVECTOR_SDIV: return "bvsdiv";
1251 : 121 : case Kind::BITVECTOR_SREM: return "bvsrem";
1252 : 98 : case Kind::BITVECTOR_SMOD: return "bvsmod";
1253 : 1792 : case Kind::BITVECTOR_SHL: return "bvshl";
1254 : 1815 : case Kind::BITVECTOR_LSHR: return "bvlshr";
1255 : 1549 : case Kind::BITVECTOR_ASHR: return "bvashr";
1256 : 12041 : case Kind::BITVECTOR_ULT: return "bvult";
1257 : 4272 : case Kind::BITVECTOR_ULE: return "bvule";
1258 : 4042 : case Kind::BITVECTOR_UGT: return "bvugt";
1259 : 3872 : case Kind::BITVECTOR_UGE: return "bvuge";
1260 : 14594 : case Kind::BITVECTOR_SLT: return "bvslt";
1261 : 4415 : case Kind::BITVECTOR_SLE: return "bvsle";
1262 : 4415 : case Kind::BITVECTOR_SGT: return "bvsgt";
1263 : 4537 : case Kind::BITVECTOR_SGE: return "bvsge";
1264 : 7 : case Kind::BITVECTOR_NEGO: return "bvnego";
1265 : 18 : case Kind::BITVECTOR_UADDO: return "bvuaddo";
1266 : 22 : case Kind::BITVECTOR_SADDO: return "bvsaddo";
1267 : 14 : case Kind::BITVECTOR_UMULO: return "bvumulo";
1268 : 27 : case Kind::BITVECTOR_SMULO: return "bvsmulo";
1269 : 18 : case Kind::BITVECTOR_USUBO: return "bvusubo";
1270 : 26 : case Kind::BITVECTOR_SSUBO: return "bvssubo";
1271 : 18 : case Kind::BITVECTOR_SDIVO: return "bvsdivo";
1272 : 2509 : case Kind::BITVECTOR_UBV_TO_INT: return "ubv_to_int";
1273 : 19 : case Kind::BITVECTOR_SBV_TO_INT: return "sbv_to_int";
1274 : 16 : case Kind::BITVECTOR_REDOR: return "bvredor";
1275 : 16 : case Kind::BITVECTOR_REDAND: return "bvredand";
1276 : :
1277 : 8679 : case Kind::BITVECTOR_EXTRACT: return "extract";
1278 : 352 : case Kind::BITVECTOR_REPEAT: return "repeat";
1279 : 4793 : case Kind::BITVECTOR_ZERO_EXTEND: return "zero_extend";
1280 : 6767 : case Kind::BITVECTOR_SIGN_EXTEND: return "sign_extend";
1281 : 246 : case Kind::BITVECTOR_ROTATE_LEFT: return "rotate_left";
1282 : 250 : case Kind::BITVECTOR_ROTATE_RIGHT: return "rotate_right";
1283 : 98 : case Kind::INT_TO_BITVECTOR: return "int_to_bv";
1284 : 267 : case Kind::BITVECTOR_ITE: return "bvite";
1285 : 4 : case Kind::BITVECTOR_ULTBV: return "bvultbv";
1286 : 34 : case Kind::BITVECTOR_SLTBV: return "bvsltbv";
1287 : :
1288 : 4428 : case Kind::BITVECTOR_FROM_BOOLS: return "@from_bools";
1289 : 4193 : case Kind::BITVECTOR_BIT: return "@bit";
1290 : 694 : case Kind::BITVECTOR_SIZE: return "@bvsize";
1291 : 676 : case Kind::CONST_BITVECTOR_SYMBOLIC: return "@bv";
1292 : :
1293 : : // datatypes theory
1294 : 926 : case Kind::APPLY_TESTER: return "is";
1295 : 29 : case Kind::APPLY_UPDATER: return "update";
1296 : 0 : case Kind::TUPLE_TYPE: return "Tuple";
1297 : 0 : case Kind::NULLABLE_TYPE: return "Nullable";
1298 : 27 : case Kind::TUPLE_PROJECT: return "tuple.project";
1299 : 26 : case Kind::NULLABLE_LIFT: return "nullable.lift";
1300 : :
1301 : : // set theory
1302 : 33 : case Kind::SET_EMPTY: return "set.empty";
1303 : 15 : case Kind::SET_UNIVERSE: return "set.universe";
1304 : 1639 : case Kind::SET_UNION: return "set.union";
1305 : 689 : case Kind::SET_INTER: return "set.inter";
1306 : 617 : case Kind::SET_MINUS: return "set.minus";
1307 : 174 : case Kind::SET_SUBSET: return "set.subset";
1308 : 6532 : case Kind::SET_MEMBER: return "set.member";
1309 : 17366 : case Kind::SET_TYPE: return "Set";
1310 : 1778 : case Kind::SET_SINGLETON: return "set.singleton";
1311 : 87 : case Kind::SET_INSERT: return "set.insert";
1312 : 107 : case Kind::SET_COMPLEMENT: return "set.complement";
1313 : 1711 : case Kind::SET_CARD: return "set.card";
1314 : 47 : case Kind::SET_COMPREHENSION: return "set.comprehension";
1315 : 261 : case Kind::SET_CHOOSE: return "set.choose";
1316 : 20 : case Kind::SET_IS_EMPTY: return "set.is_empty";
1317 : 126 : case Kind::SET_IS_SINGLETON: return "set.is_singleton";
1318 : 82 : case Kind::SET_MAP: return "set.map";
1319 : 229 : case Kind::SET_FILTER: return "set.filter";
1320 : 24 : case Kind::SET_ALL: return "set.all";
1321 : 15 : case Kind::SET_SOME: return "set.some";
1322 : 28 : case Kind::SET_FOLD: return "set.fold";
1323 : 534 : case Kind::RELATION_JOIN: return "rel.join";
1324 : 7 : case Kind::RELATION_TABLE_JOIN: return "rel.table_join";
1325 : 98 : case Kind::RELATION_PRODUCT: return "rel.product";
1326 : 160 : case Kind::RELATION_TRANSPOSE: return "rel.transpose";
1327 : 97 : case Kind::RELATION_TCLOSURE: return "rel.tclosure";
1328 : 13 : case Kind::RELATION_IDEN: return "rel.iden";
1329 : 102 : case Kind::RELATION_JOIN_IMAGE: return "rel.join_image";
1330 : 52 : case Kind::RELATION_GROUP: return "rel.group";
1331 : 3 : case Kind::RELATION_AGGREGATE: return "rel.aggr";
1332 : 28 : case Kind::RELATION_PROJECT: return "rel.project";
1333 : 0 : case Kind::SET_EMPTY_OF_TYPE: return "@set.empty_of_type";
1334 : :
1335 : : // bag theory
1336 : 432 : case Kind::BAG_TYPE: return "Bag";
1337 : 2 : case Kind::BAG_EMPTY: return "bag.empty";
1338 : 56 : case Kind::BAG_UNION_MAX: return "bag.union_max";
1339 : 398 : case Kind::BAG_UNION_DISJOINT: return "bag.union_disjoint";
1340 : 47 : case Kind::BAG_INTER_MIN: return "bag.inter_min";
1341 : 34 : case Kind::BAG_DIFFERENCE_SUBTRACT: return "bag.difference_subtract";
1342 : 60 : case Kind::BAG_DIFFERENCE_REMOVE: return "bag.difference_remove";
1343 : 19 : case Kind::BAG_SUBBAG: return "bag.subbag";
1344 : 433 : case Kind::BAG_COUNT: return "bag.count";
1345 : 77 : case Kind::BAG_MEMBER: return "bag.member";
1346 : 22 : case Kind::BAG_SETOF: return "bag.setof";
1347 : 656 : case Kind::BAG_MAKE: return "bag";
1348 : 92 : case Kind::BAG_CARD: return "bag.card";
1349 : 37 : case Kind::BAG_CHOOSE: return "bag.choose";
1350 : 152 : case Kind::BAG_MAP: return "bag.map";
1351 : 116 : case Kind::BAG_FILTER: return "bag.filter";
1352 : 12 : case Kind::BAG_ALL: return "bag.all";
1353 : 3 : case Kind::BAG_SOME: return "bag.some";
1354 : 29 : case Kind::BAG_FOLD: return "bag.fold";
1355 : 6 : case Kind::BAG_PARTITION: return "bag.partition";
1356 : 32 : case Kind::TABLE_PRODUCT: return "table.product";
1357 : 55 : case Kind::TABLE_PROJECT: return "table.project";
1358 : 3 : case Kind::TABLE_AGGREGATE: return "table.aggr";
1359 : 16 : case Kind::TABLE_JOIN: return "table.join";
1360 : 41 : case Kind::TABLE_GROUP:
1361 : 41 : return "table.group";
1362 : :
1363 : : // fp theory
1364 : 18 : case Kind::FLOATINGPOINT_FP: return "fp";
1365 : 9 : case Kind::FLOATINGPOINT_EQ: return "fp.eq";
1366 : 38 : case Kind::FLOATINGPOINT_ABS: return "fp.abs";
1367 : 64 : case Kind::FLOATINGPOINT_NEG: return "fp.neg";
1368 : 84 : case Kind::FLOATINGPOINT_ADD: return "fp.add";
1369 : 21 : case Kind::FLOATINGPOINT_SUB: return "fp.sub";
1370 : 49 : case Kind::FLOATINGPOINT_MULT: return "fp.mul";
1371 : 10 : case Kind::FLOATINGPOINT_DIV: return "fp.div";
1372 : 0 : case Kind::FLOATINGPOINT_FMA: return "fp.fma";
1373 : 10 : case Kind::FLOATINGPOINT_SQRT: return "fp.sqrt";
1374 : 10 : case Kind::FLOATINGPOINT_REM: return "fp.rem";
1375 : 10 : case Kind::FLOATINGPOINT_RTI: return "fp.roundToIntegral";
1376 : 15 : case Kind::FLOATINGPOINT_MIN: return "fp.min";
1377 : 5 : case Kind::FLOATINGPOINT_MAX: return "fp.max";
1378 : 18 : case Kind::FLOATINGPOINT_MIN_TOTAL: return "fp.min_total";
1379 : 0 : case Kind::FLOATINGPOINT_MAX_TOTAL: return "fp.max_total";
1380 : :
1381 : 189 : case Kind::FLOATINGPOINT_LEQ: return "fp.leq";
1382 : 66 : case Kind::FLOATINGPOINT_LT: return "fp.lt";
1383 : 31 : case Kind::FLOATINGPOINT_GEQ: return "fp.geq";
1384 : 6 : case Kind::FLOATINGPOINT_GT: return "fp.gt";
1385 : :
1386 : 6 : case Kind::FLOATINGPOINT_IS_NORMAL: return "fp.isNormal";
1387 : 11 : case Kind::FLOATINGPOINT_IS_SUBNORMAL: return "fp.isSubnormal";
1388 : 17 : case Kind::FLOATINGPOINT_IS_ZERO: return "fp.isZero";
1389 : 7 : case Kind::FLOATINGPOINT_IS_INF: return "fp.isInfinite";
1390 : 55 : case Kind::FLOATINGPOINT_IS_NAN: return "fp.isNaN";
1391 : 29 : case Kind::FLOATINGPOINT_IS_NEG: return "fp.isNegative";
1392 : 8 : case Kind::FLOATINGPOINT_IS_POS: return "fp.isPositive";
1393 : :
1394 : 0 : case Kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV: return "to_fp";
1395 : 2 : case Kind::FLOATINGPOINT_TO_FP_FROM_FP: return "to_fp";
1396 : 5 : case Kind::FLOATINGPOINT_TO_FP_FROM_REAL: return "to_fp";
1397 : 8 : case Kind::FLOATINGPOINT_TO_FP_FROM_SBV: return "to_fp";
1398 : 43 : case Kind::FLOATINGPOINT_TO_FP_FROM_UBV: return "to_fp_unsigned";
1399 : 0 : case Kind::FLOATINGPOINT_TO_UBV: return "fp.to_ubv";
1400 : 0 : case Kind::FLOATINGPOINT_TO_UBV_TOTAL: return "fp.to_ubv_total";
1401 : 0 : case Kind::FLOATINGPOINT_TO_SBV: return "fp.to_sbv";
1402 : 0 : case Kind::FLOATINGPOINT_TO_SBV_TOTAL: return "fp.to_sbv_total";
1403 : 18 : case Kind::FLOATINGPOINT_TO_REAL: return "fp.to_real";
1404 : 18 : case Kind::FLOATINGPOINT_TO_REAL_TOTAL: return "fp.to_real_total";
1405 : :
1406 : 10 : case Kind::FLOATINGPOINT_COMPONENT_NAN: return "@fp.NAN";
1407 : 7 : case Kind::FLOATINGPOINT_COMPONENT_INF: return "@fp.INF";
1408 : 7 : case Kind::FLOATINGPOINT_COMPONENT_ZERO: return "@fp.ZERO";
1409 : 6 : case Kind::FLOATINGPOINT_COMPONENT_SIGN: return "@fp.SIGN";
1410 : 7 : case Kind::FLOATINGPOINT_COMPONENT_EXPONENT: return "@fp.EXPONENT";
1411 : 7 : case Kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND: return "@fp.SIGNIFICAND";
1412 : 0 : case Kind::ROUNDINGMODE_BITBLAST: return "@fp.RMBITBLAST";
1413 : :
1414 : : // string theory
1415 : 32168 : case Kind::STRING_CONCAT: return "str.++";
1416 : 15465 : case Kind::STRING_LENGTH: return "str.len";
1417 : 9664 : case Kind::STRING_SUBSTR: return "str.substr";
1418 : 164 : case Kind::STRING_UPDATE: return "str.update";
1419 : 3137 : case Kind::STRING_CONTAINS: return "str.contains";
1420 : 235 : case Kind::STRING_CHARAT: return "str.at";
1421 : 1323 : case Kind::STRING_INDEXOF: return "str.indexof";
1422 : 159 : case Kind::STRING_INDEXOF_RE: return "str.indexof_re";
1423 : 2212 : case Kind::STRING_REPLACE: return "str.replace";
1424 : 273 : case Kind::STRING_REPLACE_ALL: return "str.replace_all";
1425 : 109 : case Kind::STRING_REPLACE_RE: return "str.replace_re";
1426 : 85 : case Kind::STRING_REPLACE_RE_ALL: return "str.replace_re_all";
1427 : 93 : case Kind::STRING_TO_LOWER: return "str.to_lower";
1428 : 71 : case Kind::STRING_TO_UPPER: return "str.to_upper";
1429 : 146 : case Kind::STRING_REV: return "str.rev";
1430 : 276 : case Kind::STRING_PREFIX: return "str.prefixof";
1431 : 118 : case Kind::STRING_SUFFIX: return "str.suffixof";
1432 : 238 : case Kind::STRING_LEQ: return "str.<=";
1433 : 68 : case Kind::STRING_LT: return "str.<";
1434 : 129 : case Kind::STRING_FROM_CODE: return "str.from_code";
1435 : 819 : case Kind::STRING_TO_CODE: return "str.to_code";
1436 : 41 : case Kind::STRING_IS_DIGIT: return "str.is_digit";
1437 : 260 : case Kind::STRING_ITOS: return "str.from_int";
1438 : 344 : case Kind::STRING_STOI: return "str.to_int";
1439 : 3051 : case Kind::STRING_IN_REGEXP: return "str.in_re";
1440 : 2805 : case Kind::STRING_TO_REGEXP: return "str.to_re";
1441 : 0 : case Kind::STRING_UNIT: return "str.unit";
1442 : 417 : case Kind::REGEXP_NONE: return "re.none";
1443 : 186 : case Kind::REGEXP_ALL: return "re.all";
1444 : 1409 : case Kind::REGEXP_ALLCHAR: return "re.allchar";
1445 : 2458 : case Kind::REGEXP_CONCAT: return "re.++";
1446 : 976 : case Kind::REGEXP_UNION: return "re.union";
1447 : 211 : case Kind::REGEXP_INTER: return "re.inter";
1448 : 1570 : case Kind::REGEXP_STAR: return "re.*";
1449 : 189 : case Kind::REGEXP_PLUS: return "re.+";
1450 : 74 : case Kind::REGEXP_OPT: return "re.opt";
1451 : 733 : case Kind::REGEXP_RANGE: return "re.range";
1452 : 6 : case Kind::REGEXP_REPEAT: return "re.^";
1453 : 30 : case Kind::REGEXP_LOOP: return "re.loop";
1454 : 201 : case Kind::REGEXP_COMPLEMENT: return "re.comp";
1455 : 74 : case Kind::REGEXP_DIFF: return "re.diff";
1456 : 47883 : case Kind::SEQUENCE_TYPE: return "Seq";
1457 : 1126 : case Kind::SEQ_UNIT: return "seq.unit";
1458 : 746 : case Kind::SEQ_NTH: return "seq.nth";
1459 : 0 : case Kind::SEQ_EMPTY_OF_TYPE: return "@seq.empty_of_type";
1460 : :
1461 : : // sep theory
1462 : 307 : case Kind::SEP_STAR: return "sep";
1463 : 390 : case Kind::SEP_PTO: return "pto";
1464 : 26 : case Kind::SEP_WAND: return "wand";
1465 : 107 : case Kind::SEP_EMP: return "sep.emp";
1466 : 3 : case Kind::SEP_NIL: return "sep.nil";
1467 : 234 : case Kind::SEP_LABEL: return "@sep_label";
1468 : :
1469 : : // quantifiers
1470 : 191686 : case Kind::FORALL: return "forall";
1471 : 5642 : case Kind::EXISTS: return "exists";
1472 : :
1473 : : // HO
1474 : 17269 : case Kind::HO_APPLY: return "@";
1475 : :
1476 : 380040 : default:; /* fall through */
1477 : : }
1478 : :
1479 : : // fall back on however the kind prints itself; this probably
1480 : : // won't be SMT-LIB v2 compliant, but it will be clear from the
1481 : : // output that support for the kind needs to be added here.
1482 : : // no SMT way to print these
1483 : 380040 : return kind::kindToString(k);
1484 : : }
1485 : :
1486 : 53581 : std::string Smt2Printer::smtKindStringOf(const Node& n)
1487 : : {
1488 : 53581 : Kind k = n.getKind();
1489 : 53581 : if (n.getNumChildren() > 0 && n[0].getType().isSequence())
1490 : : {
1491 : : // this method parallels cvc5::Term::getKind
1492 [ + + ][ + + ]: 3715 : switch (k)
[ + + ][ + + ]
[ + + ][ + + ]
[ - ]
1493 : : {
1494 : 1121 : case Kind::STRING_CONCAT: return "seq.++";
1495 : 1445 : case Kind::STRING_LENGTH: return "seq.len";
1496 : 640 : case Kind::STRING_SUBSTR: return "seq.extract";
1497 : 265 : case Kind::STRING_UPDATE: return "seq.update";
1498 : 18 : case Kind::STRING_CHARAT: return "seq.at";
1499 : 75 : case Kind::STRING_CONTAINS: return "seq.contains";
1500 : 2 : case Kind::STRING_INDEXOF: return "seq.indexof";
1501 : 31 : case Kind::STRING_REPLACE: return "seq.replace";
1502 : 6 : case Kind::STRING_REPLACE_ALL: return "seq.replace_all";
1503 : 50 : case Kind::STRING_REV: return "seq.rev";
1504 : 27 : case Kind::STRING_PREFIX: return "seq.prefixof";
1505 : 35 : case Kind::STRING_SUFFIX: return "seq.suffixof";
1506 : 0 : default:
1507 : : // fall through to conversion below
1508 : 0 : break;
1509 : : }
1510 : : }
1511 : : // by default
1512 : 49866 : return smtKindString(k);
1513 : : }
1514 : :
1515 : 79412 : void Smt2Printer::toStreamDeclareType(std::ostream& out,
1516 : : const std::vector<TypeNode>& argTypes,
1517 : : TypeNode tn) const
1518 : : {
1519 : 79412 : out << "(";
1520 [ + + ]: 79412 : if (!argTypes.empty())
1521 : : {
1522 : 6022 : copy(argTypes.begin(),
1523 : 6022 : argTypes.end() - 1,
1524 : 6022 : ostream_iterator<TypeNode>(out, " "));
1525 : 6022 : out << argTypes.back();
1526 : : }
1527 : 79412 : out << ") " << tn;
1528 : 79412 : }
1529 : :
1530 : 7304 : void Smt2Printer::toStreamType(std::ostream& out, TypeNode tn) const
1531 : : {
1532 : : // we currently must call TypeNode::toStream here.
1533 : 7304 : tn.toStream(out);
1534 : 7304 : }
1535 : :
1536 : 42 : void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core) const
1537 : : {
1538 : 42 : out << "(" << std::endl;
1539 [ + + ]: 42 : if (core.useNames())
1540 : : {
1541 : : // use the names
1542 : 26 : const std::vector<std::string>& cnames = core.getCoreNames();
1543 [ + + ]: 69 : for (const std::string& cn : cnames)
1544 : : {
1545 : 43 : out << cvc5::internal::quoteSymbol(cn) << std::endl;
1546 : : }
1547 : : }
1548 : : else
1549 : : {
1550 : : // otherwise, use the formulas
1551 [ + + ]: 32 : for (UnsatCore::const_iterator i = core.begin(); i != core.end(); ++i)
1552 : : {
1553 : 16 : out << *i << endl;
1554 : : }
1555 : : }
1556 : 42 : out << ")" << endl;
1557 : 42 : }/* Smt2Printer::toStream(UnsatCore, map<Expr, string>) */
1558 : :
1559 : 239 : void Smt2Printer::toStream(std::ostream& out, const smt::Model& m) const
1560 : : {
1561 : : //print the model
1562 : 239 : out << "(" << endl;
1563 : : // don't need to print approximations since they are built into choice
1564 : : // functions in the values of variables.
1565 : 239 : this->Printer::toStream(out, m);
1566 : 239 : out << ")" << endl;
1567 : : //print the heap model, if it exists
1568 : 239 : Node h, neq;
1569 [ + + ]: 239 : if (m.getHeapModel(h, neq))
1570 : : {
1571 : : // description of the heap+what nil is equal to fully describes model
1572 : 1 : out << "(heap" << endl;
1573 : 1 : out << h << endl;
1574 : 1 : out << neq << endl;
1575 : 1 : out << ")" << std::endl;
1576 : : }
1577 : 239 : }
1578 : :
1579 : 200 : void Smt2Printer::toStreamModelSort(std::ostream& out,
1580 : : TypeNode tn,
1581 : : const std::vector<Node>& elements) const
1582 : : {
1583 [ - + ]: 200 : if (!tn.isUninterpretedSort())
1584 : : {
1585 : 0 : out << "ERROR: don't know how to print non uninterpreted sort in model: "
1586 : 0 : << tn << std::endl;
1587 : 0 : return;
1588 : : }
1589 : 200 : auto modelUninterpPrint = options::ioutils::getModelUninterpPrint(out);
1590 [ + + ]: 200 : if (modelUninterpPrint == options::ModelUninterpPrintMode::Datatype)
1591 : : {
1592 : 2 : out << "(declare-datatype " << tn << " (";
1593 [ + + ]: 8 : for (size_t i=0, nelements=elements.size(); i<nelements; i++)
1594 : : {
1595 : 6 : Node trn = elements[i];
1596 [ + + ]: 6 : if (i>0)
1597 : : {
1598 : 4 : out << " ";
1599 : : }
1600 [ - + ][ - + ]: 6 : Assert (trn.getKind() == Kind::UNINTERPRETED_SORT_VALUE);
[ - - ]
1601 : : // prints as raw symbol
1602 : : const UninterpretedSortValue& av =
1603 : 6 : trn.getConst<UninterpretedSortValue>();
1604 : 6 : out << "(" << cvc5::internal::quoteSymbol(av.getSymbol()) << ")";
1605 : 6 : }
1606 : 2 : out << "))" << std::endl;
1607 : 2 : return;
1608 : : }
1609 : : // print the cardinality
1610 : 198 : out << "; cardinality of " << tn << " is " << elements.size() << endl;
1611 [ - + ]: 198 : if (modelUninterpPrint == options::ModelUninterpPrintMode::DeclSortAndFun)
1612 : : {
1613 : 0 : Printer::toStreamCmdDeclareType(out, tn);
1614 : 0 : out << std::endl;
1615 : : }
1616 : : // print the representatives
1617 [ + + ]: 588 : for (const Node& trn : elements)
1618 : : {
1619 [ + - ]: 390 : if (modelUninterpPrint == options::ModelUninterpPrintMode::DeclSortAndFun
1620 [ + + ]: 390 : || modelUninterpPrint == options::ModelUninterpPrintMode::DeclFun)
1621 : : {
1622 : 2 : out << "(declare-fun ";
1623 [ + - ]: 2 : if (trn.getKind() == Kind::UNINTERPRETED_SORT_VALUE)
1624 : : {
1625 : : // prints as raw symbol
1626 : : const UninterpretedSortValue& av =
1627 : 2 : trn.getConst<UninterpretedSortValue>();
1628 : 2 : out << cvc5::internal::quoteSymbol(av.getSymbol());
1629 : : }
1630 : : else
1631 : : {
1632 : 0 : DebugUnhandled()
1633 : 0 : << "model domain element is not an uninterpreted sort value: "
1634 : : << trn;
1635 : : out << trn;
1636 : : }
1637 : 2 : out << " () " << tn << ")" << endl;
1638 : 2 : }
1639 : : else
1640 : : {
1641 : 388 : out << "; rep: " << trn << endl;
1642 : : }
1643 : : }
1644 : : }
1645 : :
1646 : 445 : void Smt2Printer::toStreamModelTerm(std::ostream& out,
1647 : : const Node& n,
1648 : : const Node& value) const
1649 : : {
1650 [ + + ]: 445 : if (value.getKind() == Kind::LAMBDA)
1651 : : {
1652 : 13 : TypeNode rangeType = n.getType().getRangeType();
1653 : 13 : out << "(define-fun " << n << " " << value[0] << " " << rangeType << " ";
1654 : 13 : toStream(out, value[1]);
1655 : 13 : out << ")" << endl;
1656 : 13 : }
1657 : : else
1658 : : {
1659 : 432 : out << "(define-fun " << n << " () " << n.getType() << " ";
1660 : 432 : toStream(out, value);
1661 : 432 : out << ")" << endl;
1662 : : }
1663 : 445 : }
1664 : :
1665 : 23 : void Smt2Printer::toStreamCmdSuccess(std::ostream& out) const
1666 : : {
1667 : 23 : out << "success" << endl;
1668 : 23 : }
1669 : :
1670 : 0 : void Smt2Printer::toStreamCmdInterrupted(std::ostream& out) const
1671 : : {
1672 : 0 : out << "interrupted" << endl;
1673 : 0 : }
1674 : :
1675 : 6 : void Smt2Printer::toStreamCmdUnsupported(std::ostream& out) const
1676 : : {
1677 : : #ifdef CVC5_COMPETITION_MODE
1678 : : // if in competition mode, lie and say we're ok
1679 : : // (we have nothing to lose by saying success, and everything to lose
1680 : : // if we say "unsupported")
1681 : : out << "success" << endl;
1682 : : #else /* CVC5_COMPETITION_MODE */
1683 : 6 : out << "unsupported" << endl;
1684 : : #endif /* CVC5_COMPETITION_MODE */
1685 : 6 : }
1686 : :
1687 : 127 : static void errorToStream(std::ostream& out, std::string message)
1688 : : {
1689 : 127 : out << "(error " << cvc5::internal::quoteString(message) << ')' << endl;
1690 : 127 : }
1691 : :
1692 : 95 : void Smt2Printer::toStreamCmdFailure(std::ostream& out,
1693 : : const std::string& message) const
1694 : : {
1695 : 95 : errorToStream(out, message);
1696 : 95 : }
1697 : :
1698 : 32 : void Smt2Printer::toStreamCmdRecoverableFailure(
1699 : : std::ostream& out, const std::string& message) const
1700 : : {
1701 : 32 : errorToStream(out, message);
1702 : 32 : }
1703 : :
1704 : 36028 : void Smt2Printer::toStreamCmdAssert(std::ostream& out, Node n) const
1705 : : {
1706 : 36028 : out << "(assert " << n << ')';
1707 : 36028 : }
1708 : :
1709 : 1031 : void Smt2Printer::toStreamCmdPush(std::ostream& out, uint32_t nscopes) const
1710 : : {
1711 : 1031 : out << "(push " << nscopes << ")";
1712 : 1031 : }
1713 : :
1714 : 821 : void Smt2Printer::toStreamCmdPop(std::ostream& out, uint32_t nscopes) const
1715 : : {
1716 : 821 : out << "(pop " << nscopes << ")";
1717 : 821 : }
1718 : :
1719 : 4629 : void Smt2Printer::toStreamCmdCheckSat(std::ostream& out) const
1720 : : {
1721 : 4629 : out << "(check-sat)";
1722 : 4629 : }
1723 : :
1724 : 667 : void Smt2Printer::toStreamCmdCheckSatAssuming(
1725 : : std::ostream& out, const std::vector<Node>& nodes) const
1726 : : {
1727 : 667 : out << "(check-sat-assuming ( ";
1728 : 667 : copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, " "));
1729 : 667 : out << "))";
1730 : 667 : }
1731 : :
1732 : 0 : void Smt2Printer::toStreamCmdQuery(std::ostream& out, Node n) const
1733 : : {
1734 [ - - ]: 0 : if (!n.isNull())
1735 : : {
1736 : 0 : toStreamCmdCheckSatAssuming(out, {n});
1737 : : }
1738 : : else
1739 : : {
1740 : 0 : toStreamCmdCheckSat(out);
1741 : : }
1742 : 0 : }
1743 : :
1744 : 17 : void Smt2Printer::toStreamCmdReset(std::ostream& out) const
1745 : : {
1746 : 17 : out << "(reset)";
1747 : 17 : }
1748 : :
1749 : 13 : void Smt2Printer::toStreamCmdResetAssertions(std::ostream& out) const
1750 : : {
1751 : 13 : out << "(reset-assertions)";
1752 : 13 : }
1753 : :
1754 : 464 : void Smt2Printer::toStreamCmdQuit(std::ostream& out) const { out << "(exit)"; }
1755 : :
1756 : 96532 : void Smt2Printer::toStreamCmdDeclareFunction(
1757 : : std::ostream& out,
1758 : : const std::string& id,
1759 : : const std::vector<TypeNode>& argTypes,
1760 : : TypeNode type) const
1761 : : {
1762 [ + + ]: 96532 : if (d_variant == Variant::alf_variant)
1763 : : {
1764 : 17120 : out << "(declare-const " << cvc5::internal::quoteSymbol(id);
1765 [ + + ]: 17120 : if (!argTypes.empty())
1766 : : {
1767 : 4107 : out << " (->";
1768 [ + + ]: 11456 : for (const TypeNode& tn : argTypes)
1769 : : {
1770 : 7349 : out << " " << tn;
1771 : : }
1772 : : }
1773 : 17120 : out << " " << type;
1774 [ + + ]: 17120 : if (!argTypes.empty())
1775 : : {
1776 : 4107 : out << ')';
1777 : : }
1778 : 17120 : out << ')';
1779 : 17120 : return;
1780 : : }
1781 : 79412 : out << "(declare-fun " << cvc5::internal::quoteSymbol(id) << " ";
1782 : 79412 : toStreamDeclareType(out, argTypes, type);
1783 : 79412 : out << ')';
1784 : : }
1785 : :
1786 : 0 : void Smt2Printer::toStreamCmdDeclareOracleFun(
1787 : : std::ostream& out,
1788 : : const std::string& id,
1789 : : const std::vector<TypeNode>& argTypes,
1790 : : TypeNode type,
1791 : : const std::string& binName) const
1792 : : {
1793 : 0 : out << "(declare-oracle-fun " << cvc5::internal::quoteSymbol(id) << " ";
1794 : 0 : toStreamDeclareType(out, argTypes, type);
1795 : 0 : out << " " << binName << ")";
1796 : 0 : }
1797 : :
1798 : 4 : void Smt2Printer::toStreamCmdDeclarePool(
1799 : : std::ostream& out,
1800 : : const std::string& id,
1801 : : TypeNode type,
1802 : : const std::vector<Node>& initValue) const
1803 : : {
1804 : 4 : out << "(declare-pool " << cvc5::internal::quoteSymbol(id) << ' ' << type << " (";
1805 [ + + ]: 9 : for (size_t i = 0, n = initValue.size(); i < n; ++i)
1806 : : {
1807 [ + + ]: 5 : if (i != 0) {
1808 : 3 : out << ' ';
1809 : : }
1810 : 5 : out << initValue[i];
1811 : : }
1812 : 4 : out << "))";
1813 : 4 : }
1814 : :
1815 : 1911 : void Smt2Printer::toStreamCmdDefineFunction(std::ostream& out,
1816 : : const std::string& id,
1817 : : const std::vector<Node>& formals,
1818 : : TypeNode range,
1819 : : Node formula) const
1820 : : {
1821 [ + + ]: 1911 : if (d_variant == Variant::alf_variant)
1822 : : {
1823 : 557 : out << "(define " << cvc5::internal::quoteSymbol(id) << " ";
1824 : 557 : toStreamSortedVarList(out, formals);
1825 : 557 : out << " " << formula << ')';
1826 : 557 : return;
1827 : : }
1828 : 1354 : out << "(define-fun " << cvc5::internal::quoteSymbol(id) << " ";
1829 : 1354 : toStreamSortedVarList(out, formals);
1830 : 1354 : out << " " << range << ' ' << formula << ')';
1831 : : }
1832 : :
1833 : 120 : void Smt2Printer::toStreamCmdDefineFunctionRec(
1834 : : std::ostream& out,
1835 : : const std::vector<Node>& funcs,
1836 : : const std::vector<std::vector<Node>>& formals,
1837 : : const std::vector<Node>& formulas) const
1838 : : {
1839 : 120 : out << "(define-fun";
1840 [ + + ]: 120 : if (funcs.size() > 1)
1841 : : {
1842 : 9 : out << "s";
1843 : : }
1844 : 120 : out << "-rec ";
1845 [ + + ]: 120 : if (funcs.size() > 1)
1846 : : {
1847 : 9 : out << "(";
1848 : : }
1849 [ + + ]: 269 : for (unsigned i = 0, size = funcs.size(); i < size; i++)
1850 : : {
1851 [ + + ]: 149 : if (funcs.size() > 1)
1852 : : {
1853 [ + + ]: 38 : if (i > 0)
1854 : : {
1855 : 29 : out << " ";
1856 : : }
1857 : 38 : out << "(";
1858 : : }
1859 : 149 : out << funcs[i] << " ";
1860 : : // print its type signature
1861 : 149 : toStreamSortedVarList(out, formals[i]);
1862 : 149 : TypeNode type = funcs[i].getType();
1863 [ + + ]: 149 : if (type.isFunction())
1864 : : {
1865 : 141 : type = type.getRangeType();
1866 : : }
1867 : 149 : out << " " << type;
1868 [ + + ]: 149 : if (funcs.size() > 1)
1869 : : {
1870 : 38 : out << ")";
1871 : : }
1872 : 149 : }
1873 [ + + ]: 120 : if (funcs.size() > 1)
1874 : : {
1875 : 9 : out << ") (";
1876 : : }
1877 : : else
1878 : : {
1879 : 111 : out << " ";
1880 : : }
1881 [ + + ]: 269 : for (unsigned i = 0, size = formulas.size(); i < size; i++)
1882 : : {
1883 [ + + ]: 149 : if (i > 0)
1884 : : {
1885 : 29 : out << " ";
1886 : : }
1887 : 149 : out << formulas[i];
1888 : : }
1889 [ + + ]: 120 : if (funcs.size() > 1)
1890 : : {
1891 : 9 : out << ")";
1892 : : }
1893 : 120 : out << ")";
1894 : 120 : }
1895 : :
1896 : 2463 : void Smt2Printer::toStreamSortedVarList(std::ostream& out,
1897 : : const std::vector<Node>& vars) const
1898 : : {
1899 : 2463 : out << "(";
1900 [ + + ]: 6174 : for (size_t i = 0, nvars = vars.size(); i < nvars; i++)
1901 : : {
1902 : 3711 : out << "(" << vars[i] << " " << vars[i].getType() << ")";
1903 [ + + ]: 3711 : if (i + 1 < nvars)
1904 : : {
1905 : 2376 : out << " ";
1906 : : }
1907 : : }
1908 : 2463 : out << ")";
1909 : 2463 : }
1910 : :
1911 : 2961 : void Smt2Printer::toStreamCmdDeclareType(std::ostream& out,
1912 : : const std::string& id,
1913 : : size_t arity) const
1914 : : {
1915 [ + + ]: 2961 : if (d_variant == Variant::alf_variant)
1916 : : {
1917 : 1293 : out << "(declare-const " << cvc5::internal::quoteSymbol(id) << " ";
1918 [ + + ]: 1293 : if (arity > 0)
1919 : : {
1920 : 4 : out << "(->";
1921 [ + + ]: 10 : for (size_t i = 0; i < arity; i++)
1922 : : {
1923 : 6 : out << " Type";
1924 : : }
1925 : 4 : out << " Type))";
1926 : : }
1927 : : else
1928 : : {
1929 : 1289 : out << "Type)";
1930 : : }
1931 : 1293 : return;
1932 : : }
1933 : 3336 : out << "(declare-sort " << cvc5::internal::quoteSymbol(id) << " " << arity
1934 : 1668 : << ")";
1935 : : }
1936 : :
1937 : 126 : void Smt2Printer::toStreamCmdDefineType(std::ostream& out,
1938 : : const std::string& id,
1939 : : const std::vector<TypeNode>& params,
1940 : : TypeNode t) const
1941 : : {
1942 : 126 : out << "(define-sort " << cvc5::internal::quoteSymbol(id) << " (";
1943 [ + + ]: 126 : if (params.size() > 0)
1944 : : {
1945 : 1 : copy(
1946 : 1 : params.begin(), params.end() - 1, ostream_iterator<TypeNode>(out, " "));
1947 : 1 : out << params.back();
1948 : : }
1949 : 126 : out << ") " << t << ")";
1950 : 126 : }
1951 : :
1952 : 0 : void Smt2Printer::toStreamCmdSimplify(std::ostream& out, Node n) const
1953 : : {
1954 : 0 : out << "(simplify " << n << ')';
1955 : 0 : }
1956 : :
1957 : 50 : void Smt2Printer::toStreamCmdGetValue(std::ostream& out,
1958 : : const std::vector<Node>& nodes) const
1959 : : {
1960 : 50 : out << "(get-value ( ";
1961 : 50 : copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, " "));
1962 : 50 : out << "))";
1963 : 50 : }
1964 : :
1965 : 1 : void Smt2Printer::toStreamCmdGetModelDomainElements(std::ostream& out,
1966 : : TypeNode type) const
1967 : : {
1968 : 1 : out << "(get-model-domain-elements " << type << ")";
1969 : 1 : }
1970 : :
1971 : 24 : void Smt2Printer::toStreamCmdGetModel(std::ostream& out) const
1972 : : {
1973 : 24 : out << "(get-model)";
1974 : 24 : }
1975 : :
1976 : 7 : void Smt2Printer::toStreamCmdBlockModel(std::ostream& out,
1977 : : modes::BlockModelsMode mode) const
1978 : : {
1979 : 7 : out << "(block-model :";
1980 [ + + ][ - ]: 7 : switch (mode)
1981 : : {
1982 : 4 : case modes::BlockModelsMode::LITERALS: out << "literals"; break;
1983 : 3 : case modes::BlockModelsMode::VALUES: out << "values"; break;
1984 : 0 : default: Unreachable() << "Invalid block models mode " << mode;
1985 : : }
1986 : 7 : out << ")";
1987 : 7 : }
1988 : :
1989 : 3 : void Smt2Printer::toStreamCmdBlockModelValues(
1990 : : std::ostream& out, const std::vector<Node>& nodes) const
1991 : : {
1992 : 3 : out << "(block-model-values (";
1993 [ + + ]: 10 : for (size_t i = 0, n = nodes.size(); i < n; ++i)
1994 : : {
1995 [ + + ]: 7 : if (i != 0)
1996 : : {
1997 : 4 : out << ' ';
1998 : : }
1999 : 7 : out << nodes[i];
2000 : : }
2001 : 3 : out << "))";
2002 : 3 : }
2003 : :
2004 : 5 : void Smt2Printer::toStreamCmdGetAssignment(std::ostream& out) const
2005 : : {
2006 : 5 : out << "(get-assignment)";
2007 : 5 : }
2008 : :
2009 : 1 : void Smt2Printer::toStreamCmdGetAssertions(std::ostream& out) const
2010 : : {
2011 : 1 : out << "(get-assertions)";
2012 : 1 : }
2013 : :
2014 : 6 : void Smt2Printer::toStreamCmdGetProof(std::ostream& out,
2015 : : modes::ProofComponent c) const
2016 : : {
2017 : 6 : out << "(get-proof";
2018 [ + + ]: 6 : if (c != modes::ProofComponent::FULL)
2019 : : {
2020 : 4 : out << " :" << c;
2021 : : }
2022 : 6 : out << ")";
2023 : 6 : }
2024 : :
2025 : 5 : void Smt2Printer::toStreamCmdGetUnsatAssumptions(std::ostream& out) const
2026 : : {
2027 : 5 : out << "(get-unsat-assumptions)";
2028 : 5 : }
2029 : :
2030 : 12 : void Smt2Printer::toStreamCmdGetUnsatCore(std::ostream& out) const
2031 : : {
2032 : 12 : out << "(get-unsat-core)";
2033 : 12 : }
2034 : :
2035 : 3 : void Smt2Printer::toStreamCmdGetDifficulty(std::ostream& out) const
2036 : : {
2037 : 3 : out << "(get-difficulty)";
2038 : 3 : }
2039 : :
2040 : 3 : void Smt2Printer::toStreamCmdGetTimeoutCore(std::ostream& out) const
2041 : : {
2042 : 3 : out << "(get-timeout-core)";
2043 : 3 : }
2044 : :
2045 : 3 : void Smt2Printer::toStreamCmdGetTimeoutCoreAssuming(
2046 : : std::ostream& out, const std::vector<Node>& assumptions) const
2047 : : {
2048 : 3 : out << "(get-timeout-core-assuming (";
2049 : 3 : bool firstTime = true;
2050 [ + + ]: 9 : for (const Node& a : assumptions)
2051 : : {
2052 [ + + ]: 6 : if (firstTime)
2053 : : {
2054 : 3 : firstTime = false;
2055 : : }
2056 : : else
2057 : : {
2058 : 3 : out << " ";
2059 : : }
2060 : 6 : out << a;
2061 : : }
2062 : 3 : out << "))";
2063 : 3 : }
2064 : :
2065 : 7 : void Smt2Printer::toStreamCmdGetLearnedLiterals(std::ostream& out,
2066 : : modes::LearnedLitType t) const
2067 : : {
2068 : 7 : out << "(get-learned-literals";
2069 [ + + ]: 7 : if (t != modes::LearnedLitType::INPUT)
2070 : : {
2071 : 5 : out << " :" << t;
2072 : : }
2073 : 7 : out << ")";
2074 : 7 : }
2075 : :
2076 : 4208 : void Smt2Printer::toStreamCmdSetBenchmarkLogic(std::ostream& out,
2077 : : const std::string& logic) const
2078 : : {
2079 : 4208 : out << "(set-logic " << logic << ')';
2080 : 4208 : }
2081 : :
2082 : 3163 : void Smt2Printer::toStreamCmdSetInfo(std::ostream& out,
2083 : : const std::string& flag,
2084 : : const std::string& value) const
2085 : : {
2086 : 3163 : out << "(set-info :" << flag << " " << value << ")";
2087 : 3163 : }
2088 : :
2089 : 16 : void Smt2Printer::toStreamCmdGetInfo(std::ostream& out,
2090 : : const std::string& flag) const
2091 : : {
2092 : 16 : out << "(get-info :" << flag << ')';
2093 : 16 : }
2094 : :
2095 : 1423 : void Smt2Printer::toStreamCmdSetOption(std::ostream& out,
2096 : : const std::string& flag,
2097 : : const std::string& value) const
2098 : : {
2099 : 1423 : out << "(set-option :" << flag << ' ';
2100 : : // special cases: output channels require surrounding quotes in smt2 format
2101 [ + + ]: 2844 : if (flag == "diagnostic-output-channel" || flag == "regular-output-channel"
2102 [ + + ][ + + ]: 2844 : || flag == "in")
[ + + ]
2103 : : {
2104 : 4 : out << "\"" << value << "\"";
2105 : : }
2106 : : else
2107 : : {
2108 : 1419 : out << value;
2109 : : }
2110 : 1423 : out << ')';
2111 : 1423 : }
2112 : :
2113 : 43 : void Smt2Printer::toStreamCmdGetOption(std::ostream& out,
2114 : : const std::string& flag) const
2115 : : {
2116 : 43 : out << "(get-option :" << flag << ')';
2117 : 43 : }
2118 : :
2119 : 1201 : void Smt2Printer::toStream(std::ostream& out, const DType& dt) const
2120 : : {
2121 [ + + ]: 3429 : for (size_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
2122 : : {
2123 : 2228 : const DTypeConstructor& cons = dt[i];
2124 [ + + ]: 2228 : if (i != 0)
2125 : : {
2126 : 1027 : out << " ";
2127 : : }
2128 : 2228 : out << "(" << cvc5::internal::quoteSymbol(cons.getName());
2129 [ + + ]: 4322 : for (size_t j = 0, nargs = cons.getNumArgs(); j < nargs; j++)
2130 : : {
2131 : 2094 : const DTypeSelector& arg = cons[j];
2132 : 2094 : out << " (" << arg.getSelector() << " " << arg.getRangeType() << ")";
2133 : : }
2134 : 2228 : out << ")";
2135 : : }
2136 : 1201 : }
2137 : :
2138 : 945 : void Smt2Printer::toStreamCmdDatatypeDeclaration(
2139 : : std::ostream& out, const std::vector<TypeNode>& datatypes) const
2140 : : {
2141 [ - + ][ - + ]: 945 : Assert(!datatypes.empty());
[ - - ]
2142 [ - + ][ - + ]: 945 : Assert(datatypes[0].isDatatype());
[ - - ]
2143 : 945 : const DType& d0 = datatypes[0].getDType();
2144 [ - + ]: 945 : if (d0.isTuple())
2145 : : {
2146 : : // not necessary to print tuples
2147 : 0 : Assert(datatypes.size() == 1);
2148 : 0 : return;
2149 : : }
2150 : 945 : out << "(declare-";
2151 : : // Ethos does not support codatatypes, we just print as an ordinary
2152 : : // datatype for now
2153 [ + + ][ + + ]: 945 : if (d0.isCodatatype() && d_variant != Variant::alf_variant)
[ + + ]
2154 : : {
2155 : 16 : out << "co";
2156 : : }
2157 : 945 : out << "datatypes";
2158 : 945 : out << " (";
2159 [ + + ]: 2146 : for (const TypeNode& t : datatypes)
2160 : : {
2161 [ - + ][ - + ]: 1201 : Assert(t.isDatatype());
[ - - ]
2162 : 1201 : const DType& d = t.getDType();
2163 : 1201 : out << "(" << cvc5::internal::quoteSymbol(d.getName());
2164 : 1201 : out << " " << d.getNumParameters() << ")";
2165 : : }
2166 : 945 : out << ") (";
2167 [ + + ]: 2146 : for (const TypeNode& t : datatypes)
2168 : : {
2169 [ - + ][ - + ]: 1201 : Assert(t.isDatatype());
[ - - ]
2170 : 1201 : const DType& d = t.getDType();
2171 [ + + ]: 1201 : if (d.isParametric())
2172 : : {
2173 : 50 : out << "(par (";
2174 [ + + ]: 114 : for (unsigned p = 0, nparam = d.getNumParameters(); p < nparam; p++)
2175 : : {
2176 [ + + ]: 64 : out << (p > 0 ? " " : "") << d.getParameter(p);
2177 : : }
2178 : 50 : out << ")";
2179 : : }
2180 : 1201 : out << "(";
2181 : 1201 : toStream(out, d);
2182 : 1201 : out << ")";
2183 [ + + ]: 1201 : if (d.isParametric())
2184 : : {
2185 : 50 : out << ")";
2186 : : }
2187 : : }
2188 : 945 : out << ")";
2189 : 945 : out << ")";
2190 : : }
2191 : :
2192 : 49 : void Smt2Printer::toStreamCmdDeclareHeap(std::ostream& out,
2193 : : TypeNode locType,
2194 : : TypeNode dataType) const
2195 : : {
2196 : 49 : out << "(declare-heap (" << locType << " " << dataType << "))";
2197 : 49 : }
2198 : :
2199 : 3974 : void Smt2Printer::toStreamSkolem(std::ostream& out,
2200 : : Node cacheVal,
2201 : : SkolemId id,
2202 : : bool isApplied,
2203 : : int toDepth,
2204 : : const LetBinding* lbind) const
2205 : : {
2206 : : // true if this is a standalone skolem that requires printing with arguments
2207 [ + + ][ + + ]: 3974 : bool unappliedApp = (!isApplied && !cacheVal.isNull());
2208 [ + + ]: 3974 : if (unappliedApp)
2209 : : {
2210 : 3605 : out << "(";
2211 : : }
2212 : 3974 : out << "@" << id;
2213 [ + + ]: 3974 : if (cacheVal.getKind() == Kind::SEXPR)
2214 : : {
2215 [ + + ]: 814 : for (const Node& cv : cacheVal)
2216 : : {
2217 : 576 : out << " ";
2218 : 576 : toStream(out, cv, lbind, toDepth);
2219 : 576 : }
2220 : : }
2221 [ + + ]: 3736 : else if (!cacheVal.isNull())
2222 : : {
2223 : 3546 : out << " ";
2224 : 3546 : toStream(out, cacheVal, lbind, toDepth);
2225 : : }
2226 [ + + ]: 3974 : if (unappliedApp)
2227 : : {
2228 : 3605 : out << ")";
2229 : : }
2230 [ + + ]: 369 : else if (isApplied)
2231 : : {
2232 : : // separates further arguments
2233 : 267 : out << " ";
2234 : : }
2235 : 3974 : }
2236 : :
2237 : 9 : void Smt2Printer::toStreamCmdEmpty(CVC5_UNUSED std::ostream& out,
2238 : : CVC5_UNUSED const std::string& name) const
2239 : : {
2240 : 9 : }
2241 : :
2242 : 9 : void Smt2Printer::toStreamCmdEcho(std::ostream& out,
2243 : : const std::string& output) const
2244 : : {
2245 : 9 : out << "(echo " << cvc5::internal::quoteString(output) << ')';
2246 : 9 : }
2247 : :
2248 : : /*
2249 : : --------------------------------------------------------------------------
2250 : : Handling SyGuS commands
2251 : : --------------------------------------------------------------------------
2252 : : */
2253 : :
2254 : 235 : std::string Smt2Printer::sygusGrammarString(const TypeNode& t)
2255 : : {
2256 : 235 : std::stringstream out;
2257 [ + - ][ + - ]: 235 : if (!t.isNull() && t.isDatatype() && t.getDType().isSygus())
[ + - ][ + - ]
2258 : : {
2259 : 235 : std::stringstream types_predecl, types_list;
2260 : 235 : std::set<TypeNode> grammarTypes;
2261 : 235 : std::list<TypeNode> typesToPrint;
2262 : 235 : grammarTypes.insert(t);
2263 : 235 : typesToPrint.push_back(t);
2264 : 235 : NodeManager* nm = t.getNodeManager();
2265 : : // for each datatype in grammar
2266 : : // name
2267 : : // sygus type
2268 : : // constructors in order
2269 : : do
2270 : : {
2271 : 482 : TypeNode curr = typesToPrint.front();
2272 : 482 : typesToPrint.pop_front();
2273 : : // skip builtin fields, which can originate from any-constant constructors
2274 [ + - ][ - + ]: 482 : if (!curr.isDatatype() || !curr.getDType().isSygus())
[ - + ]
2275 : : {
2276 : 0 : continue;
2277 : : }
2278 : 482 : const DType& dt = curr.getDType();
2279 : 482 : types_list << '(' << dt.getName() << ' ' << dt.getSygusType() << " (";
2280 : 482 : types_predecl << '(' << dt.getName() << ' ' << dt.getSygusType() << ") ";
2281 [ + + ]: 2478 : for (size_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
2282 : : {
2283 [ + + ]: 1996 : if (i > 0)
2284 : : {
2285 : 1514 : types_list << ' ';
2286 : : }
2287 : 1996 : const DTypeConstructor& cons = dt[i];
2288 [ + + ]: 1996 : if (cons.isSygusAnyConstant())
2289 : : {
2290 : 31 : types_list << "(Constant " << cons[0].getRangeType() << ")";
2291 : : }
2292 : : else
2293 : : {
2294 : : // make a sygus term
2295 : 1965 : std::vector<Node> cchildren;
2296 : 1965 : cchildren.push_back(cons.getConstructor());
2297 [ + + ]: 3921 : for (size_t j = 0, nargs = cons.getNumArgs(); j < nargs; j++)
2298 : : {
2299 : 1956 : TypeNode argType = cons[j].getRangeType();
2300 : 1956 : std::stringstream ss;
2301 : 1956 : ss << argType;
2302 : 1956 : Node bv = NodeManager::mkBoundVar(ss.str(), argType);
2303 : 1956 : cchildren.push_back(bv);
2304 : : // if fresh type, store it for later processing
2305 [ + + ]: 1956 : if (grammarTypes.insert(argType).second)
2306 : : {
2307 : 247 : typesToPrint.push_back(argType);
2308 : : }
2309 : 1956 : }
2310 : 1965 : Node consToPrint = nm->mkNode(Kind::APPLY_CONSTRUCTOR, cchildren);
2311 : : // now, print it using the conversion to builtin with external
2312 : 3930 : types_list << theory::datatypes::utils::sygusToBuiltin(consToPrint,
2313 : 1965 : true);
2314 : 1965 : }
2315 : : }
2316 : 482 : types_list << "))";
2317 [ + - ][ + + ]: 964 : } while (!typesToPrint.empty());
2318 : :
2319 : 235 : out << "(" << types_predecl.str() << ")(" << types_list.str() << ')';
2320 : 235 : }
2321 : 470 : return out.str();
2322 : 235 : }
2323 : :
2324 : 403 : void Smt2Printer::toStreamCmdSynthFun(std::ostream& out,
2325 : : const std::string& id,
2326 : : const std::vector<Node>& vars,
2327 : : TypeNode rangeType,
2328 : : TypeNode sygusType) const
2329 : : {
2330 : 403 : out << "(synth-fun " << cvc5::internal::quoteSymbol(id) << ' ';
2331 : : // print variable list
2332 : 403 : toStreamSortedVarList(out, vars);
2333 : : // print return type
2334 : 403 : out << ' ' << rangeType;
2335 : : // print grammar, if any
2336 [ + + ]: 403 : if (!sygusType.isNull())
2337 : : {
2338 : 192 : out << sygusGrammarString(sygusType);
2339 : : }
2340 : 403 : out << ')';
2341 : 403 : }
2342 : :
2343 : 360 : void Smt2Printer::toStreamCmdDeclareVar(std::ostream& out,
2344 : : const std::string& id,
2345 : : TypeNode type) const
2346 : : {
2347 : 720 : out << "(declare-var " << cvc5::internal::quoteSymbol(id) << ' ' << type
2348 : 360 : << ')';
2349 : 360 : }
2350 : :
2351 : 699 : void Smt2Printer::toStreamCmdConstraint(std::ostream& out, Node n) const
2352 : : {
2353 : 699 : out << "(constraint " << n << ')';
2354 : 699 : }
2355 : :
2356 : 4 : void Smt2Printer::toStreamCmdAssume(std::ostream& out, Node n) const
2357 : : {
2358 : 4 : out << "(assume " << n << ')';
2359 : 4 : }
2360 : :
2361 : 13 : void Smt2Printer::toStreamCmdInvConstraint(
2362 : : std::ostream& out, Node inv, Node pre, Node trans, Node post) const
2363 : : {
2364 : 26 : out << "(inv-constraint " << inv << ' ' << pre << ' ' << trans << ' ' << post
2365 : 13 : << ')';
2366 : 13 : }
2367 : :
2368 : 232 : void Smt2Printer::toStreamCmdCheckSynth(std::ostream& out) const
2369 : : {
2370 : 232 : out << "(check-synth)";
2371 : 232 : }
2372 : :
2373 : 6 : void Smt2Printer::toStreamCmdCheckSynthNext(std::ostream& out) const
2374 : : {
2375 : 6 : out << "(check-synth-next)";
2376 : 6 : }
2377 : :
2378 : 26 : void Smt2Printer::toStreamCmdFindSynth(std::ostream& out,
2379 : : modes::FindSynthTarget fst,
2380 : : TypeNode sygusType) const
2381 : : {
2382 : 26 : out << "(find-synth :" << fst;
2383 : : // print grammar, if any
2384 [ + + ]: 26 : if (!sygusType.isNull())
2385 : : {
2386 : 1 : out << " " << sygusGrammarString(sygusType);
2387 : : }
2388 : 26 : out << ")";
2389 : 26 : }
2390 : :
2391 : 1 : void Smt2Printer::toStreamCmdFindSynthNext(std::ostream& out) const
2392 : : {
2393 : 1 : out << "(find-synth-next)";
2394 : 1 : }
2395 : :
2396 : 23 : void Smt2Printer::toStreamCmdGetInterpol(std::ostream& out,
2397 : : const std::string& name,
2398 : : Node conj,
2399 : : TypeNode sygusType) const
2400 : : {
2401 : 23 : out << "(get-interpolant " << cvc5::internal::quoteSymbol(name) << ' ' << conj;
2402 [ + + ]: 23 : if (!sygusType.isNull())
2403 : : {
2404 : 5 : out << ' ' << sygusGrammarString(sygusType);
2405 : : }
2406 : 23 : out << ')';
2407 : 23 : }
2408 : :
2409 : 1 : void Smt2Printer::toStreamCmdGetInterpolNext(std::ostream& out) const
2410 : : {
2411 : 1 : out << "(get-interpolant-next)";
2412 : 1 : }
2413 : :
2414 : 33 : void Smt2Printer::toStreamCmdGetAbduct(std::ostream& out,
2415 : : const std::string& name,
2416 : : Node conj,
2417 : : TypeNode sygusType) const
2418 : : {
2419 : 33 : out << "(get-abduct ";
2420 : 33 : out << name << ' ';
2421 : 33 : out << conj << ' ';
2422 : :
2423 : : // print grammar, if any
2424 [ + + ]: 33 : if (!sygusType.isNull())
2425 : : {
2426 : 6 : out << sygusGrammarString(sygusType);
2427 : : }
2428 : 33 : out << ')';
2429 : 33 : }
2430 : :
2431 : 6 : void Smt2Printer::toStreamCmdGetAbductNext(std::ostream& out) const
2432 : : {
2433 : 6 : out << "(get-abduct-next)";
2434 : 6 : }
2435 : :
2436 : 19 : void Smt2Printer::toStreamCmdGetQuantifierElimination(std::ostream& out,
2437 : : Node n,
2438 : : bool doFull) const
2439 : : {
2440 [ + + ]: 19 : out << '(' << (doFull ? "get-qe" : "get-qe-disjunct") << ' ' << n << ')';
2441 : 19 : }
2442 : :
2443 : : /*
2444 : : --------------------------------------------------------------------------
2445 : : End of Handling SyGuS commands
2446 : : --------------------------------------------------------------------------
2447 : : */
2448 : :
2449 : : } // namespace smt2
2450 : : } // namespace printer
2451 : : } // namespace cvc5::internal
|
