expose description of global parameters #6048

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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);

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)); }

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

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.

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);

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.