1 /*++
2 Copyright (c) 2008 Microsoft Corporation
3
4 Module Name:
5
6 ast_smt_pp.cpp
7
8 Abstract:
9
10 Pretty printer of AST formulas as SMT benchmarks.
11
12 Author:
13
14 Michal Moskal (micmo) 2008-04-09.
15 Nikolaj Bjorner (nbjorner)
16
17 Revision History:
18
19
20 --*/
21
22 #include<sstream>
23 #include<iostream>
24 #include "util/vector.h"
25 #include "util/smt2_util.h"
26 #include "ast/ast_smt_pp.h"
27 #include "ast/ast_smt2_pp.h"
28 #include "ast/arith_decl_plugin.h"
29 #include "ast/bv_decl_plugin.h"
30 #include "ast/array_decl_plugin.h"
31 #include "ast/datatype_decl_plugin.h"
32 #include "ast/seq_decl_plugin.h"
33 #include "ast/fpa_decl_plugin.h"
34 #include "ast/for_each_ast.h"
35 #include "ast/decl_collector.h"
36 #include "math/polynomial/algebraic_numbers.h"
37
38
39 // ---------------------------------------
40 // smt_renaming
41
42 static const char m_predef_names[][8] = {
43 "=", ">=", "<=", "+", "-", "*", ">", "<", "!=", "or", "and", "implies", "not", "iff", "xor",
44 "true", "false", "forall", "exists", "let", "flet"
45 };
46
fix_symbol(symbol s,int k)47 symbol smt_renaming::fix_symbol(symbol s, int k) {
48 std::ostringstream buffer;
49 char const * data = s.is_numerical() ? "" : s.bare_str();
50
51 if (k == 0 && data && *data) {
52 if (s.is_numerical()) {
53 return s;
54 }
55 if (is_special(data)) {
56 return s;
57 }
58 if (all_is_legal(data)) {
59 return s;
60 }
61 }
62
63 if (s.is_numerical()) {
64 buffer << s << k;
65 return symbol(buffer.str());
66 }
67
68 if (!s.bare_str()) {
69 buffer << "null";
70 }
71 else if (is_smt2_quoted_symbol(s)) {
72 buffer << mk_smt2_quoted_symbol(s);
73 }
74 else {
75 buffer << s;
76 }
77 if (k > 0) {
78 buffer << "!" << k;
79 }
80
81 return symbol(buffer.str());
82 }
83
is_legal(char c)84 bool smt_renaming::is_legal(char c) {
85 return c == '.' || c == '_' || c == '\''
86 || c == '?' || c == '!' || isalnum(c);
87 }
88
is_special(char const * s)89 bool smt_renaming::is_special(char const* s) {
90 if (!s) return false;
91 if (s[0] != '|') return false;
92 ++s;
93 while (*s) {
94 if (s[0] == '|') {
95 return (0 == s[1]);
96 }
97 ++s;
98 }
99 return false;
100 }
101
is_numerical(char const * s)102 bool smt_renaming::is_numerical(char const* s) {
103 while (*s) {
104 if (!isdigit(*s)) {
105 return false;
106 }
107 ++s;
108 }
109 return true;
110 }
111
all_is_legal(char const * s)112 bool smt_renaming::all_is_legal(char const* s) {
113 if (!s) return false;
114 if (is_numerical(s)) return false;
115 while (*s) {
116 if (!is_legal(*s)) return false;
117 ++s;
118 }
119 return true;
120 }
121
smt_renaming()122 smt_renaming::smt_renaming() {
123 for (unsigned i = 0; i < Z3_ARRAYSIZE(m_predef_names); ++i) {
124 symbol s(m_predef_names[i]);
125 m_translate.insert(s, sym_b(s, false));
126 m_rev_translate.insert(s, s);
127 }
128 }
129
130 // Ensure that symbols that are used both with skolems and non-skolems are named apart.
get_symbol(symbol s0,bool is_skolem)131 symbol smt_renaming::get_symbol(symbol s0, bool is_skolem) {
132 sym_b sb;
133 symbol s;
134 if (m_translate.find(s0, sb)) {
135 if (is_skolem == sb.is_skolem)
136 return sb.name;
137 if (sb.name_aux != symbol::null) {
138 return sb.name_aux;
139 }
140 int k = 0;
141 symbol s1;
142 do {
143 s = fix_symbol(s0, k++);
144 }
145 while (s == s0 || (m_rev_translate.find(s, s1) && s1 != s0));
146 m_rev_translate.insert(s, s0);
147 sb.name_aux = s;
148 m_translate.insert(s, sb);
149 return s;
150 }
151
152 int k = 0;
153 do {
154 s = fix_symbol(s0, k++);
155 }
156 while (m_rev_translate.contains(s));
157 m_translate.insert(s0, sym_b(s, is_skolem));
158 m_rev_translate.insert(s, s0);
159 return s;
160 }
161
162 // ---------------------------------------
163 // smt_printer
164
165 class smt_printer {
166 std::ostream& m_out;
167 ast_manager& m_manager;
168 ptr_vector<quantifier>& m_qlists;
169 smt_renaming& m_renaming;
170 unsigned m_indent;
171 unsigned m_num_var_names;
172 char const* const* m_var_names;
173 ptr_vector<expr> m_todo;
174 ast_mark m_mark;
175 unsigned m_num_lets;
176 arith_util m_autil;
177 bv_util m_bvutil;
178 seq_util m_sutil;
179 fpa_util m_futil;
180 family_id m_basic_fid;
181 family_id m_bv_fid;
182 family_id m_arith_fid;
183 family_id m_array_fid;
184 family_id m_dt_fid;
185 family_id m_fpa_fid;
186 family_id m_label_fid;
187 symbol m_logic;
188 symbol m_AUFLIRA;
189 bool m_no_lets;
190 bool m_simplify_implies;
191 expr* m_top;
192
is_bool(sort * s)193 bool is_bool(sort* s) {
194 return
195 m_basic_fid == s->get_family_id() &&
196 s->get_decl_kind() == BOOL_SORT;
197 }
198
is_bool(expr * e)199 bool is_bool(expr* e) {
200 return is_bool(e->get_sort());
201 }
202
is_proof(sort * s)203 bool is_proof(sort* s) {
204 return
205 m_basic_fid == s->get_family_id() &&
206 s->get_decl_kind() == PROOF_SORT;
207 }
208
is_proof(expr * e)209 bool is_proof(expr* e) {
210 return is_proof(e->get_sort());
211 }
212
pp_id(expr * n)213 void pp_id(expr* n) {
214 m_out << (is_bool(n)?"$x":(is_proof(n)?"@x":"?x")) << n->get_id();
215 }
216
pp_decl(func_decl * d)217 void pp_decl(func_decl* d) {
218 symbol sym = m_renaming.get_symbol(d->get_name(), d->is_skolem());
219 if (d->get_family_id() == m_dt_fid) {
220 datatype_util util(m_manager);
221 if (util.is_recognizer(d)) {
222 visit_params(false, sym, d->get_num_parameters(), d->get_parameters());
223 }
224 else {
225 m_out << sym;
226 }
227 }
228 else if (m_manager.is_ite(d)) {
229 m_out << "ite";
230 }
231 else if (m_manager.is_implies(d)) {
232 m_out << "=>";
233 }
234 else if (is_decl_of(d, m_arith_fid, OP_UMINUS)) {
235 m_out << "-";
236 }
237 else {
238 visit_params(false, sym, d->get_num_parameters(), d->get_parameters());
239 }
240 m_out << " ";
241 }
242
is_sort_param(unsigned num_params,parameter const * params)243 bool is_sort_param(unsigned num_params, parameter const* params) {
244 return
245 num_params == 1 &&
246 params[0].is_ast() &&
247 is_sort(params[0].get_ast());
248 }
249
visit_params(bool is_sort_symbol,symbol const & sym,unsigned num_params,parameter const * params)250 void visit_params(bool is_sort_symbol, symbol const& sym, unsigned num_params, parameter const* params) {
251 if (0 == num_params) {
252 m_out << sym;
253 return;
254 }
255
256 if (is_sort_symbol && sym == symbol("String")) {
257 m_out << "String";
258 return;
259 }
260 if (is_sort_symbol &&
261 sym != symbol("BitVec") &&
262 sym != symbol("FloatingPoint") &&
263 sym != symbol("RoundingMode")) {
264 m_out << "(" << sym << " ";
265 }
266 else if (!is_sort_symbol && is_sort_param(num_params, params)) {
267 m_out << "(as " << sym << " ";
268 }
269 else {
270 m_out << "(_ " << sym << " ";
271 }
272
273 for (unsigned i = 0; i < num_params; ++i) {
274 parameter const& p = params[i];
275 if (p.is_ast()) {
276 if (is_sort(p.get_ast())) {
277 visit_sort(to_sort(p.get_ast()));
278 }
279 else if (is_expr(p.get_ast())) {
280 pp_expr(to_expr(p.get_ast()));
281 }
282 else if (is_func_decl(p.get_ast())) {
283 pp_decl(to_func_decl(p.get_ast()));
284 }
285 else {
286 m_out << "#" << p.get_ast()->get_id();
287 }
288 }
289 else {
290 m_out << p;
291 }
292 if (i + 1 < num_params) {
293 m_out << " ";
294 }
295 }
296 m_out << ")";
297 }
298
is_auflira() const299 bool is_auflira() const {
300 return m_logic == m_AUFLIRA;
301 }
302
visit_sort(sort * s,bool bool2int=false)303 void visit_sort(sort* s, bool bool2int = false) {
304 symbol sym;
305 if (s->is_sort_of(m_bv_fid, BV_SORT)) {
306 sym = symbol("BitVec");
307 }
308 else if (s->is_sort_of(m_arith_fid, REAL_SORT)) {
309 sym = s->get_name();
310 }
311 else if (m_manager.is_bool(s)) {
312 sym = symbol("Bool");
313 }
314 else if (s->is_sort_of(m_arith_fid, INT_SORT)) {
315 sym = s->get_name();
316 }
317 else if (s->is_sort_of(m_array_fid, ARRAY_SORT)) {
318 sym = "Array";
319 }
320 else if (s->is_sort_of(m_dt_fid, DATATYPE_SORT)) {
321 datatype_util util(m_manager);
322 unsigned num_sorts = util.get_datatype_num_parameter_sorts(s);
323 if (num_sorts > 0) {
324 m_out << "(";
325 }
326 m_out << m_renaming.get_symbol(s->get_name(), false);
327 if (num_sorts > 0) {
328 for (unsigned i = 0; i < num_sorts; ++i) {
329 m_out << " ";
330 visit_sort(util.get_datatype_parameter_sort(s, i));
331 }
332 m_out << ")";
333 }
334 return;
335 }
336 else {
337 sym = m_renaming.get_symbol(s->get_name(), false);
338 }
339 visit_params(true, sym, s->get_num_parameters(), s->get_parameters());
340 }
341
display_rational(rational const & r,bool is_int)342 void display_rational(rational const & r, bool is_int) {
343 bool d = !is_int;
344 if (r.is_int()) {
345 m_out << r << (d ? ".0" : "");
346 }
347 else {
348 m_out << "(/ " << numerator(r) << (d ? ".0" : "") << " " << denominator(r) << (d ? ".0" : "") << ")";
349 }
350 }
351
352
pp_arg(expr * arg,app * parent)353 void pp_arg(expr *arg, app *parent) {
354 pp_marked_expr(arg);
355 }
356
visit_app(app * n)357 void visit_app(app* n) {
358 rational val;
359 bool is_int, pos;
360 buffer<symbol> names;
361 unsigned bv_size;
362 zstring s;
363 unsigned num_args = n->get_num_args();
364 func_decl* decl = n->get_decl();
365 scoped_mpf float_val(m_futil.fm());
366 if (m_autil.is_numeral(n, val, is_int)) {
367 if (val.is_neg()) {
368 val.neg();
369 m_out << "(- ";
370 display_rational(val, is_int);
371 m_out << ")";
372 }
373 else {
374 display_rational(val, is_int);
375 }
376 }
377 else if (m_autil.is_irrational_algebraic_numeral(n)) {
378 anum const & aval = m_autil.to_irrational_algebraic_numeral(n);
379 std::ostringstream buffer;
380 m_autil.am().display_root_smt2(buffer, aval);
381 m_out << buffer.str();
382 }
383 else if (m_sutil.str.is_string(n, s)) {
384 std::string encs = s.encode();
385 m_out << "\"";
386 for (unsigned i = 0; i < encs.length(); ++i) {
387 if (encs[i] == '\"') {
388 m_out << "\"\"";
389 }
390 else {
391 m_out << encs[i];
392 }
393 }
394 m_out << "\"";
395 }
396 else if (m_bvutil.is_numeral(n, val, bv_size)) {
397 m_out << "(_ bv" << val << " " << bv_size << ")";
398 }
399 else if (m_futil.is_numeral(n, float_val)) {
400 m_out << mk_ismt2_pp(n, m_manager);
401 }
402 else if (m_bvutil.is_bit2bool(n)) {
403 unsigned bit = n->get_decl()->get_parameter(0).get_int();
404 m_out << "(= ((_ extract " << bit << " " << bit << ") ";
405 pp_marked_expr(n->get_arg(0));
406 m_out << ") (_ bv1 1))";
407 }
408 else if (m_manager.is_label(n, pos, names) && !names.empty()) {
409 m_out << "(! ";
410 pp_marked_expr(n->get_arg(0));
411 m_out << (pos?":lblpos":":lblneg") << " " << m_renaming.get_symbol(names[0], false) << ")";
412 }
413 else if (m_manager.is_label_lit(n, names) && !names.empty()) {
414 m_out << "(! true :lblpos " << m_renaming.get_symbol(names[0], false) << ")";
415 }
416 else if (num_args == 0) {
417 if (decl->private_parameters()) {
418 m_out << m_renaming.get_symbol(decl->get_name(), decl->is_skolem());
419 }
420 else {
421 symbol sym = m_renaming.get_symbol(decl->get_name(), decl->is_skolem());
422 visit_params(false, sym, decl->get_num_parameters(), decl->get_parameters());
423 }
424 }
425 else if (num_args == 1 && n->get_family_id() == m_label_fid) {
426 expr* ch = n->get_arg(0);
427 pp_marked_expr(ch);
428 }
429 else if (m_simplify_implies && m_manager.is_implies(decl) && m_manager.is_implies(n->get_arg(1))) {
430 expr *curr = n;
431 expr *arg;
432 m_out << "(=> (and";
433 while (m_manager.is_implies(curr)) {
434 arg = to_app(curr)->get_arg(0);
435
436 m_out << " ";
437 pp_arg(arg, n);
438 curr = to_app(curr)->get_arg(1);
439 }
440 m_out << ") ";
441 pp_arg(curr, n);
442 m_out << ")";
443
444 }
445 else if (m_manager.is_distinct(decl)) {
446 ptr_vector<expr> args(num_args, n->get_args());
447 unsigned idx = 0;
448 m_out << "(and";
449 while (true) {
450 while (idx < args.size() && !args[idx])
451 idx++;
452 if (idx >= args.size()) break;
453 sort * s = args[idx]->get_sort();
454 unsigned next = idx + 1;
455
456 // check if there is only a single one
457 while (next < args.size() && (!args[next] || args[next]->get_sort() != s))
458 next++;
459 if (next >= args.size()) {
460 args[idx] = 0;
461 // if so, skip it
462 continue;
463 }
464
465 // otherwise print all of the relevant sort
466 m_out << " (distinct";
467 for (unsigned i = idx; i < args.size(); ++i) {
468 if (args[i] && s == args[i]->get_sort()) {
469 m_out << " ";
470 pp_marked_expr(args[i]);
471 args[i] = 0;
472 }
473 }
474 m_out << ")";
475 }
476 m_out << " true)";
477 }
478 else {
479 m_out << "(";
480 pp_decl(decl);
481 for (unsigned i = 0; i < num_args; ++i) {
482 pp_arg(n->get_arg(i), n);
483 if (i + 1 < num_args) {
484 m_out << " ";
485 }
486 }
487 m_out << ")";
488 }
489 }
490
print_no_lets(expr * e)491 void print_no_lets(expr *e) {
492 smt_printer p(m_out, m_manager, m_qlists, m_renaming, m_logic, true, m_simplify_implies, m_indent, m_num_var_names, m_var_names);
493 p(e);
494 }
495
print_bound(symbol const & name)496 void print_bound(symbol const& name) {
497 m_out << name;
498 }
499
visit_quantifier(quantifier * q)500 void visit_quantifier(quantifier* q) {
501 m_qlists.push_back(q);
502
503 m_out << "(";
504 switch (q->get_kind()) {
505 case forall_k: m_out << "forall "; break;
506 case exists_k: m_out << "exists "; break;
507 case lambda_k: m_out << "lambda "; break;
508 }
509 m_out << "(";
510 for (unsigned i = 0; i < q->get_num_decls(); ++i) {
511 sort* s = q->get_decl_sort(i);
512 m_out << "(";
513 print_bound(m_renaming.get_symbol(q->get_decl_name(i), false));
514 m_out << " ";
515 visit_sort(s, true);
516 m_out << ") ";
517 }
518 m_out << ")";
519
520 if ((q->get_num_patterns() > 0 || q->get_qid() != symbol::null)) {
521 m_out << "(! ";
522 }
523 {
524 smt_printer p(m_out, m_manager, m_qlists, m_renaming, m_logic, false, m_simplify_implies, m_indent, m_num_var_names, m_var_names);
525 p(q->get_expr());
526 }
527
528 for (unsigned i = 0; i < q->get_num_patterns(); ++i) {
529 app *pat = reinterpret_cast<app*> (q->get_pattern(i));
530
531 if (pat->get_num_args() == 1 && is_app(pat->get_arg(0))) {
532 app *app = to_app(pat->get_arg(0));
533 if (app->get_num_args() == 1 && app->get_decl()->get_name().str() == "sk_hack") {
534 /*
535 m_out << " :ex_act { ";
536 print_no_lets(app->get_arg(0));
537 m_out << "}";
538 */
539 continue;
540 }
541 }
542
543 m_out << " :pattern ( ";
544 for (unsigned j = 0; j < pat->get_num_args(); ++j) {
545 print_no_lets(pat->get_arg(j));
546 m_out << " ";
547 }
548 m_out << ")";
549 }
550
551 if (q->get_qid() != symbol::null)
552 m_out << " :qid " << q->get_qid();
553
554 if ((q->get_num_patterns() > 0 || q->get_qid() != symbol::null)) {
555 m_out << ")";
556 }
557 m_out << ")";
558 newline();
559 m_qlists.pop_back();
560 }
561
newline()562 void newline() {
563 unsigned i = m_indent;
564 m_out << "\n";
565 while (i > 0) { m_out << " "; --i; }
566 }
567
visit_var(var * v)568 void visit_var(var* v) {
569 unsigned idx = v->get_idx();
570 for (unsigned i = m_qlists.size(); ; --i) {
571 if (i == 0) {
572 break;
573 }
574 quantifier* q = m_qlists[i-1];
575 unsigned num_decls = q->get_num_decls();
576 if (idx < num_decls) {
577 unsigned offs = num_decls-idx-1;
578 symbol name = m_renaming.get_symbol(q->get_decl_name(offs), false);
579 print_bound(name);
580 return;
581 }
582 idx -= num_decls;
583 }
584 if (idx < m_num_var_names) {
585 m_out << m_var_names[m_num_var_names - idx - 1];
586 }
587 else {
588 m_out << "?" << idx;
589 }
590 }
591
pp_marked_expr(expr * n)592 void pp_marked_expr(expr* n) {
593 if (m_mark.is_marked(n)) {
594 pp_id(n);
595 }
596 else {
597 pp_expr(n);
598 }
599 }
600
pp_expr(expr * n)601 void pp_expr(expr* n) {
602 switch(n->get_kind()) {
603 case AST_QUANTIFIER:
604 visit_quantifier(to_quantifier(n));
605 break;
606 case AST_APP:
607 visit_app(to_app(n));
608 break;
609 case AST_VAR:
610 visit_var(to_var(n));
611 break;
612 default:
613 UNREACHABLE();
614 }
615 }
616
visit_expr(expr * n)617 void visit_expr(expr* n) {
618 m_out << "(let ((";
619 pp_id(n);
620 m_out << " ";
621 pp_expr(n);
622 m_out << ")";
623 m_out << ")";
624 newline();
625 }
626
is_unit(expr * n)627 bool is_unit(expr* n) {
628 if (n->get_ref_count() <= 2 && is_small(n)) {
629 return true;
630 }
631 if (n == m_top) {
632 return true;
633 }
634 switch(n->get_kind()) {
635 case AST_VAR:
636 return true;
637 case AST_APP:
638 return to_app(n)->get_num_args() == 0;
639 default:
640 return false;
641 }
642 }
643
644 static const unsigned m_line_length = 80;
645
is_small(expr * n)646 bool is_small(expr* n) {
647 unsigned sz = 0;
648 return is_small(n, sz);
649 }
650
is_small(expr * n,unsigned & sz)651 bool is_small(expr* n, unsigned& sz) {
652 if (sz > m_line_length) {
653 return false;
654 }
655 if (m_mark.is_marked(n)) {
656 sz += 5;
657 return sz <= m_line_length;
658 }
659 switch(n->get_kind()) {
660 case AST_QUANTIFIER:
661 return false;
662 case AST_VAR:
663 sz += 5;
664 return sz <= m_line_length;
665 case AST_APP: {
666 app* a = to_app(n);
667 func_decl* d = a->get_decl();
668 symbol const& s = d->get_name();
669 if (s.is_numerical()) {
670 sz += 4;
671 }
672 if (s.is_numerical()) {
673 sz += 7;
674 }
675 else if (s.bare_str()) {
676 sz += 3 + static_cast<unsigned>(strlen(s.bare_str()));
677 }
678 for (unsigned i = 0; i < a->get_num_args() && sz <= m_line_length; ++i) {
679 sz += 1;
680 if (!is_small(a->get_arg(i), sz)) {
681 return false;
682 }
683 }
684 return sz <= m_line_length;
685 }
686 default:
687 return false;
688 }
689 }
690
visit_children(expr * n)691 bool visit_children(expr* n) {
692 unsigned todo_size = m_todo.size();
693 switch(n->get_kind()) {
694 case AST_QUANTIFIER:
695 case AST_VAR:
696 break;
697 case AST_APP: {
698 app* a = to_app(n);
699 for (unsigned i = 0; i < a->get_num_args(); ++i) {
700 expr* ch = a->get_arg(i);
701 if (!is_unit(ch) && !m_mark.is_marked(ch)) {
702 m_todo.push_back(ch);
703 }
704 }
705 break;
706 }
707 default:
708 UNREACHABLE();
709 break;
710 }
711 bool all_visited = todo_size == m_todo.size();
712 return all_visited;
713 }
714
715 public:
smt_printer(std::ostream & out,ast_manager & m,ptr_vector<quantifier> & ql,smt_renaming & rn,symbol logic,bool no_lets,bool simplify_implies,unsigned indent,unsigned num_var_names=0,char const * const * var_names=nullptr)716 smt_printer(std::ostream& out, ast_manager& m, ptr_vector<quantifier>& ql, smt_renaming& rn,
717 symbol logic, bool no_lets, bool simplify_implies, unsigned indent, unsigned num_var_names = 0, char const* const* var_names = nullptr) :
718 m_out(out),
719 m_manager(m),
720 m_qlists(ql),
721 m_renaming(rn),
722 m_indent(indent),
723 m_num_var_names(num_var_names),
724 m_var_names(var_names),
725 m_num_lets(0),
726 m_autil(m),
727 m_bvutil(m),
728 m_sutil(m),
729 m_futil(m),
730 m_logic(logic),
731 m_AUFLIRA("AUFLIRA"),
732 // It's much easier to read those testcases with that.
733 m_no_lets(no_lets),
734 m_simplify_implies(simplify_implies)
735 {
736 m_basic_fid = m.get_basic_family_id();
737 m_label_fid = m.mk_family_id("label");
738 m_bv_fid = m.mk_family_id("bv");
739 m_arith_fid = m.mk_family_id("arith");
740 m_array_fid = m.mk_family_id("array");
741 m_dt_fid = m.mk_family_id("datatype");
742 m_fpa_fid = m.mk_family_id("fpa");
743 }
744
operator ()(expr * n)745 void operator()(expr* n) {
746 m_top = n;
747 if (!m_no_lets) {
748 switch(n->get_kind()) {
749 case AST_APP:
750 for (unsigned i = 0; i < to_app(n)->get_num_args(); ++i) {
751 m_todo.push_back(to_app(n)->get_arg(i));
752 }
753 break;
754 // Don't do this for quantifiers -- they need to have the body be
755 // visited when the m_qlist contains the relevant quantifier.
756 default:
757 break;
758 }
759 }
760
761 while (!m_todo.empty()) {
762 expr* m = m_todo.back();
763 if (m_mark.is_marked(m)) {
764 m_todo.pop_back();
765 }
766 else if (is_unit(m)) {
767 m_todo.pop_back();
768 }
769 else if (visit_children(m)) {
770 m_todo.pop_back();
771 m_mark.mark(m, true);
772 visit_expr(m);
773 ++m_num_lets;
774 }
775 }
776
777 pp_marked_expr(n);
778 for (unsigned i = 0; i < m_num_lets; ++i) {
779 m_out << ")";
780 }
781 m_mark.reset();
782 m_num_lets = 0;
783 m_top = nullptr;
784 }
785
pp_dt(ast_mark & mark,sort * s)786 void pp_dt(ast_mark& mark, sort* s) {
787 datatype_util util(m_manager);
788 SASSERT(util.is_datatype(s));
789
790 sort_ref_vector ps(m_manager);
791 ptr_vector<datatype::def> defs;
792 util.get_defs(s, defs);
793
794 unsigned j = 0;
795 for (datatype::def* d : defs) {
796 sort_ref sr = d->instantiate(ps);
797 if (mark.is_marked(sr))
798 continue;
799 mark.mark(sr, true);
800 defs[j++] = d;
801 }
802 defs.shrink(j);
803 if (defs.empty())
804 return;
805
806 m_out << "(declare-datatypes (";
807 bool first_def = true;
808 for (datatype::def* d : defs) {
809 if (!first_def) m_out << "\n "; else first_def = false;
810 m_out << "(" << ensure_quote(d->name()) << " " << d->params().size() << ")";
811 }
812 m_out << ") (";
813 bool first_sort = true;
814 for (datatype::def* d : defs) {
815 if (!first_sort) m_out << "\n "; else first_sort = false;
816 if (!d->params().empty()) {
817 m_out << "(par (";
818 bool first_param = true;
819 for (sort* s : d->params()) {
820 if (!first_param) m_out << " "; else first_param = false;
821 visit_sort(s);
822 }
823 m_out << ")";
824 }
825 m_out << "(";
826 bool first_constr = true;
827 for (datatype::constructor* f : *d) {
828 if (!first_constr) m_out << " "; else first_constr = false;
829 m_out << "(";
830 m_out << m_renaming.get_symbol(f->name(), false);
831 for (datatype::accessor* a : *f) {
832 m_out << " (" << m_renaming.get_symbol(a->name(), false) << " ";
833 visit_sort(a->range());
834 m_out << ")";
835 }
836 m_out << ")";
837 }
838 if (!d->params().empty()) {
839 m_out << ")";
840 }
841 m_out << ")";
842 }
843 m_out << "))";
844 newline();
845 }
846
847
pp_sort_decl(ast_mark & mark,sort * s)848 void pp_sort_decl(ast_mark& mark, sort* s) {
849 if (mark.is_marked(s)) {
850 return;
851 }
852 if (s->is_sort_of(m_dt_fid, DATATYPE_SORT)) {
853 pp_dt(mark, s);
854 }
855 else {
856 m_out << "(declare-sort ";
857 visit_sort(s);
858 m_out << " 0)";
859 newline();
860 }
861 mark.mark(s, true);
862 }
863
operator ()(sort * s)864 void operator()(sort* s) {
865 ast_mark mark;
866 pp_sort_decl(mark, s);
867 }
868
operator ()(func_decl * d)869 void operator()(func_decl* d) {
870 m_out << "(declare-fun ";
871 pp_decl(d);
872 m_out << "(";
873 for (unsigned i = 0; i < d->get_arity(); ++i) {
874 if (i > 0) m_out << " ";
875 visit_sort(d->get_domain(i), true);
876 }
877 m_out << ") ";
878 visit_sort(d->get_range());
879 m_out << ")";
880 }
881
visit_pred(func_decl * d)882 void visit_pred(func_decl* d) {
883 m_out << "(";
884 pp_decl(d);
885 for (unsigned i = 0; i < d->get_arity(); ++i) {
886 m_out << " ";
887 visit_sort(d->get_domain(i), true);
888 }
889 m_out << ")";
890 }
891 };
892
893
894 // ---------------------------------------
895 // ast_smt_pp:
896
ast_smt_pp(ast_manager & m)897 ast_smt_pp::ast_smt_pp(ast_manager& m):
898 m_manager(m),
899 m_assumptions(m),
900 m_assumptions_star(m),
901 m_benchmark_name(),
902 m_source_info(),
903 m_status("unknown"),
904 m_category(),
905 m_logic(),
906 m_dt_fid(m.mk_family_id("datatype")),
907 m_is_declared(&m_is_declared_default),
908 m_simplify_implies(true)
909 {}
910
display_expr_smt2(std::ostream & strm,expr * n,unsigned indent,unsigned num_var_names,char const * const * var_names)911 void ast_smt_pp::display_expr_smt2(std::ostream& strm, expr* n, unsigned indent, unsigned num_var_names, char const* const* var_names) {
912 ptr_vector<quantifier> ql;
913 smt_renaming rn;
914 smt_printer p(strm, m_manager, ql, rn, m_logic, false, m_simplify_implies, indent, num_var_names, var_names);
915 p(n);
916 }
917
display_ast_smt2(std::ostream & strm,ast * a,unsigned indent,unsigned num_var_names,char const * const * var_names)918 void ast_smt_pp::display_ast_smt2(std::ostream& strm, ast* a, unsigned indent, unsigned num_var_names, char const* const* var_names) {
919 ptr_vector<quantifier> ql;
920 smt_renaming rn;
921 smt_printer p(strm, m_manager, ql, rn, m_logic, false, m_simplify_implies, indent, num_var_names, var_names);
922 if (is_expr(a)) {
923 p(to_expr(a));
924 }
925 else if (is_func_decl(a)) {
926 p(to_func_decl(a));
927 }
928 else {
929 SASSERT(is_sort(a));
930 p(to_sort(a));
931 }
932 }
933
display_sort_decl(std::ostream & out,sort * s,ast_mark & seen)934 void ast_smt_pp::display_sort_decl(std::ostream& out, sort* s, ast_mark& seen) {
935 ptr_vector<quantifier> ql;
936 smt_renaming rn;
937 smt_printer p(out, m_manager, ql, rn, m_logic, false, m_simplify_implies, 0, 0, nullptr);
938 p.pp_sort_decl(seen, s);
939 }
940
941
942
display_smt2(std::ostream & strm,expr * n)943 void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
944 ptr_vector<quantifier> ql;
945 ast_manager& m = m_manager;
946 decl_collector decls(m);
947 smt_renaming rn;
948
949 for (expr* a : m_assumptions) {
950 decls.visit(a);
951 }
952 for (expr* a : m_assumptions_star) {
953 decls.visit(a);
954 }
955 decls.visit(n);
956
957 if (m.is_proof(n)) {
958 strm << "(";
959 }
960 if (m_benchmark_name != symbol::null) {
961 strm << "; " << m_benchmark_name << "\n";
962 }
963 if (m_source_info != symbol::null && m_source_info != symbol("")) {
964 strm << "; :source { " << m_source_info << " }\n";
965 }
966 if (m.is_bool(n)) {
967 strm << "(set-info :status " << m_status << ")\n";
968 }
969 if (m_category != symbol::null && m_category != symbol("")) {
970 strm << "; :category { " << m_category << " }\n";
971 }
972 if (m_logic != symbol::null && m_logic != symbol("")) {
973 strm << "(set-logic " << m_logic << ")\n";
974 }
975 if (!m_attributes.empty()) {
976 strm << "; " << m_attributes;
977 }
978
979 #if 0
980 decls.display_decls(strm);
981 #else
982 decls.order_deps(0);
983 ast_mark sort_mark;
984 for (sort* s : decls.get_sorts()) {
985 if (!(*m_is_declared)(s)) {
986 smt_printer p(strm, m, ql, rn, m_logic, true, true, m_simplify_implies, 0);
987 p.pp_sort_decl(sort_mark, s);
988 }
989 }
990
991 for (unsigned i = 0; i < decls.get_num_decls(); ++i) {
992 func_decl* d = decls.get_func_decls()[i];
993 if (!(*m_is_declared)(d)) {
994 smt_printer p(strm, m, ql, rn, m_logic, true, true, m_simplify_implies, 0);
995 p(d);
996 strm << "\n";
997 }
998 }
999
1000 #endif
1001
1002 for (expr* a : m_assumptions) {
1003 smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 1);
1004 strm << "(assert\n ";
1005 p(a);
1006 strm << ")\n";
1007 }
1008
1009 for (expr* a : m_assumptions_star) {
1010 smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 1);
1011 strm << "(assert\n ";
1012 p(a);
1013 strm << ")\n";
1014 }
1015
1016 smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 0);
1017 if (m.is_bool(n)) {
1018 if (!m.is_true(n)) {
1019 strm << "(assert\n ";
1020 p(n);
1021 strm << ")\n";
1022 }
1023 strm << "(check-sat)\n";
1024 }
1025 else if (m.is_proof(n)) {
1026 strm << "(proof\n";
1027 p(n);
1028 strm << "))\n";
1029 }
1030 else {
1031 p(n);
1032 }
1033 }
1034