From 3e6bddbad1d8e7886b13abaadfcabef416df7acc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 30 Nov 2012 17:20:45 -0800
Subject: [PATCH] converted pp_params
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
src/api/api_ast.cpp | 7 ++-
src/ast/ast_pp.h | 2 +-
src/ast/ast_printer.cpp | 8 +--
src/ast/ast_smt2_pp.cpp | 50 ++++++++++-----
src/ast/ast_smt2_pp.h | 29 ++++-----
src/ast/pp.cpp | 61 ++++++-------------
src/ast/pp.h | 14 +----
src/ast/pp_params.cpp | 57 -----------------
src/ast/pp_params.h | 46 --------------
src/ast/pp_params.pyg | 17 ++++++
src/ast/substitution/substitution_tree.cpp | 4 +-
src/cmd_context/cmd_context.cpp | 11 ++--
.../extra_cmds/polynomial_cmds.cpp | 8 ++-
src/front_end_params/front_end_params.h | 1 -
src/model/model_pp.cpp | 3 +-
src/model/model_smt2_pp.cpp | 4 +-
src/muz_qe/dl_context.cpp | 8 +--
src/muz_qe/pdr_manager.cpp | 4 +-
src/shell/main.cpp | 1 -
src/tactic/fpa/fpa2bv_converter.cpp | 2 +-
20 files changed, 114 insertions(+), 223 deletions(-)
delete mode 100644 src/ast/pp_params.cpp
delete mode 100644 src/ast/pp_params.h
create mode 100644 src/ast/pp_params.pyg
diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index 1503b387f..45892bac3 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -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]));
}
diff --git a/src/ast/ast_pp.h b/src/ast/ast_pp.h
index d99fb7670..7e7bdfc4e 100644
--- a/src/ast/ast_pp.h
+++ b/src/ast/ast_pp.h
@@ -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):
diff --git a/src/ast/ast_printer.cpp b/src/ast/ast_printer.cpp
index 33ddcb709..8d6ed91f7 100644
--- a/src/ast/ast_printer.cpp
+++ b/src/ast/ast_printer.cpp
@@ -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();
diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
index dcc7a1a0d..afe301ddf 100644
--- a/src/ast/ast_smt2_pp.cpp
+++ b/src/ast/ast_smt2_pp.cpp
@@ -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) {
diff --git a/src/ast/ast_smt2_pp.h b/src/ast/ast_smt2_pp.h
index 048dd8d67..aa84d6e03 100644
--- a/src/ast/ast_smt2_pp.h
+++ b/src/ast/ast_smt2_pp.h
@@ -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);
};
diff --git a/src/ast/pp.cpp b/src/ast/pp.cpp
index d05776e78..13247127d 100644
--- a/src/ast/pp.cpp
+++ b/src/ast/pp.cpp
@@ -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);
-}
-
diff --git a/src/ast/pp.h b/src/ast/pp.h
index 13afcb07c..f567afa4a 100644
--- a/src/ast/pp.h
+++ b/src/ast/pp.h
@@ -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_ */
diff --git a/src/ast/pp_params.cpp b/src/ast/pp_params.cpp
deleted file mode 100644
index 0cf3e455d..000000000
--- a/src/ast/pp_params.cpp
+++ /dev/null
@@ -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);
-}
-
diff --git a/src/ast/pp_params.h b/src/ast/pp_params.h
deleted file mode 100644
index 970f97968..000000000
--- a/src/ast/pp_params.h
+++ /dev/null
@@ -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_ */
-
diff --git a/src/ast/pp_params.pyg b/src/ast/pp_params.pyg
new file mode 100644
index 000000000..57d6e185d
--- /dev/null
+++ b/src/ast/pp_params.pyg
@@ -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')))
diff --git a/src/ast/substitution/substitution_tree.cpp b/src/ast/substitution/substitution_tree.cpp
index 81b2f7be6..037d51e32 100644
--- a/src/ast/substitution/substitution_tree.cpp
+++ b/src/ast/substitution/substitution_tree.cpp
@@ -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";
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index d14ce3076..5dcc4268c 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -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 {
diff --git a/src/cmd_context/extra_cmds/polynomial_cmds.cpp b/src/cmd_context/extra_cmds/polynomial_cmds.cpp
index 7b37b750e..e68789dac 100644
--- a/src/cmd_context/extra_cmds/polynomial_cmds.cpp
+++ b/src/cmd_context/extra_cmds/polynomial_cmds.cpp
@@ -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]);
diff --git a/src/front_end_params/front_end_params.h b/src/front_end_params/front_end_params.h
index f9e62cd01..b87265c01 100644
--- a/src/front_end_params/front_end_params.h
+++ b/src/front_end_params/front_end_params.h
@@ -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"
diff --git a/src/model/model_pp.cpp b/src/model/model_pp.cpp
index a8e8a0880..b968c7184 100644
--- a/src/model/model_pp.cpp
+++ b/src/model/model_pp.cpp
@@ -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 << ")";
diff --git a/src/model/model_smt2_pp.cpp b/src/model/model_smt2_pp.cpp
index 1a639b5f1..929668638 100644
--- a/src/model/model_smt2_pp.cpp
+++ b/src/model/model_smt2_pp.cpp
@@ -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";
}
}
diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp
index 4a9bba27c..3a2844964 100644
--- a/src/muz_qe/dl_context.cpp
+++ b/src/muz_qe/dl_context.cpp
@@ -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());
diff --git a/src/muz_qe/pdr_manager.cpp b/src/muz_qe/pdr_manager.cpp
index ad53f45db..9536d8f36 100644
--- a/src/muz_qe/pdr_manager.cpp
+++ b/src/muz_qe/pdr_manager.cpp
@@ -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";
}
diff --git a/src/shell/main.cpp b/src/shell/main.cpp
index d6e7b1bf1..56882a02b 100644
--- a/src/shell/main.cpp
+++ b/src/shell/main.cpp
@@ -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;
diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp
index 77ff50e9b..62cc76266 100644
--- a/src/tactic/fpa/fpa2bv_converter.cpp
+++ b/src/tactic/fpa/fpa2bv_converter.cpp
@@ -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;);
}
}