From 92a29b1e43c97bbefe092dc116ca8c8568ab7241 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 4 Dec 2012 11:55:12 -0800
Subject: [PATCH] added Z3_global_param_reset_all API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
examples/c/test_capi.c | 67 +++++------------------------------
src/api/api_config_params.cpp | 7 ++++
src/api/c++/z3++.h | 1 +
src/api/python/z3.py | 5 +++
src/api/z3_api.h | 11 ++++++
src/util/gparams.cpp | 31 +++++++++-------
src/util/gparams.h | 5 +++
7 files changed, 56 insertions(+), 71 deletions(-)
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<param_descrs*>::iterator it = m_module_param_descrs.begin();
- dictionary<param_descrs*>::iterator end = m_module_param_descrs.end();
- for (; it != end; ++it) {
- dealloc(it->m_value);
- }
+ reset();
+ dictionary<param_descrs*>::iterator it = m_module_param_descrs.begin();
+ dictionary<param_descrs*>::iterator end = m_module_param_descrs.end();
+ for (; it != end; ++it) {
+ dealloc(it->m_value);
}
- {
- dictionary<params_ref*>::iterator it = m_module_params.begin();
- dictionary<params_ref*>::iterator end = m_module_params.end();
- for (; it != end; ++it) {
- dealloc(it->m_value);
- }
+ }
+
+ void reset() {
+ m_params.reset();
+ dictionary<params_ref*>::iterator it = m_module_params.begin();
+ dictionary<params_ref*>::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.