From 19e73fb2addbe28344c5ba1c8eaf374679557e51 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 29 Mar 2016 16:13:31 +0100 Subject: [PATCH] whitespace --- src/ast/ast_smt2_pp.cpp | 86 ++++++++++++------------ src/ast/ast_smt_pp.cpp | 142 ++++++++++++++++++++-------------------- 2 files changed, 114 insertions(+), 114 deletions(-) diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index 1afa13117..1a7f051a0 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -87,10 +87,10 @@ bool smt2_pp_environment::is_indexed_fdecl(func_decl * f) const { } bool smt2_pp_environment::is_sort_param(func_decl * f) const { - return + return f->get_family_id() != null_family_id && - f->get_num_parameters() == 1 && - f->get_parameter(0).is_ast() && + f->get_num_parameters() == 1 && + f->get_parameter(0).is_ast() && is_sort(f->get_parameter(0).get_ast()) && f->get_range() == to_sort(f->get_parameter(0).get_ast()); } @@ -107,8 +107,8 @@ format * smt2_pp_environment::pp_fdecl_params(format * fname, func_decl * f) { ptr_buffer fs; fs.push_back(fname); for (unsigned i = 0; i < num; i++) { - SASSERT(f->get_parameter(i).is_int() || - f->get_parameter(i).is_rational() || + SASSERT(f->get_parameter(i).is_int() || + f->get_parameter(i).is_rational() || (f->get_parameter(i).is_ast() && is_func_decl(f->get_parameter(i).get_ast()))); if (f->get_parameter(i).is_int()) fs.push_back(mk_int(get_manager(), f->get_parameter(i).get_int())); @@ -122,7 +122,7 @@ format * smt2_pp_environment::pp_fdecl_params(format * fname, func_decl * f) { format * smt2_pp_environment::pp_fdecl(func_decl * f, unsigned & len) { format * fname = pp_fdecl_name(f, len); - if (f->get_family_id() == null_family_id) + if (f->get_family_id() == null_family_id) return fname; if (is_sort_param(f)) { len = UINT_MAX; @@ -247,7 +247,7 @@ format * smt2_pp_environment::pp_float_literal(app * t, bool use_bv_lits, bool u buf << "(_ -oo " << v.get().get_ebits() << " " << v.get().get_sbits() << ")"; return mk_string(m, buf.c_str()); } - else if (fm.is_pzero(v)) { + else if (fm.is_pzero(v)) { buf << "(_ +zero " << v.get().get_ebits() << " " << v.get().get_sbits() << ")"; return mk_string(m, buf.c_str()); } @@ -257,9 +257,9 @@ format * smt2_pp_environment::pp_float_literal(app * t, bool use_bv_lits, bool u } else if (use_float_real_lits) { - buf << "((_ to_fp " << v.get().get_ebits() << " " << - v.get().get_sbits() << ") RTZ " << - fm.to_string(v).c_str() << ")"; + buf << "((_ to_fp " << v.get().get_ebits() << " " << + v.get().get_sbits() << ") RTZ " << + fm.to_string(v).c_str() << ")"; return mk_string(m, buf.c_str()); } else { @@ -283,7 +283,7 @@ format * smt2_pp_environment::pp_float_literal(app * t, bool use_bv_lits, bool u app_ref e_sig(m); e_sig = get_bvutil().mk_numeral(rational(sig), v.get().get_sbits() - 1); body = mk_compose(m, body, pp_bv_literal(e_sig, use_bv_lits, false)); - + body = mk_compose(m, body, mk_string(m, ")")); return body; } @@ -356,7 +356,7 @@ format * smt2_pp_environment::pp_arith_literal(app * t, bool decimal, unsigned d am.display_decimal(buffer, abs_val, decimal_prec); } else { - am.display_root_smt2(buffer, val2); + am.display_root_smt2(buffer, val2); } vf = mk_string(get_manager(), buffer.str().c_str()); return is_neg ? mk_neg(vf) : vf; @@ -378,7 +378,7 @@ format * smt2_pp_environment::pp_string_literal(app * t) { buffer << encs[i]; } } - buffer << "\""; + buffer << "\""; return mk_string(get_manager(), buffer.str().c_str()); } @@ -395,7 +395,7 @@ format_ns::format * smt2_pp_environment::pp_sort(sort * s) { // This method is redefined in cmd_context::pp_env: support for parametric sorts. // Here, we just pretty print builtin sorts: Bool, Int, Real, BitVec and Array. ast_manager & m = get_manager(); - if (m.is_bool(s)) + if (m.is_bool(s)) return mk_string(m, "Bool"); if (get_autil().is_int(s)) return mk_string(m, "Int"); @@ -431,7 +431,7 @@ format_ns::format * smt2_pp_environment::pp_sort(sort * s) { fs.push_back(pp_sort(to_sort(s->get_parameter(0).get_ast()))); return mk_seq1(m, fs.begin(), fs.end(), f2f(), get_sutil().is_seq(s)?"Seq":"Re"); } - return format_ns::mk_string(get_manager(), s->get_name().str().c_str()); + return format_ns::mk_string(get_manager(), s->get_name().str().c_str()); } typedef app_ref_vector format_ref_vector; @@ -449,8 +449,8 @@ class smt2_printer { expr2alias * m_expr2alias; // expr -> position @ m_aliased_exprs, m_aliased_pps, m_aliased_lvls_names. ptr_vector m_aliased_exprs; format_ref_vector m_aliased_pps; - svector > m_aliased_lvls_names; - unsigned m_next_alias_idx; + svector > m_aliased_lvls_names; + unsigned m_next_alias_idx; struct scope { unsigned m_aliased_exprs_lim; unsigned m_old_next_alias_idx; @@ -461,7 +461,7 @@ class smt2_printer { svector m_var_names; typedef hashtable symbol_set; symbol_set m_var_names_set; - + struct frame { expr * m_curr; unsigned m_idx; @@ -469,7 +469,7 @@ class smt2_printer { bool m_use_alias; // if new aliases can be created frame(expr * c, unsigned i, unsigned s, bool use_alias):m_curr(c), m_idx(i), m_spos(s), m_use_alias(use_alias) {} }; - + svector m_frame_stack; format_ref_vector m_format_stack; struct info { @@ -517,7 +517,7 @@ class smt2_printer { SASSERT(m_aliased_exprs.size() == m_aliased_pps.size()); SASSERT(m_aliased_exprs.size() == m_aliased_lvls_names.size()); unsigned idx = m_aliased_exprs.size(); - m_expr2alias->insert(n, idx); + m_expr2alias->insert(n, idx); m_aliased_exprs.push_back(n); m_aliased_pps.push_back(nf); m_aliased_lvls_names.push_back(std::make_pair(lvl, name)); @@ -567,12 +567,12 @@ class smt2_printer { buf.append(")"); f = mk_string(m(), buf.c_str()); } - m_format_stack.push_back(f); + m_format_stack.push_back(f); m_info_stack.push_back(info(0, 1, 1)); } format * pp_attribute(char const * attr, format * f) { - return mk_compose(m(), + return mk_compose(m(), mk_string(m(), attr), mk_indent(m(), static_cast(strlen(attr)), f)); } @@ -639,7 +639,7 @@ class smt2_printer { } return false; } - + void process_var(var * v) { pp_var(v); pop_frame(); @@ -651,7 +651,7 @@ class smt2_printer { expr * arg = t->get_arg(fr.m_idx); fr.m_idx++; if (pp_aliased(arg)) - continue; + continue; switch (arg->get_kind()) { case AST_VAR: pp_var(to_var(arg)); @@ -679,11 +679,11 @@ class smt2_printer { m_format_stack.shrink(fr.m_spos); m_info_stack.shrink(fr.m_spos); if (fr.m_use_alias && m_root != t && - ((f_info.m_depth >= m_pp_max_depth) || + ((f_info.m_depth >= m_pp_max_depth) || ((f_info.m_weight >= m_pp_min_alias_size || is_quantifier(t)) && m_soccs.is_shared(t)))) { symbol a = next_alias(); - TRACE("smt2_pp", tout << "a: " << a << " depth: " << f_info.m_depth << ", weight: " << f_info.m_weight - << ", lvl: " << f_info.m_lvl << " t: #" << t->get_id() << "\n" << mk_ll_pp(t, m()) + TRACE("smt2_pp", tout << "a: " << a << " depth: " << f_info.m_depth << ", weight: " << f_info.m_weight + << ", lvl: " << f_info.m_lvl << " t: #" << t->get_id() << "\n" << mk_ll_pp(t, m()) << ", is-shared: " << m_soccs.is_shared(t) << "\n";); register_alias(t, f, f_info.m_lvl, a); m_format_stack.push_back(mk_string(m(), a.str().c_str())); @@ -745,7 +745,7 @@ class smt2_printer { f = mk_group(m(), mk_compose(m(), mk_indent(m(), 1, mk_compose(m(), mk_string(m(), "("), fname)), mk_indent(m(), SMALL_INDENT, mk_compose(m(), - mk_seq(m(), it, end, f2f()), + mk_seq(m(), it, end, f2f()), mk_string(m(), ")"))))); } else { @@ -756,7 +756,7 @@ class smt2_printer { mk_indent(m(), len + 2, mk_compose(m(), mk_string(m(), " "), first, - mk_seq(m(), it, end, f2f()), + mk_seq(m(), it, end, f2f()), mk_string(m(), ")"))))); } } @@ -832,7 +832,7 @@ class smt2_printer { m_expr2alias = m_expr2alias_stack[lvl]; m_next_alias_idx = 1; } - + void end_scope() { TRACE("pp_scope", tout << "[end-scope] before sz: " << m_aliased_exprs.size() << ", m_root: " << m_root << "\n";); m_expr2alias->reset(); @@ -853,7 +853,7 @@ class smt2_printer { void register_var_names(quantifier * q) { unsigned num_decls = q->get_num_decls(); for (unsigned i = 0; i < num_decls; i++) { - symbol name = ensure_quote_sym(q->get_decl_name(i)); + symbol name = ensure_quote_sym(q->get_decl_name(i)); if (name.is_numerical()) { unsigned idx = 1; name = next_name("x", idx); @@ -914,7 +914,7 @@ class smt2_printer { format * f_body = pp_let(m_format_stack.back(), num_lets); // The current SMT2 frontend uses weight 1 as default. #define MIN_WEIGHT 1 - if (q->has_patterns() || q->get_weight() > MIN_WEIGHT || + if (q->has_patterns() || q->get_weight() > MIN_WEIGHT || q->get_skid() != symbol::null || (q->get_qid() != symbol::null && !q->get_qid().is_numerical())) { ptr_buffer buf; buf.push_back(f_body); @@ -952,12 +952,12 @@ class smt2_printer { format * fs[2] = { f_decls, f_body }; char const * header = q->is_forall() ? "forall" : "exists"; format * f = mk_seq3(m(), fs, fs+2, f2f(), header, 1, SMALL_INDENT); - + info f_info = m_info_stack.back(); f_info.m_lvl = 0; // quantifiers don't depend on any let-decls, pp_let added all dependencies for the body. f_info.m_depth++; f_info.m_weight += q->get_num_decls()*2 + num_lets*8; - + unregister_var_names(q); end_scope(); @@ -1002,7 +1002,7 @@ class smt2_printer { reset_stacks(); SASSERT(&(r.get_manager()) == &(fm())); m_soccs(n); - TRACE("smt2_pp_shared", + TRACE("smt2_pp_shared", tout << "shared terms for:\n" << mk_pp(n, m()) << "\n"; tout << "------>\n"; shared_occs::iterator it = m_soccs.begin_shared(); @@ -1043,7 +1043,7 @@ public: m_env(env), m_soccs(m_manager), m_root(0), - m_aliased_pps(fm()), + m_aliased_pps(fm()), m_next_alias_idx(1), m_format_stack(fm()) { init_expr2alias_stack(); @@ -1108,7 +1108,7 @@ public: }; -void mk_smt2_format(expr * n, smt2_pp_environment & env, params_ref const & p, +void mk_smt2_format(expr * n, smt2_pp_environment & env, params_ref const & p, unsigned num_vars, char const * var_prefix, format_ref & r, sbuffer & var_names) { smt2_printer pr(env, p); @@ -1125,13 +1125,13 @@ void mk_smt2_format(func_decl * f, smt2_pp_environment & env, params_ref const & pr(f, r); } -std::ostream & ast_smt2_pp(std::ostream & out, expr * n, smt2_pp_environment & env, params_ref const & p, unsigned indent, +std::ostream & ast_smt2_pp(std::ostream & out, expr * n, smt2_pp_environment & env, params_ref const & p, unsigned indent, unsigned num_vars, char const * var_prefix) { ast_manager & m = env.get_manager(); format_ref r(fm(m)); sbuffer var_names; mk_smt2_format(n, env, p, num_vars, var_prefix, r, var_names); - if (indent > 0) + if (indent > 0) r = mk_indent(m, indent, r.get()); pp(out, r.get(), m, p); return out; @@ -1142,7 +1142,7 @@ std::ostream & ast_smt2_pp(std::ostream & out, sort * s, smt2_pp_environment & e format_ref r(fm(m)); sbuffer var_names; mk_smt2_format(s, env, p, r); - if (indent > 0) + if (indent > 0) r = mk_indent(m, indent, r.get()); pp(out, r.get(), m, p); return out; @@ -1153,7 +1153,7 @@ std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, smt2_pp_environmen format_ref r(fm(m)); sbuffer var_names; mk_smt2_format(f, env, p, r); - if (indent > 0) + if (indent > 0) r = mk_indent(m, indent, r.get()); pp(out, r.get(), m, p); return out; @@ -1225,13 +1225,13 @@ std::ostream& operator<<(std::ostream& out, app_ref_vector const& e) { } std::ostream& operator<<(std::ostream& out, func_decl_ref_vector const& e) { - for (unsigned i = 0; i < e.size(); ++i) + for (unsigned i = 0; i < e.size(); ++i) out << mk_ismt2_pp(e[i], e.get_manager()) << "\n"; return out; } std::ostream& operator<<(std::ostream& out, sort_ref_vector const& e) { - for (unsigned i = 0; i < e.size(); ++i) + for (unsigned i = 0; i < e.size(); ++i) out << mk_ismt2_pp(e[i], e.get_manager()) << "\n"; return out; } diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index 82137483a..61a86a541 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -43,7 +43,7 @@ static const char m_predef_names[][8] = { symbol smt_renaming::fix_symbol(symbol s, int k) { std::ostringstream buffer; char const * data = s.is_numerical() ? "" : s.bare_str(); - + if (data[0] && !data[1]) { switch (data[0]) { case '/': data = "op_div"; break; @@ -51,7 +51,7 @@ symbol smt_renaming::fix_symbol(symbol s, int k) { default: break; } } - + if (k == 0 && *data) { if (s.is_numerical()) { return s; @@ -63,10 +63,10 @@ symbol smt_renaming::fix_symbol(symbol s, int k) { return s; } } - + if (s.is_numerical()) { buffer << s << k; - return symbol(buffer.str().c_str()); + return symbol(buffer.str().c_str()); } if (is_smt2_quoted_symbol(s)) { @@ -78,12 +78,12 @@ symbol smt_renaming::fix_symbol(symbol s, int k) { if (k > 0) { buffer << k; } - + return symbol(buffer.str().c_str()); } bool smt_renaming::is_legal(char c) { - return c == '.' || c == '_' || c == '\'' + return c == '.' || c == '_' || c == '\'' || c == '?' || c == '!' || isalnum(c); } @@ -134,11 +134,11 @@ symbol smt_renaming::get_symbol(symbol s0) { if (m_translate.find(s0, s)) { return s; } - + int k = 0; do { s = fix_symbol(s0, k++); - } + } while (m_rev_translate.contains(s)); m_translate.insert(s0, s); m_rev_translate.insert(s, s0); @@ -176,7 +176,7 @@ class smt_printer { expr* m_top; bool is_bool(sort* s) { - return + return m_basic_fid == s->get_family_id() && s->get_decl_kind() == BOOL_SORT; } @@ -186,13 +186,13 @@ class smt_printer { } bool is_proof(sort* s) { - return + return m_basic_fid == s->get_family_id() && - s->get_decl_kind() == PROOF_SORT; + s->get_decl_kind() == PROOF_SORT; } - bool is_proof(expr* e) { - return is_proof(m_manager.get_sort(e)); + bool is_proof(expr* e) { + return is_proof(m_manager.get_sort(e)); } void pp_id(expr* n) { @@ -236,8 +236,8 @@ class smt_printer { } bool is_sort_param(unsigned num_params, parameter const* params) { - return - num_params == 1 && + return + num_params == 1 && params[0].is_ast() && is_sort(params[0].get_ast()); } @@ -254,13 +254,13 @@ class smt_printer { return; } if (is_sort_symbol && sym != symbol("BitVec")) { - m_out << "(" << sym << " "; + m_out << "(" << sym << " "; } else if (!is_sort_symbol && is_sort_param(num_params, params)) { m_out << "(as " << sym << " "; } else { - m_out << "(_ " << sym << " "; + m_out << "(_ " << sym << " "; } } else { @@ -302,13 +302,13 @@ class smt_printer { m_out << "]"; } } - + bool is_auflira() const { return m_logic == m_AUFLIRA; } void visit_sort(sort* s, bool bool2int = false) { - symbol sym; + symbol sym; if (bool2int && is_bool(s) && !m_is_smt2) { sym = symbol("Int"); } else if (s->is_sort_of(m_bv_fid, BV_SORT)) { @@ -326,7 +326,7 @@ class smt_printer { else if (s->is_sort_of(m_array_fid, ARRAY_SORT) && m_is_smt2) { sym = "Array"; } - else if (s->is_sort_of(m_array_fid, ARRAY_SORT) && !m_is_smt2) { + else if (s->is_sort_of(m_array_fid, ARRAY_SORT) && !m_is_smt2) { unsigned num_params = s->get_num_parameters(); SASSERT(num_params >= 2); if (is_auflira()) { @@ -341,12 +341,12 @@ class smt_printer { } sort* s1 = to_sort(s->get_parameter(0).get_ast()); sort* s2 = to_sort(s->get_parameter(1).get_ast()); - if (num_params == 2 && + if (num_params == 2 && s1->is_sort_of(m_bv_fid, BV_SORT) && s2->is_sort_of(m_bv_fid, BV_SORT)) { m_out << "Array"; m_out << "[" << s1->get_parameter(0).get_int(); - m_out << ":" << s2->get_parameter(0).get_int() << "]"; + m_out << ":" << s2->get_parameter(0).get_int() << "]"; return; } m_out << "(Array "; @@ -379,7 +379,7 @@ class smt_printer { } } - + void pp_arg(expr *arg, app *parent) { if (!m_is_smt2 && is_bool(arg) && is_var(arg) && parent->get_family_id() == m_basic_fid) { @@ -387,7 +387,7 @@ class smt_printer { pp_marked_expr(arg); m_out << " 0))"; } else if (!m_is_smt2 && is_bool(arg) && !is_var(arg) && - parent->get_family_id() != m_basic_fid && + parent->get_family_id() != m_basic_fid && parent->get_family_id() != m_dt_fid) { m_out << "(ite "; @@ -403,7 +403,7 @@ class smt_printer { bool is_int, pos; buffer names; unsigned bv_size; - zstring s; + zstring s; unsigned num_args = n->get_num_args(); func_decl* decl = n->get_decl(); if (m_autil.is_numeral(n, val, is_int)) { @@ -433,7 +433,7 @@ class smt_printer { m_out << encs[i]; } } - m_out << "\""; + m_out << "\""; } else if (m_bvutil.is_numeral(n, val, bv_size)) { if (m_is_smt2) { @@ -443,7 +443,7 @@ class smt_printer { m_out << "bv" << val << "[" << bv_size << "]"; } } - else if (m_bvutil.is_bit2bool(n)) { + else if (m_bvutil.is_bit2bool(n)) { unsigned bit = n->get_decl()->get_parameter(0).get_int(); if (m_is_smt2) { m_out << "(= ((_ extract " << bit << " " << bit << ") "; @@ -458,14 +458,14 @@ class smt_printer { } else if (m_manager.is_label(n, pos, names) && names.size() >= 1) { if (m_is_smt2) { - m_out << "(! "; + m_out << "(! "; pp_marked_expr(n->get_arg(0)); m_out << (pos?":lblpos":":lblneg") << " " << m_renaming.get_symbol(names[0]) << ")"; } else { m_out << "(" << (pos?"lblpos":"lblneg") << " " << m_renaming.get_symbol(names[0]) << " "; expr* ch = n->get_arg(0); - pp_marked_expr(ch); + pp_marked_expr(ch); m_out << ")"; } } @@ -547,13 +547,13 @@ class smt_printer { m_out << " "; } } - m_out << ")"; + m_out << ")"; } } void print_no_lets(expr *e) { - smt_printer p(m_out, m_manager, m_qlists, m_renaming, m_logic, true, m_simplify_implies, m_is_smt2, m_indent, m_num_var_names, m_var_names); + smt_printer p(m_out, m_manager, m_qlists, m_renaming, m_logic, true, m_simplify_implies, m_is_smt2, m_indent, m_num_var_names, m_var_names); p(e); } @@ -565,7 +565,7 @@ class smt_printer { } void visit_quantifier(quantifier* q) { - m_qlists.push_back(q); + m_qlists.push_back(q); m_out << "("; if (q->is_forall()) { @@ -588,12 +588,12 @@ class smt_printer { if (m_is_smt2) { m_out << ")"; } - + if (m_is_smt2 && (q->get_num_patterns() > 0 || q->get_qid() != symbol::null)) { m_out << "(! "; } { - smt_printer p(m_out, m_manager, m_qlists, m_renaming, m_logic, false, m_is_smt2, m_simplify_implies, m_indent, m_num_var_names, m_var_names); + smt_printer p(m_out, m_manager, m_qlists, m_renaming, m_logic, false, m_is_smt2, m_simplify_implies, m_indent, m_num_var_names, m_var_names); p(q->get_expr()); } @@ -644,7 +644,7 @@ class smt_printer { void newline() { unsigned i = m_indent; m_out << "\n"; - while (i > 0) { m_out << " "; --i; } + while (i > 0) { m_out << " "; --i; } } void visit_var(var* v) { @@ -685,15 +685,15 @@ class smt_printer { case AST_QUANTIFIER: visit_quantifier(to_quantifier(n)); break; - case AST_APP: + case AST_APP: visit_app(to_app(n)); break; - case AST_VAR: + case AST_VAR: visit_var(to_var(n)); break; default: UNREACHABLE(); - } + } } void visit_expr(expr* n) { @@ -714,7 +714,7 @@ class smt_printer { } m_out << ")"; newline(); - } + } bool is_unit(expr* n) { if (n->get_ref_count() <= 2 && is_small(n)) { @@ -724,9 +724,9 @@ class smt_printer { return true; } switch(n->get_kind()) { - case AST_VAR: + case AST_VAR: return true; - case AST_APP: + case AST_APP: return to_app(n)->get_num_args() == 0; default: return false; @@ -749,9 +749,9 @@ class smt_printer { return sz <= m_line_length; } switch(n->get_kind()) { - case AST_QUANTIFIER: + case AST_QUANTIFIER: return false; - case AST_VAR: + case AST_VAR: sz += 5; return sz <= m_line_length; case AST_APP: { @@ -777,14 +777,14 @@ class smt_printer { } default: return false; - } - } + } + } bool visit_children(expr* n) { unsigned todo_size = m_todo.size(); switch(n->get_kind()) { - case AST_QUANTIFIER: - case AST_VAR: + case AST_QUANTIFIER: + case AST_VAR: break; case AST_APP: { app* a = to_app(n); @@ -805,9 +805,9 @@ class smt_printer { } public: - smt_printer(std::ostream& out, ast_manager& m, ptr_vector& ql, smt_renaming& rn, + smt_printer(std::ostream& out, ast_manager& m, ptr_vector& ql, smt_renaming& rn, symbol logic, bool no_lets, bool is_smt2, bool simplify_implies, unsigned indent, unsigned num_var_names = 0, char const* const* var_names = 0) : - m_out(out), + m_out(out), m_manager(m), m_qlists(ql), m_renaming(rn), @@ -832,7 +832,7 @@ public: m_array_fid = m.mk_family_id("array"); m_dt_fid = m.mk_family_id("datatype"); } - + void operator()(expr* n) { m_top = n; if (!m_no_lets) { @@ -842,7 +842,7 @@ public: m_todo.push_back(to_app(n)->get_arg(i)); } break; - // Don't do this for quantifiers -- they need to have the body be + // Don't do this for quantifiers -- they need to have the body be // visited when the m_qlist contains the relevant quantifier. default: break; @@ -867,7 +867,7 @@ public: pp_marked_expr(n); for (unsigned i = 0; i < m_num_lets; ++i) { - m_out << ")"; + m_out << ")"; } m_mark.reset(); m_num_lets = 0; @@ -880,7 +880,7 @@ public: ptr_vector const* decls; ptr_vector rec_sorts; - rec_sorts.push_back(s); + rec_sorts.push_back(s); mark.mark(s, true); // collect siblings and sorts that have not already been printed. @@ -905,20 +905,20 @@ public: } else { pp_sort_decl(mark, s2); - } + } } } } } if (m_is_smt2) { - // TBD: datatypes may be declared parametrically. + // TBD: datatypes may be declared parametrically. // get access to parametric generalization, or print // monomorphic specialization with a tag that gets reused at use-point. m_out << "(declare-datatypes () ("; } else { - m_out << ":datatypes ("; + m_out << ":datatypes ("; } for (unsigned si = 0; si < rec_sorts.size(); ++si) { s = rec_sorts[si]; @@ -928,7 +928,7 @@ public: decls = util.get_datatype_constructors(s); for (unsigned i = 0; i < decls->size(); ++i) { - func_decl* f = (*decls)[i]; + func_decl* f = (*decls)[i]; ptr_vector const& accs = *util.get_constructor_accessors(f); if (m_is_smt2 || accs.size() > 0) { m_out << "("; @@ -937,7 +937,7 @@ public: if (!accs.empty() || !m_is_smt2) { m_out << " "; } - for (unsigned j = 0; j < accs.size(); ++j) { + for (unsigned j = 0; j < accs.size(); ++j) { func_decl* a = accs[j]; m_out << "(" << m_renaming.get_symbol(a->get_name()) << " "; visit_sort(a->get_range()); @@ -1081,7 +1081,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { ptr_vector ql; ast_manager& m = m_manager; decl_collector decls(m); - smt_renaming rn; + smt_renaming rn; for (unsigned i = 0; i < m_assumptions.size(); ++i) { decls.visit(m_assumptions[i].get()); @@ -1089,7 +1089,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { for (unsigned i = 0; i < m_assumptions_star.size(); ++i) { decls.visit(m_assumptions_star[i].get()); } - decls.visit(n); + decls.visit(n); if (m.is_proof(n)) { strm << "("; @@ -1099,7 +1099,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { } if (m_source_info != symbol::null && m_source_info != symbol("")) { strm << "; :source { " << m_source_info << " }\n"; - } + } if (m.is_bool(n)) { strm << "(set-info :status " << m_status << ")\n"; } @@ -1119,7 +1119,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { if (!(*m_is_declared)(s)) { smt_printer p(strm, m, ql, rn, m_logic, true, true, m_simplify_implies, 0); p.pp_sort_decl(sort_mark, s); - } + } } for (unsigned i = 0; i < decls.get_num_decls(); ++i) { @@ -1147,7 +1147,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { strm << ")\n"; } - for (unsigned i = 0; i < m_assumptions_star.size(); ++i) { + for (unsigned i = 0; i < m_assumptions_star.size(); ++i) { smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 1); strm << "(assert\n "; p(m_assumptions_star[i].get()); @@ -1170,13 +1170,13 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { } else { p(n); - } + } } void ast_smt_pp::display(std::ostream& strm, expr* n) { ptr_vector ql; decl_collector decls(m_manager); - smt_renaming rn; + smt_renaming rn; for (unsigned i = 0; i < m_assumptions.size(); ++i) { decls.visit(m_assumptions[i].get()); @@ -1185,7 +1185,7 @@ void ast_smt_pp::display(std::ostream& strm, expr* n) { decls.visit(m_assumptions_star[i].get()); } decls.visit(n); - + strm << "(benchmark "; if (m_benchmark_name != symbol::null) { @@ -1214,8 +1214,8 @@ void ast_smt_pp::display(std::ostream& strm, expr* n) { sort* s = decls.get_sorts()[i]; if (!(*m_is_declared)(s)) { smt_printer p(strm, m_manager, ql, rn, m_logic, true, false, m_simplify_implies, 0); - p.pp_sort_decl(sort_mark, s); - } + p.pp_sort_decl(sort_mark, s); + } } for (unsigned i = 0; i < decls.get_num_decls(); ++i) { @@ -1242,14 +1242,14 @@ void ast_smt_pp::display(std::ostream& strm, expr* n) { expr * e = m_assumptions[i].get(); strm << ":assumption\n"; smt_printer p(strm, m_manager, ql, rn, m_logic, false, false, m_simplify_implies, 0); - p(e); - strm << "\n"; + p(e); + strm << "\n"; } for (unsigned i = 0; i < m_assumptions_star.size(); ++i) { strm << ":assumption-core\n"; smt_printer p(strm, m_manager, ql, rn, m_logic, false, false, m_simplify_implies, 0); - p(m_assumptions_star[i].get()); + p(m_assumptions_star[i].get()); strm << "\n"; }