#7468 - add option (get-info :parameters) to display solver parameters that were updated globally and distinct from defaults

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

src/cmd_context/basic_cmds.cpp

@@ -433,7 +433,7 @@ class set_option_cmd : public set_get_option_cmd {
     }
 
     void set_param(cmd_context & ctx, char const * value) {
-        try {
+        try {            
             gparams::set(m_option, value);
             env_params::updt_params();
             ctx.global_params_updated();
@@ -693,7 +693,7 @@ public:
         m_rlimit(":rlimit") {
     }
     char const * get_usage() const override { return "<keyword>"; }
-    char const * get_descr(cmd_context & ctx) const override { return "get information."; }
+    char const * get_descr(cmd_context & ctx) const override { return "(get-info :?) for options."; }
     unsigned get_arity() const override { return 1; }
     cmd_arg_kind next_arg_kind(cmd_context & ctx) const override { return CPK_KEYWORD; }
     void set_next_arg(cmd_context & ctx, symbol const & opt) override {
@@ -707,7 +707,7 @@ public:
             ctx.regular_stream() << "(:name \"Z3\")" << std::endl;
         }
         else if (opt == m_authors) {
-            ctx.regular_stream() << "(:authors \"Leonardo de Moura, Nikolaj Bjorner and Christoph Wintersteiger\")" << std::endl;
+            ctx.regular_stream() << "(:authors \"Leonardo de Moura, Nikolaj Bjorner, Lev Nachmanson and Christoph Wintersteiger\")" << std::endl;
         }
         else if (opt == m_version) {
             ctx.regular_stream() << "(:version \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER
@@ -731,8 +731,20 @@ public:
         else if (opt == m_assertion_stack_levels) {
             ctx.regular_stream() << "(:assertion-stack-levels " << ctx.num_scopes() << ")" << std::endl;
         }
+        else if (opt == symbol(":parameters")) {
+            ctx.display_parameters(ctx.regular_stream());
+        }
         else {
-            ctx.print_unsupported(opt, m_line, m_pos);
+            if (opt != symbol(":?"))
+               ctx.print_unsupported(opt, m_line, m_pos);
+            ctx.regular_stream() << "; (get-info :reason-unknown)\n";
+            ctx.regular_stream() << "; (get-info :status)\n";
+            ctx.regular_stream() << "; (get-info :version)\n";
+            ctx.regular_stream() << "; (get-info :authors)\n";
+            ctx.regular_stream() << "; (get-info :error-behavior)\n";
+            ctx.regular_stream() << "; (get-info :parameters)\n";
+            ctx.regular_stream() << "; (get-info :rlimit)\n";
+            ctx.regular_stream() << "; (get-info :assertion-stack-levels)\n";
         }
     }
 };

src/cmd_context/cmd_context.cpp

@@ -1902,6 +1902,11 @@ void cmd_context::display_model(model_ref& mdl) {
     }
 }
 
+void cmd_context::display_parameters(std::ostream& out) {
+    if (m_solver)
+        m_solver->display_parameters(out);
+}
+
 void cmd_context::add_declared_functions(model& mdl) {
     model_params p;
     if (!p.user_functions())

src/cmd_context/cmd_context.h

@@ -506,6 +506,7 @@ public:
     void display_assertions();
     void display_statistics(bool show_total_time = false, double total_time = 0.0);
     void display_dimacs();
+    void display_parameters(std::ostream& out);
     void reset(bool finalize = false);
     void assert_expr(expr * t);
     void assert_expr(symbol const & name, expr * t);

src/solver/solver.cpp

@@ -225,6 +225,18 @@ void solver::collect_param_descrs(param_descrs & r) {
     insert_ctrl_c(r);
 }
 
+std::ostream& solver::display_parameters(std::ostream& out) {
+    //
+    // this is a partial patch. 
+    // The modules should be present in 'p'.
+    // if p has smt parameters that are updated, they may be visible.
+    // parameters within sub-solvers will / may not be visible at this level.
+    //
+    auto const& p = get_params();
+    gparams::display_updated_parameters(out, p);
+    return out;
+}
+
 void solver::reset_params(params_ref const & p) {
     m_params.append(p);
     solver_params sp(m_params);

src/solver/solver.h

@@ -81,6 +81,11 @@ public:
     */
     virtual void collect_param_descrs(param_descrs & r);
 
+    /**
+    * \brief display parameters
+    */
+    std::ostream& display_parameters(std::ostream& out);
+
     /**
        \brief Push a parameter state. It is restored upon pop.
        Only a single scope of push is supported.

src/util/gparams.cpp

@@ -412,7 +412,7 @@ public:
         }
     }
 
-    std::string get_value(params_ref const & ps, std::string const & p) {
+    std::string get_value(params_ref const& ps, std::string const& p) {
         symbol sp(p.c_str());
         std::ostringstream buffer;
         ps.display(buffer, sp);
@@ -430,6 +430,19 @@ public:
         return r;
     }
 
+    void display_updated_parameters(std::ostream& out, params_ref const& p) {
+        param_descrs* d = nullptr;
+        for (auto const& [k, v] : m_module_params) {
+            if (!get_module_param_descr(k, d))
+                continue;
+            params_ref* ps = nullptr;
+            if (!m_module_params.find(k, ps))
+                continue;
+            ps->display_smt2(out, k, *d);
+            p.display_smt2(out, k, *d);
+        }
+    }
+
     std::string get_value(char const * name) {
         std::string m, p;
         normalize(name, m, p);
@@ -691,3 +704,7 @@ std::string& gparams::g_buffer() {
     SASSERT(g_imp);
     return g_imp->m_buffer;
 }
+
+void gparams::display_updated_parameters(std::ostream& out, params_ref const& p) {
+    g_imp->display_updated_parameters(out, p);
+}

src/util/gparams.h

@@ -118,9 +118,11 @@ public:
     
     // Auxiliary APIs for better command line support
     static void display_modules(std::ostream & out);
+    static void display_updated_parameters(std::ostream& out, params_ref const& p);
     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

@@ -476,7 +476,8 @@ public:
 
     void display_smt2(std::ostream & out, char const* module, param_descrs& descrs) const {
         for (params::entry const& e : m_entries) {
-            if (!descrs.contains(e.first)) continue;
+            if (!descrs.contains(e.first)) 
+                continue;
             out << "(set-option :";
             out << module << ".";        
             out << e.first;
@@ -504,6 +505,7 @@ public:
                 break;
             }
             out << ")\n";
+            out << "; " << descrs.get_descr(e.first) << "\n";
         }
     }