mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

whitespace

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-03-29 16:13:31 +01:00
parent 7eec68c954
commit 19e73fb2ad
2 changed files with 114 additions and 114 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

86
src/ast/ast_smt2_pp.cpp
View file

@ -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<format> 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<expr> m_aliased_exprs;
format_ref_vector m_aliased_pps;
svector<std::pair<unsigned, symbol> > m_aliased_lvls_names;
unsigned m_next_alias_idx;
svector<std::pair<unsigned, symbol> > 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<symbol> m_var_names;
typedef hashtable<symbol, symbol_hash_proc, symbol_eq_proc> 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<frame> 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<unsigned>(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<format**, f2f>(m(), it, end, f2f()),
mk_seq<format**, f2f>(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<format**, f2f>(m(), it, end, f2f()),
mk_seq<format**, f2f>(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<format> 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<format**, f2f>(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<symbol> & 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<symbol> 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<symbol> 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<symbol> 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;
}

142
src/ast/ast_smt_pp.cpp
View file

@ -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<symbol> 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<quantifier>& ql, smt_renaming& rn,
smt_printer(std::ostream& out, ast_manager& m, ptr_vector<quantifier>& 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<func_decl> const* decls;
ptr_vector<sort> 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<func_decl> 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<quantifier> 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<quantifier> 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";
}