chasing parameter setting bug

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/api/api_solver.cpp

@@ -36,17 +36,7 @@ extern "C" {
     static void init_solver_core(Z3_context c, Z3_solver _s) {
         ast_manager & m = mk_c(c)->m();
         Z3_solver_ref * s = to_solver(_s);
-        s->m_solver->set_produce_proofs(mk_c(c)->produce_proofs());
-        s->m_solver->set_produce_unsat_cores(s->m_params.get_bool("unsat_core", mk_c(c)->produce_unsat_cores()));
-        s->m_solver->set_produce_models(s->m_params.get_bool("model", mk_c(c)->produce_models()));
-        if (!mk_c(c)->use_auto_config()) {
-            params_ref p = s->m_params;
-            p.set_bool("auto_config", false);
-            s->m_solver->updt_params(p);
-        }
-        else {
-            s->m_solver->updt_params(s->m_params);
-        }
+        mk_c(c)->params().init_solver_params(mk_c(c)->m(), *(s->m_solver), s->m_params);
         s->m_solver->init(m, s->m_logic);
         s->m_initialized = true;
     }

src/cmd_context/cmd_context.cpp

@@ -1444,15 +1444,9 @@ void cmd_context::validate_model() {
 }
 
 void cmd_context::init_solver_options(solver * s) {
-    m_solver->set_produce_unsat_cores(produce_unsat_cores());
-    m_solver->set_produce_models(produce_models());
-    m_solver->set_produce_proofs(produce_proofs());
+    params_ref p;
+    m_params.init_solver_params(m(), *m_solver, p);
     m_solver->init(m(), m_logic);
-    if (!m_params.m_auto_config) {
-        params_ref p;
-        p.set_bool("auto_config", false);
-        m_solver->updt_params(p);
-    }
 }
 
 void cmd_context::set_solver(solver * s) {

src/cmd_context/context_params.cpp

@@ -20,6 +20,8 @@ Notes:
 #include"context_params.h"
 #include"gparams.h"
 #include"params.h"
+#include"ast.h"
+#include"solver.h"
 
 context_params::context_params() {
     updt_params();
@@ -112,3 +114,23 @@ void context_params::collect_param_descrs(param_descrs & d) {
     d.insert("unsat_core", CPK_BOOL, "unsat-core generation for solvers, this parameter can be overwritten when creating a solver, not every solver in Z3 supports unsat core generation", "false");
     d.insert("debug_ref_count", CPK_BOOL, "debug support for AST reference counting", "false");
 }
+
+params_ref context_params::merge_default_params(params_ref const & p) {
+    if (!m_auto_config && !p.contains("auto_config")) {
+        params_ref new_p = p;
+        new_p.set_bool("auto_config", false);
+        return new_p;
+    }
+    else {
+        return p;
+    }
+}
+
+void context_params::init_solver_params(ast_manager & m, solver & s, params_ref const & p) {
+    s.set_produce_proofs(m.proofs_enabled() && m_proof);
+    s.set_produce_models(p.get_bool("model", m_model));
+    s.set_produce_unsat_cores(p.get_bool("unsat_core", m_unsat_core));
+    s.updt_params(merge_default_params(p));
+}
+
+

src/cmd_context/context_params.h

@@ -21,6 +21,8 @@ Notes:
 #define _CONTEXT_PARAMS_H_
 
 #include"params.h"
+class ast_manager;
+class solver;
 
 class context_params {
     void set_bool(bool & opt, char const * param, char const * value);
@@ -45,6 +47,22 @@ public:
     /*
       REG_PARAMS('context_params::collect_param_descrs')
     */
+    
+    /**
+       \brief Goodie for updating the solver params
+       based on the configuration of the context_params object.
+
+       This method is used when creating solvers from the
+       cmd_context and API.
+    */
+    void init_solver_params(ast_manager & m, solver & s, params_ref const & p);
+
+    /**
+       \brief Include in p parameters derived from this context_params.
+       These are parameters that are meaningful for tactics and solvers.
+       Example: auto_config
+    */
+    params_ref merge_default_params(params_ref const & p);
 };
 
 

src/cmd_context/tactic_cmds.cpp

@@ -36,7 +36,7 @@ tactic_cmd::~tactic_cmd() {
     dealloc(m_factory);
 }
 
-tactic * tactic_cmd::mk(ast_manager & m) { 
+tactic * tactic_cmd::mk(ast_manager & m) {
     return (*m_factory)(m, params_ref()); 
 }
 
@@ -185,7 +185,7 @@ public:
     }
     
     virtual void execute(cmd_context & ctx) {
-        params_ref p = ps();
+        params_ref p = ctx.params().merge_default_params(ps());
         tactic_ref tref = using_params(sexpr2tactic(ctx, m_tactic), p);
         tref->set_logic(ctx.get_logic());
         ast_manager & m = ctx.m();
@@ -295,7 +295,7 @@ public:
     }
     
     virtual void execute(cmd_context & ctx) {
-        params_ref p = ps();
+        params_ref p = ctx.params().merge_default_params(ps());
         tactic_ref tref = using_params(sexpr2tactic(ctx, m_tactic), p);
         {
             tactic & t = *(tref.get());

src/tactic/tactical.cpp

@@ -1242,8 +1242,7 @@ public:
     virtual void updt_params(params_ref const & p) {
         TRACE("using_params", 
               tout << "before p: " << p << "\n";
-              tout << "m_params: " << m_params << "\n";
-              ;);
+              tout << "m_params: " << m_params << "\n";);
         
         params_ref new_p = p;
         new_p.append(m_params);