diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c index 70cdc2852..27bf6de2c 100644 --- a/examples/c/test_capi.c +++ b/examples/c/test_capi.c @@ -70,7 +70,7 @@ Z3_context mk_context_custom(Z3_config cfg, Z3_error_handler err) { Z3_context ctx; - Z3_set_param_value(cfg, "MODEL", "true"); + Z3_set_param_value(cfg, "model", "true"); ctx = Z3_mk_context(cfg); Z3_set_error_handler(ctx, err); @@ -105,7 +105,7 @@ Z3_context mk_context() Z3_context mk_proof_context() { Z3_config cfg = Z3_mk_config(); Z3_context ctx; - Z3_set_param_value(cfg, "PROOF_MODE", "2"); + Z3_set_param_value(cfg, "proof", "true"); ctx = mk_context_custom(cfg, throw_z3_error); Z3_del_config(cfg); return ctx; @@ -1038,12 +1038,12 @@ void quantifier_example1() /* If quantified formulas are asserted in a logical context, then Z3 may return L_UNDEF. In this case, the model produced by Z3 should be viewed as a potential/candidate model. */ - Z3_set_param_value(cfg, "MODEL", "true"); + /* The current model finder for quantified formulas cannot handle injectivity. So, we are limiting the number of iterations to avoid a long "wait". */ - Z3_set_param_value(cfg, "MBQI_MAX_ITERATIONS", "10"); + Z3_global_param_set("smt.mbqi.max_iterations", "10"); ctx = mk_context_custom(cfg, error_handler); Z3_del_config(cfg); @@ -1087,8 +1087,9 @@ void quantifier_example1() if (Z3_get_search_failure(ctx) != Z3_QUANTIFIERS) { exitf("unexpected result"); } - Z3_del_context(ctx); + /* reset global parameters set by this function */ + Z3_global_param_reset_all(); } /** @@ -1646,7 +1647,7 @@ void parser_example3() cfg = Z3_mk_config(); /* See quantifer_example1 */ - Z3_set_param_value(cfg, "MODEL", "true"); + Z3_set_param_value(cfg, "model", "true"); ctx = mk_context_custom(cfg, error_handler); Z3_del_config(cfg); @@ -2249,57 +2250,6 @@ void unsat_core_and_proof_example() { Z3_del_context(ctx); } -/** - \brief Extract classes of implied equalities. - - This example illustrates the use of #Z3_get_implied_equalities. -*/ -void get_implied_equalities_example() { - Z3_config cfg = Z3_mk_config(); - Z3_context ctx; - - printf("\nget_implied_equalities example\n"); - LOG_MSG("get_implied_equalities example"); - - Z3_set_param_value(cfg, "ARITH_PROCESS_ALL_EQS", "true"); - Z3_set_param_value(cfg, "ARITH_EQ_BOUNDS", "true"); - ctx = Z3_mk_context(cfg); - Z3_del_config(cfg); - { - Z3_sort int_ty = Z3_mk_int_sort(ctx); - Z3_ast a = mk_int_var(ctx,"a"); - Z3_ast b = mk_int_var(ctx,"b"); - Z3_ast c = mk_int_var(ctx,"c"); - Z3_ast d = mk_int_var(ctx,"d"); - Z3_func_decl f = Z3_mk_func_decl(ctx, Z3_mk_string_symbol(ctx,"f"), 1, &int_ty, int_ty); - Z3_ast fa = Z3_mk_app(ctx, f, 1, &a); - Z3_ast fb = Z3_mk_app(ctx, f, 1, &b); - Z3_ast fc = Z3_mk_app(ctx, f, 1, &c); - unsigned const num_terms = 7; - unsigned i; - Z3_ast terms[7] = { a, b, c, d, fa, fb, fc }; - unsigned class_ids[7] = { 0, 0, 0, 0, 0, 0, 0 }; - - Z3_assert_cnstr(ctx, Z3_mk_eq(ctx, a, b)); - Z3_assert_cnstr(ctx, Z3_mk_eq(ctx, b, c)); - Z3_assert_cnstr(ctx, Z3_mk_le(ctx, fc, b)); - Z3_assert_cnstr(ctx, Z3_mk_le(ctx, b, fa)); - - Z3_get_implied_equalities(ctx, num_terms, terms, class_ids); - for (i = 0; i < num_terms; ++i) { - printf("Class %s |-> %d\n", Z3_ast_to_string(ctx, terms[i]), class_ids[i]); - } - printf("asserting f(a) <= b\n"); - Z3_assert_cnstr(ctx, Z3_mk_le(ctx, fa, b)); - Z3_get_implied_equalities(ctx, num_terms, terms, class_ids); - for (i = 0; i < num_terms; ++i) { - printf("Class %s |-> %d\n", Z3_ast_to_string(ctx, terms[i]), class_ids[i]); - } - } - /* delete logical context */ - Z3_del_context(ctx); -} - #define MAX_RETRACTABLE_ASSERTIONS 1024 /** @@ -2504,7 +2454,7 @@ void reference_counter_example() { LOG_MSG("reference_counter_example"); cfg = Z3_mk_config(); - Z3_set_param_value(cfg, "MODEL", "true"); + Z3_set_param_value(cfg, "model", "true"); // Create a Z3 context where the user is reponsible for managing // Z3_ast reference counters. ctx = Z3_mk_context_rc(cfg); @@ -2685,7 +2635,6 @@ int main() { binary_tree_example(); enum_example(); unsat_core_and_proof_example(); - get_implied_equalities_example(); incremental_example1(); reference_counter_example(); smt2parser_example(); diff --git a/src/api/api_config_params.cpp b/src/api/api_config_params.cpp index 908900043..aaaabb7b2 100644 --- a/src/api/api_config_params.cpp +++ b/src/api/api_config_params.cpp @@ -43,6 +43,13 @@ extern "C" { } } + void Z3_API Z3_global_param_reset_all() { + memory::initialize(UINT_MAX); + LOG_Z3_global_param_reset_all(); + gparams::reset(); + env_params::updt_params(); + } + std::string g_Z3_global_param_get_buffer; Z3_bool_opt Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value) { diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index bdb462df0..fca009cea 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -67,6 +67,7 @@ namespace z3 { inline void set_param(char const * param, char const * value) { Z3_global_param_set(param, value); } inline void set_param(char const * param, bool value) { Z3_global_param_set(param, value ? "true" : "false"); } inline void set_param(char const * param, int value) { std::ostringstream oss; oss << value; Z3_global_param_set(param, oss.str().c_str()); } + inline void reset_params() { Z3_global_param_reset_all(); } /** \brief Exception used to sign API usage errors. diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 301267ce1..033626747 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -219,6 +219,11 @@ def set_param(*args, **kws): Z3_global_param_set(str(prev), _to_param_value(a)) prev = None +def reset_params(): + """Reset all global (or module) parameters. + """ + Z3_global_param_reset_all() + def set_option(*args, **kws): """Alias for 'set_param' for backward compatibility. """ diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 5ef92b931..49d59e125 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1260,6 +1260,17 @@ extern "C" { def_API('Z3_global_param_set', VOID, (_in(STRING), _in(STRING))) */ void Z3_API Z3_global_param_set(__in Z3_string param_id, __in Z3_string param_value); + + + /** + \brief Restore the value of all global (and module) parameters. + This command will not affect already created objects (such as tactics and solvers). + + \sa Z3_global_param_set + + def_API('Z3_global_param_reset_all', VOID, ()) + */ + void Z3_API Z3_global_param_reset_all(); /** \brief Get a global (or module) parameter. diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index 183678c59..976393e46 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -60,20 +60,22 @@ public: } ~imp() { - { - dictionary::iterator it = m_module_param_descrs.begin(); - dictionary::iterator end = m_module_param_descrs.end(); - for (; it != end; ++it) { - dealloc(it->m_value); - } + reset(); + dictionary::iterator it = m_module_param_descrs.begin(); + dictionary::iterator end = m_module_param_descrs.end(); + for (; it != end; ++it) { + dealloc(it->m_value); } - { - dictionary::iterator it = m_module_params.begin(); - dictionary::iterator end = m_module_params.end(); - for (; it != end; ++it) { - dealloc(it->m_value); - } + } + + void reset() { + m_params.reset(); + dictionary::iterator it = m_module_params.begin(); + dictionary::iterator end = m_module_params.end(); + for (; it != end; ++it) { + dealloc(it->m_value); } + m_module_params.reset(); } // ----------------------------------------------- @@ -448,6 +450,11 @@ public: gparams::imp * gparams::g_imp = 0; +void gparams::reset() { + SASSERT(g_imp != 0); + g_imp->reset(); +} + void gparams::set(char const * name, char const * value) { TRACE("gparams", tout << "setting [" << name << "] <- '" << value << "'\n";); SASSERT(g_imp != 0); diff --git a/src/util/gparams.h b/src/util/gparams.h index a41044c84..a55761830 100644 --- a/src/util/gparams.h +++ b/src/util/gparams.h @@ -27,6 +27,11 @@ class gparams { public: typedef default_exception exception; + /** + \brief Reset all global and module parameters. + */ + static void reset(); + /** \brief Set a global parameter \c name with \c value.