From 9754ccf8a14750eded85360c96414e1736846fe0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 4 Dec 2012 11:16:42 -0800 Subject: [PATCH 1/2] fixing problems with the new parameter framework Signed-off-by: Leonardo de Moura --- src/cmd_context/basic_cmds.cpp | 4 ++-- src/cmd_context/cmd_context.cpp | 10 ++++++++++ src/cmd_context/cmd_context.h | 1 + src/parsers/smt2/smt2parser.cpp | 22 ++++++++++++++++------ src/smt/params/smt_params_helper.pyg | 1 + src/smt/params/theory_arith_params.cpp | 1 + src/tactic/core/nnf_tactic.cpp | 2 +- 7 files changed, 32 insertions(+), 9 deletions(-) diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index df9efc4dd..8f65485ae 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -307,7 +307,7 @@ class set_option_cmd : public set_get_option_cmd { try { gparams::set(m_option, value); env_params::updt_params(); - ctx.params().updt_params(); + ctx.global_params_updated(); } catch (gparams::exception ex) { throw cmd_exception(ex.msg()); @@ -517,7 +517,7 @@ public: } else { try { - std::string val = gparams::get_value(opt); + ctx.regular_stream() << gparams::get_value(opt) << std::endl; } 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 b27e1e177..0380e91ea 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -342,6 +342,16 @@ cmd_context::~cmd_context() { m_check_sat_result = 0; } +void cmd_context::global_params_updated() { + m_params.updt_params(); + if (m_solver) { + params_ref p; + if (!m_params.m_auto_config) + p.set_bool("auto_config", false); + m_solver->updt_params(p); + } +} + void cmd_context::set_produce_models(bool f) { if (m_solver) m_solver->set_produce_models(f); diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index ca3ada7cf..2edc87ca6 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -249,6 +249,7 @@ public: cmd_context(bool main_ctx = true, ast_manager * m = 0, symbol const & l = symbol::null); ~cmd_context(); context_params & params() { return m_params; } + void global_params_updated(); // this method should be invoked when global (and module) params are updated. void set_logic(symbol const & s); bool has_logic() const { return m_logic != symbol::null; } symbol const & get_logic() const { return m_logic; } diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index c0c8d5bc5..ee93dca2f 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -35,6 +35,7 @@ namespace smt2 { class parser { cmd_context & m_ctx; + params_ref m_params; scanner m_scanner; scanner::token m_curr; cmd * m_curr_cmd; @@ -2285,6 +2286,10 @@ namespace smt2 { shrink(m_sexpr_stack, sexpr_spos); m_symbol_stack.shrink(sym_spos); m_num_bindings = 0; + // HACK for propagating the update of parser parameters + if (norm_param_name(s) == "set_option") { + updt_params(); + } return; } else { @@ -2357,9 +2362,10 @@ namespace smt2 { } public: - parser(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & _p): + parser(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & p): m_ctx(ctx), - m_scanner(ctx, is, interactive, _p), + m_params(p), + m_scanner(ctx, is, interactive, p), m_curr(scanner::NULL_TOKEN), m_curr_cmd(0), m_num_bindings(0), @@ -2397,15 +2403,19 @@ namespace smt2 { // the following assertion does not hold if ctx was already attached to an AST manager before the parser object is created. // SASSERT(!m_ctx.has_manager()); - parser_params p(_p); - m_ignore_user_patterns = p.ignore_user_patterns(); - m_ignore_bad_patterns = p.ignore_bad_patterns(); - m_display_error_for_vs = p.error_for_visual_studio(); + updt_params(); } ~parser() { reset_stack(); } + + void updt_params() { + parser_params p(m_params); + m_ignore_user_patterns = p.ignore_user_patterns(); + m_ignore_bad_patterns = p.ignore_bad_patterns(); + m_display_error_for_vs = p.error_for_visual_studio(); + } void reset() { reset_stack(); diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index bcdf78b73..ee583ff85 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -35,6 +35,7 @@ def_module_params(module_name='smt', ('arith.nl.rounds', UINT, 1024, 'threshold for number of (nested) final checks for non linear arithmetic'), ('arith.euclidean_solver', BOOL, False, 'eucliean solver for linear integer arithmetic'), ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'), + ('arith.propagation_mode', UINT, 2, '0 - no propagation, 1 - propagate existing literals, 2 - refine bounds'), ('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'), ('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'), ('arith.ignore_int', BOOL, False, 'treat integer variables as real'))) diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp index 5a1101524..7281a5daa 100644 --- a/src/smt/params/theory_arith_params.cpp +++ b/src/smt/params/theory_arith_params.cpp @@ -32,6 +32,7 @@ void theory_arith_params::updt_params(params_ref const & _p) { m_arith_branch_cut_ratio = p.arith_branch_cut_ratio(); m_arith_int_eq_branching = p.arith_int_eq_branch(); m_arith_ignore_int = p.arith_ignore_int(); + m_arith_bound_prop = static_cast(p.arith_propagation_mode()); } diff --git a/src/tactic/core/nnf_tactic.cpp b/src/tactic/core/nnf_tactic.cpp index fdaf03d55..a79a4ed06 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("mode", symbol("full")); TRACE("nnf", tout << "mk_nnf: " << new_p << "\n";); return using_params(mk_snf_tactic(m, p), new_p); } From ff999773b2a75fa8c9f362d00c31d38ea116447e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 4 Dec 2012 11:17:24 -0800 Subject: [PATCH 2/2] adjusting verbose msgs Signed-off-by: Leonardo de Moura --- src/smt/smt_model_checker.cpp | 15 +++++++-------- src/smt/smt_quantifier.cpp | 3 +-- 2 files changed, 8 insertions(+), 10 deletions(-) diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 704c272ee..53f3af961 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -312,7 +312,7 @@ namespace smt { TRACE("model_checker", tout << "MODEL_CHECKER INVOKED\n"; tout << "model:\n"; model_pp(tout, *m_curr_model);); if (m_params.m_mbqi_trace) { - verbose_stream() << "[mbqi] started\n"; + verbose_stream() << "(smt.mbqi \"started\")\n"; } init_aux_context(); @@ -324,13 +324,12 @@ namespace smt { quantifier * q = *it; if (m_context->is_relevant(q) && m_context->get_assignment(q) == l_true) { if (m_params.m_mbqi_trace && q->get_qid() != symbol::null) { - verbose_stream() << "[mbqi] checking: " << q->get_qid() << "\n"; + verbose_stream() << "(smt.mbqi :checking " << q->get_qid() << ")\n"; } found_relevant = true; if (!check(q)) { - IF_VERBOSE(5, verbose_stream() << "current model does not satisfy: " << q->get_qid() << "\n";); - if (m_params.m_mbqi_trace) { - verbose_stream() << "[mbqi] failed " << q->get_qid() << "\n"; + if (m_params.m_mbqi_trace || get_verbosity_level() >= 5) { + verbose_stream() << "(smt.mbqi :failed " << q->get_qid() << ")\n"; } num_failures++; } @@ -347,9 +346,9 @@ namespace smt { m_curr_model->cleanup(); if (m_params.m_mbqi_trace) { if (num_failures == 0) - verbose_stream() << "[mbqi] succeeded\n"; + verbose_stream() << "(smt.mbqi :succeeded true)\n"; else - verbose_stream() << "[mbqi] num failures " << num_failures << "\n"; + verbose_stream() << "(smt.mbqi :num-failures " << num_failures << ")\n"; } return num_failures == 0; } @@ -360,7 +359,7 @@ namespace smt { } void model_checker::restart_eh() { - IF_VERBOSE(100, verbose_stream() << "instantiating new instances...\n";); + IF_VERBOSE(100, verbose_stream() << "(smt.mbqi \"instantiating new instances...\")\n";); assert_new_instances(); reset_new_instances(); } diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 799dd3c49..d56fe0cff 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -562,7 +562,7 @@ namespace smt { virtual quantifier_manager::check_model_result check_model(proto_model * m, obj_map const & root2value) { if (m_fparams->m_mbqi) { - IF_VERBOSE(10, verbose_stream() << "model based quantifier instantiation...\n";); + IF_VERBOSE(10, verbose_stream() << "(smt.mbqi)\n";); if (m_model_checker->check(m, root2value)) { return quantifier_manager::SAT; } @@ -594,7 +594,6 @@ namespace smt { final_check_status final_check_quant() { if (use_ematching()) { if (m_lazy_matching_idx < m_fparams->m_qi_max_lazy_multipattern_matching) { - IF_VERBOSE(100, verbose_stream() << "matching delayed multi-patterns... \n";); m_lazy_mam->rematch(); m_context->push_trail(value_trail(m_lazy_matching_idx)); m_lazy_matching_idx++;