1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Morgan Deters, Dejan Jovanovic |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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 CVC output language. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "printer/cvc/cvc_printer.h" |
17 |
|
|
18 |
|
#include <algorithm> |
19 |
|
#include <iostream> |
20 |
|
#include <iterator> |
21 |
|
#include <stack> |
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/datatype_index.h" |
29 |
|
#include "expr/dtype.h" |
30 |
|
#include "expr/dtype_cons.h" |
31 |
|
#include "expr/dtype_selector.h" |
32 |
|
#include "expr/emptyset.h" |
33 |
|
#include "expr/node_manager_attributes.h" // for VarNameAttr |
34 |
|
#include "expr/node_visitor.h" |
35 |
|
#include "expr/sequence.h" |
36 |
|
#include "options/language.h" // for LANG_AST |
37 |
|
#include "options/smt_options.h" |
38 |
|
#include "printer/let_binding.h" |
39 |
|
#include "smt/command.h" |
40 |
|
#include "smt/node_command.h" |
41 |
|
#include "smt/smt_engine.h" |
42 |
|
#include "theory/arrays/theory_arrays_rewriter.h" |
43 |
|
#include "theory/substitutions.h" |
44 |
|
#include "theory/theory_model.h" |
45 |
|
#include "util/bitvector.h" |
46 |
|
#include "util/divisible.h" |
47 |
|
#include "util/rational.h" |
48 |
|
#include "util/string.h" |
49 |
|
|
50 |
|
using namespace std; |
51 |
|
|
52 |
|
namespace cvc5 { |
53 |
|
namespace printer { |
54 |
|
namespace cvc { |
55 |
|
|
56 |
2816 |
void CvcPrinter::toStream(std::ostream& out, |
57 |
|
TNode n, |
58 |
|
int toDepth, |
59 |
|
size_t dag) const |
60 |
|
{ |
61 |
2816 |
if(dag != 0) { |
62 |
1914 |
LetBinding lbind(dag + 1); |
63 |
957 |
toStreamNodeWithLetify(out, n, toDepth, false, &lbind); |
64 |
|
} else { |
65 |
1859 |
toStreamNode(out, n, toDepth, false, nullptr); |
66 |
|
} |
67 |
2816 |
} |
68 |
|
|
69 |
431 |
void toStreamRational(std::ostream& out, Node n, bool forceRational) |
70 |
|
{ |
71 |
431 |
Assert(n.getKind() == kind::CONST_RATIONAL); |
72 |
431 |
const Rational& rat = n.getConst<Rational>(); |
73 |
431 |
if (rat.isIntegral() && !forceRational) |
74 |
|
{ |
75 |
431 |
out << rat.getNumerator(); |
76 |
|
} |
77 |
|
else |
78 |
|
{ |
79 |
|
out << '(' << rat.getNumerator() << '/' << rat.getDenominator() << ')'; |
80 |
|
} |
81 |
431 |
} |
82 |
|
|
83 |
5197 |
void CvcPrinter::toStreamNode(std::ostream& out, |
84 |
|
TNode n, |
85 |
|
int depth, |
86 |
|
bool bracket, |
87 |
|
LetBinding* lbind) const |
88 |
|
{ |
89 |
5197 |
if (depth == 0) { |
90 |
|
out << "(...)"; |
91 |
|
} else { |
92 |
5197 |
--depth; |
93 |
|
} |
94 |
|
|
95 |
|
// null |
96 |
5197 |
if(n.getKind() == kind::NULL_EXPR) { |
97 |
|
out << "null"; |
98 |
4242 |
return; |
99 |
|
} |
100 |
|
|
101 |
|
// variables |
102 |
5197 |
if(n.isVar()) { |
103 |
4370 |
string s; |
104 |
2185 |
if(n.getAttribute(expr::VarNameAttr(), s)) { |
105 |
2185 |
out << s; |
106 |
|
} else { |
107 |
|
if(n.getKind() == kind::VARIABLE) { |
108 |
|
out << "var_"; |
109 |
|
} else { |
110 |
|
out << n.getKind() << '_'; |
111 |
|
} |
112 |
|
out << n.getId(); |
113 |
|
} |
114 |
2185 |
return; |
115 |
|
} |
116 |
3012 |
if(n.isNullaryOp()) { |
117 |
|
if( n.getKind() == kind::UNIVERSE_SET ){ |
118 |
|
out << "UNIVERSE :: " << n.getType(); |
119 |
|
}else{ |
120 |
|
//unknown printer |
121 |
|
out << n.getKind(); |
122 |
|
} |
123 |
|
return; |
124 |
|
} |
125 |
|
|
126 |
|
// constants |
127 |
3012 |
if(n.getMetaKind() == kind::metakind::CONSTANT) { |
128 |
1612 |
switch(n.getKind()) { |
129 |
54 |
case kind::BITVECTOR_TYPE: |
130 |
54 |
out << "BITVECTOR(" << n.getConst<BitVectorSize>().d_size << ")"; |
131 |
54 |
break; |
132 |
12 |
case kind::CONST_BITVECTOR: { |
133 |
12 |
const BitVector& bv = n.getConst<BitVector>(); |
134 |
12 |
const Integer& x = bv.getValue(); |
135 |
12 |
out << "0bin"; |
136 |
12 |
unsigned size = bv.getSize(); |
137 |
60 |
while (size-- > 0) |
138 |
|
{ |
139 |
24 |
out << (x.testBit(size) ? '1' : '0'); |
140 |
|
} |
141 |
12 |
break; |
142 |
|
} |
143 |
12 |
case kind::CONST_BOOLEAN: |
144 |
|
// the default would print "1" or "0" for bool, that's not correct |
145 |
|
// for our purposes |
146 |
12 |
out << (n.getConst<bool>() ? "TRUE" : "FALSE"); |
147 |
12 |
break; |
148 |
431 |
case kind::CONST_RATIONAL: { |
149 |
431 |
toStreamRational(out, n, false); |
150 |
431 |
break; |
151 |
|
} |
152 |
26 |
case kind::CONST_STRING: |
153 |
|
{ |
154 |
26 |
out << '"' << n.getConst<String>().toString() << '"'; |
155 |
26 |
break; |
156 |
|
} |
157 |
|
case kind::CONST_SEQUENCE: |
158 |
|
{ |
159 |
|
const Sequence& sn = n.getConst<Sequence>(); |
160 |
|
const std::vector<Node>& snvec = sn.getVec(); |
161 |
|
if (snvec.size() > 1) |
162 |
|
{ |
163 |
|
out << "CONCAT("; |
164 |
|
} |
165 |
|
bool first = true; |
166 |
|
for (const Node& snvc : snvec) |
167 |
|
{ |
168 |
|
if (!first) |
169 |
|
{ |
170 |
|
out << ", "; |
171 |
|
} |
172 |
|
out << "SEQ_UNIT(" << snvc << ")"; |
173 |
|
first = false; |
174 |
|
} |
175 |
|
if (snvec.size() > 1) |
176 |
|
{ |
177 |
|
out << ")"; |
178 |
|
} |
179 |
|
break; |
180 |
|
} |
181 |
824 |
case kind::TYPE_CONSTANT: |
182 |
824 |
switch(TypeConstant tc = n.getConst<TypeConstant>()) { |
183 |
40 |
case REAL_TYPE: |
184 |
40 |
out << "REAL"; |
185 |
40 |
break; |
186 |
768 |
case INTEGER_TYPE: |
187 |
768 |
out << "INT"; |
188 |
768 |
break; |
189 |
12 |
case BOOLEAN_TYPE: |
190 |
12 |
out << "BOOLEAN"; |
191 |
12 |
break; |
192 |
4 |
case STRING_TYPE: |
193 |
4 |
out << "STRING"; |
194 |
4 |
break; |
195 |
|
default: |
196 |
|
out << tc; |
197 |
|
break; |
198 |
|
} |
199 |
824 |
break; |
200 |
|
|
201 |
253 |
case kind::DATATYPE_TYPE: { |
202 |
|
const DType& dt = NodeManager::currentNM()->getDTypeForIndex( |
203 |
253 |
n.getConst<DatatypeIndexConstant>().getIndex()); |
204 |
253 |
if( dt.isTuple() ){ |
205 |
34 |
out << '['; |
206 |
79 |
for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) { |
207 |
45 |
if (i > 0) { |
208 |
20 |
out << ", "; |
209 |
|
} |
210 |
90 |
TypeNode t = dt[0][i].getRangeType(); |
211 |
45 |
out << t; |
212 |
|
} |
213 |
34 |
out << ']'; |
214 |
|
} |
215 |
219 |
else if (dt.isRecord()) |
216 |
|
{ |
217 |
59 |
out << "[# "; |
218 |
208 |
for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) { |
219 |
149 |
if (i > 0) { |
220 |
96 |
out << ", "; |
221 |
|
} |
222 |
298 |
TypeNode t = dt[0][i].getRangeType(); |
223 |
149 |
out << dt[0][i].getSelector() << ":" << t; |
224 |
|
} |
225 |
59 |
out << " #]"; |
226 |
|
}else{ |
227 |
160 |
out << dt.getName(); |
228 |
|
} |
229 |
|
} |
230 |
253 |
break; |
231 |
|
|
232 |
|
case kind::EMPTYSET: |
233 |
|
out << "{} :: " << n.getConst<EmptySet>().getType(); |
234 |
|
break; |
235 |
|
|
236 |
|
case kind::STORE_ALL: { |
237 |
|
const ArrayStoreAll& asa = n.getConst<ArrayStoreAll>(); |
238 |
|
out << "ARRAY(" << asa.getType().getArrayIndexType() << " OF " |
239 |
|
<< asa.getType().getArrayConstituentType() |
240 |
|
<< ") : " << asa.getValue(); |
241 |
|
break; |
242 |
|
} |
243 |
|
|
244 |
|
default: |
245 |
|
// Fall back to whatever operator<< does on underlying type; we |
246 |
|
// might luck out and print something reasonable. |
247 |
|
kind::metakind::NodeValueConstPrinter::toStream(out, n); |
248 |
|
} |
249 |
|
|
250 |
1612 |
return; |
251 |
|
} |
252 |
|
|
253 |
|
enum OpType { |
254 |
|
PREFIX, |
255 |
|
INFIX, |
256 |
|
POSTFIX |
257 |
|
} opType; |
258 |
|
|
259 |
|
//The default operation type is PREFIX |
260 |
1400 |
opType = PREFIX; |
261 |
|
|
262 |
2355 |
stringstream op; // operation (such as '+') |
263 |
|
|
264 |
1400 |
switch(n.getKind()) { |
265 |
|
|
266 |
|
// BUILTIN |
267 |
71 |
case kind::EQUAL: |
268 |
71 |
if( n[0].getType().isBoolean() ){ |
269 |
28 |
op << "<=>"; |
270 |
|
}else{ |
271 |
43 |
op << '='; |
272 |
|
} |
273 |
71 |
opType = INFIX; |
274 |
71 |
break; |
275 |
|
case kind::ITE: |
276 |
|
out << "IF "; |
277 |
|
toStreamNode(out, n[0], depth, true, lbind); |
278 |
|
out << " THEN "; |
279 |
|
toStreamNode(out, n[1], depth, true, lbind); |
280 |
|
out << " ELSE "; |
281 |
|
toStreamNode(out, n[2], depth, true, lbind); |
282 |
|
out << " ENDIF"; |
283 |
|
return; |
284 |
|
break; |
285 |
216 |
case kind::SEXPR: |
286 |
|
// no-op |
287 |
216 |
break; |
288 |
2 |
case kind::LAMBDA: |
289 |
2 |
out << "(LAMBDA"; |
290 |
2 |
toStreamNode(out, n[0], depth, true, lbind); |
291 |
2 |
out << ": "; |
292 |
2 |
toStreamNodeWithLetify(out, n[1], depth, true, lbind); |
293 |
2 |
out << ")"; |
294 |
2 |
return; |
295 |
|
break; |
296 |
|
case kind::WITNESS: |
297 |
|
out << "(WITNESS"; |
298 |
|
toStreamNode(out, n[0], depth, true, lbind); |
299 |
|
out << " : "; |
300 |
|
toStreamNodeWithLetify(out, n[1], depth, true, lbind); |
301 |
|
out << ')'; |
302 |
|
return; |
303 |
|
case kind::DISTINCT: |
304 |
|
// distinct not supported directly, blast it away with the rewriter |
305 |
|
toStreamNode(out, theory::Rewriter::rewrite(n), depth, true, lbind); |
306 |
|
return; |
307 |
212 |
case kind::SORT_TYPE: |
308 |
|
{ |
309 |
212 |
string name; |
310 |
212 |
if(n.getAttribute(expr::VarNameAttr(), name)) { |
311 |
212 |
out << name; |
312 |
212 |
return; |
313 |
|
} |
314 |
|
} |
315 |
|
break; |
316 |
|
|
317 |
|
// BOOL |
318 |
40 |
case kind::AND: |
319 |
40 |
op << "AND"; |
320 |
40 |
opType = INFIX; |
321 |
40 |
break; |
322 |
58 |
case kind::OR: |
323 |
58 |
op << "OR"; |
324 |
58 |
opType = INFIX; |
325 |
58 |
break; |
326 |
87 |
case kind::NOT: |
327 |
87 |
op << "NOT"; |
328 |
87 |
opType = PREFIX; |
329 |
87 |
break; |
330 |
|
case kind::XOR: |
331 |
|
op << "XOR"; |
332 |
|
opType = INFIX; |
333 |
|
break; |
334 |
|
case kind::IMPLIES: |
335 |
|
op << "=>"; |
336 |
|
opType = INFIX; |
337 |
|
break; |
338 |
|
|
339 |
|
// UF |
340 |
118 |
case kind::APPLY_UF: |
341 |
118 |
toStreamNode(op, n.getOperator(), depth, false, lbind); |
342 |
118 |
break; |
343 |
|
case kind::CARDINALITY_CONSTRAINT: |
344 |
|
case kind::COMBINED_CARDINALITY_CONSTRAINT: |
345 |
|
out << "CARDINALITY_CONSTRAINT"; |
346 |
|
break; |
347 |
|
|
348 |
|
case kind::FUNCTION_TYPE: |
349 |
|
if (n.getNumChildren() > 1) { |
350 |
|
if (n.getNumChildren() > 2) { |
351 |
|
out << '('; |
352 |
|
} |
353 |
|
for (unsigned i = 1; i < n.getNumChildren(); ++i) { |
354 |
|
if (i > 1) { |
355 |
|
out << ", "; |
356 |
|
} |
357 |
|
toStreamNode(out, n[i - 1], depth, false, lbind); |
358 |
|
} |
359 |
|
if (n.getNumChildren() > 2) { |
360 |
|
out << ')'; |
361 |
|
} |
362 |
|
} |
363 |
|
out << " -> "; |
364 |
|
toStreamNode(out, n[n.getNumChildren() - 1], depth, false, lbind); |
365 |
|
return; |
366 |
|
break; |
367 |
|
|
368 |
|
// DATATYPES |
369 |
|
case kind::PARAMETRIC_DATATYPE: { |
370 |
|
const DType& dt = NodeManager::currentNM()->getDTypeForIndex( |
371 |
|
n[0].getConst<DatatypeIndexConstant>().getIndex()); |
372 |
|
out << dt.getName() << '['; |
373 |
|
for (unsigned i = 1; i < n.getNumChildren(); ++i) |
374 |
|
{ |
375 |
|
if (i > 1) |
376 |
|
{ |
377 |
|
out << ','; |
378 |
|
} |
379 |
|
out << n[i]; |
380 |
|
} |
381 |
|
out << ']'; |
382 |
|
} |
383 |
|
return; |
384 |
|
break; |
385 |
|
case kind::APPLY_TYPE_ASCRIPTION: { |
386 |
|
toStreamNode(out, n[0], depth, false, lbind); |
387 |
|
out << "::"; |
388 |
|
TypeNode t = n.getOperator().getConst<AscriptionType>().getType(); |
389 |
|
out << (t.isFunctionLike() ? t.getRangeType() : t); |
390 |
|
} |
391 |
|
return; |
392 |
|
break; |
393 |
329 |
case kind::APPLY_CONSTRUCTOR: { |
394 |
627 |
TypeNode t = n.getType(); |
395 |
329 |
if( t.isTuple() ){ |
396 |
298 |
if( n.getNumChildren()==1 ){ |
397 |
45 |
out << "TUPLE"; |
398 |
|
} |
399 |
|
} |
400 |
31 |
else if (t.isRecord()) |
401 |
|
{ |
402 |
1 |
const DType& dt = t.getDType(); |
403 |
1 |
const DTypeConstructor& recCons = dt[0]; |
404 |
1 |
out << "(# "; |
405 |
3 |
for (size_t i = 0, nargs = recCons.getNumArgs(); i < nargs; i++) |
406 |
|
{ |
407 |
2 |
if (i != 0) |
408 |
|
{ |
409 |
1 |
out << ", "; |
410 |
|
} |
411 |
2 |
out << recCons[i].getName() << " := "; |
412 |
2 |
toStreamNode(out, n[i], depth, false, lbind); |
413 |
|
} |
414 |
1 |
out << " #)"; |
415 |
1 |
return; |
416 |
|
} |
417 |
|
else |
418 |
|
{ |
419 |
30 |
toStreamNode(op, n.getOperator(), depth, false, lbind); |
420 |
30 |
if (n.getNumChildren() == 0) |
421 |
|
{ |
422 |
|
// for datatype constants d, we print "d" and not "d()" |
423 |
30 |
out << op.str(); |
424 |
30 |
return; |
425 |
|
} |
426 |
298 |
} |
427 |
|
} |
428 |
298 |
break; |
429 |
61 |
case kind::APPLY_SELECTOR: |
430 |
|
case kind::APPLY_SELECTOR_TOTAL: { |
431 |
63 |
TypeNode t = n[0].getType(); |
432 |
63 |
Node opn = n.getOperator(); |
433 |
61 |
if (!t.isDatatype()) |
434 |
|
{ |
435 |
|
toStreamNode(op, opn, depth, false, lbind); |
436 |
|
} |
437 |
61 |
else if (t.isTuple() || t.isRecord()) |
438 |
|
{ |
439 |
59 |
toStreamNode(out, n[0], depth, true, lbind); |
440 |
59 |
out << '.'; |
441 |
59 |
const DType& dt = t.getDType(); |
442 |
59 |
if (t.isTuple()) |
443 |
|
{ |
444 |
|
int sindex; |
445 |
54 |
if (n.getKind() == kind::APPLY_SELECTOR) |
446 |
|
{ |
447 |
2 |
sindex = DType::indexOf(opn); |
448 |
|
} |
449 |
|
else |
450 |
|
{ |
451 |
52 |
sindex = dt[0].getSelectorIndexInternal(opn); |
452 |
|
} |
453 |
54 |
Assert(sindex >= 0); |
454 |
54 |
out << sindex; |
455 |
|
} |
456 |
|
else |
457 |
|
{ |
458 |
5 |
toStreamNode(out, opn, depth, false, lbind); |
459 |
|
} |
460 |
59 |
return; |
461 |
|
}else{ |
462 |
2 |
toStreamNode(op, opn, depth, false, lbind); |
463 |
2 |
} |
464 |
|
} |
465 |
2 |
break; |
466 |
|
case kind::APPLY_TESTER: { |
467 |
|
Assert(!n.getType().isTuple() && !n.getType().isRecord()); |
468 |
|
op << "is_"; |
469 |
|
unsigned cindex = DType::indexOf(n.getOperator()); |
470 |
|
const DType& dt = DType::datatypeOf(n.getOperator()); |
471 |
|
toStreamNode(op, dt[cindex].getConstructor(), depth, false, lbind); |
472 |
|
} |
473 |
|
break; |
474 |
|
case kind::CONSTRUCTOR_TYPE: |
475 |
|
case kind::SELECTOR_TYPE: |
476 |
|
if(n.getNumChildren() > 1) { |
477 |
|
if(n.getNumChildren() > 2) { |
478 |
|
out << '('; |
479 |
|
} |
480 |
|
for(unsigned i = 0; i < n.getNumChildren() - 1; ++i) { |
481 |
|
if(i > 0) { |
482 |
|
out << ", "; |
483 |
|
} |
484 |
|
toStreamNode(out, n[i], depth, false, lbind); |
485 |
|
} |
486 |
|
if(n.getNumChildren() > 2) { |
487 |
|
out << ')'; |
488 |
|
} |
489 |
|
out << " -> "; |
490 |
|
} |
491 |
|
toStreamNode(out, n[n.getNumChildren() - 1], depth, false, lbind); |
492 |
|
return; |
493 |
|
case kind::TESTER_TYPE: |
494 |
|
toStreamNode(out, n[0], depth, false, lbind); |
495 |
|
out << " -> BOOLEAN"; |
496 |
|
return; |
497 |
|
break; |
498 |
|
|
499 |
|
// ARRAYS |
500 |
54 |
case kind::ARRAY_TYPE: |
501 |
54 |
out << "ARRAY "; |
502 |
54 |
toStreamNode(out, n[0], depth, false, lbind); |
503 |
54 |
out << " OF "; |
504 |
54 |
toStreamNode(out, n[1], depth, false, lbind); |
505 |
54 |
return; |
506 |
|
break; |
507 |
22 |
case kind::SELECT: |
508 |
22 |
toStreamNode(out, n[0], depth, true, lbind); |
509 |
22 |
out << '['; |
510 |
22 |
toStreamNode(out, n[1], depth, false, lbind); |
511 |
22 |
out << ']'; |
512 |
22 |
return; |
513 |
|
break; |
514 |
|
case kind::STORE: { |
515 |
|
stack<TNode> stk; |
516 |
|
stk.push(n); |
517 |
|
while(stk.top()[0].getKind() == kind::STORE) { |
518 |
|
stk.push(stk.top()[0]); |
519 |
|
} |
520 |
|
if (bracket) { |
521 |
|
out << '('; |
522 |
|
} |
523 |
|
TNode x = stk.top(); |
524 |
|
toStreamNode(out, x[0], depth, false, lbind); |
525 |
|
out << " WITH ["; |
526 |
|
toStreamNode(out, x[1], depth, false, lbind); |
527 |
|
out << "] := "; |
528 |
|
toStreamNode(out, x[2], depth, false, lbind); |
529 |
|
stk.pop(); |
530 |
|
while(!stk.empty()) { |
531 |
|
x = stk.top(); |
532 |
|
out << ", ["; |
533 |
|
toStreamNode(out, x[1], depth, false, lbind); |
534 |
|
out << "] := "; |
535 |
|
toStreamNode(out, x[2], depth, false, lbind); |
536 |
|
stk.pop(); |
537 |
|
} |
538 |
|
if (bracket) { |
539 |
|
out << ')'; |
540 |
|
} |
541 |
|
return; |
542 |
|
break; |
543 |
|
} |
544 |
|
|
545 |
|
// ARITHMETIC |
546 |
15 |
case kind::PLUS: |
547 |
15 |
op << '+'; |
548 |
15 |
opType = INFIX; |
549 |
15 |
break; |
550 |
12 |
case kind::MULT: |
551 |
|
case kind::NONLINEAR_MULT: |
552 |
12 |
op << '*'; |
553 |
12 |
opType = INFIX; |
554 |
12 |
break; |
555 |
|
case kind::MINUS: |
556 |
|
op << '-'; |
557 |
|
opType = INFIX; |
558 |
|
break; |
559 |
|
case kind::UMINUS: |
560 |
|
op << '-'; |
561 |
|
opType = PREFIX; |
562 |
|
break; |
563 |
1 |
case kind::DIVISION: |
564 |
|
case kind::DIVISION_TOTAL: |
565 |
1 |
op << '/'; |
566 |
1 |
opType = INFIX; |
567 |
1 |
break; |
568 |
|
case kind::INTS_DIVISION: |
569 |
|
case kind::INTS_DIVISION_TOTAL: |
570 |
|
op << "DIV"; |
571 |
|
opType = INFIX; |
572 |
|
break; |
573 |
|
case kind::INTS_MODULUS: |
574 |
|
case kind::INTS_MODULUS_TOTAL: |
575 |
|
op << "MOD"; |
576 |
|
opType = INFIX; |
577 |
|
break; |
578 |
18 |
case kind::LT: |
579 |
18 |
op << '<'; |
580 |
18 |
opType = INFIX; |
581 |
18 |
break; |
582 |
|
case kind::LEQ: |
583 |
|
op << "<="; |
584 |
|
opType = INFIX; |
585 |
|
break; |
586 |
|
case kind::GT: |
587 |
|
op << '>'; |
588 |
|
opType = INFIX; |
589 |
|
break; |
590 |
9 |
case kind::GEQ: |
591 |
9 |
op << ">="; |
592 |
9 |
opType = INFIX; |
593 |
9 |
break; |
594 |
2 |
case kind::POW: |
595 |
2 |
op << '^'; |
596 |
2 |
opType = INFIX; |
597 |
2 |
break; |
598 |
|
case kind::ABS: |
599 |
|
op << "ABS"; |
600 |
|
opType = PREFIX; |
601 |
|
break; |
602 |
|
case kind::IS_INTEGER: |
603 |
|
op << "IS_INTEGER"; |
604 |
|
opType = PREFIX; |
605 |
|
break; |
606 |
|
case kind::TO_INTEGER: |
607 |
|
op << "FLOOR"; |
608 |
|
opType = PREFIX; |
609 |
|
break; |
610 |
|
case kind::TO_REAL: |
611 |
|
case kind::CAST_TO_REAL: |
612 |
|
{ |
613 |
|
if (n[0].getKind() == kind::CONST_RATIONAL) |
614 |
|
{ |
615 |
|
// print the constant as a rational |
616 |
|
toStreamRational(out, n[0], true); |
617 |
|
} |
618 |
|
else |
619 |
|
{ |
620 |
|
// ignore, there is no to-real in CVC language |
621 |
|
toStreamNode(out, n[0], depth, false, lbind); |
622 |
|
} |
623 |
|
return; |
624 |
|
} |
625 |
|
case kind::DIVISIBLE: |
626 |
|
out << "DIVISIBLE("; |
627 |
|
toStreamNode(out, n[0], depth, false, lbind); |
628 |
|
out << ", " << n.getOperator().getConst<Divisible>().k << ")"; |
629 |
|
return; |
630 |
|
|
631 |
|
// BITVECTORS |
632 |
|
case kind::BITVECTOR_XOR: |
633 |
|
op << "BVXOR"; |
634 |
|
break; |
635 |
|
case kind::BITVECTOR_NAND: |
636 |
|
op << "BVNAND"; |
637 |
|
break; |
638 |
|
case kind::BITVECTOR_NOR: |
639 |
|
op << "BVNOR"; |
640 |
|
break; |
641 |
|
case kind::BITVECTOR_XNOR: |
642 |
|
op << "BVXNOR"; |
643 |
|
break; |
644 |
|
case kind::BITVECTOR_COMP: |
645 |
|
op << "BVCOMP"; |
646 |
|
break; |
647 |
|
case kind::BITVECTOR_UDIV: |
648 |
|
op << "BVUDIV"; |
649 |
|
break; |
650 |
|
case kind::BITVECTOR_UREM: |
651 |
|
op << "BVUREM"; |
652 |
|
break; |
653 |
|
case kind::BITVECTOR_SDIV: |
654 |
|
op << "BVSDIV"; |
655 |
|
break; |
656 |
|
case kind::BITVECTOR_SREM: |
657 |
|
op << "BVSREM"; |
658 |
|
break; |
659 |
|
case kind::BITVECTOR_SMOD: |
660 |
|
op << "BVSMOD"; |
661 |
|
break; |
662 |
|
case kind::BITVECTOR_SHL: |
663 |
|
op << "BVSHL"; |
664 |
|
break; |
665 |
|
case kind::BITVECTOR_LSHR: |
666 |
|
op << "BVLSHR"; |
667 |
|
break; |
668 |
|
case kind::BITVECTOR_ASHR: |
669 |
|
op << "BVASHR"; |
670 |
|
break; |
671 |
|
case kind::BITVECTOR_ULT: |
672 |
|
op << "BVLT"; |
673 |
|
break; |
674 |
|
case kind::BITVECTOR_ULE: |
675 |
|
op << "BVLE"; |
676 |
|
break; |
677 |
|
case kind::BITVECTOR_UGT: |
678 |
|
op << "BVGT"; |
679 |
|
break; |
680 |
|
case kind::BITVECTOR_UGE: |
681 |
|
op << "BVGE"; |
682 |
|
break; |
683 |
|
case kind::BITVECTOR_SLT: |
684 |
|
op << "BVSLT"; |
685 |
|
break; |
686 |
|
case kind::BITVECTOR_SLE: |
687 |
|
op << "BVSLE"; |
688 |
|
break; |
689 |
|
case kind::BITVECTOR_SGT: |
690 |
|
op << "BVSGT"; |
691 |
|
break; |
692 |
|
case kind::BITVECTOR_SGE: |
693 |
|
op << "BVSGE"; |
694 |
|
break; |
695 |
|
case kind::BITVECTOR_NEG: |
696 |
|
op << "BVUMINUS"; |
697 |
|
break; |
698 |
4 |
case kind::BITVECTOR_NOT: |
699 |
4 |
op << "~"; |
700 |
4 |
break; |
701 |
|
case kind::BITVECTOR_AND: |
702 |
|
op << "&"; |
703 |
|
opType = INFIX; |
704 |
|
break; |
705 |
|
case kind::BITVECTOR_OR: |
706 |
|
op << "|"; |
707 |
|
opType = INFIX; |
708 |
|
break; |
709 |
|
case kind::BITVECTOR_CONCAT: |
710 |
|
op << "@"; |
711 |
|
opType = INFIX; |
712 |
|
break; |
713 |
4 |
case kind::BITVECTOR_ADD: |
714 |
|
{ |
715 |
|
// This interprets a BITVECTOR_ADD as a bvadd in SMT-LIB |
716 |
4 |
Assert(n.getType().isBitVector()); |
717 |
4 |
unsigned numc = n.getNumChildren()-2; |
718 |
4 |
unsigned child = 0; |
719 |
4 |
while (child < numc) { |
720 |
|
out << "BVPLUS("; |
721 |
|
out << n.getType().getBitVectorSize(); |
722 |
|
out << ','; |
723 |
|
toStreamNode(out, n[child], depth, false, lbind); |
724 |
|
out << ','; |
725 |
|
++child; |
726 |
|
} |
727 |
4 |
out << "BVPLUS("; |
728 |
4 |
out << n.getType().getBitVectorSize(); |
729 |
4 |
out << ','; |
730 |
4 |
toStreamNode(out, n[child], depth, false, lbind); |
731 |
4 |
out << ','; |
732 |
4 |
toStreamNode(out, n[child + 1], depth, false, lbind); |
733 |
4 |
while (child > 0) { |
734 |
|
out << ')'; |
735 |
|
--child; |
736 |
|
} |
737 |
4 |
out << ')'; |
738 |
4 |
return; |
739 |
|
break; |
740 |
|
} |
741 |
|
case kind::BITVECTOR_SUB: |
742 |
|
out << "BVSUB("; |
743 |
|
Assert(n.getType().isBitVector()); |
744 |
|
out << n.getType().getBitVectorSize(); |
745 |
|
out << ','; |
746 |
|
toStreamNode(out, n[0], depth, false, lbind); |
747 |
|
out << ','; |
748 |
|
toStreamNode(out, n[1], depth, false, lbind); |
749 |
|
out << ')'; |
750 |
|
return; |
751 |
|
break; |
752 |
2 |
case kind::BITVECTOR_MULT: { |
753 |
2 |
Assert(n.getType().isBitVector()); |
754 |
2 |
unsigned numc = n.getNumChildren()-2; |
755 |
2 |
unsigned child = 0; |
756 |
2 |
while (child < numc) { |
757 |
|
out << "BVMULT("; |
758 |
|
out << n.getType().getBitVectorSize(); |
759 |
|
out << ','; |
760 |
|
toStreamNode(out, n[child], depth, false, lbind); |
761 |
|
out << ','; |
762 |
|
++child; |
763 |
|
} |
764 |
2 |
out << "BVMULT("; |
765 |
2 |
out << n.getType().getBitVectorSize(); |
766 |
2 |
out << ','; |
767 |
2 |
toStreamNode(out, n[child], depth, false, lbind); |
768 |
2 |
out << ','; |
769 |
2 |
toStreamNode(out, n[child + 1], depth, false, lbind); |
770 |
2 |
while (child > 0) { |
771 |
|
out << ')'; |
772 |
|
--child; |
773 |
|
} |
774 |
2 |
out << ')'; |
775 |
2 |
return; |
776 |
|
break; |
777 |
|
} |
778 |
4 |
case kind::BITVECTOR_EXTRACT: |
779 |
4 |
op << n.getOperator().getConst<BitVectorExtract>(); |
780 |
4 |
opType = POSTFIX; |
781 |
4 |
break; |
782 |
|
case kind::BITVECTOR_BITOF: |
783 |
|
op << n.getOperator().getConst<BitVectorBitOf>(); |
784 |
|
opType = POSTFIX; |
785 |
|
break; |
786 |
|
case kind::BITVECTOR_REPEAT: |
787 |
|
out << "BVREPEAT("; |
788 |
|
toStreamNode(out, n[0], depth, false, lbind); |
789 |
|
out << ", " << n.getOperator().getConst<BitVectorRepeat>() << ')'; |
790 |
|
return; |
791 |
|
break; |
792 |
8 |
case kind::BITVECTOR_ZERO_EXTEND: |
793 |
8 |
out << "BVZEROEXTEND("; |
794 |
8 |
toStreamNode(out, n[0], depth, false, lbind); |
795 |
8 |
out << ", " << n.getOperator().getConst<BitVectorZeroExtend>() << ')'; |
796 |
8 |
return; |
797 |
|
break; |
798 |
|
case kind::BITVECTOR_SIGN_EXTEND: |
799 |
|
out << "SX("; |
800 |
|
toStreamNode(out, n[0], depth, false, lbind); |
801 |
|
out << ", " << n.getType().getBitVectorSize() << ')'; |
802 |
|
return; |
803 |
|
break; |
804 |
|
case kind::BITVECTOR_ROTATE_LEFT: |
805 |
|
out << "BVROTL("; |
806 |
|
toStreamNode(out, n[0], depth, false, lbind); |
807 |
|
out << ", " << n.getOperator().getConst<BitVectorRotateLeft>() << ')'; |
808 |
|
return; |
809 |
|
break; |
810 |
|
case kind::BITVECTOR_ROTATE_RIGHT: |
811 |
|
out << "BVROTR("; |
812 |
|
toStreamNode(out, n[0], depth, false, lbind); |
813 |
|
out << ", " << n.getOperator().getConst<BitVectorRotateRight>() << ')'; |
814 |
|
return; |
815 |
|
break; |
816 |
|
|
817 |
|
// SETS |
818 |
46 |
case kind::SET_TYPE: |
819 |
46 |
out << "SET OF "; |
820 |
46 |
toStreamNode(out, n[0], depth, false, lbind); |
821 |
46 |
return; |
822 |
|
break; |
823 |
|
case kind::UNION: |
824 |
|
op << '|'; |
825 |
|
opType = INFIX; |
826 |
|
break; |
827 |
|
case kind::INTERSECTION: |
828 |
|
op << '&'; |
829 |
|
opType = INFIX; |
830 |
|
break; |
831 |
|
case kind::SETMINUS: |
832 |
|
op << '-'; |
833 |
|
opType = INFIX; |
834 |
|
break; |
835 |
|
case kind::SUBSET: |
836 |
|
op << "<="; |
837 |
|
opType = INFIX; |
838 |
|
break; |
839 |
|
case kind::MEMBER: |
840 |
|
op << "IS_IN"; |
841 |
|
opType = INFIX; |
842 |
|
break; |
843 |
|
case kind::COMPLEMENT: |
844 |
|
op << "~"; |
845 |
|
opType = PREFIX; |
846 |
|
break; |
847 |
|
case kind::PRODUCT: |
848 |
|
op << "PRODUCT"; |
849 |
|
opType = INFIX; |
850 |
|
break; |
851 |
|
case kind::JOIN: |
852 |
|
op << "JOIN"; |
853 |
|
opType = INFIX; |
854 |
|
break; |
855 |
|
case kind::TRANSPOSE: |
856 |
|
op << "TRANSPOSE"; |
857 |
|
opType = PREFIX; |
858 |
|
break; |
859 |
|
case kind::TCLOSURE: |
860 |
|
op << "TCLOSURE"; |
861 |
|
opType = PREFIX; |
862 |
|
break; |
863 |
|
case kind::IDEN: |
864 |
|
op << "IDEN"; |
865 |
|
opType = PREFIX; |
866 |
|
break; |
867 |
|
case kind::JOIN_IMAGE: |
868 |
|
op << "JOIN_IMAGE"; |
869 |
|
opType = INFIX; |
870 |
|
break; |
871 |
3 |
case kind::SINGLETON: |
872 |
3 |
out << "{"; |
873 |
3 |
toStreamNode(out, n[0], depth, false, lbind); |
874 |
3 |
out << "}"; |
875 |
3 |
return; |
876 |
|
break; |
877 |
|
case kind::INSERT: { |
878 |
|
if(bracket) { |
879 |
|
out << '('; |
880 |
|
} |
881 |
|
out << '{'; |
882 |
|
size_t i = 0; |
883 |
|
toStreamNode(out, n[i++], depth, false, lbind); |
884 |
|
for(;i+1 < n.getNumChildren(); ++i) { |
885 |
|
out << ", "; |
886 |
|
toStreamNode(out, n[i], depth, false, lbind); |
887 |
|
} |
888 |
|
out << "} | "; |
889 |
|
toStreamNode(out, n[i], depth, true, lbind); |
890 |
|
if(bracket) { |
891 |
|
out << ')'; |
892 |
|
} |
893 |
|
return; |
894 |
|
break; |
895 |
|
} |
896 |
|
case kind::CARD: { |
897 |
|
out << "CARD("; |
898 |
|
toStreamNode(out, n[0], depth, false, lbind); |
899 |
|
out << ")"; |
900 |
|
return; |
901 |
|
break; |
902 |
|
} |
903 |
|
|
904 |
|
// Quantifiers |
905 |
|
case kind::FORALL: |
906 |
|
out << "(FORALL"; |
907 |
|
toStreamNode(out, n[0], depth, true, lbind); |
908 |
|
out << " : "; |
909 |
|
toStreamNodeWithLetify(out, n[1], depth, true, lbind); |
910 |
|
out << ')'; |
911 |
|
// TODO: user patterns? |
912 |
|
return; |
913 |
|
case kind::EXISTS: |
914 |
|
out << "(EXISTS"; |
915 |
|
toStreamNode(out, n[0], depth, true, lbind); |
916 |
|
out << " : "; |
917 |
|
toStreamNodeWithLetify(out, n[1], depth, true, lbind); |
918 |
|
out << ')'; |
919 |
|
// TODO: user patterns? |
920 |
|
return; |
921 |
|
case kind::INST_CONSTANT: |
922 |
|
out << "INST_CONSTANT"; |
923 |
|
break; |
924 |
2 |
case kind::BOUND_VAR_LIST: |
925 |
2 |
out << '('; |
926 |
4 |
for(size_t i = 0; i < n.getNumChildren(); ++i) { |
927 |
2 |
if(i > 0) { |
928 |
|
out << ", "; |
929 |
|
} |
930 |
2 |
toStreamNode(out, n[i], -1, false, lbind); |
931 |
2 |
out << ":"; |
932 |
2 |
n[i].getType().toStream(out, language::output::LANG_CVC); |
933 |
2 |
} |
934 |
2 |
out << ')'; |
935 |
2 |
return; |
936 |
|
case kind::INST_PATTERN: |
937 |
|
out << "INST_PATTERN"; |
938 |
|
break; |
939 |
|
case kind::INST_PATTERN_LIST: |
940 |
|
out << "INST_PATTERN_LIST"; |
941 |
|
break; |
942 |
|
|
943 |
|
// string operators |
944 |
|
case kind::STRING_CONCAT: |
945 |
|
out << "CONCAT"; |
946 |
|
break; |
947 |
|
case kind::STRING_CHARAT: |
948 |
|
out << "CHARAT"; |
949 |
|
break; |
950 |
|
case kind::STRING_LENGTH: |
951 |
|
out << "LENGTH"; |
952 |
|
break; |
953 |
|
case kind::STRING_SUBSTR: out << "SUBSTR"; break; |
954 |
|
|
955 |
|
default: |
956 |
|
Warning() << "Kind printing not implemented for the case of " << n.getKind() << endl; |
957 |
|
break; |
958 |
|
} |
959 |
|
|
960 |
955 |
switch (opType) { |
961 |
725 |
case PREFIX: |
962 |
725 |
out << op.str(); |
963 |
725 |
if (n.getNumChildren() > 0) |
964 |
|
{ |
965 |
725 |
out << '('; |
966 |
|
} |
967 |
725 |
break; |
968 |
226 |
case INFIX: |
969 |
226 |
if (bracket) { |
970 |
106 |
out << '('; |
971 |
|
} |
972 |
226 |
break; |
973 |
4 |
case POSTFIX: |
974 |
4 |
out << '('; |
975 |
4 |
break; |
976 |
|
} |
977 |
|
|
978 |
2841 |
for (unsigned i = 0; i < n.getNumChildren(); ++ i) { |
979 |
1886 |
if (i > 0) { |
980 |
931 |
if (opType == INFIX) { |
981 |
316 |
out << ' ' << op.str() << ' '; |
982 |
|
} else { |
983 |
615 |
out << ", "; |
984 |
|
} |
985 |
|
} |
986 |
1886 |
toStreamNode(out, n[i], depth, opType == INFIX, lbind); |
987 |
|
} |
988 |
|
|
989 |
955 |
switch (opType) { |
990 |
725 |
case PREFIX: |
991 |
725 |
if (n.getNumChildren() > 0) |
992 |
|
{ |
993 |
725 |
out << ')'; |
994 |
|
} |
995 |
725 |
break; |
996 |
226 |
case INFIX: |
997 |
226 |
if (bracket) { |
998 |
106 |
out << ')'; |
999 |
|
} |
1000 |
226 |
break; |
1001 |
4 |
case POSTFIX: |
1002 |
4 |
out << ')' << op.str(); |
1003 |
4 |
break; |
1004 |
|
} |
1005 |
|
} |
1006 |
|
|
1007 |
|
template <class T> |
1008 |
|
static bool tryToStream(std::ostream& out, const Command* c, bool cvc3Mode); |
1009 |
|
|
1010 |
|
template <class T> |
1011 |
|
static bool tryToStream(std::ostream& out, |
1012 |
|
const CommandStatus* s, |
1013 |
|
bool cvc3Mode); |
1014 |
|
|
1015 |
17035 |
void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const |
1016 |
|
{ |
1017 |
34070 |
if (tryToStream<CommandSuccess>(out, s, d_cvc3Mode) |
1018 |
8 |
|| tryToStream<CommandFailure>(out, s, d_cvc3Mode) |
1019 |
3 |
|| tryToStream<CommandRecoverableFailure>(out, s, d_cvc3Mode) |
1020 |
|
|| tryToStream<CommandUnsupported>(out, s, d_cvc3Mode) |
1021 |
17035 |
|| tryToStream<CommandInterrupted>(out, s, d_cvc3Mode)) |
1022 |
|
{ |
1023 |
17035 |
return; |
1024 |
|
} |
1025 |
|
|
1026 |
|
out << "ERROR: don't know how to print a CommandStatus of class: " |
1027 |
|
<< typeid(*s).name() << endl; |
1028 |
|
|
1029 |
|
}/* CvcPrinter::toStream(CommandStatus*) */ |
1030 |
|
|
1031 |
|
void CvcPrinter::toStreamModelSort(std::ostream& out, |
1032 |
|
const smt::Model& m, |
1033 |
|
TypeNode tn) const |
1034 |
|
{ |
1035 |
|
if (!tn.isSort()) |
1036 |
|
{ |
1037 |
|
out << "ERROR: don't know how to print a non uninterpreted sort in model: " |
1038 |
|
<< tn << std::endl; |
1039 |
|
return; |
1040 |
|
} |
1041 |
|
const theory::TheoryModel* tm = m.getTheoryModel(); |
1042 |
|
const std::vector<Node>* type_reps = tm->getRepSet()->getTypeRepsOrNull(tn); |
1043 |
45 |
if (options::modelUninterpPrint() == options::ModelUninterpPrintMode::DtEnum |
1044 |
|
&& type_reps != nullptr) |
1045 |
|
{ |
1046 |
|
out << "DATATYPE" << std::endl; |
1047 |
|
out << " " << tn << " = "; |
1048 |
|
for (size_t i = 0; i < type_reps->size(); i++) |
1049 |
|
{ |
1050 |
|
if (i > 0) |
1051 |
|
{ |
1052 |
|
out << "| "; |
1053 |
|
} |
1054 |
|
out << (*type_reps)[i] << " "; |
1055 |
|
} |
1056 |
|
out << std::endl << "END;" << std::endl; |
1057 |
|
} |
1058 |
|
else if (type_reps != nullptr) |
1059 |
|
{ |
1060 |
|
out << "% cardinality of " << tn << " is " << type_reps->size() |
1061 |
|
<< std::endl; |
1062 |
|
toStreamCmdDeclareType(out, tn); |
1063 |
|
for (Node type_rep : *type_reps) |
1064 |
|
{ |
1065 |
|
if (type_rep.isVar()) |
1066 |
|
{ |
1067 |
|
out << type_rep << " : " << tn << ";" << std::endl; |
1068 |
|
} |
1069 |
|
else |
1070 |
|
{ |
1071 |
|
out << "% rep: " << type_rep << std::endl; |
1072 |
|
} |
1073 |
|
} |
1074 |
|
} |
1075 |
|
else |
1076 |
|
{ |
1077 |
|
toStreamCmdDeclareType(out, tn); |
1078 |
|
} |
1079 |
|
} |
1080 |
|
|
1081 |
6 |
void CvcPrinter::toStreamModelTerm(std::ostream& out, |
1082 |
|
const smt::Model& m, |
1083 |
|
Node n) const |
1084 |
|
{ |
1085 |
6 |
const theory::TheoryModel* tm = m.getTheoryModel(); |
1086 |
12 |
TypeNode tn = n.getType(); |
1087 |
6 |
out << n << " : "; |
1088 |
6 |
if (tn.isFunction() || tn.isPredicate()) |
1089 |
|
{ |
1090 |
2 |
out << "("; |
1091 |
4 |
for (size_t i = 0; i < tn.getNumChildren() - 1; i++) |
1092 |
|
{ |
1093 |
2 |
if (i > 0) |
1094 |
|
{ |
1095 |
|
out << ", "; |
1096 |
|
} |
1097 |
2 |
out << tn[i]; |
1098 |
|
} |
1099 |
2 |
out << ") -> " << tn.getRangeType(); |
1100 |
|
} |
1101 |
|
else |
1102 |
|
{ |
1103 |
4 |
out << tn; |
1104 |
|
} |
1105 |
|
// We get the value from the theory model directly, which notice |
1106 |
|
// does not have to go through the standard SmtEngine::getValue interface. |
1107 |
12 |
Node val = tm->getValue(n); |
1108 |
12 |
if (options::modelUninterpPrint() == options::ModelUninterpPrintMode::DtEnum |
1109 |
6 |
&& val.getKind() == kind::STORE) |
1110 |
|
{ |
1111 |
|
TypeNode type_node = val[1].getType(); |
1112 |
|
if (tn.isSort()) |
1113 |
|
{ |
1114 |
|
const std::vector<Node>* type_reps = |
1115 |
|
tm->getRepSet()->getTypeRepsOrNull(type_node); |
1116 |
|
if (type_reps != nullptr) |
1117 |
|
{ |
1118 |
|
Cardinality indexCard(type_reps->size()); |
1119 |
|
val = theory::arrays::TheoryArraysRewriter::normalizeConstant( |
1120 |
|
val, indexCard); |
1121 |
|
} |
1122 |
|
} |
1123 |
|
} |
1124 |
6 |
out << " = " << val << ";" << std::endl; |
1125 |
6 |
} |
1126 |
|
|
1127 |
4 |
void CvcPrinter::toStream(std::ostream& out, const smt::Model& m) const |
1128 |
|
{ |
1129 |
4 |
const theory::TheoryModel* tm = m.getTheoryModel(); |
1130 |
|
// print the model comments |
1131 |
8 |
std::stringstream c; |
1132 |
4 |
tm->getComments(c); |
1133 |
8 |
std::string ln; |
1134 |
4 |
while (std::getline(c, ln)) |
1135 |
|
{ |
1136 |
|
out << "; " << ln << std::endl; |
1137 |
|
} |
1138 |
|
|
1139 |
|
// print the model |
1140 |
4 |
out << "MODEL BEGIN" << std::endl; |
1141 |
4 |
this->Printer::toStream(out, m); |
1142 |
4 |
out << "MODEL END;" << std::endl; |
1143 |
4 |
} |
1144 |
|
|
1145 |
|
void CvcPrinter::toStreamCmdAssert(std::ostream& out, Node n) const |
1146 |
|
{ |
1147 |
|
out << "ASSERT " << n << ';' << std::endl; |
1148 |
|
} |
1149 |
|
|
1150 |
|
void CvcPrinter::toStreamCmdPush(std::ostream& out) const |
1151 |
|
{ |
1152 |
|
out << "PUSH;" << std::endl; |
1153 |
|
} |
1154 |
|
|
1155 |
|
void CvcPrinter::toStreamCmdPop(std::ostream& out) const |
1156 |
|
{ |
1157 |
|
out << "POP;" << std::endl; |
1158 |
|
} |
1159 |
|
|
1160 |
|
void CvcPrinter::toStreamCmdCheckSat(std::ostream& out, Node n) const |
1161 |
|
{ |
1162 |
|
if (d_cvc3Mode) |
1163 |
|
{ |
1164 |
|
out << "PUSH; "; |
1165 |
|
} |
1166 |
|
if (!n.isNull()) |
1167 |
|
{ |
1168 |
|
out << "CHECKSAT " << n << ';'; |
1169 |
|
} |
1170 |
|
else |
1171 |
|
{ |
1172 |
|
out << "CHECKSAT;"; |
1173 |
|
} |
1174 |
|
if (d_cvc3Mode) |
1175 |
|
{ |
1176 |
|
out << " POP;"; |
1177 |
|
} |
1178 |
|
out << std::endl; |
1179 |
|
} |
1180 |
|
|
1181 |
|
void CvcPrinter::toStreamCmdCheckSatAssuming( |
1182 |
|
std::ostream& out, const std::vector<Node>& nodes) const |
1183 |
|
{ |
1184 |
|
if (d_cvc3Mode) |
1185 |
|
{ |
1186 |
|
out << "PUSH; "; |
1187 |
|
} |
1188 |
|
out << "CHECKSAT"; |
1189 |
|
if (nodes.size() > 0) |
1190 |
|
{ |
1191 |
|
out << ' ' << nodes[0]; |
1192 |
|
for (size_t i = 1, n = nodes.size(); i < n; ++i) |
1193 |
|
{ |
1194 |
|
out << " AND " << nodes[i]; |
1195 |
|
} |
1196 |
|
} |
1197 |
|
out << ';'; |
1198 |
|
if (d_cvc3Mode) |
1199 |
|
{ |
1200 |
|
out << " POP;"; |
1201 |
|
} |
1202 |
|
out << std::endl; |
1203 |
|
} |
1204 |
|
|
1205 |
|
void CvcPrinter::toStreamCmdQuery(std::ostream& out, Node n) const |
1206 |
|
{ |
1207 |
|
if (d_cvc3Mode) |
1208 |
|
{ |
1209 |
|
out << "PUSH; "; |
1210 |
|
} |
1211 |
|
if (!n.isNull()) |
1212 |
|
{ |
1213 |
|
out << "QUERY " << n << ';'; |
1214 |
|
} |
1215 |
|
else |
1216 |
|
{ |
1217 |
|
out << "QUERY TRUE;"; |
1218 |
|
} |
1219 |
|
if (d_cvc3Mode) |
1220 |
|
{ |
1221 |
|
out << " POP;"; |
1222 |
|
} |
1223 |
|
out << std::endl; |
1224 |
|
} |
1225 |
|
|
1226 |
|
void CvcPrinter::toStreamCmdReset(std::ostream& out) const |
1227 |
|
{ |
1228 |
|
out << "RESET;" << std::endl; |
1229 |
|
} |
1230 |
|
|
1231 |
|
void CvcPrinter::toStreamCmdResetAssertions(std::ostream& out) const |
1232 |
|
{ |
1233 |
|
out << "RESET ASSERTIONS;" << std::endl; |
1234 |
|
} |
1235 |
|
|
1236 |
|
void CvcPrinter::toStreamCmdQuit(std::ostream& out) const |
1237 |
|
{ |
1238 |
|
// out << "EXIT;" << std::endl; |
1239 |
|
} |
1240 |
|
|
1241 |
|
void CvcPrinter::toStreamCmdCommandSequence( |
1242 |
|
std::ostream& out, const std::vector<Command*>& sequence) const |
1243 |
|
{ |
1244 |
|
for (CommandSequence::const_iterator i = sequence.cbegin(); |
1245 |
|
i != sequence.cend(); |
1246 |
|
++i) |
1247 |
|
{ |
1248 |
|
out << *i; |
1249 |
|
} |
1250 |
|
} |
1251 |
|
|
1252 |
|
void CvcPrinter::toStreamCmdDeclarationSequence( |
1253 |
|
std::ostream& out, const std::vector<Command*>& sequence) const |
1254 |
|
{ |
1255 |
|
DeclarationSequence::const_iterator i = sequence.cbegin(); |
1256 |
|
for (;;) |
1257 |
|
{ |
1258 |
|
DeclarationDefinitionCommand* dd = |
1259 |
|
static_cast<DeclarationDefinitionCommand*>(*i++); |
1260 |
|
Assert(dd != nullptr); |
1261 |
|
if (i != sequence.cend()) |
1262 |
|
{ |
1263 |
|
out << dd->getSymbol() << ", "; |
1264 |
|
} |
1265 |
|
else |
1266 |
|
{ |
1267 |
|
out << *dd; |
1268 |
|
break; |
1269 |
|
} |
1270 |
|
} |
1271 |
|
out << std::endl; |
1272 |
|
} |
1273 |
|
|
1274 |
|
void CvcPrinter::toStreamCmdDeclareFunction(std::ostream& out, |
1275 |
|
const std::string& id, |
1276 |
|
TypeNode type) const |
1277 |
|
{ |
1278 |
|
out << id << " : " << type << ';' << std::endl; |
1279 |
|
} |
1280 |
|
|
1281 |
|
void CvcPrinter::toStreamCmdDefineFunction(std::ostream& out, |
1282 |
|
const std::string& id, |
1283 |
|
const std::vector<Node>& formals, |
1284 |
|
TypeNode range, |
1285 |
|
Node formula) const |
1286 |
|
{ |
1287 |
|
std::vector<TypeNode> sorts; |
1288 |
|
sorts.reserve(formals.size() + 1); |
1289 |
|
for (const Node& n : formals) |
1290 |
|
{ |
1291 |
|
sorts.push_back(n.getType()); |
1292 |
|
} |
1293 |
|
sorts.push_back(range); |
1294 |
|
|
1295 |
|
out << id << " : " << NodeManager::currentNM()->mkFunctionType(sorts) |
1296 |
|
<< " = "; |
1297 |
|
if (formals.size() > 0) |
1298 |
|
{ |
1299 |
|
out << "LAMBDA("; |
1300 |
|
vector<Node>::const_iterator i = formals.cbegin(); |
1301 |
|
while (i != formals.end()) |
1302 |
|
{ |
1303 |
|
out << (*i) << ":" << (*i).getType(); |
1304 |
|
if (++i != formals.end()) |
1305 |
|
{ |
1306 |
|
out << ", "; |
1307 |
|
} |
1308 |
|
} |
1309 |
|
out << "): "; |
1310 |
|
} |
1311 |
|
out << formula << ';' << std::endl; |
1312 |
|
} |
1313 |
|
|
1314 |
|
void CvcPrinter::toStreamCmdDeclareType(std::ostream& out, |
1315 |
|
TypeNode type) const |
1316 |
|
{ |
1317 |
|
size_t arity = type.isSortConstructor() ? type.getSortConstructorArity() : 0; |
1318 |
|
if (arity > 0) |
1319 |
|
{ |
1320 |
|
out << "ERROR: Don't know how to print parameterized type declaration " |
1321 |
|
"in CVC language." |
1322 |
|
<< std::endl; |
1323 |
|
} |
1324 |
|
else |
1325 |
|
{ |
1326 |
|
out << type << " : TYPE;" << std::endl; |
1327 |
|
} |
1328 |
|
} |
1329 |
|
|
1330 |
|
void CvcPrinter::toStreamCmdDefineType(std::ostream& out, |
1331 |
|
const std::string& id, |
1332 |
|
const std::vector<TypeNode>& params, |
1333 |
|
TypeNode t) const |
1334 |
|
{ |
1335 |
|
if (params.size() > 0) |
1336 |
|
{ |
1337 |
|
out << "ERROR: Don't know how to print parameterized type definition " |
1338 |
|
"in CVC language:" |
1339 |
|
<< std::endl; |
1340 |
|
} |
1341 |
|
else |
1342 |
|
{ |
1343 |
|
out << id << " : TYPE = " << t << ';' << std::endl; |
1344 |
|
} |
1345 |
|
} |
1346 |
|
|
1347 |
|
void CvcPrinter::toStreamCmdSimplify(std::ostream& out, Node n) const |
1348 |
|
{ |
1349 |
|
out << "TRANSFORM " << n << ';' << std::endl; |
1350 |
|
} |
1351 |
|
|
1352 |
|
void CvcPrinter::toStreamCmdGetValue(std::ostream& out, |
1353 |
|
const std::vector<Node>& nodes) const |
1354 |
|
{ |
1355 |
|
Assert(!nodes.empty()); |
1356 |
|
out << "GET_VALUE "; |
1357 |
|
copy(nodes.begin(), |
1358 |
|
nodes.end() - 1, |
1359 |
|
ostream_iterator<Node>(out, ";\nGET_VALUE ")); |
1360 |
|
out << nodes.back() << ';' << std::endl; |
1361 |
|
} |
1362 |
|
|
1363 |
|
void CvcPrinter::toStreamCmdGetModel(std::ostream& out) const |
1364 |
|
{ |
1365 |
|
out << "COUNTERMODEL;" << std::endl; |
1366 |
|
} |
1367 |
|
|
1368 |
|
void CvcPrinter::toStreamCmdGetAssignment(std::ostream& out) const |
1369 |
|
{ |
1370 |
|
out << "% (get-assignment)" << std::endl; |
1371 |
|
} |
1372 |
|
|
1373 |
|
void CvcPrinter::toStreamCmdGetAssertions(std::ostream& out) const |
1374 |
|
{ |
1375 |
|
out << "WHERE;" << std::endl; |
1376 |
|
} |
1377 |
|
|
1378 |
|
void CvcPrinter::toStreamCmdGetProof(std::ostream& out) const |
1379 |
|
{ |
1380 |
|
out << "DUMP_PROOF;" << std::endl; |
1381 |
|
} |
1382 |
|
|
1383 |
|
void CvcPrinter::toStreamCmdGetUnsatCore(std::ostream& out) const |
1384 |
|
{ |
1385 |
|
out << "DUMP_UNSAT_CORE;" << std::endl; |
1386 |
|
} |
1387 |
|
|
1388 |
|
void CvcPrinter::toStreamCmdSetBenchmarkStatus(std::ostream& out, |
1389 |
|
Result::Sat status) const |
1390 |
|
{ |
1391 |
|
out << "% (set-info :status " << status << ')' << std::endl; |
1392 |
|
} |
1393 |
|
|
1394 |
|
void CvcPrinter::toStreamCmdSetBenchmarkLogic(std::ostream& out, |
1395 |
|
const std::string& logic) const |
1396 |
|
{ |
1397 |
|
out << "OPTION \"logic\" \"" << logic << "\";" << std::endl; |
1398 |
|
} |
1399 |
|
|
1400 |
|
void CvcPrinter::toStreamCmdSetInfo(std::ostream& out, |
1401 |
|
const std::string& flag, |
1402 |
|
const std::string& value) const |
1403 |
|
{ |
1404 |
|
out << "% (set-info " << flag << ' ' << value << ')' << std::endl; |
1405 |
|
} |
1406 |
|
|
1407 |
|
void CvcPrinter::toStreamCmdGetInfo(std::ostream& out, |
1408 |
|
const std::string& flag) const |
1409 |
|
{ |
1410 |
|
out << "% (get-info " << flag << ')' << std::endl; |
1411 |
|
} |
1412 |
|
|
1413 |
|
void CvcPrinter::toStreamCmdSetOption(std::ostream& out, |
1414 |
|
const std::string& flag, |
1415 |
|
const std::string& value) const |
1416 |
|
{ |
1417 |
|
out << "OPTION \"" << flag << "\" " << value << ';' << std::endl; |
1418 |
|
} |
1419 |
|
|
1420 |
|
void CvcPrinter::toStreamCmdGetOption(std::ostream& out, |
1421 |
|
const std::string& flag) const |
1422 |
|
{ |
1423 |
|
out << "% (get-option " << flag << ')' << std::endl; |
1424 |
|
} |
1425 |
|
|
1426 |
|
void CvcPrinter::toStreamCmdDatatypeDeclaration( |
1427 |
|
std::ostream& out, const std::vector<TypeNode>& datatypes) const |
1428 |
|
{ |
1429 |
|
Assert(!datatypes.empty() && datatypes[0].isDatatype()); |
1430 |
|
const DType& dt0 = datatypes[0].getDType(); |
1431 |
|
// do not print tuple/datatype internal declarations |
1432 |
|
if (datatypes.size() != 1 || (!dt0.isTuple() && !dt0.isRecord())) |
1433 |
|
{ |
1434 |
|
out << "DATATYPE" << endl; |
1435 |
|
bool firstDatatype = true; |
1436 |
|
for (const TypeNode& t : datatypes) |
1437 |
|
{ |
1438 |
|
if (!firstDatatype) |
1439 |
|
{ |
1440 |
|
out << ',' << endl; |
1441 |
|
} |
1442 |
|
const DType& dt = t.getDType(); |
1443 |
|
out << " " << dt.getName(); |
1444 |
|
if (dt.isParametric()) |
1445 |
|
{ |
1446 |
|
out << '['; |
1447 |
|
for (size_t j = 0; j < dt.getNumParameters(); ++j) |
1448 |
|
{ |
1449 |
|
if (j > 0) |
1450 |
|
{ |
1451 |
|
out << ','; |
1452 |
|
} |
1453 |
|
out << dt.getParameter(j); |
1454 |
|
} |
1455 |
|
out << ']'; |
1456 |
|
} |
1457 |
|
out << " = "; |
1458 |
|
for (size_t j = 0, ncons = dt.getNumConstructors(); j < ncons; j++) |
1459 |
|
{ |
1460 |
|
const DTypeConstructor& cons = dt[j]; |
1461 |
|
if (j != 0) |
1462 |
|
{ |
1463 |
|
out << " | "; |
1464 |
|
} |
1465 |
|
out << cons.getName(); |
1466 |
|
if (cons.getNumArgs() > 0) |
1467 |
|
{ |
1468 |
|
out << '('; |
1469 |
|
for (size_t k = 0, nargs = cons.getNumArgs(); k < nargs; k++) |
1470 |
|
{ |
1471 |
|
if (k != 0) |
1472 |
|
{ |
1473 |
|
out << ", "; |
1474 |
|
} |
1475 |
|
const DTypeSelector& selector = cons[k]; |
1476 |
|
TypeNode tr = selector.getRangeType(); |
1477 |
|
if (tr.isDatatype()) |
1478 |
|
{ |
1479 |
|
const DType& sdt = tr.getDType(); |
1480 |
|
out << selector.getName() << ": " << sdt.getName(); |
1481 |
|
} |
1482 |
|
else |
1483 |
|
{ |
1484 |
|
out << selector.getName() << ": " << tr; |
1485 |
|
} |
1486 |
|
} |
1487 |
|
out << ')'; |
1488 |
|
} |
1489 |
|
} |
1490 |
|
firstDatatype = false; |
1491 |
|
} |
1492 |
|
out << endl << "END;" << std::endl; |
1493 |
|
} |
1494 |
|
} |
1495 |
|
|
1496 |
|
void CvcPrinter::toStreamCmdComment(std::ostream& out, |
1497 |
|
const std::string& comment) const |
1498 |
|
{ |
1499 |
|
out << "% " << comment << std::endl; |
1500 |
|
} |
1501 |
|
|
1502 |
|
void CvcPrinter::toStreamCmdEmpty(std::ostream& out, |
1503 |
|
const std::string& name) const |
1504 |
|
{ |
1505 |
|
out << std::endl; |
1506 |
|
} |
1507 |
|
|
1508 |
|
void CvcPrinter::toStreamCmdEcho(std::ostream& out, |
1509 |
|
const std::string& output) const |
1510 |
|
{ |
1511 |
|
out << "ECHO \"" << output << "\";" << std::endl; |
1512 |
|
} |
1513 |
|
|
1514 |
|
template <class T> |
1515 |
|
static bool tryToStream(std::ostream& out, const Command* c, bool cvc3Mode) |
1516 |
|
{ |
1517 |
|
if(typeid(*c) == typeid(T)) { |
1518 |
|
toStream(out, dynamic_cast<const T*>(c), cvc3Mode); |
1519 |
|
return true; |
1520 |
|
} |
1521 |
|
return false; |
1522 |
|
} |
1523 |
|
|
1524 |
17027 |
static void toStream(std::ostream& out, const CommandSuccess* s, bool cvc3Mode) |
1525 |
|
{ |
1526 |
17027 |
if(Command::printsuccess::getPrintSuccess(out)) { |
1527 |
|
out << "OK" << endl; |
1528 |
|
} |
1529 |
17027 |
} |
1530 |
|
|
1531 |
|
static void toStream(std::ostream& out, |
1532 |
|
const CommandUnsupported* s, |
1533 |
|
bool cvc3Mode) |
1534 |
|
{ |
1535 |
|
out << "UNSUPPORTED" << endl; |
1536 |
|
} |
1537 |
|
|
1538 |
|
static void toStream(std::ostream& out, |
1539 |
|
const CommandInterrupted* s, |
1540 |
|
bool cvc3Mode) |
1541 |
|
{ |
1542 |
|
out << "INTERRUPTED" << endl; |
1543 |
|
} |
1544 |
|
|
1545 |
5 |
static void toStream(std::ostream& out, const CommandFailure* s, bool cvc3Mode) |
1546 |
|
{ |
1547 |
5 |
out << s->getMessage() << endl; |
1548 |
5 |
} |
1549 |
|
|
1550 |
3 |
static void toStream(std::ostream& out, |
1551 |
|
const CommandRecoverableFailure* s, |
1552 |
|
bool cvc3Mode) |
1553 |
|
{ |
1554 |
3 |
out << s->getMessage() << endl; |
1555 |
3 |
} |
1556 |
|
|
1557 |
|
template <class T> |
1558 |
17046 |
static bool tryToStream(std::ostream& out, |
1559 |
|
const CommandStatus* s, |
1560 |
|
bool cvc3Mode) |
1561 |
|
{ |
1562 |
17046 |
if(typeid(*s) == typeid(T)) { |
1563 |
17035 |
toStream(out, dynamic_cast<const T*>(s), cvc3Mode); |
1564 |
17035 |
return true; |
1565 |
|
} |
1566 |
11 |
return false; |
1567 |
|
} |
1568 |
|
|
1569 |
959 |
void CvcPrinter::toStreamNodeWithLetify(std::ostream& out, |
1570 |
|
Node n, |
1571 |
|
int toDepth, |
1572 |
|
bool bracket, |
1573 |
|
LetBinding* lbind) const |
1574 |
|
{ |
1575 |
959 |
if (lbind == nullptr) |
1576 |
|
{ |
1577 |
2 |
toStreamNode(out, n, toDepth, bracket, nullptr); |
1578 |
2 |
return; |
1579 |
|
} |
1580 |
1914 |
std::vector<Node> letList; |
1581 |
957 |
lbind->letify(n, letList); |
1582 |
957 |
if (!letList.empty()) |
1583 |
|
{ |
1584 |
12 |
std::map<Node, uint32_t>::const_iterator it; |
1585 |
12 |
out << "LET "; |
1586 |
12 |
bool first = true; |
1587 |
64 |
for (size_t i = 0, nlets = letList.size(); i < nlets; i++) |
1588 |
|
{ |
1589 |
52 |
if (!first) |
1590 |
|
{ |
1591 |
40 |
out << ", "; |
1592 |
|
} |
1593 |
|
else |
1594 |
|
{ |
1595 |
12 |
first = false; |
1596 |
|
} |
1597 |
104 |
Node nl = letList[i]; |
1598 |
52 |
uint32_t id = lbind->getId(nl); |
1599 |
52 |
out << "_let_" << id << " = "; |
1600 |
104 |
Node nlc = lbind->convert(nl, "_let_", false); |
1601 |
52 |
toStreamNode(out, nlc, toDepth, true, lbind); |
1602 |
|
} |
1603 |
12 |
out << " IN "; |
1604 |
|
} |
1605 |
1914 |
Node nc = lbind->convert(n, "_let_"); |
1606 |
|
// print the body, passing the lbind object |
1607 |
957 |
toStreamNode(out, nc, toDepth, bracket, lbind); |
1608 |
957 |
lbind->popScope(); |
1609 |
|
} |
1610 |
|
|
1611 |
|
} // namespace cvc |
1612 |
|
} // namespace printer |
1613 |
29322 |
} // namespace cvc5 |