From f15de18c4a6041d8f752f0606f2c30f903a00db7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 1 Dec 2012 22:53:55 -0800 Subject: [PATCH] context params Signed-off-by: Leonardo de Moura --- src/cmd_context/basic_cmds.cpp | 3 + src/cmd_context/cmd_context.cpp | 49 +++++----- src/cmd_context/cmd_context.h | 7 +- src/cmd_context/context_params.cpp | 114 ++++++++++++++++++++++ src/cmd_context/context_params.h | 52 ++++++++++ src/front_end_params/front_end_params.cpp | 5 - src/shell/datalog_frontend.h | 1 - src/shell/main.cpp | 3 - src/solver/strategic_solver.cpp | 2 - src/util/env_params.cpp | 2 +- src/util/gparams.cpp | 4 +- 11 files changed, 204 insertions(+), 38 deletions(-) create mode 100644 src/cmd_context/context_params.cpp create mode 100644 src/cmd_context/context_params.h diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index d3861257b..df9efc4dd 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -29,6 +29,7 @@ Notes: #include"eval_cmd.h" #include"gparams.h" #include"model_params.hpp" +#include"env_params.h" class help_cmd : public cmd { svector m_cmds; @@ -305,6 +306,8 @@ class set_option_cmd : public set_get_option_cmd { void set_param(cmd_context & ctx, char const * value) { try { gparams::set(m_option, value); + env_params::updt_params(); + ctx.params().updt_params(); } catch (gparams::exception ex) { throw cmd_exception(ex.msg()); diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 984a535c7..1a018a41d 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -359,48 +359,43 @@ cmd_context::~cmd_context() { } void cmd_context::set_produce_models(bool f) { - // PARAM-TODO - // params().m_model = f; if (m_solver) m_solver->set_produce_models(f); + m_params.m_model = f; } void cmd_context::set_produce_unsat_cores(bool f) { // can only be set before initialization SASSERT(!has_manager()); - m_produce_unsat_cores = f; + m_params.m_unsat_core = f; } void cmd_context::set_produce_proofs(bool f) { - // PARAM-TODO // can only be set before initialization SASSERT(!has_manager()); - // params().m_proof_mode = f ? PGM_FINE : PGM_DISABLED; + m_params.m_proof = f; } bool cmd_context::produce_models() const { - // PARAM-TODO - // return params().m_model; - return true; + return m_params.m_model; } bool cmd_context::produce_proofs() const { - // PARAM-TODO - // return params().m_proof_mode != PGM_DISABLED; - return false; + return m_params.m_proof; +} + +bool cmd_context::produce_unsat_cores() const { + return m_params.m_unsat_core; } bool cmd_context::well_sorted_check_enabled() const { - // PARAM-TODO - return true; + return m_params.m_well_sorted_check; } bool cmd_context::validate_model_enabled() const { - // PARAM-TODO - return false; + return m_params.m_validate_model; } - cmd_context::check_sat_state cmd_context::cs_state() const { if (m_check_sat_result.get() == 0) return css_clear; @@ -593,10 +588,7 @@ void cmd_context::init_manager_core(bool new_manager) { insert(pm().mk_plist_decl()); } if (m_solver) { - m_solver->set_produce_unsat_cores(produce_unsat_cores()); - m_solver->set_produce_models(produce_models()); - m_solver->set_produce_proofs(produce_proofs()); - m_solver->init(m(), m_logic); + init_solver_options(m_solver.get()); } m_check_logic.set_logic(m(), m_logic); } @@ -1455,14 +1447,23 @@ void cmd_context::validate_model() { } } +void cmd_context::init_solver_options(solver * s) { + m_solver->set_produce_unsat_cores(produce_unsat_cores()); + m_solver->set_produce_models(produce_models()); + m_solver->set_produce_proofs(produce_proofs()); + m_solver->init(m(), m_logic); + if (!m_params.m_auto_config) { + params_ref p; + p.set_bool("auto_config", false); + m_solver->updt_params(p); + } +} + void cmd_context::set_solver(solver * s) { m_check_sat_result = 0; m_solver = s; if (has_manager() && s != 0) { - m_solver->set_produce_unsat_cores(produce_unsat_cores()); - m_solver->set_produce_models(produce_models()); - m_solver->set_produce_proofs(produce_proofs()); - m_solver->init(m(), m_logic); + init_solver_options(s); // assert formulas and create scopes in the new solver. unsigned lim = 0; svector::iterator it = m_scopes.begin(); diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index c2acba0dc..ae517b0c2 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -36,6 +36,7 @@ Notes: #include"check_logic.h" #include"progress_callback.h" #include"scoped_ptr_vector.h" +#include"context_params.h" /** \brief Auxiliary function for converting SMT2 keywords into Z3 internal parameter names. @@ -135,6 +136,7 @@ public: }; protected: + context_params m_params; bool m_main_ctx; symbol m_logic; bool m_interactive_mode; @@ -246,9 +248,12 @@ protected: void print_unsupported_msg() { regular_stream() << "unsupported" << std::endl; } void print_unsupported_info(symbol const& s) { if (s != symbol::null) diagnostic_stream() << "; " << s << std::endl;} + void init_solver_options(solver * s); + 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 set_logic(symbol const & s); bool has_logic() const { return m_logic != symbol::null; } symbol const & get_logic() const { return m_logic; } @@ -270,7 +275,7 @@ public: void set_random_seed(unsigned s) { m_random_seed = s; } bool produce_models() const; bool produce_proofs() const; - bool produce_unsat_cores() const { return m_produce_unsat_cores; } + bool produce_unsat_cores() const; bool well_sorted_check_enabled() const; bool validate_model_enabled() const; void set_produce_models(bool flag); diff --git a/src/cmd_context/context_params.cpp b/src/cmd_context/context_params.cpp new file mode 100644 index 000000000..c7efa0d8d --- /dev/null +++ b/src/cmd_context/context_params.cpp @@ -0,0 +1,114 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + context_params.cpp + +Abstract: + + Goodies for managing context parameters in the cmd_context and + api_context + +Author: + + Leonardo (leonardo) 2012-12-01 + +Notes: + +--*/ +#include"context_params.h" +#include"gparams.h" +#include"params.h" + +context_params::context_params() { + updt_params(); +} + +void context_params::set_bool(bool & opt, char const * param, char const * value) { + if (strcmp(value, "true") == 0) { + opt = true; + } + else if (strcmp(value, "false") == 0) { + opt = false; + } + else { + throw default_exception("invalid value '%s' for Boolean parameter '%s'", value, param); + } +} + +void context_params::set(char const * param, char const * value) { + std::string p = param; + unsigned n = p.size(); + for (unsigned i = 0; i < n; i++) { + if (p[i] >= 'A' && p[i] <= 'Z') + p[i] = p[i] - 'A' + 'a'; + else if (p[i] == '-') + p[i] = '_'; + } + if (p == "timeout") { + long val = strtol(value, 0, 10); + m_timeout = static_cast(val); + } + else if (p == "type_check" || p == "well_sorted_check") { + set_bool(m_well_sorted_check, param, value); + } + else if (p == "auto_config") { + set_bool(m_auto_config, param, value); + } + else if (p == "proof") { + set_bool(m_proof, param, value); + } + else if (p == "model") { + set_bool(m_model, param, value); + } + else if (p == "validate_model") { + set_bool(m_validate_model, param, value); + } + else if (p == "trace") { + set_bool(m_trace, param, value); + } + else if (p == "trace_file_name") { + m_trace_file_name = value; + } + else if (p == "unsat_core") { + set_bool(m_unsat_core, param, value); + } + else if (p == "debug_ref_count") { + set_bool(m_debug_ref_count, param, value); + } + else { + throw default_exception("unknown parameter '%s'", p.c_str()); + } +} + +void context_params::updt_params() { + updt_params(gparams::get()); +} + +void context_params::updt_params(params_ref const & p) { + m_timeout = p.get_uint("timeout", UINT_MAX); + m_well_sorted_check = p.get_bool("type_check", p.get_bool("well_sorted_check", true)); + m_auto_config = p.get_bool("auto_config", true); + m_proof = p.get_bool("proof", false); + m_model = p.get_bool("model", true); + m_validate_model = p.get_bool("validate_model", false); + m_trace = p.get_bool("trace", false); + m_trace_file_name = p.get_str("trace_file_name", "z3.log"); + m_unsat_core = p.get_bool("unsat_core", false); + m_debug_ref_count = p.get_bool("debug_ref_count", false); +} + +void context_params::collect_param_descrs(param_descrs & d) { + d.insert("timeout", CPK_UINT, "default timeout (in milliseconds) used for solvers", "4294967295"); + d.insert("well_sorted_check", CPK_BOOL, "type checker", "true"); + d.insert("type_check", CPK_BOOL, "type checker (alias for well_sorted_check)", "true"); + d.insert("auto_config", CPK_BOOL, "use heuristics to automatically select solver and configure it", "true"); + d.insert("proof", CPK_BOOL, "proof generation, it must be enabled when the Z3 context is created", "false"); + d.insert("model", CPK_BOOL, "model generation for solvers, this parameter can be overwritten when creating a solver", "true"); + d.insert("validate_model", CPK_BOOL, "validate models produced by solvers", "false"); + d.insert("trace", CPK_BOOL, "trace generation for VCC", "false"); + d.insert("trace_file_name", CPK_STRING, "trace out file name (see option 'trace')", "z3.log"); + d.insert("unsat_core", CPK_BOOL, "unsat-core generation for solvers, this parameter can be overwritten when creating a solver, not every solver in Z3 supports unsat core generation", "false"); + d.insert("debug_ref_count", CPK_BOOL, "debug support for AST reference counting", "false"); +} diff --git a/src/cmd_context/context_params.h b/src/cmd_context/context_params.h new file mode 100644 index 000000000..556c3bd3f --- /dev/null +++ b/src/cmd_context/context_params.h @@ -0,0 +1,52 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + context_params.h + +Abstract: + + Goodies for managing context parameters in the cmd_context and + api_context + +Author: + + Leonardo (leonardo) 2012-12-01 + +Notes: + +--*/ +#ifndef _CONTEXT_PARAMS_H_ +#define _CONTEXT_PARAMS_H_ + +#include"params.h" + +class context_params { + void set_bool(bool & opt, char const * param, char const * value); + +public: + bool m_auto_config; + bool m_proof; + bool m_debug_ref_count; + bool m_trace; + std::string m_trace_file_name; + bool m_well_sorted_check; + bool m_model; + bool m_validate_model; + bool m_unsat_core; + unsigned m_timeout; + bool m_statistics; + + context_params(); + void set(char const * param, char const * value); + void updt_params(); + void updt_params(params_ref const & p); + static void collect_param_descrs(param_descrs & d); + /* + REG_PARAMS('context_params::collect_param_descrs') + */ +}; + + +#endif diff --git a/src/front_end_params/front_end_params.cpp b/src/front_end_params/front_end_params.cpp index 32692180f..f00c21d56 100644 --- a/src/front_end_params/front_end_params.cpp +++ b/src/front_end_params/front_end_params.cpp @@ -32,10 +32,6 @@ void front_end_params::register_params(ini_params & p) { p.register_bool_param("well_sorted_check", m_well_sorted_check, "enable/disable type checker"); 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"); #ifdef _WINDOWS // The non-windows memory manager does not have access to memory sizes. @@ -47,7 +43,6 @@ void front_end_params::register_params(ini_params & p) { PRIVATE_PARAMS({ - p.register_bool_param("debug_ref_count", m_debug_ref_count); }); } diff --git a/src/shell/datalog_frontend.h b/src/shell/datalog_frontend.h index 7e08fce0e..bf4194ef4 100644 --- a/src/shell/datalog_frontend.h +++ b/src/shell/datalog_frontend.h @@ -23,7 +23,6 @@ struct datalog_params { symbol m_default_table; bool m_default_table_checked; datalog_params(); - // virtual void register_params(ini_params& p); }; unsigned read_datalog(char const * file, datalog_params const& dl_params, front_end_params & front_end_params); diff --git a/src/shell/main.cpp b/src/shell/main.cpp index 90473c21f..9cef54628 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -116,10 +116,7 @@ void init_params() { if (!g_params_initialized) { z3_bound_num_procs(); g_front_end_params = new front_end_params(); - // g_params = new ini_params(); g_extra_params = new extra_params(); - // g_front_end_params->register_params(*g_params); - // g_extra_params->register_params(*g_params); g_params_initialized = true; } } diff --git a/src/solver/strategic_solver.cpp b/src/solver/strategic_solver.cpp index 8ce098c51..40d77066e 100644 --- a/src/solver/strategic_solver.cpp +++ b/src/solver/strategic_solver.cpp @@ -99,8 +99,6 @@ void strategic_solver::updt_params(params_ref const & p) { m_inc_solver->updt_params(p); m_params = p; m_auto_config = p.get_bool("auto_config", true); - // PARAM-TODO - // PROOFS, MODELS, UNSATCORES } void strategic_solver::collect_param_descrs(param_descrs & r) { diff --git a/src/util/env_params.cpp b/src/util/env_params.cpp index cf1d31b85..a76c2308b 100644 --- a/src/util/env_params.cpp +++ b/src/util/env_params.cpp @@ -24,7 +24,7 @@ Notes: void env_params::updt_params() { params_ref p = gparams::get(); - set_verbosity_level(p.get_uint("verbose", 0)); + set_verbosity_level(p.get_uint("verbose", get_verbosity_level())); enable_warning_messages(p.get_bool("warning", true)); memory::set_max_size(p.get_uint("memory_max_size", 0)); } diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index 29377eb8d..85b648a55 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -86,7 +86,9 @@ public: void display(std::ostream & out, unsigned indent, bool smt2_style) { #pragma omp critical (gparams) { - m_param_descrs.display(out, indent, smt2_style); + out << "Global parameters\n"; + m_param_descrs.display(out, indent + 4, smt2_style); + out << "\n"; dictionary::iterator it = m_module_param_descrs.begin(); dictionary::iterator end = m_module_param_descrs.end(); for (; it != end; ++it) {