fixed more problems in the new param framework

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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

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})
+    >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True})
-    (params :model 1 :relevancy 2 :elim-and 1)
+    (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
 

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<unsigned>(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);

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:

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;

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

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<phase_selection>(p.phase_selection());
     m_restart_strategy = static_cast<restart_strategy>(p.restart_strategy());
@@ -29,6 +31,11 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_case_split_strategy = static_cast<case_split_strategy>(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) {

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'),

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)));
 }

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

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

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_uint("seed", 11);
-    p1.set_bool(":factor", false);
+    p1.set_bool("factor", false);
     params_ref p2 = p;
-    p2.set_uint(":seed", 13);
+    p2.set_uint("seed", 13);
-    p2.set_bool(":factor", false);
+    p2.set_bool("factor", false);
 
     return and_then(mk_simplify_tactic(m, p),
                     mk_nnf_tactic(m, p),

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("elim_and", true);
-    main_p.set_bool(":sort-store", true);
+    main_p.set_bool("sort_store", true);
 
     params_ref simp2_p = p;
-    simp2_p.set_bool(":som", true);
+    simp2_p.set_bool("som", true);
-    simp2_p.set_bool(":pull-cheap-ite", true);
+    simp2_p.set_bool("pull_cheap_ite", true);
-    simp2_p.set_bool(":push-ite-bv", false);
+    simp2_p.set_bool("push_ite_bv", false);
-    simp2_p.set_bool(":local-ctx", true);
+    simp2_p.set_bool("local_ctx", true);
-    simp2_p.set_uint(":local-ctx-limit", 10000000);
+    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_depth", 32);
-    ctx_simp_p.set_uint(":max-steps", 5000000);
+    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),

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("elim_and", true);
-    main_p.set_bool(":som", true);
+    main_p.set_bool("som", true);
-    main_p.set_bool(":sort-store", 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_depth", 30);
-    ctx_simp_p.set_uint(":max-steps", 5000000);
+    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),

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("elim_and", true);
-    main_p.set_bool(":push-ite-bv", true);
+    main_p.set_bool("push_ite_bv", true);
-    main_p.set_bool(":blast-distinct", true);
+    main_p.set_bool("blast_distinct", true);
 
     params_ref simp2_p = p;
-    simp2_p.set_bool(":som", true);
+    simp2_p.set_bool("som", true);
-    simp2_p.set_bool(":pull-cheap-ite", true);
+    simp2_p.set_bool("pull_cheap_ite", true);
-    simp2_p.set_bool(":push-ite-bv", false);
+    simp2_p.set_bool("push_ite_bv", false);
-    simp2_p.set_bool(":local-ctx", true);
+    simp2_p.set_bool("local_ctx", true);
-    simp2_p.set_uint(":local-ctx-limit", 10000000);
+    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_depth", 32);
-    ctx_simp_p.set_uint(":max-steps", 50000000);
+    ctx_simp_p.set_uint("max_steps", 50000000);
 
     params_ref hoist_p;
-    hoist_p.set_bool(":hoist-mul", true);
+    hoist_p.set_bool("hoist_mul", true);
-    hoist_p.set_bool(":som", false);
+    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.

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("elim_and", true);
-    main_p.set_bool(":blast-distinct", true);
+    main_p.set_bool("blast_distinct", true);
-    main_p.set_bool(":som", 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("pull_cheap_ite", true);
-    pull_ite_p.set_bool(":local-ctx", true);
+    pull_ite_p.set_bool("local_ctx", true);
-    pull_ite_p.set_uint(":local-ctx-limit", 10000000);
+    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("flat", false); 
-    bv_solver_p.set_bool(":som", 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<double>(BIG_PROBLEM))),
                               mk_and(mk_not(mk_produce_proofs_probe()),

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("arith.branch_cut_ratio", 10000000);
-    solver_p.set_uint(":random-seed", rs);
+    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("arith.branch_cut_ratio", 10000000);
-    solver_p.set_uint(":random-seed", rs);
+    solver_p.set_uint("random_seed", rs);
-    solver_p.set_uint(":relevancy", 0);
+    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("flat", false); 
-    solver_p.set_bool(":som", 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_bool("ite_extra", true);    
-    pb2bv_p.set_uint(":pb2bv-all-clauses-limit", 8);
+    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_bool("ite_extra", true);    
-    pb2bv_p.set_uint(":pb2bv-all-clauses-limit", 8);
+    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_lower", rational(-16));
-    add_bounds_p1.set_rat(":add-bound-upper", rational(15));
+    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_lower", rational(-32));
-    add_bounds_p2.set_rat(":add-bound-upper", rational(31));
+    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("elim_and", true);
-    main_p.set_bool(":som", true);
+    main_p.set_bool("som", true);
-    // main_p.set_bool(":push-ite-arith", 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("pull_cheap_ite", true);
-    pull_ite_p.set_bool(":push-ite-arith", false);
+    pull_ite_p.set_bool("push_ite_arith", false);
-    pull_ite_p.set_bool(":local-ctx", true);
+    pull_ite_p.set_bool("local_ctx", true);
-    pull_ite_p.set_uint(":local-ctx-limit", 10000000);
+    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_depth", 30);
-    ctx_simp_p.set_uint(":max-steps", 5000000);
+    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,

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("elim_and", true);
-    main_p.set_bool(":som", true);
+    main_p.set_bool("som", true);
-    main_p.set_bool(":blast-distinct", 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_depth", 30);
-    ctx_simp_p.set_uint(":max-steps", 5000000);
+    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);
-    lhs_p.set_bool(":eq2ineq", 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

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("flat", false);
-    p.set_bool(":hi-div0", true); 
+    p.set_bool("hi_div0", true); 
-    p.set_bool(":elim-and", true);
+    p.set_bool("elim_and", true);
-    p.set_bool(":blast-distinct", true);
+    p.set_bool("blast_distinct", true);
     
     params_ref simp2_p = p;
-    simp2_p.set_bool(":local-ctx", true);
+    simp2_p.set_bool("local_ctx", true);
-    simp2_p.set_uint(":local-ctx-limit", 10000000);
+    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("pull_cheap_ite", true);
-    pull_ite_p.set_bool(":local-ctx", true);
+    pull_ite_p.set_bool("local_ctx", true);
-    pull_ite_p.set_uint(":local-ctx-limit", 10000000);
+    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_depth", 30);
-    ctx_simp_p.set_uint(":max-steps", 5000000);
+    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),

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_uint("seed", 11);
-    p1.set_bool(":factor", false);
+    p1.set_bool("factor", false);
     params_ref p2 = p;
-    p2.set_uint(":seed", 13);
+    p2.set_uint("seed", 13);
-    p2.set_bool(":factor", false);
+    p2.set_bool("factor", false);
 
     return and_then(mk_simplify_tactic(m, p), 
                     mk_propagate_values_tactic(m, p),

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("pull_cheap_ite", true);
-    s2_p.set_bool(":local-ctx", true);
+    s2_p.set_bool("local_ctx", true);
-    s2_p.set_uint(":local-ctx-limit", 10000000);
+    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),

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("elim_and", true);
-    main_p.set_bool(":blast-distinct", true);
+    main_p.set_bool("blast_distinct", true);
 
     tactic * preamble_st = and_then(mk_simplify_tactic(m),
                                     mk_propagate_values_tactic(m),

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("pull_cheap_ite", true);
-    pull_ite_p.set_bool(":local-ctx", true);
+    pull_ite_p.set_bool("local_ctx", true);
-    pull_ite_p.set_uint(":local-ctx-limit", 10000000);
+    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_depth", 30);
-    ctx_simp_p.set_uint(":max-steps", 5000000);
+    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");
+    qi_p.set_str("qi.cost", "0");
-    TRACE("qi_cost", qi_p.display(tout); tout << "\n" << qi_p.get_str("qi_cost", "<null>") << "\n";);
+    TRACE("qi_cost", qi_p.display(tout); tout << "\n" << qi_p.get_str("qi.cost", "<null>") << "\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<double>(128)))),
                                             using_params(mk_smt_tactic(), qi_p),

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_bool("mbqi", true);
-    main_p.set_uint(":mbqi-max-iterations", -1);
+    main_p.set_uint("mbqi_max_iterations", -1);
-    main_p.set_bool(":elim-and", true);
+    main_p.set_bool("elim_and", true);
-    main_p.set_bool(":solver", 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));

src/test/dl_context.cpp

@@ -72,9 +72,9 @@ void tst_dl_context() {
 
     params_ref params;
     for(unsigned rel_index=0; rel_index<rel_cnt; rel_index++) {
-        params.set_sym(":default-relation", relations[rel_index]);
+        params.set_sym("default_relation", relations[rel_index]);
         for(int eager_checking=1; eager_checking>=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";

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);
     
 }

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_table", symbol("sparse"));
-    params.set_sym(":default-relation", symbol("tr_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;

src/util/debug.cpp

@@ -22,6 +22,7 @@ Revision History:
 #endif
 #include<iostream>
 #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());

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;

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;