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