mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

converted pp_params

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-11-30 17:20:45 -08:00
parent 4f9442864a
commit 3e6bddbad1
20 changed files with 114 additions and 223 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/api/api_ast.cpp
View file

@ -36,6 +36,7 @@ Revision History:
#include"scoped_ctrl_c.h"
#include"cancel_eh.h"
#include"scoped_timer.h"
#include"pp_params.hpp"
extern "C" {
@ -833,7 +834,8 @@ extern "C" {
break;
case Z3_PRINT_SMTLIB_COMPLIANT: {
ast_smt_pp pp(mk_c(c)->m());
pp.set_simplify_implies(get_pp_default_params().m_pp_simplify_implies);
pp_params params;
pp.set_simplify_implies(params.simplify_implies());
ast* a1 = to_ast(a);
pp.set_logic(mk_c(c)->fparams().m_smtlib_logic.c_str());
if (!is_expr(a1)) {
@ -886,7 +888,8 @@ extern "C" {
pp.set_logic(logic);
pp.set_status(status);
pp.add_attributes(attributes);
pp.set_simplify_implies(get_pp_default_params().m_pp_simplify_implies);
pp_params params;
pp.set_simplify_implies(params.simplify_implies());
for (unsigned i = 0; i < num_assumptions; ++i) {
pp.add_assumption(to_expr(assumptions[i]));
}

2
src/ast/ast_pp.h
View file

@ -24,7 +24,7 @@ Revision History:
#include"ast_smt2_pp.h"
struct mk_pp : public mk_ismt2_pp {
mk_pp(ast * t, ast_manager & m, pp_params const & p, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = 0):
mk_pp(ast * t, ast_manager & m, params_ref const & p, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = 0):
mk_ismt2_pp(t, m, p, indent, num_vars, var_prefix) {
}
mk_pp(ast * t, ast_manager & m, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = 0):

8
src/ast/ast_printer.cpp
View file

@ -33,14 +33,14 @@ public:
virtual void display(std::ostream & out, func_decl * f, unsigned indent = 0) const {
out << f->get_name();
}
virtual void pp(sort * s, format_ns::format_ref & r) const { mk_smt2_format(s, env(), get_pp_default_params(), r); }
virtual void pp(func_decl * f, format_ns::format_ref & r) const { mk_smt2_format(f, env(), get_pp_default_params(), r); }
virtual void pp(sort * s, format_ns::format_ref & r) const { mk_smt2_format(s, env(), params_ref(), r); }
virtual void pp(func_decl * f, format_ns::format_ref & r) const { mk_smt2_format(f, env(), params_ref(), r); }
virtual void pp(expr * n, format_ns::format_ref & r) const {
sbuffer<symbol> buf;
mk_smt2_format(n, env(), get_pp_default_params(), 0, 0, r, buf);
mk_smt2_format(n, env(), params_ref(), 0, 0, r, buf);
}
virtual void pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer<symbol> & var_names) const {
mk_smt2_format(n, env(), get_pp_default_params(), num_vars, var_prefix, r, var_names);
mk_smt2_format(n, env(), params_ref(), num_vars, var_prefix, r, var_names);
}
virtual void display(std::ostream & out, expr * n, unsigned indent, unsigned num_vars, char const * var_prefix, sbuffer<symbol> & var_names) const {
NOT_IMPLEMENTED_YET();

50
src/ast/ast_smt2_pp.cpp
View file

@ -24,6 +24,7 @@ Revision History:
#include"ast_ll_pp.h"
#include"ast_pp.h"
#include"algebraic_numbers.h"
#include"pp_params.hpp"
using namespace format_ns;
#define ALIAS_PREFIX "a"
@ -376,7 +377,6 @@ typedef app_ref_vector format_ref_vector;
class smt2_printer {
ast_manager & m_manager;
pp_params const & m_params;
smt2_pp_environment & m_env;
shared_occs m_soccs;
@ -421,6 +421,16 @@ class smt2_printer {
string_buffer<> m_next_name_buffer;
// Config
bool m_pp_decimal;
unsigned m_pp_decimal_precision;
bool m_pp_bv_lits;
bool m_pp_bv_neg;
unsigned m_pp_max_depth;
unsigned m_pp_min_alias_size;
bool m_pp_flat_assoc;
symbol next_name(char const * prefix, unsigned & idx) {
while (true) {
m_next_name_buffer.reset();
@ -508,10 +518,10 @@ class smt2_printer {
void pp_const(app * c) {
format * f;
if (m_env.get_autil().is_numeral(c) || m_env.get_autil().is_irrational_algebraic_numeral(c)) {
f = m_env.pp_arith_literal(c, m_params.m_pp_decimal, m_params.m_pp_decimal_precision);
f = m_env.pp_arith_literal(c, m_pp_decimal, m_pp_decimal_precision);
}
else if (m_env.get_bvutil().is_numeral(c)) {
f = m_env.pp_bv_literal(c, m_params.m_pp_bv_lits, m_params.m_pp_bv_neg);
f = m_env.pp_bv_literal(c, m_pp_bv_lits, m_pp_bv_neg);
}
else if (m_env.get_futil().is_value(c)) {
f = m_env.pp_float_literal(c);
@ -584,8 +594,8 @@ 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_params.m_pp_max_depth) ||
((f_info.m_weight >= m_params.m_pp_min_alias_size || is_quantifier(t)) && m_soccs.is_shared(t)))) {
((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())
@ -602,7 +612,7 @@ class smt2_printer {
}
bool flat_assoc(app * t, frame const & fr) {
if (!m_params.m_pp_flat_assoc)
if (!m_pp_flat_assoc)
return false;
func_decl * f = t->get_decl();
if (f->is_associative() && m_frame_stack.size() >= 2 && !m_soccs.is_shared(t)) {
@ -943,9 +953,8 @@ class smt2_printer {
}
public:
smt2_printer(smt2_pp_environment & env, pp_params const & params):
smt2_printer(smt2_pp_environment & env, params_ref const & params):
m_manager(env.get_manager()),
m_params(params),
m_env(env),
m_soccs(m_manager),
m_root(0),
@ -953,6 +962,15 @@ public:
m_next_alias_idx(1),
m_format_stack(fm()) {
init_expr2alias_stack();
pp_params p(params);
m_pp_decimal = p.decimal();
m_pp_decimal_precision = p.decimal_precision();
m_pp_bv_lits = p.bv_literals();
m_pp_bv_neg = p.bv_neg();
m_pp_max_depth = p.max_depth();
m_pp_min_alias_size = p.min_alias_size();
m_pp_flat_assoc = p.flat_assoc();
}
~smt2_printer() {
@ -1003,24 +1021,24 @@ public:
};
void mk_smt2_format(expr * n, smt2_pp_environment & env, pp_params 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);
pr(n, num_vars, var_prefix, r, var_names);
}
void mk_smt2_format(sort * s, smt2_pp_environment & env, pp_params const & p, format_ref & r) {
void mk_smt2_format(sort * s, smt2_pp_environment & env, params_ref const & p, format_ref & r) {
smt2_printer pr(env, p);
pr(s, r);
}
void mk_smt2_format(func_decl * f, smt2_pp_environment & env, pp_params const & p, format_ref & r) {
void mk_smt2_format(func_decl * f, smt2_pp_environment & env, params_ref const & p, format_ref & r) {
smt2_printer pr(env, p);
pr(f, r);
}
std::ostream & ast_smt2_pp(std::ostream & out, expr * n, smt2_pp_environment & env, pp_params 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));
@ -1032,7 +1050,7 @@ std::ostream & ast_smt2_pp(std::ostream & out, expr * n, smt2_pp_environment & e
return out;
}
std::ostream & ast_smt2_pp(std::ostream & out, sort * s, smt2_pp_environment & env, pp_params const & p, unsigned indent) {
std::ostream & ast_smt2_pp(std::ostream & out, sort * s, smt2_pp_environment & env, params_ref const & p, unsigned indent) {
ast_manager & m = env.get_manager();
format_ref r(fm(m));
sbuffer<symbol> var_names;
@ -1043,7 +1061,7 @@ std::ostream & ast_smt2_pp(std::ostream & out, sort * s, smt2_pp_environment & e
return out;
}
std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, smt2_pp_environment & env, pp_params const & p, unsigned indent) {
std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, smt2_pp_environment & env, params_ref const & p, unsigned indent) {
ast_manager & m = env.get_manager();
format_ref r(fm(m));
sbuffer<symbol> var_names;
@ -1054,7 +1072,7 @@ std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, smt2_pp_environmen
return out;
}
mk_ismt2_pp::mk_ismt2_pp(ast * t, ast_manager & m, pp_params const & p, unsigned indent, unsigned num_vars, char const * var_prefix):
mk_ismt2_pp::mk_ismt2_pp(ast * t, ast_manager & m, params_ref const & p, unsigned indent, unsigned num_vars, char const * var_prefix):
m_ast(t),
m_manager(m),
m_params(p),
@ -1066,7 +1084,7 @@ mk_ismt2_pp::mk_ismt2_pp(ast * t, ast_manager & m, pp_params const & p, unsigned
mk_ismt2_pp::mk_ismt2_pp(ast * t, ast_manager & m, unsigned indent, unsigned num_vars, char const * var_prefix):
m_ast(t),
m_manager(m),
m_params(get_pp_default_params()),
m_params(m_empty),
m_indent(indent),
m_num_vars(num_vars),
m_var_prefix(var_prefix) {

29
src/ast/ast_smt2_pp.h
View file

@ -23,7 +23,7 @@ Revision History:
#define _AST_SMT2_PP_H_
#include"format.h"
#include"pp_params.h"
#include"params.h"
#include"arith_decl_plugin.h"
#include"bv_decl_plugin.h"
#include"array_decl_plugin.h"
@ -82,28 +82,29 @@ public:
virtual bool uses(symbol const & s) const { return false; }
};
void mk_smt2_format(expr * n, smt2_pp_environment & env, pp_params const & p,
void mk_smt2_format(expr * n, smt2_pp_environment & env, params_ref const & p,
unsigned num_vars, char const * var_prefix,
format_ns::format_ref & r, sbuffer<symbol> & var_names);
void mk_smt2_format(sort * s, smt2_pp_environment & env, pp_params const & p, format_ns::format_ref & r);
void mk_smt2_format(func_decl * f, smt2_pp_environment & env, pp_params const & p, format_ns::format_ref & r);
void mk_smt2_format(sort * s, smt2_pp_environment & env, params_ref const & p, format_ns::format_ref & r);
void mk_smt2_format(func_decl * f, smt2_pp_environment & env, params_ref const & p, format_ns::format_ref & r);
std::ostream & ast_smt2_pp(std::ostream & out, expr * n, smt2_pp_environment & env, pp_params const & p, unsigned indent = 0,
std::ostream & ast_smt2_pp(std::ostream & out, expr * n, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0,
unsigned num_vars = 0, char const * var_prefix = 0);
std::ostream & ast_smt2_pp(std::ostream & out, sort * s, smt2_pp_environment & env, pp_params const & p, unsigned indent = 0);
std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, smt2_pp_environment & env, pp_params const & p, unsigned indent = 0);
std::ostream & ast_smt2_pp(std::ostream & out, sort * s, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0);
std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0);
/**
\brief Internal wrapper (for debugging purposes only)
*/
struct mk_ismt2_pp {
ast * m_ast;
ast_manager & m_manager;
pp_params const & m_params;
unsigned m_indent;
unsigned m_num_vars;
char const * m_var_prefix;
mk_ismt2_pp(ast * t, ast_manager & m, pp_params const & p, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = 0);
ast * m_ast;
ast_manager & m_manager;
params_ref m_empty;
params_ref const & m_params;
unsigned m_indent;
unsigned m_num_vars;
char const * m_var_prefix;
mk_ismt2_pp(ast * t, ast_manager & m, params_ref const & p, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = 0);
mk_ismt2_pp(ast * t, ast_manager & m, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = 0);
};

61
src/ast/pp.cpp
View file

@ -17,40 +17,9 @@ Revision History:
--*/
#include"pp.h"
#include"pp_params.hpp"
using namespace format_ns;
void pp_param_descrs(param_descrs & p) {
p.insert("max_indent", CPK_UINT, "max. indentation in pretty printer");
p.insert("max_num_lines", CPK_UINT, "max. number of lines to be displayed in pretty printer");
p.insert("max_width", CPK_UINT, "max. width in pretty printer");
p.insert("max_ribbon", CPK_UINT, "max. ribbon (width - indentation) in pretty printer");
p.insert("max_depth", CPK_UINT, "max. term depth (when pretty printing SMT2 terms/formulas)");
p.insert("min_alias_size", CPK_UINT, "min. size for creating an alias for a shared term (when pretty printing SMT2 terms/formulas)");
p.insert("decimal", CPK_BOOL, "pretty print real numbers using decimal notation (the output may be truncated). Z3 adds a '?' if the value is not precise");
p.insert("decimal_precision", CPK_BOOL, "maximum number of decimal places to be used when pp.decimal=true");
p.insert("bv_literals", CPK_BOOL, "use Bit-Vector literals (e.g, #x0F and #b0101) during pretty printing");
p.insert("bv_neg", CPK_BOOL, "use bvneg when displaying Bit-Vector literals where the most significant bit is 1");
p.insert("flat_assoc", CPK_BOOL, "flat associative operators (when pretty printing SMT2 terms/formulas)");
p.insert("fixed_indent", CPK_BOOL, "use a fixed indentation for applications");
p.insert("single_line", CPK_BOOL, "ignore line breaks when true");
p.insert("bounded", CPK_BOOL, "ignore characters exceeding max widht");
p.insert("simplify_implies", CPK_BOOL, "simplify nested implications for pretty printing");
}
pp_params g_pp_params;
void set_pp_default_params(pp_params const & p) {
g_pp_params = p;
}
void register_pp_params(ini_params & p) {
g_pp_params.register_params(p);
}
pp_params const & get_pp_default_params() {
return g_pp_params;
}
static std::pair<unsigned, bool> space_upto_line_break(ast_manager & m, format * f) {
unsigned r;
SASSERT(f->get_family_id() == fm(m).get_family_id("format"));
@ -87,7 +56,15 @@ inline bool fits(ast_manager & m, format * f, unsigned space_left) {
return s <= space_left;
}
void pp(std::ostream & out, format * f, ast_manager & m, pp_params const & p) {
void pp(std::ostream & out, format * f, ast_manager & m, params_ref const & _p) {
pp_params p(_p);
unsigned max_width = p.max_width();
unsigned max_ribbon = p.max_ribbon();
unsigned max_num_lines = p.max_num_lines();
unsigned max_indent = p.max_indent();
bool bounded = p.bounded();
bool single_line = p.single_line();
unsigned pos = 0;
unsigned ribbon_pos = 0;
unsigned line = 0;
@ -98,7 +75,7 @@ void pp(std::ostream & out, format * f, ast_manager & m, pp_params const & p) {
todo.push_back(std::make_pair(f, 0));
app_ref space(mk_string(m, " "), fm(m));
while (!todo.empty()) {
if (line >= p.m_pp_max_num_lines)
if (line >= max_num_lines)
return;
std::pair<format *, unsigned> pair = todo.back();
format * f = pair.first;
@ -107,10 +84,10 @@ void pp(std::ostream & out, format * f, ast_manager & m, pp_params const & p) {
SASSERT(f->get_family_id() == fm(m).get_family_id("format"));
switch (f->get_decl_kind()) {
case OP_STRING:
if (p.m_pp_bounded && pos > p.m_pp_max_width)
if (bounded && pos > max_width)
break;
len = static_cast<unsigned>(strlen(f->get_decl()->get_parameter(0).get_symbol().bare_str()));
if (p.m_pp_bounded && pos + len > p.m_pp_max_width) {
if (bounded && pos + len > max_width) {
out << "...";
break;
}
@ -121,7 +98,7 @@ void pp(std::ostream & out, format * f, ast_manager & m, pp_params const & p) {
case OP_INDENT:
todo.push_back(std::make_pair(to_app(f->get_arg(0)),
std::min(indent + f->get_decl()->get_parameter(0).get_int(),
p.m_pp_max_indent)));
max_indent)));
break;
case OP_COMPOSE:
i = f->get_num_args();
@ -131,7 +108,7 @@ void pp(std::ostream & out, format * f, ast_manager & m, pp_params const & p) {
}
break;
case OP_CHOICE:
space_left = std::min(p.m_pp_max_width - pos, p.m_pp_max_ribbon - pos);
space_left = std::min(max_width - pos, max_ribbon - pos);
if (space_left > 0 && fits(m, to_app(f->get_arg(0)), space_left))
todo.push_back(std::make_pair(to_app(f->get_arg(0)), indent));
else
@ -139,14 +116,14 @@ void pp(std::ostream & out, format * f, ast_manager & m, pp_params const & p) {
break;
case OP_LINE_BREAK:
case OP_LINE_BREAK_EXT:
if (p.m_pp_single_line) {
if (single_line) {
todo.push_back(std::make_pair(space, indent));
break;
}
pos = indent;
ribbon_pos = 0;
line++;
if (line < p.m_pp_max_num_lines) {
if (line < max_num_lines) {
out << "\n";
for (unsigned i = 0; i < indent; i++)
out << " ";
@ -160,7 +137,3 @@ void pp(std::ostream & out, format * f, ast_manager & m, pp_params const & p) {
}
}
void pp(std::ostream & out, format_ns::format * f, ast_manager & m) {
pp(out, f, m, g_pp_params);
}

14
src/ast/pp.h
View file

@ -20,21 +20,9 @@ Revision History:
#define _PP_H_
#include"format.h"
#include"pp_params.h"
#include"params.h"
/*
REG_MODULE_PARAMS('pp', 'pp_param_descrs')
*/
void pp_param_descrs(param_descrs & d);
void set_pp_default_params(pp_params const & p);
void register_pp_params(ini_params & p);
pp_params const & get_pp_default_params();
void pp(std::ostream & out, format_ns::format * f, ast_manager & m, pp_params const & p);
void pp(std::ostream & out, format_ns::format * f, ast_manager & m);
void pp(std::ostream & out, format_ns::format * f, ast_manager & m, params_ref const & p = params_ref());
#endif /* _PP_H_ */

57
src/ast/pp_params.cpp
View file

@ -1,57 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
pp_params.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-01-20.
Revision History:
--*/
#include"pp_params.h"
pp_params::pp_params():
m_pp_max_indent(UINT_MAX),
m_pp_max_num_lines(UINT_MAX),
m_pp_max_width(80),
m_pp_max_ribbon(80),
m_pp_max_depth(5),
m_pp_min_alias_size(10),
m_pp_decimal(false),
m_pp_decimal_precision(10),
m_pp_bv_lits(true),
m_pp_bv_neg(false),
m_pp_flat_assoc(true),
m_pp_fixed_indent(false),
m_pp_single_line(false),
m_pp_bounded(false),
m_pp_simplify_implies(false) {
}
void pp_params::register_params(ini_params & p) {
p.register_unsigned_param("PP_MAX_INDENT", m_pp_max_indent, "max. indentation in pretty printer", true);
p.register_unsigned_param("PP_MAX_NUM_LINES", m_pp_max_num_lines, "max. number of lines to be displayed in pretty printer", true);
p.register_unsigned_param("PP_MAX_WIDTH", m_pp_max_width, "max. width in pretty printer", true);
p.register_unsigned_param("PP_MAX_RIBBON", m_pp_max_ribbon, "max. ribbon (width - indentation) in pretty printer", true);
p.register_unsigned_param("PP_MAX_DEPTH", m_pp_max_depth, "max. term depth (when pretty printing SMT2 terms/formulas)", true);
p.register_unsigned_param("PP_MIN_ALIAS_SIZE", m_pp_min_alias_size, "min. size for creating an alias for a shared term (when pretty printing SMT2 terms/formulas)", true);
p.register_bool_param("PP_DECIMAL", m_pp_decimal, "pretty print real numbers using decimal notation (the output may be truncated). Z3 adds a '?' if the value is not precise", true);
p.register_unsigned_param("PP_DECIMAL_PRECISION", m_pp_decimal_precision, "maximum number of decimal places to be used when PP_DECIMAL=true", true);
p.register_bool_param("PP_BV_LITERALS", m_pp_bv_lits, "use Bit-Vector literals (e.g, #x0F and #b0101) during pretty printing", true);
p.register_bool_param("PP_BV_NEG", m_pp_bv_neg, "use bvneg when displaying Bit-Vector literals where the most significant bit is 1", true);
p.register_bool_param("PP_FLAT_ASSOC", m_pp_flat_assoc, "flat associative operators (when pretty printing SMT2 terms/formulas)", true);
p.register_bool_param("PP_FIXED_INDENT", m_pp_fixed_indent, "use a fixed indentation for applications", true);
p.register_bool_param("PP_SINGLE_LINE", m_pp_single_line, "ignore line breaks when true", true);
p.register_bool_param("PP_BOUNDED", m_pp_bounded, "ignore characters exceeding max widht", true);
p.register_bool_param("PP_SIMPLIFY_IMPLIES", m_pp_simplify_implies, "simplify nested implications for pretty printing", true);
}

46
src/ast/pp_params.h
View file

@ -1,46 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
pp_params.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-01-20.
Revision History:
--*/
#ifndef _PP_PARAMS_H_
#define _PP_PARAMS_H_
#include"ini_file.h"
struct pp_params {
unsigned m_pp_max_indent; // max. indentation
unsigned m_pp_max_num_lines; // max. num. lines
unsigned m_pp_max_width; // max. width
unsigned m_pp_max_ribbon; // max. ribbon: width - indentation
unsigned m_pp_max_depth;
unsigned m_pp_min_alias_size;
bool m_pp_decimal; // display reals using decimals
unsigned m_pp_decimal_precision; // max. number of decimal places
bool m_pp_bv_lits;
bool m_pp_bv_neg; // use bvneg to display bit-vector literals which the most significant bit is 1
bool m_pp_flat_assoc;
bool m_pp_fixed_indent;
bool m_pp_single_line; // ignore line breaks if true
bool m_pp_bounded; // ignore characters exceeding max width.
bool m_pp_simplify_implies; // simplify nested implications during pretty printing
pp_params();
void register_params(ini_params & p);
};
#endif /* _PP_PARAMS_H_ */

17
src/ast/pp_params.pyg Normal file
View file

@ -0,0 +1,17 @@
def_module_params('pp',
export=True,
params=(('max_indent', UINT, UINT_MAX, 'max. indentation in pretty printer'),
('max_num_lines', UINT, UINT_MAX, 'max. number of lines to be displayed in pretty printer'),
('max_width', UINT, 80, 'max. width in pretty printer'),
('max_ribbon', UINT, 80, 'max. ribbon (width - indentation) in pretty printer'),
('max_depth', UINT, 5, 'max. term depth (when pretty printing SMT2 terms/formulas)'),
('min_alias_size', UINT, 10, 'min. size for creating an alias for a shared term (when pretty printing SMT2 terms/formulas)'),
('decimal', BOOL, False, 'pretty print real numbers using decimal notation (the output may be truncated). Z3 adds a ? if the value is not precise'),
('decimal_precision', UINT, 10, 'maximum number of decimal places to be used when pp.decimal=true'),
('bv_literals', BOOL, True, 'use Bit-Vector literals (e.g, #x0F and #b0101) during pretty printing'),
('bv_neg', BOOL, False, 'use bvneg when displaying Bit-Vector literals where the most significant bit is 1'),
('flat_assoc', BOOL, True, 'flat associative operators (when pretty printing SMT2 terms/formulas)'),
('fixed_indent', BOOL, False, 'use a fixed indentation for applications'),
('single_line', BOOL, False, 'ignore line breaks when true'),
('bounded', BOOL, False, 'ignore characters exceeding max widht'),
('simplify_implies', BOOL, True, 'simplify nested implications for pretty printing')))

4
src/ast/substitution/substitution_tree.cpp
View file

@ -607,8 +607,8 @@ void substitution_tree::display(std::ostream & out, node * n, unsigned delta) co
out << " ";
display(out, n->m_subst);
if (n->m_leaf) {
pp_params p;
p.m_pp_single_line = true;
params_ref p;
p.set_bool("single_line", true);
out << " ==> ";
out << mk_pp(n->m_expr, m_manager, p);
out << "\n";

11
src/cmd_context/cmd_context.cpp
View file

@ -1536,8 +1536,7 @@ cmd_context::pp_env & cmd_context::get_pp_env() const {
}
void cmd_context::pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer<symbol> & var_names) const {
mk_smt2_format(n, get_pp_env(), get_pp_default_params(),
num_vars, var_prefix, r, var_names);
mk_smt2_format(n, get_pp_env(), params_ref(), num_vars, var_prefix, r, var_names);
}
void cmd_context::pp(expr * n, format_ns::format_ref & r) const {
@ -1546,7 +1545,7 @@ void cmd_context::pp(expr * n, format_ns::format_ref & r) const {
}
void cmd_context::pp(func_decl * f, format_ns::format_ref & r) const {
mk_smt2_format(f, get_pp_env(), get_pp_default_params(), r);
mk_smt2_format(f, get_pp_env(), params_ref(), r);
}
void cmd_context::display(std::ostream & out, sort * s, unsigned indent) const {
@ -1554,7 +1553,7 @@ void cmd_context::display(std::ostream & out, sort * s, unsigned indent) const {
f = pp(s);
if (indent > 0)
f = format_ns::mk_indent(m(), indent, f);
::pp(out, f.get(), m(), get_pp_default_params());
::pp(out, f.get(), m());
}
void cmd_context::display(std::ostream & out, expr * n, unsigned indent, unsigned num_vars, char const * var_prefix, sbuffer<symbol> & var_names) const {
@ -1562,7 +1561,7 @@ void cmd_context::display(std::ostream & out, expr * n, unsigned indent, unsigne
pp(n, num_vars, var_prefix, f, var_names);
if (indent > 0)
f = format_ns::mk_indent(m(), indent, f);
::pp(out, f.get(), m(), get_pp_default_params());
::pp(out, f.get(), m());
}
void cmd_context::display(std::ostream & out, expr * n, unsigned indent) const {
@ -1575,7 +1574,7 @@ void cmd_context::display(std::ostream & out, func_decl * d, unsigned indent) co
pp(d, f);
if (indent > 0)
f = format_ns::mk_indent(m(), indent, f);
::pp(out, f.get(), m(), get_pp_default_params());
::pp(out, f.get(), m());
}
void cmd_context::dump_assertions(std::ostream & out) const {

8
src/cmd_context/extra_cmds/polynomial_cmds.cpp
View file

@ -26,10 +26,10 @@ Notes:
#include"parametric_cmd.h"
#include"mpq.h"
#include"algebraic_numbers.h"
#include"pp.h"
#include"pp_params.h"
#include"polynomial_var2value.h"
#include"expr2var.h"
#include"pp.h"
#include"pp_params.hpp"
static void to_poly(cmd_context & ctx, expr * t) {
polynomial::numeral_manager nm;
@ -145,9 +145,11 @@ class poly_isolate_roots_cmd : public cmd {
scoped_anum_vector rs(m_am);
m_am.isolate_roots(m_p, m_x2v, rs);
ctx.regular_stream() << "(roots";
pp_params params;
bool pp_decimal = params.decimal();
for (unsigned i = 0; i < rs.size(); i++) {
ctx.regular_stream() << std::endl;
if (!get_pp_default_params().m_pp_decimal)
if (!pp_decimal)
m_am.display_root_smt2(ctx.regular_stream(), rs[i]);
else
m_am.display_decimal(ctx.regular_stream(), rs[i]);

1
src/front_end_params/front_end_params.h
View file

@ -23,7 +23,6 @@ Revision History:
#include"ast.h"
#include"preprocessor_params.h"
#include"smt_params.h"
#include"pp_params.h"
#include"parser_params.h"
#include"arith_simplifier_params.h"
#include"model_params.h"

3
src/model/model_pp.cpp
View file

@ -85,8 +85,7 @@ static void display_functions(std::ostream & out, model_core const & md) {
if (fi->is_partial())
out << " #unspecified";
else {
pp_params const & params = get_pp_default_params();
out << " " << mk_ismt2_pp(fi->get_else(), m, params, 5, arity, "x");
out << " " << mk_ismt2_pp(fi->get_else(), m, params_ref(), 5, arity, "x");
}
for (unsigned j = 0; j < num_entries; j++)
out << ")";

4
src/model/model_smt2_pp.cpp
View file

@ -128,7 +128,7 @@ static void pp_uninterp_sorts(std::ostream & out, ast_printer_context & ctx, mod
format_ref f_card(fm(m));
f_card = mk_indent(m, indent, mk_seq1<format**, f2f>(m, f_args, f_args+2, f2f(), "forall"));
pp_indent(out, indent);
pp(out, f_card, m, get_pp_default_params());
pp(out, f_card, m);
out << "\n";
pp_indent(out, indent);
out << ";; -----------\n";
@ -284,7 +284,7 @@ static void pp_funs(std::ostream & out, ast_printer_context & ctx, model_core co
body.get(),
mk_string(m, ")")))));
pp_indent(out, indent);
pp(out, def.get(), m, get_pp_default_params());
pp(out, def.get(), m);
out << "\n";
}
}

8
src/muz_qe/dl_context.cpp
View file

@ -1672,12 +1672,11 @@ namespace datalog {
bool print_low_level = m_params.get_bool("print_low_level_smt2", false);
bool do_declare_vars = m_params.get_bool("print_with_variable_declarations", true);
#define PP(_e_) if (print_low_level) out << mk_smt_pp(_e_, m); else ast_smt2_pp(out, _e_, env, params);
#define PP(_e_) if (print_low_level) out << mk_smt_pp(_e_, m); else ast_smt2_pp(out, _e_, env);
get_rules_as_formulas(rules, names);
smt2_pp_environment_dbg env(m);
pp_params params;
mk_fresh_name fresh_names;
collect_free_funcs(num_axioms, axioms, visited, visitor, fresh_names);
collect_free_funcs(rules.size(), rules.c_ptr(), visited, visitor, fresh_names);
@ -1719,7 +1718,7 @@ namespace datalog {
func_decl* f = *it;
out << "(declare-rel " << f->get_name() << " (";
for (unsigned i = 0; i < f->get_arity(); ++i) {
ast_smt2_pp(out, f->get_domain(i), env, params);
ast_smt2_pp(out, f->get_domain(i), env);
if (i + 1 < f->get_arity()) {
out << " ";
}
@ -1796,7 +1795,6 @@ namespace datalog {
//
smt2_pp_environment_dbg env(m);
var_subst vsubst(m, false);
pp_params param;
expr_ref_vector fresh_vars(m), subst(m);
expr_ref res(m);
@ -1839,7 +1837,7 @@ namespace datalog {
symbol name = fresh_names.next();
fresh_vars.push_back(m.mk_const(name, s));
out << "(declare-var " << name << " ";
ast_smt2_pp(out, s, env, param);
ast_smt2_pp(out, s, env);
out << ")\n";
}
subst.push_back(fresh_vars[vars[max_var]].get());

4
src/muz_qe/pdr_manager.cpp
View file

@ -29,7 +29,6 @@ Revision History:
#include "model_smt2_pp.h"
#include "model_converter.h"
namespace pdr {
class collect_decls_proc {
@ -143,11 +142,10 @@ namespace pdr {
}
}
smt2_pp_environment_dbg env(m);
pp_params params;
func_decl_set::iterator it = aux_decls.begin(), end = aux_decls.end();
for (; it != end; ++it) {
func_decl* f = *it;
ast_smt2_pp(out, f, env, params);
ast_smt2_pp(out, f, env);
out << "\n";
}

1
src/shell/main.cpp
View file

@ -127,7 +127,6 @@ void init_params() {
g_extra_params = new extra_params();
register_verbosity_level(*g_params);
register_warning(*g_params);
register_pp_params(*g_params);
g_front_end_params->register_params(*g_params);
g_extra_params->register_params(*g_params);
g_params_initialized = true;

2
src/tactic/fpa/fpa2bv_converter.cpp
View file

@ -105,7 +105,7 @@ void fpa2bv_converter::mk_value(func_decl * f, unsigned num, expr * const * args
mk_triple(bv_sgn, bv_sig, biased_exp, result);
TRACE("fpa2bv_dbg", tout << "value of [" << sign << " " << m_mpz_manager.to_string(sig) << " " << exp << "] is "
<< mk_ismt2_pp(result, m) << std::endl;);
<< mk_ismt2_pp(result, m) << std::endl;);
}
}