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 : : * The pretty-printer interface for the SMT2 output language.
11 : : */
12 : :
13 : : #include "printer/smt2/smt2_printer.h"
14 : :
15 : : #include <cvc5/cvc5.h>
16 : :
17 : : #include <iostream>
18 : : #include <list>
19 : : #include <string>
20 : : #include <typeinfo>
21 : : #include <vector>
22 : :
23 : : #include "expr/array_store_all.h"
24 : : #include "expr/ascription_type.h"
25 : : #include "expr/cardinality_constraint.h"
26 : : #include "expr/dtype.h"
27 : : #include "expr/dtype_cons.h"
28 : : #include "expr/emptybag.h"
29 : : #include "expr/emptyset.h"
30 : : #include "expr/function_array_const.h"
31 : : #include "expr/node_visitor.h"
32 : : #include "expr/sequence.h"
33 : : #include "expr/skolem_manager.h"
34 : : #include "options/io_utils.h"
35 : : #include "options/language.h"
36 : : #include "printer/let_binding.h"
37 : : #include "proof/unsat_core.h"
38 : : #include "smt/model.h"
39 : : #include "theory/arrays/theory_arrays_rewriter.h"
40 : : #include "theory/builtin/abstract_type.h"
41 : : #include "theory/builtin/generic_op.h"
42 : : #include "theory/datatypes/project_op.h"
43 : : #include "theory/datatypes/sygus_datatype_utils.h"
44 : : #include "theory/quantifiers/quantifiers_attributes.h"
45 : : #include "theory/strings/theory_strings_utils.h"
46 : : #include "theory/theory_model.h"
47 : : #include "theory/uf/function_const.h"
48 : : #include "theory/uf/theory_uf_rewriter.h"
49 : : #include "util/bitvector.h"
50 : : #include "util/divisible.h"
51 : : #include "util/finite_field_value.h"
52 : : #include "util/floatingpoint.h"
53 : : #include "util/iand.h"
54 : : #include "util/indexed_root_predicate.h"
55 : : #include "util/real_algebraic_number.h"
56 : : #include "util/regexp.h"
57 : : #include "util/smt2_quote_string.h"
58 : : #include "util/string.h"
59 : : #include "util/uninterpreted_sort_value.h"
60 : :
61 : : using namespace std;
62 : :
63 : : namespace cvc5::internal {
64 : : namespace printer {
65 : : namespace smt2 {
66 : :
67 : 2183335 : static void toStreamRational(std::ostream& out, const Rational& r, bool isReal)
68 : : {
69 : 2183335 : bool neg = r.sgn() < 0;
70 : 2183335 : bool arithTokens = options::ioutils::getPrintArithLitToken(out);
71 : : // Print the rational, possibly as a real.
72 : : // Notice that we print (/ (- 5) 3) instead of (- (/ 5 3)),
73 : : // the former is compliant with real values in the smt lib standard.
74 [ + + ]: 2183335 : if (r.isIntegral())
75 : : {
76 [ + + ]: 2124801 : if (arithTokens)
77 : : {
78 [ + + ]: 1660271 : if (neg)
79 : : {
80 : 191320 : out << "-" << -r;
81 : : }
82 : : else
83 : : {
84 : 1468951 : out << r;
85 : : }
86 [ + + ]: 1660271 : if (isReal)
87 : : {
88 : 218536 : out << "/1";
89 : : }
90 : : }
91 : : else
92 : : {
93 [ + + ]: 464530 : if (neg)
94 : : {
95 : 24635 : out << "(- " << -r;
96 : : }
97 : : else
98 : : {
99 : 439895 : out << r;
100 : : }
101 [ + + ]: 464530 : if (isReal)
102 : : {
103 : 67841 : out << ".0";
104 : : }
105 [ + + ]: 464530 : if (neg)
106 : : {
107 : 24635 : out << ")";
108 : : }
109 : : }
110 : : }
111 : : else
112 : : {
113 [ - + ][ - + ]: 58534 : Assert(isReal);
[ - - ]
114 [ + + ]: 58534 : if (arithTokens)
115 : : {
116 [ + + ]: 26205 : if (neg)
117 : : {
118 : 13456 : Rational abs_r = (-r);
119 : 13456 : out << '-' << abs_r.getNumerator() << '/' << abs_r.getDenominator();
120 : 13456 : }
121 : : else
122 : : {
123 : 12749 : out << r.getNumerator() << '/' << r.getDenominator();
124 : : }
125 : : }
126 : : else
127 : : {
128 : 32329 : out << "(/ ";
129 [ + + ]: 32329 : if (neg)
130 : : {
131 : 16343 : Rational abs_r = (-r);
132 : 16343 : out << "(- " << abs_r.getNumerator() << ") " << abs_r.getDenominator();
133 : 16343 : }
134 : : else
135 : : {
136 : 15986 : out << r.getNumerator() << ' ' << r.getDenominator();
137 : : }
138 : 32329 : out << ')';
139 : : }
140 : : }
141 : 2183335 : }
142 : :
143 : 11269965 : void Smt2Printer::toStream(std::ostream& out,
144 : : TNode n,
145 : : int toDepth,
146 : : size_t dag) const
147 : : {
148 [ + + ]: 11269965 : if (dag == 0)
149 : : {
150 : 6107293 : toStream(out, n, nullptr, toDepth);
151 : 6107293 : return;
152 : : }
153 : 10325344 : LetBinding lbind("_let_", dag + 1);
154 : :
155 : 5162672 : std::string cparen;
156 : 5162672 : std::vector<Node> letList;
157 : 5162672 : lbind.letify(n, letList);
158 [ + + ]: 5162672 : if (!letList.empty())
159 : : {
160 : 25329 : std::stringstream cparens;
161 : 25329 : std::map<Node, uint32_t>::const_iterator it;
162 [ + + ]: 255996 : for (size_t i = 0, nlets = letList.size(); i < nlets; i++)
163 : : {
164 : 230667 : Node nl = letList[i];
165 : 230667 : out << "(let ((";
166 : 230667 : uint32_t id = lbind.getId(nl);
167 : 230667 : out << "_let_" << id << " ";
168 : 230667 : toStream(out, nl, &lbind, toDepth, false);
169 : 230667 : out << ")) ";
170 : 230667 : cparens << ")";
171 : 230667 : }
172 : 25329 : cparen = cparens.str();
173 : 25329 : }
174 : : // Print the body, passing the lbind object. Note that we don't convert
175 : : // n here, and instead rely on the printing method to lookup ids in the
176 : : // given let binding.
177 : 5162672 : toStream(out, n, &lbind, toDepth);
178 : 5162672 : out << cparen;
179 : 5162672 : lbind.popScope();
180 : 5162672 : }
181 : :
182 : 5171601 : void Smt2Printer::toStream(std::ostream& out,
183 : : TNode n,
184 : : const LetBinding* lbind,
185 : : bool lbindTop) const
186 : : {
187 : 5171601 : int toDepth = options::ioutils::getNodeDepth(out);
188 : 5171601 : toStream(out, n, lbind, toDepth, lbindTop);
189 : 5171601 : }
190 : :
191 : 11140416 : void Smt2Printer::toStream(std::ostream& out, TNode n) const
192 : : {
193 : 11140416 : size_t dag = options::ioutils::getDagThresh(out);
194 : 11140416 : int toDepth = options::ioutils::getNodeDepth(out);
195 : 11140416 : toStream(out, n, toDepth, dag);
196 : 11140416 : }
197 : :
198 : 339260 : void Smt2Printer::toStream(std::ostream& out, Kind k) const
199 : : {
200 : 339260 : out << smtKindString(k);
201 : 339260 : }
202 : :
203 : 39595053 : bool Smt2Printer::toStreamBase(std::ostream& out,
204 : : TNode n,
205 : : const LetBinding* lbind,
206 : : int toDepth) const
207 : : {
208 : : // null
209 [ + + ]: 39595053 : if (n.getKind() == Kind::NULL_EXPR)
210 : : {
211 : 14 : out << "null";
212 : 14 : return true;
213 : : }
214 : :
215 : 39595039 : NodeManager* nm = n.getNodeManager();
216 : : // constant
217 [ + + ]: 39595039 : if (n.getMetaKind() == kind::metakind::CONSTANT)
218 : : {
219 [ + + ][ + + ]: 5261604 : switch (n.getKind())
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ - + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
220 : : {
221 : 572464 : case Kind::TYPE_CONSTANT:
222 [ + + ][ + + ]: 572464 : switch (n.getConst<TypeConstant>())
[ + + ][ - ]
223 : : {
224 : 153177 : case BOOLEAN_TYPE: out << "Bool"; break;
225 : 30502 : case REAL_TYPE: out << "Real"; break;
226 : 308663 : case INTEGER_TYPE: out << "Int"; break;
227 : 51748 : case STRING_TYPE: out << "String"; break;
228 : 28030 : case REGEXP_TYPE: out << "RegLan"; break;
229 : 344 : case ROUNDINGMODE_TYPE: out << "RoundingMode"; break;
230 : 0 : default:
231 : : // fall back on whatever operator<< does on underlying type; we
232 : : // might luck out and be SMT-LIB v2 compliant
233 : 0 : n.constToStream(out);
234 : : }
235 : 572464 : break;
236 : 154022 : case Kind::ABSTRACT_TYPE:
237 : : {
238 : 154022 : const AbstractType& at = n.getConst<AbstractType>();
239 : 154022 : Kind atk = at.getKind();
240 : 154022 : out << "?";
241 : : // note that the fully abstract type (where atk is ABSTRACT_TYPE) is
242 : : // printed simply as "?", not, e.g., "?Abstract"
243 [ + + ]: 154022 : if (atk != Kind::ABSTRACT_TYPE)
244 : : {
245 : 49007 : out << smtKindString(atk);
246 : : }
247 : 154022 : break;
248 : : }
249 : 2845 : case Kind::APPLY_INDEXED_SYMBOLIC_OP:
250 : 2845 : out << smtKindString(n.getConst<GenericOp>().getKind());
251 : 2845 : break;
252 : 69339 : case Kind::BITVECTOR_TYPE:
253 : 69339 : out << "(_ BitVec " << n.getConst<BitVectorSize>().d_size << ")";
254 : 69339 : break;
255 : 587 : case Kind::FINITE_FIELD_TYPE:
256 : 587 : out << "(_ FiniteField " << n.getConst<FfSize>().d_val << ")";
257 : 587 : break;
258 : 215 : case Kind::FLOATINGPOINT_TYPE:
259 : 215 : out << "(_ FloatingPoint "
260 : 215 : << n.getConst<FloatingPointSize>().exponentWidth() << " "
261 : 215 : << n.getConst<FloatingPointSize>().significandWidth() << ")";
262 : 215 : break;
263 : 171271 : case Kind::CONST_BITVECTOR:
264 : : {
265 : 171271 : const BitVector& bv = n.getConst<BitVector>();
266 [ + + ]: 171271 : if (options::ioutils::getBvPrintConstsAsIndexedSymbols(out))
267 : : {
268 : 10 : out << "(_ bv" << bv.getValue() << " " << bv.getSize() << ")";
269 : : }
270 : : else
271 : : {
272 : 171261 : out << "#b" << bv.toString();
273 : : }
274 : 171271 : break;
275 : : }
276 : 1139 : case Kind::CONST_FINITE_FIELD:
277 : : {
278 : 1139 : const FiniteFieldValue& ff = n.getConst<FiniteFieldValue>();
279 : 1139 : out << "#f" << ff.getValue() << "m" << ff.getFieldSize();
280 : 1139 : break;
281 : : }
282 : 548 : case Kind::CONST_FLOATINGPOINT:
283 : : {
284 : 1096 : out << n.getConst<FloatingPoint>().toString(
285 : 548 : options::ioutils::getBvPrintConstsAsIndexedSymbols(out));
286 : 548 : break;
287 : : }
288 : 1201 : case Kind::CONST_ROUNDINGMODE:
289 [ + + ][ + + ]: 1201 : switch (n.getConst<RoundingMode>())
[ + - ]
290 : : {
291 : 357 : case RoundingMode::ROUND_NEAREST_TIES_TO_EVEN:
292 : 357 : out << "roundNearestTiesToEven";
293 : 357 : break;
294 : 197 : case RoundingMode::ROUND_NEAREST_TIES_TO_AWAY:
295 : 197 : out << "roundNearestTiesToAway";
296 : 197 : break;
297 : 184 : case RoundingMode::ROUND_TOWARD_POSITIVE:
298 : 184 : out << "roundTowardPositive";
299 : 184 : break;
300 : 184 : case RoundingMode::ROUND_TOWARD_NEGATIVE:
301 : 184 : out << "roundTowardNegative";
302 : 184 : break;
303 : 279 : case RoundingMode::ROUND_TOWARD_ZERO: out << "roundTowardZero"; break;
304 : 0 : default:
305 : 0 : Unreachable() << "Invalid value of rounding mode constant ("
306 : 0 : << n.getConst<RoundingMode>() << ")";
307 : : }
308 : 1201 : break;
309 : 1994980 : case Kind::CONST_BOOLEAN:
310 : : // the default would print "1" or "0" for bool, that's not correct
311 : : // for our purposes
312 [ + + ]: 1994980 : out << (n.getConst<bool>() ? "true" : "false");
313 : 1994980 : break;
314 : 36 : case Kind::BUILTIN: out << smtKindString(n.getConst<Kind>()); break;
315 : 344911 : case Kind::CONST_RATIONAL:
316 : : {
317 : 344911 : const Rational& r = n.getConst<Rational>();
318 : 344911 : toStreamRational(out, r, true);
319 : 344911 : break;
320 : : }
321 : 1838424 : case Kind::CONST_INTEGER:
322 : : {
323 : 1838424 : const Rational& r = n.getConst<Rational>();
324 : 1838424 : toStreamRational(out, r, false);
325 : 1838424 : break;
326 : : }
327 : :
328 : 68875 : case Kind::CONST_STRING:
329 : : {
330 : 68875 : std::string s = n.getConst<String>().toString();
331 : 68875 : out << '"';
332 [ + + ]: 274209 : for (size_t i = 0; i < s.size(); ++i)
333 : : {
334 : 205334 : char c = s[i];
335 [ + + ]: 205334 : if (c == '"')
336 : : {
337 : 39 : out << "\"\"";
338 : : }
339 : : else
340 : : {
341 : 205295 : out << c;
342 : : }
343 : : }
344 : 68875 : out << '"';
345 : 68875 : break;
346 : 68875 : }
347 : 685 : case Kind::CONST_SEQUENCE:
348 : : {
349 : 685 : const Sequence& sn = n.getConst<Sequence>();
350 : 685 : const std::vector<Node>& snvec = sn.getVec();
351 [ + + ]: 685 : if (snvec.empty())
352 : : {
353 : 485 : out << "(as seq.empty ";
354 : 485 : toStreamType(out, n.getType());
355 : 485 : out << ")";
356 : : }
357 : : else
358 : : {
359 : : // prints as the corresponding concatenation of seq.unit
360 : 200 : Node cc = theory::strings::utils::mkConcatForConstSequence(n);
361 : 200 : toStream(out, cc, lbind, toDepth);
362 : 200 : }
363 : 685 : break;
364 : : }
365 : :
366 : 204 : case Kind::STORE_ALL:
367 : : {
368 : 204 : ArrayStoreAll asa = n.getConst<ArrayStoreAll>();
369 : 204 : out << "((as const ";
370 : 204 : toStreamType(out, asa.getType());
371 : 204 : out << ") ";
372 [ - + ]: 408 : toStream(
373 : 204 : out, asa.getValue(), lbind, toDepth < 0 ? toDepth : toDepth - 1);
374 : 204 : out << ")";
375 : 204 : break;
376 : 204 : }
377 : 3929 : case Kind::FUNCTION_ARRAY_CONST:
378 : : {
379 : : // prints as the equivalent lambda
380 : 3929 : Node lam = theory::uf::FunctionConst::toLambda(n);
381 : 3929 : toStream(out, lam, lbind, toDepth);
382 : 3929 : break;
383 : 3929 : }
384 : :
385 : 1769 : case Kind::UNINTERPRETED_SORT_VALUE:
386 : : {
387 : 1769 : const UninterpretedSortValue& v = n.getConst<UninterpretedSortValue>();
388 : 3538 : out << "(as " << cvc5::internal::quoteSymbol(v.getSymbol()) << " "
389 : 1769 : << n.getType() << ")";
390 : 1769 : break;
391 : : }
392 : 91 : case Kind::CARDINALITY_CONSTRAINT_OP:
393 : : {
394 : 91 : const CardinalityConstraint& cc = n.getConst<CardinalityConstraint>();
395 : 91 : TypeNode tn = cc.getType();
396 : 91 : out << "(_ fmf.card " << tn << " " << cc.getUpperBound() << ")";
397 : 91 : }
398 : 91 : break;
399 : 0 : case Kind::COMBINED_CARDINALITY_CONSTRAINT_OP:
400 : : {
401 : : const CombinedCardinalityConstraint& cc =
402 : 0 : n.getConst<CombinedCardinalityConstraint>();
403 : 0 : out << "(_ fmf.combined_card " << cc.getUpperBound() << ")";
404 : : }
405 : 0 : break;
406 : 30 : case Kind::DIVISIBLE_OP:
407 : 30 : out << "(_ divisible " << n.getConst<Divisible>().k << ")";
408 : 30 : break;
409 : 1123 : case Kind::SET_EMPTY:
410 : 1123 : out << "(as set.empty ";
411 : 1123 : toStreamType(out, n.getConst<EmptySet>().getType());
412 : 1123 : out << ")";
413 : 1123 : break;
414 : :
415 : 184 : case Kind::BAG_EMPTY:
416 : 184 : out << "(as bag.empty ";
417 : 184 : toStreamType(out, n.getConst<EmptyBag>().getType());
418 : 184 : out << ")";
419 : 184 : break;
420 : 8113 : case Kind::BITVECTOR_EXTRACT_OP:
421 : : {
422 : 8113 : BitVectorExtract p = n.getConst<BitVectorExtract>();
423 : 8113 : out << "(_ extract " << p.d_high << ' ' << p.d_low << ")";
424 : 8113 : break;
425 : : }
426 : 463 : case Kind::BITVECTOR_REPEAT_OP:
427 : 463 : out << "(_ repeat " << n.getConst<BitVectorRepeat>().d_repeatAmount
428 : 463 : << ")";
429 : 463 : break;
430 : 8938 : case Kind::BITVECTOR_ZERO_EXTEND_OP:
431 : 8938 : out << "(_ zero_extend "
432 : 8938 : << n.getConst<BitVectorZeroExtend>().d_zeroExtendAmount << ")";
433 : 8938 : break;
434 : 12551 : case Kind::BITVECTOR_SIGN_EXTEND_OP:
435 : 12551 : out << "(_ sign_extend "
436 : 12551 : << n.getConst<BitVectorSignExtend>().d_signExtendAmount << ")";
437 : 12551 : break;
438 : 314 : case Kind::BITVECTOR_ROTATE_LEFT_OP:
439 : 314 : out << "(_ rotate_left "
440 : 314 : << n.getConst<BitVectorRotateLeft>().d_rotateLeftAmount << ")";
441 : 314 : break;
442 : 375 : case Kind::BITVECTOR_ROTATE_RIGHT_OP:
443 : 375 : out << "(_ rotate_right "
444 : 375 : << n.getConst<BitVectorRotateRight>().d_rotateRightAmount << ")";
445 : 375 : break;
446 : 798 : case Kind::INT_TO_BITVECTOR_OP:
447 : 798 : out << "(_ int_to_bv " << n.getConst<IntToBitVector>().d_size << ")";
448 : 798 : break;
449 : 200 : case Kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV_OP:
450 : 200 : out << "(_ to_fp "
451 : 200 : << n.getConst<FloatingPointToFPIEEEBitVector>()
452 : 200 : .getSize()
453 : 200 : .exponentWidth()
454 : 200 : << ' '
455 : 200 : << n.getConst<FloatingPointToFPIEEEBitVector>()
456 : 200 : .getSize()
457 : 200 : .significandWidth()
458 : 200 : << ")";
459 : 200 : break;
460 : 16 : case Kind::FLOATINGPOINT_TO_FP_FROM_FP_OP:
461 : 16 : out << "(_ to_fp "
462 : 16 : << n.getConst<FloatingPointToFPFloatingPoint>()
463 : 16 : .getSize()
464 : 16 : .exponentWidth()
465 : 16 : << ' '
466 : 16 : << n.getConst<FloatingPointToFPFloatingPoint>()
467 : 16 : .getSize()
468 : 16 : .significandWidth()
469 : 16 : << ")";
470 : 16 : break;
471 : 37 : case Kind::FLOATINGPOINT_TO_FP_FROM_REAL_OP:
472 : 37 : out << "(_ to_fp "
473 : 37 : << n.getConst<FloatingPointToFPReal>().getSize().exponentWidth()
474 : 37 : << ' '
475 : 37 : << n.getConst<FloatingPointToFPReal>().getSize().significandWidth()
476 : 37 : << ")";
477 : 37 : break;
478 : 7 : case Kind::FLOATINGPOINT_TO_FP_FROM_SBV_OP:
479 : 7 : out << "(_ to_fp "
480 : 7 : << n.getConst<FloatingPointToFPSignedBitVector>()
481 : 7 : .getSize()
482 : 7 : .exponentWidth()
483 : 7 : << ' '
484 : 7 : << n.getConst<FloatingPointToFPSignedBitVector>()
485 : 7 : .getSize()
486 : 7 : .significandWidth()
487 : 7 : << ")";
488 : 7 : break;
489 : 10 : case Kind::FLOATINGPOINT_TO_FP_FROM_UBV_OP:
490 : 10 : out << "(_ to_fp_unsigned "
491 : 10 : << n.getConst<FloatingPointToFPUnsignedBitVector>()
492 : 10 : .getSize()
493 : 10 : .exponentWidth()
494 : 10 : << ' '
495 : 10 : << n.getConst<FloatingPointToFPUnsignedBitVector>()
496 : 10 : .getSize()
497 : 10 : .significandWidth()
498 : 10 : << ")";
499 : 10 : break;
500 : 28 : case Kind::FLOATINGPOINT_TO_UBV_OP:
501 : 28 : out << "(_ fp.to_ubv "
502 : 28 : << n.getConst<FloatingPointToUBV>().d_bv_size.d_size << ")";
503 : 28 : break;
504 : 11 : case Kind::FLOATINGPOINT_TO_SBV_OP:
505 : 11 : out << "(_ fp.to_sbv "
506 : 11 : << n.getConst<FloatingPointToSBV>().d_bv_size.d_size << ")";
507 : 11 : break;
508 : 30 : case Kind::FLOATINGPOINT_TO_UBV_TOTAL_OP:
509 : 30 : out << "(_ fp.to_ubv_total "
510 : 30 : << n.getConst<FloatingPointToUBVTotal>().d_bv_size.d_size << ")";
511 : 30 : break;
512 : 12 : case Kind::FLOATINGPOINT_TO_SBV_TOTAL_OP:
513 : 12 : out << "(_ fp.to_sbv_total "
514 : 12 : << n.getConst<FloatingPointToSBVTotal>().d_bv_size.d_size << ")";
515 : 12 : break;
516 : 14 : case Kind::REGEXP_REPEAT_OP:
517 : 14 : out << "(_ re.^ " << n.getConst<RegExpRepeat>().d_repeatAmount << ")";
518 : 14 : break;
519 : 48 : case Kind::REGEXP_LOOP_OP:
520 : 48 : out << "(_ re.loop " << n.getConst<RegExpLoop>().d_loopMinOcc << " "
521 : 48 : << n.getConst<RegExpLoop>().d_loopMaxOcc << ")";
522 : 48 : break;
523 : 225 : case Kind::TUPLE_PROJECT_OP:
524 : : case Kind::TABLE_PROJECT_OP:
525 : : case Kind::TABLE_AGGREGATE_OP:
526 : : case Kind::TABLE_JOIN_OP:
527 : : case Kind::TABLE_GROUP_OP:
528 : : case Kind::RELATION_GROUP_OP:
529 : : case Kind::RELATION_AGGREGATE_OP:
530 : : case Kind::RELATION_PROJECT_OP:
531 : : case Kind::RELATION_TABLE_JOIN_OP:
532 : : {
533 : 225 : ProjectOp op = n.getConst<ProjectOp>();
534 : 225 : const std::vector<uint32_t>& indices = op.getIndices();
535 : 225 : Kind k = NodeManager::operatorToKind(n);
536 [ + + ]: 225 : if (indices.empty())
537 : : {
538 : 32 : out << smtKindString(k);
539 : : }
540 : : else
541 : : {
542 : 193 : out << "(_ " << smtKindString(k);
543 [ + + ]: 759 : for (uint32_t i : indices)
544 : : {
545 : 566 : out << " " << i;
546 : : }
547 : 193 : out << ")";
548 : : }
549 : 225 : }
550 : 225 : break;
551 : 542 : default:
552 : : // fall back on whatever operator<< does on underlying type; we
553 : : // might luck out and be SMT-LIB v2 compliant
554 : 542 : n.constToStream(out);
555 : : }
556 : :
557 : 5261604 : return true;
558 : : }
559 : :
560 : 34333435 : Kind k = n.getKind();
561 [ + + ][ + + ]: 34333435 : if (k == Kind::DATATYPE_TYPE || k == Kind::TUPLE_TYPE
562 [ + + ]: 34304842 : || k == Kind::NULLABLE_TYPE)
563 : : {
564 : 28889 : const DType& dt = n.getNodeManager()->getDTypeFor(n);
565 [ + + ]: 28889 : if (dt.isTuple())
566 : : {
567 : 2340 : unsigned int nargs = dt[0].getNumArgs();
568 [ + + ]: 2340 : if (nargs == 0)
569 : : {
570 : 18 : out << "UnitTuple";
571 : : }
572 : : else
573 : : {
574 : 2322 : out << "(Tuple";
575 [ + + ]: 7644 : for (unsigned int i = 0; i < nargs; i++)
576 : : {
577 : 5322 : out << " ";
578 : 5322 : toStreamType(out, dt[0][i].getRangeType());
579 : : }
580 : 2322 : out << ")";
581 : : }
582 : 2340 : return true;
583 : : }
584 [ + + ]: 26549 : if (dt.isNullable())
585 : : {
586 : 296 : out << "(Nullable " << dt[1][0].getRangeType() << ")";
587 : : }
588 : : else
589 : : {
590 : 26253 : out << cvc5::internal::quoteSymbol(dt.getName());
591 : : }
592 : 26549 : return true;
593 : : }
594 [ + + ]: 34304546 : else if (k == Kind::APPLY_TYPE_ASCRIPTION)
595 : : {
596 : 61 : TypeNode typeAsc = n.getOperator().getConst<AscriptionType>().getType();
597 : : // use type ascription
598 : 61 : out << "(as ";
599 [ - + ]: 61 : toStream(out, n[0], lbind, toDepth < 0 ? toDepth : toDepth - 1);
600 : 61 : out << " " << typeAsc << ")";
601 : 61 : return true;
602 : 61 : }
603 [ + + ]: 34304485 : else if (n.isVar())
604 : : {
605 : 22308866 : bool printed = false;
606 [ + + ]: 22308866 : if (k == Kind::SKOLEM)
607 : : {
608 : 6665 : SkolemManager* sm = nm->getSkolemManager();
609 : : SkolemId id;
610 : 6665 : Node cacheVal;
611 [ + - ]: 6665 : if (sm->isSkolemFunction(n, id, cacheVal))
612 : : {
613 [ + + ]: 6665 : if (id == SkolemId::INTERNAL)
614 : : {
615 [ + + ]: 171 : if (sm->isAbstractValue(n))
616 : : {
617 : : // abstract value
618 : 8 : std::string s = n.getName();
619 : 8 : out << "(as " << cvc5::internal::quoteSymbol(s) << " "
620 : 8 : << n.getType() << ")";
621 : 8 : printed = true;
622 : 8 : }
623 : : }
624 [ + + ]: 6494 : else if (options::ioutils::getPrintSkolemDefinitions(out))
625 : : {
626 : 3817 : toStreamSkolem(
627 : : out, cacheVal, id, /*isApplied=*/false, toDepth, lbind);
628 : 3817 : printed = true;
629 : : }
630 : : }
631 : 6665 : }
632 [ + + ]: 22308866 : if (!printed)
633 : : {
634 : : // variable
635 [ + + ]: 22305041 : if (n.hasName())
636 : : {
637 : 21999928 : std::string s = n.getName();
638 [ + + ]: 21999928 : if (k == Kind::RAW_SYMBOL)
639 : : {
640 : : // raw symbols are never quoted
641 : 4014150 : out << s;
642 : : }
643 : : else
644 : : {
645 : 17985778 : out << cvc5::internal::quoteSymbol(s);
646 : : }
647 : 21999928 : }
648 : : else
649 : : {
650 [ + + ]: 305113 : if (k == Kind::VARIABLE)
651 : : {
652 : 4 : out << "var_";
653 : : }
654 : : else
655 : : {
656 : 305109 : out << k << '_';
657 : : }
658 : 305113 : out << n.getId();
659 : : }
660 : : }
661 : 22308866 : return true;
662 : : }
663 [ + + ]: 11995619 : else if (k == Kind::APPLY_UF)
664 : : {
665 [ + + ]: 1394693 : if (!n.getOperator().isVar())
666 : : {
667 : : // Must print as HO apply instead. This ensures un-beta-reduced function
668 : : // applications can be reparsed.
669 : 3739 : Node hoa = theory::uf::TheoryUfRewriter::getHoApplyForApplyUf(n);
670 : 3739 : toStream(out, hoa, lbind, toDepth);
671 : 3739 : return true;
672 : 3739 : }
673 [ + + ]: 1390954 : else if (n.getOperator().getKind() == Kind::SKOLEM)
674 : : {
675 : 1113 : SkolemManager* sm = nm->getSkolemManager();
676 : : SkolemId id;
677 : 1113 : Node cacheVal;
678 [ + - ]: 1113 : if (sm->isSkolemFunction(n.getOperator(), id, cacheVal))
679 : : {
680 [ + + ]: 1113 : if (options::ioutils::getPrintSkolemDefinitions(out))
681 : : {
682 [ + - ]: 298 : if (n.getNumChildren() != 0)
683 : : {
684 : 298 : out << '(';
685 : : }
686 : 298 : toStreamSkolem(out, cacheVal, id, /*isApplied=*/true, toDepth, lbind);
687 : 298 : return false;
688 : : }
689 : : }
690 [ + + ]: 1113 : }
691 : : }
692 [ + + ]: 10600926 : else if (k == Kind::CONSTRUCTOR_TYPE)
693 : : {
694 : 61 : Node range = n[n.getNumChildren() - 1];
695 : 61 : toStream(out, range, lbind, toDepth);
696 : 61 : return true;
697 : 61 : }
698 [ + + ][ + + ]: 10600865 : else if (k == Kind::HO_APPLY && options::ioutils::getFlattenHOChains(out))
[ + + ]
699 : : {
700 : 301 : out << "(";
701 : : // collapse "@" chains, i.e.
702 : : //
703 : : // ((a b) c) --> (a b c)
704 : : //
705 : : // (((a b) ((c d) e)) f) --> (a b (c d e) f)
706 : : {
707 : 301 : Node head = n;
708 : 301 : std::vector<Node> args;
709 [ + + ]: 845 : while (head.getKind() == Kind::HO_APPLY)
710 : : {
711 : 544 : args.insert(args.begin(), head[1]);
712 : 544 : head = head[0];
713 : : }
714 : 301 : toStream(out, head, lbind, toDepth);
715 [ + + ]: 845 : for (unsigned i = 0, size = args.size(); i < size; ++i)
716 : : {
717 : 544 : out << " ";
718 : 544 : toStream(out, args[i], lbind, toDepth);
719 : : }
720 : 301 : out << ")";
721 : 301 : }
722 : 301 : return true;
723 : : }
724 [ + + ]: 10600564 : else if (k == Kind::MATCH)
725 : : {
726 : 34 : out << '(' << smtKindString(k) << " ";
727 : 34 : toStream(out, n[0], lbind, toDepth);
728 : 34 : out << " (";
729 [ + + ]: 108 : for (size_t i = 1, nchild = n.getNumChildren(); i < nchild; i++)
730 : : {
731 [ + + ]: 74 : if (i > 1)
732 : : {
733 : 40 : out << " ";
734 : : }
735 : 74 : toStream(out, n[i], lbind, toDepth);
736 : : }
737 : 34 : out << "))";
738 : 34 : return true;
739 : : }
740 [ + + ][ + + ]: 10600530 : else if (k == Kind::MATCH_BIND_CASE || k == Kind::MATCH_CASE)
741 : : {
742 : 78 : out << '(';
743 : : // ignore the binder for MATCH_BIND_CASE
744 [ + + ]: 78 : size_t patIndex = (k == Kind::MATCH_BIND_CASE ? 1 : 0);
745 : : // The pattern should be printed as a pattern (symbol applied to symbols),
746 : : // not as a term. In particular, this means we should not print any
747 : : // type ascriptions (if any).
748 [ + + ]: 78 : if (n[patIndex].getKind() == Kind::APPLY_CONSTRUCTOR)
749 : : {
750 [ + + ]: 73 : if (n[patIndex].getNumChildren() > 0)
751 : : {
752 : 41 : out << "(";
753 : : }
754 : 73 : Node op = n[patIndex].getOperator();
755 : 73 : const DType& dt = DType::datatypeOf(op);
756 : 73 : size_t index = DType::indexOf(op);
757 : 73 : out << dt[index].getConstructor();
758 [ + + ]: 135 : for (const Node& nc : n[patIndex])
759 : : {
760 : 62 : out << " ";
761 : 62 : toStream(out, nc, lbind, toDepth);
762 : 135 : }
763 [ + + ]: 73 : if (n[patIndex].getNumChildren() > 0)
764 : : {
765 : 41 : out << ")";
766 : : }
767 : 73 : }
768 : : else
769 : : {
770 : : // otherwise, a variable, just print
771 [ - + ][ - + ]: 5 : Assert(n[patIndex].isVar());
[ - - ]
772 : 5 : toStream(out, n[patIndex], lbind, toDepth);
773 : : }
774 : 78 : out << " ";
775 : 78 : toStream(out, n[patIndex + 1], lbind, toDepth);
776 : 78 : out << ")";
777 : 78 : return true;
778 : : }
779 [ + + ]: 10600452 : else if (k == Kind::BOUND_VAR_LIST)
780 : : {
781 : 142179 : out << '(';
782 [ + + ]: 411169 : for (TNode::iterator i = n.begin(), iend = n.end(); i != iend;)
783 : : {
784 : 268990 : out << '(';
785 [ - + ]: 268990 : toStream(out, *i, nullptr, toDepth < 0 ? toDepth : toDepth - 1);
786 : 268990 : out << ' ' << (*i).getType() << ')';
787 [ + + ]: 268990 : if (++i != iend)
788 : : {
789 : 126811 : out << ' ';
790 : : }
791 : : }
792 : 142179 : out << ')';
793 : 142179 : return true;
794 : : }
795 [ + + ]: 10458273 : else if (k == Kind::SET_UNIVERSE)
796 : : {
797 : 438 : out << "(as set.universe " << n.getType() << ")";
798 : 438 : return true;
799 : : }
800 [ + + ]: 10457835 : else if (k == Kind::SEP_NIL)
801 : : {
802 : 49 : out << "(as sep.nil " << n.getType() << ")";
803 : 49 : return true;
804 : : }
805 [ + + ][ + + ]: 10457786 : else if (k == Kind::FORALL || k == Kind::EXISTS || k == Kind::LAMBDA
[ + + ]
806 [ + + ]: 10330669 : || k == Kind::WITNESS)
807 : : {
808 : 127569 : out << '(' << smtKindString(k) << " ";
809 : : // do not letify the bound variable list
810 : 127569 : toStream(out, n[0], nullptr, toDepth);
811 : 127569 : out << " ";
812 : 127569 : bool needsPrintAnnot = false;
813 : 127569 : size_t dag = options::ioutils::getDagThresh(out);
814 [ - + ]: 127569 : size_t newDepth = (toDepth < 0 ? toDepth : toDepth - 1);
815 : 127569 : std::stringstream annot;
816 [ + + ]: 127569 : if (n.getNumChildren() == 3)
817 : : {
818 [ + + ]: 3758 : for (const Node& nc : n[2])
819 : : {
820 : 1929 : Kind nck = nc.getKind();
821 [ + + ]: 1929 : if (nck == Kind::INST_PATTERN)
822 : : {
823 : 1304 : needsPrintAnnot = true;
824 : 1304 : annot << " :pattern (";
825 [ + + ]: 2710 : for (size_t i = 0, nchild = nc.getNumChildren(); i < nchild; i++)
826 : : {
827 [ + + ]: 1406 : if (i > 0)
828 : : {
829 : 102 : annot << " ";
830 : : }
831 : 1406 : toStream(annot, nc[i], newDepth, dag);
832 : : }
833 : 1304 : annot << ")";
834 : : }
835 [ + + ]: 625 : else if (nck == Kind::INST_NO_PATTERN)
836 : : {
837 : 2 : needsPrintAnnot = true;
838 : 2 : annot << " :no-pattern ";
839 : 2 : toStream(annot, nc[0], newDepth, dag);
840 : : }
841 [ + + ][ + + ]: 623 : else if (nck == Kind::INST_POOL || nck == Kind::INST_ADD_TO_POOL
842 [ + + ]: 613 : || nck == Kind::SKOLEM_ADD_TO_POOL)
843 : : {
844 : 12 : needsPrintAnnot = true;
845 [ + + ][ + - ]: 12 : switch (nck)
846 : : {
847 : 6 : case Kind::INST_POOL: annot << " :pool"; break;
848 : 4 : case Kind::INST_ADD_TO_POOL: annot << " :inst-add-to-pool"; break;
849 : 2 : case Kind::SKOLEM_ADD_TO_POOL:
850 : 2 : annot << " :skolem-add-to-pool";
851 : 2 : break;
852 : 0 : default: break;
853 : : }
854 : 12 : annot << " (";
855 [ + + ]: 31 : for (size_t i = 0, nchild = nc.getNumChildren(); i < nchild; i++)
856 : : {
857 [ + + ]: 19 : if (i > 0)
858 : : {
859 : 7 : annot << " ";
860 : : }
861 : 19 : toStream(annot, nc[i], newDepth, dag);
862 : : }
863 : 12 : annot << ")";
864 : 12 : }
865 [ + - ]: 611 : else if (nck == Kind::INST_ATTRIBUTE)
866 : : {
867 : : // notice that INST_ATTRIBUTES either have an "internal" form,
868 : : // where the argument is a variable with an internal attribute set
869 : : // on it, or an "external" form where it is of the form
870 : : // (INST_ATTRIBUTE "keyword" [nodeValues]). We print the latter
871 : : // here only.
872 [ + + ]: 611 : if (nc[0].getKind() == Kind::CONST_STRING)
873 : : {
874 : 553 : needsPrintAnnot = true;
875 : : // print out as string to avoid quotes
876 : 553 : annot << " :" << nc[0].getConst<String>().toString();
877 [ + + ]: 1106 : for (size_t j = 1, nchild = nc.getNumChildren(); j < nchild; j++)
878 : : {
879 : 553 : annot << " ";
880 : 553 : toStream(annot, nc[j], newDepth, dag);
881 : : }
882 : : }
883 : : }
884 : 3758 : }
885 : : }
886 : : // Use a fresh let binder, since using existing let symbols may violate
887 : : // scoping issues for let-bound variables, see explanation in let_binding.h.
888 [ + + ]: 127569 : if (needsPrintAnnot)
889 : : {
890 : 1771 : out << "(! ";
891 : 1771 : annot << ")";
892 : : }
893 : 127569 : toStream(out, n[1], newDepth, dag);
894 : 127569 : out << annot.str() << ")";
895 : 127569 : return true;
896 : 127569 : }
897 : :
898 : 11720873 : bool stillNeedToPrintParams = true;
899 : 11720873 : bool printed = true;
900 : : // operator
901 [ + + ]: 11720873 : if (n.getNumChildren() != 0)
902 : : {
903 : 11713667 : out << '(';
904 : : }
905 [ + - ][ - + ]: 11720873 : switch (k)
[ + + ][ + + ]
[ + + ]
906 : : {
907 : 4 : case Kind::REAL_ALGEBRAIC_NUMBER:
908 : : {
909 : : const RealAlgebraicNumber& ran =
910 : 4 : n.getOperator().getConst<RealAlgebraicNumber>();
911 : 4 : out << "(_ real_algebraic_number " << ran << ")";
912 : 4 : stillNeedToPrintParams = false;
913 : 4 : break;
914 : : }
915 : 0 : case Kind::INDEXED_ROOT_PREDICATE_OP:
916 : : {
917 : 0 : const IndexedRootPredicate& irp = n.getConst<IndexedRootPredicate>();
918 : 0 : out << "(_ root_predicate " << irp.d_index << ")";
919 : 0 : stillNeedToPrintParams = false;
920 : 0 : break;
921 : : }
922 : 0 : case Kind::BITVECTOR_BIT:
923 : 0 : out << "(_ @bit " << n.getOperator().getConst<BitVectorBit>().d_bitIndex
924 : 0 : << ")";
925 : 0 : stillNeedToPrintParams = false;
926 : 0 : break;
927 : 8791 : case Kind::APPLY_CONSTRUCTOR:
928 : : {
929 : 8791 : const DType& dt = DType::datatypeOf(n.getOperator());
930 [ + + ]: 8791 : if (dt.isTuple())
931 : : {
932 : 2649 : stillNeedToPrintParams = false;
933 [ + + ]: 2649 : if (dt[0].getNumArgs() == 0)
934 : : {
935 : 16 : out << "tuple.unit";
936 : : }
937 : : else
938 : : {
939 : 2633 : out << "tuple";
940 : : }
941 : : }
942 [ + + ]: 8791 : if (dt.isNullable())
943 : : {
944 : 156 : stillNeedToPrintParams = false;
945 [ + + ]: 156 : if (n.getNumChildren() == 0)
946 : : {
947 : 94 : out << "(as nullable.null " << n.getType() << ")";
948 : : }
949 : : else
950 : : {
951 : 62 : out << "nullable.some";
952 : : }
953 : : }
954 : 8791 : break;
955 : : }
956 : 29835 : case Kind::APPLY_SELECTOR:
957 : : {
958 : 29835 : Node op = n.getOperator();
959 : 29835 : const DType& dt = DType::datatypeOf(op);
960 [ + + ]: 29835 : if (dt.isTuple())
961 : : {
962 : 492 : stillNeedToPrintParams = false;
963 : 492 : out << "(_ tuple.select " << DType::indexOf(op) << ")";
964 : : }
965 [ + + ]: 29343 : else if (dt.isNullable())
966 : : {
967 : 76 : stillNeedToPrintParams = false;
968 : 76 : out << "nullable.val";
969 : : }
970 : 29835 : }
971 : 29835 : break;
972 : 1059 : case Kind::APPLY_TESTER:
973 : : {
974 : 1059 : Node op = n.getOperator();
975 : 1059 : size_t cindex = DType::indexOf(op);
976 : 1059 : const DType& dt = DType::datatypeOf(op);
977 [ + + ]: 1059 : if (dt.isNullable())
978 : : {
979 : 19 : stillNeedToPrintParams = false;
980 [ + + ]: 19 : if (cindex == 0)
981 : : {
982 : 11 : out << "nullable.is_null";
983 : : }
984 : : else
985 : : {
986 : 8 : out << "nullable.is_some";
987 : : }
988 : : }
989 : : else
990 : : {
991 : 1040 : stillNeedToPrintParams = false;
992 : 1040 : out << "(_ is ";
993 [ - + ]: 2080 : toStream(out,
994 : 2080 : dt[cindex].getConstructor(),
995 : : lbind,
996 : : toDepth < 0 ? toDepth : toDepth - 1);
997 : 1040 : out << ")";
998 : : }
999 : 1059 : }
1000 : 1059 : break;
1001 : 52 : case Kind::APPLY_UPDATER:
1002 : : {
1003 : 52 : stillNeedToPrintParams = false;
1004 : 52 : Node op = n.getOperator();
1005 : 52 : size_t index = DType::indexOf(op);
1006 : 52 : const DType& dt = DType::datatypeOf(op);
1007 : 52 : size_t cindex = DType::cindexOf(op);
1008 [ + + ]: 52 : if (dt.isTuple())
1009 : : {
1010 : 10 : out << "(_ tuple.update " << index << ")";
1011 : : }
1012 : : else
1013 : : {
1014 : 42 : out << "(_ update ";
1015 [ - + ]: 84 : toStream(out,
1016 : 84 : dt[cindex][index].getSelector(),
1017 : : lbind,
1018 : : toDepth < 0 ? toDepth : toDepth - 1);
1019 : 42 : out << ")";
1020 : : }
1021 : 52 : }
1022 : 52 : break;
1023 : : // kinds that don't print their operator
1024 : 2632255 : case Kind::SEXPR:
1025 : : case Kind::INSTANTIATED_SORT_TYPE:
1026 : : case Kind::PARAMETRIC_DATATYPE:
1027 : : case Kind::INST_PATTERN:
1028 : : case Kind::INST_NO_PATTERN:
1029 : 2632255 : case Kind::INST_PATTERN_LIST: printed = false; break;
1030 : 56778 : case Kind::STRING_CONCAT:
1031 : : case Kind::STRING_LENGTH:
1032 : : case Kind::STRING_SUBSTR:
1033 : : case Kind::STRING_UPDATE:
1034 : : case Kind::STRING_CHARAT:
1035 : : case Kind::STRING_CONTAINS:
1036 : : case Kind::STRING_INDEXOF:
1037 : : case Kind::STRING_REPLACE:
1038 : : case Kind::STRING_REPLACE_ALL:
1039 : : case Kind::STRING_REV:
1040 : : case Kind::STRING_PREFIX:
1041 : : case Kind::STRING_SUFFIX:
1042 : : // maybe print seq. instead of str.
1043 : 56778 : out << smtKindStringOf(n);
1044 : 56778 : break;
1045 : 8992099 : default:
1046 : : // by default, print the kind using the smtKindString utility
1047 [ + + ]: 8992099 : if (n.getMetaKind() != kind::metakind::PARAMETERIZED)
1048 : : {
1049 : 7566193 : out << smtKindString(k);
1050 : : }
1051 : 8992099 : break;
1052 : : }
1053 : 11720873 : if (n.getMetaKind() == kind::metakind::PARAMETERIZED
1054 [ + + ][ + + ]: 11720873 : && stillNeedToPrintParams)
[ + + ]
1055 : : {
1056 [ + - ]: 1461159 : if (toDepth != 0)
1057 : : {
1058 [ - + ]: 2922318 : toStream(
1059 : 2922318 : out, n.getOperator(), lbind, toDepth < 0 ? toDepth : toDepth - 1);
1060 : : }
1061 : : else
1062 : : {
1063 : 0 : out << "(...)";
1064 : : }
1065 : : }
1066 : : // finished if we have no children
1067 [ + + ]: 11720873 : if (n.getNumChildren() == 0)
1068 : : {
1069 : 7206 : return true;
1070 : : }
1071 [ + + ]: 11713667 : if (printed)
1072 : : {
1073 : : // if printed anything, now add a space
1074 : 9081412 : out << ' ';
1075 : : }
1076 : 11713667 : return false;
1077 : : }
1078 : :
1079 : 18544593 : void Smt2Printer::toStream(std::ostream& out,
1080 : : TNode n,
1081 : : const LetBinding* lbind,
1082 : : int toDepth,
1083 : : bool lbindTop) const
1084 : : {
1085 : 18544593 : std::vector<std::tuple<TNode, size_t, int>> visit;
1086 : 18544593 : TNode cur;
1087 : : size_t curChild;
1088 : : int cdepth;
1089 : 18544593 : visit.emplace_back(n, 0, toDepth);
1090 : : do
1091 : : {
1092 : 81222267 : cur = std::get<0>(visit.back());
1093 : 81222267 : curChild = std::get<1>(visit.back());
1094 : 81222267 : cdepth = std::get<2>(visit.back());
1095 [ + + ]: 81222267 : if (curChild == 0)
1096 : : {
1097 [ + + ]: 49883430 : if (lbind != nullptr)
1098 : : {
1099 [ + + ]: 28175986 : if (lbindTop)
1100 : : {
1101 : : // see if its letified
1102 : 26846110 : uint32_t lid = lbind->getId(cur);
1103 [ + + ]: 26846110 : if (lid != 0)
1104 : : {
1105 : 10288377 : out << lbind->getPrefix() << lid;
1106 : 10288377 : visit.pop_back();
1107 : 10288377 : continue;
1108 : : }
1109 : : }
1110 : : else
1111 : : {
1112 : 1329876 : lbindTop = true;
1113 : : }
1114 : : }
1115 : : // print the operator
1116 : : // if printed as standalone, we are done
1117 [ + + ]: 39595053 : if (toStreamBase(out, cur, lbind, cdepth))
1118 : : {
1119 : 27881088 : visit.pop_back();
1120 : 27881088 : continue;
1121 : : }
1122 [ - + ]: 11713965 : else if (cdepth == 0)
1123 : : {
1124 : 0 : visit.pop_back();
1125 : 0 : out << "(...)";
1126 [ - - ]: 0 : if (cur.getNumChildren() > 0)
1127 : : {
1128 : 0 : out << ')';
1129 : : }
1130 : 0 : continue;
1131 : : }
1132 : : }
1133 [ + + ]: 43052802 : if (curChild < cur.getNumChildren())
1134 : : {
1135 : 31338837 : std::get<1>(visit.back())++;
1136 : : // toStreamBase akready adds space, skip adding space before first child
1137 [ + + ]: 31338837 : if (curChild > 0)
1138 : : {
1139 : 19624872 : out << ' ';
1140 : : }
1141 [ - + ]: 31338837 : visit.emplace_back(cur[curChild], 0, cdepth < 0 ? cdepth : cdepth - 1);
1142 : : }
1143 : : else
1144 : : {
1145 [ - + ][ - + ]: 11713965 : Assert(cur.getNumChildren() > 0);
[ - - ]
1146 : 11713965 : out << ')';
1147 : 11713965 : visit.pop_back();
1148 : : }
1149 [ + + ]: 81222267 : } while (!visit.empty());
1150 : 18544593 : }
1151 : :
1152 : 8679796 : std::string Smt2Printer::smtKindString(Kind k)
1153 : : {
1154 [ + + ][ + - ]: 8679796 : switch (k)
[ - + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ - - ]
[ - + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ - - ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + - ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ - + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ - + ][ + + ]
[ + - ][ - - ]
[ - + ][ + + ]
[ + + ][ + + ]
[ + - ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ - + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ - + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + ]
1155 : : {
1156 : : // builtin theory
1157 : 10853 : case Kind::FUNCTION_TYPE: return "->";
1158 : 2439235 : case Kind::EQUAL: return "=";
1159 : 26076 : 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 : 1106172 : case Kind::NOT: return "not";
1166 : 905485 : case Kind::AND: return "and";
1167 : 185787 : case Kind::IMPLIES: return "=>";
1168 : 1518346 : case Kind::OR: return "or";
1169 : 43044 : case Kind::XOR: return "xor";
1170 : 247650 : case Kind::ITE: return "ite";
1171 : :
1172 : : // uf theory
1173 : 520 : case Kind::APPLY_UF: break;
1174 : :
1175 : 8705 : case Kind::LAMBDA: return "lambda";
1176 : 36 : case Kind::MATCH: return "match";
1177 : 466 : case Kind::WITNESS: return "witness";
1178 : :
1179 : : // arith theory
1180 : 365956 : case Kind::ADD: return "+";
1181 : 290176 : case Kind::MULT:
1182 : 290176 : case Kind::NONLINEAR_MULT: return "*";
1183 : 97 : case Kind::IAND: return "iand";
1184 : 109 : case Kind::PIAND: return "piand";
1185 : 383 : case Kind::POW2: return "int.pow2";
1186 : 585 : case Kind::EXPONENTIAL: return "exp";
1187 : 628 : 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 : 1660 : case Kind::PI: return "real.pi";
1200 : 60 : case Kind::SQRT: return "sqrt";
1201 : 69373 : case Kind::SUB: return "-";
1202 : 34470 : case Kind::NEG: return "-";
1203 : 51998 : case Kind::LT: return "<";
1204 : 88966 : case Kind::LEQ: return "<=";
1205 : 17520 : case Kind::GT: return ">";
1206 : 245057 : case Kind::GEQ: return ">=";
1207 : 3304 : case Kind::DIVISION: return "/";
1208 : 370 : case Kind::DIVISION_TOTAL: return "/_total";
1209 : 2441 : case Kind::INTS_DIVISION: return "div";
1210 : 1059 : case Kind::INTS_DIVISION_TOTAL: return "div_total";
1211 : 2813 : case Kind::INTS_MODULUS: return "mod";
1212 : 957 : 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 : 1848 : case Kind::ABS: return "abs";
1216 : 196 : case Kind::IS_INTEGER: return "is_int";
1217 : 516 : case Kind::TO_INTEGER: return "to_int";
1218 : 8429 : 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 : 17258 : case Kind::SELECT: return "select";
1224 : 6483 : case Kind::STORE: return "store";
1225 : 15495 : case Kind::ARRAY_TYPE: return "Array";
1226 : 23 : case Kind::EQ_RANGE: return "eqrange";
1227 : :
1228 : : // ff theory
1229 : 1169 : case Kind::FINITE_FIELD_ADD: return "ff.add";
1230 : 59 : case Kind::FINITE_FIELD_BITSUM: return "ff.bitsum";
1231 : 1440 : case Kind::FINITE_FIELD_MULT: return "ff.mul";
1232 : 183 : case Kind::FINITE_FIELD_NEG: return "ff.neg";
1233 : :
1234 : : // bv theory
1235 : 27784 : case Kind::BITVECTOR_CONCAT: return "concat";
1236 : 10596 : case Kind::BITVECTOR_AND: return "bvand";
1237 : 5935 : case Kind::BITVECTOR_OR: return "bvor";
1238 : 4785 : case Kind::BITVECTOR_XOR: return "bvxor";
1239 : 6008 : case Kind::BITVECTOR_NOT: return "bvnot";
1240 : 499 : case Kind::BITVECTOR_NAND: return "bvnand";
1241 : 639 : case Kind::BITVECTOR_NOR: return "bvnor";
1242 : 738 : case Kind::BITVECTOR_XNOR: return "bvxnor";
1243 : 3725 : case Kind::BITVECTOR_COMP: return "bvcomp";
1244 : 11622 : case Kind::BITVECTOR_MULT: return "bvmul";
1245 : 18232 : case Kind::BITVECTOR_ADD: return "bvadd";
1246 : 6221 : case Kind::BITVECTOR_SUB: return "bvsub";
1247 : 3733 : case Kind::BITVECTOR_NEG: return "bvneg";
1248 : 660 : case Kind::BITVECTOR_UDIV: return "bvudiv";
1249 : 479 : case Kind::BITVECTOR_UREM: return "bvurem";
1250 : 230 : case Kind::BITVECTOR_SDIV: return "bvsdiv";
1251 : 121 : case Kind::BITVECTOR_SREM: return "bvsrem";
1252 : 98 : case Kind::BITVECTOR_SMOD: return "bvsmod";
1253 : 1974 : case Kind::BITVECTOR_SHL: return "bvshl";
1254 : 2004 : case Kind::BITVECTOR_LSHR: return "bvlshr";
1255 : 1780 : case Kind::BITVECTOR_ASHR: return "bvashr";
1256 : 12819 : case Kind::BITVECTOR_ULT: return "bvult";
1257 : 4410 : case Kind::BITVECTOR_ULE: return "bvule";
1258 : 4124 : case Kind::BITVECTOR_UGT: return "bvugt";
1259 : 3946 : case Kind::BITVECTOR_UGE: return "bvuge";
1260 : 15424 : case Kind::BITVECTOR_SLT: return "bvslt";
1261 : 4496 : case Kind::BITVECTOR_SLE: return "bvsle";
1262 : 4480 : case Kind::BITVECTOR_SGT: return "bvsgt";
1263 : 4610 : 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 : 2444 : 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 : 9674 : case Kind::BITVECTOR_EXTRACT: return "extract";
1278 : 383 : case Kind::BITVECTOR_REPEAT: return "repeat";
1279 : 5106 : case Kind::BITVECTOR_ZERO_EXTEND: return "zero_extend";
1280 : 8226 : case Kind::BITVECTOR_SIGN_EXTEND: return "sign_extend";
1281 : 260 : case Kind::BITVECTOR_ROTATE_LEFT: return "rotate_left";
1282 : 267 : case Kind::BITVECTOR_ROTATE_RIGHT: return "rotate_right";
1283 : 105 : case Kind::INT_TO_BITVECTOR: return "int_to_bv";
1284 : 372 : case Kind::BITVECTOR_ITE: return "bvite";
1285 : 9 : case Kind::BITVECTOR_ULTBV: return "bvultbv";
1286 : 69 : case Kind::BITVECTOR_SLTBV: return "bvsltbv";
1287 : :
1288 : 4697 : case Kind::BITVECTOR_FROM_BOOLS: return "@from_bools";
1289 : 4418 : case Kind::BITVECTOR_BIT: return "@bit";
1290 : 719 : case Kind::BITVECTOR_SIZE: return "@bvsize";
1291 : 684 : case Kind::CONST_BITVECTOR_SYMBOLIC: return "@bv";
1292 : :
1293 : : // datatypes theory
1294 : 914 : 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 : 16 : case Kind::SET_UNIVERSE: return "set.universe";
1304 : 1642 : case Kind::SET_UNION: return "set.union";
1305 : 689 : case Kind::SET_INTER: return "set.inter";
1306 : 623 : case Kind::SET_MINUS: return "set.minus";
1307 : 174 : case Kind::SET_SUBSET: return "set.subset";
1308 : 6530 : case Kind::SET_MEMBER: return "set.member";
1309 : 18094 : case Kind::SET_TYPE: return "Set";
1310 : 1782 : 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 : 1706 : 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 : 44 : 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 : 659 : 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 : 6 : 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 : 20 : 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 : 27 : case Kind::FLOATINGPOINT_DIV: return "fp.div";
1372 : 11 : case Kind::FLOATINGPOINT_FMA: return "fp.fma";
1373 : 10 : case Kind::FLOATINGPOINT_SQRT: return "fp.sqrt";
1374 : 16 : 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 : 192 : case Kind::FLOATINGPOINT_LEQ: return "fp.leq";
1382 : 74 : case Kind::FLOATINGPOINT_LT: return "fp.lt";
1383 : 34 : case Kind::FLOATINGPOINT_GEQ: return "fp.geq";
1384 : 10 : case Kind::FLOATINGPOINT_GT: return "fp.gt";
1385 : :
1386 : 6 : case Kind::FLOATINGPOINT_IS_NORMAL: return "fp.isNormal";
1387 : 18 : case Kind::FLOATINGPOINT_IS_SUBNORMAL: return "fp.isSubnormal";
1388 : 22 : case Kind::FLOATINGPOINT_IS_ZERO: return "fp.isZero";
1389 : 7 : case Kind::FLOATINGPOINT_IS_INF: return "fp.isInfinite";
1390 : 70 : 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 : 15 : 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 : 35143 : case Kind::STRING_CONCAT: return "str.++";
1416 : 16061 : case Kind::STRING_LENGTH: return "str.len";
1417 : 10003 : case Kind::STRING_SUBSTR: return "str.substr";
1418 : 164 : case Kind::STRING_UPDATE: return "str.update";
1419 : 3285 : case Kind::STRING_CONTAINS: return "str.contains";
1420 : 250 : case Kind::STRING_CHARAT: return "str.at";
1421 : 1350 : case Kind::STRING_INDEXOF: return "str.indexof";
1422 : 159 : case Kind::STRING_INDEXOF_RE: return "str.indexof_re";
1423 : 2458 : case Kind::STRING_REPLACE: return "str.replace";
1424 : 301 : 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 : 825 : case Kind::STRING_TO_CODE: return "str.to_code";
1436 : 41 : case Kind::STRING_IS_DIGIT: return "str.is_digit";
1437 : 280 : case Kind::STRING_ITOS: return "str.from_int";
1438 : 344 : case Kind::STRING_STOI: return "str.to_int";
1439 : 3093 : case Kind::STRING_IN_REGEXP: return "str.in_re";
1440 : 2814 : case Kind::STRING_TO_REGEXP: return "str.to_re";
1441 : 0 : case Kind::STRING_UNIT: return "str.unit";
1442 : 425 : case Kind::REGEXP_NONE: return "re.none";
1443 : 186 : case Kind::REGEXP_ALL: return "re.all";
1444 : 1415 : case Kind::REGEXP_ALLCHAR: return "re.allchar";
1445 : 2459 : case Kind::REGEXP_CONCAT: return "re.++";
1446 : 983 : case Kind::REGEXP_UNION: return "re.union";
1447 : 211 : case Kind::REGEXP_INTER: return "re.inter";
1448 : 1579 : case Kind::REGEXP_STAR: return "re.*";
1449 : 189 : case Kind::REGEXP_PLUS: return "re.+";
1450 : 74 : case Kind::REGEXP_OPT: return "re.opt";
1451 : 742 : 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 : 209 : case Kind::REGEXP_COMPLEMENT: return "re.comp";
1455 : 74 : case Kind::REGEXP_DIFF: return "re.diff";
1456 : 50414 : case Kind::SEQUENCE_TYPE: return "Seq";
1457 : 1150 : 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 : 186597 : case Kind::FORALL: return "forall";
1471 : 5733 : case Kind::EXISTS: return "exists";
1472 : :
1473 : : // HO
1474 : 15893 : case Kind::HO_APPLY: return "@";
1475 : :
1476 : 370306 : 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 : 370306 : return kind::kindToString(k);
1484 : : }
1485 : :
1486 : 56778 : std::string Smt2Printer::smtKindStringOf(const Node& n)
1487 : : {
1488 : 56778 : Kind k = n.getKind();
1489 : 56778 : if (n.getNumChildren() > 0 && n[0].getType().isSequence())
1490 : : {
1491 : : // this method parallels cvc5::Term::getKind
1492 [ + + ][ + + ]: 3736 : switch (k)
[ + + ][ + + ]
[ + + ][ + + ]
[ - ]
1493 : : {
1494 : 1133 : case Kind::STRING_CONCAT: return "seq.++";
1495 : 1445 : case Kind::STRING_LENGTH: return "seq.len";
1496 : 643 : 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 : 78 : 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 : 9 : 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 : 53042 : return smtKindString(k);
1513 : : }
1514 : :
1515 : 79496 : void Smt2Printer::toStreamDeclareType(std::ostream& out,
1516 : : const std::vector<TypeNode>& argTypes,
1517 : : TypeNode tn) const
1518 : : {
1519 : 79496 : out << "(";
1520 [ + + ]: 79496 : if (!argTypes.empty())
1521 : : {
1522 : 6040 : copy(argTypes.begin(),
1523 : 6040 : argTypes.end() - 1,
1524 : 6040 : ostream_iterator<TypeNode>(out, " "));
1525 : 6040 : out << argTypes.back();
1526 : : }
1527 : 79496 : out << ") " << tn;
1528 : 79496 : }
1529 : :
1530 : 7318 : void Smt2Printer::toStreamType(std::ostream& out, TypeNode tn) const
1531 : : {
1532 : : // we currently must call TypeNode::toStream here.
1533 : 7318 : tn.toStream(out);
1534 : 7318 : }
1535 : :
1536 : 51 : void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core) const
1537 : : {
1538 : 51 : out << "(" << std::endl;
1539 [ + + ]: 51 : if (core.useNames())
1540 : : {
1541 : : // use the names
1542 : 35 : const std::vector<std::string>& cnames = core.getCoreNames();
1543 [ + + ]: 78 : 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 : 51 : out << ")" << endl;
1557 : 51 : } /* Smt2Printer::toStream(UnsatCore, map<Expr, string>) */
1558 : :
1559 : 241 : void Smt2Printer::toStream(std::ostream& out, const smt::Model& m) const
1560 : : {
1561 : : // print the model
1562 : 241 : out << "(" << endl;
1563 : : // don't need to print approximations since they are built into choice
1564 : : // functions in the values of variables.
1565 : 241 : this->Printer::toStream(out, m);
1566 : 241 : out << ")" << endl;
1567 : : // print the heap model, if it exists
1568 : 241 : Node h, neq;
1569 [ + + ]: 241 : 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 : 241 : }
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 : 6 : const UninterpretedSortValue& av = trn.getConst<UninterpretedSortValue>();
1603 : 6 : out << "(" << cvc5::internal::quoteSymbol(av.getSymbol()) << ")";
1604 : 6 : }
1605 : 2 : out << "))" << std::endl;
1606 : 2 : return;
1607 : : }
1608 : : // print the cardinality
1609 : 198 : out << "; cardinality of " << tn << " is " << elements.size() << endl;
1610 [ - + ]: 198 : if (modelUninterpPrint == options::ModelUninterpPrintMode::DeclSortAndFun)
1611 : : {
1612 : 0 : Printer::toStreamCmdDeclareType(out, tn);
1613 : 0 : out << std::endl;
1614 : : }
1615 : : // print the representatives
1616 [ + + ]: 588 : for (const Node& trn : elements)
1617 : : {
1618 [ + - ]: 390 : if (modelUninterpPrint == options::ModelUninterpPrintMode::DeclSortAndFun
1619 [ + + ]: 390 : || modelUninterpPrint == options::ModelUninterpPrintMode::DeclFun)
1620 : : {
1621 : 2 : out << "(declare-fun ";
1622 [ + - ]: 2 : if (trn.getKind() == Kind::UNINTERPRETED_SORT_VALUE)
1623 : : {
1624 : : // prints as raw symbol
1625 : : const UninterpretedSortValue& av =
1626 : 2 : trn.getConst<UninterpretedSortValue>();
1627 : 2 : out << cvc5::internal::quoteSymbol(av.getSymbol());
1628 : : }
1629 : : else
1630 : : {
1631 : 0 : DebugUnhandled()
1632 : 0 : << "model domain element is not an uninterpreted sort value: "
1633 : : << trn;
1634 : : out << trn;
1635 : : }
1636 : 2 : out << " () " << tn << ")" << endl;
1637 : 2 : }
1638 : : else
1639 : : {
1640 : 388 : out << "; rep: " << trn << endl;
1641 : : }
1642 : : }
1643 : : }
1644 : :
1645 : 447 : void Smt2Printer::toStreamModelTerm(std::ostream& out,
1646 : : const Node& n,
1647 : : const Node& value) const
1648 : : {
1649 [ + + ]: 447 : if (value.getKind() == Kind::LAMBDA)
1650 : : {
1651 : 13 : TypeNode rangeType = n.getType().getRangeType();
1652 : 13 : out << "(define-fun " << n << " " << value[0] << " " << rangeType << " ";
1653 : 13 : toStream(out, value[1]);
1654 : 13 : out << ")" << endl;
1655 : 13 : }
1656 : : else
1657 : : {
1658 : 434 : out << "(define-fun " << n << " () " << n.getType() << " ";
1659 : 434 : toStream(out, value);
1660 : 434 : out << ")" << endl;
1661 : : }
1662 : 447 : }
1663 : :
1664 : 23 : void Smt2Printer::toStreamCmdSuccess(std::ostream& out) const
1665 : : {
1666 : 23 : out << "success" << endl;
1667 : 23 : }
1668 : :
1669 : 0 : void Smt2Printer::toStreamCmdInterrupted(std::ostream& out) const
1670 : : {
1671 : 0 : out << "interrupted" << endl;
1672 : 0 : }
1673 : :
1674 : 6 : void Smt2Printer::toStreamCmdUnsupported(std::ostream& out) const
1675 : : {
1676 : : #ifdef CVC5_COMPETITION_MODE
1677 : : // if in competition mode, lie and say we're ok
1678 : : // (we have nothing to lose by saying success, and everything to lose
1679 : : // if we say "unsupported")
1680 : : out << "success" << endl;
1681 : : #else /* CVC5_COMPETITION_MODE */
1682 : 6 : out << "unsupported" << endl;
1683 : : #endif /* CVC5_COMPETITION_MODE */
1684 : 6 : }
1685 : :
1686 : 123 : static void errorToStream(std::ostream& out, std::string message)
1687 : : {
1688 : 123 : out << "(error " << cvc5::internal::quoteString(message) << ')' << endl;
1689 : 123 : }
1690 : :
1691 : 87 : void Smt2Printer::toStreamCmdFailure(std::ostream& out,
1692 : : const std::string& message) const
1693 : : {
1694 : 87 : errorToStream(out, message);
1695 : 87 : }
1696 : :
1697 : 36 : void Smt2Printer::toStreamCmdRecoverableFailure(
1698 : : std::ostream& out, const std::string& message) const
1699 : : {
1700 : 36 : errorToStream(out, message);
1701 : 36 : }
1702 : :
1703 : 36108 : void Smt2Printer::toStreamCmdAssert(std::ostream& out, Node n) const
1704 : : {
1705 : 36108 : out << "(assert " << n << ')';
1706 : 36108 : }
1707 : :
1708 : 1031 : void Smt2Printer::toStreamCmdPush(std::ostream& out, uint32_t nscopes) const
1709 : : {
1710 : 1031 : out << "(push " << nscopes << ")";
1711 : 1031 : }
1712 : :
1713 : 821 : void Smt2Printer::toStreamCmdPop(std::ostream& out, uint32_t nscopes) const
1714 : : {
1715 : 821 : out << "(pop " << nscopes << ")";
1716 : 821 : }
1717 : :
1718 : 4674 : void Smt2Printer::toStreamCmdCheckSat(std::ostream& out) const
1719 : : {
1720 : 4674 : out << "(check-sat)";
1721 : 4674 : }
1722 : :
1723 : 673 : void Smt2Printer::toStreamCmdCheckSatAssuming(
1724 : : std::ostream& out, const std::vector<Node>& nodes) const
1725 : : {
1726 : 673 : out << "(check-sat-assuming ( ";
1727 : 673 : copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, " "));
1728 : 673 : out << "))";
1729 : 673 : }
1730 : :
1731 : 0 : void Smt2Printer::toStreamCmdQuery(std::ostream& out, Node n) const
1732 : : {
1733 [ - - ]: 0 : if (!n.isNull())
1734 : : {
1735 : 0 : toStreamCmdCheckSatAssuming(out, {n});
1736 : : }
1737 : : else
1738 : : {
1739 : 0 : toStreamCmdCheckSat(out);
1740 : : }
1741 : 0 : }
1742 : :
1743 : 17 : void Smt2Printer::toStreamCmdReset(std::ostream& out) const
1744 : : {
1745 : 17 : out << "(reset)";
1746 : 17 : }
1747 : :
1748 : 13 : void Smt2Printer::toStreamCmdResetAssertions(std::ostream& out) const
1749 : : {
1750 : 13 : out << "(reset-assertions)";
1751 : 13 : }
1752 : :
1753 : 466 : void Smt2Printer::toStreamCmdQuit(std::ostream& out) const { out << "(exit)"; }
1754 : :
1755 : 96648 : void Smt2Printer::toStreamCmdDeclareFunction(
1756 : : std::ostream& out,
1757 : : const std::string& id,
1758 : : const std::vector<TypeNode>& argTypes,
1759 : : TypeNode type) const
1760 : : {
1761 [ + + ]: 96648 : if (d_variant == Variant::eo_variant)
1762 : : {
1763 : 17152 : out << "(declare-const " << cvc5::internal::quoteSymbol(id);
1764 [ + + ]: 17152 : if (!argTypes.empty())
1765 : : {
1766 : 4107 : out << " (->";
1767 [ + + ]: 11446 : for (const TypeNode& tn : argTypes)
1768 : : {
1769 : 7339 : out << " " << tn;
1770 : : }
1771 : : }
1772 : 17152 : out << " " << type;
1773 [ + + ]: 17152 : if (!argTypes.empty())
1774 : : {
1775 : 4107 : out << ')';
1776 : : }
1777 : 17152 : out << ')';
1778 : 17152 : return;
1779 : : }
1780 : 79496 : out << "(declare-fun " << cvc5::internal::quoteSymbol(id) << " ";
1781 : 79496 : toStreamDeclareType(out, argTypes, type);
1782 : 79496 : out << ')';
1783 : : }
1784 : :
1785 : 0 : void Smt2Printer::toStreamCmdDeclareOracleFun(
1786 : : std::ostream& out,
1787 : : const std::string& id,
1788 : : const std::vector<TypeNode>& argTypes,
1789 : : TypeNode type,
1790 : : const std::string& binName) const
1791 : : {
1792 : 0 : out << "(declare-oracle-fun " << cvc5::internal::quoteSymbol(id) << " ";
1793 : 0 : toStreamDeclareType(out, argTypes, type);
1794 : 0 : out << " " << binName << ")";
1795 : 0 : }
1796 : :
1797 : 4 : void Smt2Printer::toStreamCmdDeclarePool(
1798 : : std::ostream& out,
1799 : : const std::string& id,
1800 : : TypeNode type,
1801 : : const std::vector<Node>& initValue) const
1802 : : {
1803 : 8 : out << "(declare-pool " << cvc5::internal::quoteSymbol(id) << ' ' << type
1804 : 4 : << " (";
1805 [ + + ]: 9 : for (size_t i = 0, n = initValue.size(); i < n; ++i)
1806 : : {
1807 [ + + ]: 5 : if (i != 0)
1808 : : {
1809 : 3 : out << ' ';
1810 : : }
1811 : 5 : out << initValue[i];
1812 : : }
1813 : 4 : out << "))";
1814 : 4 : }
1815 : :
1816 : 1914 : void Smt2Printer::toStreamCmdDefineFunction(std::ostream& out,
1817 : : const std::string& id,
1818 : : const std::vector<Node>& formals,
1819 : : TypeNode range,
1820 : : Node formula) const
1821 : : {
1822 [ + + ]: 1914 : if (d_variant == Variant::eo_variant)
1823 : : {
1824 : 558 : out << "(define " << cvc5::internal::quoteSymbol(id) << " ";
1825 : 558 : toStreamSortedVarList(out, formals);
1826 : 558 : out << " " << formula << ')';
1827 : 558 : return;
1828 : : }
1829 : 1356 : out << "(define-fun " << cvc5::internal::quoteSymbol(id) << " ";
1830 : 1356 : toStreamSortedVarList(out, formals);
1831 : 1356 : out << " " << range << ' ' << formula << ')';
1832 : : }
1833 : :
1834 : 120 : void Smt2Printer::toStreamCmdDefineFunctionRec(
1835 : : std::ostream& out,
1836 : : const std::vector<Node>& funcs,
1837 : : const std::vector<std::vector<Node>>& formals,
1838 : : const std::vector<Node>& formulas) const
1839 : : {
1840 : 120 : out << "(define-fun";
1841 [ + + ]: 120 : if (funcs.size() > 1)
1842 : : {
1843 : 9 : out << "s";
1844 : : }
1845 : 120 : out << "-rec ";
1846 [ + + ]: 120 : if (funcs.size() > 1)
1847 : : {
1848 : 9 : out << "(";
1849 : : }
1850 [ + + ]: 269 : for (unsigned i = 0, size = funcs.size(); i < size; i++)
1851 : : {
1852 [ + + ]: 149 : if (funcs.size() > 1)
1853 : : {
1854 [ + + ]: 38 : if (i > 0)
1855 : : {
1856 : 29 : out << " ";
1857 : : }
1858 : 38 : out << "(";
1859 : : }
1860 : 149 : out << funcs[i] << " ";
1861 : : // print its type signature
1862 : 149 : toStreamSortedVarList(out, formals[i]);
1863 : 149 : TypeNode type = funcs[i].getType();
1864 [ + + ]: 149 : if (type.isFunction())
1865 : : {
1866 : 141 : type = type.getRangeType();
1867 : : }
1868 : 149 : out << " " << type;
1869 [ + + ]: 149 : if (funcs.size() > 1)
1870 : : {
1871 : 38 : out << ")";
1872 : : }
1873 : 149 : }
1874 [ + + ]: 120 : if (funcs.size() > 1)
1875 : : {
1876 : 9 : out << ") (";
1877 : : }
1878 : : else
1879 : : {
1880 : 111 : out << " ";
1881 : : }
1882 [ + + ]: 269 : for (unsigned i = 0, size = formulas.size(); i < size; i++)
1883 : : {
1884 [ + + ]: 149 : if (i > 0)
1885 : : {
1886 : 29 : out << " ";
1887 : : }
1888 : 149 : out << formulas[i];
1889 : : }
1890 [ + + ]: 120 : if (funcs.size() > 1)
1891 : : {
1892 : 9 : out << ")";
1893 : : }
1894 : 120 : out << ")";
1895 : 120 : }
1896 : :
1897 : 2466 : void Smt2Printer::toStreamSortedVarList(std::ostream& out,
1898 : : const std::vector<Node>& vars) const
1899 : : {
1900 : 2466 : out << "(";
1901 [ + + ]: 6177 : for (size_t i = 0, nvars = vars.size(); i < nvars; i++)
1902 : : {
1903 : 3711 : out << "(" << vars[i] << " " << vars[i].getType() << ")";
1904 [ + + ]: 3711 : if (i + 1 < nvars)
1905 : : {
1906 : 2376 : out << " ";
1907 : : }
1908 : : }
1909 : 2466 : out << ")";
1910 : 2466 : }
1911 : :
1912 : 2980 : void Smt2Printer::toStreamCmdDeclareType(std::ostream& out,
1913 : : const std::string& id,
1914 : : size_t arity) const
1915 : : {
1916 : 5960 : out << "(declare-sort " << cvc5::internal::quoteSymbol(id) << " " << arity
1917 : 2980 : << ")";
1918 : 2980 : }
1919 : :
1920 : 128 : void Smt2Printer::toStreamCmdDefineType(std::ostream& out,
1921 : : const std::string& id,
1922 : : const std::vector<TypeNode>& params,
1923 : : TypeNode t) const
1924 : : {
1925 : 128 : out << "(define-sort " << cvc5::internal::quoteSymbol(id) << " (";
1926 [ + + ]: 128 : if (params.size() > 0)
1927 : : {
1928 : 1 : copy(
1929 : 1 : params.begin(), params.end() - 1, ostream_iterator<TypeNode>(out, " "));
1930 : 1 : out << params.back();
1931 : : }
1932 : 128 : out << ") " << t << ")";
1933 : 128 : }
1934 : :
1935 : 0 : void Smt2Printer::toStreamCmdSimplify(std::ostream& out, Node n) const
1936 : : {
1937 : 0 : out << "(simplify " << n << ')';
1938 : 0 : }
1939 : :
1940 : 52 : void Smt2Printer::toStreamCmdGetValue(std::ostream& out,
1941 : : const std::vector<Node>& nodes) const
1942 : : {
1943 : 52 : out << "(get-value ( ";
1944 : 52 : copy(nodes.begin(), nodes.end(), ostream_iterator<Node>(out, " "));
1945 : 52 : out << "))";
1946 : 52 : }
1947 : :
1948 : 1 : void Smt2Printer::toStreamCmdGetModelDomainElements(std::ostream& out,
1949 : : TypeNode type) const
1950 : : {
1951 : 1 : out << "(get-model-domain-elements " << type << ")";
1952 : 1 : }
1953 : :
1954 : 25 : void Smt2Printer::toStreamCmdGetModel(std::ostream& out) const
1955 : : {
1956 : 25 : out << "(get-model)";
1957 : 25 : }
1958 : :
1959 : 7 : void Smt2Printer::toStreamCmdBlockModel(std::ostream& out,
1960 : : modes::BlockModelsMode mode) const
1961 : : {
1962 : 7 : out << "(block-model :";
1963 [ + + ][ - ]: 7 : switch (mode)
1964 : : {
1965 : 4 : case modes::BlockModelsMode::LITERALS: out << "literals"; break;
1966 : 3 : case modes::BlockModelsMode::VALUES: out << "values"; break;
1967 : 0 : default: Unreachable() << "Invalid block models mode " << mode;
1968 : : }
1969 : 7 : out << ")";
1970 : 7 : }
1971 : :
1972 : 3 : void Smt2Printer::toStreamCmdBlockModelValues(
1973 : : std::ostream& out, const std::vector<Node>& nodes) const
1974 : : {
1975 : 3 : out << "(block-model-values (";
1976 [ + + ]: 10 : for (size_t i = 0, n = nodes.size(); i < n; ++i)
1977 : : {
1978 [ + + ]: 7 : if (i != 0)
1979 : : {
1980 : 4 : out << ' ';
1981 : : }
1982 : 7 : out << nodes[i];
1983 : : }
1984 : 3 : out << "))";
1985 : 3 : }
1986 : :
1987 : 5 : void Smt2Printer::toStreamCmdGetAssignment(std::ostream& out) const
1988 : : {
1989 : 5 : out << "(get-assignment)";
1990 : 5 : }
1991 : :
1992 : 1 : void Smt2Printer::toStreamCmdGetAssertions(std::ostream& out) const
1993 : : {
1994 : 1 : out << "(get-assertions)";
1995 : 1 : }
1996 : :
1997 : 7 : void Smt2Printer::toStreamCmdGetProof(std::ostream& out,
1998 : : modes::ProofComponent c) const
1999 : : {
2000 : 7 : out << "(get-proof";
2001 [ + + ]: 7 : if (c != modes::ProofComponent::FULL)
2002 : : {
2003 : 4 : out << " :" << c;
2004 : : }
2005 : 7 : out << ")";
2006 : 7 : }
2007 : :
2008 : 6 : void Smt2Printer::toStreamCmdGetUnsatAssumptions(std::ostream& out) const
2009 : : {
2010 : 6 : out << "(get-unsat-assumptions)";
2011 : 6 : }
2012 : :
2013 : 13 : void Smt2Printer::toStreamCmdGetUnsatCore(std::ostream& out) const
2014 : : {
2015 : 13 : out << "(get-unsat-core)";
2016 : 13 : }
2017 : :
2018 : 3 : void Smt2Printer::toStreamCmdGetDifficulty(std::ostream& out) const
2019 : : {
2020 : 3 : out << "(get-difficulty)";
2021 : 3 : }
2022 : :
2023 : 6 : void Smt2Printer::toStreamCmdGetTimeoutCore(std::ostream& out) const
2024 : : {
2025 : 6 : out << "(get-timeout-core)";
2026 : 6 : }
2027 : :
2028 : 3 : void Smt2Printer::toStreamCmdGetTimeoutCoreAssuming(
2029 : : std::ostream& out, const std::vector<Node>& assumptions) const
2030 : : {
2031 : 3 : out << "(get-timeout-core-assuming (";
2032 : 3 : bool firstTime = true;
2033 [ + + ]: 9 : for (const Node& a : assumptions)
2034 : : {
2035 [ + + ]: 6 : if (firstTime)
2036 : : {
2037 : 3 : firstTime = false;
2038 : : }
2039 : : else
2040 : : {
2041 : 3 : out << " ";
2042 : : }
2043 : 6 : out << a;
2044 : : }
2045 : 3 : out << "))";
2046 : 3 : }
2047 : :
2048 : 7 : void Smt2Printer::toStreamCmdGetLearnedLiterals(std::ostream& out,
2049 : : modes::LearnedLitType t) const
2050 : : {
2051 : 7 : out << "(get-learned-literals";
2052 [ + + ]: 7 : if (t != modes::LearnedLitType::INPUT)
2053 : : {
2054 : 5 : out << " :" << t;
2055 : : }
2056 : 7 : out << ")";
2057 : 7 : }
2058 : :
2059 : 4261 : void Smt2Printer::toStreamCmdSetBenchmarkLogic(std::ostream& out,
2060 : : const std::string& logic) const
2061 : : {
2062 : 4261 : out << "(set-logic " << logic << ')';
2063 : 4261 : }
2064 : :
2065 : 3170 : void Smt2Printer::toStreamCmdSetInfo(std::ostream& out,
2066 : : const std::string& flag,
2067 : : const std::string& value) const
2068 : : {
2069 : 3170 : out << "(set-info :" << flag << " " << value << ")";
2070 : 3170 : }
2071 : :
2072 : 17 : void Smt2Printer::toStreamCmdGetInfo(std::ostream& out,
2073 : : const std::string& flag) const
2074 : : {
2075 : 17 : out << "(get-info :" << flag << ')';
2076 : 17 : }
2077 : :
2078 : 1428 : void Smt2Printer::toStreamCmdSetOption(std::ostream& out,
2079 : : const std::string& flag,
2080 : : const std::string& value) const
2081 : : {
2082 : 1428 : out << "(set-option :" << flag << ' ';
2083 : : // special cases: output channels require surrounding quotes in smt2 format
2084 [ + + ]: 2854 : if (flag == "diagnostic-output-channel" || flag == "regular-output-channel"
2085 [ + + ][ + + ]: 2854 : || flag == "in")
[ + + ]
2086 : : {
2087 : 4 : out << "\"" << value << "\"";
2088 : : }
2089 : : else
2090 : : {
2091 : 1424 : out << value;
2092 : : }
2093 : 1428 : out << ')';
2094 : 1428 : }
2095 : :
2096 : 43 : void Smt2Printer::toStreamCmdGetOption(std::ostream& out,
2097 : : const std::string& flag) const
2098 : : {
2099 : 43 : out << "(get-option :" << flag << ')';
2100 : 43 : }
2101 : :
2102 : 1203 : void Smt2Printer::toStream(std::ostream& out, const DType& dt) const
2103 : : {
2104 [ + + ]: 3432 : for (size_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
2105 : : {
2106 : 2229 : const DTypeConstructor& cons = dt[i];
2107 [ + + ]: 2229 : if (i != 0)
2108 : : {
2109 : 1026 : out << " ";
2110 : : }
2111 : 2229 : out << "(" << cvc5::internal::quoteSymbol(cons.getName());
2112 [ + + ]: 4322 : for (size_t j = 0, nargs = cons.getNumArgs(); j < nargs; j++)
2113 : : {
2114 : 2093 : const DTypeSelector& arg = cons[j];
2115 : 2093 : out << " (" << arg.getSelector() << " " << arg.getRangeType() << ")";
2116 : : }
2117 : 2229 : out << ")";
2118 : : }
2119 : 1203 : }
2120 : :
2121 : 949 : void Smt2Printer::toStreamCmdDatatypeDeclaration(
2122 : : std::ostream& out, const std::vector<TypeNode>& datatypes) const
2123 : : {
2124 [ - + ][ - + ]: 949 : Assert(!datatypes.empty());
[ - - ]
2125 [ - + ][ - + ]: 949 : Assert(datatypes[0].isDatatype());
[ - - ]
2126 : 949 : const DType& d0 = datatypes[0].getDType();
2127 [ - + ]: 949 : if (d0.isTuple())
2128 : : {
2129 : : // not necessary to print tuples
2130 : 0 : Assert(datatypes.size() == 1);
2131 : 0 : return;
2132 : : }
2133 : 949 : out << "(declare-";
2134 : : // Ethos does not support codatatypes, we just print as an ordinary
2135 : : // datatype for now
2136 [ + + ][ + + ]: 949 : if (d0.isCodatatype() && d_variant != Variant::eo_variant)
[ + + ]
2137 : : {
2138 : 16 : out << "co";
2139 : : }
2140 : 949 : out << "datatypes";
2141 : 949 : out << " (";
2142 [ + + ]: 2152 : for (const TypeNode& t : datatypes)
2143 : : {
2144 [ - + ][ - + ]: 1203 : Assert(t.isDatatype());
[ - - ]
2145 : 1203 : const DType& d = t.getDType();
2146 : 1203 : out << "(" << cvc5::internal::quoteSymbol(d.getName());
2147 : 1203 : out << " " << d.getNumParameters() << ")";
2148 : : }
2149 : 949 : out << ") (";
2150 [ + + ]: 2152 : for (const TypeNode& t : datatypes)
2151 : : {
2152 [ - + ][ - + ]: 1203 : Assert(t.isDatatype());
[ - - ]
2153 : 1203 : const DType& d = t.getDType();
2154 [ + + ]: 1203 : if (d.isParametric())
2155 : : {
2156 : 50 : out << "(par (";
2157 [ + + ]: 114 : for (unsigned p = 0, nparam = d.getNumParameters(); p < nparam; p++)
2158 : : {
2159 [ + + ]: 64 : out << (p > 0 ? " " : "") << d.getParameter(p);
2160 : : }
2161 : 50 : out << ")";
2162 : : }
2163 : 1203 : out << "(";
2164 : 1203 : toStream(out, d);
2165 : 1203 : out << ")";
2166 [ + + ]: 1203 : if (d.isParametric())
2167 : : {
2168 : 50 : out << ")";
2169 : : }
2170 : : }
2171 : 949 : out << ")";
2172 : 949 : out << ")";
2173 : : }
2174 : :
2175 : 49 : void Smt2Printer::toStreamCmdDeclareHeap(std::ostream& out,
2176 : : TypeNode locType,
2177 : : TypeNode dataType) const
2178 : : {
2179 : 49 : out << "(declare-heap (" << locType << " " << dataType << "))";
2180 : 49 : }
2181 : :
2182 : 4115 : void Smt2Printer::toStreamSkolem(std::ostream& out,
2183 : : Node cacheVal,
2184 : : SkolemId id,
2185 : : bool isApplied,
2186 : : int toDepth,
2187 : : const LetBinding* lbind) const
2188 : : {
2189 : : // true if this is a standalone skolem that requires printing with arguments
2190 [ + + ][ + + ]: 4115 : bool unappliedApp = (!isApplied && !cacheVal.isNull());
2191 [ + + ]: 4115 : if (unappliedApp)
2192 : : {
2193 : 3713 : out << "(";
2194 : : }
2195 : 4115 : out << "@" << id;
2196 [ + + ]: 4115 : if (cacheVal.getKind() == Kind::SEXPR)
2197 : : {
2198 [ + + ]: 844 : for (const Node& cv : cacheVal)
2199 : : {
2200 : 596 : out << " ";
2201 : 596 : toStream(out, cv, lbind, toDepth);
2202 : 596 : }
2203 : : }
2204 [ + + ]: 3867 : else if (!cacheVal.isNull())
2205 : : {
2206 : 3672 : out << " ";
2207 : 3672 : toStream(out, cacheVal, lbind, toDepth);
2208 : : }
2209 [ + + ]: 4115 : if (unappliedApp)
2210 : : {
2211 : 3713 : out << ")";
2212 : : }
2213 [ + + ]: 402 : else if (isApplied)
2214 : : {
2215 : : // separates further arguments
2216 : 298 : out << " ";
2217 : : }
2218 : 4115 : }
2219 : :
2220 : 9 : void Smt2Printer::toStreamCmdEmpty(CVC5_UNUSED std::ostream& out,
2221 : : CVC5_UNUSED const std::string& name) const
2222 : : {
2223 : 9 : }
2224 : :
2225 : 9 : void Smt2Printer::toStreamCmdEcho(std::ostream& out,
2226 : : const std::string& output) const
2227 : : {
2228 : 9 : out << "(echo " << cvc5::internal::quoteString(output) << ')';
2229 : 9 : }
2230 : :
2231 : : /*
2232 : : --------------------------------------------------------------------------
2233 : : Handling SyGuS commands
2234 : : --------------------------------------------------------------------------
2235 : : */
2236 : :
2237 : 235 : std::string Smt2Printer::sygusGrammarString(const TypeNode& t)
2238 : : {
2239 : 235 : std::stringstream out;
2240 [ + - ][ + - ]: 235 : if (!t.isNull() && t.isDatatype() && t.getDType().isSygus())
[ + - ][ + - ]
2241 : : {
2242 : 235 : std::stringstream types_predecl, types_list;
2243 : 235 : std::set<TypeNode> grammarTypes;
2244 : 235 : std::list<TypeNode> typesToPrint;
2245 : 235 : grammarTypes.insert(t);
2246 : 235 : typesToPrint.push_back(t);
2247 : 235 : NodeManager* nm = t.getNodeManager();
2248 : : // for each datatype in grammar
2249 : : // name
2250 : : // sygus type
2251 : : // constructors in order
2252 : : do
2253 : : {
2254 : 482 : TypeNode curr = typesToPrint.front();
2255 : 482 : typesToPrint.pop_front();
2256 : : // skip builtin fields, which can originate from any-constant constructors
2257 [ + - ][ - + ]: 482 : if (!curr.isDatatype() || !curr.getDType().isSygus())
[ - + ]
2258 : : {
2259 : 0 : continue;
2260 : : }
2261 : 482 : const DType& dt = curr.getDType();
2262 : 482 : types_list << '(' << dt.getName() << ' ' << dt.getSygusType() << " (";
2263 : 482 : types_predecl << '(' << dt.getName() << ' ' << dt.getSygusType() << ") ";
2264 [ + + ]: 2478 : for (size_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
2265 : : {
2266 [ + + ]: 1996 : if (i > 0)
2267 : : {
2268 : 1514 : types_list << ' ';
2269 : : }
2270 : 1996 : const DTypeConstructor& cons = dt[i];
2271 [ + + ]: 1996 : if (cons.isSygusAnyConstant())
2272 : : {
2273 : 31 : types_list << "(Constant " << cons[0].getRangeType() << ")";
2274 : : }
2275 : : else
2276 : : {
2277 : : // make a sygus term
2278 : 1965 : std::vector<Node> cchildren;
2279 : 1965 : cchildren.push_back(cons.getConstructor());
2280 [ + + ]: 3921 : for (size_t j = 0, nargs = cons.getNumArgs(); j < nargs; j++)
2281 : : {
2282 : 1956 : TypeNode argType = cons[j].getRangeType();
2283 : 1956 : std::stringstream ss;
2284 : 1956 : ss << argType;
2285 : 1956 : Node bv = NodeManager::mkBoundVar(ss.str(), argType);
2286 : 1956 : cchildren.push_back(bv);
2287 : : // if fresh type, store it for later processing
2288 [ + + ]: 1956 : if (grammarTypes.insert(argType).second)
2289 : : {
2290 : 247 : typesToPrint.push_back(argType);
2291 : : }
2292 : 1956 : }
2293 : 1965 : Node consToPrint = nm->mkNode(Kind::APPLY_CONSTRUCTOR, cchildren);
2294 : : // now, print it using the conversion to builtin with external
2295 : 3930 : types_list << theory::datatypes::utils::sygusToBuiltin(consToPrint,
2296 : 1965 : true);
2297 : 1965 : }
2298 : : }
2299 : 482 : types_list << "))";
2300 [ + - ][ + + ]: 964 : } while (!typesToPrint.empty());
2301 : :
2302 : 235 : out << "(" << types_predecl.str() << ")(" << types_list.str() << ')';
2303 : 235 : }
2304 : 470 : return out.str();
2305 : 235 : }
2306 : :
2307 : 403 : void Smt2Printer::toStreamCmdSynthFun(std::ostream& out,
2308 : : const std::string& id,
2309 : : const std::vector<Node>& vars,
2310 : : TypeNode rangeType,
2311 : : TypeNode sygusType) const
2312 : : {
2313 : 403 : out << "(synth-fun " << cvc5::internal::quoteSymbol(id) << ' ';
2314 : : // print variable list
2315 : 403 : toStreamSortedVarList(out, vars);
2316 : : // print return type
2317 : 403 : out << ' ' << rangeType;
2318 : : // print grammar, if any
2319 [ + + ]: 403 : if (!sygusType.isNull())
2320 : : {
2321 : 192 : out << sygusGrammarString(sygusType);
2322 : : }
2323 : 403 : out << ')';
2324 : 403 : }
2325 : :
2326 : 360 : void Smt2Printer::toStreamCmdDeclareVar(std::ostream& out,
2327 : : const std::string& id,
2328 : : TypeNode type) const
2329 : : {
2330 : 720 : out << "(declare-var " << cvc5::internal::quoteSymbol(id) << ' ' << type
2331 : 360 : << ')';
2332 : 360 : }
2333 : :
2334 : 699 : void Smt2Printer::toStreamCmdConstraint(std::ostream& out, Node n) const
2335 : : {
2336 : 699 : out << "(constraint " << n << ')';
2337 : 699 : }
2338 : :
2339 : 4 : void Smt2Printer::toStreamCmdAssume(std::ostream& out, Node n) const
2340 : : {
2341 : 4 : out << "(assume " << n << ')';
2342 : 4 : }
2343 : :
2344 : 13 : void Smt2Printer::toStreamCmdInvConstraint(
2345 : : std::ostream& out, Node inv, Node pre, Node trans, Node post) const
2346 : : {
2347 : 26 : out << "(inv-constraint " << inv << ' ' << pre << ' ' << trans << ' ' << post
2348 : 13 : << ')';
2349 : 13 : }
2350 : :
2351 : 232 : void Smt2Printer::toStreamCmdCheckSynth(std::ostream& out) const
2352 : : {
2353 : 232 : out << "(check-synth)";
2354 : 232 : }
2355 : :
2356 : 6 : void Smt2Printer::toStreamCmdCheckSynthNext(std::ostream& out) const
2357 : : {
2358 : 6 : out << "(check-synth-next)";
2359 : 6 : }
2360 : :
2361 : 26 : void Smt2Printer::toStreamCmdFindSynth(std::ostream& out,
2362 : : modes::FindSynthTarget fst,
2363 : : TypeNode sygusType) const
2364 : : {
2365 : 26 : out << "(find-synth :" << fst;
2366 : : // print grammar, if any
2367 [ + + ]: 26 : if (!sygusType.isNull())
2368 : : {
2369 : 1 : out << " " << sygusGrammarString(sygusType);
2370 : : }
2371 : 26 : out << ")";
2372 : 26 : }
2373 : :
2374 : 1 : void Smt2Printer::toStreamCmdFindSynthNext(std::ostream& out) const
2375 : : {
2376 : 1 : out << "(find-synth-next)";
2377 : 1 : }
2378 : :
2379 : 23 : void Smt2Printer::toStreamCmdGetInterpol(std::ostream& out,
2380 : : const std::string& name,
2381 : : Node conj,
2382 : : TypeNode sygusType) const
2383 : : {
2384 : 23 : out << "(get-interpolant " << cvc5::internal::quoteSymbol(name) << ' '
2385 : 23 : << conj;
2386 [ + + ]: 23 : if (!sygusType.isNull())
2387 : : {
2388 : 5 : out << ' ' << sygusGrammarString(sygusType);
2389 : : }
2390 : 23 : out << ')';
2391 : 23 : }
2392 : :
2393 : 1 : void Smt2Printer::toStreamCmdGetInterpolNext(std::ostream& out) const
2394 : : {
2395 : 1 : out << "(get-interpolant-next)";
2396 : 1 : }
2397 : :
2398 : 33 : void Smt2Printer::toStreamCmdGetAbduct(std::ostream& out,
2399 : : const std::string& name,
2400 : : Node conj,
2401 : : TypeNode sygusType) const
2402 : : {
2403 : 33 : out << "(get-abduct ";
2404 : 33 : out << name << ' ';
2405 : 33 : out << conj << ' ';
2406 : :
2407 : : // print grammar, if any
2408 [ + + ]: 33 : if (!sygusType.isNull())
2409 : : {
2410 : 6 : out << sygusGrammarString(sygusType);
2411 : : }
2412 : 33 : out << ')';
2413 : 33 : }
2414 : :
2415 : 6 : void Smt2Printer::toStreamCmdGetAbductNext(std::ostream& out) const
2416 : : {
2417 : 6 : out << "(get-abduct-next)";
2418 : 6 : }
2419 : :
2420 : 19 : void Smt2Printer::toStreamCmdGetQuantifierElimination(std::ostream& out,
2421 : : Node n,
2422 : : bool doFull) const
2423 : : {
2424 [ + + ]: 19 : out << '(' << (doFull ? "get-qe" : "get-qe-disjunct") << ' ' << n << ')';
2425 : 19 : }
2426 : :
2427 : : /*
2428 : : --------------------------------------------------------------------------
2429 : : End of Handling SyGuS commands
2430 : : --------------------------------------------------------------------------
2431 : : */
2432 : :
2433 : : } // namespace smt2
2434 : : } // namespace printer
2435 : : } // namespace cvc5::internal
|
