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

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2012-12-03 08:14:54 -08:00
commit 361e9039bb
28 changed files with 462 additions and 240 deletions
Download patch file Download diff file Expand all files Collapse all files

6
scripts/mk_util.py
View file

@ -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.

41
src/ast/rewriter/arith_rewriter.cpp
View file

@ -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<arith_rewriter_core>::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) {

15
src/ast/rewriter/arith_rewriter_params.pyg Normal file
View file

@ -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))).")))

11
src/ast/rewriter/array_rewriter.cpp
View file

@ -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) {

5
src/ast/rewriter/array_rewriter_params.pyg Normal file
View file

@ -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")))

24
src/ast/rewriter/bool_rewriter.cpp
View file

@ -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) {

9
src/ast/rewriter/bool_rewriter_params.pyg Normal file
View file

@ -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")))

28
src/ast/rewriter/bv_rewriter.cpp
View file

@ -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<bv_rewriter_core>::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

10
src/ast/rewriter/bv_rewriter_params.pyg Normal file
View file

@ -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")))

19
src/ast/rewriter/poly_rewriter_def.h
View file

@ -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<Config>::g_ste_blowup_msg = "sum of monomials blowup"
template<typename Config>
void poly_rewriter<Config>::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<Config>::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<typename Config>
void poly_rewriter<Config>::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<typename Config>

8
src/ast/rewriter/poly_rewriter_params.pyg Normal file
View file

@ -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")))

11
src/ast/rewriter/rewriter_params.pyg Normal file
View file

@ -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.")))

25
src/ast/rewriter/th_rewriter.cpp
View file

@ -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() {

3
src/ast/rewriter/th_rewriter.h
View file

@ -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;

14
src/sat/sat_asymm_branch.cpp
View file

@ -17,6 +17,7 @@ Revision History:
--*/
#include"sat_asymm_branch.h"
#include"sat_asymm_branch_params.hpp"
#include"sat_solver.h"
#include"stopwatch.h"
#include"trace.h"
@ -193,18 +194,17 @@ namespace sat {
}
}
void asymm_branch::updt_params(params_ref const & p) {
m_asymm_branch = p.get_bool("asymm_branch", true);
m_asymm_branch_rounds = p.get_uint("asymm_branch_rounds", 32);
m_asymm_branch_limit = p.get_uint("asymm_branch_limit", 100000000);
void asymm_branch::updt_params(params_ref const & _p) {
sat_asymm_branch_params p(_p);
m_asymm_branch = p.asymm_branch();
m_asymm_branch_rounds = p.asymm_branch_rounds();
m_asymm_branch_limit = p.asymm_branch_limit();
if (m_asymm_branch_limit > INT_MAX)
m_asymm_branch_limit = INT_MAX;
}
void asymm_branch::collect_param_descrs(param_descrs & d) {
d.insert("asymm_branch", CPK_BOOL, "(default: true) asymmetric branching.");
d.insert("asymm_branch_rounds", CPK_UINT, "(default: 32) maximum number of rounds of asymmetric branching.");
d.insert("asymm_branch_limit", CPK_UINT, "approx. maximum number of literals visited during asymmetric branching.");
sat_asymm_branch_params::collect_param_descrs(d);
}
void asymm_branch::collect_statistics(statistics & st) {

6
src/sat/sat_asymm_branch_params.pyg Normal file
View file

@ -0,0 +1,6 @@
def_module_params(module_name='sat',
class_name='sat_asymm_branch_params',
export=True,
params=(('asymm_branch', BOOL, True, 'asymmetric branching'),
('asymm_branch.rounds', UINT, 32, 'maximum number of rounds of asymmetric branching'),
('asymm_branch.limit', UINT, 100000000, 'approx. maximum number of literals visited during asymmetric branching')))

70
src/sat/sat_config.cpp
View file

@ -18,6 +18,7 @@ Revision History:
--*/
#include"sat_config.h"
#include"sat_types.h"
#include"sat_params.hpp"
namespace sat {
@ -36,10 +37,11 @@ namespace sat {
updt_params(p);
}
void config::updt_params(params_ref const & p) {
m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
void config::updt_params(params_ref const & _p) {
sat_params p(_p);
m_max_memory = megabytes_to_bytes(p.max_memory());
symbol s = p.get_sym("restart", m_luby);
symbol s = p.restart();
if (s == m_luby)
m_restart = RS_LUBY;
else if (s == m_geometric)
@ -47,7 +49,7 @@ namespace sat {
else
throw sat_param_exception("invalid restart strategy");
s = p.get_sym("phase", m_caching);
s = p.phase();
if (s == m_always_false)
m_phase = PS_ALWAYS_FALSE;
else if (s == m_always_true)
@ -59,29 +61,31 @@ namespace sat {
else
throw sat_param_exception("invalid phase selection strategy");
m_phase_caching_on = p.get_uint("phase_caching_on", 400);
m_phase_caching_off = p.get_uint("phase_caching_off", 100);
m_phase_caching_on = p.phase_caching_on();
m_phase_caching_off = p.phase_caching_off();
m_restart_initial = p.get_uint("restart_initial", 100);
m_restart_factor = p.get_double("restart_factor", 1.5);
m_restart_initial = p.restart_initial();
m_restart_factor = p.restart_factor();
m_random_freq = p.get_double("random_freq", 0.01);
m_random_freq = p.random_freq();
m_burst_search = p.get_uint("burst_search", 100);
m_burst_search = p.burst_search();
m_max_conflicts = p.get_uint("max_conflicts", UINT_MAX);
m_max_conflicts = p.max_conflicts();
// These parameters are not exposed
m_simplify_mult1 = _p.get_uint("simplify_mult1", 300);
m_simplify_mult2 = _p.get_double("simplify_mult2", 1.5);
m_simplify_max = _p.get_uint("simplify_max", 500000);
// --------------------------------
m_simplify_mult1 = p.get_uint("simplify_mult1", 300);
m_simplify_mult2 = p.get_double("simplify_mult2", 1.5);
m_simplify_max = p.get_uint("simplify_max", 500000);
s = p.get_sym("gc_strategy", m_glue_psm);
s = p.gc();
if (s == m_dyn_psm) {
m_gc_strategy = GC_DYN_PSM;
m_gc_initial = p.get_uint("gc_initial", 500);
m_gc_increment = p.get_uint("gc_increment", 100);
m_gc_small_lbd = p.get_uint("gc_small_lbd", 3);
m_gc_k = p.get_uint("gc_k", 7);
m_gc_initial = p.gc_initial();
m_gc_increment = p.gc_increment();
m_gc_small_lbd = p.gc_small_lbd();
m_gc_k = p.gc_k();
if (m_gc_k > 255)
m_gc_k = 255;
}
@ -96,31 +100,15 @@ namespace sat {
m_gc_strategy = GC_PSM_GLUE;
else
throw sat_param_exception("invalid gc strategy");
m_gc_initial = p.get_uint("gc_initial", 20000);
m_gc_increment = p.get_uint("gc_increment", 500);
m_gc_initial = p.gc_initial();
m_gc_increment = p.gc_increment();
}
m_minimize_lemmas = p.get_bool("minimize_lemmas", true);
m_dyn_sub_res = p.get_bool("dyn_sub_res", true);
m_minimize_lemmas = p.minimize_lemmas();
m_dyn_sub_res = p.dyn_sub_res();
}
void config::collect_param_descrs(param_descrs & r) {
insert_max_memory(r);
r.insert("phase", CPK_SYMBOL, "(default: caching) phase selection strategy: always_false, always_true, caching, random.");
r.insert("phase_caching_on", CPK_UINT, "(default: 400)");
r.insert("phase_caching_off", CPK_UINT, "(default: 100)");
r.insert("restart", CPK_SYMBOL, "(default: luby) restart strategy: luby or geometric.");
r.insert("restart_initial", CPK_UINT, "(default: 100) initial restart (number of conflicts).");
r.insert("restart_factor", CPK_DOUBLE, "(default: 1.5) restart increment factor for geometric strategy.");
r.insert("random_freq", CPK_DOUBLE, "(default: 0.01) frequency of random case splits.");
r.insert("burst_search", CPK_UINT, "(default: 100) number of conflicts before first global simplification.");
r.insert("max_conflicts", CPK_UINT, "(default: inf) maximum number of conflicts.");
r.insert("gc_strategy", CPK_SYMBOL, "(default: glue_psm) garbage collection strategy: psm, glue, glue_psm, dyn_psm.");
r.insert("gc_initial", CPK_UINT, "(default: 20000) learned clauses garbage collection frequence.");
r.insert("gc_increment", CPK_UINT, "(default: 500) increment to the garbage collection threshold.");
r.insert("gc_small_lbd", CPK_UINT, "(default: 3) learned clauses with small LBD are never deleted (only used in dyn_psm).");
r.insert("gc_k", CPK_UINT, "(default: 7) learned clauses that are inactive for k gc rounds are permanently deleted (only used in dyn_psm).");
r.insert("minimize_lemmas", CPK_BOOL, "(default: true) minimize learned clauses.");
r.insert("dyn_sub_res", CPK_BOOL, "(default: true) dynamic subsumption resolution for minimizing learned clauses.");
sat_params::collect_param_descrs(r);
}
};

20
src/sat/sat_params.pyg Normal file
View file

@ -0,0 +1,20 @@
def_module_params('sat',
export=True,
description='propositional SAT solver',
params=(max_memory_param(),
('phase', SYMBOL, 'caching', 'phase selection strategy: always_false, always_true, caching, random'),
('phase.caching.on', UINT, 400, 'phase caching on period (in number of conflicts)'),
('phase.caching.off', UINT, 100, 'phase caching off period (in number of conflicts)'),
('restart', SYMBOL, 'luby', 'restart strategy: luby or geometric'),
('restart.initial', UINT, 100, 'initial restart (number of conflicts)'),
('restart.factor', DOUBLE, 1.5, 'restart increment factor for geometric strategy'),
('random_freq', DOUBLE, 0.01, 'frequency of random case splits'),
('burst_search', UINT, 100, 'number of conflicts before first global simplification'),
('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts'),
('gc', SYMBOL, 'glue_psm', 'garbage collection strategy: psm, glue, glue_psm, dyn_psm'),
('gc.initial', UINT, 20000, 'learned clauses garbage collection frequence'),
('gc.increment', UINT, 500, 'increment to the garbage collection threshold'),
('gc.small_lbd', UINT, 3, 'learned clauses with small LBD are never deleted (only used in dyn_psm)'),
('gc.k', UINT, 7, 'learned clauses that are inactive for k gc rounds are permanently deleted (only used in dyn_psm)'),
('minimize_lemmas', BOOL, True, 'minimize learned clauses'),
('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses')))

8
src/sat/sat_scc.cpp
View file

@ -21,6 +21,7 @@ Revision History:
#include"sat_elim_eqs.h"
#include"stopwatch.h"
#include"trace.h"
#include"sat_scc_params.hpp"
namespace sat {
@ -230,12 +231,13 @@ namespace sat {
m_num_elim = 0;
}
void scc::updt_params(params_ref const & p) {
m_scc = p.get_bool("scc", true);
void scc::updt_params(params_ref const & _p) {
sat_scc_params p(_p);
m_scc = p.scc();
}
void scc::collect_param_descrs(param_descrs & d) {
d.insert("scc", CPK_BOOL, "(default: true) eliminate Boolean variables by computing strongly connected components.");
sat_scc_params::collect_param_descrs(d);
}
};

5
src/sat/sat_scc_params.pyg Normal file
View file

@ -0,0 +1,5 @@
def_module_params(module_name='sat',
class_name='sat_scc_params',
export=True,
params=(('scc', BOOL, True, 'eliminate Boolean variables by computing strongly connected components'),))

56
src/sat/sat_simplifier.cpp
View file

@ -19,6 +19,7 @@ Revision History:
--*/
#include"sat_simplifier.h"
#include"sat_simplifier_params.hpp"
#include"sat_solver.h"
#include"stopwatch.h"
#include"trace.h"
@ -1430,45 +1431,28 @@ namespace sat {
m_new_cls.finalize();
}
void simplifier::updt_params(params_ref const & p) {
m_elim_blocked_clauses = p.get_bool("elim_blocked_clauses", false);
m_elim_blocked_clauses_at = p.get_uint("elim_blocked_clauses_at", 2);
m_blocked_clause_limit = p.get_uint("blocked_clause_limit", 100000000);
m_resolution = p.get_bool("resolution", true);
m_res_limit = p.get_uint("resolution_limit", 500000000);
m_res_occ_cutoff = p.get_uint("res_occ_cutoff", 10);
m_res_occ_cutoff1 = p.get_uint("res_occ_cutoff_range1", 8);
m_res_occ_cutoff2 = p.get_uint("res_occ_cutoff_range2", 5);
m_res_occ_cutoff3 = p.get_uint("res_occ_cutoff_range3", 3);
m_res_lit_cutoff1 = p.get_uint("res_lit_cutoff_range1", 700);
m_res_lit_cutoff2 = p.get_uint("res_lit_cutoff_range2", 400);
m_res_lit_cutoff3 = p.get_uint("res_lit_cutoff_range3", 300);
m_res_cls_cutoff1 = p.get_uint("res_cls_cutoff1", 100000);
m_res_cls_cutoff2 = p.get_uint("res_cls_cutoff2", 700000);
m_subsumption = p.get_bool("subsumption", true);
m_subsumption_limit = p.get_uint("subsumption_limit", 100000000);
void simplifier::updt_params(params_ref const & _p) {
sat_simplifier_params p(_p);
m_elim_blocked_clauses = p.elim_blocked_clauses();
m_elim_blocked_clauses_at = p.elim_blocked_clauses_at();
m_blocked_clause_limit = p.blocked_clause_limit();
m_resolution = p.resolution();
m_res_limit = p.resolution_limit();
m_res_occ_cutoff = p.resolution_occ_cutoff();
m_res_occ_cutoff1 = p.resolution_occ_cutoff_range1();
m_res_occ_cutoff2 = p.resolution_occ_cutoff_range2();
m_res_occ_cutoff3 = p.resolution_occ_cutoff_range3();
m_res_lit_cutoff1 = p.resolution_lit_cutoff_range1();
m_res_lit_cutoff2 = p.resolution_lit_cutoff_range2();
m_res_lit_cutoff3 = p.resolution_lit_cutoff_range3();
m_res_cls_cutoff1 = p.resolution_cls_cutoff1();
m_res_cls_cutoff2 = p.resolution_cls_cutoff2();
m_subsumption = p.subsumption();
m_subsumption_limit = p.subsumption_limit();
}
void simplifier::collect_param_descrs(param_descrs & r) {
r.insert("elim_blocked_clauses", CPK_BOOL, "(default: false) eliminate blocked clauses.");
r.insert("elim_blocked_clauses_at", CPK_UINT, "(default: 2) eliminate blocked clauses only once at the given simplification round.");
r.insert("blocked_clause_limit", CPK_UINT, "(default: 100000000) maximum number of literals visited during blocked clause elimination.");
r.insert("resolution", CPK_BOOL, "(default: true) eliminate boolean variables using resolution.");
r.insert("resolution_limit", CPK_UINT, "(default: 500000000) approx. maximum number of literals visited during variable elimination.");
r.insert("res_occ_cutoff", CPK_UINT, "(default: 10) first cutoff (on number of positive/negative occurrences) for Boolean variable elimination.");
r.insert("res_occ_cutoff_range1", CPK_UINT, "(default: 8) second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing less than res_cls_cutoff1 clauses.");
r.insert("res_occ_cutoff_range2", CPK_UINT, "(default: 5) second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing more than res_cls_cutoff1 and less than res_cls_cutoff2.");
r.insert("res_occ_cutoff_range3", CPK_UINT, "(default: 3) second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing more than res_cls_cutoff2.");
r.insert("res_lit_cutoff_range1", CPK_UINT, "(default: 700) second cutoff (total number of literals) for Boolean variable elimination, for problems containing less than res_cls_cutoff1 clauses.");
r.insert("res_lit_cutoff_range2", CPK_UINT, "(default: 400) second cutoff (total number of literals) for Boolean variable elimination, for problems containing more than res_cls_cutoff1 and less than res_cls_cutoff2.");
r.insert("res_lit_cutoff_range3", CPK_UINT, "(default: 300) second cutoff (total number of literals) for Boolean variable elimination, for problems containing more than res_cls_cutoff2.");
r.insert("res_cls_cutoff1", CPK_UINT, "(default: 100000000) limit1 - total number of problems clauses for the second cutoff of Boolean variable elimination.");
r.insert("res_cls_cutoff2", CPK_UINT, "(default: 700000000) limit2 - total number of problems clauses for the second cutoff of Boolean variable elimination.");
r.insert("subsumption", CPK_BOOL, "(default: true) eliminate subsumed clauses.");
r.insert("subsumption_limit", CPK_UINT, "(default: 100000000) approx. maximum number of literals visited during subsumption (and subsumption resolution).");
sat_simplifier_params::collect_param_descrs(r);
}
void simplifier::collect_statistics(statistics & st) {

19
src/sat/sat_simplifier_params.pyg Normal file
View file

@ -0,0 +1,19 @@
def_module_params(module_name='sat',
class_name='sat_simplifier_params',
export=True,
params=(('elim_blocked_clauses', BOOL, False, 'eliminate blocked clauses'),
('elim_blocked_clauses_at', UINT, 2, 'eliminate blocked clauses only once at the given simplification round'),
('blocked_clause_limit', UINT, 100000000, 'maximum number of literals visited during blocked clause elimination'),
('resolution', BOOL, True, 'eliminate boolean variables using resolution'),
('resolution.limit', UINT, 500000000, 'approx. maximum number of literals visited during variable elimination'),
('resolution.occ_cutoff', UINT, 10, 'first cutoff (on number of positive/negative occurrences) for Boolean variable elimination'),
('resolution.occ_cutoff_range1', UINT, 8, 'second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing less than res_cls_cutoff1 clauses'),
('resolution.occ_cutoff_range2', UINT, 5, 'second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing more than res_cls_cutoff1 and less than res_cls_cutoff2'),
('resolution.occ_cutoff_range3', UINT, 3, 'second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing more than res_cls_cutoff2'),
('resolution.lit_cutoff_range1', UINT, 700, 'second cutoff (total number of literals) for Boolean variable elimination, for problems containing less than res_cls_cutoff1 clauses'),
('resolution.lit_cutoff_range2', UINT, 400, 'second cutoff (total number of literals) for Boolean variable elimination, for problems containing more than res_cls_cutoff1 and less than res_cls_cutoff2'),
('resolution.lit_cutoff_range3', UINT, 300, 'second cutoff (total number of literals) for Boolean variable elimination, for problems containing more than res_cls_cutoff2'),
('resolution.cls_cutoff1', UINT, 100000000, 'limit1 - total number of problems clauses for the second cutoff of Boolean variable elimination'),
('resolution.cls_cutoff2', UINT, 700000000, 'limit2 - total number of problems clauses for the second cutoff of Boolean variable elimination'),
('subsumption', BOOL, True, 'eliminate subsumed clauses'),
('subsumption.limit', UINT, 100000000, 'approx. maximum number of literals visited during subsumption (and subsumption resolution)')))

41
src/shell/main.cpp
View file

@ -77,7 +77,10 @@ void display_usage() {
std::cout << " " << OPT << "version prints version number of Z3.\n";
std::cout << " " << OPT << "v:level be verbose, where <level> is the verbosity level.\n";
std::cout << " " << OPT << "nw disable warning messages.\n";
std::cout << " " << OPT << "ps display Z3 global (and module) parameters.\n";
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, 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.
@ -166,7 +169,7 @@ void parse_cmd_line_args(int argc, char ** argv) {
}
else if (strcmp(opt_name, "v") == 0) {
if (!opt_arg)
error("option argument (/v:level) is missing.");
error("option argument (-v:level) is missing.");
long lvl = strtol(opt_arg, 0, 10);
set_verbosity_level(lvl);
}
@ -175,39 +178,59 @@ void parse_cmd_line_args(int argc, char ** argv) {
}
else if (strcmp(opt_name, "T") == 0) {
if (!opt_arg)
error("option argument (/T:timeout) is missing.");
error("option argument (-T:timeout) is missing.");
long tm = strtol(opt_arg, 0, 10);
set_timeout(tm * 1000);
}
else if (strcmp(opt_name, "t") == 0) {
if (!opt_arg)
error("option argument (/t:timeout) is missing.");
error("option argument (-t:timeout) is missing.");
gparams::set("timeout", opt_arg);
}
else if (strcmp(opt_name, "nw") == 0) {
enable_warning_messages(false);
}
else if (strcmp(opt_name, "ps") == 0) {
gparams::display(std::cout);
else if (strcmp(opt_name, "p") == 0) {
gparams::display(std::cout, 0, false, false);
exit(0);
}
else if (strcmp(opt_name, "pd") == 0) {
gparams::display(std::cout, 0, false, true);
exit(0);
}
else if (strcmp(opt_name, "pm") == 0) {
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) {
if (!opt_arg)
error("option argument (-pp:name) is missing.");
gparams::display_parameter(std::cout, opt_arg);
exit(0);
}
#ifdef _TRACE
else if (strcmp(opt_name, "tr") == 0) {
if (!opt_arg)
error("option argument (/tr:tag) is missing.");
error("option argument (-tr:tag) is missing.");
enable_trace(opt_arg);
}
#endif
#ifdef Z3DEBUG
else if (strcmp(opt_name, "dbg") == 0) {
if (!opt_arg)
error("option argument (/dbg:tag) is missing.");
error("option argument (-dbg:tag) is missing.");
enable_debug(opt_arg);
}
#endif
else if (strcmp(opt_name, "memory") == 0) {
if (!opt_arg)
error("option argument (/memory:val) is missing.");
error("option argument (-memory:val) is missing.");
gparams::set("memory_max_size", opt_arg);
}
else {

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

@ -1403,7 +1403,7 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const *
SASSERT(num == 1);
expr * sgn, * s, * e;
split(args[0], sgn, s, e);
result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, s), e);
result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s);
}
void fpa2bv_converter::split(expr * e, expr * & sgn, expr * & sig, expr * & exp) const {

227
src/util/gparams.cpp
View file

@ -36,13 +36,27 @@ bool is_old_param_name(symbol const & name) {
}
struct gparams::imp {
bool m_modules_registered;
dictionary<param_descrs*> m_module_param_descrs;
dictionary<char const *> m_module_descrs;
param_descrs m_param_descrs;
dictionary<params_ref *> m_module_params;
params_ref m_params;
void check_registered() {
if (m_modules_registered)
return;
m_modules_registered = true;
gparams_register_modules();
}
dictionary<param_descrs*> & get_module_param_descrs() { check_registered(); return m_module_param_descrs; }
dictionary<char const *> & 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,54 +76,44 @@ 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);
}
void display(std::ostream & out, unsigned indent, bool smt2_style) {
#pragma omp critical (gparams)
{
out << "Global parameters\n";
m_param_descrs.display(out, indent + 4, smt2_style);
out << "\n";
dictionary<param_descrs*>::iterator it = m_module_param_descrs.begin();
dictionary<param_descrs*>::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;
}
out << "\n";
it->m_value->display(out, indent + 4, smt2_style);
}
}
}
// -----------------------------------------------
//
// Parameter setting & retrieval
//
// -----------------------------------------------
void normalize(char const * name, /* out */ symbol & mod_name, /* out */ symbol & param_name) {
if (*name == ':')
@ -152,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 {
@ -211,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 {
@ -223,7 +227,7 @@ public:
}
}
}
catch (exception & ex) {
catch (z3_exception & ex) {
// Exception cannot cross critical section boundaries.
error = true;
error_msg = ex.msg();
@ -263,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 {
@ -273,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 {
@ -282,7 +286,7 @@ public:
}
}
}
catch (exception & ex) {
catch (z3_exception & ex) {
// Exception cannot cross critical section boundaries.
error = true;
error_msg = ex.msg();
@ -315,6 +319,117 @@ 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";
get_param_descrs().display(out, indent + 4, smt2_style, include_descr);
out << "\n";
if (!smt2_style) {
out << "To set a module parameter, use <module-name>.<parameter-name>=value\n";
out << "Example: pp.decimal=true\n";
out << "\n";
}
dictionary<param_descrs*>::iterator it = get_module_param_descrs().begin();
dictionary<param_descrs*>::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";
it->m_value->display(out, indent + 4, smt2_style, include_descr);
}
}
}
void display_modules(std::ostream & out) {
#pragma omp critical (gparams)
{
dictionary<param_descrs*>::iterator it = get_module_param_descrs().begin();
dictionary<param_descrs*>::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";
}
}
}
void display_module(std::ostream & out, symbol const & module_name) {
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();
}
}
if (error)
throw exception(error_msg);
}
void display_parameter(std::ostream & out, char const * name) {
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();
}
}
if (error)
throw exception(error_msg);
}
};
gparams::imp * gparams::g_imp = 0;
@ -370,15 +485,29 @@ params_ref gparams::get() {
return g_imp->get();
}
void gparams::display(std::ostream & out, unsigned indent, bool smt2_style) {
void gparams::display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) {
SASSERT(g_imp != 0);
g_imp->display(out, indent, smt2_style);
g_imp->display(out, indent, smt2_style, include_descr);
}
void gparams::display_modules(std::ostream & out) {
SASSERT(g_imp != 0);
g_imp->display_modules(out);
}
void gparams::display_module(std::ostream & out, char const * module_name) {
SASSERT(g_imp != 0);
g_imp->display_module(out, symbol(module_name));
}
void gparams::display_parameter(std::ostream & out, char const * name) {
SASSERT(g_imp != 0);
g_imp->display_parameter(out, name);
}
void gparams::init() {
TRACE("gparams", tout << "gparams::init()\n";);
g_imp = alloc(imp);
gparams_register_modules();
}
void gparams::finalize() {

7
src/util/gparams.h
View file

@ -106,8 +106,13 @@ public:
/**
\brief Dump information about available parameters in the given output stream.
*/
static void display(std::ostream & out, unsigned indent = 0, bool smt2_style=false);
static void display(std::ostream & out, unsigned indent = 0, bool smt2_style=false, bool include_descr=true);
// Auxiliary APIs for better command line support
static void display_modules(std::ostream & out);
static void display_module(std::ostream & out, char const * module_name);
static void display_parameter(std::ostream & out, char const * name);
/**
\brief Initialize the global parameter management module.

10
src/util/params.cpp
View file

@ -95,7 +95,7 @@ struct param_descrs::imp {
bool operator()(symbol const & s1, symbol const & s2) const { return strcmp(s1.bare_str(), s2.bare_str()) < 0; }
};
void display(std::ostream & out, unsigned indent, bool smt2_style) const {
void display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) const {
svector<symbol> names;
dictionary<info>::iterator it = m_info.begin();
dictionary<info>::iterator end = m_info.end();
@ -124,7 +124,9 @@ struct param_descrs::imp {
info d;
m_info.find(*it2, d);
SASSERT(d.m_descr);
out << " (" << d.m_kind << ") " << d.m_descr;
out << " (" << d.m_kind << ")";
if (include_descr)
out << " " << d.m_descr;
if (d.m_default != 0)
out << " (default: " << d.m_default << ")";
out << "\n";
@ -209,8 +211,8 @@ symbol param_descrs::get_param_name(unsigned i) const {
return m_imp->get_param_name(i);
}
void param_descrs::display(std::ostream & out, unsigned indent, bool smt2_style) const {
return m_imp->display(out, indent, smt2_style);
void param_descrs::display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) const {
return m_imp->display(out, indent, smt2_style, include_descr);
}
void insert_max_memory(param_descrs & r) {

2
src/util/params.h
View file

@ -119,7 +119,7 @@ public:
char const * get_descr(symbol const & name) const;
char const * get_default(char const * name) const;
char const * get_default(symbol const & name) const;
void display(std::ostream & out, unsigned indent = 0, bool smt2_style=false) const;
void display(std::ostream & out, unsigned indent = 0, bool smt2_style=false, bool include_descr=true) const;
unsigned size() const;
symbol get_param_name(unsigned idx) const;
};