diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 45892bac3..c604927fd 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -675,7 +675,7 @@ extern "C" { ast_manager & m = mk_c(c)->m(); expr * a = to_expr(_a); params_ref p = to_param_ref(_p); - unsigned timeout = p.get_uint("timeout", UINT_MAX); + unsigned timeout = p.get_uint("timeout", mk_c(c)->get_timeout()); bool use_ctrl_c = p.get_bool("ctrl_c", false); th_rewriter m_rw(m, p); expr_ref result(m); diff --git a/src/api/api_config_params.cpp b/src/api/api_config_params.cpp index c14e68919..908900043 100644 --- a/src/api/api_config_params.cpp +++ b/src/api/api_config_params.cpp @@ -17,7 +17,6 @@ Revision History: --*/ #include"z3.h" #include"api_context.h" -#include"api_config_params.h" #include"pp.h" #include"api_log_macros.h" #include"api_util.h" @@ -25,16 +24,7 @@ Revision History: #include"symbol.h" #include"gparams.h" #include"env_params.h" - -namespace api { - - config_params::config_params() { - } - - config_params::config_params(front_end_params const & p):m_params(p) { - } - -}; +#include"context_params.h" extern "C" { void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value) { @@ -68,7 +58,7 @@ extern "C" { // The error handler is only available for contexts // Just throw a warning. std::ostringstream buffer; - buffer << "Error setting " << param_id << ", " << ex.msg(); + buffer << "Error setting " << param_id << ": " << ex.msg(); warning_msg(buffer.str().c_str()); return Z3_FALSE; } @@ -77,28 +67,41 @@ extern "C" { Z3_config Z3_API Z3_mk_config() { memory::initialize(UINT_MAX); LOG_Z3_mk_config(); - Z3_config r = reinterpret_cast(alloc(api::config_params)); + Z3_config r = reinterpret_cast(alloc(context_params)); RETURN_Z3(r); } void Z3_API Z3_del_config(Z3_config c) { LOG_Z3_del_config(c); - dealloc((reinterpret_cast(c))); + dealloc((reinterpret_cast(c))); } void Z3_API Z3_set_param_value(Z3_config c, char const * param_id, char const * param_value) { LOG_Z3_set_param_value(c, param_id, param_value); - // PARAM-TODO save the parameter + try { + context_params * p = reinterpret_cast(c); + p->set(param_id, param_value); + } + catch (z3_exception & ex) { + // The error handler is only available for contexts + // Just throw a warning. + std::ostringstream buffer; + buffer << "Error setting " << param_id << ": " << ex.msg(); + warning_msg(buffer.str().c_str()); + } } void Z3_API Z3_update_param_value(Z3_context c, Z3_string param_id, Z3_string param_value) { + Z3_TRY; LOG_Z3_update_param_value(c, param_id, param_value); RESET_ERROR_CODE(); - // NOOP in the current version + mk_c(c)->params().set(param_id, param_value); + Z3_CATCH; } Z3_bool Z3_API Z3_get_param_value(Z3_context c, Z3_string param_id, Z3_string* param_value) { LOG_Z3_get_param_value(c, param_id, param_value); + // TODO return Z3_FALSE; } diff --git a/src/api/api_config_params.h b/src/api/api_config_params.h deleted file mode 100644 index 99ded289d..000000000 --- a/src/api/api_config_params.h +++ /dev/null @@ -1,34 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - api_config_params.h - -Abstract: - Configuration parameters - -Author: - - Leonardo de Moura (leonardo) 2012-02-29. - -Revision History: - ---*/ -#ifndef _API_CONFIG_PARAMS_H_ -#define _API_CONFIG_PARAMS_H_ - -#include"front_end_params.h" - -namespace api { - - class config_params { - public: - front_end_params m_params; - config_params(); - config_params(front_end_params const & p); - }; - -}; - -#endif diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 11fb28a02..02069e06d 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -18,7 +18,6 @@ Revision History: --*/ #include"api_context.h" -#include"api_config_params.h" #include"smtparser.h" #include"version.h" #include"ast_pp.h" @@ -54,14 +53,6 @@ namespace api { return static_cast(f); } - context::param_ini::param_ini(front_end_params & p) : m_params(p) { - p.open_trace_file(); - } - - context::param_ini::~param_ini() { - m_params.close_trace_file(); - } - context::add_plugins::add_plugins(ast_manager & m) { reg_decl_plugins(m); } @@ -88,10 +79,10 @@ namespace api { } } - context::context(config_params * p, bool user_ref_count): - m_params(p ? p->m_params : front_end_params()), + context::context(context_params * p, bool user_ref_count): + m_params(*p), m_user_ref_count(user_ref_count), - m_manager(m_params.m_proof_mode, m_params.m_trace_stream), + m_manager(m_params.m_proof ? PGM_FINE : PGM_DISABLED), // PARAM-TODO , _fparams.m_proof_mode, m_fparams.m_trace_stream), m_plugins(m_manager), m_arith_util(m_manager), m_bv_util(m_manager), @@ -114,8 +105,6 @@ namespace api { // // Configuration parameter settings. // - memory::set_high_watermark(static_cast(m_params.m_memory_high_watermark)*1024*1024); - memory::set_max_size(static_cast(m_params.m_memory_max_size)*1024*1024); if (m_params.m_debug_ref_count) { m_manager.debug_ref_count(); } @@ -334,7 +323,8 @@ namespace api { smt::kernel & context::get_smt_kernel() { if (!m_solver) { - m_solver = alloc(smt::kernel, m_manager, m_params); + // PARAM-TODO: copy config_params -> fparams + m_solver = alloc(smt::kernel, m_manager, m_fparams); } return *m_solver; } @@ -419,15 +409,15 @@ extern "C" { Z3_context Z3_API Z3_mk_context(Z3_config c) { LOG_Z3_mk_context(c); - memory::initialize(0); - Z3_context r = reinterpret_cast(alloc(api::context, reinterpret_cast(c), false)); + memory::initialize(UINT_MAX); + Z3_context r = reinterpret_cast(alloc(api::context, reinterpret_cast(c), false)); RETURN_Z3(r); } Z3_context Z3_API Z3_mk_context_rc(Z3_config c) { LOG_Z3_mk_context_rc(c); - memory::initialize(0); - Z3_context r = reinterpret_cast(alloc(api::context, reinterpret_cast(c), true)); + memory::initialize(UINT_MAX); + Z3_context r = reinterpret_cast(alloc(api::context, reinterpret_cast(c), true)); RETURN_Z3(r); } @@ -573,11 +563,4 @@ ast_manager & Z3_API Z3_get_manager(__in Z3_context c) { return mk_c(c)->m(); } -front_end_params& Z3_API Z3_get_parameters(__in Z3_context c) { - return mk_c(c)->fparams(); -} -Z3_context Z3_mk_context_from_params(front_end_params const& p) { - api::config_params cp(p); - return reinterpret_cast(alloc(api::context, &cp)); -} diff --git a/src/api/api_context.h b/src/api/api_context.h index 76c601d60..df0f488af 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -31,28 +31,19 @@ Revision History: #include"front_end_params.h" #include"event_handler.h" #include"tactic_manager.h" +#include"context_params.h" namespace smtlib { class parser; }; namespace api { - class config_params; - Z3_search_failure mk_Z3_search_failure(smt::failure f); class context : public tactic_manager { - class param_ini { - front_end_params & m_params; - public: - param_ini(front_end_params & p); - ~param_ini(); - }; - struct add_plugins { add_plugins(ast_manager & m); }; - - front_end_params m_params; + context_params m_params; bool m_user_ref_count; //!< if true, the user is responsible for managing referenc counters. ast_manager m_manager; add_plugins m_plugins; @@ -61,8 +52,11 @@ namespace api { bv_util m_bv_util; datalog::dl_decl_util m_datalog_util; + // Support for old solver API + front_end_params m_fparams; smt::kernel * m_solver; // General purpose solver for backward compatibility - + // ------------------------------- + ast_ref_vector m_last_result; //!< used when m_user_ref_count == true ast_ref_vector m_ast_trail; //!< used when m_user_ref_count == false unsigned_vector m_ast_lim; @@ -102,11 +96,16 @@ namespace api { // // ------------------------ - context(config_params * p, bool user_ref_count = false); + context(context_params * p, bool user_ref_count = false); ~context(); - - front_end_params & fparams() { return m_params; } ast_manager & m() { return m_manager; } + + context_params & params() { return m_params; } + bool produce_proofs() const { return m_manager.proofs_enabled(); } + bool produce_models() const { return m_params.m_model; } + bool produce_unsat_cores() const { return m_params.m_unsat_core; } + bool use_auto_config() const { return m_params.m_auto_config; } + unsigned get_timeout() const { return m_params.m_timeout; } arith_util & autil() { return m_arith_util; } bv_util & bvutil() { return m_bv_util; } datalog::dl_decl_util & datalog_util() { return m_datalog_util; } @@ -167,12 +166,13 @@ namespace api { static void out_of_memory_handler(void * _ctx); void check_sorts(ast * n); + // ------------------------ // // Solver interface for backward compatibility // // ------------------------ - + front_end_params & fparams() { return m_fparams; } bool has_solver() const { return m_solver != 0; } smt::kernel & get_smt_kernel(); void assert_cnstr(expr * a); diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index 34ca9627a..4c54a4332 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -265,7 +265,7 @@ extern "C" { RESET_ERROR_CODE(); lbool r = l_undef; cancel_eh eh(*to_fixedpoint_ref(d)); - unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", UINT_MAX); + unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", mk_c(c)->get_timeout()); api::context::set_interruptable(*(mk_c(c)), eh); { scoped_timer timer(timeout, &eh); @@ -289,7 +289,7 @@ extern "C" { LOG_Z3_fixedpoint_query_relations(c, d, num_relations, relations); RESET_ERROR_CODE(); lbool r = l_undef; - unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", UINT_MAX); + unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", mk_c(c)->get_timeout()); cancel_eh eh(*to_fixedpoint_ref(d)); api::context::set_interruptable(*(mk_c(c)), eh); { diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 31901d360..67d083704 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -36,10 +36,17 @@ extern "C" { static void init_solver_core(Z3_context c, Z3_solver _s) { ast_manager & m = mk_c(c)->m(); Z3_solver_ref * s = to_solver(_s); - s->m_solver->set_produce_proofs(m.proofs_enabled()); - s->m_solver->set_produce_unsat_cores(s->m_params.get_bool("unsat_core", false)); - s->m_solver->set_produce_models(s->m_params.get_bool("model", true)); - s->m_solver->updt_params(s->m_params); + s->m_solver->set_produce_proofs(mk_c(c)->produce_proofs()); + s->m_solver->set_produce_unsat_cores(s->m_params.get_bool("unsat_core", mk_c(c)->produce_unsat_cores())); + s->m_solver->set_produce_models(s->m_params.get_bool("model", mk_c(c)->produce_models())); + if (!mk_c(c)->use_auto_config()) { + params_ref p = s->m_params; + p.set_bool("auto_config", false); + s->m_solver->updt_params(p); + } + else { + s->m_solver->updt_params(s->m_params); + } s->m_solver->init(m, s->m_logic); s->m_initialized = true; } @@ -237,7 +244,7 @@ extern "C" { } } expr * const * _assumptions = to_exprs(assumptions); - unsigned timeout = to_solver(s)->m_params.get_uint("timeout", UINT_MAX); + unsigned timeout = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout()); bool use_ctrl_c = to_solver(s)->m_params.get_bool("ctrl_c", false); cancel_eh eh(*to_solver_ref(s)); api::context::set_interruptable(*(mk_c(c)), eh); diff --git a/src/api/z3_api.h b/src/api/z3_api.h index a0c6434c2..16bf9193c 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1308,6 +1308,12 @@ extern "C" { - debug_ref_count (Boolean) Enable debug support for Z3_ast reference counting - trace (Boolean) Tracing support for VCC - trace_file_name (String) Trace out file for VCC traces + - timeout (unsigned) default timeout (in milliseconds) used for solvers + - well_sorted_check type checker + - auto_config use heuristics to automatically select solver and configure it + - model model generation for solvers, this parameter can be overwritten when creating a solver + - validate_model validate models produced by solvers + - unsat_core unsat-core generation for solvers, this parameter can be overwritten when creating a solver \sa Z3_set_param_value \sa Z3_del_config @@ -1420,19 +1426,18 @@ extern "C" { #endif /** - \brief This is a deprecated function. This is a NOOP in the current version of Z3. + \brief Set a value of a context parameter. - \deprecated Use #Z3_global_param_set. + \sa Use #Z3_global_param_set. def_API('Z3_update_param_value', VOID, (_in(CONTEXT), _in(STRING), _in(STRING))) */ void Z3_API Z3_update_param_value(__in Z3_context c, __in Z3_string param_id, __in Z3_string param_value); /** - \brief This is a deprecated function. This is a NOOP in the current version of Z3. - It always return Z3_FALSE. + \brief Return the value of a context parameter. - \deprecated Use #Z3_global_param_get + \sa Use #Z3_global_param_get def_API('Z3_get_param_value', BOOL, (_in(CONTEXT), _in(STRING), _out(STRING))) */