From a99b8fe797d8a26d358f6013a1a06c444b2ca5ad Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 2 Dec 2012 22:03:30 -0800 Subject: [PATCH] exposed rewriter parameters Signed-off-by: Leonardo de Moura --- scripts/mk_util.py | 6 +- src/ast/rewriter/arith_rewriter.cpp | 41 ++--- src/ast/rewriter/arith_rewriter_params.pyg | 15 ++ src/ast/rewriter/array_rewriter.cpp | 11 +- src/ast/rewriter/array_rewriter_params.pyg | 5 + src/ast/rewriter/bool_rewriter.cpp | 24 ++- src/ast/rewriter/bool_rewriter_params.pyg | 9 + src/ast/rewriter/bv_rewriter.cpp | 28 ++- src/ast/rewriter/bv_rewriter_params.pyg | 10 ++ src/ast/rewriter/poly_rewriter_def.h | 19 +- src/ast/rewriter/poly_rewriter_params.pyg | 8 + src/ast/rewriter/rewriter_params.pyg | 11 ++ src/ast/rewriter/th_rewriter.cpp | 25 ++- src/ast/rewriter/th_rewriter.h | 3 - src/shell/main.cpp | 14 +- src/util/gparams.cpp | 198 ++++++++++++++------- 16 files changed, 265 insertions(+), 162 deletions(-) create mode 100644 src/ast/rewriter/arith_rewriter_params.pyg create mode 100644 src/ast/rewriter/array_rewriter_params.pyg create mode 100644 src/ast/rewriter/bool_rewriter_params.pyg create mode 100644 src/ast/rewriter/bv_rewriter_params.pyg create mode 100644 src/ast/rewriter/poly_rewriter_params.pyg create mode 100644 src/ast/rewriter/rewriter_params.pyg diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 2906b11fe..98fae665a 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1507,11 +1507,15 @@ def def_module_params(module_name, export, params, class_name=None, description= print "Generated '%s'" % hpp def max_memory_param(): - return ('max_memory', UINT, UINT_MAX, 'maximum amount of memory in megabytes.') + return ('max_memory', UINT, UINT_MAX, 'maximum amount of memory in megabytes') + +def max_steps_param(): + return ('max_steps', UINT, UINT_MAX, 'maximum number of steps') PYG_GLOBALS = { 'UINT' : UINT, 'BOOL' : BOOL, 'DOUBLE' : DOUBLE, 'STRING' : STRING, 'SYMBOL' : SYMBOL, 'UINT_MAX' : UINT_MAX, 'max_memory_param' : max_memory_param, + 'max_steps_param' : max_steps_param, 'def_module_params' : def_module_params } # Execute python auxiliary scripts that generate extra code for Z3. diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index f5fdcf8af..a5dfda6e7 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -17,23 +17,25 @@ Notes: --*/ #include"arith_rewriter.h" +#include"arith_rewriter_params.hpp" #include"poly_rewriter_def.h" #include"algebraic_numbers.h" #include"ast_pp.h" -void arith_rewriter::updt_local_params(params_ref const & p) { - m_arith_lhs = p.get_bool("arith_lhs", false); - m_gcd_rounding = p.get_bool("gcd_rounding", false); - m_eq2ineq = p.get_bool("eq2ineq", false); - m_elim_to_real = p.get_bool("elim_to_real", false); - m_push_to_real = p.get_bool("push_to_real", true); - m_anum_simp = p.get_bool("algebraic_number_evaluator", true); - m_max_degree = p.get_uint("max_degree", 64); - m_expand_power = p.get_bool("expand_power", false); - m_mul2power = p.get_bool("mul_to_power", false); - m_elim_rem = p.get_bool("elim_rem", false); - m_expand_tan = p.get_bool("expand_tan", false); - set_sort_sums(p.get_bool("sort_sums", false)); // set here to avoid collision with bvadd +void arith_rewriter::updt_local_params(params_ref const & _p) { + arith_rewriter_params p(_p); + m_arith_lhs = p.arith_lhs(); + m_gcd_rounding = p.gcd_rounding(); + m_eq2ineq = p.eq2ineq(); + m_elim_to_real = p.elim_to_real(); + m_push_to_real = p.push_to_real(); + m_anum_simp = p.algebraic_number_evaluator(); + m_max_degree = p.max_degree(); + m_expand_power = p.expand_power(); + m_mul2power = p.mul_to_power(); + m_elim_rem = p.elim_rem(); + m_expand_tan = p.expand_tan(); + set_sort_sums(p.sort_sums()); } void arith_rewriter::updt_params(params_ref const & p) { @@ -43,18 +45,7 @@ void arith_rewriter::updt_params(params_ref const & p) { void arith_rewriter::get_param_descrs(param_descrs & r) { poly_rewriter::get_param_descrs(r); - r.insert("algebraic_number_evaluator", CPK_BOOL, "(default: true) simplify/evaluate expressions containing (algebraic) irrational numbers."); - r.insert("mul_to_power", CPK_BOOL, "(default: false) collpase (* t ... t) into (^ t k), it is ignored if expand_power is true."); - r.insert("expand_power", CPK_BOOL, "(default: false) expand (^ t k) into (* t ... t) if 1 < k <= max_degree."); - r.insert("expand_tan", CPK_BOOL, "(default: false) replace (tan x) with (/ (sin x) (cos x))."); - r.insert("max_degree", CPK_UINT, "(default: 64) max degree of algebraic numbers (and power operators) processed by simplifier."); - r.insert("eq2ineq", CPK_BOOL, "(default: false) split arithmetic equalities into two inequalities."); - r.insert("sort_sums", CPK_BOOL, "(default: false) sort the arguments of + application."); - r.insert("gcd_rounding", CPK_BOOL, "(default: false) use gcd rounding on integer arithmetic atoms."); - r.insert("arith_lhs", CPK_BOOL, "(default: false) all monomials are moved to the left-hand-side, and the right-hand-side is just a constant."); - r.insert("elim_to_real", CPK_BOOL, "(default: false) eliminate to_real from arithmetic predicates that contain only integers."); - r.insert("push_to_real", CPK_BOOL, "(default: true) distribute to_real over * and +."); - r.insert("elim_rem", CPK_BOOL, "(default: false) replace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y)))."); + arith_rewriter_params::collect_param_descrs(r); } br_status arith_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { diff --git a/src/ast/rewriter/arith_rewriter_params.pyg b/src/ast/rewriter/arith_rewriter_params.pyg new file mode 100644 index 000000000..8a41d838d --- /dev/null +++ b/src/ast/rewriter/arith_rewriter_params.pyg @@ -0,0 +1,15 @@ +def_module_params(module_name='rewriter', + class_name='arith_rewriter_params', + export=True, + params=(("algebraic_number_evaluator", BOOL, True, "simplify/evaluate expressions containing (algebraic) irrational numbers."), + ("mul_to_power", BOOL, False, "collpase (* t ... t) into (^ t k), it is ignored if expand_power is true."), + ("expand_power", BOOL, False, "expand (^ t k) into (* t ... t) if 1 < k <= max_degree."), + ("expand_tan", BOOL, False, "replace (tan x) with (/ (sin x) (cos x))."), + ("max_degree", UINT, 64, "max degree of algebraic numbers (and power operators) processed by simplifier."), + ("eq2ineq", BOOL, False, "split arithmetic equalities into two inequalities."), + ("sort_sums", BOOL, False, "sort the arguments of + application."), + ("gcd_rounding", BOOL, False, "use gcd rounding on integer arithmetic atoms."), + ("arith_lhs", BOOL, False, "all monomials are moved to the left-hand-side, and the right-hand-side is just a constant."), + ("elim_to_real", BOOL, False, "eliminate to_real from arithmetic predicates that contain only integers."), + ("push_to_real", BOOL, True, "distribute to_real over * and +."), + ("elim_rem", BOOL, False, "replace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y)))."))) diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index ac93e0f87..9dbbeb231 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -17,17 +17,18 @@ Notes: --*/ #include"array_rewriter.h" +#include"array_rewriter_params.hpp" #include"ast_lt.h" #include"ast_pp.h" -void array_rewriter::updt_params(params_ref const & p) { - m_sort_store = p.get_bool("sort_store", false); - m_expand_select_store = p.get_bool("expand_select_store", false); +void array_rewriter::updt_params(params_ref const & _p) { + array_rewriter_params p(_p); + m_sort_store = p.sort_store(); + m_expand_select_store = p.expand_select_store(); } void array_rewriter::get_param_descrs(param_descrs & r) { - r.insert("expand_select_store", CPK_BOOL, "(default: false) replace a (select (store ...) ...) term by an if-then-else term."); - r.insert("sort_store", CPK_BOOL, "(default: false) sort nested stores when the indices are known to be different."); + array_rewriter_params::collect_param_descrs(r); } br_status array_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { diff --git a/src/ast/rewriter/array_rewriter_params.pyg b/src/ast/rewriter/array_rewriter_params.pyg new file mode 100644 index 000000000..2e3ae9f6a --- /dev/null +++ b/src/ast/rewriter/array_rewriter_params.pyg @@ -0,0 +1,5 @@ +def_module_params(module_name='rewriter', + class_name='array_rewriter_params', + export=True, + params=(("expand_select_store", BOOL, False, "replace a (select (store ...) ...) term by an if-then-else term"), + ("sort_store", BOOL, False, "sort nested stores when the indices are known to be different"))) diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index b3f422fe5..4fcaf02fe 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -17,25 +17,21 @@ Notes: --*/ #include"bool_rewriter.h" +#include"bool_rewriter_params.hpp" #include"rewriter_def.h" -void bool_rewriter::updt_params(params_ref const & p) { - m_flat = p.get_bool("flat", true); - m_elim_and = p.get_bool("elim_and", false); - m_local_ctx = p.get_bool("local_ctx", false); - m_local_ctx_limit = p.get_uint("local_ctx_limit", UINT_MAX); - m_blast_distinct = p.get_bool("blast_distinct", false); - m_ite_extra_rules = p.get_bool("ite_extra_rules", false); +void bool_rewriter::updt_params(params_ref const & _p) { + bool_rewriter_params p(_p); + m_flat = p.flat(); + m_elim_and = p.elim_and(); + m_local_ctx = p.local_ctx(); + m_local_ctx_limit = p.local_ctx_limit(); + m_blast_distinct = p.blast_distinct(); + m_ite_extra_rules = p.ite_extra_rules(); } void bool_rewriter::get_param_descrs(param_descrs & r) { - r.insert("ite_extra_rules", CPK_BOOL, - "(default: false) extra ite simplifications, these additional simplifications may reduce size locally but increase globally."); - r.insert("flat", CPK_BOOL, "(default: true) create nary applications for and,or,+,*,bvadd,bvmul,bvand,bvor,bvxor."); - r.insert("elim_and", CPK_BOOL, "(default: false) conjunctions are rewritten using negation and disjunctions."); - r.insert("local_ctx", CPK_BOOL, "(default: false) perform local (i.e., cheap) context simplifications."); - r.insert("local_ctx_limit", CPK_UINT, "(default: inf) limit for applying local context simplifier."); - r.insert("blast_distinct", CPK_BOOL, "(default: false) expand a distinct predicate into a quadratic number of disequalities."); + bool_rewriter_params::collect_param_descrs(r); } br_status bool_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { diff --git a/src/ast/rewriter/bool_rewriter_params.pyg b/src/ast/rewriter/bool_rewriter_params.pyg new file mode 100644 index 000000000..a5bcf6f5d --- /dev/null +++ b/src/ast/rewriter/bool_rewriter_params.pyg @@ -0,0 +1,9 @@ +def_module_params(module_name='rewriter', + class_name='bool_rewriter_params', + export=True, + params=(("ite_extra_rules", BOOL, False, "extra ite simplifications, these additional simplifications may reduce size locally but increase globally"), + ("flat", BOOL, True, "create nary applications for and,or,+,*,bvadd,bvmul,bvand,bvor,bvxor"), + ("elim_and", BOOL, False, "conjunctions are rewritten using negation and disjunctions"), + ("local_ctx", BOOL, False, "perform local (i.e., cheap) context simplifications"), + ("local_ctx_limit", UINT, UINT_MAX, "limit for applying local context simplifier"), + ("blast_distinct", BOOL, False, "expand a distinct predicate into a quadratic number of disequalities"))) diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index fbc1f7c11..5fd562676 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -17,6 +17,7 @@ Notes: --*/ #include"bv_rewriter.h" +#include"bv_rewriter_params.hpp" #include"poly_rewriter_def.h" #include"ast_smt2_pp.h" @@ -53,15 +54,16 @@ app * mk_extract_proc::operator()(unsigned high, unsigned low, expr * arg) { return r; } -void bv_rewriter::updt_local_params(params_ref const & p) { - m_hi_div0 = p.get_bool("hi_div0", true); - m_elim_sign_ext = p.get_bool("elim_sign_ext", true); - m_mul2concat = p.get_bool("mul2concat", false); - m_bit2bool = p.get_bool("bit2bool", true); - m_blast_eq_value = p.get_bool("blast_eq_value", false); - m_mkbv2num = p.get_bool("mkbv2num", false); - m_split_concat_eq = p.get_bool("split_concat_eq", false); - m_udiv2mul = p.get_bool("udiv2mul", false); +void bv_rewriter::updt_local_params(params_ref const & _p) { + bv_rewriter_params p(_p); + m_hi_div0 = p.hi_div0(); + m_elim_sign_ext = p.elim_sign_ext(); + m_mul2concat = p.mul2concat(); + m_bit2bool = p.bit2bool(); + m_blast_eq_value = p.blast_eq_value(); + m_split_concat_eq = p.split_concat_eq(); + m_udiv2mul = p.udiv2mul(); + m_mkbv2num = _p.get_bool("mkbv2num", false); } void bv_rewriter::updt_params(params_ref const & p) { @@ -71,13 +73,7 @@ void bv_rewriter::updt_params(params_ref const & p) { void bv_rewriter::get_param_descrs(param_descrs & r) { poly_rewriter::get_param_descrs(r); - r.insert("udiv2mul", CPK_BOOL, "(default: false) convert constant udiv to mul."); - r.insert("split_concat_eq", CPK_BOOL, "(default: false) split equalities of the form (= (concat t1 t2) t3)."); - r.insert("bit2bool", CPK_BOOL, "(default: true) try to convert bit-vector terms of size 1 into Boolean terms."); - r.insert("blast_eq_value", CPK_BOOL, "(default: false) blast (some) Bit-vector equalities into bits."); - r.insert("elim_sign_ext", CPK_BOOL, "(default: true) expand sign-ext operator using concat and extract."); - r.insert("hi_div0", CPK_BOOL, "(default: true) use the 'hardware interpretation' for division by zero (for bit-vector terms)."); - r.insert("mul2concat", CPK_BOOL, "(default: false) replace multiplication by a power of two into a concatenation."); + bv_rewriter_params::collect_param_descrs(r); #ifndef _EXTERNAL_RELEASE r.insert("mkbv2num", CPK_BOOL, "(default: false) convert (mkbv [true/false]*) into a numeral"); #endif diff --git a/src/ast/rewriter/bv_rewriter_params.pyg b/src/ast/rewriter/bv_rewriter_params.pyg new file mode 100644 index 000000000..780d8e724 --- /dev/null +++ b/src/ast/rewriter/bv_rewriter_params.pyg @@ -0,0 +1,10 @@ +def_module_params(module_name='rewriter', + class_name='bv_rewriter_params', + export=True, + params=(("udiv2mul", BOOL, False, "convert constant udiv to mul"), + ("split_concat_eq", BOOL, False, "split equalities of the form (= (concat t1 t2) t3)"), + ("bit2bool", BOOL, True, "try to convert bit-vector terms of size 1 into Boolean terms"), + ("blast_eq_value", BOOL, False, "blast (some) Bit-vector equalities into bits"), + ("elim_sign_ext", BOOL, True, "expand sign-ext operator using concat and extract"), + ("hi_div0", BOOL, True, "use the 'hardware interpretation' for division by zero (for bit-vector terms)"), + ("mul2concat", BOOL, False, "replace multiplication by a power of two into a concatenation"))) diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h index e6c8a653c..290144c75 100644 --- a/src/ast/rewriter/poly_rewriter_def.h +++ b/src/ast/rewriter/poly_rewriter_def.h @@ -17,6 +17,7 @@ Notes: --*/ #include"poly_rewriter.h" +#include"poly_rewriter_params.hpp" #include"ast_lt.h" #include"ast_ll_pp.h" #include"ast_smt2_pp.h" @@ -26,20 +27,18 @@ char const * poly_rewriter::g_ste_blowup_msg = "sum of monomials blowup" template -void poly_rewriter::updt_params(params_ref const & p) { - m_flat = p.get_bool("flat", true); - m_som = p.get_bool("som", false); - m_hoist_mul = p.get_bool("hoist_mul", false); - m_hoist_cmul = p.get_bool("hoist_cmul", false); - m_som_blowup = p.get_uint("som_blowup", UINT_MAX); +void poly_rewriter::updt_params(params_ref const & _p) { + poly_rewriter_params p(_p); + m_flat = p.flat(); + m_som = p.som(); + m_hoist_mul = p.hoist_mul(); + m_hoist_cmul = p.hoist_cmul(); + m_som_blowup = p.som_blowup(); } template void poly_rewriter::get_param_descrs(param_descrs & r) { - r.insert("som", CPK_BOOL, "(default: false) put polynomials in som-of-monomials form."); - r.insert("som_blowup", CPK_UINT, "(default: infty) maximum number of monomials generated when putting a polynomial in sum-of-monomials normal form"); - r.insert("hoist_mul", CPK_BOOL, "(default: false) hoist multiplication over summation to minimize number of multiplications"); - r.insert("hoist_cmul", CPK_BOOL, "(default: false) hoist constant multiplication over summation to minimize number of multiplications"); + poly_rewriter_params::collect_param_descrs(r); } template diff --git a/src/ast/rewriter/poly_rewriter_params.pyg b/src/ast/rewriter/poly_rewriter_params.pyg new file mode 100644 index 000000000..18d1e1dba --- /dev/null +++ b/src/ast/rewriter/poly_rewriter_params.pyg @@ -0,0 +1,8 @@ +def_module_params(module_name='rewriter', + class_name='poly_rewriter_params', + export=True, + params=(("som", BOOL, False, "put polynomials in som-of-monomials form"), + ("som_blowup", UINT, UINT_MAX, "maximum number of monomials generated when putting a polynomial in sum-of-monomials normal form"), + ("hoist_mul", BOOL, False, "hoist multiplication over summation to minimize number of multiplications"), + ("hoist_cmul", BOOL, False, "hoist constant multiplication over summation to minimize number of multiplications"), + ("flat", BOOL, True, "create nary applications for and,or,+,*,bvadd,bvmul,bvand,bvor,bvxor"))) diff --git a/src/ast/rewriter/rewriter_params.pyg b/src/ast/rewriter/rewriter_params.pyg new file mode 100644 index 000000000..3a8ed5d5e --- /dev/null +++ b/src/ast/rewriter/rewriter_params.pyg @@ -0,0 +1,11 @@ +def_module_params('rewriter', + description='new formula simplification module used in the tactic framework, and new solvers', + export=True, + params=(max_memory_param(), + max_steps_param(), + ("flat", BOOL, True, "create nary applications for and,or,+,*,bvadd,bvmul,bvand,bvor,bvxor"), + ("push_ite_arith", BOOL, False, "push if-then-else over arithmetic terms."), + ("push_ite_bv", BOOL, False, "push if-then-else over bit-vector terms."), + ("pull_cheap_ite", BOOL, False, "pull if-then-else terms when cheap."), + ("cache_all", BOOL, False, "cache all intermediate results."))) + diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index da4dd3860..07ee7698d 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -17,6 +17,7 @@ Notes: --*/ #include"th_rewriter.h" +#include"rewriter_params.hpp" #include"bool_rewriter.h" #include"arith_rewriter.h" #include"bv_rewriter.h" @@ -56,14 +57,15 @@ struct th_rewriter_cfg : public default_rewriter_cfg { ast_manager & m() const { return m_b_rw.m(); } - void updt_local_params(params_ref const & p) { - m_flat = p.get_bool("flat", true); - m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); - m_max_steps = p.get_uint("max_steps", UINT_MAX); - m_pull_cheap_ite = p.get_bool("pull_cheap_ite", false); - m_cache_all = p.get_bool("cache_all", false); - m_push_ite_arith = p.get_bool("push_ite_arith", false); - m_push_ite_bv = p.get_bool("push_ite_bv", false); + void updt_local_params(params_ref const & _p) { + rewriter_params p(_p); + m_flat = p.flat(); + m_max_memory = megabytes_to_bytes(p.max_memory()); + m_max_steps = p.max_steps(); + m_pull_cheap_ite = p.pull_cheap_ite(); + m_cache_all = p.cache_all(); + m_push_ite_arith = p.push_ite_arith(); + m_push_ite_bv = p.push_ite_bv(); } void updt_params(params_ref const & p) { @@ -693,12 +695,7 @@ void th_rewriter::get_param_descrs(param_descrs & r) { arith_rewriter::get_param_descrs(r); bv_rewriter::get_param_descrs(r); array_rewriter::get_param_descrs(r); - insert_max_memory(r); - insert_max_steps(r); - r.insert("push_ite_arith", CPK_BOOL, "(default: false) push if-then-else over arithmetic terms."); - r.insert("push_ite_bv", CPK_BOOL, "(default: false) push if-then-else over bit-vector terms."); - r.insert("pull_cheap_ite", CPK_BOOL, "(default: false) pull if-then-else terms when cheap."); - r.insert("cache_all", CPK_BOOL, "(default: false) cache all intermediate results."); + rewriter_params::collect_param_descrs(r); } th_rewriter::~th_rewriter() { diff --git a/src/ast/rewriter/th_rewriter.h b/src/ast/rewriter/th_rewriter.h index 19a89d286..b25558dd9 100644 --- a/src/ast/rewriter/th_rewriter.h +++ b/src/ast/rewriter/th_rewriter.h @@ -37,9 +37,6 @@ public: void updt_params(params_ref const & p); static void get_param_descrs(param_descrs & r); - /* - REG_MODULE_PARAMS('simplify', 'th_rewriter::get_param_descrs') - */ unsigned get_cache_size() const; unsigned get_num_steps() const; diff --git a/src/shell/main.cpp b/src/shell/main.cpp index 6dd4aa2e8..21ee8b71c 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -80,8 +80,8 @@ void display_usage() { std::cout << " " << OPT << "p display Z3 global (and module) parameters.\n"; std::cout << " " << OPT << "pd display Z3 global (and module) parameter descriptions.\n"; std::cout << " " << OPT << "pm:name display Z3 module ('name') parameters.\n"; - std::cout << " " << OPT << "pp:name display Z3 parameter description.\n"; - std::cout << " --" << " all remaining arguments are assumed to be part of the input file name. This option allows Z3 to read files with strange names such as: -foo.smt2.\n"; + std::cout << " " << OPT << "pp:name display Z3 parameter description, if 'name' is not provided, then all module names are listed.\n"; + std::cout << " --" << " all remaining arguments are assumed to be part of the input file name. This option allows Z3 to read files with strange names such as: -foo.smt2.\n"; std::cout << "\nResources:\n"; // timeout and memout are now available on Linux and OSX too. std::cout << " " << OPT << "T:timeout set the timeout (in seconds).\n"; @@ -199,9 +199,13 @@ void parse_cmd_line_args(int argc, char ** argv) { exit(0); } else if (strcmp(opt_name, "pm") == 0) { - if (!opt_arg) - error("option argument (-pm:name) is missing."); - gparams::display_module(std::cout, opt_arg); + if (opt_arg) { + gparams::display_module(std::cout, opt_arg); + } + else { + gparams::display_modules(std::cout); + std::cout << "\nUse -pm:name to display all parameters available at module 'name'\n"; + } exit(0); } else if (strcmp(opt_name, "pp") == 0) { diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index 314049727..4aecd0c05 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -36,13 +36,27 @@ bool is_old_param_name(symbol const & name) { } struct gparams::imp { + bool m_modules_registered; dictionary m_module_param_descrs; dictionary m_module_descrs; param_descrs m_param_descrs; dictionary m_module_params; params_ref m_params; + + void check_registered() { + if (m_modules_registered) + return; + m_modules_registered = true; + gparams_register_modules(); + } + + dictionary & get_module_param_descrs() { check_registered(); return m_module_param_descrs; } + dictionary & get_module_descrs() { check_registered(); return m_module_descrs; } + param_descrs & get_param_descrs() { check_registered(); return m_param_descrs; } + public: - imp() { + imp(): + m_modules_registered(false) { } ~imp() { @@ -62,35 +76,45 @@ public: } } + // ----------------------------------------------- + // + // Module registration routines. + // They are invoked when descriptions are initialized + // + // ----------------------------------------------- + void register_global(param_descrs & d) { - #pragma omp critical (gparams) - { - m_param_descrs.copy(d); - } + // Don't need synchronization here, this method + // is invoked from check_registered that is already protected. + m_param_descrs.copy(d); } void register_module(char const * module_name, param_descrs * d) { - #pragma omp critical (gparams) - { - symbol s(module_name); - param_descrs * old_d; - if (m_module_param_descrs.find(s, old_d)) { - old_d->copy(*d); - dealloc(d); - } - else { - m_module_param_descrs.insert(s, d); - } + // Don't need synchronization here, this method + // is invoked from check_registered that is already protected. + symbol s(module_name); + param_descrs * old_d; + if (m_module_param_descrs.find(s, old_d)) { + old_d->copy(*d); + dealloc(d); + } + else { + m_module_param_descrs.insert(s, d); } } void register_module_descr(char const * module_name, char const * descr) { - #pragma omp critical (gparams) - { - m_module_descrs.insert(symbol(module_name), descr); - } + // Don't need synchronization here, this method + // is invoked from check_registered that is already protected. + m_module_descrs.insert(symbol(module_name), descr); } + // ----------------------------------------------- + // + // Parameter setting & retrieval + // + // ----------------------------------------------- + void normalize(char const * name, /* out */ symbol & mod_name, /* out */ symbol & param_name) { if (*name == ':') name++; @@ -132,7 +156,7 @@ public: void throw_unknown_parameter(symbol const & param_name, symbol const & mod_name) { if (mod_name == symbol::null) { if (is_old_param_name(param_name)) { - throw exception("unknown parameter '%s', this is an old parameter name, invoke 'z3 -ps' to obtain the new parameter list", + throw exception("unknown parameter '%s', this is an old parameter name, invoke 'z3 -p' to obtain the new parameter list", param_name.bare_str()); } else { @@ -191,11 +215,11 @@ public: symbol m, p; normalize(name, m, p); if (m == symbol::null) { - set(m_param_descrs, p, value, m); + set(get_param_descrs(), p, value, m); } else { param_descrs * d; - if (m_module_param_descrs.find(m, d)) { + if (get_module_param_descrs().find(m, d)) { set(*d, p, value, m); } else { @@ -203,7 +227,7 @@ public: } } } - catch (exception & ex) { + catch (z3_exception & ex) { // Exception cannot cross critical section boundaries. error = true; error_msg = ex.msg(); @@ -243,7 +267,7 @@ public: r = get_value(m_params, p); } else { - r = get_default(m_param_descrs, p, m); + r = get_default(get_param_descrs(), p, m); } } else { @@ -253,7 +277,7 @@ public: } else { param_descrs * d; - if (m_module_param_descrs.find(m, d)) { + if (get_module_param_descrs().find(m, d)) { r = get_default(*d, p, m); } else { @@ -262,7 +286,7 @@ public: } } } - catch (exception & ex) { + catch (z3_exception & ex) { // Exception cannot cross critical section boundaries. error = true; error_msg = ex.msg(); @@ -295,23 +319,29 @@ public: return result; } + // ----------------------------------------------- + // + // Pretty printing + // + // ----------------------------------------------- + void display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) { #pragma omp critical (gparams) { out << "Global parameters\n"; - m_param_descrs.display(out, indent + 4, smt2_style, include_descr); + get_param_descrs().display(out, indent + 4, smt2_style, include_descr); out << "\n"; if (!smt2_style) { out << "To set a module parameter, use .=value\n"; out << "Example: pp.decimal=true\n"; out << "\n"; } - dictionary::iterator it = m_module_param_descrs.begin(); - dictionary::iterator end = m_module_param_descrs.end(); + dictionary::iterator it = get_module_param_descrs().begin(); + dictionary::iterator end = get_module_param_descrs().end(); for (; it != end; ++it) { out << "[module] " << it->m_key; char const * descr = 0; - if (m_module_descrs.find(it->m_key, descr)) { + if (get_module_descrs().find(it->m_key, descr)) { out << ", description: " << descr; } out << "\n"; @@ -321,53 +351,84 @@ public: } void display_modules(std::ostream & out) { - dictionary::iterator it = m_module_param_descrs.begin(); - dictionary::iterator end = m_module_param_descrs.end(); - for (; it != end; ++it) { - out << "[module] " << it->m_key; - char const * descr = 0; - if (m_module_descrs.find(it->m_key, descr)) { - out << ", description: " << descr; + #pragma omp critical (gparams) + { + dictionary::iterator it = get_module_param_descrs().begin(); + dictionary::iterator end = get_module_param_descrs().end(); + for (; it != end; ++it) { + out << "[module] " << it->m_key; + char const * descr = 0; + if (get_module_descrs().find(it->m_key, descr)) { + out << ", description: " << descr; + } + out << "\n"; } - out << "\n"; } } void display_module(std::ostream & out, symbol const & module_name) { - param_descrs * d = 0; - if (!m_module_param_descrs.find(module_name, d)) - throw exception("unknown module '%s'", module_name.bare_str()); - out << "[module] " << module_name; - char const * descr = 0; - if (m_module_descrs.find(module_name, descr)) { - out << ", description: " << descr; + bool error = false; + std::string error_msg; + #pragma omp critical (gparams) + { + try { + param_descrs * d = 0; + if (!get_module_param_descrs().find(module_name, d)) + throw exception("unknown module '%s'", module_name.bare_str()); + out << "[module] " << module_name; + char const * descr = 0; + if (get_module_descrs().find(module_name, descr)) { + out << ", description: " << descr; + } + out << "\n"; + d->display(out, 4, false); + } + catch (z3_exception & ex) { + // Exception cannot cross critical section boundaries. + error = true; + error_msg = ex.msg(); + } } - out << "\n"; - d->display(out, 4, false); + if (error) + throw exception(error_msg); } void display_parameter(std::ostream & out, char const * name) { - symbol m, p; - normalize(name, m, p); - std::cout << name << " " << m << " " << p << "\n"; - param_descrs * d; - if (m == symbol::null) { - d = &m_param_descrs; + bool error = false; + std::string error_msg; + #pragma omp critical (gparams) + { + try { + symbol m, p; + normalize(name, m, p); + std::cout << name << " " << m << " " << p << "\n"; + param_descrs * d; + if (m == symbol::null) { + d = &get_param_descrs(); + } + else { + if (!get_module_param_descrs().find(m, d)) + throw exception("unknown module '%s'", m.bare_str()); + } + if (!d->contains(p)) + throw_unknown_parameter(p, m); + out << " name: " << p << "\n"; + if (m != symbol::null) { + out << " module: " << m << "\n"; + out << " qualified name: " << m << "." << p << "\n"; + } + out << " type: " << d->get_kind(p) << "\n"; + out << " description: " << d->get_descr(p) << "\n"; + out << " default value: " << d->get_default(p) << "\n"; + } + catch (z3_exception & ex) { + // Exception cannot cross critical section boundaries. + error = true; + error_msg = ex.msg(); + } } - else { - if (!m_module_param_descrs.find(m, d)) - throw exception("unknown module '%s'", m.bare_str()); - } - if (!d->contains(p)) - throw_unknown_parameter(p, m); - out << " name: " << p << "\n"; - if (m != symbol::null) { - out << " module: " << m << "\n"; - out << " qualified name: " << m << "." << p << "\n"; - } - out << " type: " << d->get_kind(p) << "\n"; - out << " description: " << d->get_descr(p) << "\n"; - out << " default value: " << d->get_default(p) << "\n"; + if (error) + throw exception(error_msg); } }; @@ -447,7 +508,6 @@ void gparams::display_parameter(std::ostream & out, char const * name) { void gparams::init() { TRACE("gparams", tout << "gparams::init()\n";); g_imp = alloc(imp); - gparams_register_modules(); } void gparams::finalize() {