From 6d7d205e13f0ee1562f4ea2c458cef002ba7e6ca Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 3 Dec 2012 15:02:34 -0800 Subject: [PATCH] fixed more problems in the new param framework Signed-off-by: Leonardo de Moura --- src/api/api_params.cpp | 8 ++-- src/api/python/z3.py | 7 ++- src/cmd_context/cmd_context.cpp | 16 ------- src/cmd_context/cmd_context.h | 5 --- src/cmd_context/parametric_cmd.cpp | 2 +- src/cmd_context/tactic_cmds.cpp | 2 +- src/smt/params/smt_params.cpp | 7 +++ src/smt/params/smt_params_helper.pyg | 2 + src/tactic/arith/degree_shift_tactic.cpp | 2 +- src/tactic/arith/purify_arith_tactic.cpp | 2 +- src/tactic/sls/sls_tactic.cpp | 2 +- src/tactic/smtlogics/nra_tactic.cpp | 8 ++-- src/tactic/smtlogics/qfaufbv_tactic.cpp | 20 ++++----- src/tactic/smtlogics/qfauflia_tactic.cpp | 12 ++--- src/tactic/smtlogics/qfbv_tactic.cpp | 36 +++++++-------- src/tactic/smtlogics/qfidl_tactic.cpp | 26 +++++------ src/tactic/smtlogics/qflia_tactic.cpp | 56 ++++++++++++------------ src/tactic/smtlogics/qflra_tactic.cpp | 18 ++++---- src/tactic/smtlogics/qfnia_tactic.cpp | 28 ++++++------ src/tactic/smtlogics/qfnra_tactic.cpp | 10 ++--- src/tactic/smtlogics/qfuf_tactic.cpp | 6 +-- src/tactic/smtlogics/qfufbv_tactic.cpp | 4 +- src/tactic/smtlogics/quant_tactics.cpp | 14 +++--- src/tactic/ufbv/ufbv_tactic.cpp | 10 ++--- src/test/dl_context.cpp | 4 +- src/test/dl_product_relation.cpp | 2 +- src/test/dl_query.cpp | 12 ++--- src/util/debug.cpp | 6 ++- src/util/params.cpp | 23 ++++++++++ src/util/params.h | 3 ++ 30 files changed, 185 insertions(+), 168 deletions(-) diff --git a/src/api/api_params.cpp b/src/api/api_params.cpp index 74899bc44..19634af32 100644 --- a/src/api/api_params.cpp +++ b/src/api/api_params.cpp @@ -66,7 +66,7 @@ extern "C" { Z3_TRY; LOG_Z3_params_set_bool(c, p, k, v); RESET_ERROR_CODE(); - to_params(p)->m_params.set_bool(to_symbol(k), v != 0); + to_params(p)->m_params.set_bool(norm_param_name(to_symbol(k)).c_str(), v != 0); Z3_CATCH; } @@ -77,7 +77,7 @@ extern "C" { Z3_TRY; LOG_Z3_params_set_uint(c, p, k, v); RESET_ERROR_CODE(); - to_params(p)->m_params.set_uint(to_symbol(k), v); + to_params(p)->m_params.set_uint(norm_param_name(to_symbol(k)).c_str(), v); Z3_CATCH; } @@ -88,7 +88,7 @@ extern "C" { Z3_TRY; LOG_Z3_params_set_double(c, p, k, v); RESET_ERROR_CODE(); - to_params(p)->m_params.set_double(to_symbol(k), v); + to_params(p)->m_params.set_double(norm_param_name(to_symbol(k)).c_str(), v); Z3_CATCH; } @@ -99,7 +99,7 @@ extern "C" { Z3_TRY; LOG_Z3_params_set_symbol(c, p, k, v); RESET_ERROR_CODE(); - to_params(p)->m_params.set_sym(to_symbol(k), to_symbol(v)); + to_params(p)->m_params.set_sym(norm_param_name(to_symbol(k)).c_str(), to_symbol(v)); Z3_CATCH; } diff --git a/src/api/python/z3.py b/src/api/python/z3.py index b03cf1fd8..71fd9a732 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -223,7 +223,7 @@ def get_option(name): """Return the value of a Z3 global (or module) parameter >>> get_option('nlsat.reorder') - true + 'true' """ ptr = (ctypes.c_char_p * 1)() if Z3_global_param_get(str(name), ptr): @@ -4384,8 +4384,8 @@ def args2params(arguments, keywords, ctx=None): """Convert python arguments into a Z3_params object. A ':' is added to the keywords, and '_' is replaced with '-' - >>> args2params([':model', True, ':relevancy', 2], {'elim_and' : True}) - (params :model 1 :relevancy 2 :elim-and 1) + >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True}) + (params model 1 relevancy 2 elim_and 1) """ if __debug__: _z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.") @@ -4398,7 +4398,6 @@ def args2params(arguments, keywords, ctx=None): r.set(prev, a) prev = None for k, v in keywords.iteritems(): - k = ':' + k.replace('_', '-') r.set(k, v) return r diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index c6bfeb663..b27e1e177 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -38,22 +38,6 @@ 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); diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index ae517b0c2..ca3ada7cf 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -38,11 +38,6 @@ Notes: #include"scoped_ptr_vector.h" #include"context_params.h" -/** - \brief Auxiliary function for converting SMT2 keywords into Z3 internal parameter names. -*/ -std::string smt2_keyword_to_param(symbol const & k); - class func_decls { func_decl * m_decls; public: diff --git a/src/cmd_context/parametric_cmd.cpp b/src/cmd_context/parametric_cmd.cpp index f028c3b9d..c229bc29c 100644 --- a/src/cmd_context/parametric_cmd.cpp +++ b/src/cmd_context/parametric_cmd.cpp @@ -38,7 +38,7 @@ 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 = symbol(smt2_keyword_to_param(s).c_str()); + m_last = symbol(norm_param_name(s).c_str()); if (pdescrs(ctx).get_kind(m_last.bare_str()) == CPK_INVALID) throw cmd_exception("invalid keyword argument"); return; diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index 8a7449a88..ca87406c7 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -497,7 +497,7 @@ static tactic * mk_using_params(cmd_context & ctx, sexpr * n) { throw cmd_exception("invalid using-params combinator, keyword expected", c->get_line(), c->get_pos()); if (i == num_children) throw cmd_exception("invalid using-params combinator, parameter value expected", c->get_line(), c->get_pos()); - symbol param_name = symbol(smt2_keyword_to_param(c->get_symbol()).c_str()); + symbol param_name = symbol(norm_param_name(c->get_symbol()).c_str()); c = n->get_child(i); i++; switch (descrs.get_kind(param_name)) { diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index fb5ada715..113a2bead 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -22,6 +22,8 @@ Revision History: void smt_params::updt_local_params(params_ref const & _p) { smt_params_helper p(_p); m_auto_config = p.auto_config(); + m_random_seed = p.random_seed(); + m_relevancy_lvl = p.relevancy(); m_ematching = p.ematching(); m_phase_selection = static_cast(p.phase_selection()); m_restart_strategy = static_cast(p.restart_strategy()); @@ -29,6 +31,11 @@ void smt_params::updt_local_params(params_ref const & _p) { m_case_split_strategy = static_cast(p.case_split()); m_delay_units = p.delay_units(); m_delay_units_threshold = p.delay_units_threshold(); + m_preprocess = _p.get_bool("preprocess", true); // hidden parameter + if (_p.get_bool("arith.greatest_error_pivot", false)) + m_arith_pivot_strategy = ARITH_PIVOT_GREATEST_ERROR; + else if (_p.get_bool("arith.least_error_pivot", false)) + m_arith_pivot_strategy = ARITH_PIVOT_LEAST_ERROR; } void smt_params::updt_params(params_ref const & p) { diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 8db95a581..bcdf78b73 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -3,6 +3,8 @@ def_module_params(module_name='smt', description='smt solver based on lazy smt', export=True, params=(('auto_config', BOOL, True, 'automatically configure solver'), + ('random_seed', UINT, 0, 'random seed for the smt solver'), + ('relevancy', UINT, 2, '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'), ('macro_finder', BOOL, False, 'try to find universally quantified formulas that can be viewed as macros'), ('ematching', BOOL, True, 'E-Matching based quantifier instantiation'), ('phase_selection', UINT, 4, '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'), diff --git a/src/tactic/arith/degree_shift_tactic.cpp b/src/tactic/arith/degree_shift_tactic.cpp index 8e2c6d7cb..a1aa0bdc8 100644 --- a/src/tactic/arith/degree_shift_tactic.cpp +++ b/src/tactic/arith/degree_shift_tactic.cpp @@ -342,7 +342,7 @@ protected: tactic * mk_degree_shift_tactic(ast_manager & m, params_ref const & p) { params_ref mul2power_p; - mul2power_p.set_bool(":mul-to-power", true); + mul2power_p.set_bool("mul_to_power", true); return and_then(using_params(mk_simplify_tactic(m), mul2power_p), clean(alloc(degree_shift_tactic, m))); } diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index d6ed86c08..d2292ede9 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -902,7 +902,7 @@ 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); diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index 290a0ad35..f49ce8422 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -1855,7 +1855,7 @@ 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("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); diff --git a/src/tactic/smtlogics/nra_tactic.cpp b/src/tactic/smtlogics/nra_tactic.cpp index 623b7e55e..845b6bfec 100644 --- a/src/tactic/smtlogics/nra_tactic.cpp +++ b/src/tactic/smtlogics/nra_tactic.cpp @@ -27,11 +27,11 @@ Notes: tactic * mk_nra_tactic(ast_manager & m, params_ref const& p) { params_ref p1 = p; - p1.set_uint(":seed", 11); - p1.set_bool(":factor", false); + p1.set_uint("seed", 11); + p1.set_bool("factor", false); params_ref p2 = p; - p2.set_uint(":seed", 13); - p2.set_bool(":factor", false); + p2.set_uint("seed", 13); + p2.set_bool("factor", false); return and_then(mk_simplify_tactic(m, p), mk_nnf_tactic(m, p), diff --git a/src/tactic/smtlogics/qfaufbv_tactic.cpp b/src/tactic/smtlogics/qfaufbv_tactic.cpp index 5f371da0c..cb14fa778 100644 --- a/src/tactic/smtlogics/qfaufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfaufbv_tactic.cpp @@ -29,22 +29,22 @@ Notes: tactic * mk_qfaufbv_tactic(ast_manager & m, params_ref const & p) { params_ref main_p; - main_p.set_bool(":elim-and", true); - main_p.set_bool(":sort-store", true); + main_p.set_bool("elim_and", true); + main_p.set_bool("sort_store", 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 ctx_simp_p; - ctx_simp_p.set_uint(":max-depth", 32); - ctx_simp_p.set_uint(":max-steps", 5000000); + ctx_simp_p.set_uint("max_depth", 32); + ctx_simp_p.set_uint("max_steps", 5000000); params_ref solver_p; - solver_p.set_bool(":array-old-simplifier", false); + solver_p.set_bool("array.simplify", false); // disable array simplifications at old_simplify module tactic * preamble_st = and_then(mk_simplify_tactic(m), mk_propagate_values_tactic(m), diff --git a/src/tactic/smtlogics/qfauflia_tactic.cpp b/src/tactic/smtlogics/qfauflia_tactic.cpp index 422be13d5..89f96d354 100644 --- a/src/tactic/smtlogics/qfauflia_tactic.cpp +++ b/src/tactic/smtlogics/qfauflia_tactic.cpp @@ -26,16 +26,16 @@ Notes: tactic * mk_qfauflia_tactic(ast_manager & m, params_ref const & p) { params_ref main_p; - main_p.set_bool(":elim-and", true); - main_p.set_bool(":som", true); - main_p.set_bool(":sort-store", true); + main_p.set_bool("elim_and", true); + main_p.set_bool("som", true); + main_p.set_bool("sort_store", true); params_ref ctx_simp_p; - ctx_simp_p.set_uint(":max-depth", 30); - ctx_simp_p.set_uint(":max-steps", 5000000); + ctx_simp_p.set_uint("max_depth", 30); + ctx_simp_p.set_uint("max_steps", 5000000); params_ref solver_p; - solver_p.set_bool(":array-old-simplifier", false); + solver_p.set_bool("array.simplify", false); // disable array simplifications at old_simplify module tactic * preamble_st = and_then(mk_simplify_tactic(m), mk_propagate_values_tactic(m), diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index 5924c5bdf..51b040332 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -33,40 +33,40 @@ Notes: tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) { params_ref main_p; - main_p.set_bool(":elim-and", true); - main_p.set_bool(":push-ite-bv", true); - main_p.set_bool(":blast-distinct", true); + main_p.set_bool("elim_and", true); + main_p.set_bool("push_ite_bv", true); + main_p.set_bool("blast_distinct", 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 local_ctx_p = p; - local_ctx_p.set_bool(":local-ctx", true); + local_ctx_p.set_bool("local_ctx", true); params_ref solver_p; - solver_p.set_bool(":preprocess", false); // preprocessor of smt::context is not needed. + solver_p.set_bool("preprocess", false); // preprocessor of smt::context is not needed. params_ref no_flat_p; - no_flat_p.set_bool(":flat", false); + no_flat_p.set_bool("flat", false); params_ref ctx_simp_p; - ctx_simp_p.set_uint(":max-depth", 32); - ctx_simp_p.set_uint(":max-steps", 50000000); + ctx_simp_p.set_uint("max_depth", 32); + ctx_simp_p.set_uint("max_steps", 50000000); params_ref hoist_p; - hoist_p.set_bool(":hoist-mul", true); - hoist_p.set_bool(":som", false); + hoist_p.set_bool("hoist_mul", true); + hoist_p.set_bool("som", false); params_ref solve_eq_p; // conservative guassian elimination. - solve_eq_p.set_uint(":solve-eqs-max-occs", 2); + solve_eq_p.set_uint("solve_eqs_max_occs", 2); params_ref big_aig_p; - big_aig_p.set_bool(":aig-per-assertion", false); + big_aig_p.set_bool("aig_per_assertion", false); tactic * preamble_st = and_then(and_then(mk_simplify_tactic(m), mk_propagate_values_tactic(m), @@ -74,7 +74,7 @@ tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) { mk_elim_uncnstr_tactic(m), if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))), using_params(mk_simplify_tactic(m), simp2_p)), - // Z3 can solve a couple of extra benchmarks by using :hoist-mul + // Z3 can solve a couple of extra benchmarks by using hoist_mul // but the timeout in SMT-COMP is too small. // Moreover, it impacted negatively some easy benchmarks. // We should decide later, if we keep it or not. diff --git a/src/tactic/smtlogics/qfidl_tactic.cpp b/src/tactic/smtlogics/qfidl_tactic.cpp index 57aef4991..de05797e8 100644 --- a/src/tactic/smtlogics/qfidl_tactic.cpp +++ b/src/tactic/smtlogics/qfidl_tactic.cpp @@ -37,23 +37,23 @@ Notes: tactic * mk_qfidl_tactic(ast_manager & m, params_ref const & p) { params_ref main_p; - main_p.set_bool(":elim-and", true); - main_p.set_bool(":blast-distinct", true); - main_p.set_bool(":som", true); + main_p.set_bool("elim_and", true); + main_p.set_bool("blast_distinct", true); + main_p.set_bool("som", true); params_ref lhs_p; - lhs_p.set_bool(":arith-lhs", true); + lhs_p.set_bool("arith_lhs", true); params_ref lia2pb_p; - lia2pb_p.set_uint(":lia2pb-max-bits", 4); + lia2pb_p.set_uint("lia2pb_max_bits", 4); params_ref pb2bv_p; - pb2bv_p.set_uint(":pb2bv-all-clauses-limit", 8); + pb2bv_p.set_uint("pb2bv_all_clauses_limit", 8); params_ref pull_ite_p; - pull_ite_p.set_bool(":pull-cheap-ite", true); - pull_ite_p.set_bool(":local-ctx", true); - pull_ite_p.set_uint(":local-ctx-limit", 10000000); + pull_ite_p.set_bool("pull_cheap_ite", true); + pull_ite_p.set_bool("local_ctx", true); + pull_ite_p.set_uint("local_ctx_limit", 10000000); tactic * preamble_st = and_then(and_then(mk_simplify_tactic(m), mk_fix_dl_var_tactic(m), @@ -71,10 +71,10 @@ tactic * mk_qfidl_tactic(ast_manager & m, params_ref const & p) { params_ref bv_solver_p; // The cardinality constraint encoding generates a lot of shared if-then-else's that can be flattened. // Several of them are simplified to and/or. If we flat them, we increase a lot the memory consumption. - bv_solver_p.set_bool(":flat", false); - bv_solver_p.set_bool(":som", false); + bv_solver_p.set_bool("flat", false); + bv_solver_p.set_bool("som", false); // dynamic psm seems to work well. - bv_solver_p.set_sym(":gc-strategy", symbol("dyn-psm")); + bv_solver_p.set_sym("gc", symbol("dyn_psm")); tactic * bv_solver = using_params(and_then(mk_simplify_tactic(m), mk_propagate_values_tactic(m), @@ -93,7 +93,7 @@ tactic * mk_qfidl_tactic(ast_manager & m, params_ref const & p) { bv_solver); params_ref diff_neq_p; - diff_neq_p.set_uint(":diff-neq-max-k", 25); + diff_neq_p.set_uint("diff_neq_max_k", 25); tactic * st = cond(mk_and(mk_lt(mk_num_consts_probe(), mk_const_probe(static_cast(BIG_PROBLEM))), mk_and(mk_not(mk_produce_proofs_probe()), diff --git a/src/tactic/smtlogics/qflia_tactic.cpp b/src/tactic/smtlogics/qflia_tactic.cpp index 1fb30faae..6b05cff96 100644 --- a/src/tactic/smtlogics/qflia_tactic.cpp +++ b/src/tactic/smtlogics/qflia_tactic.cpp @@ -64,17 +64,17 @@ probe * mk_quasi_pb_probe() { // Create SMT solver that does not use cuts static tactic * mk_no_cut_smt_tactic(unsigned rs) { params_ref solver_p; - solver_p.set_uint(":arith-branch-cut-ratio", 10000000); - solver_p.set_uint(":random-seed", rs); + solver_p.set_uint("arith.branch_cut_ratio", 10000000); + solver_p.set_uint("random_seed", rs); return using_params(mk_smt_tactic_using(false), solver_p); } // Create SMT solver that does not use cuts static tactic * mk_no_cut_no_relevancy_smt_tactic(unsigned rs) { params_ref solver_p; - solver_p.set_uint(":arith-branch-cut-ratio", 10000000); - solver_p.set_uint(":random-seed", rs); - solver_p.set_uint(":relevancy", 0); + solver_p.set_uint("arith.branch_cut_ratio", 10000000); + solver_p.set_uint("random_seed", rs); + solver_p.set_uint("relevancy", 0); return using_params(mk_smt_tactic_using(false), solver_p); } @@ -82,10 +82,10 @@ static tactic * mk_bv2sat_tactic(ast_manager & m) { params_ref solver_p; // The cardinality constraint encoding generates a lot of shared if-then-else's that can be flattened. // Several of them are simplified to and/or. If we flat them, we increase a lot the memory consumption. - solver_p.set_bool(":flat", false); - solver_p.set_bool(":som", false); + solver_p.set_bool("flat", false); + solver_p.set_bool("som", false); // dynamic psm seems to work well. - solver_p.set_sym(":gc-strategy", symbol("dyn-psm")); + solver_p.set_sym("gc", symbol("dyn_psm")); return using_params(and_then(mk_simplify_tactic(m), mk_propagate_values_tactic(m), @@ -101,8 +101,8 @@ static tactic * mk_bv2sat_tactic(ast_manager & m) { static tactic * mk_pb_tactic(ast_manager & m) { params_ref pb2bv_p; - pb2bv_p.set_bool(":ite-extra", true); - pb2bv_p.set_uint(":pb2bv-all-clauses-limit", 8); + pb2bv_p.set_bool("ite_extra", true); + pb2bv_p.set_uint("pb2bv_all_clauses_limit", 8); return and_then(fail_if_not(mk_is_pb_probe()), fail_if(mk_produce_proofs_probe()), @@ -119,8 +119,8 @@ static tactic * mk_pb_tactic(ast_manager & m) { static tactic * mk_lia2sat_tactic(ast_manager & m) { params_ref pb2bv_p; - pb2bv_p.set_bool(":ite-extra", true); - pb2bv_p.set_uint(":pb2bv-all-clauses-limit", 8); + pb2bv_p.set_bool("ite_extra", true); + pb2bv_p.set_uint("pb2bv_all_clauses_limit", 8); return and_then(fail_if(mk_is_unbounded_probe()), fail_if(mk_produce_proofs_probe()), @@ -137,11 +137,11 @@ static tactic * mk_lia2sat_tactic(ast_manager & m) { // Fails if the problem is no ILP. static tactic * mk_ilp_model_finder_tactic(ast_manager & m) { params_ref add_bounds_p1; - add_bounds_p1.set_rat(":add-bound-lower", rational(-16)); - add_bounds_p1.set_rat(":add-bound-upper", rational(15)); + add_bounds_p1.set_rat("add_bound_lower", rational(-16)); + add_bounds_p1.set_rat("add_bound_upper", rational(15)); params_ref add_bounds_p2; - add_bounds_p2.set_rat(":add-bound-lower", rational(-32)); - add_bounds_p2.set_rat(":add-bound-upper", rational(31)); + add_bounds_p2.set_rat("add_bound_lower", rational(-32)); + add_bounds_p2.set_rat("add_bound_upper", rational(31)); return and_then(fail_if_not(mk_and(mk_is_ilp_probe(), mk_is_unbounded_probe())), fail_if(mk_produce_proofs_probe()), @@ -170,22 +170,22 @@ static tactic * mk_bounded_tactic(ast_manager & m) { tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) { params_ref main_p; - main_p.set_bool(":elim-and", true); - main_p.set_bool(":som", true); - // main_p.set_bool(":push-ite-arith", true); + main_p.set_bool("elim_and", true); + main_p.set_bool("som", true); + // main_p.set_bool("push_ite_arith", true); params_ref pull_ite_p; - pull_ite_p.set_bool(":pull-cheap-ite", true); - pull_ite_p.set_bool(":push-ite-arith", false); - pull_ite_p.set_bool(":local-ctx", true); - pull_ite_p.set_uint(":local-ctx-limit", 10000000); + pull_ite_p.set_bool("pull_cheap_ite", true); + pull_ite_p.set_bool("push_ite_arith", false); + pull_ite_p.set_bool("local_ctx", true); + pull_ite_p.set_uint("local_ctx_limit", 10000000); params_ref ctx_simp_p; - ctx_simp_p.set_uint(":max-depth", 30); - ctx_simp_p.set_uint(":max-steps", 5000000); + ctx_simp_p.set_uint("max_depth", 30); + ctx_simp_p.set_uint("max_steps", 5000000); params_ref lhs_p; - lhs_p.set_bool(":arith-lhs", true); + lhs_p.set_bool("arith_lhs", true); tactic * preamble_st = and_then(and_then(mk_simplify_tactic(m), mk_propagate_values_tactic(m), @@ -197,10 +197,10 @@ tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) { ); params_ref quasi_pb_p; - quasi_pb_p.set_uint(":lia2pb-max-bits", 64); + quasi_pb_p.set_uint("lia2pb_max_bits", 64); params_ref no_cut_p; - no_cut_p.set_uint(":arith-branch-cut-ratio", 10000000); + no_cut_p.set_uint("arith.branch_cut_ratio", 10000000); tactic * st = using_params(and_then(preamble_st, diff --git a/src/tactic/smtlogics/qflra_tactic.cpp b/src/tactic/smtlogics/qflra_tactic.cpp index 42aaa96b7..41f0e16f3 100644 --- a/src/tactic/smtlogics/qflra_tactic.cpp +++ b/src/tactic/smtlogics/qflra_tactic.cpp @@ -29,23 +29,23 @@ Notes: tactic * mk_qflra_tactic(ast_manager & m, params_ref const & p) { params_ref pivot_p; - pivot_p.set_bool(":arith-greatest-error-pivot", true); + pivot_p.set_bool("arith.greatest_error_pivot", true); params_ref main_p = p; - main_p.set_bool(":elim-and", true); - main_p.set_bool(":som", true); - main_p.set_bool(":blast-distinct", true); + main_p.set_bool("elim_and", true); + main_p.set_bool("som", true); + main_p.set_bool("blast_distinct", true); params_ref ctx_simp_p; - ctx_simp_p.set_uint(":max-depth", 30); - ctx_simp_p.set_uint(":max-steps", 5000000); + ctx_simp_p.set_uint("max_depth", 30); + ctx_simp_p.set_uint("max_steps", 5000000); params_ref lhs_p; - lhs_p.set_bool(":arith-lhs", true); - lhs_p.set_bool(":eq2ineq", true); + lhs_p.set_bool("arith_lhs", true); + lhs_p.set_bool("eq2ineq", true); params_ref elim_to_real_p; - elim_to_real_p.set_bool(":elim-to-real", true); + elim_to_real_p.set_bool("elim_to_real", true); #if 0 diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp index e87d36503..950291221 100644 --- a/src/tactic/smtlogics/qfnia_tactic.cpp +++ b/src/tactic/smtlogics/qfnia_tactic.cpp @@ -31,14 +31,14 @@ Notes: tactic * mk_qfnia_bv_solver(ast_manager & m, params_ref const & p_ref) { params_ref p = p_ref; - p.set_bool(":flat", false); - p.set_bool(":hi-div0", true); - p.set_bool(":elim-and", true); - p.set_bool(":blast-distinct", true); + p.set_bool("flat", false); + p.set_bool("hi_div0", true); + p.set_bool("elim_and", true); + p.set_bool("blast_distinct", true); params_ref simp2_p = p; - simp2_p.set_bool(":local-ctx", true); - simp2_p.set_uint(":local-ctx-limit", 10000000); + simp2_p.set_bool("local_ctx", true); + simp2_p.set_uint("local_ctx_limit", 10000000); tactic * r = using_params(and_then(mk_simplify_tactic(m), @@ -53,19 +53,19 @@ tactic * mk_qfnia_bv_solver(ast_manager & m, params_ref const & p_ref) { tactic * mk_qfnia_premable(ast_manager & m, params_ref const & p_ref) { params_ref pull_ite_p = p_ref; - pull_ite_p.set_bool(":pull-cheap-ite", true); - pull_ite_p.set_bool(":local-ctx", true); - pull_ite_p.set_uint(":local-ctx-limit", 10000000); + pull_ite_p.set_bool("pull_cheap_ite", true); + pull_ite_p.set_bool("local_ctx", true); + pull_ite_p.set_uint("local_ctx_limit", 10000000); params_ref ctx_simp_p = p_ref; - ctx_simp_p.set_uint(":max-depth", 30); - ctx_simp_p.set_uint(":max-steps", 5000000); + ctx_simp_p.set_uint("max_depth", 30); + ctx_simp_p.set_uint("max_steps", 5000000); params_ref simp_p = p_ref; - simp_p.set_bool(":hoist-mul", true); + simp_p.set_bool("hoist_mul", true); params_ref elim_p = p_ref; - elim_p.set_uint(":max-memory",20); + elim_p.set_uint("max_memory",20); return and_then(mk_simplify_tactic(m), @@ -79,7 +79,7 @@ tactic * mk_qfnia_premable(ast_manager & m, params_ref const & p_ref) { tactic * mk_qfnia_sat_solver(ast_manager & m, params_ref const & p) { params_ref nia2sat_p = p; - nia2sat_p.set_uint(":nla2bv-max-bv-size", 64); + nia2sat_p.set_uint("nla2bv_max_bv_size", 64); return and_then(mk_nla2bv_tactic(m, nia2sat_p), mk_qfnia_bv_solver(m, p), diff --git a/src/tactic/smtlogics/qfnra_tactic.cpp b/src/tactic/smtlogics/qfnra_tactic.cpp index a2877eefa..716b4868b 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(), @@ -34,11 +34,11 @@ static tactic * mk_qfnra_sat_solver(ast_manager& m, params_ref const& p, unsigne tactic * mk_qfnra_tactic(ast_manager & m, params_ref const& p) { params_ref p1 = p; - p1.set_uint(":seed", 11); - p1.set_bool(":factor", false); + p1.set_uint("seed", 11); + p1.set_bool("factor", false); params_ref p2 = p; - p2.set_uint(":seed", 13); - p2.set_bool(":factor", false); + p2.set_uint("seed", 13); + p2.set_bool("factor", false); return and_then(mk_simplify_tactic(m, p), mk_propagate_values_tactic(m, p), diff --git a/src/tactic/smtlogics/qfuf_tactic.cpp b/src/tactic/smtlogics/qfuf_tactic.cpp index 3acfb8d98..567325f6a 100644 --- a/src/tactic/smtlogics/qfuf_tactic.cpp +++ b/src/tactic/smtlogics/qfuf_tactic.cpp @@ -26,9 +26,9 @@ Notes: tactic * mk_qfuf_tactic(ast_manager & m, params_ref const & p) { params_ref s2_p; - s2_p.set_bool(":pull-cheap-ite", true); - s2_p.set_bool(":local-ctx", true); - s2_p.set_uint(":local-ctx-limit", 10000000); + s2_p.set_bool("pull_cheap_ite", true); + s2_p.set_bool("local_ctx", true); + s2_p.set_uint("local_ctx_limit", 10000000); return and_then(mk_simplify_tactic(m, p), mk_propagate_values_tactic(m, p), mk_solve_eqs_tactic(m, p), diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp index 400ff9891..d10b7c1b4 100644 --- a/src/tactic/smtlogics/qfufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfufbv_tactic.cpp @@ -28,8 +28,8 @@ Notes: tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p) { params_ref main_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); tactic * preamble_st = and_then(mk_simplify_tactic(m), mk_propagate_values_tactic(m), diff --git a/src/tactic/smtlogics/quant_tactics.cpp b/src/tactic/smtlogics/quant_tactics.cpp index 4bb896c74..6b5ede813 100644 --- a/src/tactic/smtlogics/quant_tactics.cpp +++ b/src/tactic/smtlogics/quant_tactics.cpp @@ -27,13 +27,13 @@ Revision History: static tactic * mk_quant_preprocessor(ast_manager & m, bool disable_gaussian = false) { params_ref pull_ite_p; - pull_ite_p.set_bool(":pull-cheap-ite", true); - pull_ite_p.set_bool(":local-ctx", true); - pull_ite_p.set_uint(":local-ctx-limit", 10000000); + pull_ite_p.set_bool("pull_cheap_ite", true); + pull_ite_p.set_bool("local_ctx", true); + pull_ite_p.set_uint("local_ctx_limit", 10000000); params_ref ctx_simp_p; - ctx_simp_p.set_uint(":max-depth", 30); - ctx_simp_p.set_uint(":max-steps", 5000000); + ctx_simp_p.set_uint("max_depth", 30); + ctx_simp_p.set_uint("max_steps", 5000000); tactic * solve_eqs; if (disable_gaussian) @@ -71,8 +71,8 @@ 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";); + qi_p.set_str("qi.cost", "0"); + 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/ufbv_tactic.cpp b/src/tactic/ufbv/ufbv_tactic.cpp index 85ec506aa..80d403b67 100644 --- a/src/tactic/ufbv/ufbv_tactic.cpp +++ b/src/tactic/ufbv/ufbv_tactic.cpp @@ -37,7 +37,7 @@ tactic * mk_der_fp_tactic(ast_manager & m, params_ref const & p) { tactic * mk_ufbv_preprocessor_tactic(ast_manager & m, params_ref const & p) { params_ref no_elim_and(p); - no_elim_and.set_bool(":elim-and", false); + no_elim_and.set_bool("elim_and", false); return and_then( mk_trace_tactic("ufbv_pre"), @@ -61,10 +61,10 @@ tactic * mk_ufbv_preprocessor_tactic(ast_manager & m, params_ref const & p) { tactic * mk_ufbv_tactic(ast_manager & m, params_ref const & p) { params_ref main_p(p); - main_p.set_bool(":mbqi", true); - main_p.set_uint(":mbqi-max-iterations", -1); - main_p.set_bool(":elim-and", true); - main_p.set_bool(":solver", true); + main_p.set_bool("mbqi", true); + main_p.set_uint("mbqi_max_iterations", -1); + main_p.set_bool("elim_and", true); + main_p.set_bool("solver", true); tactic * t = and_then(repeat(mk_ufbv_preprocessor_tactic(m, main_p), 2), mk_smt_tactic_using(false, main_p)); diff --git a/src/test/dl_context.cpp b/src/test/dl_context.cpp index c004c531f..ff7548abc 100644 --- a/src/test/dl_context.cpp +++ b/src/test/dl_context.cpp @@ -72,9 +72,9 @@ void tst_dl_context() { params_ref params; for(unsigned rel_index=0; rel_index=0; eager_checking--) { - params.set_bool(":eager-emptiness-checking", eager_checking!=0); + params.set_bool("eager_emptiness_checking", eager_checking!=0); std::cerr << "Testing " << relations[rel_index] << "\n"; std::cerr << "Eager emptiness checking " << (eager_checking!=0 ? "on" : "off") << "\n"; diff --git a/src/test/dl_product_relation.cpp b/src/test/dl_product_relation.cpp index 4b67b32af..e58634ec8 100644 --- a/src/test/dl_product_relation.cpp +++ b/src/test/dl_product_relation.cpp @@ -343,7 +343,7 @@ void tst_dl_product_relation() { test_functional_columns(fparams, params); - params.set_sym(":default-relation", symbol("tr_sparse")); + params.set_sym("default_relation", symbol("tr_sparse")); test_finite_product_relation(fparams, params); } diff --git a/src/test/dl_query.cpp b/src/test/dl_query.cpp index 712ae386a..ad21247af 100644 --- a/src/test/dl_query.cpp +++ b/src/test/dl_query.cpp @@ -50,7 +50,7 @@ void dl_query_test(ast_manager & m, smt_params & fparams, params_ref& params, dl_decl_util decl_util(m); context ctx_q(m, fparams); - params.set_bool(":magic-sets-for-queries", use_magic_sets); + params.set_bool("magic_sets_for_queries", use_magic_sets); ctx_q.updt_params(params); { parser* p = parser::create(ctx_q,m); @@ -125,7 +125,7 @@ void dl_query_test(ast_manager & m, smt_params & fparams, params_ref& params, } void dl_query_test_wpa(smt_params & fparams, params_ref& params) { - params.set_bool(":magic-sets-for-queries", true); + params.set_bool("magic_sets_for_queries", true); ast_manager m; reg_decl_plugins(m); arith_util arith(m); @@ -185,8 +185,8 @@ void dl_query_test_wpa(smt_params & fparams, params_ref& params) { void tst_dl_query() { smt_params fparams; params_ref params; - params.set_sym(":default-table", symbol("sparse")); - params.set_sym(":default-relation", symbol("tr_sparse")); + params.set_sym("default_table", symbol("sparse")); + params.set_sym("default_relation", symbol("tr_sparse")); //params.m_dl_default_table = symbol("hashtable"); //params.m_dl_default_relation = symbol("tr_hashtable"); @@ -212,9 +212,9 @@ void tst_dl_query() { ctx_base.dl_saturate(); for(unsigned use_restarts=0; use_restarts<=1; use_restarts++) { - params.set_uint(":initial-restart-timeout", use_restarts ? 100 : 0); + params.set_uint("initial_restart_timeout", use_restarts ? 100 : 0); for(unsigned use_similar=0; use_similar<=1; use_similar++) { - params.set_uint(":similarity-compressor", use_similar != 0); + params.set_uint("similarity_compressor", use_similar != 0); for(unsigned use_magic_sets=0; use_magic_sets<=1; use_magic_sets++) { stopwatch watch; diff --git a/src/util/debug.cpp b/src/util/debug.cpp index 41e0a48fc..75ea8586a 100644 --- a/src/util/debug.cpp +++ b/src/util/debug.cpp @@ -22,6 +22,7 @@ Revision History: #endif #include #include"str_hashtable.h" +#include"z3_exception.h" volatile bool g_enable_assertions = true; @@ -73,7 +74,7 @@ void invoke_gdb() { char buffer[1024]; int * x = 0; for (;;) { - std::cerr << "(C)ontinue, (A)bort, (S)top, Invoke (G)DB\n"; + std::cerr << "(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB\n"; char result; std::cin >> result; switch(result) { @@ -88,6 +89,9 @@ void invoke_gdb() { // force seg fault... *x = 0; return; + case 't': + case 'T': + throw default_exception("assertion violation"); case 'G': case 'g': sprintf(buffer, "gdb -nw /proc/%d/exe %d", getpid(), getpid()); diff --git a/src/util/params.cpp b/src/util/params.cpp index c0b8653ae..f302f7721 100644 --- a/src/util/params.cpp +++ b/src/util/params.cpp @@ -21,6 +21,29 @@ Notes: #include"symbol.h" #include"dictionary.h" +std::string norm_param_name(char const * n) { + if (n == 0) + return "_"; + if (*n == ':') + n++; + std::string r = n; + unsigned sz = r.size(); + if (sz == 0) + return "_"; + for (unsigned i = 0; i < sz; i++) { + char curr = r[i]; + if ('A' <= curr && curr <= 'Z') + r[i] = curr - 'A' + 'a'; + else if (curr == '-' || curr == ':') + r[i] = '_'; + } + return r; +} + +std::string norm_param_name(symbol const & n) { + return norm_param_name(n.bare_str()); +} + struct param_descrs::imp { struct info { param_kind m_kind; diff --git a/src/util/params.h b/src/util/params.h index 164de9ab3..13850758c 100644 --- a/src/util/params.h +++ b/src/util/params.h @@ -22,6 +22,9 @@ Notes: #include"cmd_context_types.h" #include"vector.h" +std::string norm_param_name(char const * n); +std::string norm_param_name(symbol const & n); + typedef cmd_arg_kind param_kind; class params;