add parameter descriptions

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

doc/mk_api_doc.py

@@ -24,6 +24,7 @@
 Z3PY_ENABLED=True
 DOTNET_ENABLED=True
 JAVA_ENABLED=True
+Z3OPTIONS_ENABLED=True
 DOTNET_API_SEARCH_PATHS=['../src/api/dotnet']
 JAVA_API_SEARCH_PATHS=['../src/api/java']
 SCRIPT_DIR=os.path.abspath(os.path.dirname(__file__))
@@ -237,6 +238,25 @@ def doc_path(path):
     else:
         print('Javascript documentation disabled')
 
+    if Z3OPTIONS_ENABLED:
+        print("Z3 Options Enabled")
+        out = subprocess.call([Z3_EXE, "-pm"],stdout=subprocess.PIPE).communicate()[0]
+        modules = []
+        if out != None:
+            out = out.decode(sys.stdout.encoding)
+            module_re = re.compile(r"\[module\] (.*)\,")
+            lines = out.split("\n")
+            for line in lines:
+                m = module_re.search(line)
+                if m:
+                    modules += [m.group(1)]
+        for module in modules:
+            out = subprocess.call([Z3_EXE, "-pmhtml:%s" % module],stdout=subprocess.PIPE).communicate()[0]
+            if out == None:
+                continue
+            out = out.decode(sys.stdout.encoding)
+
+
     doxygen_config_file = temp_path('z3api.cfg')
     configure_file(
         doc_path('z3api.cfg.in'),

src/cmd_context/cmd_context.cpp

@@ -1054,7 +1054,7 @@ func_decl * cmd_context::find_func_decl(symbol const & s, unsigned num_indices,
     if (f) 
         return f;
     builtin_decl d;
-    if (domain && m_builtin_decls.find(s, d)) {
+    if ((arity == 0 || domain) && m_builtin_decls.find(s, d)) {
         family_id fid = d.m_fid;
         decl_kind k   = d.m_decl;
         // Hack: if d.m_next != 0, we use domain[0] (if available) to decide which plugin we use.

src/math/simplex/model_based_opt.cpp

@@ -1260,6 +1260,7 @@ namespace opt {
             vector<var> coeffs = m_rows[ri].m_vars;
             rational coeff = m_rows[ri].m_coeff;
             unsigned v = m_rows[ri].m_id;
+            rational v_value = m_var2value[v];
 
             unsigned w = UINT_MAX;
             rational offset(0);
@@ -1270,14 +1271,14 @@ namespace opt {
 
             rational w_value = w == UINT_MAX ? offset : m_var2value[w];
 
-            // add v = a*z + w - k*K = 0, for k = (a*z_value + w_value) div K
+            // add v = a*z + w - V, for k = (a*z_value + w_value) div K
             // claim: (= (mod x K) (- x (* K (div x K)))))) is a theorem for every x, K != 0
-            rational kK = div(a * z_value + w_value, K) * K;
+            rational V = v_value - a * z_value - w_value;
             vector<var> mod_coeffs;
             mod_coeffs.push_back(var(v, rational::minus_one()));
             mod_coeffs.push_back(var(z, a));
             if (w != UINT_MAX) mod_coeffs.push_back(var(w, rational::one()));
-            add_constraint(mod_coeffs, kK + offset, t_eq);
+            add_constraint(mod_coeffs, V + offset, t_eq);
             add_lower_bound(v, rational::zero());
             add_upper_bound(v, K - 1);
 

src/qe/mbp/mbp_arith.cpp

@@ -214,20 +214,6 @@ namespace mbp {
                     throw default_exception("mbp evaluation didn't produce a truth value");
                 }
             }
-            else if (a.is_mod(t, t1, t2) && is_numeral(t2, mul1) && !mul1.is_zero()) {
-                rational r;
-                val = eval(t);
-                if (!a.is_numeral(val, r))
-                    throw default_exception("mbp evaluation didn't produce an integer");
-                c += mul * r;
-
-               rational c0(-r), mul0(1);
-               obj_map<expr, rational> ts0;
-               linearize(mbo, eval, mul0, t1, c0, fmls, ts0, tids);
-               vars coeffs;
-               extract_coefficients(mbo, eval, ts0, tids, coeffs);
-               mbo.add_divides(coeffs, c0, mul1);
-            }
             else if (false && a.is_mod(t, t1, t2) && is_numeral(t2, mul1) && mul1 > 0) {
                 // v = t1 mod mul1
                 vars coeffs;
@@ -240,6 +226,20 @@ namespace mbp {
                 rational c0 = add_def(t1, mul1, coeffs);
                 tids.insert(t, mbo.add_div(coeffs, c0, mul1));
             }
+            else if (a.is_mod(t, t1, t2) && is_numeral(t2, mul1) && !mul1.is_zero()) {
+                rational r;
+                val = eval(t);
+                if (!a.is_numeral(val, r))
+                    throw default_exception("mbp evaluation didn't produce an integer");
+                c += mul * r;
+
+                rational c0(-r), mul0(1);
+                obj_map<expr, rational> ts0;
+                linearize(mbo, eval, mul0, t1, c0, fmls, ts0, tids);
+                vars coeffs;
+                extract_coefficients(mbo, eval, ts0, tids, coeffs);
+                mbo.add_divides(coeffs, c0, mul1);
+            }
             else
                 insert_mul(t, mul, ts);
         }

src/sat/smt/euf_proof.cpp

@@ -27,9 +27,20 @@ namespace euf {
         m_drat_initialized = true;
     }
 
+    void solver::drat_log_params(func_decl* f) {
+        for (unsigned i = f->get_num_parameters(); i-- > 0; ) {
+            auto const& p = f->get_parameter(i);
+            if (!p.is_ast()) 
+                continue;
+            ast* a = p.get_ast();
+            if (is_func_decl(a))
+                drat_log_decl(to_func_decl(a));
+        }
+    }
     void solver::drat_log_expr1(expr* e) {
         if (is_app(e)) {
             app* a = to_app(e);
+            drat_log_params(a->get_decl());
             drat_log_decl(a->get_decl());
             std::stringstream strm;
             strm << mk_ismt2_func(a->get_decl(), m);

src/sat/smt/euf_solver.h

@@ -176,6 +176,7 @@ namespace euf {
         void log_antecedents(literal l, literal_vector const& r);
         void log_justification(literal l, th_explain const& jst);
         void drat_log_decl(func_decl* f);
+        void drat_log_params(func_decl* f);
         void drat_log_expr1(expr* n);
         ptr_vector<expr> m_drat_todo;
         obj_hashtable<ast> m_drat_asts;

src/shell/drat_frontend.cpp

@@ -363,6 +363,21 @@ class smt_checker {
                     result = au.mk_numeral(num, true);
                     return;
                 }
+                if (name == "as-array" && sz == 3) {
+                    array_util au(m);
+                    auto const* ch2 = sexpr->get_child(2);
+                    switch (ch2->get_kind()) {
+                    case sexpr::kind_t::COMPOSITE:
+                        break;
+                    default:
+                        name = sexpr->get_child(2)->get_symbol();
+                        f = ctx.find_func_decl(name);
+                        if (f) {
+                            result = au.mk_as_array(f);
+                            return;
+                        }
+                    }
+                }
                 for (unsigned i = 2; i < sz; ++i) {
                     auto* child = sexpr->get_child(i);
                     if (child->is_numeral() && child->get_numeral().is_unsigned())
@@ -378,7 +393,6 @@ class smt_checker {
             name = sexpr->get_symbol();
             break;
         case sexpr::kind_t::BV_NUMERAL: {
-            std::cout << "bv numeral\n";
             goto bail;            
         }
         case sexpr::kind_t::STRING:

src/shell/main.cpp

@@ -95,6 +95,7 @@ void display_usage() {
     std::cout << "  -p          display Z3 global (and module) parameters.\n";
     std::cout << "  -pd         display Z3 global (and module) parameter descriptions.\n";
     std::cout << "  -pm:name    display Z3 module ('name') parameters.\n";
+    std::cout << "  -pmmd:name  display Z3 module ('name') parameters in Markdown format.\n";
     std::cout << "  -pp:name    display Z3 parameter description, if 'name' is not provided, then all module names are listed.\n";
     std::cout << "  -tactics[:name]  display built-in tactics or if argument is given, display detailed information on tactic.\n";
     std::cout << "  -probes     display avilable probes.\n";
@@ -246,6 +247,15 @@ static void parse_cmd_line_args(std::string& input_file, int argc, char ** argv)
                 gparams::display(std::cout, 0, false, true);
                 exit(0);
             }
+            else if (strcmp(opt_name, "pmmd") == 0) {
+                if (opt_arg) 
+                    gparams::display_module_markdown(std::cout, opt_arg);
+                else {
+                    gparams::display_modules(std::cout);
+                    std::cout << "\nUse -pm:name to display all parameters available at module 'name'\n";
+                }
+                exit(0);
+            }
             else if (strcmp(opt_name, "pm") == 0) {
                 if (opt_arg) {
                     gparams::display_module(std::cout, opt_arg);

src/smt/theory_arith_core.h

@@ -561,6 +561,14 @@ namespace smt {
     void theory_arith<Ext>::mk_idiv_mod_axioms(expr * dividend, expr * divisor) {
         th_rewriter & s  = ctx.get_rewriter();
         if (!m_util.is_zero(divisor)) {
+            auto mk_mul = [&](expr* a, expr* b) { 
+                if (m_util.is_mul(a)) {
+                    ptr_vector<expr> args(to_app(a)->get_num_args(), to_app(a)->get_args());
+                    args.push_back(b);
+                    return m_util.mk_mul(args.size(), args.data());
+                }
+                return m_util.mk_mul(a, b);
+            };
             // if divisor is zero, then idiv and mod are uninterpreted functions.
             expr_ref div(m), mod(m), zero(m), abs_divisor(m), one(m);
             expr_ref eqz(m), eq(m), lower(m), upper(m), qr(m), le(m), ge(m);
@@ -571,7 +579,7 @@ namespace smt {
             abs_divisor = m_util.mk_sub(m.mk_ite(m_util.mk_lt(divisor, zero), m_util.mk_sub(zero, divisor), divisor), one);
             s(abs_divisor);
             eqz         = m.mk_eq(divisor, zero);
-            qr          = m_util.mk_add(m_util.mk_mul(divisor, div), mod);
+            qr          = m_util.mk_add(mk_mul(divisor, div), mod);
             eq          = m.mk_eq(qr, dividend);
             lower       = m_util.mk_ge(mod, zero);
             upper       = m_util.mk_le(mod, abs_divisor);
@@ -590,7 +598,7 @@ namespace smt {
             mk_axiom(eqz, upper, !m_util.is_numeral(abs_divisor));
             rational k;
 
-            //m_arith_eq_adapter.mk_axioms(ensure_enode(qr), ensure_enode(dividend));
+            // m_arith_eq_adapter.mk_axioms(ensure_enode(qr), ensure_enode(dividend));
 
             if (m_util.is_zero(dividend)) {
                 mk_axiom(eqz, m.mk_eq(div, zero));

src/util/gparams.cpp

@@ -533,6 +533,22 @@ struct gparams::imp {
         out << "\n";
         d->display(out, 4, false);
     }
+    void display_module_markdown(std::ostream & out, char const* module_name) {
+        lock_guard lock(*gparams_mux);
+        param_descrs * d = nullptr;
+        if (!get_module_param_descr(module_name, d)) {
+            std::stringstream strm;
+            strm << "unknown module '" << module_name << "'";                    
+            throw exception(std::move(strm).str());
+        }
+        out << "## Module " << module_name << "\n\n";
+        char const * descr = nullptr;
+        if (get_module_descrs().find(module_name, descr)) {
+            out << "Description: " << descr;
+        }
+        out << "\n";
+        d->display_markdown(out);
+    }
 
     param_descrs const& get_global_param_descrs() {
         lock_guard lock(*gparams_mux);
@@ -643,6 +659,11 @@ void gparams::display_module(std::ostream & out, char const * module_name) {
     g_imp->display_module(out, module_name);
 }
 
+void gparams::display_module_markdown(std::ostream & out, char const * module_name) {
+    SASSERT(g_imp);
+    g_imp->display_module_markdown(out, module_name);
+}
+
 void gparams::display_parameter(std::ostream & out, char const * name) {
     SASSERT(g_imp);
     g_imp->display_parameter(out, name);

src/util/gparams.h

@@ -119,6 +119,7 @@ class gparams {
     // Auxiliary APIs for better command line support
     static void display_modules(std::ostream & out);
     static void display_module(std::ostream & out, char const * module_name);
+    static void display_module_markdown(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();
 

src/util/params.cpp

@@ -161,12 +161,16 @@ struct param_descrs::imp {
         bool operator()(symbol const & s1, symbol const & s2) const { return ::lt(s1, s2); }        
     };
 
-    void display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) const {
+    void display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr, bool markdown) const {
         svector<symbol> names;
         for (auto const& kv : m_info) {
             names.push_back(kv.m_key);
         }
         std::sort(names.begin(), names.end(), symlt());
+        if (markdown) {
+            out << " Parameter | Type | Description | Default\n";
+            out << " ----------------------------------------\n";            
+        }
         for (symbol const& name : names) {
             for (unsigned i = 0; i < indent; i++) out << " ";
             if (smt2_style)
@@ -186,10 +190,20 @@ struct param_descrs::imp {
             info d;
             m_info.find(name, d);
             SASSERT(d.m_descr);
-            out << " (" << d.m_kind << ")";
+            if (markdown) 
+                out << " | " << d.m_kind << " ";
+            else
+                out << " (" << d.m_kind << ")";
+            if (markdown)
+                out << " | ";
             if (include_descr)
                 out << " " << d.m_descr;
-            if (d.m_default != nullptr)
+            if (markdown) {
+                out << " | ";
+                if (d.m_default)
+                    out << d.m_default;
+            }
+            else if (d.m_default != nullptr)
                 out << " (default: " << d.m_default << ")";
             out << "\n";
         }
@@ -280,7 +294,11 @@ char const* param_descrs::get_module(symbol const& name) const {
 }
 
 void param_descrs::display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) const {
-    return m_imp->display(out, indent, smt2_style, include_descr);
+    return m_imp->display(out, indent, smt2_style, include_descr, false);
+}
+
+void param_descrs::display_markdown(std::ostream & out, bool smt2_style, bool include_descr) const {
+    return m_imp->display(out, 0, smt2_style, include_descr, true);
 }
 
 void insert_max_memory(param_descrs & r) {

src/util/params.h

@@ -130,6 +130,7 @@ class param_descrs {
     char const * get_default(char const * name) const;
     char const * get_default(symbol const & name) const;
     void display(std::ostream & out, unsigned indent = 0, bool smt2_style=false, bool include_descr=true) const;
+    void display_markdown(std::ostream& out, bool smt2_style = false, bool include_descr = true) const;
     unsigned size() const; 
     symbol get_param_name(unsigned idx) const;
     char const * get_module(symbol const& name) const;