add documentation methods to param_descrs, add C++ API and example for param_descrs. Issue #443

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

examples/c++/example.cpp

@@ -1095,6 +1095,22 @@ void sudoku_example() {
     }
 }
 
+void param_descrs_example() {
+    std::cout << "parameter description example\n";
+    context c;
+    param_descrs p = param_descrs::simplify_param_descrs(c);
+    std::cout << p << "\n";
+    unsigned sz = p.size();
+    for (unsigned i = 0; i < sz; ++i) {
+        symbol nm = p.name(i);
+        char const* kind = "other";
+        Z3_param_kind k = p.kind(nm);
+        if (k == Z3_PK_UINT) kind = "uint";
+        if (k == Z3_PK_BOOL) kind = "bool";
+        std::cout << nm << ": " << p.documentation(nm) << " kind: " << kind << "\n";
+    }
+}
+
 int main() {
 
     try {
@@ -1136,6 +1152,7 @@ int main() {
         substitute_example(); std::cout << "\n";
         opt_example(); std::cout << "\n";
         extract_example(); std::cout << "\n";
+        param_descrs_example(); std::cout << "\n";
         sudoku_example(); std::cout << "\n";
         std::cout << "done\n";
     }

src/api/api_params.cpp

@@ -179,6 +179,19 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    Z3_string Z3_API Z3_param_descrs_get_documentation(Z3_context c, Z3_param_descrs p, Z3_symbol s) {
+        Z3_TRY;
+        LOG_Z3_param_descrs_get_documentation(c, p, s);
+        RESET_ERROR_CODE();
+        char const* result = to_param_descrs_ptr(p)->get_descr(to_symbol(s));
+        if (result == 0) {
+            SET_ERROR_CODE(Z3_IOB);
+            RETURN_Z3(0);
+        }
+        return mk_c(c)->mk_external_string(result);
+        Z3_CATCH_RETURN(0);
+    }
+
     Z3_string Z3_API Z3_param_descrs_to_string(Z3_context c, Z3_param_descrs p) {
         Z3_TRY;
         LOG_Z3_param_descrs_to_string(c, p);

src/api/c++/z3++.h

@@ -49,6 +49,7 @@ namespace z3 {
     class context;
     class symbol;
     class params;
+    class param_descrs;
     class ast;
     class sort;
     class func_decl;
@@ -286,6 +287,9 @@ namespace z3 {
 
     };
 
+
+
+
     template<typename T>
     class array {
         T *      m_array;
@@ -338,6 +342,30 @@ namespace z3 {
     }
 
 
+    class param_descrs : public object {
+        Z3_param_descrs m_descrs;
+    public:
+        param_descrs(context& c, Z3_param_descrs d): object(c), m_descrs(d) { Z3_param_descrs_inc_ref(c, d); }
+        param_descrs(param_descrs const& o): object(o.ctx()), m_descrs(o.m_descrs) { Z3_param_descrs_inc_ref(ctx(), m_descrs); }
+        param_descrs& operator=(param_descrs const& o) {
+            Z3_param_descrs_inc_ref(o.ctx(), o.m_descrs);
+            Z3_param_descrs_dec_ref(ctx(), m_descrs);
+            m_descrs = o.m_descrs;
+            m_ctx = o.m_ctx;
+            return *this;
+        }
+        ~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)); }
+
+        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)); }
+        Z3_param_kind kind(symbol const& s) { return Z3_param_descrs_get_kind(ctx(), m_descrs, s); }
+        std::string documentation(symbol const& s) { char const* r = Z3_param_descrs_get_documentation(ctx(), m_descrs, s); check_error(); return r; }
+        std::string to_string() const { return Z3_param_descrs_to_string(ctx(), m_descrs); }
+    };
+
+    inline std::ostream& operator<<(std::ostream & out, param_descrs const & d) { return out << d.to_string(); }
+
     class params : public object {
         Z3_params m_params;
     public:
@@ -1572,6 +1600,8 @@ namespace z3 {
                                    fmls,
                                    fml));
         }
+        param_descrs get_param_descrs() { return param_descrs(ctx(), Z3_solver_get_param_descrs(ctx(), m_solver)); }
+
     };
     inline std::ostream & operator<<(std::ostream & out, solver const & s) { out << Z3_solver_to_string(s.ctx(), s); return out; }
 
@@ -1686,6 +1716,7 @@ namespace z3 {
         friend tactic repeat(tactic const & t, unsigned max);
         friend tactic with(tactic const & t, params const & p);
         friend tactic try_for(tactic const & t, unsigned ms);
+        param_descrs get_param_descrs() { return param_descrs(ctx(), Z3_tactic_get_param_descrs(ctx(), m_tactic)); }
     };
 
     inline tactic operator&(tactic const & t1, tactic const & t2) {

src/api/dotnet/ParamDescrs.cs

@@ -46,6 +46,15 @@ namespace Microsoft.Z3
             return (Z3_param_kind)Native.Z3_param_descrs_get_kind(Context.nCtx, NativeObject, name.NativeObject);
         }
 
+        /// <summary>
+        /// Retrieve documentation of parameter.
+        /// </summary>
+        public string GetDocumentation(Symbol name)
+        {
+            Contract.Requires(name != null);
+            return Native.Z3_param_descrs_get_documentation(Context.nCtx, NativeObject, name.NativeObject);
+        }
+
         /// <summary>
         /// Retrieve all names of parameters.
         /// </summary>

src/api/java/ParamDescrs.java

@@ -44,6 +44,15 @@ public class ParamDescrs extends Z3Object
                 getContext().nCtx(), getNativeObject(), name.getNativeObject()));
     }
 
+    /**
+     * Retrieve documentation of parameter.
+     **/
+
+     public String getDocumentation(Symbol name)
+     {
+	 return Native.paramDescrsGetDocumentation(getContext().nCtx(), getNativeObject(), name.getNativeObject());
+     }
+
     /**
      * Retrieve all names of parameters.
      * 

src/api/python/z3.py

@@ -4649,6 +4649,11 @@ class ParamDescrsRef:
         """
         return Z3_param_descrs_get_kind(self.ctx.ref(), self.descr, to_symbol(n, self.ctx))
 
+    def get_documentation(self, n):
+        """Return the documentation string of the parameter named `n`.
+        """
+        return Z3_param_descrs_get_documentation(self.ctx.ref(), self.descr, to_symbol(n, self.ctx))
+
     def __getitem__(self, arg):
         if _is_int(arg):
             return self.get_name(arg)

src/api/z3_api.h

@@ -1666,6 +1666,13 @@ extern "C" {
     */
     Z3_symbol Z3_API Z3_param_descrs_get_name(Z3_context c, Z3_param_descrs p, unsigned i);
 
+    /**
+       \brief Retrieve documentation string corresponding to parameter name \c s.
+
+       def_API('Z3_param_descrs_get_documentation', STRING, (_in(CONTEXT), _in(PARAM_DESCRS), _in(SYMBOL)))
+     */
+    Z3_string Z3_API Z3_param_descrs_get_documentation(Z3_context c, Z3_param_descrs p, Z3_symbol s);
+
     /**
        \brief Convert a parameter description set into a string. This function is mainly used for printing the
        contents of a parameter description set.