diff --git a/.gitignore b/.gitignore index a26ee7565..3fe56e9f3 100644 --- a/.gitignore +++ b/.gitignore @@ -42,6 +42,7 @@ config.status configure install_tactic.cpp mem_initializer.cpp +gparams_register_modules.cpp scripts/config-debug.mk scripts/config-release.mk src/api/api_commands.cpp diff --git a/RELEASE_NOTES b/RELEASE_NOTES index 617b44bd0..4c74b41a5 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -16,7 +16,7 @@ Version 4.3.2 - Fixed incorrect result returned by Z3_solver_get_num_scopes. (Thanks to Herman Venter). This bug was introduced in Z3 4.3.0 -- Java bindings. To enable them, we must use the option `--java` when executing the `mk_make.py` script. Example: `python scripts/mk_make.py --java +- Java bindings. To enable them, we must use the option `--java` when executing the `mk_make.py` script. Example: `python scripts/mk_make.py --java` - Fixed crash when parsing incorrect formulas. The crash was introduced when support for "arithmetic coercions" was added in Z3 4.3.0. diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 4bbaa80a8..0c40d9a56 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1418,6 +1418,7 @@ def mk_auto_src(): mk_pat_db() mk_all_install_tactic_cpps() mk_all_mem_initializer_cpps() + mk_all_gparams_register_modules() # TODO: delete after src/ast/pattern/expr_pattern_match # database.smt ==> database.h @@ -1594,7 +1595,7 @@ def mk_all_install_tactic_cpps(): # This file implements the procedures # void mem_initialize() # void mem_finalize() -# This procedures are invoked by the Z3 memory_manager +# These procedures are invoked by the Z3 memory_manager def mk_mem_initializer_cpp(cnames, path): initializer_cmds = [] finalizer_cmds = [] @@ -1653,6 +1654,56 @@ def mk_all_mem_initializer_cpps(): cnames.append(c.name) mk_mem_initializer_cpp(cnames, c.src_dir) +# Generate an mem_initializer.cpp at path. +# This file implements the procedure +# void gparams_register_modules() +# This procedure is invoked by gparams::init() +def mk_gparams_register_modules(cnames, path): + cmds = [] + mod_cmds = [] + fullname = '%s/gparams_register_modules.cpp' % path + fout = open(fullname, 'w') + fout.write('// Automatically generated file.\n') + fout.write('#include"gparams.h"\n') + reg_pat = re.compile('[ \t]*REG_PARAMS\(\'([^\']*)\'\)') + reg_mod_pat = re.compile('[ \t]*REG_MODULE_PARAMS\(\'([^\']*)\', *\'([^\']*)\'\)') + for cname in cnames: + c = get_component(cname) + h_files = filter(lambda f: f.endswith('.h'), os.listdir(c.src_dir)) + for h_file in h_files: + added_include = False + fin = open("%s/%s" % (c.src_dir, h_file), 'r') + for line in fin: + m = reg_pat.match(line) + if m: + if not added_include: + added_include = True + fout.write('#include"%s"\n' % h_file) + cmds.append((m.group(1))) + m = reg_mod_pat.match(line) + if m: + if not added_include: + added_include = True + fout.write('#include"%s"\n' % h_file) + mod_cmds.append((m.group(1), m.group(2))) + fout.write('void gparams_register_modules() {\n') + for code in cmds: + fout.write('{ param_descrs d; %s(*d); gparams::register_global(d); }\n' % code) + for (mod, code) in mod_cmds: + fout.write('{ param_descrs * d = alloc(param_descrs); %s(*d); gparams::register_module("%s", d); }\n' % (code, mod)) + fout.write('}\n') + if VERBOSE: + print "Generated '%s'" % fullname + +def mk_all_gparams_register_modules(): + if not ONLY_MAKEFILES: + for c in get_components(): + if c.require_mem_initializer(): + cnames = [] + cnames.extend(c.deps) + cnames.append(c.name) + mk_gparams_register_modules(cnames, c.src_dir) + # Generate a .def based on the files at c.export_files slot. def mk_def_file(c): pat1 = re.compile(".*Z3_API.*") diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index aeddf63c3..1503b387f 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -674,8 +674,8 @@ extern "C" { ast_manager & m = mk_c(c)->m(); expr * a = to_expr(_a); params_ref p = to_param_ref(_p); - unsigned timeout = p.get_uint(":timeout", UINT_MAX); - bool use_ctrl_c = p.get_bool(":ctrl-c", false); + unsigned timeout = p.get_uint("timeout", UINT_MAX); + bool use_ctrl_c = p.get_bool("ctrl_c", false); th_rewriter m_rw(m, p); expr_ref result(m); cancel_eh eh(m_rw); diff --git a/src/api/api_config_params.cpp b/src/api/api_config_params.cpp index 07e043726..550212cf9 100644 --- a/src/api/api_config_params.cpp +++ b/src/api/api_config_params.cpp @@ -21,6 +21,7 @@ Revision History: #include"pp.h" #include"api_log_macros.h" #include"api_util.h" +#include"cmd_context.h" #include"symbol.h" namespace api { @@ -41,8 +42,6 @@ namespace api { }; -extern std::string smt_keyword2opt_name(symbol const & opt); - extern "C" { Z3_config Z3_API Z3_mk_config() { LOG_Z3_mk_config(); @@ -62,7 +61,7 @@ extern "C" { api::config_params* p = reinterpret_cast(c); if (param_id != 0 && param_id[0] == ':') { // Allow SMT2 style paramater names such as :model, :relevancy, etc - std::string new_param_id = smt_keyword2opt_name(symbol(param_id)); + std::string new_param_id = smt2_keyword_to_param(symbol(param_id)); p->m_ini.set_param_value(new_param_id.c_str(), param_value); } else { @@ -91,7 +90,7 @@ extern "C" { } if (param_id != 0 && param_id[0] == ':') { // Allow SMT2 style paramater names such as :model, :relevancy, etc - std::string new_param_id = smt_keyword2opt_name(symbol(param_id)); + std::string new_param_id = smt2_keyword_to_param(symbol(param_id)); ini.set_param_value(new_param_id.c_str(), param_value); } else { diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index 0200a4405..3c434600b 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -265,7 +265,7 @@ extern "C" { RESET_ERROR_CODE(); lbool r = l_undef; cancel_eh eh(*to_fixedpoint_ref(d)); - unsigned timeout = to_fixedpoint(d)->m_params.get_uint(":timeout", UINT_MAX); + unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", UINT_MAX); api::context::set_interruptable(*(mk_c(c)), eh); { scoped_timer timer(timeout, &eh); @@ -289,7 +289,7 @@ extern "C" { LOG_Z3_fixedpoint_query_relations(c, d, num_relations, relations); RESET_ERROR_CODE(); lbool r = l_undef; - unsigned timeout = to_fixedpoint(d)->m_params.get_uint(":timeout", UINT_MAX); + unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", UINT_MAX); cancel_eh eh(*to_fixedpoint_ref(d)); api::context::set_interruptable(*(mk_c(c)), eh); { diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 790ca8f59..a85e8d83a 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -37,8 +37,8 @@ extern "C" { ast_manager & m = mk_c(c)->m(); Z3_solver_ref * s = to_solver(_s); s->m_solver->set_produce_proofs(m.proofs_enabled()); - s->m_solver->set_produce_unsat_cores(s->m_params.get_bool(":unsat-core", false)); - s->m_solver->set_produce_models(s->m_params.get_bool(":model", true)); + s->m_solver->set_produce_unsat_cores(s->m_params.get_bool("unsat_core", false)); + s->m_solver->set_produce_models(s->m_params.get_bool("model", true)); s->m_solver->set_front_end_params(mk_c(c)->fparams()); s->m_solver->updt_params(s->m_params); s->m_solver->init(m, s->m_logic); @@ -127,8 +127,8 @@ extern "C" { LOG_Z3_solver_set_params(c, s, p); RESET_ERROR_CODE(); if (to_solver(s)->m_initialized) { - bool old_model = to_solver(s)->m_params.get_bool(":model", true); - bool new_model = to_param_ref(p).get_bool(":model", true); + bool old_model = to_solver(s)->m_params.get_bool("model", true); + bool new_model = to_param_ref(p).get_bool("model", true); if (old_model != new_model) to_solver_ref(s)->set_produce_models(new_model); to_solver_ref(s)->updt_params(to_param_ref(p)); @@ -238,8 +238,8 @@ extern "C" { } } expr * const * _assumptions = to_exprs(assumptions); - unsigned timeout = to_solver(s)->m_params.get_uint(":timeout", UINT_MAX); - bool use_ctrl_c = to_solver(s)->m_params.get_bool(":ctrl-c", false); + unsigned timeout = to_solver(s)->m_params.get_uint("timeout", UINT_MAX); + bool use_ctrl_c = to_solver(s)->m_params.get_bool("ctrl_c", false); cancel_eh eh(*to_solver_ref(s)); api::context::set_interruptable(*(mk_c(c)), eh); lbool result; diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp index ff55923a4..5bce218e6 100644 --- a/src/api/api_tactic.cpp +++ b/src/api/api_tactic.cpp @@ -404,8 +404,8 @@ extern "C" { Z3_apply_result_ref * ref = alloc(Z3_apply_result_ref, mk_c(c)->m()); mk_c(c)->save_object(ref); - unsigned timeout = p.get_uint(":timeout", UINT_MAX); - bool use_ctrl_c = p.get_bool(":ctrl-c", false); + unsigned timeout = p.get_uint("timeout", UINT_MAX); + bool use_ctrl_c = p.get_bool("ctrl_c", false); cancel_eh eh(*to_tactic_ref(t)); to_tactic_ref(t)->updt_params(p); diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp index 4d8849178..d525fa167 100644 --- a/src/ast/normal_forms/nnf.cpp +++ b/src/ast/normal_forms/nnf.cpp @@ -122,11 +122,11 @@ public: } void updt_params(params_ref const & p) { - m_sk_hack_enabled = p.get_bool(":nnf-sk-hack", false); + m_sk_hack_enabled = p.get_bool("sk_hack", false); } static void get_param_descrs(param_descrs & r) { - r.insert(":nnf-sk-hack", CPK_BOOL, "(default: false) hack for VCC"); + r.insert("sk_hack", CPK_BOOL, "(default: false) hack for VCC"); } ast_manager & m() const { return m_manager; } @@ -264,7 +264,7 @@ struct nnf::imp { } void updt_local_params(params_ref const & p) { - symbol mode_sym = p.get_sym(":nnf-mode", m_skolem); + symbol mode_sym = p.get_sym("mode", m_skolem); if (mode_sym == m_skolem) m_mode = NNF_SKOLEM; else if (mode_sym == "full") @@ -276,18 +276,18 @@ struct nnf::imp { TRACE("nnf", tout << "nnf-mode: " << m_mode << " " << mode_sym << "\n" << p << "\n";); - m_ignore_labels = p.get_bool(":nnf-ignore-labels", false); - m_skolemize = p.get_bool(":skolemize", true); - m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX)); + m_ignore_labels = p.get_bool("ignore_labels", false); + m_skolemize = p.get_bool("skolemize", true); + m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); } static void get_param_descrs(param_descrs & r) { insert_max_memory(r); - r.insert(":nnf-mode", CPK_SYMBOL, + r.insert("mode", CPK_SYMBOL, "(default: skolem) NNF translation mode: skolem (skolem normal form), quantifiers (skolem normal form + quantifiers in NNF), full"); - r.insert(":nnf-ignore-labels", CPK_BOOL, + r.insert("ignore_labels", CPK_BOOL, "(default: false) remove/ignore labels in the input formula, this option is ignored if proofs are enabled"); - r.insert(":skolemize", CPK_BOOL, + r.insert("skolemize", CPK_BOOL, "(default: true) skolemize (existential force) quantifiers"); skolemizer::get_param_descrs(r); } @@ -884,15 +884,15 @@ nnf::nnf(ast_manager & m, defined_names & n, params_ref const & p) { nnf::nnf(ast_manager & m, defined_names & n, nnf_params & np) { params_ref p; if (np.m_nnf_mode == NNF_FULL) - p.set_sym(":nnf-mode", symbol("full")); + p.set_sym("mode", symbol("full")); else if (np.m_nnf_mode == NNF_QUANT) - p.set_sym(":nnf-mode", symbol("quantifiers")); + p.set_sym("mode", symbol("quantifiers")); if (np.m_nnf_ignore_labels) - p.set_bool(":nnf-ignore-labels", true); + p.set_bool("ignore_labels", true); if (np.m_nnf_sk_hack) - p.set_bool(":nnf-sk-hack", true); + p.set_bool("sk_hack", true); m_imp = alloc(imp, m, n, p); } diff --git a/src/ast/normal_forms/nnf.h b/src/ast/normal_forms/nnf.h index 685083ff7..96807afc0 100644 --- a/src/ast/normal_forms/nnf.h +++ b/src/ast/normal_forms/nnf.h @@ -41,6 +41,9 @@ public: ); void updt_params(params_ref const & p); + /* + REG_MODULE_PARAMS('nnf', 'nnf::get_param_descrs') + */ static void get_param_descrs(param_descrs & r); void cancel() { set_cancel(true); } diff --git a/src/ast/pp.cpp b/src/ast/pp.cpp index 43f19e166..d05776e78 100644 --- a/src/ast/pp.cpp +++ b/src/ast/pp.cpp @@ -19,6 +19,24 @@ Revision History: #include"pp.h" 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) { diff --git a/src/ast/pp.h b/src/ast/pp.h index 43c1de7b7..13afcb07c 100644 --- a/src/ast/pp.h +++ b/src/ast/pp.h @@ -21,6 +21,12 @@ Revision History: #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); diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 3efc14abe..f5fdcf8af 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -22,18 +22,18 @@ Notes: #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 + 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_params(params_ref const & p) { @@ -43,18 +43,18 @@ 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)))."); + 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)))."); } 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/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index 268f4dca0..ac93e0f87 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -21,13 +21,13 @@ Notes: #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); + m_sort_store = p.get_bool("sort_store", false); + m_expand_select_store = p.get_bool("expand_select_store", false); } 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."); + 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."); } 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/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp index c64ea56d0..1fd83e91f 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp +++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp @@ -125,12 +125,12 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg { } void updt_params(params_ref const & p) { - m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX)); - m_max_steps = p.get_uint(":max-steps", UINT_MAX); - m_blast_add = p.get_bool(":blast-add", true); - m_blast_mul = p.get_bool(":blast-mul", true); - m_blast_full = p.get_bool(":blast-full", false); - m_blast_quant = p.get_bool(":blast-quant", false); + m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); + m_max_steps = p.get_uint("max_steps", UINT_MAX); + m_blast_add = p.get_bool("blast_add", true); + m_blast_mul = p.get_bool("blast_mul", true); + m_blast_full = p.get_bool("blast_full", false); + m_blast_quant = p.get_bool("blast_quant", false); m_blaster.set_max_memory(m_max_memory); } diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index b7fe296c4..b3f422fe5 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -20,21 +20,22 @@ Notes: #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); + 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::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."); + 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."); } 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/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index adef6a5b0..fbc1f7c11 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -54,14 +54,14 @@ app * mk_extract_proc::operator()(unsigned high, unsigned low, expr * arg) { } 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); + 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_params(params_ref const & p) { @@ -71,15 +71,15 @@ 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."); + 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."); #ifndef _EXTERNAL_RELEASE - r.insert(":mkbv2num", CPK_BOOL, "(default: false) convert (mkbv [true/false]*) into a numeral"); + r.insert("mkbv2num", CPK_BOOL, "(default: false) convert (mkbv [true/false]*) into a numeral"); #endif } diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h index e942b453a..e6c8a653c 100644 --- a/src/ast/rewriter/poly_rewriter_def.h +++ b/src/ast/rewriter/poly_rewriter_def.h @@ -27,19 +27,19 @@ 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); + 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); } 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"); + 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"); } template diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index ee55d53e7..da4dd3860 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -57,13 +57,13 @@ 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); + 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_params(params_ref const & p) { @@ -695,10 +695,10 @@ void th_rewriter::get_param_descrs(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."); + 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."); } th_rewriter::~th_rewriter() { diff --git a/src/ast/rewriter/th_rewriter.h b/src/ast/rewriter/th_rewriter.h index 1b77c42c7..19a89d286 100644 --- a/src/ast/rewriter/th_rewriter.h +++ b/src/ast/rewriter/th_rewriter.h @@ -37,7 +37,9 @@ 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/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 4c24b5ae6..1960cd22a 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -28,6 +28,7 @@ Notes: #include"simplify_cmd.h" #include"eval_cmd.h" #include"front_end_params.h" +#include"gparams.h" class help_cmd : public cmd { svector m_cmds; @@ -219,25 +220,6 @@ UNARY_CMD(pp_cmd, "display", "", "display the given term.", CPK_EXPR, expr UNARY_CMD(echo_cmd, "echo", "", "display the given string", CPK_STRING, char const *, ctx.regular_stream() << arg << std::endl;); -/** - \brief Convert a keyword into an internal Z3 option name -*/ -std::string smt_keyword2opt_name(symbol const & opt) { - std::string r; - SASSERT(opt.bare_str()[0] == ':'); - r = opt.bare_str() + 1; - unsigned sz = static_cast(r.size()); - for (unsigned i = 0; i < sz; i++) { - char curr = r[i]; - if ('a' <= curr && curr <= 'z') - r[i] = 'A' + (curr - 'a'); - else if (curr == '-') - r[i] = '_'; - } - TRACE("smt2_opt_name", tout << opt << " -> '" << r << "'\n";); - return r; -} - class set_get_option_cmd : public cmd { protected: symbol m_true; @@ -259,7 +241,6 @@ protected: symbol m_numeral_as_real; symbol m_error_behavior; symbol m_int_real_coercions; - ini_params m_ini; bool is_builtin_option(symbol const & s) const { return @@ -289,10 +270,7 @@ public: m_global_decls(":global-decls"), m_numeral_as_real(":numeral-as-real"), m_error_behavior(":error-behavior"), - m_int_real_coercions(":int-real-coercions"), - m_ini(false) { - params.register_params(m_ini); - register_pp_params(m_ini); + m_int_real_coercions(":int-real-coercions") { } virtual ~set_get_option_cmd() {} @@ -324,22 +302,11 @@ class set_option_cmd : public set_get_option_cmd { } void set_param(cmd_context & ctx, char const * value) { - m_ini.freeze(ctx.has_manager()); - std::string internal_opt = smt_keyword2opt_name(m_option); try { - std::string old_value; - if (!m_ini.get_param_value(internal_opt.c_str(), old_value)) { - m_unsupported = true; - return; - } - m_ini.set_param_value(internal_opt.c_str(), value); + gparams::set(m_option, value); } - catch (set_get_param_exception ex) { - std::string msg = "error setting '"; - msg += m_option.str(); - msg += "', "; - msg += ex.get_msg(); - throw cmd_exception(msg); + catch (gparams::exception ex) { + throw cmd_exception(ex.msg()); } } @@ -545,12 +512,10 @@ public: print_bool(ctx, ctx.m().int_real_coercions()); } else { - std::string iopt = smt_keyword2opt_name(opt); - std::string r; - if (m_ini.get_param_value(iopt.c_str(), r)) { - ctx.regular_stream() << r << std::endl; + try { + std::string val = gparams::get_value(opt); } - else { + catch (gparams::exception ex) { ctx.print_unsupported(opt); } } diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index afcac48ac..d14ce3076 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -39,6 +39,22 @@ Notes: #include"model_evaluator.h" #include"for_each_expr.h" +std::string smt2_keyword_to_param(symbol const & opt) { + std::string r; + SASSERT(opt.bare_str()[0] == ':'); + r = opt.bare_str() + 1; + unsigned sz = static_cast(r.size()); + for (unsigned i = 0; i < sz; i++) { + char curr = r[i]; + if ('A' <= curr && curr <= 'Z') + r[i] = curr - 'A' + 'a'; + else if (curr == '-') + r[i] = '_'; + } + TRACE("smt2_keyword_to_param", tout << opt << " -> '" << r << "'\n";); + return r; +} + func_decls::func_decls(ast_manager & m, func_decl * f): m_decls(TAG(func_decl*, f, 0)) { m.inc_ref(f); @@ -1400,9 +1416,9 @@ void cmd_context::validate_model() { get_check_sat_result()->get_model(md); SASSERT(md.get() != 0); params_ref p; - p.set_uint(":max-degree", UINT_MAX); // evaluate algebraic numbers of any degree. - p.set_uint(":sort-store", true); - p.set_bool(":model-completion", true); + p.set_uint("max_degree", UINT_MAX); // evaluate algebraic numbers of any degree. + p.set_uint("sort_store", true); + p.set_bool("model_completion", true); model_evaluator evaluator(*(md.get()), p); contains_array_op_proc contains_array(m()); { diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 5f83e0224..6688f66d9 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -37,6 +37,11 @@ Notes: #include"progress_callback.h" #include"scoped_ptr_vector.h" +/** + \brief Auxiliary function for converting SMT2 keywords into Z3 internal parameter names. +*/ +std::string smt2_keyword_to_param(symbol const & k); + struct front_end_params; class func_decls { diff --git a/src/cmd_context/eval_cmd.cpp b/src/cmd_context/eval_cmd.cpp index fe9c738a2..7ebe2f54f 100644 --- a/src/cmd_context/eval_cmd.cpp +++ b/src/cmd_context/eval_cmd.cpp @@ -62,7 +62,7 @@ public: SASSERT(last_result); last_result->get_model(md); expr_ref r(ctx.m()); - unsigned timeout = m_params.get_uint(":timeout", UINT_MAX); + unsigned timeout = m_params.get_uint("timeout", UINT_MAX); model_evaluator ev(*(md.get()), m_params); cancel_eh eh(ev); { diff --git a/src/cmd_context/extra_cmds/dbg_cmds.cpp b/src/cmd_context/extra_cmds/dbg_cmds.cpp index b7b4f058d..509b5ff2e 100644 --- a/src/cmd_context/extra_cmds/dbg_cmds.cpp +++ b/src/cmd_context/extra_cmds/dbg_cmds.cpp @@ -141,8 +141,8 @@ public: UNARY_CMD(bool_rewriter_cmd, "dbg-bool-rewriter", "", "apply the Boolean rewriter to the given term", CPK_EXPR, expr *, { expr_ref t(ctx.m()); params_ref p; - p.set_bool(":flat", false); - SASSERT(p.get_bool(":flat", true) == false); + p.set_bool("flat", false); + SASSERT(p.get_bool("flat", true) == false); bool_rewriter_star r(ctx.m(), p); r(arg, t); ctx.display(ctx.regular_stream(), t); @@ -153,7 +153,7 @@ UNARY_CMD(bool_frewriter_cmd, "dbg-bool-flat-rewriter", "", "apply the Boo expr_ref t(ctx.m()); { params_ref p; - p.set_bool(":flat", true); + p.set_bool("flat", true); bool_rewriter_star r(ctx.m(), p); r(arg, t); } @@ -165,8 +165,8 @@ UNARY_CMD(elim_and_cmd, "dbg-elim-and", "", "apply the Boolean rewriter (e expr_ref t(ctx.m()); { params_ref p; - p.set_bool(":flat", true); - p.set_bool(":elim-and", true); + p.set_bool("flat", true); + p.set_bool("elim_and", true); bool_rewriter_star r(ctx.m(), p); r(arg, t); } @@ -208,15 +208,15 @@ UNARY_CMD(some_value_cmd, "dbg-some-value", "", "retrieve some value of th void tst_params(cmd_context & ctx) { params_ref p1; params_ref p2; - p1.set_uint(":val", 100); + p1.set_uint("val", 100); p2 = p1; - SASSERT(p2.get_uint(":val", 0) == 100); - p2.set_uint(":val", 200); - SASSERT(p2.get_uint(":val", 0) == 200); - SASSERT(p1.get_uint(":val", 0) == 100); + SASSERT(p2.get_uint("val", 0) == 100); + p2.set_uint("val", 200); + SASSERT(p2.get_uint("val", 0) == 200); + SASSERT(p1.get_uint("val", 0) == 100); p2 = p1; - SASSERT(p2.get_uint(":val", 0) == 100); - SASSERT(p1.get_uint(":val", 0) == 100); + SASSERT(p2.get_uint("val", 0) == 100); + SASSERT(p1.get_uint("val", 0) == 100); ctx.regular_stream() << "worked" << std::endl; } diff --git a/src/cmd_context/extra_cmds/subpaving_cmds.cpp b/src/cmd_context/extra_cmds/subpaving_cmds.cpp index 9b84ddf68..632f558dc 100644 --- a/src/cmd_context/extra_cmds/subpaving_cmds.cpp +++ b/src/cmd_context/extra_cmds/subpaving_cmds.cpp @@ -31,7 +31,7 @@ static void to_subpaving(cmd_context & ctx, expr * t) { expr2var e2v(m); expr2subpaving e2s(m, *s, &e2v); params_ref p; - p.set_bool(":mul-to-power", true); + p.set_bool("mul_to_power", true); th_rewriter simp(m, p); expr_ref t_s(m); simp(t, t_s); diff --git a/src/cmd_context/parametric_cmd.cpp b/src/cmd_context/parametric_cmd.cpp index bc06d3ee6..f028c3b9d 100644 --- a/src/cmd_context/parametric_cmd.cpp +++ b/src/cmd_context/parametric_cmd.cpp @@ -16,6 +16,7 @@ Notes: --*/ #include +#include"cmd_context.h" #include"parametric_cmd.h" char const * parametric_cmd::get_descr(cmd_context & ctx) const { @@ -37,13 +38,15 @@ cmd_arg_kind parametric_cmd::next_arg_kind(cmd_context & ctx) const { void parametric_cmd::set_next_arg(cmd_context & ctx, symbol const & s) { if (m_last == symbol::null) { - m_last = s; + m_last = symbol(smt2_keyword_to_param(s).c_str()); if (pdescrs(ctx).get_kind(m_last.bare_str()) == CPK_INVALID) throw cmd_exception("invalid keyword argument"); return; } - m_params.set_sym(m_last.bare_str(), s); - m_last = symbol::null; + else { + m_params.set_sym(m_last.bare_str(), s); + m_last = symbol::null; + } } param_descrs const & parametric_cmd::pdescrs(cmd_context & ctx) const { diff --git a/src/cmd_context/simplify_cmd.cpp b/src/cmd_context/simplify_cmd.cpp index 089eb353b..3a1828a51 100644 --- a/src/cmd_context/simplify_cmd.cpp +++ b/src/cmd_context/simplify_cmd.cpp @@ -40,9 +40,9 @@ public: virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) { th_rewriter::get_param_descrs(p); insert_timeout(p); - p.insert(":print", CPK_BOOL, "(default: true) print the simplified term."); - p.insert(":print-proofs", CPK_BOOL, "(default: false) print a proof showing the original term is equal to the resultant one."); - p.insert(":print-statistics", CPK_BOOL, "(default: false) print statistics."); + p.insert("print", CPK_BOOL, "(default: true) print the simplified term."); + p.insert("print_proofs", CPK_BOOL, "(default: false) print a proof showing the original term is equal to the resultant one."); + p.insert("print_statistics", CPK_BOOL, "(default: false) print statistics."); } virtual ~simplify_cmd() { @@ -67,12 +67,12 @@ public: throw cmd_exception("invalid simplify command, argument expected"); expr_ref r(ctx.m()); proof_ref pr(ctx.m()); - if (m_params.get_bool(":som", false)) - m_params.set_bool(":flat", true); + if (m_params.get_bool("som", false)) + m_params.set_bool("flat", true); th_rewriter s(ctx.m(), m_params); unsigned cache_sz; unsigned num_steps = 0; - unsigned timeout = m_params.get_uint(":timeout", UINT_MAX); + unsigned timeout = m_params.get_uint("timeout", UINT_MAX); bool failed = false; cancel_eh eh(s); { @@ -94,17 +94,17 @@ public: num_steps = s.get_num_steps(); s.cleanup(); } - if (m_params.get_bool(":print", true)) { + if (m_params.get_bool("print", true)) { ctx.display(ctx.regular_stream(), r); ctx.regular_stream() << std::endl; } - if (!failed && m_params.get_bool(":print-proofs", false)) { + if (!failed && m_params.get_bool("print_proofs", false)) { ast_smt_pp pp(ctx.m()); pp.set_logic(ctx.get_logic().str().c_str()); pp.display_expr_smt2(ctx.regular_stream(), pr.get()); ctx.regular_stream() << std::endl; } - if (m_params.get_bool(":print-statistics", false)) { + if (m_params.get_bool("print_statistics", false)) { shared_occs s1(ctx.m()); if (!failed) s1(r); diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index 32adb5f47..b911e3634 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -153,7 +153,7 @@ public: virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) { insert_timeout(p); insert_max_memory(p); - p.insert(":print-statistics", CPK_BOOL, "(default: false) print statistics."); + p.insert("print_statistics", CPK_BOOL, "(default: false) print statistics."); } void display_statistics(cmd_context & ctx, tactic * t) { @@ -180,9 +180,9 @@ public: virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) { exec_given_tactic_cmd::init_pdescrs(ctx, p); - p.insert(":print-unsat-core", CPK_BOOL, "(default: false) print unsatisfiable core."); - p.insert(":print-proof", CPK_BOOL, "(default: false) print proof."); - p.insert(":print-model", CPK_BOOL, "(default: false) print model."); + p.insert("print_unsat_core", CPK_BOOL, "(default: false) print unsatisfiable core."); + p.insert("print_proof", CPK_BOOL, "(default: false) print proof."); + p.insert("print_model", CPK_BOOL, "(default: false) print model."); } virtual void execute(cmd_context & ctx) { @@ -192,7 +192,7 @@ public: tref->set_front_end_params(ctx.params()); tref->set_logic(ctx.get_logic()); ast_manager & m = ctx.m(); - unsigned timeout = p.get_uint(":timeout", UINT_MAX); + unsigned timeout = p.get_uint("timeout", UINT_MAX); goal_ref g = alloc(goal, m, ctx.produce_proofs(), ctx.produce_models(), ctx.produce_unsat_cores()); assert_exprs_from(ctx, *g); TRACE("check_sat_using", g->display(tout);); @@ -241,7 +241,7 @@ public: ptr_vector core_elems; m.linearize(core, core_elems); result->m_core.append(core_elems.size(), core_elems.c_ptr()); - if (p.get_bool(":print-unsat-core", false)) { + if (p.get_bool("print_unsat_core", false)) { ctx.regular_stream() << "(unsat-core"; ptr_vector::const_iterator it = core_elems.begin(); ptr_vector::const_iterator end = core_elems.end(); @@ -255,7 +255,7 @@ public: if (ctx.produce_models() && md) { result->m_model = md; - if (p.get_bool(":print-model", false)) { + if (p.get_bool("print_model", false)) { ctx.regular_stream() << "(model " << std::endl; model_smt2_pp(ctx.regular_stream(), ctx, *md, 2); ctx.regular_stream() << ")" << std::endl; @@ -266,12 +266,12 @@ public: if (ctx.produce_proofs() && pr) { result->m_proof = pr; - if (p.get_bool(":print-proof", false)) { + if (p.get_bool("print_proof", false)) { ctx.regular_stream() << mk_ismt2_pp(pr, m) << "\n"; } } - if (p.get_bool(":print-statistics", false)) + if (p.get_bool("print_statistics", false)) display_statistics(ctx, tref.get()); } }; @@ -285,14 +285,14 @@ public: virtual char const * get_main_descr() const { return "apply the given tactic to the current context, and print the resultant set of goals."; } virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) { - p.insert(":print", CPK_BOOL, "(default: true) print resultant goals."); + p.insert("print", CPK_BOOL, "(default: true) print resultant goals."); #ifndef _EXTERNAL_RELEASE - p.insert(":print-proof", CPK_BOOL, "(default: false) print proof associated with each assertion."); + p.insert("print_proof", CPK_BOOL, "(default: false) print proof associated with each assertion."); #endif - p.insert(":print-model-converter", CPK_BOOL, "(default: false) print model converter."); - p.insert(":print-benchmark", CPK_BOOL, "(default: false) display resultant goals as a SMT2 benchmark."); + p.insert("print_model_converter", CPK_BOOL, "(default: false) print model converter."); + p.insert("print_benchmark", CPK_BOOL, "(default: false) display resultant goals as a SMT2 benchmark."); #ifndef _EXTERNAL_RELEASE - p.insert(":print-dependencies", CPK_BOOL, "(default: false) print dependencies when displaying the resultant set of goals."); + p.insert("print_dependencies", CPK_BOOL, "(default: false) print dependencies when displaying the resultant set of goals."); #endif exec_given_tactic_cmd::init_pdescrs(ctx, p); } @@ -307,7 +307,7 @@ public: goal_ref g = alloc(goal, m, ctx.produce_proofs(), ctx.produce_models(), ctx.produce_unsat_cores()); assert_exprs_from(ctx, *g); - unsigned timeout = p.get_uint(":timeout", UINT_MAX); + unsigned timeout = p.get_uint("timeout", UINT_MAX); goal_ref_buffer result_goals; model_converter_ref mc; @@ -330,8 +330,8 @@ public: } } - if (!failed && p.get_bool(":print", true)) { - bool print_dependencies = p.get_bool(":print-dependencies", false); + if (!failed && p.get_bool("print", true)) { + bool print_dependencies = p.get_bool("print_dependencies", false); ctx.regular_stream() << "(goals\n"; unsigned sz = result_goals.size(); for (unsigned i = 0; i < sz; i++) { @@ -344,12 +344,12 @@ public: } #ifndef _EXTERNAL_RELEASE - if (!failed && ctx.produce_proofs() && p.get_bool(":print-proof", false)) { + if (!failed && ctx.produce_proofs() && p.get_bool("print_proof", false)) { // TODO } #endif - if (!failed && p.get_bool(":print-benchmark", false)) { + if (!failed && p.get_bool("print_benchmark", false)) { unsigned num_goals = result_goals.size(); SASSERT(num_goals > 0); if (num_goals == 1) { @@ -381,10 +381,10 @@ public: } } - if (!failed && mc && p.get_bool(":print-model-converter", false)) + if (!failed && mc && p.get_bool("print_model_converter", false)) mc->display(ctx.regular_stream()); - if (p.get_bool(":print-statistics", false)) + if (p.get_bool("print_statistics", false)) display_statistics(ctx, tref.get()); } } diff --git a/src/front_end_params/arith_simplifier_params.cpp b/src/front_end_params/arith_simplifier_params.cpp index 0c2f5c710..21808bc1e 100644 --- a/src/front_end_params/arith_simplifier_params.cpp +++ b/src/front_end_params/arith_simplifier_params.cpp @@ -20,7 +20,7 @@ Revision History: #include"arith_simplifier_params.h" void arith_simplifier_params::register_params(ini_params & p) { - p.register_bool_param("ARITH_EXPAND_EQS", m_arith_expand_eqs); - p.register_bool_param("ARITH_PROCESS_ALL_EQS", m_arith_process_all_eqs); + p.register_bool_param("arith_expand_eqs", m_arith_expand_eqs); + p.register_bool_param("arith_process_all_eqs", m_arith_process_all_eqs); } diff --git a/src/front_end_params/bit_blaster_params.h b/src/front_end_params/bit_blaster_params.h index 8196774ca..ab183d7fc 100644 --- a/src/front_end_params/bit_blaster_params.h +++ b/src/front_end_params/bit_blaster_params.h @@ -29,8 +29,8 @@ struct bit_blaster_params { m_bb_quantifiers(false) { } void register_params(ini_params & p) { - p.register_bool_param("BB_EXT_GATES", m_bb_ext_gates, "use extended gates during bit-blasting"); - p.register_bool_param("BB_QUANTIFIERS", m_bb_quantifiers, "convert bit-vectors to Booleans in quantifiers"); + p.register_bool_param("bb_ext_gates", m_bb_ext_gates, "use extended gates during bit-blasting"); + p.register_bool_param("bb_quantifiers", m_bb_quantifiers, "convert bit-vectors to Booleans in quantifiers"); } }; diff --git a/src/front_end_params/bv_simplifier_params.h b/src/front_end_params/bv_simplifier_params.h index a6ff749c4..50dedfd22 100644 --- a/src/front_end_params/bv_simplifier_params.h +++ b/src/front_end_params/bv_simplifier_params.h @@ -30,8 +30,8 @@ struct bv_simplifier_params { m_bv2int_distribute(true) { } void register_params(ini_params & p) { - p.register_bool_param("HI_DIV0", m_hi_div0, "if true, then Z3 uses the usual hardware interpretation for division (rem, mod) by zero. Otherwise, these operations are considered uninterpreted."); - p.register_bool_param("BV2INT_DISTRIBUTE", m_bv2int_distribute, "if true, then int2bv is distributed over arithmetical operators."); + p.register_bool_param("hi_div0", m_hi_div0, "if true, then Z3 uses the usual hardware interpretation for division (rem, mod) by zero. Otherwise, these operations are considered uninterpreted."); + p.register_bool_param("bv2int_distribute", m_bv2int_distribute, "if true, then int2bv is distributed over arithmetical operators."); } }; diff --git a/src/front_end_params/cnf_params.cpp b/src/front_end_params/cnf_params.cpp index 57d02e8db..fffd698a6 100644 --- a/src/front_end_params/cnf_params.cpp +++ b/src/front_end_params/cnf_params.cpp @@ -20,7 +20,7 @@ Revision History: #include"cnf_params.h" void cnf_params::register_params(ini_params & p) { - p.register_unsigned_param("CNF_FACTOR", m_cnf_factor, "the maximum number of clauses that can be created when converting a subformula"); - p.register_int_param("CNF_MODE", 0, 3, reinterpret_cast(m_cnf_mode), "CNF translation mode: 0 - disabled, 1 - quantifiers in CNF, 2 - 0 + opportunistic, 3 - full"); + p.register_unsigned_param("cnf_factor", m_cnf_factor, "the maximum number of clauses that can be created when converting a subformula"); + p.register_int_param("cnf_mode", 0, 3, reinterpret_cast(m_cnf_mode), "CNF translation mode: 0 - disabled, 1 - quantifiers in CNF, 2 - 0 + opportunistic, 3 - full"); } diff --git a/src/front_end_params/dyn_ack_params.cpp b/src/front_end_params/dyn_ack_params.cpp index b4d0546a9..90a0bb17b 100644 --- a/src/front_end_params/dyn_ack_params.cpp +++ b/src/front_end_params/dyn_ack_params.cpp @@ -19,13 +19,13 @@ Revision History: #include"dyn_ack_params.h" void dyn_ack_params::register_params(ini_params & p) { - p.register_int_param("DACK", 0, 2, reinterpret_cast(m_dack), + p.register_int_param("dack", 0, 2, reinterpret_cast(m_dack), "0 - disable dynamic ackermannization, 1 - expand Leibniz's axiom if a congruence is the root of a conflict, 2 - expand Leibniz's axiom if a congruence is used during conflict resolution."); - p.register_bool_param("DACK_EQ", m_dack_eq, "enable dynamic ackermannization for transtivity of equalities"); - p.register_unsigned_param("DACK_THRESHOLD", m_dack_threshold, "number of times the congruence rule must be used before Leibniz's axiom is expanded"); - p.register_double_param("DACK_FACTOR", m_dack_factor, "number of instance per conflict"); - p.register_unsigned_param("DACK_GC", m_dack_gc, "Dynamic ackermannization garbage collection frequency (per conflict)."); - p.register_double_param("DACK_GC_INV_DECAY", m_dack_gc_inv_decay); + p.register_bool_param("dack_eq", m_dack_eq, "enable dynamic ackermannization for transtivity of equalities"); + p.register_unsigned_param("dack_threshold", m_dack_threshold, "number of times the congruence rule must be used before Leibniz's axiom is expanded"); + p.register_double_param("dack_factor", m_dack_factor, "number of instance per conflict"); + p.register_unsigned_param("dack_gc", m_dack_gc, "Dynamic ackermannization garbage collection frequency (per conflict)."); + p.register_double_param("dack_gc_inv_decay", m_dack_gc_inv_decay); } diff --git a/src/front_end_params/front_end_params.cpp b/src/front_end_params/front_end_params.cpp index 7aea7e7ee..9d05a3fc3 100644 --- a/src/front_end_params/front_end_params.cpp +++ b/src/front_end_params/front_end_params.cpp @@ -25,62 +25,62 @@ void front_end_params::register_params(ini_params & p) { parser_params::register_params(p); arith_simplifier_params::register_params(p); model_params::register_params(p); - p.register_bool_param("AT_LABELS_CEX", m_at_labels_cex, + p.register_bool_param("at_labels_cex", m_at_labels_cex, "only use labels that contain '@' when building multiple counterexamples"); - p.register_bool_param("CHECK_AT_LABELS", m_check_at_labels, + p.register_bool_param("check_at_labels", m_check_at_labels, "check that labels containing '@' are used correctly to only produce unique counter examples"); - p.register_bool_param("DEFAULT_QID", m_default_qid, "create a default quantifier id based on its position, the id is used to report profiling information (see QI_PROFILE)"); + p.register_bool_param("default_qid", m_default_qid, "create a default quantifier id based on its position, the id is used to report profiling information (see QI_PROFILE)"); - p.register_bool_param("TYPE_CHECK", m_well_sorted_check, "enable/disable type checker"); - p.register_bool_param("WELL_SORTED_CHECK", m_well_sorted_check, "enable/disable type checker"); - p.register_bool_param("INTERACTIVE", m_interactive, "enable interactive mode using Simplify input format"); - p.register_unsigned_param("SOFT_TIMEOUT", m_soft_timeout, "set approximate timeout for each solver query (milliseconds), the value 0 represents no timeout", true); - p.register_double_param("INSTRUCTION_MAX", m_instr_out, "set the (approximate) maximal number of instructions per invocation of check", true); - p.register_bool_param("AUTO_CONFIG", m_auto_config, "use heuristics to set Z3 configuration parameters, it is only available for the SMT-LIB input format"); - p.register_int_param("PROOF_MODE", 0, 2, reinterpret_cast(m_proof_mode), "select proof generation mode: 0 - disabled, 1 - coarse grain, 2 - fine grain"); - p.register_bool_param("TRACE", m_trace, "enable tracing for the Axiom Profiler tool"); - p.register_string_param("TRACE_FILE_NAME", m_trace_file_name, "tracing file name"); - p.register_bool_param("ASYNC_COMMANDS", m_async_commands, "enable/disable support for asynchronous commands in the Simplify front-end."); - p.register_bool_param("DISPLAY_CONFIG", m_display_config, "display configuration used by Z3"); + p.register_bool_param("type_check", m_well_sorted_check, "enable/disable type checker"); + p.register_bool_param("well_sorted_check", m_well_sorted_check, "enable/disable type checker"); + p.register_bool_param("interactive", m_interactive, "enable interactive mode using Simplify input format"); + p.register_unsigned_param("soft_timeout", m_soft_timeout, "set approximate timeout for each solver query (milliseconds), the value 0 represents no timeout", true); + p.register_double_param("instruction_max", m_instr_out, "set the (approximate) maximal number of instructions per invocation of check", true); + p.register_bool_param("auto_config", m_auto_config, "use heuristics to set Z3 configuration parameters, it is only available for the SMT-LIB input format"); + p.register_int_param("proof_mode", 0, 2, reinterpret_cast(m_proof_mode), "select proof generation mode: 0 - disabled, 1 - coarse grain, 2 - fine grain"); + p.register_bool_param("trace", m_trace, "enable tracing for the Axiom Profiler tool"); + p.register_string_param("trace_file_name", m_trace_file_name, "tracing file name"); + p.register_bool_param("async_commands", m_async_commands, "enable/disable support for asynchronous commands in the Simplify front-end."); + p.register_bool_param("display_config", m_display_config, "display configuration used by Z3"); #ifdef _WINDOWS // The non-windows memory manager does not have access to memory sizes. - p.register_unsigned_param("MEMORY_HIGH_WATERMARK", m_memory_high_watermark, + p.register_unsigned_param("memory_high_watermark", m_memory_high_watermark, "set high watermark for memory consumption (in megabytes)"); - p.register_unsigned_param("MEMORY_MAX_SIZE", m_memory_max_size, + p.register_unsigned_param("memory_max_size", m_memory_max_size, "set hard upper limit for memory consumption (in megabytes)"); #endif #ifndef _EXTERNAL_RELEASE // external users should not have access to it. - p.register_bool_param("PREPROCESS", m_preprocess); + p.register_bool_param("preprocess", m_preprocess); #endif - p.register_bool_param("USER_THEORY_PREPROCESS_AXIOMS", + p.register_bool_param("user_theory_preprocess_axioms", m_user_theory_preprocess_axioms, "Apply full pre-processing to user theory axioms", true); - p.register_bool_param("USER_THEORY_PERSIST_AXIOMS", + p.register_bool_param("user_theory_persist_axioms", m_user_theory_persist_axioms, "Persist user axioms to the base level", true); - p.register_bool_param("SMTLIB2_COMPLIANT", m_smtlib2_compliant); + p.register_bool_param("smtlib2_compliant", m_smtlib2_compliant); - p.register_bool_param("IGNORE_BAD_PATTERNS", m_ignore_bad_patterns); + p.register_bool_param("ignore_bad_patterns", m_ignore_bad_patterns); PRIVATE_PARAMS({ - p.register_bool_param("IGNORE_CHECKSAT", m_ignore_checksat); - p.register_bool_param("DEBUG_REF_COUNT", m_debug_ref_count); - p.register_bool_param("IGNORE_USER_PATTERNS", m_ignore_user_patterns); - p.register_bool_param("INCREMENTAL_CORE_ASSERT", m_incremental_core_assert); - DEBUG_CODE(p.register_int_param("COPY_PARAMS", m_copy_params);); + p.register_bool_param("ignore_checksat", m_ignore_checksat); + p.register_bool_param("debug_ref_count", m_debug_ref_count); + p.register_bool_param("ignore_user_patterns", m_ignore_user_patterns); + p.register_bool_param("incremental_core_assert", m_incremental_core_assert); + DEBUG_CODE(p.register_int_param("copy_params", m_copy_params);); }); // temporary hack until strategic_solver is ported to new tactic framework PRIVATE_PARAMS({ - p.register_bool_param("NLSAT", m_nlsat); + p.register_bool_param("nlsat", m_nlsat); }); } diff --git a/src/front_end_params/model_params.cpp b/src/front_end_params/model_params.cpp index df6420b7a..a859684d8 100644 --- a/src/front_end_params/model_params.cpp +++ b/src/front_end_params/model_params.cpp @@ -20,14 +20,14 @@ Revision History: #include"model_params.h" void model_params::register_params(ini_params & p) { - p.register_bool_param("MODEL_PARTIAL", m_model_partial, "enable/disable partial function interpretations", true); - p.register_bool_param("MODEL_V1", m_model_v1_pp, + p.register_bool_param("model_partial", m_model_partial, "enable/disable partial function interpretations", true); + p.register_bool_param("model_v1", m_model_v1_pp, "use Z3 version 1.x pretty printer", true); - p.register_bool_param("MODEL_V2", m_model_v2_pp, + p.register_bool_param("model_v2", m_model_v2_pp, "use Z3 version 2.x (x <= 16) pretty printer", true); - p.register_bool_param("MODEL_COMPACT", m_model_compact, + p.register_bool_param("model_compact", m_model_compact, "try to compact function graph (i.e., function interpretations that are lookup tables", true); - p.register_bool_param("MODEL_COMPLETION", m_model_completion, + p.register_bool_param("model_completion", m_model_completion, "assigns an interptetation to symbols that do not have one in the current model, when evaluating expressions in the current model", true); } diff --git a/src/front_end_params/nnf_params.cpp b/src/front_end_params/nnf_params.cpp index 044ca155e..351997f98 100644 --- a/src/front_end_params/nnf_params.cpp +++ b/src/front_end_params/nnf_params.cpp @@ -19,8 +19,8 @@ Revision History: #include"nnf_params.h" void nnf_params::register_params(ini_params & p) { - p.register_unsigned_param("NNF_FACTOR", m_nnf_factor, "the maximum growth factor during NNF translation (auxiliary definitions are introduced if the threshold is reached)"); - p.register_int_param("NNF_MODE", 0, 3, reinterpret_cast(m_nnf_mode), "NNF translation mode: 0 - skolem normal form, 1 - 0 + quantifiers in NNF, 2 - 1 + opportunistic, 3 - full"); - p.register_bool_param("NNF_IGNORE_LABELS", m_nnf_ignore_labels, "remove/ignore labels in the input formula, this option is ignored if proofs are enabled"); - p.register_bool_param("NNF_SK_HACK", m_nnf_sk_hack, "hack for VCC"); + p.register_unsigned_param("nnf_factor", m_nnf_factor, "the maximum growth factor during NNF translation (auxiliary definitions are introduced if the threshold is reached)"); + p.register_int_param("nnf_mode", 0, 3, reinterpret_cast(m_nnf_mode), "NNF translation mode: 0 - skolem normal form, 1 - 0 + quantifiers in NNF, 2 - 1 + opportunistic, 3 - full"); + p.register_bool_param("nnf_ignore_labels", m_nnf_ignore_labels, "remove/ignore labels in the input formula, this option is ignored if proofs are enabled"); + p.register_bool_param("nnf_sk_hack", m_nnf_sk_hack, "hack for VCC"); } diff --git a/src/front_end_params/params2front_end_params.cpp b/src/front_end_params/params2front_end_params.cpp index a2bae371c..4c5866786 100644 --- a/src/front_end_params/params2front_end_params.cpp +++ b/src/front_end_params/params2front_end_params.cpp @@ -27,28 +27,28 @@ Revision History: the new strategy framework. */ void params2front_end_params(params_ref const & s, front_end_params & t) { - t.m_relevancy_lvl = s.get_uint(":relevancy", t.m_relevancy_lvl); + t.m_relevancy_lvl = s.get_uint("relevancy", t.m_relevancy_lvl); TRACE("qi_cost", s.display(tout); tout << "\n";); - t.m_qi_cost = s.get_str(":qi-cost", t.m_qi_cost.c_str()); - t.m_mbqi = s.get_bool(":mbqi", t.m_mbqi); - t.m_mbqi_max_iterations = s.get_uint(":mbqi-max-iterations", t.m_mbqi_max_iterations); - t.m_random_seed = s.get_uint(":random-seed", t.m_random_seed); - t.m_model = s.get_bool(":produce-models", t.m_model); - if (s.get_bool(":produce-proofs", false)) + t.m_qi_cost = s.get_str("qi_cost", t.m_qi_cost.c_str()); + t.m_mbqi = s.get_bool("mbqi", t.m_mbqi); + t.m_mbqi_max_iterations = s.get_uint("mbqi_max_iterations", t.m_mbqi_max_iterations); + t.m_random_seed = s.get_uint("random_seed", t.m_random_seed); + t.m_model = s.get_bool("produce_models", t.m_model); + if (s.get_bool("produce_proofs", false)) t.m_proof_mode = PGM_FINE; - t.m_well_sorted_check = s.get_bool(":check-sorts", t.m_well_sorted_check); - t.m_qi_eager_threshold = s.get_double(":qi-eager-threshold", t.m_qi_eager_threshold); - t.m_qi_lazy_threshold = s.get_double(":qi-lazy-threshold", t.m_qi_lazy_threshold); - t.m_preprocess = s.get_bool(":preprocess", t.m_preprocess); - t.m_hi_div0 = s.get_bool(":hi-div0", t.m_hi_div0); - t.m_auto_config = s.get_bool(":auto-config", t.m_auto_config); - t.m_array_simplify = s.get_bool(":array-old-simplifier", t.m_array_simplify); - t.m_arith_branch_cut_ratio = s.get_uint(":arith-branch-cut-ratio", t.m_arith_branch_cut_ratio); - t.m_arith_expand_eqs = s.get_bool(":arith-expand-eqs", t.m_arith_expand_eqs); + t.m_well_sorted_check = s.get_bool("check_sorts", t.m_well_sorted_check); + t.m_qi_eager_threshold = s.get_double("qi_eager_threshold", t.m_qi_eager_threshold); + t.m_qi_lazy_threshold = s.get_double("qi_lazy_threshold", t.m_qi_lazy_threshold); + t.m_preprocess = s.get_bool("preprocess", t.m_preprocess); + t.m_hi_div0 = s.get_bool("hi_div0", t.m_hi_div0); + t.m_auto_config = s.get_bool("auto_config", t.m_auto_config); + t.m_array_simplify = s.get_bool("array_old_simplifier", t.m_array_simplify); + t.m_arith_branch_cut_ratio = s.get_uint("arith_branch_cut_ratio", t.m_arith_branch_cut_ratio); + t.m_arith_expand_eqs = s.get_bool("arith_expand_eqs", t.m_arith_expand_eqs); - if (s.get_bool(":arith-greatest-error-pivot", false)) + if (s.get_bool("arith_greatest_error_pivot", false)) t.m_arith_pivot_strategy = ARITH_PIVOT_GREATEST_ERROR; - else if (s.get_bool(":arith-least-error-pivot", false)) + else if (s.get_bool("arith_least_error_pivot", false)) t.m_arith_pivot_strategy = ARITH_PIVOT_LEAST_ERROR; } @@ -59,22 +59,22 @@ void params2front_end_params(params_ref const & s, front_end_params & t) { */ void front_end_params2params(front_end_params const & s, params_ref & t) { if (s.m_model) - t.set_bool(":produce-models", true); + t.set_bool("produce_models", true); if (!s.m_hi_div0) - t.set_bool(":hi-div0", false); + t.set_bool("hi_div0", false); } /** \brief Bridge for using params_ref with smt::context. */ void solver_front_end_params_descrs(param_descrs & r) { - r.insert(":hi-div0", CPK_BOOL, "(default: true) if true, then Z3 uses the usual hardware interpretation for division (rem, mod) by zero. Otherwise, these operations are considered uninterpreted"); - r.insert(":relevancy", CPK_UINT, "relevancy propagation heuristic: 0 - disabled, 1 - relevancy is tracked by only affects quantifier instantiation, 2 - relevancy is tracked, and an atom is only asserted if it is relevant"); - r.insert(":mbqi", CPK_BOOL, "model based quantifier instantiation (MBQI)"); - r.insert(":mbqi-max-iterations", CPK_UINT, "maximum number of rounds of MBQI"); - r.insert(":random-seed", CPK_UINT, "random seed for smt solver"); - r.insert(":qi-eager-threshold", CPK_DOUBLE, "threshold for eager quantifier instantiation"); - r.insert(":qi-lazy-threshold", CPK_DOUBLE, "threshold for lazy quantifier instantiation"); - r.insert(":auto_config", CPK_BOOL, "use heuristics to automatically configure smt solver"); - r.insert(":arith-branch-cut-ratio", CPK_UINT, "branch&bound / gomory cut ratio"); + r.insert("hi_div0", CPK_BOOL, "(default: true) if true, then Z3 uses the usual hardware interpretation for division (rem, mod) by zero. Otherwise, these operations are considered uninterpreted"); + r.insert("relevancy", CPK_UINT, "relevancy propagation heuristic: 0 - disabled, 1 - relevancy is tracked by only affects quantifier instantiation, 2 - relevancy is tracked, and an atom is only asserted if it is relevant"); + r.insert("mbqi", CPK_BOOL, "model based quantifier instantiation (MBQI)"); + r.insert("mbqi_max_iterations", CPK_UINT, "maximum number of rounds of MBQI"); + r.insert("random_seed", CPK_UINT, "random seed for smt solver"); + r.insert("qi_eager_threshold", CPK_DOUBLE, "threshold for eager quantifier instantiation"); + r.insert("qi_lazy_threshold", CPK_DOUBLE, "threshold for lazy quantifier instantiation"); + r.insert("auto_config", CPK_BOOL, "use heuristics to automatically configure smt solver"); + r.insert("arith_branch_cut_ratio", CPK_UINT, "branch&bound / gomory cut ratio"); } diff --git a/src/front_end_params/parser_params.cpp b/src/front_end_params/parser_params.cpp index 000885fa5..3edd03fb0 100644 --- a/src/front_end_params/parser_params.cpp +++ b/src/front_end_params/parser_params.cpp @@ -6,8 +6,8 @@ parser_params::parser_params() : } void parser_params::register_params(ini_params & p) { - p.register_bool_param("DUMP_GOAL_AS_SMT", m_dump_goal_as_smt, "write goal back to output in SMT format"); - p.register_bool_param("DISPLAY_ERROR_FOR_VISUAL_STUDIO", m_display_error_for_vs, "display error messages in Visual Studio format"); + p.register_bool_param("dump_goal_as_smt", m_dump_goal_as_smt, "write goal back to output in SMT format"); + p.register_bool_param("display_error_for_visual_studio", m_display_error_for_vs, "display error messages in Visual Studio format"); } diff --git a/src/front_end_params/pattern_inference_params.cpp b/src/front_end_params/pattern_inference_params.cpp index 176fdd8c2..4b0d4c964 100644 --- a/src/front_end_params/pattern_inference_params.cpp +++ b/src/front_end_params/pattern_inference_params.cpp @@ -19,19 +19,19 @@ Revision History: #include"pattern_inference_params.h" void pattern_inference_params::register_params(ini_params & p) { - p.register_unsigned_param("PI_MAX_MULTI_PATTERNS", m_pi_max_multi_patterns, + p.register_unsigned_param("pi_max_multi_patterns", m_pi_max_multi_patterns, "when patterns are not provided, the prover uses a heuristic to infer them. This option sets the threshold on the number of extra multi-patterns that can be created. By default, the prover creates at most one multi-pattern when there is no unary pattern"); - p.register_bool_param("PI_BLOCK_LOOP_PATTERNS", m_pi_block_loop_patterns, + p.register_bool_param("pi_block_loop_patterns", m_pi_block_loop_patterns, "block looping patterns during pattern inference"); - p.register_int_param("PI_ARITH", 0, 2, reinterpret_cast(m_pi_arith), + p.register_int_param("pi_arith", 0, 2, reinterpret_cast(m_pi_arith), "0 - do not infer patterns with arithmetic terms, 1 - use patterns with arithmetic terms if there is no other pattern, 2 - always use patterns with arithmetic terms."); - p.register_bool_param("PI_USE_DATABASE", m_pi_use_database); - p.register_unsigned_param("PI_ARITH_WEIGHT", m_pi_arith_weight, "default weight for quantifiers where the only available pattern has nested arithmetic terms."); - p.register_unsigned_param("PI_NON_NESTED_ARITH_WEIGHT", m_pi_non_nested_arith_weight, "default weight for quantifiers where the only available pattern has non nested arithmetic terms."); - p.register_bool_param("PI_PULL_QUANTIFIERS", m_pi_pull_quantifiers, "pull nested quantifiers, if no pattern was found."); - p.register_int_param("PI_NOPAT_WEIGHT", m_pi_nopat_weight, "set weight of quantifiers without patterns, if negative the weight is not changed."); - p.register_bool_param("PI_AVOID_SKOLEMS", m_pi_avoid_skolems); - p.register_bool_param("PI_WARNINGS", m_pi_warnings, "enable/disable warning messages in the pattern inference module."); + p.register_bool_param("pi_use_database", m_pi_use_database); + p.register_unsigned_param("pi_arith_weight", m_pi_arith_weight, "default weight for quantifiers where the only available pattern has nested arithmetic terms."); + p.register_unsigned_param("pi_non_nested_arith_weight", m_pi_non_nested_arith_weight, "default weight for quantifiers where the only available pattern has non nested arithmetic terms."); + p.register_bool_param("pi_pull_quantifiers", m_pi_pull_quantifiers, "pull nested quantifiers, if no pattern was found."); + p.register_int_param("pi_nopat_weight", m_pi_nopat_weight, "set weight of quantifiers without patterns, if negative the weight is not changed."); + p.register_bool_param("pi_avoid_skolems", m_pi_avoid_skolems); + p.register_bool_param("pi_warnings", m_pi_warnings, "enable/disable warning messages in the pattern inference module."); } diff --git a/src/front_end_params/preprocessor_params.h b/src/front_end_params/preprocessor_params.h index 4b32feb60..89bd01b48 100644 --- a/src/front_end_params/preprocessor_params.h +++ b/src/front_end_params/preprocessor_params.h @@ -84,25 +84,25 @@ public: pattern_inference_params::register_params(p); bit_blaster_params::register_params(p); bv_simplifier_params::register_params(p); - p.register_int_param("LIFT_ITE", 0, 2, reinterpret_cast(m_lift_ite), "ite term lifting: 0 - no lifting, 1 - conservative, 2 - full"); - p.register_int_param("NG_LIFT_ITE", 0, 2, reinterpret_cast(m_ng_lift_ite), "ite (non-ground) term lifting: 0 - no lifting, 1 - conservative, 2 - full"); - p.register_bool_param("ELIM_TERM_ITE", m_eliminate_term_ite, "eliminate term if-then-else in the preprocessor"); - p.register_bool_param("ELIM_AND", m_eliminate_and, "represent (and a b) as (not (or (not a) (not b)))"); - p.register_bool_param("MACRO_FINDER", m_macro_finder, "try to find universally quantified formulas that can be viewed as macros"); - p.register_bool_param("PROPAGATE_VALUES", m_propagate_values, "propagate values during preprocessing step"); - p.register_bool_param("PROPAGATE_BOOLEANS", m_propagate_booleans, "propagate boolean values during preprocessing step"); - p.register_bool_param("PULL_CHEAP_ITE_TREES", m_pull_cheap_ite_trees); - p.register_bool_param("PULL_NESTED_QUANTIFIERS", m_pull_nested_quantifiers, "eliminate nested quantifiers by moving nested quantified variables to the outermost quantifier, it is unnecessary if the formula is converted into CNF"); - p.register_bool_param("REFINE_INJ_AXIOM", m_refine_inj_axiom); - p.register_bool_param("ELIM_BOUNDS", m_eliminate_bounds, "cheap Fourier-Motzkin"); + p.register_int_param("lift_ite", 0, 2, reinterpret_cast(m_lift_ite), "ite term lifting: 0 - no lifting, 1 - conservative, 2 - full"); + p.register_int_param("ng_lift_ite", 0, 2, reinterpret_cast(m_ng_lift_ite), "ite (non-ground) term lifting: 0 - no lifting, 1 - conservative, 2 - full"); + p.register_bool_param("elim_term_ite", m_eliminate_term_ite, "eliminate term if-then-else in the preprocessor"); + p.register_bool_param("elim_and", m_eliminate_and, "represent (and a b) as (not (or (not a) (not b)))"); + p.register_bool_param("macro_finder", m_macro_finder, "try to find universally quantified formulas that can be viewed as macros"); + p.register_bool_param("propagate_values", m_propagate_values, "propagate values during preprocessing step"); + p.register_bool_param("propagate_booleans", m_propagate_booleans, "propagate boolean values during preprocessing step"); + p.register_bool_param("pull_cheap_ite_trees", m_pull_cheap_ite_trees); + p.register_bool_param("pull_nested_quantifiers", m_pull_nested_quantifiers, "eliminate nested quantifiers by moving nested quantified variables to the outermost quantifier, it is unnecessary if the formula is converted into CNF"); + p.register_bool_param("refine_inj_axiom", m_refine_inj_axiom); + p.register_bool_param("elim_bounds", m_eliminate_bounds, "cheap Fourier-Motzkin"); - p.register_bool_param("BIT2INT", m_simplify_bit2int, "hoist bit2int conversions over arithmetical expressions"); - p.register_bool_param("DISTRIBUTE_FORALL", m_distribute_forall); - p.register_bool_param("REDUCE_ARGS", m_reduce_args); - p.register_bool_param("QUASI_MACROS", m_quasi_macros); - p.register_bool_param("RESTRICTED_QUASI_MACROS", m_restricted_quasi_macros); - p.register_bool_param("BV_MAX_SHARING", m_max_bv_sharing); - p.register_bool_param("PRE_SIMPLIFIER", m_pre_simplifier); + p.register_bool_param("bit2int", m_simplify_bit2int, "hoist bit2int conversions over arithmetical expressions"); + p.register_bool_param("distribute_forall", m_distribute_forall); + p.register_bool_param("reduce_args", m_reduce_args); + p.register_bool_param("quasi_macros", m_quasi_macros); + p.register_bool_param("restricted_quasi_macros", m_restricted_quasi_macros); + p.register_bool_param("bv_max_sharing", m_max_bv_sharing); + p.register_bool_param("pre_simplifier", m_pre_simplifier); } }; diff --git a/src/front_end_params/qi_params.h b/src/front_end_params/qi_params.h index bd41de12c..aee2c4d3d 100644 --- a/src/front_end_params/qi_params.h +++ b/src/front_end_params/qi_params.h @@ -107,31 +107,31 @@ struct qi_params { } void register_params(ini_params & p) { - p.register_unsigned_param("QI_MAX_EAGER_MULTI_PATTERNS", m_qi_max_eager_multipatterns, + p.register_unsigned_param("qi_max_eager_multi_patterns", m_qi_max_eager_multipatterns, "Specify the number of extra multi patterns that are processed eagerly. By default, the prover use at most one multi-pattern eagerly when there is no unary pattern. This value should be smaller than or equal to PI_MAX_MULTI_PATTERNS"); - p.register_unsigned_param("QI_MAX_LAZY_MULTI_PATTERN_MATCHING", m_qi_max_lazy_multipattern_matching, "Maximum number of rounds of matching in a branch for delayed multipatterns. A multipattern is delayed based on the value of QI_MAX_EAGER_MULTI_PATTERNS"); - p.register_string_param("QI_COST", m_qi_cost, "The cost function for quantifier instantiation"); - p.register_string_param("QI_NEW_GEN", m_qi_new_gen, "The function for calculating the generation of newly constructed terms"); - p.register_double_param("QI_EAGER_THRESHOLD", m_qi_eager_threshold, "Threshold for eager quantifier instantiation"); - p.register_double_param("QI_LAZY_THRESHOLD", m_qi_lazy_threshold, "Threshold for lazy quantifier instantiation"); - p.register_bool_param("QI_PROFILE", m_qi_profile); - p.register_unsigned_param("QI_PROFILE_FREQ", m_qi_profile_freq); - p.register_int_param("QI_QUICK_CHECKER", 0, 2, reinterpret_cast(m_qi_quick_checker), "0 - do not use (cheap) model checker, 1 - instantiate instances unsatisfied by current model, 2 - 1 + instantiate instances not satisfied by current model"); - p.register_bool_param("QI_LAZY_QUICK_CHECKER", m_qi_lazy_quick_checker); - p.register_bool_param("QI_PROMOTE_UNSAT", m_qi_promote_unsat); - p.register_unsigned_param("QI_MAX_INSTANCES", m_qi_max_instances); - p.register_bool_param("QI_LAZY_INSTANTIATION", m_qi_lazy_instantiation); - p.register_bool_param("QI_CONSERVATIVE_FINAL_CHECK", m_qi_conservative_final_check); + p.register_unsigned_param("qi_max_lazy_multi_pattern_matching", m_qi_max_lazy_multipattern_matching, "Maximum number of rounds of matching in a branch for delayed multipatterns. A multipattern is delayed based on the value of QI_MAX_EAGER_MULTI_PATTERNS"); + p.register_string_param("qi_cost", m_qi_cost, "The cost function for quantifier instantiation"); + p.register_string_param("qi_new_gen", m_qi_new_gen, "The function for calculating the generation of newly constructed terms"); + p.register_double_param("qi_eager_threshold", m_qi_eager_threshold, "Threshold for eager quantifier instantiation"); + p.register_double_param("qi_lazy_threshold", m_qi_lazy_threshold, "Threshold for lazy quantifier instantiation"); + p.register_bool_param("qi_profile", m_qi_profile); + p.register_unsigned_param("qi_profile_freq", m_qi_profile_freq); + p.register_int_param("qi_quick_checker", 0, 2, reinterpret_cast(m_qi_quick_checker), "0 - do not use (cheap) model checker, 1 - instantiate instances unsatisfied by current model, 2 - 1 + instantiate instances not satisfied by current model"); + p.register_bool_param("qi_lazy_quick_checker", m_qi_lazy_quick_checker); + p.register_bool_param("qi_promote_unsat", m_qi_promote_unsat); + p.register_unsigned_param("qi_max_instances", m_qi_max_instances); + p.register_bool_param("qi_lazy_instantiation", m_qi_lazy_instantiation); + p.register_bool_param("qi_conservative_final_check", m_qi_conservative_final_check); - p.register_bool_param("MBQI", m_mbqi, "Model Based Quantifier Instantiation (MBQI)"); - p.register_unsigned_param("MBQI_MAX_CEXS", m_mbqi_max_cexs, "Initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation", true); - p.register_unsigned_param("MBQI_MAX_CEXS_INCR", m_mbqi_max_cexs_incr, "Increment for MBQI_MAX_CEXS, the increment is performed after each round of MBQI", true); - p.register_unsigned_param("MBQI_MAX_ITERATIONS", m_mbqi_max_iterations, "Maximum number of rounds of MBQI", true); - p.register_bool_param("MBQI_TRACE", m_mbqi_trace, "Generate tracing messages for Model Based Quantifier Instantiation (MBQI). It will display a message before every round of MBQI, and the quantifiers that were not satisfied.", true); - p.register_unsigned_param("MBQI_FORCE_TEMPLATE", m_mbqi_force_template, "Some quantifiers can be used as templates for building interpretations for functions. Z3 uses heuristics to decide whether a quantifier will be used as a template or not. Quantifiers with weight >= MBQI_FORCE_TEMPLATE are forced to be used as a template", true); + p.register_bool_param("mbqi", m_mbqi, "Model Based Quantifier Instantiation (MBQI)"); + p.register_unsigned_param("mbqi_max_cexs", m_mbqi_max_cexs, "Initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation", true); + p.register_unsigned_param("mbqi_max_cexs_incr", m_mbqi_max_cexs_incr, "Increment for MBQI_MAX_CEXS, the increment is performed after each round of MBQI", true); + p.register_unsigned_param("mbqi_max_iterations", m_mbqi_max_iterations, "Maximum number of rounds of MBQI", true); + p.register_bool_param("mbqi_trace", m_mbqi_trace, "Generate tracing messages for Model Based Quantifier Instantiation (MBQI). It will display a message before every round of MBQI, and the quantifiers that were not satisfied.", true); + p.register_unsigned_param("mbqi_force_template", m_mbqi_force_template, "Some quantifiers can be used as templates for building interpretations for functions. Z3 uses heuristics to decide whether a quantifier will be used as a template or not. Quantifiers with weight >= MBQI_FORCE_TEMPLATE are forced to be used as a template", true); - p.register_bool_param("INST_GEN", m_instgen, "Enable Instantiation Generation solver (disables other quantifier reasoning)", false); + p.register_bool_param("inst_gen", m_instgen, "Enable Instantiation Generation solver (disables other quantifier reasoning)", false); } }; diff --git a/src/front_end_params/smt_params.cpp b/src/front_end_params/smt_params.cpp index 0c4a0c844..14db6020a 100644 --- a/src/front_end_params/smt_params.cpp +++ b/src/front_end_params/smt_params.cpp @@ -27,82 +27,82 @@ void smt_params::register_params(ini_params & p) { theory_bv_params::register_params(p); theory_datatype_params::register_params(p); - p.register_bool_param("CHECK_PROOF", m_check_proof); - p.register_bool_param("DISPLAY_PROOF", m_display_proof); - p.register_bool_param("DISPLAY_DOT_PROOF", m_display_dot_proof); - p.register_bool_param("DISPLAY_UNSAT_CORE", m_display_unsat_core); - p.register_bool_param("INTERNALIZER_NNF", m_internalizer_nnf); - p.register_bool_param("EQ_PROPAGATION", m_eq_propagation); - p.register_bool_param("BIN_CLAUSES", m_binary_clause_opt); - p.register_unsigned_param("RELEVANCY", m_relevancy_lvl, "relevancy propagation heuristic: 0 - disabled, 1 - relevancy is tracked by only affects quantifier instantiation, 2 - relevancy is tracked, and an atom is only asserted if it is relevant", true); - p.register_bool_param("RELEVANCY_LEMMA", m_relevancy_lemma, "true if lemmas are used to propagate relevancy"); - p.register_unsigned_param("RANDOM_SEED", m_random_seed, "random seed for Z3"); - p.register_percentage_param("RANDOM_CASE_SPLIT_FREQ", m_random_var_freq, "frequency of random case splits"); - p.register_int_param("PHASE_SELECTION", 0, 6, reinterpret_cast(m_phase_selection), "phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences"); - p.register_bool_param("MINIMIZE_LEMMAS", m_minimize_lemmas, "enable/disable lemma minimization algorithm"); - p.register_unsigned_param("MAX_CONFLICTS", m_max_conflicts, "maximum number of conflicts"); + p.register_bool_param("check_proof", m_check_proof); + p.register_bool_param("display_proof", m_display_proof); + p.register_bool_param("display_dot_proof", m_display_dot_proof); + p.register_bool_param("display_unsat_core", m_display_unsat_core); + p.register_bool_param("internalizer_nnf", m_internalizer_nnf); + p.register_bool_param("eq_propagation", m_eq_propagation); + p.register_bool_param("bin_clauses", m_binary_clause_opt); + p.register_unsigned_param("relevancy", m_relevancy_lvl, "relevancy propagation heuristic: 0 - disabled, 1 - relevancy is tracked by only affects quantifier instantiation, 2 - relevancy is tracked, and an atom is only asserted if it is relevant", true); + p.register_bool_param("relevancy_lemma", m_relevancy_lemma, "true if lemmas are used to propagate relevancy"); + p.register_unsigned_param("random_seed", m_random_seed, "random seed for Z3"); + p.register_percentage_param("random_case_split_freq", m_random_var_freq, "frequency of random case splits"); + p.register_int_param("phase_selection", 0, 6, reinterpret_cast(m_phase_selection), "phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences"); + p.register_bool_param("minimize_lemmas", m_minimize_lemmas, "enable/disable lemma minimization algorithm"); + p.register_unsigned_param("max_conflicts", m_max_conflicts, "maximum number of conflicts"); - p.register_unsigned_param("RECENT_LEMMA_THRESHOLD", m_recent_lemmas_size); - p.register_unsigned_param("TICK", m_tick); + p.register_unsigned_param("recent_lemma_threshold", m_recent_lemmas_size); + p.register_unsigned_param("tick", m_tick); PRIVATE_PARAMS({ - p.register_bool_param("THEORY_RESOLVE", m_theory_resolve, "Apply theory resolution to produce auxiliary conflict clauses", true); + p.register_bool_param("theory_resolve", m_theory_resolve, "Apply theory resolution to produce auxiliary conflict clauses", true); }); - p.register_int_param("RESTART_STRATEGY", 0, 4, reinterpret_cast(m_restart_strategy), "0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic"); - p.register_unsigned_param("RESTART_INITIAL", m_restart_initial, + p.register_int_param("restart_strategy", 0, 4, reinterpret_cast(m_restart_strategy), "0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic"); + p.register_unsigned_param("restart_initial", m_restart_initial, "inital restart frequency in number of conflicts, it is also the unit for the luby sequence"); - p.register_double_param("RESTART_FACTOR", m_restart_factor, "when using geometric (or inner-outer-geometric) progression of restarts, it specifies the constant used to multiply the currect restart threshold"); - p.register_bool_param("RESTART_ADAPTIVE", m_restart_adaptive, "disable restarts based on the search 'agility'"); - p.register_percentage_param("RESTART_AGILITY_THRESHOLD", m_restart_agility_threshold); + p.register_double_param("restart_factor", m_restart_factor, "when using geometric (or inner-outer-geometric) progression of restarts, it specifies the constant used to multiply the currect restart threshold"); + p.register_bool_param("restart_adaptive", m_restart_adaptive, "disable restarts based on the search 'agility'"); + p.register_percentage_param("restart_agility_threshold", m_restart_agility_threshold); - p.register_int_param("LEMMA_GC_STRATEGY", 0, 2, reinterpret_cast(m_lemma_gc_strategy), "0 - fixed, 1 - geometric, 2 - at every restart"); - p.register_bool_param("LEMMA_GC_HALF", m_lemma_gc_half, "true for simple gc algorithm (delete approx. half of the clauses)"); - p.register_unsigned_param("LEMMA_GC_INITIAL", m_lemma_gc_initial, "lemma initial gc frequency (in number of conflicts), used by fixed or geometric strategies"); - p.register_double_param("LEMMA_GC_FACTOR", m_lemma_gc_factor, "used by geometric strategy"); - p.register_unsigned_param("LEMMA_GC_NEW_OLD_RATIO", m_new_old_ratio); - p.register_unsigned_param("LEMMA_GC_NEW_CLAUSE_ACTIVITY", m_new_clause_activity); - p.register_unsigned_param("LEMMA_GC_OLD_CLAUSE_ACTIVITY", m_old_clause_activity); - p.register_unsigned_param("LEMMA_GC_NEW_CLAUSE_RELEVANCY", m_new_clause_relevancy); - p.register_unsigned_param("LEMMA_GC_OLD_CLAUSE_RELEVANCY", m_old_clause_activity); + p.register_int_param("lemma_gc_strategy", 0, 2, reinterpret_cast(m_lemma_gc_strategy), "0 - fixed, 1 - geometric, 2 - at every restart"); + p.register_bool_param("lemma_gc_half", m_lemma_gc_half, "true for simple gc algorithm (delete approx. half of the clauses)"); + p.register_unsigned_param("lemma_gc_initial", m_lemma_gc_initial, "lemma initial gc frequency (in number of conflicts), used by fixed or geometric strategies"); + p.register_double_param("lemma_gc_factor", m_lemma_gc_factor, "used by geometric strategy"); + p.register_unsigned_param("lemma_gc_new_old_ratio", m_new_old_ratio); + p.register_unsigned_param("lemma_gc_new_clause_activity", m_new_clause_activity); + p.register_unsigned_param("lemma_gc_old_clause_activity", m_old_clause_activity); + p.register_unsigned_param("lemma_gc_new_clause_relevancy", m_new_clause_relevancy); + p.register_unsigned_param("lemma_gc_old_clause_relevancy", m_old_clause_activity); - p.register_bool_param("SIMPLIFY_CLAUSES", m_simplify_clauses); + p.register_bool_param("simplify_clauses", m_simplify_clauses); - p.register_int_param("RANDOM_INITIAL_ACTIVITY", 0, 2, reinterpret_cast(m_random_initial_activity)); + p.register_int_param("random_initial_activity", 0, 2, reinterpret_cast(m_random_initial_activity)); PRIVATE_PARAMS({ - p.register_double_param("INV_DECAY", m_inv_decay); - p.register_unsigned_param("PHASE_CACHING_ON_DURATION", m_phase_caching_on); - p.register_unsigned_param("PHASE_CACHING_OFF_DURATION", m_phase_caching_off); + p.register_double_param("inv_decay", m_inv_decay); + p.register_unsigned_param("phase_caching_on_duration", m_phase_caching_on); + p.register_unsigned_param("phase_caching_off_duration", m_phase_caching_off); }); - p.register_bool_param("SMTLIB_DUMP_LEMMAS", m_smtlib_dump_lemmas); - p.register_string_param("SMTLIB_LOGIC", m_smtlib_logic, "Name used for the :logic field when generating SMT-LIB benchmarks"); - p.register_bool_param("DISPLAY_FEATURES", m_display_features); + p.register_bool_param("smtlib_dump_lemmas", m_smtlib_dump_lemmas); + p.register_string_param("smtlib_logic", m_smtlib_logic, "Name used for the :logic field when generating SMT-LIB benchmarks"); + p.register_bool_param("display_features", m_display_features); - p.register_bool_param("NEW_CORE2TH_EQ", m_new_core2th_eq); - p.register_bool_param("EMATCHING", m_ematching, "E-Matching based quantifier instantiation"); + p.register_bool_param("new_core2th_eq", m_new_core2th_eq); + p.register_bool_param("ematching", m_ematching, "E-Matching based quantifier instantiation"); - p.register_bool_param("PROFILE_RES_SUB", m_profile_res_sub); + p.register_bool_param("profile_res_sub", m_profile_res_sub); #ifndef _EXTERNAL_RELEASE - p.register_bool_param("DISPLAY_BOOL_VAR2EXPR", m_display_bool_var2expr); - p.register_bool_param("DISPLAY_LL_BOOL_VAR2EXPR", m_display_ll_bool_var2expr); - p.register_bool_param("ABORT_AFTER_PREPROC", m_abort_after_preproc, "abort after preprocessing step, this flag is only useful for debugging purposes"); - p.register_bool_param("DISPLAY_INSTALLED_THEORIES", m_display_installed_theories, "display theories installed at smt::context", true); + p.register_bool_param("display_bool_var2expr", m_display_bool_var2expr); + p.register_bool_param("display_ll_bool_var2expr", m_display_ll_bool_var2expr); + p.register_bool_param("abort_after_preproc", m_abort_after_preproc, "abort after preprocessing step, this flag is only useful for debugging purposes"); + p.register_bool_param("display_installed_theories", m_display_installed_theories, "display theories installed at smt::context", true); #endif - p.register_int_param("CASE_SPLIT", 0, 5, reinterpret_cast(m_case_split_strategy), "0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal"); - p.register_unsigned_param("REL_CASE_SPLIT_ORDER", 0, 2, m_rel_case_split_order, "structural (relevancy) splitting order: 0 - left-to-right (default), 1 - random, 2 - right-to-left"); - p.register_bool_param("LOOKAHEAD_DISEQ", m_lookahead_diseq); + p.register_int_param("case_split", 0, 5, reinterpret_cast(m_case_split_strategy), "0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal"); + p.register_unsigned_param("rel_case_split_order", 0, 2, m_rel_case_split_order, "structural (relevancy) splitting order: 0 - left-to-right (default), 1 - random, 2 - right-to-left"); + p.register_bool_param("lookahead_diseq", m_lookahead_diseq); - p.register_bool_param("DELAY_UNITS", m_delay_units); - p.register_unsigned_param("DELAY_UNITS_THRESHOLD", m_delay_units_threshold); + p.register_bool_param("delay_units", m_delay_units); + p.register_unsigned_param("delay_units_threshold", m_delay_units_threshold); - p.register_bool_param("MODEL", m_model, "enable/disable model construction", true); - p.register_bool_param("MODEL_VALIDATE", m_model_validate, "validate the model", true); - p.register_bool_param("MODEL_ON_TIMEOUT", m_model_on_timeout, "after hitting soft-timeout or memory high watermark, generate a candidate model", true); - p.register_bool_param("MODEL_ON_FINAL_CHECK", m_model_on_final_check, "display candidate model (in the standard output) whenever Z3 hits a final check", true); + p.register_bool_param("model", m_model, "enable/disable model construction", true); + p.register_bool_param("model_validate", m_model_validate, "validate the model", true); + p.register_bool_param("model_on_timeout", m_model_on_timeout, "after hitting soft-timeout or memory high watermark, generate a candidate model", true); + p.register_bool_param("model_on_final_check", m_model_on_final_check, "display candidate model (in the standard output) whenever Z3 hits a final check", true); - p.register_unsigned_param("PROGRESS_SAMPLING_FREQ", m_progress_sampling_freq, "frequency for progress output in miliseconds"); + p.register_unsigned_param("progress_sampling_freq", m_progress_sampling_freq, "frequency for progress output in miliseconds"); } diff --git a/src/front_end_params/theory_arith_params.cpp b/src/front_end_params/theory_arith_params.cpp index 2d77b6e73..49a654dbf 100644 --- a/src/front_end_params/theory_arith_params.cpp +++ b/src/front_end_params/theory_arith_params.cpp @@ -21,56 +21,56 @@ Revision History: void theory_arith_params::register_params(ini_params & p) { #ifdef _EXTERNAL_RELEASE - p.register_int_param("ARITH_SOLVER", 0, 3, reinterpret_cast(m_arith_mode), "select arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination"); + p.register_int_param("arith_solver", 0, 3, reinterpret_cast(m_arith_mode), "select arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination"); #else - p.register_int_param("ARITH_SOLVER", 0, 4, reinterpret_cast(m_arith_mode), "select arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination, 4 - model guided arith_solver"); + p.register_int_param("arith_solver", 0, 4, reinterpret_cast(m_arith_mode), "select arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination, 4 - model guided arith_solver"); #endif - p.register_bool_param("ARITH_FORCE_SIMPLEX", m_arith_auto_config_simplex, "force Z3 to use simplex solver."); - p.register_unsigned_param("ARITH_BLANDS_RULE_THRESHOLD", m_arith_blands_rule_threshold); - p.register_bool_param("ARITH_PROPAGATE_EQS", m_arith_propagate_eqs); - p.register_int_param("ARITH_PROPAGATION_MODE", 0, 2, reinterpret_cast(m_arith_bound_prop)); - p.register_bool_param("ARITH_STRONGER_LEMMAS", m_arith_stronger_lemmas); - p.register_bool_param("ARITH_SKIP_BIG_COEFFS", m_arith_skip_rows_with_big_coeffs); - p.register_unsigned_param("ARITH_MAX_LEMMA_SIZE", m_arith_max_lemma_size); - p.register_unsigned_param("ARITH_SMALL_LEMMA_SIZE", m_arith_small_lemma_size); - p.register_bool_param("ARITH_REFLECT", m_arith_reflect); - p.register_bool_param("ARITH_IGNORE_INT", m_arith_ignore_int); - p.register_unsigned_param("ARITH_LAZY_PIVOTING", m_arith_lazy_pivoting_lvl); - p.register_unsigned_param("ARITH_RANDOM_SEED", m_arith_random_seed); - p.register_bool_param("ARITH_RANDOM_INITIAL_VALUE", m_arith_random_initial_value); - p.register_int_param("ARITH_RANDOM_LOWER", m_arith_random_lower); - p.register_int_param("ARITH_RANDOM_UPPER", m_arith_random_upper); - p.register_bool_param("ARITH_ADAPTIVE", m_arith_adaptive); - p.register_double_param("ARITH_ADAPTIVE_ASSERTION_THRESHOLD", m_arith_adaptive_assertion_threshold, "Delay arithmetic atoms if the num-arith-conflicts/total-conflicts < threshold"); - p.register_double_param("ARITH_ADAPTIVE_PROPAGATION_THRESHOLD", m_arith_adaptive_propagation_threshold, "Disable arithmetic theory propagation if the num-arith-conflicts/total-conflicts < threshold"); - p.register_bool_param("ARITH_DUMP_LEMMAS", m_arith_dump_lemmas); - p.register_bool_param("ARITH_EAGER_EQ_AXIOMS", m_arith_eager_eq_axioms); - p.register_unsigned_param("ARITH_BRANCH_CUT_RATIO", m_arith_branch_cut_ratio); + p.register_bool_param("arith_force_simplex", m_arith_auto_config_simplex, "force Z3 to use simplex solver."); + p.register_unsigned_param("arith_blands_rule_threshold", m_arith_blands_rule_threshold); + p.register_bool_param("arith_propagate_eqs", m_arith_propagate_eqs); + p.register_int_param("arith_propagation_mode", 0, 2, reinterpret_cast(m_arith_bound_prop)); + p.register_bool_param("arith_stronger_lemmas", m_arith_stronger_lemmas); + p.register_bool_param("arith_skip_big_coeffs", m_arith_skip_rows_with_big_coeffs); + p.register_unsigned_param("arith_max_lemma_size", m_arith_max_lemma_size); + p.register_unsigned_param("arith_small_lemma_size", m_arith_small_lemma_size); + p.register_bool_param("arith_reflect", m_arith_reflect); + p.register_bool_param("arith_ignore_int", m_arith_ignore_int); + p.register_unsigned_param("arith_lazy_pivoting", m_arith_lazy_pivoting_lvl); + p.register_unsigned_param("arith_random_seed", m_arith_random_seed); + p.register_bool_param("arith_random_initial_value", m_arith_random_initial_value); + p.register_int_param("arith_random_lower", m_arith_random_lower); + p.register_int_param("arith_random_upper", m_arith_random_upper); + p.register_bool_param("arith_adaptive", m_arith_adaptive); + p.register_double_param("arith_adaptive_assertion_threshold", m_arith_adaptive_assertion_threshold, "Delay arithmetic atoms if the num-arith-conflicts/total-conflicts < threshold"); + p.register_double_param("arith_adaptive_propagation_threshold", m_arith_adaptive_propagation_threshold, "Disable arithmetic theory propagation if the num-arith-conflicts/total-conflicts < threshold"); + p.register_bool_param("arith_dump_lemmas", m_arith_dump_lemmas); + p.register_bool_param("arith_eager_eq_axioms", m_arith_eager_eq_axioms); + p.register_unsigned_param("arith_branch_cut_ratio", m_arith_branch_cut_ratio); - p.register_bool_param("ARITH_ADD_BINARY_BOUNDS", m_arith_add_binary_bounds); - p.register_unsigned_param("ARITH_PROP_STRATEGY", 0, 1, reinterpret_cast(m_arith_propagation_strategy), "Propagation strategy: 0 - use agility measures based on ration of theory conflicts, 1 - propagate proportional to ratio of theory conflicts (default)"); + p.register_bool_param("arith_add_binary_bounds", m_arith_add_binary_bounds); + p.register_unsigned_param("arith_prop_strategy", 0, 1, reinterpret_cast(m_arith_propagation_strategy), "Propagation strategy: 0 - use agility measures based on ration of theory conflicts, 1 - propagate proportional to ratio of theory conflicts (default)"); - p.register_bool_param("ARITH_EQ_BOUNDS", m_arith_eq_bounds); - p.register_bool_param("ARITH_LAZY_ADAPTER", m_arith_lazy_adapter); - p.register_bool_param("ARITH_GCD_TEST", m_arith_gcd_test); - p.register_bool_param("ARITH_EAGER_GCD", m_arith_eager_gcd); - p.register_bool_param("ARITH_ADAPTIVE_GCD", m_arith_adaptive_gcd); - p.register_unsigned_param("ARITH_PROPAGATION_THRESHOLD", m_arith_propagation_threshold); + p.register_bool_param("arith_eq_bounds", m_arith_eq_bounds); + p.register_bool_param("arith_lazy_adapter", m_arith_lazy_adapter); + p.register_bool_param("arith_gcd_test", m_arith_gcd_test); + p.register_bool_param("arith_eager_gcd", m_arith_eager_gcd); + p.register_bool_param("arith_adaptive_gcd", m_arith_adaptive_gcd); + p.register_unsigned_param("arith_propagation_threshold", m_arith_propagation_threshold); - p.register_bool_param("NL_ARITH", m_nl_arith, "enable/disable non linear arithmetic support. This option is ignored when ARITH_SOLVER != 2."); - p.register_bool_param("NL_ARITH_GB", m_nl_arith_gb, "enable/disable Grobner Basis computation. This option is ignored when NL_ARITH=false"); - p.register_bool_param("NL_ARITH_GB_EQS", m_nl_arith_gb_eqs, "enable/disable equations in the Grobner Basis to be copied to the Simplex tableau."); - p.register_bool_param("NL_ARITH_GB_PERTURBATE", m_nl_arith_gb_perturbate, "enable/disable perturbation of the variable order in GB when searching for new polynomials."); - p.register_unsigned_param("NL_ARITH_GB_THRESHOLD", m_nl_arith_gb_threshold, "Grobner basis computation can be very expensive. This is a threshold on the number of new equalities that can be generated."); - p.register_bool_param("NL_ARITH_BRANCHING", m_nl_arith_branching, "enable/disable branching on integer variables in non linear clusters"); - p.register_unsigned_param("NL_ARITH_ROUNDS", m_nl_arith_rounds, "threshold for number of (nested) final checks for non linear arithmetic."); - p.register_unsigned_param("NL_ARITH_MAX_DEGREE", m_nl_arith_max_degree, "max degree for internalizing new monomials."); + p.register_bool_param("nl_arith", m_nl_arith, "enable/disable non linear arithmetic support. This option is ignored when ARITH_SOLVER != 2."); + p.register_bool_param("nl_arith_gb", m_nl_arith_gb, "enable/disable Grobner Basis computation. This option is ignored when NL_ARITH=false"); + p.register_bool_param("nl_arith_gb_eqs", m_nl_arith_gb_eqs, "enable/disable equations in the Grobner Basis to be copied to the Simplex tableau."); + p.register_bool_param("nl_arith_gb_perturbate", m_nl_arith_gb_perturbate, "enable/disable perturbation of the variable order in GB when searching for new polynomials."); + p.register_unsigned_param("nl_arith_gb_threshold", m_nl_arith_gb_threshold, "Grobner basis computation can be very expensive. This is a threshold on the number of new equalities that can be generated."); + p.register_bool_param("nl_arith_branching", m_nl_arith_branching, "enable/disable branching on integer variables in non linear clusters"); + p.register_unsigned_param("nl_arith_rounds", m_nl_arith_rounds, "threshold for number of (nested) final checks for non linear arithmetic."); + p.register_unsigned_param("nl_arith_max_degree", m_nl_arith_max_degree, "max degree for internalizing new monomials."); PRIVATE_PARAMS({ - p.register_bool_param("ARITH_FIXNUM", m_arith_fixnum); - p.register_bool_param("ARITH_INT_ONLY", m_arith_int_only); - p.register_bool_param("ARITH_ENUM_CONST_MOD", m_arith_enum_const_mod, "Create axioms for the finite set of equalities for (mod x k) where k is a positive numeral constant"); - p.register_bool_param("ARITH_INT_EQ_BRANCHING", m_arith_int_eq_branching, "Determine branch predicates based on integer equation solving"); + p.register_bool_param("arith_fixnum", m_arith_fixnum); + p.register_bool_param("arith_int_only", m_arith_int_only); + p.register_bool_param("arith_enum_const_mod", m_arith_enum_const_mod, "Create axioms for the finite set of equalities for (mod x k) where k is a positive numeral constant"); + p.register_bool_param("arith_int_eq_branching", m_arith_int_eq_branching, "Determine branch predicates based on integer equation solving"); }); - p.register_bool_param("ARITH_EUCLIDEAN_SOLVER", m_arith_euclidean_solver, ""); + p.register_bool_param("arith_euclidean_solver", m_arith_euclidean_solver, ""); } diff --git a/src/front_end_params/theory_array_params.h b/src/front_end_params/theory_array_params.h index 9e93fefbe..3d45ebcf5 100644 --- a/src/front_end_params/theory_array_params.h +++ b/src/front_end_params/theory_array_params.h @@ -56,17 +56,17 @@ struct theory_array_params { } void register_params(ini_params & p) { - p.register_int_param("ARRAY_SOLVER", 0, 3, reinterpret_cast(m_array_mode), "0 - no array, 1 - simple, 2 - model based, 3 - full"); - p.register_bool_param("ARRAY_WEAK", m_array_weak); - p.register_bool_param("ARRAY_EXTENSIONAL", m_array_extensional); - p.register_unsigned_param("ARRAY_LAZINESS", m_array_laziness); - p.register_bool_param("ARRAY_DELAY_EXP_AXIOM", m_array_delay_exp_axiom); - p.register_bool_param("ARRAY_CG", m_array_cg); - p.register_bool_param("ARRAY_ALWAYS_PROP_UPWARD", m_array_always_prop_upward, + p.register_int_param("array_solver", 0, 3, reinterpret_cast(m_array_mode), "0 - no array, 1 - simple, 2 - model based, 3 - full"); + p.register_bool_param("array_weak", m_array_weak); + p.register_bool_param("array_extensional", m_array_extensional); + p.register_unsigned_param("array_laziness", m_array_laziness); + p.register_bool_param("array_delay_exp_axiom", m_array_delay_exp_axiom); + p.register_bool_param("array_cg", m_array_cg); + p.register_bool_param("array_always_prop_upward", m_array_always_prop_upward, "Disable the built-in filter upwards propagation"); - p.register_bool_param("ARRAY_LAZY_IEQ", m_array_lazy_ieq); - p.register_unsigned_param("ARRAY_LAZY_IEQ_DELAY", m_array_lazy_ieq_delay); - p.register_bool_param("ARRAY_CANONIZE", m_array_canonize_simplify, + p.register_bool_param("array_lazy_ieq", m_array_lazy_ieq); + p.register_unsigned_param("array_lazy_ieq_delay", m_array_lazy_ieq_delay); + p.register_bool_param("array_canonize", m_array_canonize_simplify, "Normalize arrays into normal form during simplification"); } }; diff --git a/src/front_end_params/theory_bv_params.h b/src/front_end_params/theory_bv_params.h index 38e1e263f..6bf5ac868 100644 --- a/src/front_end_params/theory_bv_params.h +++ b/src/front_end_params/theory_bv_params.h @@ -41,12 +41,12 @@ struct theory_bv_params { m_bv_blast_max_size(INT_MAX), m_bv_enable_int2bv2int(false) {} void register_params(ini_params & p) { - p.register_int_param("BV_SOLVER", 0, 2, reinterpret_cast(m_bv_mode), "0 - no bv, 1 - simple"); - p.register_unsigned_param("BV_BLAST_MAX_SIZE", m_bv_blast_max_size, "Maximal size for bit-vectors to blast"); - p.register_bool_param("BV_REFLECT", m_bv_reflect); - p.register_bool_param("BV_LAZY_LE", m_bv_lazy_le); - p.register_bool_param("BV_CC", m_bv_cc, "enable congruence closure for BV operators"); - p.register_bool_param("BV_ENABLE_INT2BV_PROPAGATION", m_bv_enable_int2bv2int, + p.register_int_param("bv_solver", 0, 2, reinterpret_cast(m_bv_mode), "0 - no bv, 1 - simple"); + p.register_unsigned_param("bv_blast_max_size", m_bv_blast_max_size, "Maximal size for bit-vectors to blast"); + p.register_bool_param("bv_reflect", m_bv_reflect); + p.register_bool_param("bv_lazy_le", m_bv_lazy_le); + p.register_bool_param("bv_cc", m_bv_cc, "enable congruence closure for BV operators"); + p.register_bool_param("bv_enable_int2bv_propagation", m_bv_enable_int2bv2int, "enable full (potentially expensive) propagation for int2bv and bv2int"); } }; diff --git a/src/front_end_params/theory_datatype_params.h b/src/front_end_params/theory_datatype_params.h index 000c4da07..33b2c1814 100644 --- a/src/front_end_params/theory_datatype_params.h +++ b/src/front_end_params/theory_datatype_params.h @@ -29,7 +29,7 @@ struct theory_datatype_params { } void register_params(ini_params & p) { - p.register_unsigned_param("DT_LAZY_SPLITS", m_dt_lazy_splits, "How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy"); + p.register_unsigned_param("dt_lazy_splits", m_dt_lazy_splits, "How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy"); } }; diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp index f7de4054c..c35e0d368 100644 --- a/src/math/polynomial/algebraic_numbers.cpp +++ b/src/math/polynomial/algebraic_numbers.cpp @@ -57,12 +57,12 @@ namespace algebraic_numbers { typedef upolynomial::factors factors; void manager::get_param_descrs(param_descrs & r) { - r.insert(":algebraic-zero-accuracy", CPK_UINT, "(default: 0) one of the most time-consuming operations in the real algebraic number module is determining the sign of a polynomial evaluated at a sample point with non-rational algebraic number values. Let k be the value of this option. If k is 0, Z3 uses precise computation. Otherwise, the result of a polynomial evaluation is considered to be 0 if Z3 can show it is inside the interval (-1/2^k, 1/2^k)."); - r.insert(":algebraic-min-mag", CPK_UINT, "(default: 16) Z3 represents algebraic numbers using a (square-free) polynomial p and an isolating interval (which contains one and only one root of p). This interval may be refined during the computations. This parameter specifies whether to cache the value of a refined interval or not. It says the minimal size of an interval for caching purposes is 1/2^16"); - r.insert(":algebraic-factor", CPK_BOOL, "(default: true) use polynomial factorization to simplify polynomials representing algebraic numbers."); - r.insert(":algebraic-factor-max-prime", CPK_UINT, "(default: 31), parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter limits the maximum prime number p to be used in the first step."); - r.insert(":algebraic-factor-num-primes", CPK_UINT, "(default: 1), parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. The search space may be reduced by factoring the polynomial in different GF(p)'s. This parameter specify the maximum number of finite factorizations to be considered, before lifiting and searching."); - r.insert(":algebraic-factor-search-size", CPK_UINT, "(default: 5000), parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter can be used to limit the search space."); + r.insert("zero_accuracy", CPK_UINT, "(default: 0) one of the most time-consuming operations in the real algebraic number module is determining the sign of a polynomial evaluated at a sample point with non-rational algebraic number values. Let k be the value of this option. If k is 0, Z3 uses precise computation. Otherwise, the result of a polynomial evaluation is considered to be 0 if Z3 can show it is inside the interval (-1/2^k, 1/2^k)."); + r.insert("min_mag", CPK_UINT, "(default: 16) Z3 represents algebraic numbers using a (square-free) polynomial p and an isolating interval (which contains one and only one root of p). This interval may be refined during the computations. This parameter specifies whether to cache the value of a refined interval or not. It says the minimal size of an interval for caching purposes is 1/2^16"); + r.insert("factor", CPK_BOOL, "(default: true) use polynomial factorization to simplify polynomials representing algebraic numbers."); + r.insert("factor_max_prime", CPK_UINT, "(default: 31), parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter limits the maximum prime number p to be used in the first step."); + r.insert("factor_num_primes", CPK_UINT, "(default: 1), parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. The search space may be reduced by factoring the polynomial in different GF(p)'s. This parameter specify the maximum number of finite factorizations to be considered, before lifiting and searching."); + r.insert("factor_search_size", CPK_UINT, "(default: 5000), parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter can be used to limit the search space."); } struct manager::imp { @@ -157,12 +157,12 @@ namespace algebraic_numbers { } void updt_params(params_ref const & p) { - m_min_magnitude = -static_cast(p.get_uint(":algebraic-min-mag", 16)); - m_factor = p.get_bool(":algebraic-factor", true); // use polynomial factorization - m_factor_params.m_max_p = p.get_uint(":algebraic-factor-max-prime", 31); - m_factor_params.m_p_trials = p.get_uint(":algebraic-factor-num-primes", 1); - m_factor_params.m_max_search_size = p.get_uint(":algebraic-factor-max-search-size", 5000); - m_zero_accuracy = -static_cast(p.get_uint(":algebraic-zero-accuracy", 0)); + m_min_magnitude = -static_cast(p.get_uint("min_mag", 16)); + m_factor = p.get_bool("factor", true); // use polynomial factorization + m_factor_params.m_max_p = p.get_uint("factor_max_prime", 31); + m_factor_params.m_p_trials = p.get_uint("factor_num_primes", 1); + m_factor_params.m_max_search_size = p.get_uint("factor_max_search_size", 5000); + m_zero_accuracy = -static_cast(p.get_uint("zero_accuracy", 0)); } unsynch_mpq_manager & qm() { diff --git a/src/math/polynomial/algebraic_numbers.h b/src/math/polynomial/algebraic_numbers.h index 4735a875b..0db3ee68c 100644 --- a/src/math/polynomial/algebraic_numbers.h +++ b/src/math/polynomial/algebraic_numbers.h @@ -60,6 +60,9 @@ namespace algebraic_numbers { manager(unsynch_mpq_manager & m, params_ref const & p = params_ref(), small_object_allocator * a = 0); ~manager(); + /* + REG_MODULE_PARAMS('algebraic', 'algebraic_numbers::manager::get_param_descrs') + */ static void get_param_descrs(param_descrs & r); static void collect_param_descrs(param_descrs & r) { get_param_descrs(r); } diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index 1b5c7965f..4e14c5661 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -50,15 +50,15 @@ namespace polynomial { } void factor_params::updt_params(params_ref const & p) { - m_max_p = p.get_uint(":factor-max-prime", UINT_MAX); - m_p_trials = p.get_uint(":factor-num-primes", 1); - m_max_search_size = p.get_uint(":factor-max-search-size", UINT_MAX); + m_max_p = p.get_uint("max_prime", UINT_MAX); + m_p_trials = p.get_uint("num_primes", 1); + m_max_search_size = p.get_uint("max_search_size", UINT_MAX); } void factor_params::get_param_descrs(param_descrs & r) { - r.insert(":factor-max-search-size", CPK_UINT, "(default: infty) Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter can be used to limit the search space."); - r.insert(":factor-max-prime", CPK_UINT, "(default: infty) Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter limits the maximum prime number p to be used in the first step."); - r.insert(":factor-num-primes", CPK_UINT, "(default: 1) Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. The search space may be reduced by factoring the polynomial in different GF(p)'s. This parameter specify the maximum number of finite factorizations to be considered, before lifiting and searching."); + r.insert("max_search_size", CPK_UINT, "(default: infty) Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter can be used to limit the search space."); + r.insert("max_prime", CPK_UINT, "(default: infty) Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter limits the maximum prime number p to be used in the first step."); + r.insert("num_primes", CPK_UINT, "(default: 1) Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. The search space may be reduced by factoring the polynomial in different GF(p)'s. This parameter specify the maximum number of finite factorizations to be considered, before lifiting and searching."); } typedef ptr_vector monomial_vector; diff --git a/src/math/polynomial/polynomial.h b/src/math/polynomial/polynomial.h index f6370e5fa..7cefe6f56 100644 --- a/src/math/polynomial/polynomial.h +++ b/src/math/polynomial/polynomial.h @@ -90,6 +90,9 @@ namespace polynomial { factor_params(); factor_params(unsigned max_p, unsigned p_trials, unsigned max_search_size); void updt_params(params_ref const & p); + /* + REG_MODULE_PARAMS('factor', polynomial::factor_params::get_param_descrs') + */ static void get_param_descrs(param_descrs & r); }; diff --git a/src/math/subpaving/subpaving_t_def.h b/src/math/subpaving/subpaving_t_def.h index 7c80de75c..c215ddf98 100644 --- a/src/math/subpaving/subpaving_t_def.h +++ b/src/math/subpaving/subpaving_t_def.h @@ -474,7 +474,7 @@ void context_t::del(interval & a) { template void context_t::updt_params(params_ref const & p) { - unsigned epsilon = p.get_uint(":epsilon", 20); + unsigned epsilon = p.get_uint("epsilon", 20); if (epsilon != 0) { nm().set(m_epsilon, static_cast(epsilon)); nm().inv(m_epsilon); @@ -485,18 +485,18 @@ void context_t::updt_params(params_ref const & p) { m_zero_epsilon = true; } - unsigned max_power = p.get_uint(":max-bound", 10); + unsigned max_power = p.get_uint("max_bound", 10); nm().set(m_max_bound, 10); nm().power(m_max_bound, max_power, m_max_bound); nm().set(m_minus_max_bound, m_max_bound); nm().neg(m_minus_max_bound); - m_max_depth = p.get_uint(":max-depth", 128); - m_max_nodes = p.get_uint(":max-nodes", 8192); + m_max_depth = p.get_uint("max_depth", 128); + m_max_nodes = p.get_uint("max_nodes", 8192); - m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX)); + m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); - unsigned prec = p.get_uint(":nth-root-precision", 8192); + unsigned prec = p.get_uint("nth_root_precision", 8192); if (prec == 0) prec = 1; nm().set(m_nth_root_prec, static_cast(prec)); @@ -505,20 +505,20 @@ void context_t::updt_params(params_ref const & p) { template void context_t::collect_param_descrs(param_descrs & d) { - d.insert(":max-nodes", CPK_UINT, "(default: 8192) maximum number of nodes in the subpaving tree."); - d.insert(":max-depth", CPK_UINT, "(default: 128) maximum depth of the subpaving tree."); - d.insert(":epsilon", CPK_UINT, "(default: 20) value k s.t. a new lower (upper) bound for x is propagated only new-lower(x) > lower(k) + 1/k * max(min(upper(x) - lower(x), |lower|), 1) (new-upper(x) < upper(x) - 1/k * max(min(upper(x) - lower(x), |lower|), 1)). If k = 0, then this restriction is ignored."); - d.insert(":max-bound", CPK_UINT, "(default 10) value k s.t. a new upper (lower) bound for x is propagated only if upper(x) > -10^k or lower(x) = -oo (lower(x) < 10^k or upper(x) = oo)"); - d.insert(":nth-root-precision", CPK_UINT, "(default 8192) value k s.t. 1/k is the precision for computing the nth root in the subpaving module."); + d.insert("max_nodes", CPK_UINT, "(default: 8192) maximum number of nodes in the subpaving tree."); + d.insert("max_depth", CPK_UINT, "(default: 128) maximum depth of the subpaving tree."); + d.insert("epsilon", CPK_UINT, "(default: 20) value k s.t. a new lower (upper) bound for x is propagated only new-lower(x) > lower(k) + 1/k * max(min(upper(x) - lower(x), |lower|), 1) (new-upper(x) < upper(x) - 1/k * max(min(upper(x) - lower(x), |lower|), 1)). If k = 0, then this restriction is ignored."); + d.insert("max_bound", CPK_UINT, "(default 10) value k s.t. a new upper (lower) bound for x is propagated only if upper(x) > -10^k or lower(x) = -oo (lower(x) < 10^k or upper(x) = oo)"); + d.insert("nth_root_precision", CPK_UINT, "(default 8192) value k s.t. 1/k is the precision for computing the nth root in the subpaving module."); } template void context_t::display_params(std::ostream & out) const { - out << ":max-nodes " << m_max_nodes << "\n"; - out << ":max-depth " << m_max_depth << "\n"; - out << ":epsilon " << nm().to_rational_string(m_epsilon) << "\n"; - out << ":max-bound " << nm().to_rational_string(m_max_bound) << "\n"; - out << ":max-memory " << m_max_memory << "\n"; + out << "max_nodes " << m_max_nodes << "\n"; + out << "max_depth " << m_max_depth << "\n"; + out << "epsilon " << nm().to_rational_string(m_epsilon) << "\n"; + out << "max_bound " << nm().to_rational_string(m_max_bound) << "\n"; + out << "max_memory " << m_max_memory << "\n"; } template diff --git a/src/math/subpaving/tactic/subpaving_tactic.cpp b/src/math/subpaving/tactic/subpaving_tactic.cpp index 7bbff4b0b..d03bacebb 100644 --- a/src/math/subpaving/tactic/subpaving_tactic.cpp +++ b/src/math/subpaving/tactic/subpaving_tactic.cpp @@ -81,14 +81,14 @@ class subpaving_tactic : public tactic { void collect_param_descrs(param_descrs & r) { m_ctx->collect_param_descrs(r); // #ifndef _EXTERNAL_RELEASE - r.insert(":numeral", CPK_SYMBOL, "(default: mpq) options: mpq, mpf, hwf, mpff, mpfx."); - r.insert(":print-nodes", CPK_BOOL, "(default: false) display subpaving tree leaves."); + r.insert("numeral", CPK_SYMBOL, "(default: mpq) options: mpq, mpf, hwf, mpff, mpfx."); + r.insert("print_nodes", CPK_BOOL, "(default: false) display subpaving tree leaves."); // #endif } void updt_params(params_ref const & p) { - m_display = p.get_bool(":print-nodes", false); - symbol engine = p.get_sym(":numeral", symbol("mpq")); + m_display = p.get_bool("print_nodes", false); + symbol engine = p.get_sym("numeral", symbol("mpq")); engine_kind new_kind; if (engine == "mpq") new_kind = MPQ; @@ -293,16 +293,16 @@ tactic * mk_subpaving_tactic_core(ast_manager & m, params_ref const & p) { tactic * mk_subpaving_tactic(ast_manager & m, params_ref const & p) { params_ref simp_p = p; - simp_p.set_bool(":arith-lhs", true); - simp_p.set_bool(":expand-power", true); - simp_p.set_uint(":max-power", UINT_MAX); - simp_p.set_bool(":som", true); - simp_p.set_bool(":eq2ineq", true); - simp_p.set_bool(":elim-and", true); - simp_p.set_bool(":blast-distinct", true); + simp_p.set_bool("arith_lhs", true); + simp_p.set_bool("expand_power", true); + simp_p.set_uint("max_power", UINT_MAX); + simp_p.set_bool("som", true); + simp_p.set_bool("eq2ineq", true); + simp_p.set_bool("elim_and", true); + simp_p.set_bool("blast_distinct", true); params_ref simp2_p = p; - simp2_p.set_bool(":mul-to-power", true); + simp2_p.set_bool("mul_to_power", true); return and_then(using_params(mk_simplify_tactic(m, p), simp_p), diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 258590121..beed0061e 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -60,10 +60,10 @@ struct evaluator_cfg : public default_rewriter_cfg { } void updt_params(params_ref const & p) { - m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX)); - m_max_steps = p.get_uint(":max-steps", UINT_MAX); - m_model_completion = p.get_bool(":model-completion", false); - m_cache = p.get_bool(":cache", 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_model_completion = p.get_bool("model_completion", false); + m_cache = p.get_bool("cache", true); } ast_manager & m() const { return m_model.get_manager(); } @@ -232,8 +232,8 @@ void model_evaluator::updt_params(params_ref const & p) { void model_evaluator::get_param_descrs(param_descrs & r) { insert_max_memory(r); insert_max_steps(r); - r.insert(":model-completion", CPK_BOOL, "(default: false) assigns an interpretation to symbols that are not intepreted by the model."); - r.insert(":cache", CPK_BOOL, "(default: true) cache intermediate results."); + r.insert("model_completion", CPK_BOOL, "(default: false) assigns an interpretation to symbols that are not intepreted by the model."); + r.insert("cache", CPK_BOOL, "(default: true) cache intermediate results."); } void model_evaluator::set_model_completion(bool f) { diff --git a/src/muz_qe/datalog_parser.cpp b/src/muz_qe/datalog_parser.cpp index f527bb25a..a1bfc629d 100644 --- a/src/muz_qe/datalog_parser.cpp +++ b/src/muz_qe/datalog_parser.cpp @@ -1162,7 +1162,7 @@ public: : dparser(ctx, ctx.get_manager()), m_bool_sort(ctx.get_manager()), m_short_sort(ctx.get_manager()), - m_use_map_names(ctx.get_params().get_bool(":use-map-names", true)) { + m_use_map_names(ctx.get_params().get_bool("use_map_names", true)) { } ~wpa_parser_impl() { reset_dealloc_values(m_sort_contents); diff --git a/src/muz_qe/dl_bmc_engine.cpp b/src/muz_qe/dl_bmc_engine.cpp index 02791bc6f..e88e04c5a 100644 --- a/src/muz_qe/dl_bmc_engine.cpp +++ b/src/muz_qe/dl_bmc_engine.cpp @@ -71,7 +71,7 @@ namespace datalog { m_ctx.set_output_predicate(m_query_pred); m_ctx.apply_default_transformation(mc, m_pc); - if (m_ctx.get_params().get_bool(":slice", true)) { + if (m_ctx.get_params().get_bool("slice", true)) { datalog::rule_transformer transformer(m_ctx); datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx); transformer.register_plugin(slice); diff --git a/src/muz_qe/dl_cmds.cpp b/src/muz_qe/dl_cmds.cpp index e19b9fef8..28e699c7c 100644 --- a/src/muz_qe/dl_cmds.cpp +++ b/src/muz_qe/dl_cmds.cpp @@ -210,7 +210,7 @@ public: datalog::context& dlctx = m_dl_ctx->dlctx(); set_background(ctx); dlctx.updt_params(m_params); - unsigned timeout = m_params.get_uint(":timeout", UINT_MAX); + unsigned timeout = m_params.get_uint("timeout", UINT_MAX); cancel_eh eh(dlctx); lbool status = l_undef; { @@ -266,9 +266,9 @@ public: virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) { m_dl_ctx->dlctx().collect_params(p); insert_timeout(p); - p.insert(":print-answer", CPK_BOOL, "(default: false) print answer instance(s) to query."); - p.insert(":print-certificate", CPK_BOOL, "(default: false) print certificate for reachability or non-reachability."); - p.insert(":print-statistics", CPK_BOOL, "(default: false) print statistics."); + p.insert("print_answer", CPK_BOOL, "(default: false) print answer instance(s) to query."); + p.insert("print_certificate", CPK_BOOL, "(default: false) print certificate for reachability or non-reachability."); + p.insert("print_statistics", CPK_BOOL, "(default: false) print statistics."); } @@ -283,7 +283,7 @@ private: } void print_answer(cmd_context& ctx) { - if (m_params.get_bool(":print-answer", false)) { + if (m_params.get_bool("print_answer", false)) { datalog::context& dlctx = m_dl_ctx->dlctx(); ast_manager& m = ctx.m(); expr_ref query_result(dlctx.get_answer_as_formula(), m); @@ -298,7 +298,7 @@ private: } void print_statistics(cmd_context& ctx) { - if (m_params.get_bool(":print-statistics", false)) { + if (m_params.get_bool("print_statistics", false)) { statistics st; datalog::context& dlctx = m_dl_ctx->dlctx(); unsigned long long max_mem = memory::get_max_used_memory(); @@ -312,7 +312,7 @@ private: } void print_certificate(cmd_context& ctx) { - if (m_params.get_bool(":print-certificate", false)) { + if (m_params.get_bool("print_certificate", false)) { datalog::context& dlctx = m_dl_ctx->dlctx(); if (!dlctx.display_certificate(ctx.regular_stream())) { throw cmd_exception("certificates are not supported for the selected engine"); diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index ec78f8e92..9fbc93248 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -960,55 +960,55 @@ namespace datalog { } void context::collect_params(param_descrs& p) { - p.insert(":engine", CPK_SYMBOL, "(default: automatically configured) select 'datalog', PDR 'pdr' engine."); - p.insert(":bit-blast", CPK_BOOL, "(default: false) bit-blast bit-vectors (for PDR engine)."); - p.insert(":default-table", CPK_SYMBOL, "default table implementation: 'sparse' (default), 'hashtable', 'bitvector', 'interval'"); - p.insert(":default-relation", CPK_SYMBOL, "default relation implementation: 'external_relation', 'pentagon'"); + p.insert("engine", CPK_SYMBOL, "(default: automatically configured) select 'datalog', PDR 'pdr' engine."); + p.insert("bit_blast", CPK_BOOL, "(default: false) bit-blast bit-vectors (for PDR engine)."); + p.insert("default_table", CPK_SYMBOL, "default table implementation: 'sparse' (default), 'hashtable', 'bitvector', 'interval'"); + p.insert("default_relation", CPK_SYMBOL, "default relation implementation: 'external_relation', 'pentagon'"); - p.insert(":generate-explanations", CPK_BOOL, "if true, signature of relations will be extended to contain explanations for facts"); - p.insert(":explanations-on-relation-level", CPK_BOOL, "if true, explanations are generated as history of each relation, " - "rather than per fact (:generate-explanations must be set to true for this option to have any effect)"); + p.insert("generate_explanations", CPK_BOOL, "if true, signature of relations will be extended to contain explanations for facts"); + p.insert("explanations_on_relation_level", CPK_BOOL, "if true, explanations are generated as history of each relation, " + "rather than per fact (generate_explanations must be set to true for this option to have any effect)"); - p.insert(":magic-sets-for-queries", CPK_BOOL, "magic set transformation will be used for queries"); - p.insert(":unbound-compressor", CPK_BOOL, "auxiliary relations will be introduced to avoid unbound variables in rule heads"); - p.insert(":similarity-compressor", CPK_BOOL, "rules that differ only in values of constants will be merged into a single rule"); - p.insert(":similarity-compressor-threshold", CPK_UINT, "if :dl-similiaryt-compressor is on, this value determines how many " + p.insert("magic_sets_for_queries", CPK_BOOL, "magic set transformation will be used for queries"); + p.insert("unbound_compressor", CPK_BOOL, "auxiliary relations will be introduced to avoid unbound variables in rule heads"); + p.insert("similarity_compressor", CPK_BOOL, "rules that differ only in values of constants will be merged into a single rule"); + p.insert("similarity_compressor_threshold", CPK_UINT, "if dl_similiaryt_compressor is on, this value determines how many " "similar rules there must be in order for them to be merged"); - p.insert(":all-or-nothing-deltas", CPK_BOOL, "compile rules so that it is enough for the delta relation in union and widening " + p.insert("all_or_nothing_deltas", CPK_BOOL, "compile rules so that it is enough for the delta relation in union and widening " "operations to determine only whether the updated relation was modified or not"); - p.insert(":compile-with-widening", CPK_BOOL, "widening will be used to compile recursive rules"); - p.insert(":eager-emptiness-checking", CPK_BOOL, "emptiness of affected relations will be checked after each instruction, " + p.insert("compile_with_widening", CPK_BOOL, "widening will be used to compile recursive rules"); + p.insert("eager_emptiness_checking", CPK_BOOL, "emptiness of affected relations will be checked after each instruction, " "so that we may ommit unnecessary instructions"); - p.insert(":default-table-checked", CPK_BOOL, - "if true, the detault table will be :default-table inside a wrapper that checks that " - "its results are the same as of :default-table-checker table"); + p.insert("default_table_checked", CPK_BOOL, + "if true, the detault table will be default_table inside a wrapper that checks that " + "its results are the same as of default_table_checker table"); - p.insert(":initial-restart-timeout", CPK_UINT, "length of saturation run before the first restart (in ms); zero means no restarts"); - p.insert(":restart-timeout-quotient", CPK_UINT, "restart timeout will be multiplied by this number after each restart"); - p.insert(":use-map-names", CPK_BOOL, "use names from map files when displaying tuples"); + p.insert("initial_restart_timeout", CPK_UINT, "length of saturation run before the first restart (in ms); zero means no restarts"); + p.insert("restart_timeout_quotient", CPK_UINT, "restart timeout will be multiplied by this number after each restart"); + p.insert("use_map_names", CPK_BOOL, "use names from map files when displaying tuples"); - p.insert(":output-profile", CPK_BOOL, "determines whether profile informations should be output when outputting Datalog rules or instructions"); - p.insert(":output-tuples", CPK_BOOL, "determines whether tuples for output predicates should be output"); - p.insert(":profile-timeout-milliseconds", CPK_UINT, "instructions and rules that took less than the threshold will not be printed when printed the instruction/rule list"); + p.insert("output_profile", CPK_BOOL, "determines whether profile informations should be output when outputting Datalog rules or instructions"); + p.insert("output_tuples", CPK_BOOL, "determines whether tuples for output predicates should be output"); + p.insert("profile_timeout_milliseconds", CPK_UINT, "instructions and rules that took less than the threshold will not be printed when printed the instruction/rule list"); - p.insert(":print-with-fixedpoint-extensions", CPK_BOOL, "(default true) use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rules"); - p.insert(":print-low-level-smt2", CPK_BOOL, "(default false) use (faster) low-level SMT2 printer (the printer is scalable but the result may not be as readable)"); + p.insert("print_with_fixedpoint_extensions", CPK_BOOL, "(default true) use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rules"); + p.insert("print_low_level_smt2", CPK_BOOL, "(default false) use (faster) low-level SMT2 printer (the printer is scalable but the result may not be as readable)"); PRIVATE_PARAMS( - p.insert(":dbg-fpr-nonempty-relation-signature", CPK_BOOL, + p.insert("dbg_fpr_nonempty_relation_signature", CPK_BOOL, "if true, finite_product_relation will attempt to avoid creating inner relation with empty signature " "by putting in half of the table columns, if it would have been empty otherwise"); - p.insert(":smt-relation-ground-recursive", CPK_BOOL, "Ensure recursive relation is ground in union"); + p.insert("smt_relation_ground_recursive", CPK_BOOL, "Ensure recursive relation is ground in union"); ); - p.insert(":fix-unbound-vars", CPK_BOOL, "fix unbound variables in tail"); - p.insert(":default-table-checker", CPK_SYMBOL, "see :default-table-checked"); - p.insert(":inline-linear", CPK_BOOL, "(default true) try linear inlining method"); - p.insert(":inline-eager", CPK_BOOL, "(default true) try eager inlining of rules"); - PRIVATE_PARAMS(p.insert(":inline-linear-branch", CPK_BOOL, "try linear inlining method with potential expansion");); + p.insert("fix_unbound_vars", CPK_BOOL, "fix unbound variables in tail"); + p.insert("default_table_checker", CPK_SYMBOL, "see default_table_checked"); + p.insert("inline_linear", CPK_BOOL, "(default true) try linear inlining method"); + p.insert("inline_eager", CPK_BOOL, "(default true) try eager inlining of rules"); + PRIVATE_PARAMS(p.insert("inline_linear_branch", CPK_BOOL, "try linear inlining method with potential expansion");); pdr::dl_interface::collect_params(p); bmc::collect_params(p); @@ -1189,7 +1189,7 @@ namespace datalog { }; void context::configure_engine() { - symbol e = m_params.get_sym(":engine", symbol()); + symbol e = m_params.get_sym("engine", symbol()); if (e == symbol("datalog")) { m_engine = DATALOG_ENGINE; @@ -1650,8 +1650,8 @@ namespace datalog { expr_ref fml(m); expr_ref_vector rules(m); svector names; - bool use_fixedpoint_extensions = m_params.get_bool(":print-with-fixedpoint-extensions", true); - bool print_low_level = m_params.get_bool(":print-low-level-smt2", false); + bool use_fixedpoint_extensions = m_params.get_bool("print_with_fixedpoint_extensions", true); + bool print_low_level = m_params.get_bool("print_low_level_smt2", false); #define PP(_e_) if (print_low_level) out << mk_smt_pp(_e_, m); else ast_smt2_pp(out, _e_, env, params); diff --git a/src/muz_qe/dl_context.h b/src/muz_qe/dl_context.h index 229bbc474..fe94dd3cc 100644 --- a/src/muz_qe/dl_context.h +++ b/src/muz_qe/dl_context.h @@ -156,25 +156,25 @@ namespace datalog { var_subst & get_var_subst() { return m_var_subst; } dl_decl_util & get_decl_util() { return m_decl_util; } - bool output_profile() const { return m_params.get_bool(":output-profile", false); } - bool fix_unbound_vars() const { return m_params.get_bool(":fix-unbound-vars", false); } - symbol default_table() const { return m_params.get_sym(":default-table", symbol("sparse")); } - symbol default_relation() const { return m_params.get_sym(":default-relation", external_relation_plugin::get_name()); } - symbol default_table_checker() const { return m_params.get_sym(":default-table-checker", symbol("sparse")); } - bool default_table_checked() const { return m_params.get_bool(":default-table-checked", false); } - bool dbg_fpr_nonempty_relation_signature() const { return m_params.get_bool(":dbg-fpr-nonempty-relation-signatures", false); } - unsigned dl_profile_milliseconds_threshold() const { return m_params.get_uint(":profile-milliseconds-threshold", 0); } - bool all_or_nothing_deltas() const { return m_params.get_bool(":all-or-nothing-deltas", false); } - bool compile_with_widening() const { return m_params.get_bool(":compile-with-widening", false); } - bool unbound_compressor() const { return m_params.get_bool(":unbound-compressor", true); } - bool similarity_compressor() const { return m_params.get_bool(":similarity-compressor", true); } - unsigned similarity_compressor_threshold() const { return m_params.get_uint(":similarity-compressor-threshold", 11); } + bool output_profile() const { return m_params.get_bool("output_profile", false); } + bool fix_unbound_vars() const { return m_params.get_bool("fix_unbound_vars", false); } + symbol default_table() const { return m_params.get_sym("default_table", symbol("sparse")); } + symbol default_relation() const { return m_params.get_sym("default_relation", external_relation_plugin::get_name()); } + symbol default_table_checker() const { return m_params.get_sym("default_table_checker", symbol("sparse")); } + bool default_table_checked() const { return m_params.get_bool("default_table_checked", false); } + bool dbg_fpr_nonempty_relation_signature() const { return m_params.get_bool("dbg_fpr_nonempty_relation_signatures", false); } + unsigned dl_profile_milliseconds_threshold() const { return m_params.get_uint("profile_milliseconds_threshold", 0); } + bool all_or_nothing_deltas() const { return m_params.get_bool("all_or_nothing_deltas", false); } + bool compile_with_widening() const { return m_params.get_bool("compile_with_widening", false); } + bool unbound_compressor() const { return m_params.get_bool("unbound_compressor", true); } + bool similarity_compressor() const { return m_params.get_bool("similarity_compressor", true); } + unsigned similarity_compressor_threshold() const { return m_params.get_uint("similarity_compressor_threshold", 11); } unsigned soft_timeout() const { return m_fparams.m_soft_timeout; } - unsigned initial_restart_timeout() const { return m_params.get_uint(":initial-restart-timeout", 0); } - bool generate_explanations() const { return m_params.get_bool(":generate-explanations", false); } - bool explanations_on_relation_level() const { return m_params.get_bool(":explanations-on-relation-level", false); } - bool magic_sets_for_queries() const { return m_params.get_bool(":magic-sets-for-queries", false); } - bool eager_emptiness_checking() const { return m_params.get_bool(":eager-emptiness-checking", true); } + unsigned initial_restart_timeout() const { return m_params.get_uint("initial_restart_timeout", 0); } + bool generate_explanations() const { return m_params.get_bool("generate_explanations", false); } + bool explanations_on_relation_level() const { return m_params.get_bool("explanations_on_relation_level", false); } + bool magic_sets_for_queries() const { return m_params.get_bool("magic_sets_for_queries", false); } + bool eager_emptiness_checking() const { return m_params.get_bool("eager_emptiness_checking", true); } void register_finite_sort(sort * s, sort_kind k); diff --git a/src/muz_qe/dl_mk_array_blast.cpp b/src/muz_qe/dl_mk_array_blast.cpp index d63528db3..a5259ba8a 100644 --- a/src/muz_qe/dl_mk_array_blast.cpp +++ b/src/muz_qe/dl_mk_array_blast.cpp @@ -30,7 +30,7 @@ namespace datalog { a(m), rm(ctx.get_rule_manager()), m_rewriter(m, m_params){ - m_params.set_bool(":expand-select-store",true); + m_params.set_bool("expand_select_store",true); m_rewriter.updt_params(m_params); } diff --git a/src/muz_qe/dl_mk_bit_blast.cpp b/src/muz_qe/dl_mk_bit_blast.cpp index 9c503360c..c523315d9 100644 --- a/src/muz_qe/dl_mk_bit_blast.cpp +++ b/src/muz_qe/dl_mk_bit_blast.cpp @@ -165,14 +165,14 @@ namespace datalog { m_rules(ctx.get_rule_manager()), m_blaster(ctx.get_manager(), m_params), m_rewriter(ctx.get_manager(), ctx, m_rules) { - m_params.set_bool(":blast-full", true); - m_params.set_bool(":blast-quant", true); + m_params.set_bool("blast_full", true); + m_params.set_bool("blast_quant", true); m_blaster.updt_params(m_params); } rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { // TODO mc, pc - if (!m_context.get_params().get_bool(":bit-blast", false)) { + if (!m_context.get_params().get_bool("bit_blast", false)) { return 0; } if (m_context.get_engine() != PDR_ENGINE) { diff --git a/src/muz_qe/dl_mk_rule_inliner.cpp b/src/muz_qe/dl_mk_rule_inliner.cpp index 1d3d62020..cfe532fb6 100644 --- a/src/muz_qe/dl_mk_rule_inliner.cpp +++ b/src/muz_qe/dl_mk_rule_inliner.cpp @@ -751,7 +751,7 @@ namespace datalog { valid.resize(sz, true); params_ref const& params = m_context.get_params(); - bool allow_branching = params.get_bool(":inline-linear-branch", false); + bool allow_branching = params.get_bool("inline_linear_branch", false); for (unsigned i = 0; i < sz; ++i) { @@ -867,7 +867,7 @@ namespace datalog { scoped_ptr res = alloc(rule_set, m_context); - if (params.get_bool(":inline-eager", true)) { + if (params.get_bool("inline_eager", true)) { TRACE("dl", source.display(tout << "before eager inlining\n");); plan_inlining(source); something_done = transform_rules(source, *res); @@ -879,7 +879,7 @@ namespace datalog { TRACE("dl", res->display(tout << "after eager inlining\n");); } - if (params.get_bool(":inline-linear", true) && inline_linear(res)) { + if (params.get_bool("inline_linear", true) && inline_linear(res)) { something_done = true; } diff --git a/src/muz_qe/dl_smt_relation.cpp b/src/muz_qe/dl_smt_relation.cpp index 55d3f7199..348c63e1c 100644 --- a/src/muz_qe/dl_smt_relation.cpp +++ b/src/muz_qe/dl_smt_relation.cpp @@ -533,7 +533,7 @@ namespace datalog { IF_VERBOSE(10, verbose_stream() << "Computing delta...\n"; ); - if (params.get_bool(":smt-relation-ground-recursive", false)) { + if (params.get_bool("smt_relation_ground_recursive", false)) { // ensure R is ground. Simplify S using assumption not R if (!is_ground(rInst)) { proof_ref pr(m); diff --git a/src/muz_qe/horn_tactic.cpp b/src/muz_qe/horn_tactic.cpp index 59e9e6fec..dd6a2c2d3 100644 --- a/src/muz_qe/horn_tactic.cpp +++ b/src/muz_qe/horn_tactic.cpp @@ -161,9 +161,9 @@ class horn_tactic : public tactic { bool produce_proofs = g->proofs_enabled(); if (produce_proofs) { - if (!m_ctx.get_params().get_bool(":generate-proof-trace", true)) { + if (!m_ctx.get_params().get_bool("generate_proof_trace", true)) { params_ref params = m_ctx.get_params(); - params.set_bool(":generate-proof-trace", true); + params.set_bool("generate_proof_trace", true); updt_params(params); } } diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index 2f43d518c..3b3ee61a1 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -1098,7 +1098,7 @@ namespace pdr { m_pm(m_fparams, m_params, m), m_query_pred(m), m_query(0), - m_search(m_params.get_bool(":bfs-model-search", true)), + m_search(m_params.get_bool("bfs_model_search", true)), m_last_result(l_undef), m_inductive_lvl(0), m_cancel(false) @@ -1323,7 +1323,7 @@ namespace pdr { }; void context::validate() { - if (!m_params.get_bool(":validate-result", false)) { + if (!m_params.get_bool("validate_result", false)) { return; } switch(m_last_result) { @@ -1414,12 +1414,12 @@ namespace pdr { void context::init_core_generalizers(datalog::rule_set& rules) { reset_core_generalizers(); classifier_proc classify(m, rules); - bool use_mc = m_params.get_bool(":use-multicore-generalizer", false); + bool use_mc = m_params.get_bool("use_multicore_generalizer", false); if (use_mc) { m_core_generalizers.push_back(alloc(core_multi_generalizer, *this, 0)); } - if (m_params.get_bool(":use-farkas", true) && !classify.is_bool()) { - if (m_params.get_bool(":inline-proof-mode", true)) { + if (m_params.get_bool("use_farkas", true) && !classify.is_bool()) { + if (m_params.get_bool("inline_proof_mode", true)) { m.toggle_proof_mode(PGM_FINE); m_fparams.m_proof_mode = PGM_FINE; m_fparams.m_arith_bound_prop = BP_NONE; @@ -1435,13 +1435,13 @@ namespace pdr { m_core_generalizers.push_back(alloc(core_farkas_generalizer, *this, m, m_fparams)); } } - if (!use_mc && m_params.get_bool(":use-inductive-generalizer", true)) { + if (!use_mc && m_params.get_bool("use_inductive_generalizer", true)) { m_core_generalizers.push_back(alloc(core_bool_inductive_generalizer, *this, 0)); } - if (m_params.get_bool(":use-interpolants", false)) { + if (m_params.get_bool("use_interpolants", false)) { m_core_generalizers.push_back(alloc(core_interpolant_generalizer, *this)); } - if (m_params.get_bool(":inductive-reachability-check", false)) { + if (m_params.get_bool("inductive_reachability_check", false)) { m_core_generalizers.push_back(alloc(core_induction_generalizer, *this)); } } @@ -1553,7 +1553,7 @@ namespace pdr { \brief Retrieve satisfying assignment with explanation. */ expr_ref context::mk_sat_answer() const { - if (m_params.get_bool(":generate-proof-trace", false)) { + if (m_params.get_bool("generate_proof_trace", false)) { proof_ref pr = get_proof(); return expr_ref(pr.get(), m); } @@ -1674,7 +1674,7 @@ namespace pdr { n.pt().add_property(ncore, uses_level?n.level():infty_level); } CASSERT("pdr",n.level() == 0 || check_invariant(n.level()-1)); - m_search.backtrack_level(!found_invariant && m_params.get_bool(":flexible-trace", false), n); + m_search.backtrack_level(!found_invariant && m_params.get_bool("flexible_trace", false), n); break; } case l_undef: { @@ -1696,7 +1696,7 @@ namespace pdr { } void context::propagate(unsigned max_prop_lvl) { - if (m_params.get_bool(":simplify-formulas-pre", false)) { + if (m_params.get_bool("simplify_formulas_pre", false)) { simplify_formulas(); } for (unsigned lvl = 0; lvl <= max_prop_lvl; lvl++) { @@ -1715,7 +1715,7 @@ namespace pdr { throw inductive_exception(); } } - if (m_params.get_bool(":simplify-formulas-post", false)) { + if (m_params.get_bool("simplify_formulas_post", false)) { simplify_formulas(); } } @@ -1763,7 +1763,7 @@ namespace pdr { */ void context::create_children(model_node& n) { SASSERT(n.level() > 0); - bool use_model_generalizer = m_params.get_bool(":use-model-generalizer", false); + bool use_model_generalizer = m_params.get_bool("use_model_generalizer", false); datalog::scoped_no_proof _sc(m); pred_transformer& pt = n.pt(); diff --git a/src/muz_qe/pdr_dl_interface.cpp b/src/muz_qe/pdr_dl_interface.cpp index b047aaae0..6cbc3b78d 100644 --- a/src/muz_qe/pdr_dl_interface.cpp +++ b/src/muz_qe/pdr_dl_interface.cpp @@ -108,13 +108,13 @@ lbool dl_interface::query(expr * query) { model_converter_ref mc = datalog::mk_skip_model_converter(); proof_converter_ref pc; - if (m_ctx.get_params().get_bool(":generate-proof-trace", false)) { + if (m_ctx.get_params().get_bool("generate_proof_trace", false)) { pc = datalog::mk_skip_proof_converter(); } m_ctx.set_output_predicate(query_pred); m_ctx.apply_default_transformation(mc, pc); - if (m_ctx.get_params().get_bool(":slice", true)) { + if (m_ctx.get_params().get_bool("slice", true)) { datalog::rule_transformer transformer(m_ctx); datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx); transformer.register_plugin(slice); @@ -133,10 +133,10 @@ lbool dl_interface::query(expr * query) { } } - if (m_ctx.get_params().get_uint(":unfold-rules",0) > 0) { - unsigned num_unfolds = m_ctx.get_params().get_uint(":unfold-rules", 0); + if (m_ctx.get_params().get_uint("unfold_rules",0) > 0) { + unsigned num_unfolds = m_ctx.get_params().get_uint("unfold_rules", 0); datalog::rule_transformer transformer1(m_ctx), transformer2(m_ctx); - if (m_ctx.get_params().get_uint(":coalesce-rules", false)) { + if (m_ctx.get_params().get_uint("coalesce_rules", false)) { transformer1.register_plugin(alloc(datalog::mk_coalesce, m_ctx)); m_ctx.transform_rules(transformer1, mc, pc); } @@ -198,7 +198,7 @@ expr_ref dl_interface::get_cover_delta(int level, func_decl* pred_orig) { } void dl_interface::add_cover(int level, func_decl* pred, expr* property) { - if (m_ctx.get_params().get_bool(":slice", true)) { + if (m_ctx.get_params().get_bool("slice", true)) { throw default_exception("Covers are incompatible with slicing. Disable slicing before using covers"); } m_context->add_cover(level, pred, property); @@ -248,28 +248,28 @@ proof_ref dl_interface::get_proof() { } void dl_interface::collect_params(param_descrs& p) { - p.insert(":bfs-model-search", CPK_BOOL, "PDR: (default true) use BFS strategy for expanding model search"); - p.insert(":use-farkas", CPK_BOOL, "PDR: (default true) use lemma generator based on Farkas (for linear real arithmetic)"); - p.insert(":generate-proof-trace", CPK_BOOL, "PDR: (default false) trace for 'sat' answer as proof object"); - p.insert(":inline-proofs", CPK_BOOL, "PDR: (default true) run PDR with proof mode turned on and extract " + p.insert("bfs_model_search", CPK_BOOL, "PDR: (default true) use BFS strategy for expanding model search"); + p.insert("use_farkas", CPK_BOOL, "PDR: (default true) use lemma generator based on Farkas (for linear real arithmetic)"); + p.insert("generate_proof_trace", CPK_BOOL, "PDR: (default false) trace for 'sat' answer as proof object"); + p.insert("inline_proofs", CPK_BOOL, "PDR: (default true) run PDR with proof mode turned on and extract " "Farkas coefficients directly (instead of creating a separate proof object when extracting coefficients)"); - p.insert(":flexible-trace", CPK_BOOL, "PDR: (default false) allow PDR generate long counter-examples " + p.insert("flexible_trace", CPK_BOOL, "PDR: (default false) allow PDR generate long counter-examples " "by extending candidate trace within search area"); - p.insert(":unfold-rules", CPK_UINT, "PDR: (default 0) unfold rules statically using iterative squarring"); - p.insert(":use-model-generalizer", CPK_BOOL, "PDR: (default false) use model for backwards propagation (instead of symbolic simulation)"); - p.insert(":validate-result", CPK_BOOL, "PDR (default false) validate result (by proof checking or model checking)"); - PRIVATE_PARAMS(p.insert(":use-multicore-generalizer", CPK_BOOL, "PDR: (default false) extract multiple cores for blocking states");); - PRIVATE_PARAMS(p.insert(":use-inductive-generalizer", CPK_BOOL, "PDR: (default true) generalize lemmas using induction strengthening");); - PRIVATE_PARAMS(p.insert(":use-interpolants", CPK_BOOL, "PDR: (default false) use iZ3 interpolation for lemma generation");); - PRIVATE_PARAMS(p.insert(":dump-interpolants", CPK_BOOL, "PDR: (default false) display interpolants");); - PRIVATE_PARAMS(p.insert(":cache-mode", CPK_UINT, "PDR: use no (0 - default) symbolic (1) or explicit cache (2) for model search");); - PRIVATE_PARAMS(p.insert(":inductive-reachability-check", CPK_BOOL, + p.insert("unfold_rules", CPK_UINT, "PDR: (default 0) unfold rules statically using iterative squarring"); + p.insert("use_model_generalizer", CPK_BOOL, "PDR: (default false) use model for backwards propagation (instead of symbolic simulation)"); + p.insert("validate_result", CPK_BOOL, "PDR (default false) validate result (by proof checking or model checking)"); + PRIVATE_PARAMS(p.insert("use_multicore_generalizer", CPK_BOOL, "PDR: (default false) extract multiple cores for blocking states");); + PRIVATE_PARAMS(p.insert("use_inductive_generalizer", CPK_BOOL, "PDR: (default true) generalize lemmas using induction strengthening");); + PRIVATE_PARAMS(p.insert("use_interpolants", CPK_BOOL, "PDR: (default false) use iZ3 interpolation for lemma generation");); + PRIVATE_PARAMS(p.insert("dump_interpolants", CPK_BOOL, "PDR: (default false) display interpolants");); + PRIVATE_PARAMS(p.insert("cache_mode", CPK_UINT, "PDR: use no (0 - default) symbolic (1) or explicit cache (2) for model search");); + PRIVATE_PARAMS(p.insert("inductive_reachability_check", CPK_BOOL, "PDR: (default false) assume negation of the cube on the previous level when " "checking for reachability (not only during cube weakening)");); - PRIVATE_PARAMS(p.insert(":max-num-contexts", CPK_UINT, "PDR: (default 500) maximal number of contexts to create");); - PRIVATE_PARAMS(p.insert(":try-minimize-core", CPK_BOOL, "PDR: (default false) try to reduce core size (before inductive minimization)");); - p.insert(":simplify-formulas-pre", CPK_BOOL, "PDR: (default false) simplify derived formulas before inductive propagation"); - p.insert(":simplify-formulas-post", CPK_BOOL, "PDR: (default false) simplify derived formulas after inductive propagation"); - p.insert(":slice", CPK_BOOL, "PDR: (default true) simplify clause set using slicing"); - p.insert(":coalesce-rules", CPK_BOOL, "BMC: (default false) coalesce rules"); + PRIVATE_PARAMS(p.insert("max_num_contexts", CPK_UINT, "PDR: (default 500) maximal number of contexts to create");); + PRIVATE_PARAMS(p.insert("try_minimize_core", CPK_BOOL, "PDR: (default false) try to reduce core size (before inductive minimization)");); + p.insert("simplify_formulas_pre", CPK_BOOL, "PDR: (default false) simplify derived formulas before inductive propagation"); + p.insert("simplify_formulas_post", CPK_BOOL, "PDR: (default false) simplify derived formulas after inductive propagation"); + p.insert("slice", CPK_BOOL, "PDR: (default true) simplify clause set using slicing"); + p.insert("coalesce_rules", CPK_BOOL, "BMC: (default false) coalesce rules"); } diff --git a/src/muz_qe/pdr_interpolant_provider.cpp b/src/muz_qe/pdr_interpolant_provider.cpp index 85655c737..bcea5cbc4 100644 --- a/src/muz_qe/pdr_interpolant_provider.cpp +++ b/src/muz_qe/pdr_interpolant_provider.cpp @@ -318,7 +318,7 @@ lbool interpolant_provider_impl::get_interpolant(expr * f1, expr * f2, expr_ref& throw default_exception("invalid interpolator output"); } res = *ait; - if (m_params.get_bool(":dump-interpolants", false)) { + if (m_params.get_bool("dump_interpolants", false)) { interpolant_provider::output_interpolant(m, f1, f2, res); } return l_true; diff --git a/src/muz_qe/pdr_prop_solver.cpp b/src/muz_qe/pdr_prop_solver.cpp index d70675d80..4fd036f48 100644 --- a/src/muz_qe/pdr_prop_solver.cpp +++ b/src/muz_qe/pdr_prop_solver.cpp @@ -212,7 +212,7 @@ namespace pdr { m(pm.get_manager()), m_pm(pm), m_name(name), - m_try_minimize_core(pm.get_params().get_bool(":try-minimize-core", false)), + m_try_minimize_core(pm.get_params().get_bool("try_minimize_core", false)), m_ctx(pm.mk_fresh()), m_pos_level_atoms(m), m_neg_level_atoms(m), diff --git a/src/muz_qe/pdr_reachable_cache.cpp b/src/muz_qe/pdr_reachable_cache.cpp index ed9926f85..f248f4d86 100644 --- a/src/muz_qe/pdr_reachable_cache.cpp +++ b/src/muz_qe/pdr_reachable_cache.cpp @@ -27,7 +27,7 @@ namespace pdr { m_ctx(0), m_ref_holder(m), m_disj_connector(m), - m_cache_mode((datalog::PDR_CACHE_MODE)params.get_uint(":cache-mode",0)) { + m_cache_mode((datalog::PDR_CACHE_MODE)params.get_uint("cache_mode",0)) { if (m_cache_mode == datalog::CONSTRAINT_CACHE) { m_ctx = pm.mk_fresh(); m_ctx->assert_expr(m_pm.get_background()); diff --git a/src/muz_qe/pdr_smt_context_manager.cpp b/src/muz_qe/pdr_smt_context_manager.cpp index d79192769..c9dcf7b4e 100644 --- a/src/muz_qe/pdr_smt_context_manager.cpp +++ b/src/muz_qe/pdr_smt_context_manager.cpp @@ -96,7 +96,7 @@ namespace pdr { smt_context_manager::smt_context_manager(front_end_params& fp, params_ref const& p, ast_manager& m): m_fparams(fp), m(m), - m_max_num_contexts(p.get_uint(":max-num-contexts", 500)), + m_max_num_contexts(p.get_uint("max_num_contexts", 500)), m_num_contexts(0), m_predicate_list(m) { } diff --git a/src/muz_qe/qe.cpp b/src/muz_qe/qe.cpp index a01500fe3..3b854b250 100644 --- a/src/muz_qe/qe.cpp +++ b/src/muz_qe/qe.cpp @@ -1340,7 +1340,7 @@ namespace qe { m_nnf(m, get_is_relevant(), get_mk_atom()) { params_ref params; - params.set_bool(":gcd-rounding", true); + params.set_bool("gcd_rounding", true); m_rewriter.updt_params(params); } @@ -2010,7 +2010,7 @@ namespace qe { } void updt_params(params_ref const& p) { - m_eliminate_variables_as_block = p.get_bool(":eliminate-variables-as-block", m_eliminate_variables_as_block); + m_eliminate_variables_as_block = p.get_bool("eliminate_variables_as_block", m_eliminate_variables_as_block); } void eliminate(bool is_forall, unsigned num_vars, app* const* vars, expr_ref& fml) { @@ -2194,7 +2194,7 @@ namespace qe { } void expr_quant_elim::updt_params(params_ref const& p) { - bool r = p.get_bool(":use-neq-qe", m_use_new_qe); + bool r = p.get_bool("use_neq_qe", m_use_new_qe); if (r != m_use_new_qe) { dealloc(m_qe); m_qe = 0; @@ -2205,9 +2205,9 @@ namespace qe { } void expr_quant_elim::collect_param_descrs(param_descrs& r) { - r.insert(":eliminate-variables-as-block", CPK_BOOL, + r.insert("eliminate_variables_as_block", CPK_BOOL, "(default: true) eliminate variables as a block (true) or one at a time (false)"); - // r.insert(":use-new-qe", CPK_BOOL, "(default: true) invoke quantifier engine based on abstracted solver"); + // r.insert("use_new_qe", CPK_BOOL, "(default: true) invoke quantifier engine based on abstracted solver"); } void expr_quant_elim::init_qe() { diff --git a/src/muz_qe/qe_cmd.cpp b/src/muz_qe/qe_cmd.cpp index 218224c51..ef8d1c058 100644 --- a/src/muz_qe/qe_cmd.cpp +++ b/src/muz_qe/qe_cmd.cpp @@ -16,8 +16,8 @@ public: virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) { insert_timeout(p); - p.insert(":print", CPK_BOOL, "(default: true) print the simplified term."); - p.insert(":print-statistics", CPK_BOOL, "(default: false) print statistics."); + p.insert("print", CPK_BOOL, "(default: true) print the simplified term."); + p.insert("print_statistics", CPK_BOOL, "(default: false) print statistics."); } virtual ~qe_cmd() { @@ -45,11 +45,11 @@ public: qe(m_target, result, pr); - if (m_params.get_bool(":print", true)) { + if (m_params.get_bool("print", true)) { ctx.display(ctx.regular_stream(), result); ctx.regular_stream() << std::endl; } - if (m_params.get_bool(":print-statistics", false)) { + if (m_params.get_bool("print_statistics", false)) { statistics st; qe.collect_statistics(st); st.display(ctx.regular_stream()); diff --git a/src/muz_qe/qe_lite.cpp b/src/muz_qe/qe_lite.cpp index 6baa7ad80..9c9f54830 100644 --- a/src/muz_qe/qe_lite.cpp +++ b/src/muz_qe/qe_lite.cpp @@ -1048,13 +1048,13 @@ namespace fm { } void updt_params(params_ref const & p) { - m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX)); - m_fm_real_only = p.get_bool(":fm-real-only", true); - m_fm_limit = p.get_uint(":fm-limit", 5000000); - m_fm_cutoff1 = p.get_uint(":fm-cutoff1", 8); - m_fm_cutoff2 = p.get_uint(":fm-cutoff2", 256); - m_fm_extra = p.get_uint(":fm-extra", 0); - m_fm_occ = p.get_bool(":fm-occ", false); + m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); + m_fm_real_only = p.get_bool("fm_real_only", true); + m_fm_limit = p.get_uint("fm_limit", 5000000); + m_fm_cutoff1 = p.get_uint("fm_cutoff1", 8); + m_fm_cutoff2 = p.get_uint("fm_cutoff2", 256); + m_fm_extra = p.get_uint("fm_extra", 0); + m_fm_occ = p.get_bool("fm_occ", false); } void set_cancel(bool f) { diff --git a/src/muz_qe/qe_sat_tactic.cpp b/src/muz_qe/qe_sat_tactic.cpp index 1480a8ca0..5f73e4a30 100644 --- a/src/muz_qe/qe_sat_tactic.cpp +++ b/src/muz_qe/qe_sat_tactic.cpp @@ -301,17 +301,17 @@ namespace qe { virtual void cleanup() {} virtual void updt_params(params_ref const & p) { - m_extrapolate_strategy_param = p.get_uint(":extrapolate-strategy", m_extrapolate_strategy_param); - m_projection_mode_param = p.get_bool(":projection-mode", m_projection_mode_param); - m_strong_context_simplify_param = p.get_bool(":strong-context-simplify", m_strong_context_simplify_param); - m_ctx_simplify_local_param = p.get_bool(":strong-context-simplify-local", m_ctx_simplify_local_param); + m_extrapolate_strategy_param = p.get_uint("extrapolate_strategy", m_extrapolate_strategy_param); + m_projection_mode_param = p.get_bool("projection_mode", m_projection_mode_param); + m_strong_context_simplify_param = p.get_bool("strong_context_simplify", m_strong_context_simplify_param); + m_ctx_simplify_local_param = p.get_bool("strong_context_simplify_local", m_ctx_simplify_local_param); } virtual void collect_param_descrs(param_descrs & r) { - r.insert(":extrapolate-strategy",CPK_UINT, "(default: 0 trivial extrapolation) 1 - nnf strengthening 2 - smt-test 3 - nnf_weakening"); - r.insert(":projection-mode", CPK_BOOL, "(default: true - full) false - partial quantifier instantiation"); - r.insert(":strong-context-simplify", CPK_BOOL, "(default: true) use strong context simplifier on result of quantifier elimination"); - r.insert(":strong-context-simplify-local", CPK_BOOL, "(default: false) use strong context simplifier locally on the new formula only"); + r.insert("extrapolate_strategy",CPK_UINT, "(default: 0 trivial extrapolation) 1 - nnf strengthening 2 - smt-test 3 - nnf_weakening"); + r.insert("projection_mode", CPK_BOOL, "(default: true - full) false - partial quantifier instantiation"); + r.insert("strong_context_simplify", CPK_BOOL, "(default: true) use strong context simplifier on result of quantifier elimination"); + r.insert("strong_context_simplify_local", CPK_BOOL, "(default: false) use strong context simplifier locally on the new formula only"); } diff --git a/src/muz_qe/qe_tactic.cpp b/src/muz_qe/qe_tactic.cpp index f17d15d6a..971d677ea 100644 --- a/src/muz_qe/qe_tactic.cpp +++ b/src/muz_qe/qe_tactic.cpp @@ -36,7 +36,7 @@ class qe_tactic : public tactic { } void updt_params(params_ref const & p) { - m_fparams.m_nlquant_elim = p.get_bool(":qe-nonlinear", false); + m_fparams.m_nlquant_elim = p.get_bool("qe_nonlinear", false); m_qe.updt_params(p); } @@ -113,7 +113,7 @@ public: virtual void collect_param_descrs(param_descrs & r) { - r.insert(":qe-nonlinear", CPK_BOOL, "(default: false) enable virtual term substitution."); + r.insert("qe_nonlinear", CPK_BOOL, "(default: false) enable virtual term substitution."); m_imp->collect_param_descrs(r); } diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 837e76ecd..d76d584f7 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -198,15 +198,15 @@ namespace nlsat { } void updt_params(params_ref const & p) { - m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX)); - m_lazy = p.get_uint(":lazy", 0); - m_simplify_cores = p.get_bool(":simplify-conflicts", true); - bool min_cores = p.get_bool(":minimize-conflicts", false); - m_reorder = p.get_bool(":reorder", true); - m_randomize = p.get_bool(":randomize", true); - m_max_conflicts = p.get_uint(":max-conflicts", UINT_MAX); - m_random_order = p.get_bool(":shuffle-vars", false); - m_random_seed = p.get_uint(":seed", 0); + m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); + m_lazy = p.get_uint("lazy", 0); + m_simplify_cores = p.get_bool("simplify_conflicts", true); + bool min_cores = p.get_bool("minimize_conflicts", false); + m_reorder = p.get_bool("reorder", true); + m_randomize = p.get_bool("randomize", true); + m_max_conflicts = p.get_uint("max_conflicts", UINT_MAX); + m_random_order = p.get_bool("shuffle_vars", false); + m_random_seed = p.get_uint("seed", 0); m_ism.set_seed(m_random_seed); m_explain.set_simplify_cores(m_simplify_cores); m_explain.set_minimize_cores(min_cores); @@ -2572,13 +2572,13 @@ namespace nlsat { void solver::collect_param_descrs(param_descrs & d) { insert_max_memory(d); algebraic_numbers::manager::collect_param_descrs(d); - d.insert(":max-conflicts", CPK_UINT, "(default: inf) maximum number of conflicts."); - d.insert(":shuffle-vars", CPK_BOOL, "(default: false) use a variable order."); - d.insert(":seed", CPK_UINT, "(default: 0) random seed."); - d.insert(":randomize", CPK_BOOL, "(default: true) randomize selection of a witness in nlsat."); - d.insert(":reorder", CPK_BOOL, "(default: true) reorder variables."); - d.insert(":lazy", CPK_UINT, "(default: 0) how lazy the solver is."); - d.insert(":simplify-conflicts", CPK_BOOL, "(default: true) simplify conflicts using equalities before resolving them in nlsat solver."); + d.insert("max_conflicts", CPK_UINT, "(default: inf) maximum number of conflicts."); + d.insert("shuffle_vars", CPK_BOOL, "(default: false) use a variable order."); + d.insert("seed", CPK_UINT, "(default: 0) random seed."); + d.insert("randomize", CPK_BOOL, "(default: true) randomize selection of a witness in nlsat."); + d.insert("reorder", CPK_BOOL, "(default: true) reorder variables."); + d.insert("lazy", CPK_UINT, "(default: 0) how lazy the solver is."); + d.insert("simplify_conflicts", CPK_BOOL, "(default: true) simplify conflicts using equalities before resolving them in nlsat solver."); } unsynch_mpq_manager & solver::qm() { diff --git a/src/nlsat/tactic/goal2nlsat.cpp b/src/nlsat/tactic/goal2nlsat.cpp index 75e3c4a40..1af98c7e8 100644 --- a/src/nlsat/tactic/goal2nlsat.cpp +++ b/src/nlsat/tactic/goal2nlsat.cpp @@ -77,8 +77,8 @@ struct goal2nlsat::imp { } void updt_params(params_ref const & p) { - m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX)); - m_factor = p.get_bool(":factor", true); + m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); + m_factor = p.get_bool("factor", true); m_fparams.updt_params(p); } @@ -293,7 +293,7 @@ goal2nlsat::~goal2nlsat() { void goal2nlsat::collect_param_descrs(param_descrs & r) { insert_max_memory(r); - r.insert(":factor", CPK_BOOL, "(default: true) factor polynomials."); + r.insert("factor", CPK_BOOL, "(default: true) factor polynomials."); polynomial::factor_params::get_param_descrs(r); } diff --git a/src/nlsat/tactic/qfnra_nlsat_tactic.cpp b/src/nlsat/tactic/qfnra_nlsat_tactic.cpp index 7bb6bd019..b05636541 100644 --- a/src/nlsat/tactic/qfnra_nlsat_tactic.cpp +++ b/src/nlsat/tactic/qfnra_nlsat_tactic.cpp @@ -31,13 +31,13 @@ Notes: tactic * mk_qfnra_nlsat_tactic(ast_manager & m, params_ref const & p) { params_ref main_p = p; - main_p.set_bool(":elim-and", true); - main_p.set_bool(":blast-distinct", true); + main_p.set_bool("elim_and", true); + main_p.set_bool("blast_distinct", true); params_ref purify_p = p; - purify_p.set_bool(":complete", false); // temporary hack, solver does not support uninterpreted functions for encoding (div0 x) applications. So, we replace it application of this kind with an uninterpreted function symbol. + purify_p.set_bool("complete", false); // temporary hack, solver does not support uninterpreted functions for encoding (div0 x) applications. So, we replace it application of this kind with an uninterpreted function symbol. tactic * factor; - if (p.get_bool(":factor", true)) + if (p.get_bool("factor", true)) factor = mk_factor_tactic(m, p); else factor = mk_skip_tactic(); diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index bc2a7120d..a7209306a 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -194,17 +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); + 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); 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."); + 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."); } void asymm_branch::collect_statistics(statistics & st) { diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 48aa270e4..e30569d89 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -22,24 +22,24 @@ Revision History: namespace sat { config::config(params_ref const & p): - m_always_true("always-true"), - m_always_false("always-false"), + m_always_true("always_true"), + m_always_false("always_false"), m_caching("caching"), m_random("random"), m_geometric("geometric"), m_luby("luby"), - m_dyn_psm("dyn-psm"), + m_dyn_psm("dyn_psm"), m_psm("psm"), m_glue("glue"), - m_glue_psm("glue-psm"), - m_psm_glue("psm-glue") { + m_glue_psm("glue_psm"), + m_psm_glue("psm_glue") { updt_params(p); } void config::updt_params(params_ref const & p) { - m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX)); + m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); - symbol s = p.get_sym(":restart", m_luby); + symbol s = p.get_sym("restart", m_luby); if (s == m_luby) m_restart = RS_LUBY; else if (s == m_geometric) @@ -47,7 +47,7 @@ namespace sat { else throw sat_param_exception("invalid restart strategy"); - s = p.get_sym(":phase", m_caching); + s = p.get_sym("phase", m_caching); if (s == m_always_false) m_phase = PS_ALWAYS_FALSE; else if (s == m_always_true) @@ -59,29 +59,29 @@ 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.get_uint("phase_caching_on", 400); + m_phase_caching_off = p.get_uint("phase_caching_off", 100); - m_restart_initial = p.get_uint(":restart-initial", 100); - m_restart_factor = p.get_double(":restart-factor", 1.5); + m_restart_initial = p.get_uint("restart_initial", 100); + m_restart_factor = p.get_double("restart_factor", 1.5); - m_random_freq = p.get_double(":random-freq", 0.01); + m_random_freq = p.get_double("random_freq", 0.01); - m_burst_search = p.get_uint(":burst-search", 100); + m_burst_search = p.get_uint("burst_search", 100); - m_max_conflicts = p.get_uint(":max-conflicts", UINT_MAX); + m_max_conflicts = p.get_uint("max_conflicts", UINT_MAX); - 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.get_sym("gc_strategy", m_glue_psm); 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.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); if (m_gc_k > 255) m_gc_k = 255; } @@ -96,31 +96,31 @@ 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.get_uint("gc_initial", 20000); + m_gc_increment = p.get_uint("gc_increment", 500); } - m_minimize_lemmas = p.get_bool(":minimize-lemmas", true); - m_dyn_sub_res = p.get_bool(":dyn-sub-res", true); + m_minimize_lemmas = p.get_bool("minimize_lemmas", true); + m_dyn_sub_res = p.get_bool("dyn_sub_res", true); } 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."); + 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."); } }; diff --git a/src/sat/sat_probing.cpp b/src/sat/sat_probing.cpp index f51b16033..f9741cd7b 100644 --- a/src/sat/sat_probing.cpp +++ b/src/sat/sat_probing.cpp @@ -243,11 +243,11 @@ namespace sat { } void probing::updt_params(params_ref const & p) { - m_probing = p.get_bool(":probing", true); - m_probing_limit = p.get_uint(":probing-limit", 5000000); - m_probing_cache = p.get_bool(":probing-cache", true); - m_probing_binary = p.get_bool(":probing-binary", true); - m_probing_cache_limit = megabytes_to_bytes(p.get_uint(":probing-chache-limit", 1024)); + m_probing = p.get_bool("probing", true); + m_probing_limit = p.get_uint("probing_limit", 5000000); + m_probing_cache = p.get_bool("probing_cache", true); + m_probing_binary = p.get_bool("probing_binary", true); + m_probing_cache_limit = megabytes_to_bytes(p.get_uint("probing_chache_limit", 1024)); } void probing::collect_param_descrs(param_descrs & d) { diff --git a/src/sat/sat_scc.cpp b/src/sat/sat_scc.cpp index 5e351290f..f2598119f 100644 --- a/src/sat/sat_scc.cpp +++ b/src/sat/sat_scc.cpp @@ -231,11 +231,11 @@ namespace sat { } void scc::updt_params(params_ref const & p) { - m_scc = p.get_bool(":scc", true); + m_scc = p.get_bool("scc", true); } void scc::collect_param_descrs(param_descrs & d) { - d.insert(":scc", CPK_BOOL, "(default: true) eliminate Boolean variables by computing strongly connected components."); + d.insert("scc", CPK_BOOL, "(default: true) eliminate Boolean variables by computing strongly connected components."); } }; diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 3f3015967..8a1713647 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -1431,44 +1431,44 @@ namespace sat { } 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); + 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::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("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_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("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)."); + 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)."); } void simplifier::collect_statistics(statistics & st) { diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 0322e80c5..399fb2c61 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1909,7 +1909,7 @@ namespace sat { m_asymm_branch.updt_params(p); m_probing.updt_params(p); m_scc.updt_params(p); - m_rand.set_seed(p.get_uint(":random-seed", 0)); + m_rand.set_seed(p.get_uint("random_seed", 0)); } void solver::collect_param_descrs(param_descrs & d) { diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index b6c2e39cf..16184e2bc 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -67,8 +67,8 @@ struct goal2sat::imp { } void updt_params(params_ref const & p) { - m_ite_extra = p.get_bool(":ite-extra", true); - m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX)); + m_ite_extra = p.get_bool("ite_extra", true); + m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); } void throw_op_not_handled() { @@ -420,7 +420,7 @@ goal2sat::goal2sat():m_imp(0) { void goal2sat::collect_param_descrs(param_descrs & r) { insert_max_memory(r); - r.insert(":ite-extra", CPK_BOOL, "(default: true) add redundant clauses (that improve unit propagation) when encoding if-then-else formulas"); + r.insert("ite_extra", CPK_BOOL, "(default: true) add redundant clauses (that improve unit propagation) when encoding if-then-else formulas"); } struct goal2sat::scoped_set_imp { @@ -575,8 +575,8 @@ struct sat2goal::imp { } void updt_params(params_ref const & p) { - m_learned = p.get_bool(":learned", false); - m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX)); + m_learned = p.get_bool("learned", false); + m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); } void checkpoint() { @@ -676,7 +676,7 @@ sat2goal::sat2goal():m_imp(0) { void sat2goal::collect_param_descrs(param_descrs & r) { insert_max_memory(r); - r.insert(":learned", CPK_BOOL, "(default: false) collect also learned clauses."); + r.insert("learned", CPK_BOOL, "(default: false) collect also learned clauses."); } struct sat2goal::scoped_set_imp { diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp index 015eb6c66..d48994861 100644 --- a/src/sat/tactic/sat_tactic.cpp +++ b/src/sat/tactic/sat_tactic.cpp @@ -210,7 +210,7 @@ tactic * mk_sat_tactic(ast_manager & m, params_ref const & p) { tactic * mk_sat_preprocessor_tactic(ast_manager & m, params_ref const & p) { params_ref p_aux; - p_aux.set_uint(":max-conflicts", 0); + p_aux.set_uint("max_conflicts", 0); tactic * t = clean(using_params(mk_sat_tactic(m, p), p_aux)); t->updt_params(p); return t; diff --git a/src/shell/datalog_frontend.cpp b/src/shell/datalog_frontend.cpp index 14dcc91c3..d422db708 100644 --- a/src/shell/datalog_frontend.cpp +++ b/src/shell/datalog_frontend.cpp @@ -72,8 +72,8 @@ static void display_statistics( code.process_all_costs(); { params_ref p(ctx.get_params()); - p.set_bool(":output-profile", true); - p.set_uint(":profile-milliseconds-threshold", 100); + p.set_bool("output_profile", true); + p.set_uint("profile_milliseconds_threshold", 100); ctx.updt_params(p); out << "--------------\n"; @@ -132,9 +132,9 @@ unsigned read_datalog(char const * file, datalog_params const& dl_params, front_ register_on_timeout_proc(on_timeout); signal(SIGINT, on_ctrl_c); params_ref params; - params.set_sym(":engine", symbol("datalog")); - params.set_sym(":default-table", dl_params.m_default_table); - params.set_bool(":default-table-checked", dl_params.m_default_table_checked); + params.set_sym("engine", symbol("datalog")); + params.set_sym("default_table", dl_params.m_default_table); + params.set_bool("default_table_checked", dl_params.m_default_table_checked); datalog::context ctx(m, front_end_params, params); size_t watermark = front_end_params.m_memory_high_watermark; @@ -252,7 +252,7 @@ unsigned read_datalog(char const * file, datalog_params const& dl_params, front_ TRACE("dl_compiler", ctx.display(tout); rules_code.display(ctx, tout);); - if (ctx.get_params().get_bool(":output-tuples", true)) { + if (ctx.get_params().get_bool("output_tuples", true)) { ctx.display_output_facts(std::cout); } diff --git a/src/shell/dimacs_frontend.cpp b/src/shell/dimacs_frontend.cpp index cf64ed110..2dbb0adf8 100644 --- a/src/shell/dimacs_frontend.cpp +++ b/src/shell/dimacs_frontend.cpp @@ -69,7 +69,7 @@ unsigned read_dimacs(char const * file_name, front_end_params & front_end_params register_on_timeout_proc(on_timeout); signal(SIGINT, on_ctrl_c); params_ref p; - p.set_bool(":produce-models", front_end_params.m_model); + p.set_bool("produce_models", front_end_params.m_model); sat::solver solver(p, 0); g_solver = &solver; diff --git a/src/shell/main.cpp b/src/shell/main.cpp index 6dc5a7ebe..d6e7b1bf1 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -32,6 +32,7 @@ Revision History: #include"timeout.h" #include"z3_exception.h" #include"error_codes.h" +#include"gparams.h" typedef enum { IN_UNSPECIFIED, IN_SMTLIB, IN_SMTLIB_2, IN_DATALOG, IN_DIMACS, IN_Z3_LOG } input_kind; @@ -76,8 +77,7 @@ void display_usage() { std::cout << " " << OPT << "version prints version number of Z3.\n"; std::cout << " " << OPT << "v:level be verbose, where is the verbosity level.\n"; std::cout << " " << OPT << "nw disable warning messages.\n"; - std::cout << " " << OPT << "ini:file configuration file.\n"; - std::cout << " " << OPT << "ini? display all available INI file parameters.\n"; + std::cout << " " << OPT << "params display all available parameters.\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. @@ -285,13 +285,8 @@ void parse_cmd_line_args(int argc, char ** argv) { else if (strcmp(opt_name, "nw") == 0) { enable_warning_messages(false); } - else if (strcmp(opt_name, "ini") == 0) { - if (!opt_arg) - error("option argument (/ini:file) is missing."); - read_ini_file(opt_arg); - } - else if (strcmp(opt_name, "ini?") == 0) { - display_ini_help(); + else if (strcmp(opt_name, "params") == 0) { + gparams::display(std::cout); exit(0); } else if (strcmp(opt_name, "geninidoc") == 0) { @@ -327,7 +322,7 @@ void parse_cmd_line_args(int argc, char ** argv) { char * key = argv[i]; *eq_pos = 0; char * value = eq_pos+1; - g_params->set_param_value(key, value); + gparams::set(key, value); } else { if (g_front_end_params->m_interactive) { diff --git a/src/smt/arith_eq_solver.cpp b/src/smt/arith_eq_solver.cpp index 417f8022b..41a61bf73 100644 --- a/src/smt/arith_eq_solver.cpp +++ b/src/smt/arith_eq_solver.cpp @@ -26,8 +26,8 @@ arith_eq_solver::arith_eq_solver(ast_manager & m, params_ref const& p): m_util(m), m_arith_rewriter(m) { - m_params.set_bool(":gcd-rounding", true); - // m_params.set_bool(":sum", true); + m_params.set_bool("gcd_rounding", true); + // m_params.set_bool("sum", true); m_arith_rewriter.updt_params(m_params); } diff --git a/src/smt/smt_implied_equalities.cpp b/src/smt/smt_implied_equalities.cpp index 91784f5f5..c6f28d4b2 100644 --- a/src/smt/smt_implied_equalities.cpp +++ b/src/smt/smt_implied_equalities.cpp @@ -197,7 +197,7 @@ namespace smt { s_stats_val_eq_timer.start(); params_ref p; - p.set_bool(":produce-models", false); + p.set_bool("produce_models", false); m_solver.updt_params(p); for (unsigned i = 0; i < terms.size(); ++i) { @@ -232,7 +232,7 @@ namespace smt { } m_stats_val_eq_timer.stop(); s_stats_val_eq_timer.stop(); - p.set_bool(":produce-models", true); + p.set_bool("produce_models", true); m_solver.updt_params(p); @@ -325,7 +325,7 @@ namespace smt { lbool operator()(unsigned num_terms, expr* const* terms, unsigned* class_ids) { params_ref p; - p.set_bool(":produce-models", true); + p.set_bool("produce_models", true); m_solver.updt_params(p); sort2term_ids termids; stopwatch timer; diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index 84587b6c9..1551c765c 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -60,8 +60,8 @@ public: } void updt_params_core(params_ref const & p) { - m_candidate_models = p.get_bool(":candidate-models", false); - m_fail_if_inconclusive = p.get_bool(":fail-if-inconclusive", true); + m_candidate_models = p.get_bool("candidate_models", false); + m_fail_if_inconclusive = p.get_bool("fail_if_inconclusive", true); } virtual void updt_params(params_ref const & p) { @@ -69,12 +69,12 @@ public: updt_params_core(p); m_params_ref = p; params2front_end_params(m_params_ref, fparams()); - SASSERT(p.get_bool(":auto_config", fparams().m_auto_config) == fparams().m_auto_config); + SASSERT(p.get_bool("auto_config", fparams().m_auto_config) == fparams().m_auto_config); } virtual void collect_param_descrs(param_descrs & r) { - r.insert(":candidate-models", CPK_BOOL, "(default: false) create candidate models even when quantifier or theory reasoning is incomplete."); - r.insert(":fail-if-inconclusive", CPK_BOOL, "(default: true) fail if found unsat (sat) for under (over) approximated goal."); + r.insert("candidate_models", CPK_BOOL, "(default: false) create candidate models even when quantifier or theory reasoning is incomplete."); + r.insert("fail_if_inconclusive", CPK_BOOL, "(default: true) fail if found unsat (sat) for under (over) approximated goal."); solver_front_end_params_descrs(r); } @@ -315,7 +315,7 @@ tactic * mk_smt_tactic(params_ref const & p) { tactic * mk_smt_tactic_using(bool auto_config, params_ref const & _p) { params_ref p = _p; - p.set_bool(":auto-config", auto_config); + p.set_bool("auto_config", auto_config); tactic * r = mk_smt_tactic(p); TRACE("smt_tactic", tout << "auto_config: " << auto_config << "\nr: " << r << "\np: " << p << "\n";); return using_params(r, p); diff --git a/src/tactic/aig/aig_tactic.cpp b/src/tactic/aig/aig_tactic.cpp index 617db0b8c..dc577eb73 100644 --- a/src/tactic/aig/aig_tactic.cpp +++ b/src/tactic/aig/aig_tactic.cpp @@ -62,14 +62,14 @@ public: } virtual void updt_params(params_ref const & p) { - m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX)); - m_aig_gate_encoding = p.get_bool(":aig-default-gate-encoding", true); - m_aig_per_assertion = p.get_bool(":aig-per-assertion", true); + m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); + m_aig_gate_encoding = p.get_bool("aig_default_gate_encoding", true); + m_aig_per_assertion = p.get_bool("aig_per_assertion", true); } virtual void collect_param_descrs(param_descrs & r) { insert_max_memory(r); - r.insert(":aig-per-assertion", CPK_BOOL, "(default: true) process one assertion at a time."); + r.insert("aig_per_assertion", CPK_BOOL, "(default: true) process one assertion at a time."); } void operator()(goal_ref const & g) { diff --git a/src/tactic/arith/add_bounds_tactic.cpp b/src/tactic/arith/add_bounds_tactic.cpp index 81e9c26cf..d396359a3 100644 --- a/src/tactic/arith/add_bounds_tactic.cpp +++ b/src/tactic/arith/add_bounds_tactic.cpp @@ -70,8 +70,8 @@ class add_bounds_tactic : public tactic { } void updt_params(params_ref const & p) { - m_lower = p.get_rat(":add-bound-lower", rational(-2)); - m_upper = p.get_rat(":add-bound-upper", rational(2)); + m_lower = p.get_rat("add_bound_lower", rational(-2)); + m_upper = p.get_rat("add_bound_upper", rational(2)); } void set_cancel(bool f) { @@ -159,8 +159,8 @@ public: } virtual void collect_param_descrs(param_descrs & r) { - r.insert(":add-bound-lower", CPK_NUMERAL, "(default: -2) lower bound to be added to unbounded variables."); - r.insert(":add-bound-upper", CPK_NUMERAL, "(default: 2) upper bound to be added to unbounded variables."); + r.insert("add_bound_lower", CPK_NUMERAL, "(default: -2) lower bound to be added to unbounded variables."); + r.insert("add_bound_upper", CPK_NUMERAL, "(default: 2) upper bound to be added to unbounded variables."); } virtual void operator()(goal_ref const & g, diff --git a/src/tactic/arith/bound_propagator.cpp b/src/tactic/arith/bound_propagator.cpp index 40c2ed49b..dbd7c5f69 100644 --- a/src/tactic/arith/bound_propagator.cpp +++ b/src/tactic/arith/bound_propagator.cpp @@ -116,15 +116,15 @@ void bound_propagator::del_constraint(constraint & c) { } void bound_propagator::updt_params(params_ref const & p) { - m_max_refinements = p.get_uint(":bound-max-refinements", 16); - m_threshold = p.get_double(":bound-threshold", 0.05); - m_small_interval = p.get_double(":bound-small-interval", 128); - m_strict2double = p.get_double(":strict2double", 0.00001); + m_max_refinements = p.get_uint("bound_max_refinements", 16); + m_threshold = p.get_double("bound_threshold", 0.05); + m_small_interval = p.get_double("bound_small_interval", 128); + m_strict2double = p.get_double("strict2double", 0.00001); } void bound_propagator::get_param_descrs(param_descrs & r) { - r.insert(":bound-max-refinements", CPK_UINT, "(default: 16) maximum number of bound refinements (per round) for unbounded variables."); - r.insert(":bound-threshold", CPK_DOUBLE, "(default: 0.05) bound propagation improvement threshold ratio."); + r.insert("bound_max_refinements", CPK_UINT, "(default: 16) maximum number of bound refinements (per round) for unbounded variables."); + r.insert("bound_threshold", CPK_DOUBLE, "(default: 0.05) bound propagation improvement threshold ratio."); } void bound_propagator::collect_statistics(statistics & st) const { diff --git a/src/tactic/arith/bv2int_rewriter.cpp b/src/tactic/arith/bv2int_rewriter.cpp index e8ddf18c9..0965f36f2 100644 --- a/src/tactic/arith/bv2int_rewriter.cpp +++ b/src/tactic/arith/bv2int_rewriter.cpp @@ -21,7 +21,7 @@ Notes: #include "ast_pp.h" void bv2int_rewriter_ctx::update_params(params_ref const& p) { - m_max_size = p.get_uint(":max-bv-size", UINT_MAX); + m_max_size = p.get_uint("max_bv_size", UINT_MAX); } struct lt_rational { diff --git a/src/tactic/arith/diff_neq_tactic.cpp b/src/tactic/arith/diff_neq_tactic.cpp index 93ac6912d..b534c8295 100644 --- a/src/tactic/arith/diff_neq_tactic.cpp +++ b/src/tactic/arith/diff_neq_tactic.cpp @@ -62,7 +62,7 @@ class diff_neq_tactic : public tactic { } void updt_params(params_ref const & p) { - m_max_k = rational(p.get_uint(":diff-neq-max-k", 1024)); + m_max_k = rational(p.get_uint("diff_neq_max_k", 1024)); m_max_neg_k = -m_max_k; if (m_max_k >= rational(INT_MAX/2)) m_max_k = rational(INT_MAX/2); @@ -374,7 +374,7 @@ public: } virtual void collect_param_descrs(param_descrs & r) { - r.insert(":diff-neq-max-k", CPK_UINT, "(default: 1024) maximum variable upper bound for diff neq solver."); + r.insert("diff_neq_max_k", CPK_UINT, "(default: 1024) maximum variable upper bound for diff neq solver."); } virtual void collect_statistics(statistics & st) const { diff --git a/src/tactic/arith/factor_tactic.cpp b/src/tactic/arith/factor_tactic.cpp index 2cfbc9ef8..752f6681d 100644 --- a/src/tactic/arith/factor_tactic.cpp +++ b/src/tactic/arith/factor_tactic.cpp @@ -40,7 +40,7 @@ class factor_tactic : public tactic { } void updt_params(params_ref const & p) { - m_split_factors = p.get_bool(":split-factors", true); + m_split_factors = p.get_bool("split_factors", true); m_fparams.updt_params(p); } @@ -311,7 +311,7 @@ public: } virtual void collect_param_descrs(param_descrs & r) { - r.insert(":split-factors", CPK_BOOL, + r.insert("split_factors", CPK_BOOL, "(default: true) apply simplifications such as (= (* p1 p2) 0) --> (or (= p1 0) (= p2 0))."); polynomial::factor_params::get_param_descrs(r); } diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp index 4796e7f39..c4b7cbaf3 100644 --- a/src/tactic/arith/fm_tactic.cpp +++ b/src/tactic/arith/fm_tactic.cpp @@ -792,13 +792,13 @@ class fm_tactic : public tactic { } void updt_params(params_ref const & p) { - m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX)); - m_fm_real_only = p.get_bool(":fm-real-only", true); - m_fm_limit = p.get_uint(":fm-limit", 5000000); - m_fm_cutoff1 = p.get_uint(":fm-cutoff1", 8); - m_fm_cutoff2 = p.get_uint(":fm-cutoff2", 256); - m_fm_extra = p.get_uint(":fm-extra", 0); - m_fm_occ = p.get_bool(":fm-occ", false); + m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); + m_fm_real_only = p.get_bool("fm_real_only", true); + m_fm_limit = p.get_uint("fm_limit", 5000000); + m_fm_cutoff1 = p.get_uint("fm_cutoff1", 8); + m_fm_cutoff2 = p.get_uint("fm_cutoff2", 256); + m_fm_extra = p.get_uint("fm_extra", 0); + m_fm_occ = p.get_bool("fm_occ", false); } void set_cancel(bool f) { @@ -1668,12 +1668,12 @@ public: virtual void collect_param_descrs(param_descrs & r) { insert_produce_models(r); insert_max_memory(r); - r.insert(":fm-real-only", CPK_BOOL, "(default: true) consider only real variables for fourier-motzkin elimination."); - r.insert(":fm-occ", CPK_BOOL, "(default: false) consider inequalities occurring in clauses for FM."); - r.insert(":fm-limit", CPK_UINT, "(default: 5000000) maximum number of constraints, monomials, clauses visited during FM."); - r.insert(":fm-cutoff1", CPK_UINT, "(default: 8) first cutoff for FM based on maximum number of lower/upper occurrences."); - r.insert(":fm-cutoff2", CPK_UINT, "(default: 256) second cutoff for FM based on num_lower * num_upper occurrences."); - r.insert(":fm-extra", CPK_UINT, "(default: 0) max. increase on the number of inequalities for each FM variable elimination step."); + r.insert("fm_real_only", CPK_BOOL, "(default: true) consider only real variables for fourier-motzkin elimination."); + r.insert("fm_occ", CPK_BOOL, "(default: false) consider inequalities occurring in clauses for FM."); + r.insert("fm_limit", CPK_UINT, "(default: 5000000) maximum number of constraints, monomials, clauses visited during FM."); + r.insert("fm_cutoff1", CPK_UINT, "(default: 8) first cutoff for FM based on maximum number of lower/upper occurrences."); + r.insert("fm_cutoff2", CPK_UINT, "(default: 256) second cutoff for FM based on num_lower * num_upper occurrences."); + r.insert("fm_extra", CPK_UINT, "(default: 0) max. increase on the number of inequalities for each FM variable elimination step."); } virtual void set_cancel(bool f) { @@ -1707,9 +1707,9 @@ public: tactic * mk_fm_tactic(ast_manager & m, params_ref const & p) { params_ref s_p = p; - s_p.set_bool(":arith-lhs", true); - s_p.set_bool(":elim-and", true); - s_p.set_bool(":som", true); + s_p.set_bool("arith_lhs", true); + s_p.set_bool("elim_and", true); + s_p.set_bool("som", true); return and_then(using_params(mk_simplify_tactic(m, s_p), s_p), clean(alloc(fm_tactic, m, p))); } diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp index 871614c1b..6fee55e4b 100644 --- a/src/tactic/arith/lia2pb_tactic.cpp +++ b/src/tactic/arith/lia2pb_tactic.cpp @@ -50,9 +50,9 @@ class lia2pb_tactic : public tactic { } void updt_params_core(params_ref const & p) { - m_partial_lia2pb = p.get_bool(":lia2pb-partial", false); - m_max_bits = p.get_uint(":lia2pb-max-bits", 32); - m_total_bits = p.get_uint(":lia2pb-total-bits", 2048); + m_partial_lia2pb = p.get_bool("lia2pb_partial", false); + m_max_bits = p.get_uint("lia2pb_max_bits", 32); + m_total_bits = p.get_uint("lia2pb_total_bits", 2048); } void updt_params(params_ref const & p) { @@ -325,9 +325,9 @@ public: } virtual void collect_param_descrs(param_descrs & r) { - r.insert(":lia2pb-partial", CPK_BOOL, "(default: false) partial lia2pb conversion."); - r.insert(":lia2pb-max-bits", CPK_UINT, "(default: 32) maximum number of bits to be used (per variable) in lia2pb."); - r.insert(":lia2pb-total-bits", CPK_UINT, "(default: 2048) total number of bits to be used (per problem) in lia2pb."); + r.insert("lia2pb_partial", CPK_BOOL, "(default: false) partial lia2pb conversion."); + r.insert("lia2pb_max_bits", CPK_UINT, "(default: 32) maximum number of bits to be used (per variable) in lia2pb."); + r.insert("lia2pb_total_bits", CPK_UINT, "(default: 2048) total number of bits to be used (per problem) in lia2pb."); } virtual void operator()(goal_ref const & in, diff --git a/src/tactic/arith/nla2bv_tactic.cpp b/src/tactic/arith/nla2bv_tactic.cpp index a9033bcd3..188ea7d70 100644 --- a/src/tactic/arith/nla2bv_tactic.cpp +++ b/src/tactic/arith/nla2bv_tactic.cpp @@ -68,7 +68,7 @@ class nla2bv_tactic : public tactic { m_is_sat_preserving(true), m_arith(m), m_bv(m), - m_bv2real(m, rational(p.get_uint(":nla2bv-root",2)), rational(p.get_uint(":nla2bv-divisor",2)), p.get_uint(":nla2bv-max-bv-size", UINT_MAX)), + m_bv2real(m, rational(p.get_uint("nla2bv_root",2)), rational(p.get_uint("nla2bv_divisor",2)), p.get_uint("nla2bv_max_bv_size", UINT_MAX)), m_bv2int_ctx(m, p), m_bounds(m), m_subst(m), @@ -76,7 +76,7 @@ class nla2bv_tactic : public tactic { m_defs(m), m_trail(m), m_fmc(0) { - m_default_bv_size = m_num_bits = p.get_uint(":nla2bv-bv-size", 4); + m_default_bv_size = m_num_bits = p.get_uint("nla2bv_bv_size", 4); } ~imp() {} @@ -436,10 +436,10 @@ public: } virtual void collect_param_descrs(param_descrs & r) { - r.insert(":nla2bv-max-bv-size", CPK_UINT, "(default: inf) maximum bit-vector size used by nla2bv tactic"); - r.insert(":nla2bv-bv-size", CPK_UINT, "(default: 4) default bit-vector size used by nla2bv tactic."); - r.insert(":nla2bv-root", CPK_UINT, "(default: 2) nla2bv tactic encodes reals into bit-vectors using expressions of the form a+b*sqrt(c), this parameter sets the value of c used in the encoding."); - r.insert(":nla2bv-divisor", CPK_UINT, "(default: 2) nla2bv tactic parameter."); + r.insert("nla2bv_max_bv_size", CPK_UINT, "(default: inf) maximum bit-vector size used by nla2bv tactic"); + r.insert("nla2bv_bv_size", CPK_UINT, "(default: 4) default bit-vector size used by nla2bv tactic."); + r.insert("nla2bv_root", CPK_UINT, "(default: 2) nla2bv tactic encodes reals into bit-vectors using expressions of the form a+b*sqrt(c), this parameter sets the value of c used in the encoding."); + r.insert("nla2bv_divisor", CPK_UINT, "(default: 2) nla2bv tactic parameter."); } /** diff --git a/src/tactic/arith/normalize_bounds_tactic.cpp b/src/tactic/arith/normalize_bounds_tactic.cpp index f7aa968ef..a62b311b5 100644 --- a/src/tactic/arith/normalize_bounds_tactic.cpp +++ b/src/tactic/arith/normalize_bounds_tactic.cpp @@ -44,7 +44,7 @@ class normalize_bounds_tactic : public tactic { } void updt_params_core(params_ref const & p) { - m_normalize_int_only = p.get_bool(":norm-int-only", true); + m_normalize_int_only = p.get_bool("norm_int_only", true); } void updt_params(params_ref const & p) { @@ -173,7 +173,7 @@ public: virtual void collect_param_descrs(param_descrs & r) { insert_produce_models(r); - r.insert(":norm-int-only", CPK_BOOL, "(default: true) normalize only the bounds of integer constants."); + r.insert("norm_int_only", CPK_BOOL, "(default: true) normalize only the bounds of integer constants."); } virtual void operator()(goal_ref const & in, diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp index 36cc801dc..8790ca5a7 100644 --- a/src/tactic/arith/pb2bv_tactic.cpp +++ b/src/tactic/arith/pb2bv_tactic.cpp @@ -863,15 +863,15 @@ private: } void updt_params(params_ref const & p) { - m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX)); - m_all_clauses_limit = p.get_uint(":pb2bv-all-clauses-limit", 8); - m_cardinality_limit = p.get_uint(":pb2bv-cardinality-limit", UINT_MAX); + m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); + m_all_clauses_limit = p.get_uint("pb2bv_all_clauses_limit", 8); + m_cardinality_limit = p.get_uint("pb2bv_cardinality_limit", UINT_MAX); } void collect_param_descrs(param_descrs & r) { insert_max_memory(r); - r.insert(":pb2bv-all-clauses-limit", CPK_UINT, "(default: 8) maximum number of literals for using equivalent CNF encoding of PB constraint."); - r.insert(":pb2bv-cardinality-limit", CPK_UINT, "(default: inf) limit for using arc-consistent cardinality constraint encoding."); + r.insert("pb2bv_all_clauses_limit", CPK_UINT, "(default: 8) maximum number of literals for using equivalent CNF encoding of PB constraint."); + r.insert("pb2bv_cardinality_limit", CPK_UINT, "(default: inf) limit for using arc-consistent cardinality constraint encoding."); } void set_cancel(bool f) { diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index 4bea07269..d6ed86c08 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -856,11 +856,11 @@ public: } virtual void collect_param_descrs(param_descrs & r) { - r.insert(":complete", CPK_BOOL, + r.insert("complete", CPK_BOOL, "(default: true) add constraints to make sure that any interpretation of a underspecified arithmetic operators is a functio. The result will include additional uninterpreted functions/constants: /0, div0, mod0, 0^0, neg-root"); - r.insert(":elim-root-objects", CPK_BOOL, + r.insert("elim_root_objects", CPK_BOOL, "(default: true) eliminate root objects."); - r.insert(":elim-inverses", CPK_BOOL, + r.insert("elim_inverses", CPK_BOOL, "(default: true) eliminate inverse trigonometric functions (asin, acos, atan)."); th_rewriter::get_param_descrs(r); } @@ -876,9 +876,9 @@ public: tactic_report report("purify-arith", *g); bool produce_proofs = g->proofs_enabled(); bool produce_models = g->models_enabled(); - bool elim_root_objs = m_params.get_bool(":elim-root-objects", true); - bool elim_inverses = m_params.get_bool(":elim-inverses", true); - bool complete = m_params.get_bool(":complete", true); + bool elim_root_objs = m_params.get_bool("elim_root_objects", true); + bool elim_inverses = m_params.get_bool("elim_inverses", true); + bool complete = m_params.get_bool("complete", true); purify_arith_proc proc(m_util, m_aux_decls, produce_proofs, elim_root_objs, elim_inverses, complete); proc(*(g.get()), mc, produce_models); @@ -902,10 +902,10 @@ public: tactic * mk_purify_arith_tactic(ast_manager & m, params_ref const & p) { params_ref elim_rem_p = p; - elim_rem_p.set_bool(":elim-rem", true); + elim_rem_p.set_bool("elim-rem", true); params_ref skolemize_p; - skolemize_p.set_bool(":skolemize", false); + skolemize_p.set_bool("skolemize", false); return and_then(using_params(mk_snf_tactic(m, skolemize_p), skolemize_p), using_params(mk_simplify_tactic(m, elim_rem_p), elim_rem_p), diff --git a/src/tactic/arith/recover_01_tactic.cpp b/src/tactic/arith/recover_01_tactic.cpp index a42bedc44..3b1a86345 100644 --- a/src/tactic/arith/recover_01_tactic.cpp +++ b/src/tactic/arith/recover_01_tactic.cpp @@ -58,7 +58,7 @@ class recover_01_tactic : public tactic { } void updt_params_core(params_ref const & p) { - m_cls_max_size = p.get_uint(":recover-01-max-bits", 10); + m_cls_max_size = p.get_uint("recover_01_max_bits", 10); } void updt_params(params_ref const & p) { @@ -408,7 +408,7 @@ public: virtual void collect_param_descrs(param_descrs & r) { th_rewriter::get_param_descrs(r); - r.insert(":recover-01-max-bits", CPK_UINT, "(default: 10) maximum number of bits to consider in a clause."); + r.insert("recover_01_max_bits", CPK_UINT, "(default: 10) maximum number of bits to consider in a clause."); } void operator()(goal_ref const & g, diff --git a/src/tactic/bv/bit_blaster_tactic.cpp b/src/tactic/bv/bit_blaster_tactic.cpp index 63d534cbb..0330141cb 100644 --- a/src/tactic/bv/bit_blaster_tactic.cpp +++ b/src/tactic/bv/bit_blaster_tactic.cpp @@ -36,7 +36,7 @@ class bit_blaster_tactic : public tactic { } void updt_params_core(params_ref const & p) { - m_blast_quant = p.get_bool(":blast-quant", false); + m_blast_quant = p.get_bool("blast_quant", false); } void updt_params(params_ref const & p) { @@ -120,10 +120,10 @@ public: virtual void collect_param_descrs(param_descrs & r) { insert_max_memory(r); insert_max_steps(r); - r.insert(":blast-mul", CPK_BOOL, "(default: true) bit-blast multipliers (and dividers, remainders)."); - r.insert(":blast-add", CPK_BOOL, "(default: true) bit-blast adders."); - r.insert(":blast-quant", CPK_BOOL, "(default: false) bit-blast quantified variables."); - r.insert(":blast-full", CPK_BOOL, "(default: false) bit-blast any term with bit-vector sort, this option will make E-matching ineffective in any pattern containing bit-vector terms."); + r.insert("blast_mul", CPK_BOOL, "(default: true) bit-blast multipliers (and dividers, remainders)."); + r.insert("blast_add", CPK_BOOL, "(default: true) bit-blast adders."); + r.insert("blast_quant", CPK_BOOL, "(default: false) bit-blast quantified variables."); + r.insert("blast_full", CPK_BOOL, "(default: false) bit-blast any term with bit-vector sort, this option will make E-matching ineffective in any pattern containing bit-vector terms."); } virtual void operator()(goal_ref const & g, diff --git a/src/tactic/bv/bv1_blaster_tactic.cpp b/src/tactic/bv/bv1_blaster_tactic.cpp index 77ab1be31..8dcaf2112 100644 --- a/src/tactic/bv/bv1_blaster_tactic.cpp +++ b/src/tactic/bv/bv1_blaster_tactic.cpp @@ -63,9 +63,9 @@ class bv1_blaster_tactic : public tactic { } void updt_params(params_ref const & p) { - m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX)); - m_max_steps = p.get_uint(":max-steps", UINT_MAX); - m_produce_models = p.get_bool(":produce-models", false); + m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); + m_max_steps = p.get_uint("max_steps", UINT_MAX); + m_produce_models = p.get_bool("produce_models", false); } bool rewrite_patterns() const { UNREACHABLE(); return false; } diff --git a/src/tactic/bv/max_bv_sharing_tactic.cpp b/src/tactic/bv/max_bv_sharing_tactic.cpp index 462c9f3e2..251e2b754 100644 --- a/src/tactic/bv/max_bv_sharing_tactic.cpp +++ b/src/tactic/bv/max_bv_sharing_tactic.cpp @@ -55,9 +55,9 @@ class max_bv_sharing_tactic : public tactic { } void updt_params(params_ref const & p) { - m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX)); - m_max_steps = p.get_uint(":max-steps", UINT_MAX); - m_max_args = p.get_uint(":max-args", 128); + m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); + m_max_steps = p.get_uint("max_steps", UINT_MAX); + m_max_args = p.get_uint("max_args", 128); } bool max_steps_exceeded(unsigned num_steps) const { @@ -298,7 +298,7 @@ public: virtual void collect_param_descrs(param_descrs & r) { insert_max_memory(r); insert_max_steps(r); - r.insert(":max-args", CPK_UINT, + r.insert("max_args", CPK_UINT, "(default: 128) maximum number of arguments (per application) that will be considered by the greedy (quadratic) heuristic."); } diff --git a/src/tactic/core/cofactor_elim_term_ite.cpp b/src/tactic/core/cofactor_elim_term_ite.cpp index b39d82201..78d532357 100644 --- a/src/tactic/core/cofactor_elim_term_ite.cpp +++ b/src/tactic/core/cofactor_elim_term_ite.cpp @@ -304,7 +304,7 @@ struct cofactor_elim_term_ite::imp { } void updt_params(params_ref const & p) { - m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX)); + m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); } void set_cancel(bool f) { diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp index 91334fd5c..cca21b90e 100644 --- a/src/tactic/core/ctx_simplify_tactic.cpp +++ b/src/tactic/core/ctx_simplify_tactic.cpp @@ -90,10 +90,10 @@ struct ctx_simplify_tactic::imp { } void updt_params(params_ref const & p) { - m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX)); - m_max_steps = p.get_uint(":max-steps", UINT_MAX); - m_max_depth = p.get_uint(":max-depth", 1024); - m_bail_on_blowup = p.get_bool(":bail-on-blowup", false); + m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); + m_max_steps = p.get_uint("max_steps", UINT_MAX); + m_max_depth = p.get_uint("max_depth", 1024); + m_bail_on_blowup = p.get_bool("bail_on_blowup", false); } void checkpoint() { @@ -519,7 +519,7 @@ void ctx_simplify_tactic::updt_params(params_ref const & p) { void ctx_simplify_tactic::get_param_descrs(param_descrs & r) { insert_max_memory(r); insert_max_steps(r); - r.insert(":max-depth", CPK_UINT, "(default: 1024) maximum term depth."); + r.insert("max_depth", CPK_UINT, "(default: 1024) maximum term depth."); } void ctx_simplify_tactic::operator()(goal_ref const & in, diff --git a/src/tactic/core/elim_term_ite_tactic.cpp b/src/tactic/core/elim_term_ite_tactic.cpp index 4f04859ac..456bad5e0 100644 --- a/src/tactic/core/elim_term_ite_tactic.cpp +++ b/src/tactic/core/elim_term_ite_tactic.cpp @@ -72,7 +72,7 @@ class elim_term_ite_tactic : public tactic { } void updt_params(params_ref const & p) { - m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX)); + m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); } }; @@ -160,7 +160,7 @@ public: virtual void collect_param_descrs(param_descrs & r) { insert_max_memory(r); insert_max_steps(r); - r.insert(":max-args", CPK_UINT, + r.insert("max_args", CPK_UINT, "(default: 128) maximum number of arguments (per application) that will be considered by the greedy (quadratic) heuristic."); } diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index 7d15bc7c0..d1dca296a 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -881,8 +881,8 @@ class elim_uncnstr_tactic : public tactic { } void updt_params(params_ref const & p) { - m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX)); - m_max_steps = p.get_uint(":max-steps", UINT_MAX); + m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); + m_max_steps = p.get_uint("max_steps", UINT_MAX); } ast_manager & m() { return m_manager; } diff --git a/src/tactic/core/nnf_tactic.cpp b/src/tactic/core/nnf_tactic.cpp index 157c7078e..fdaf03d55 100644 --- a/src/tactic/core/nnf_tactic.cpp +++ b/src/tactic/core/nnf_tactic.cpp @@ -120,7 +120,7 @@ tactic * mk_snf_tactic(ast_manager & m, params_ref const & p) { tactic * mk_nnf_tactic(ast_manager & m, params_ref const & p) { params_ref new_p(p); - new_p.set_sym(":nnf-mode", symbol("full")); + new_p.set_sym("nnf_mode", symbol("full")); TRACE("nnf", tout << "mk_nnf: " << new_p << "\n";); return using_params(mk_snf_tactic(m, p), new_p); } diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp index 9ab597dfa..6d9e6ccbd 100644 --- a/src/tactic/core/propagate_values_tactic.cpp +++ b/src/tactic/core/propagate_values_tactic.cpp @@ -44,7 +44,7 @@ class propagate_values_tactic : public tactic { } void updt_params_core(params_ref const & p) { - m_max_rounds = p.get_uint(":max-rounds", 4); + m_max_rounds = p.get_uint("max_rounds", 4); } void updt_params(params_ref const & p) { @@ -237,7 +237,7 @@ public: virtual void collect_param_descrs(param_descrs & r) { th_rewriter::get_param_descrs(r); - r.insert(":max-rounds", CPK_UINT, "(default: 2) maximum number of rounds."); + r.insert("max_rounds", CPK_UINT, "(default: 2) maximum number of rounds."); } virtual void operator()(goal_ref const & in, diff --git a/src/tactic/core/simplify_tactic.cpp b/src/tactic/core/simplify_tactic.cpp index 0408f8c8d..95db962a7 100644 --- a/src/tactic/core/simplify_tactic.cpp +++ b/src/tactic/core/simplify_tactic.cpp @@ -138,7 +138,7 @@ tactic * mk_simplify_tactic(ast_manager & m, params_ref const & p) { tactic * mk_elim_and_tactic(ast_manager & m, params_ref const & p) { params_ref xp = p; - xp.set_bool(":elim-and", true); + xp.set_bool("elim_and", true); return using_params(mk_simplify_tactic(m, xp), xp); } diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp index aa8fb03c2..995940406 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/src/tactic/core/solve_eqs_tactic.cpp @@ -71,9 +71,9 @@ class solve_eqs_tactic : public tactic { ast_manager & m() const { return m_manager; } void updt_params(params_ref const & p) { - m_ite_solver = p.get_bool(":ite-solver", true); - m_theory_solver = p.get_bool(":theory-solver", true); - m_max_occs = p.get_uint(":solve-eqs-max-occs", UINT_MAX); + m_ite_solver = p.get_bool("ite_solver", true); + m_theory_solver = p.get_bool("theory_solver", true); + m_max_occs = p.get_uint("solve_eqs_max_occs", UINT_MAX); } void set_cancel(bool f) { @@ -732,9 +732,9 @@ public: } virtual void collect_param_descrs(param_descrs & r) { - r.insert(":solve-eqs-max-occs", CPK_UINT, "(default: infty) maximum number of occurrences for considering a variable for gaussian eliminations."); - r.insert(":theory-solver", CPK_BOOL, "(default: true) use theory solvers."); - r.insert(":ite-solver", CPK_BOOL, "(default: true) use if-then-else solver."); + r.insert("solve_eqs_max_occs", CPK_UINT, "(default: infty) maximum number of occurrences for considering a variable for gaussian eliminations."); + r.insert("theory_solver", CPK_BOOL, "(default: true) use theory solvers."); + r.insert("ite_solver", CPK_BOOL, "(default: true) use if-then-else solver."); } virtual void operator()(goal_ref const & in, diff --git a/src/tactic/core/split_clause_tactic.cpp b/src/tactic/core/split_clause_tactic.cpp index f259ca8ad..5699aa178 100644 --- a/src/tactic/core/split_clause_tactic.cpp +++ b/src/tactic/core/split_clause_tactic.cpp @@ -96,11 +96,11 @@ public: } virtual void updt_params(params_ref const & p) { - m_largest_clause = p.get_bool(":split-largest-clause", false); + m_largest_clause = p.get_bool("split_largest_clause", false); } virtual void collect_param_descrs(param_descrs & r) { - r.insert(":split-largest-clause", CPK_BOOL, "(default: false) split the largest clause in the goal."); + r.insert("split_largest_clause", CPK_BOOL, "(default: false) split the largest clause in the goal."); } virtual void operator()(goal_ref const & in, diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp index 2a4f3df2e..b6c4b0655 100644 --- a/src/tactic/core/tseitin_cnf_tactic.cpp +++ b/src/tactic/core/tseitin_cnf_tactic.cpp @@ -122,12 +122,12 @@ class tseitin_cnf_tactic : public tactic { } void updt_params(params_ref const & p) { - m_common_patterns = p.get_bool(":common-patterns", true); - m_distributivity = p.get_bool(":distributivity", true); - m_distributivity_blowup = p.get_uint(":distributivity-blowup", 32); - m_ite_chains = p.get_bool(":ite-chains", true); - m_ite_extra = p.get_bool(":ite-extra", true); - m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX)); + m_common_patterns = p.get_bool("common_patterns", true); + m_distributivity = p.get_bool("distributivity", true); + m_distributivity_blowup = p.get_uint("distributivity_blowup", 32); + m_ite_chains = p.get_bool("ite_chains", true); + m_ite_extra = p.get_bool("ite_extra", true); + m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); } void push_frame(app * n) { m_frame_stack.push_back(frame(n)); } @@ -881,11 +881,11 @@ public: virtual void collect_param_descrs(param_descrs & r) { insert_max_memory(r); - r.insert(":common-patterns", CPK_BOOL, "(default: true) minimize the number of auxiliary variables during CNF encoding by identifing commonly used patterns"); - r.insert(":distributivity", CPK_BOOL, "(default: true) minimize the number of auxiliary variables during CNF encoding by applying distributivity over unshared subformulas"); - r.insert(":distributivity-blowup", CPK_UINT, "(default: 32) maximum overhead for applying distributivity during CNF encoding"); - r.insert("ite-chaing", CPK_BOOL, "(default: true) minimize the number of auxiliary variables during CNF encoding by identifing if-then-else chains"); - r.insert(":ite-extra", CPK_BOOL, "(default: true) add redundant clauses (that improve unit propagation) when encoding if-then-else formulas"); + r.insert("common_patterns", CPK_BOOL, "(default: true) minimize the number of auxiliary variables during CNF encoding by identifing commonly used patterns"); + r.insert("distributivity", CPK_BOOL, "(default: true) minimize the number of auxiliary variables during CNF encoding by applying distributivity over unshared subformulas"); + r.insert("distributivity_blowup", CPK_UINT, "(default: 32) maximum overhead for applying distributivity during CNF encoding"); + r.insert("ite_chaing", CPK_BOOL, "(default: true) minimize the number of auxiliary variables during CNF encoding by identifing if-then-else chains"); + r.insert("ite_extra", CPK_BOOL, "(default: true) add redundant clauses (that improve unit propagation) when encoding if-then-else formulas"); } virtual void operator()(goal_ref const & in, @@ -934,8 +934,8 @@ tactic * mk_tseitin_cnf_core_tactic(ast_manager & m, params_ref const & p) { tactic * mk_tseitin_cnf_tactic(ast_manager & m, params_ref const & p) { params_ref simp_p = p; - simp_p.set_bool(":elim-and", true); - simp_p.set_bool(":blast-distinct", true); + simp_p.set_bool("elim_and", true); + simp_p.set_bool("blast_distinct", true); return or_else(mk_tseitin_cnf_core_tactic(m, p), and_then(using_params(mk_simplify_tactic(m, p), simp_p), mk_tseitin_cnf_core_tactic(m, p))); diff --git a/src/tactic/fpa/fpa2bv_rewriter.h b/src/tactic/fpa/fpa2bv_rewriter.h index 62c6f1a2d..02a667f18 100644 --- a/src/tactic/fpa/fpa2bv_rewriter.h +++ b/src/tactic/fpa/fpa2bv_rewriter.h @@ -54,8 +54,8 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { } void updt_params(params_ref const & p) { - m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX)); - m_max_steps = p.get_uint(":max-steps", UINT_MAX); + m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); + m_max_steps = p.get_uint("max_steps", UINT_MAX); } bool max_steps_exceeded(unsigned num_steps) const { diff --git a/src/tactic/fpa/qffpa_tactic.cpp b/src/tactic/fpa/qffpa_tactic.cpp index d034000c4..f3c913ccc 100644 --- a/src/tactic/fpa/qffpa_tactic.cpp +++ b/src/tactic/fpa/qffpa_tactic.cpp @@ -26,7 +26,7 @@ Notes: tactic * mk_qffpa_tactic(ast_manager & m, params_ref const & p) { params_ref sat_simp_p = p; - sat_simp_p .set_bool(":elim-and", true); + sat_simp_p .set_bool("elim_and", true); return and_then(mk_simplify_tactic(m, p), mk_fpa2bv_tactic(m, p), diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index 0ad845095..290a0ad35 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -1363,16 +1363,16 @@ class sls_tactic : public tactic { static void collect_param_descrs(param_descrs & r) { insert_produce_models(r); - r.insert(":sls-restarts", CPK_UINT, "(default: infty) # of SLS restarts."); - r.insert(":random-seed", CPK_UINT, "(default: 0) random seed."); - r.insert(":plateau-limit", CPK_UINT, "(default: 100) SLS plateau limit."); + r.insert("sls_restarts", CPK_UINT, "(default: infty) # of SLS restarts."); + r.insert("random_seed", CPK_UINT, "(default: 0) random seed."); + r.insert("plateau_limit", CPK_UINT, "(default: 100) SLS plateau limit."); } void updt_params(params_ref const & p) { - m_produce_models = p.get_bool(":produce-models", false); - m_max_restarts = p.get_uint(":sls-restarts", -1); - m_tracker.set_random_seed(p.get_uint(":random-seed", 0)); - m_plateau_limit = p.get_uint(":plateau-limit", 100); + m_produce_models = p.get_bool("produce_models", false); + m_max_restarts = p.get_uint("sls_restarts", -1); + m_tracker.set_random_seed(p.get_uint("random_seed", 0)); + m_plateau_limit = p.get_uint("plateau_limit", 100); } void checkpoint() { @@ -1854,28 +1854,28 @@ tactic * mk_sls_tactic(ast_manager & m, params_ref const & p) { tactic * mk_preamble(ast_manager & m, params_ref const & p) { params_ref main_p; - main_p.set_bool(":elim-and", true); - // main_p.set_bool(":pull-cheap-ite", true); - main_p.set_bool(":push-ite-bv", true); - main_p.set_bool(":blast-distinct", true); - // main_p.set_bool(":udiv2mul", true); - main_p.set_bool(":hi-div0", true); + main_p.set_bool("elim_and", true); + // main_p.set_bool("pull-cheap_ite", true); + main_p.set_bool("push_ite_bv", true); + main_p.set_bool("blast_distinct", true); + // main_p.set_bool("udiv2mul", true); + main_p.set_bool("hi_div0", true); params_ref simp2_p = p; - simp2_p.set_bool(":som", true); - simp2_p.set_bool(":pull-cheap-ite", true); - simp2_p.set_bool(":push-ite-bv", false); - simp2_p.set_bool(":local-ctx", true); - simp2_p.set_uint(":local-ctx-limit", 10000000); + simp2_p.set_bool("som", true); + simp2_p.set_bool("pull_cheap_ite", true); + simp2_p.set_bool("push_ite_bv", false); + simp2_p.set_bool("local_ctx", true); + simp2_p.set_uint("local_ctx_limit", 10000000); params_ref hoist_p; - hoist_p.set_bool(":hoist-mul", true); - // hoist_p.set_bool(":hoist-cmul", true); - hoist_p.set_bool(":som", false); + hoist_p.set_bool("hoist_mul", true); + // hoist_p.set_bool("hoist_cmul", true); + hoist_p.set_bool("som", false); params_ref gaussian_p; // conservative gaussian elimination. - gaussian_p.set_uint(":gaussian-max-occs", 2); + gaussian_p.set_uint("gaussian_max_occs", 2); return and_then(and_then(mk_simplify_tactic(m), mk_propagate_values_tactic(m), @@ -1890,8 +1890,8 @@ tactic * mk_preamble(ast_manager & m, params_ref const & p) { tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p) { params_ref sls_p(p); - sls_p.set_uint(":sls-restarts", 10000); - sls_p.set_uint(":plateau-limit", 100); + sls_p.set_uint("sls_restarts", 10000); + sls_p.set_uint("plateau_limit", 100); tactic * t = and_then(mk_preamble(m, p), using_params(mk_sls_tactic(m, p), sls_p)); diff --git a/src/tactic/smtlogics/qfnra_tactic.cpp b/src/tactic/smtlogics/qfnra_tactic.cpp index d13d9e198..a2877eefa 100644 --- a/src/tactic/smtlogics/qfnra_tactic.cpp +++ b/src/tactic/smtlogics/qfnra_tactic.cpp @@ -25,7 +25,7 @@ Notes: static tactic * mk_qfnra_sat_solver(ast_manager& m, params_ref const& p, unsigned bv_size) { params_ref nra2sat_p = p; - nra2sat_p.set_uint(":nla2bv-max-bv-size", p.get_uint(":nla2bv-max-bv-size", bv_size)); + nra2sat_p.set_uint(":nla2bv-max-bv-size", p.get_uint("nla2bv_max_bv_size", bv_size)); return and_then(mk_nla2bv_tactic(m, nra2sat_p), mk_smt_tactic(), diff --git a/src/tactic/smtlogics/quant_tactics.cpp b/src/tactic/smtlogics/quant_tactics.cpp index 157202442..4bb896c74 100644 --- a/src/tactic/smtlogics/quant_tactics.cpp +++ b/src/tactic/smtlogics/quant_tactics.cpp @@ -72,7 +72,7 @@ tactic * mk_uflra_tactic(ast_manager & m, params_ref const & p) { tactic * mk_auflia_tactic(ast_manager & m, params_ref const & p) { params_ref qi_p; qi_p.set_str(":qi-cost", "0"); - TRACE("qi_cost", qi_p.display(tout); tout << "\n" << qi_p.get_str(":qi-cost", "") << "\n";); + TRACE("qi_cost", qi_p.display(tout); tout << "\n" << qi_p.get_str("qi_cost", "") << "\n";); tactic * st = and_then(mk_no_solve_eq_preprocessor(m), or_else(and_then(fail_if(mk_gt(mk_num_exprs_probe(), mk_const_probe(static_cast(128)))), using_params(mk_smt_tactic(), qi_p), diff --git a/src/tactic/ufbv/macro_finder_tactic.cpp b/src/tactic/ufbv/macro_finder_tactic.cpp index 3872a3a2e..14a42ec51 100644 --- a/src/tactic/ufbv/macro_finder_tactic.cpp +++ b/src/tactic/ufbv/macro_finder_tactic.cpp @@ -102,7 +102,7 @@ class macro_finder_tactic : public tactic { } void updt_params(params_ref const & p) { - m_elim_and = p.get_bool(":elim-and", false); + m_elim_and = p.get_bool("elim_and", false); } }; @@ -131,7 +131,7 @@ public: insert_max_memory(r); insert_produce_models(r); insert_produce_proofs(r); - r.insert(":elim-and", CPK_BOOL, "(default: false) eliminate conjunctions during (internal) calls to the simplifier."); + r.insert("elim_and", CPK_BOOL, "(default: false) eliminate conjunctions during (internal) calls to the simplifier."); } virtual void operator()(goal_ref const & in, diff --git a/src/test/dl_product_relation.cpp b/src/test/dl_product_relation.cpp index 2711f3e00..ac895dacf 100644 --- a/src/test/dl_product_relation.cpp +++ b/src/test/dl_product_relation.cpp @@ -128,7 +128,7 @@ namespace datalog { dl_decl_util dl_util(m); relation_manager & rmgr = ctx.get_rmanager(); - relation_plugin & rel_plugin = *ctx.get_rmanager().get_relation_plugin(params.get_sym(":default-relation", symbol("sparse"))); + relation_plugin & rel_plugin = *ctx.get_rmanager().get_relation_plugin(params.get_sym("default_relation", symbol("sparse"))); SASSERT(&rel_plugin); finite_product_relation_plugin plg(rel_plugin, rmgr); diff --git a/src/util/double_manager.h b/src/util/double_manager.h index a6a72cc6f..5334e60df 100644 --- a/src/util/double_manager.h +++ b/src/util/double_manager.h @@ -40,7 +40,7 @@ public: double_manager(params_ref const & p = params_ref()) { updt_params(p); } void updt_params(params_ref const & p) { - m_zero_tolerance = p.get_double(":zero-tolerance", 0.00000001); + m_zero_tolerance = p.get_double("zero_tolerance", 0.00000001); } static void reset(double & a) { a = 0.0; } diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp new file mode 100644 index 000000000..556e84734 --- /dev/null +++ b/src/util/gparams.cpp @@ -0,0 +1,249 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + gparams.cpp + +Abstract: + + Global parameter management. + +Author: + + Leonardo (leonardo) 2012-11-29 + +Notes: + +--*/ +#include"gparams.h" +#include"dictionary.h" + +extern void gparams_register_modules(); + +struct gparams::imp { + dictionary m_module_param_descrs; + param_descrs m_param_descrs; + dictionary m_module_params; + params_ref m_params; + params_ref m_empty; +public: + imp() { + } + + ~imp() { + { + dictionary::iterator it = m_module_param_descrs.begin(); + dictionary::iterator end = m_module_param_descrs.end(); + for (; it != end; ++it) { + dealloc(it->m_value); + } + } + { + dictionary::iterator it = m_module_params.begin(); + dictionary::iterator end = m_module_params.end(); + for (; it != end; ++it) { + dealloc(it->m_value); + } + } + } + + void register_global(param_descrs & d) { + m_param_descrs.copy(d); + } + + void register_module(char const * module_name, param_descrs * d) { + 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 display(std::ostream & out, unsigned indent, bool smt2_style) { + m_param_descrs.display(out, indent, smt2_style); + 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 << "\n"; + it->m_value->display(out, indent + 4, smt2_style); + } + } + + void normalize(char const * name, /* out */ symbol & mod_name, /* out */ symbol & param_name) { + if (*name == ':') + name++; + std::string tmp = name; + unsigned n = tmp.size(); + for (unsigned i = 0; i < n; i++) { + if (tmp[i] >= 'A' && tmp[i] <= 'Z') + tmp[i] = tmp[i] - 'A' + 'a'; + else if (tmp[i] == '-') + tmp[i] = '_'; + } + for (unsigned i = 0; i < n; i++) { + if (tmp[i] == '.') { + param_name = tmp.substr(i+1).c_str(); + tmp.resize(i); + mod_name = tmp.c_str(); + return; + } + } + param_name = tmp.c_str(); + mod_name = symbol::null; + } + + params_ref & get_params(symbol const & mod_name) { + if (mod_name == symbol::null) { + return m_params; + } + else { + params_ref * p; + if (m_module_params.find(mod_name, p)) { + return *p; + } + else { + p = alloc(params_ref); + m_module_params.insert(mod_name, p); + return *p; + } + } + } + + void set(param_descrs const & d, symbol const & param_name, char const * value, symbol const & mod_name) { + param_kind k = d.get_kind(param_name); + params_ref & ps = get_params(mod_name); + if (k == CPK_INVALID) { + if (mod_name == symbol::null) + throw default_exception("unknown parameter '%s'", param_name.bare_str()); + else + throw default_exception("unknown parameter '%s' at module '%s'", param_name.bare_str(), mod_name.bare_str()); + } + else if (k == CPK_UINT) { + long val = strtol(value, 0, 10); + ps.set_uint(param_name, static_cast(val)); + } + else if (k == CPK_BOOL) { + if (strcmp(value, "true") == 0) { + ps.set_bool(param_name, true); + } + else if (strcmp(value, "false") == 0) { + ps.set_bool(param_name, false); + } + else { + if (mod_name == symbol::null) + throw default_exception("invalid value '%s' for Boolean parameter '%s'", value, param_name.bare_str()); + else + throw default_exception("invalid value '%s' for Boolean parameter '%s' at module '%s'", value, param_name.bare_str(), mod_name.bare_str()); + } + } + else if (k == CPK_SYMBOL) { + ps.set_sym(param_name, symbol(value)); + } + else if (k == CPK_STRING) { + ps.set_str(param_name, value); + } + else { + if (mod_name == symbol::null) + throw default_exception("unsupported parameter type '%s'", param_name.bare_str()); + else + throw default_exception("unsupported parameter type '%s' at module '%s'", param_name.bare_str(), mod_name.bare_str()); + } + } + + void set(char const * name, char const * value) { + symbol m, p; + normalize(name, m, p); + if (m == symbol::null) { + set(m_param_descrs, p, value, m); + } + else { + param_descrs * d; + if (m_module_param_descrs.find(m, d)) { + set(*d, p, value, m); + } + else { + throw default_exception("invalid parameter, unknown module '%s'", m.bare_str()); + } + } + } + + std::string get_value(char const * name) { + + } + + + params_ref const & get_module(symbol const & module_name) { + params_ref * ps = 0; + if (m_module_params.find(module_name, ps)) { + return *ps; + } + else { + return m_empty; + } + } + + params_ref const & get() { + return m_params; + } + +}; + +gparams::imp * gparams::g_imp = 0; + +void gparams::set(char const * name, char const * value) { + SASSERT(g_imp != 0); + g_imp->set(name, value); +} + +std::string gparams::get_value(char const * name) { + SASSERT(g_imp != 0); + g_imp->get_value(name); +} + +void gparams::register_global(param_descrs & d) { + SASSERT(g_imp != 0); + g_imp->register_global(d); +} + +void gparams::register_module(char const * module_name, param_descrs * d) { + SASSERT(g_imp != 0); + g_imp->register_module(module_name, d); +} + +params_ref const & gparams::get_module(char const * module_name) { + return get_module(symbol(module_name)); +} + +params_ref const & gparams::get_module(symbol const & module_name) { + SASSERT(g_imp != 0); + return g_imp->get_module(module_name); +} + +params_ref const & gparams::get() { + SASSERT(g_imp != 0); + return g_imp->get(); +} + +void gparams::display(std::ostream & out, unsigned indent, bool smt2_style) { + SASSERT(g_imp != 0); + g_imp->display(out, indent, smt2_style); +} + +void gparams::init() { + g_imp = alloc(imp); + gparams_register_modules(); +} + +void gparams::finalize() { + if (g_imp != 0) { + dealloc(g_imp); + g_imp = 0; + } +} + + diff --git a/src/util/gparams.h b/src/util/gparams.h new file mode 100644 index 000000000..e02a8daa8 --- /dev/null +++ b/src/util/gparams.h @@ -0,0 +1,122 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + gparams.h + +Abstract: + + Global parameter management. + +Author: + + Leonardo (leonardo) 2012-11-29 + +Notes: + +--*/ +#ifndef _GPARAMS_H_ +#define _GPARAMS_H_ + +#include"params.h" + +class gparams { + struct imp; + static imp * g_imp; + typedef z3_exception exception; +public: + /** + \brief Set a global parameter \c name with \c value. + + The name of parameter can be composed of characters [a-z][A-Z], digits [0-9], '-' and '_'. + The character '.' is used a delimiter (more later). + + The parameter names are case-insensitive. The character '-' should be viewed as an "alias" for '_'. + Thus, the following parameter names are considered equivalent: "auto-config" and "AUTO_CONFIG". + + This function can be used to set parameters for a specific Z3 module. + This can be done by using .. + For example: + set_global_param('pp.decimal', 'true') + will set the parameter "decimal" in the module "pp" to true. + + An exception is thrown if the the parameter name is unknown, or if the value is incorrect. + */ + static void set(char const * name, char const * value); + + /** + \brief Auxiliary method used to implement get-option in SMT 2.0 front-end. + + If the parameter is not set, then it just returns 'default'. + + An exception is thrown if the the parameter name is unknown. + */ + static std::string get_value(char const * name); + + /** + \brief Register additional global parameters + + This is an auxiliary function used by our automatic code generator. + Example: the directive REG_PARAMS('collect_param_descrs') + "tells" the automatic code generator how to register the additional global parameters. + */ + static void register_global(param_descrs & d); + + /** + \brief Register parameter descriptions for a Z3 module. + The parameters of a given Z3 module can only be set using #set_global_param if + they are registered in this module using this function. + + This is an auxiliary function used by our automatic code generator. + Each module will contain directives (in comments) such as + Example: the directive REG_MODULE_PARAMS('nlsat', 'nlsat::solver::collect_param_descrs') + "tells" the automatic code generator how to register the parameters for the given + module. + */ + static void register_module(char const * module_name, param_descrs * d); + + /** + \brief Retrieves the parameters associated with the given module. + + Example: + // The following command sets the parameter "decimal" in the module "pp" to true. + set_global_param("pp.decimal", "true"); + ... + // The following command will return the global parameters that were set for the module "pp". + // In this example "p" will contain "decimal" -> true after executing this function. + params_ref const & p = get_module_params("pp") + */ + static params_ref const & get_module(char const * module_name); + static params_ref const & get_module(symbol const & module_name); + + /** + \brief Return the global parameter set (i.e., parameters that are not associated with any particular module). + */ + static params_ref const & get(); + + /** + \brief Dump information about available parameters in the given output stream. + */ + static void display(std::ostream & out, unsigned indent = 0, bool smt2_style=false); + + /** + \brief Initialize the global parameter management module. + + Remark: I set a priority in the initialization, because this module must be initialized + after the core modules such as symbol. + ADD_INITIALIZER('gparams::init();', 1) + */ + static void init(); + + /** + \brief Finalize the global parameter management module. + + ADD_FINALIZER('gparams::finalize();'); + */ + static void finalize(); +}; + + + +#endif diff --git a/src/util/params.cpp b/src/util/params.cpp index ae7f0c830..b143a82dd 100644 --- a/src/util/params.cpp +++ b/src/util/params.cpp @@ -60,7 +60,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) const { + void display(std::ostream & out, unsigned indent, bool smt2_style) const { svector names; dictionary::iterator it = m_info.begin(); dictionary::iterator end = m_info.end(); @@ -72,7 +72,20 @@ struct param_descrs::imp { svector::iterator end2 = names.end(); for (; it2 != end2; ++it2) { for (unsigned i = 0; i < indent; i++) out << " "; - out << *it2; + if (smt2_style) + out << ':'; + char const * s = it2->bare_str(); + unsigned n = strlen(s); + for (unsigned i = 0; i < n; i++) { + if (smt2_style && s[i] == '_') + out << '-'; + else if (!smt2_style && s[i] == '-') + out << '_'; + else if (s[i] >= 'A' && s[i] <= 'Z') + out << (s[i] - 'A' + 'a'); + else + out << s[i]; + } info d; d.second = 0; m_info.find(*it2, d); @@ -80,6 +93,15 @@ struct param_descrs::imp { out << " (" << d.first << ") " << d.second << "\n"; } } + + void copy(param_descrs & other) { + dictionary::iterator it = other.m_imp->m_info.begin(); + dictionary::iterator end = other.m_imp->m_info.end(); + for (; it != end; ++it) { + insert(it->m_key, it->m_value.first, it->m_value.second); + } + } + }; param_descrs::param_descrs() { @@ -90,6 +112,10 @@ param_descrs::~param_descrs() { dealloc(m_imp); } +void param_descrs::copy(param_descrs & other) { + m_imp->copy(other); +} + void param_descrs::insert(symbol const & name, param_kind k, char const * descr) { m_imp->insert(name, k, descr); } @@ -122,28 +148,28 @@ 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) const { - return m_imp->display(out, indent); +void param_descrs::display(std::ostream & out, unsigned indent, bool smt2_style) const { + return m_imp->display(out, indent, smt2_style); } void insert_max_memory(param_descrs & r) { - r.insert(":max-memory", CPK_UINT, "(default: infty) maximum amount of memory in megabytes."); + r.insert("max_memory", CPK_UINT, "(default: infty) maximum amount of memory in megabytes."); } void insert_max_steps(param_descrs & r) { - r.insert(":max-steps", CPK_UINT, "(default: infty) maximum number of steps."); + r.insert("max_steps", CPK_UINT, "(default: infty) maximum number of steps."); } void insert_produce_models(param_descrs & r) { - r.insert(":produce-models", CPK_BOOL, "(default: false) model generation."); + r.insert("produce_models", CPK_BOOL, "(default: false) model generation."); } void insert_produce_proofs(param_descrs & r) { - r.insert(":produce-proofs", CPK_BOOL, "(default: false) proof generation."); + r.insert("produce_proofs", CPK_BOOL, "(default: false) proof generation."); } void insert_timeout(param_descrs & r) { - r.insert(":timeout", CPK_UINT, "(default: infty) timeout in milliseconds."); + r.insert("timeout", CPK_UINT, "(default: infty) timeout in milliseconds."); } class params { @@ -255,6 +281,39 @@ public: } out << ")"; } + + void display(std::ostream & out, symbol const & k) const { + svector::const_iterator it = m_entries.begin(); + svector::const_iterator end = m_entries.end(); + for (; it != end; ++it) { + if (it->first != k) + continue; + switch (it->second.m_kind) { + case CPK_BOOL: + out << it->second.m_bool_value; + return; + case CPK_UINT: + out << it->second.m_uint_value; + return; + case CPK_DOUBLE: + out << it->second.m_double_value; + return; + case CPK_NUMERAL: + out << *(it->second.m_rat_value); + return; + case CPK_SYMBOL: + out << symbol::mk_symbol_from_c_ptr(it->second.m_sym_value); + return; + case CPK_STRING: + out << it->second.m_str_value; + return; + default: + out << "internal"; + return; + } + } + out << "default"; + } }; params_ref::~params_ref() { @@ -274,6 +333,17 @@ void params_ref::display(std::ostream & out) const { out << "(params)"; } +void params_ref::display(std::ostream & out, char const * k) const { + display(out, symbol(k)); +} + +void params_ref::display(std::ostream & out, symbol const & k) const { + if (m_params) + m_params->display(out, k); + else + out << "default"; +} + void params_ref::validate(param_descrs const & p) const { if (m_params) m_params->validate(p); diff --git a/src/util/params.h b/src/util/params.h index 66c4e7c7a..f587ed862 100644 --- a/src/util/params.h +++ b/src/util/params.h @@ -79,6 +79,14 @@ public: void display(std::ostream & out) const; void validate(param_descrs const & p) const; + + /* + \brief Display the value of the given parameter. + + It displays 'default' if k is not in the parameter set. + */ + void display(std::ostream & out, char const * k); + void display(std::ostream & out, symbol const & k); }; inline std::ostream & operator<<(std::ostream & out, params_ref const & ref) { @@ -92,13 +100,14 @@ class param_descrs { public: param_descrs(); ~param_descrs(); + void copy(param_descrs & other); void insert(char const * name, param_kind k, char const * descr); void insert(symbol const & name, param_kind k, char const * descr); void erase(char const * name); void erase(symbol const & name); param_kind get_kind(char const * name) const; param_kind get_kind(symbol const & name) const; - void display(std::ostream & out, unsigned indent = 0) const; + void display(std::ostream & out, unsigned indent = 0, bool smt2_style=false) const; unsigned size() const; symbol get_param_name(unsigned idx) const; };