diff --git a/src/api/api_config_params.cpp b/src/api/api_config_params.cpp index 1b551bd73..cbe89e9fb 100644 --- a/src/api/api_config_params.cpp +++ b/src/api/api_config_params.cpp @@ -64,6 +64,17 @@ extern "C" { } } + Z3_param_descrs Z3_API Z3_get_global_param_descrs(Z3_context c) { + Z3_TRY; + LOG_Z3_get_global_param_descrs(c); + Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref, *mk_c(c)); + mk_c(c)->save_object(d); + d->m_descrs = gparams::get_global_param_descrs(); + auto r = of_param_descrs(d); + RETURN_Z3(r); + Z3_CATCH_RETURN(nullptr); + } + Z3_config Z3_API Z3_mk_config(void) { try { memory::initialize(UINT_MAX); diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index e817a5859..de55bb765 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -459,6 +459,7 @@ namespace z3 { } ~param_descrs() { Z3_param_descrs_dec_ref(ctx(), m_descrs); } static param_descrs simplify_param_descrs(context& c) { return param_descrs(c, Z3_simplify_get_param_descrs(c)); } + static param_descrs global_param_descrs(context& c) { return param_descrs(c, Z3_get_global_param_descrs(c)); } unsigned size() { return Z3_param_descrs_size(ctx(), m_descrs); } symbol name(unsigned i) { return symbol(ctx(), Z3_param_descrs_get_name(ctx(), m_descrs, i)); } diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index c45a3d86e..5ad8ede50 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -225,6 +225,10 @@ class Context: """ Z3_interrupt(self.ref()) + def param_descrs(self): + """Return the global parameter description set.""" + return ParamDescrsRef(Z3_get_global_param_descrs(self.ref()), self) + # Global Z3 context _main_ctx = None diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 4e5f5f5b5..b8bca8fab 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1685,6 +1685,14 @@ extern "C" { */ void Z3_API Z3_update_param_value(Z3_context c, Z3_string param_id, Z3_string param_value); + + /** + \brief Retrieve description of global parameters. + + def_API('Z3_get_global_param_descrs', PARAM_DESCRS, (_in(CONTEXT),)) + */ + Z3_param_descrs Z3_API Z3_get_global_param_descrs(Z3_context c); + /** \brief Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers, simplifiers and tactics. diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index 28ce5a867..e7c8a4d53 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -534,6 +534,11 @@ public: d->display(out, 4, false); } + param_descrs const& get_global_param_descrs() { + lock_guard lock(*gparams_mux); + return get_param_descrs(); + } + void display_parameter(std::ostream & out, char const * name) { std::string m, p; normalize(name, m, p); @@ -624,6 +629,10 @@ void gparams::display(std::ostream & out, unsigned indent, bool smt2_style, bool g_imp->display(out, indent, smt2_style, include_descr); } +param_descrs const& gparams::get_global_param_descrs() { + return g_imp->get_global_param_descrs(); +} + void gparams::display_modules(std::ostream & out) { SASSERT(g_imp); g_imp->display_modules(out); diff --git a/src/util/gparams.h b/src/util/gparams.h index 0959c20fc..0bd5e4d60 100644 --- a/src/util/gparams.h +++ b/src/util/gparams.h @@ -120,6 +120,7 @@ public: static void display_modules(std::ostream & out); static void display_module(std::ostream & out, char const * module_name); static void display_parameter(std::ostream & out, char const * name); + static param_descrs const& get_global_param_descrs(); /** \brief Initialize the global parameter management module.