context params

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

src/cmd_context/basic_cmds.cpp

@@ -29,6 +29,7 @@ Notes:
 #include"eval_cmd.h"
 #include"gparams.h"
 #include"model_params.hpp"
+#include"env_params.h"
 
 class help_cmd : public cmd {
     svector<symbol> m_cmds;
@@ -305,6 +306,8 @@ class set_option_cmd : public set_get_option_cmd {
     void set_param(cmd_context & ctx, char const * value) {
         try {
             gparams::set(m_option, value);
+            env_params::updt_params();
+            ctx.params().updt_params();
         }
         catch (gparams::exception ex) {
             throw cmd_exception(ex.msg());

src/cmd_context/cmd_context.cpp

@@ -359,48 +359,43 @@ cmd_context::~cmd_context() {
 }
 
 void cmd_context::set_produce_models(bool f) {
-    // PARAM-TODO 
-    // params().m_model = f;
     if (m_solver)
         m_solver->set_produce_models(f);
+    m_params.m_model = f;
 }
 
 void cmd_context::set_produce_unsat_cores(bool f) {
     // can only be set before initialization
     SASSERT(!has_manager());
-    m_produce_unsat_cores = f;
+    m_params.m_unsat_core = f;
 }
 
 void cmd_context::set_produce_proofs(bool f) {
-    // PARAM-TODO
     // can only be set before initialization
     SASSERT(!has_manager());
-    // params().m_proof_mode = f ? PGM_FINE : PGM_DISABLED;
+    m_params.m_proof = f;
 }
 
 bool cmd_context::produce_models() const { 
-    // PARAM-TODO
-    // return params().m_model; 
-    return true;
+    return m_params.m_model;
 }
 
 bool cmd_context::produce_proofs() const { 
-    // PARAM-TODO
-    // return params().m_proof_mode != PGM_DISABLED; 
-    return false;
+    return m_params.m_proof;
+}
+
+bool cmd_context::produce_unsat_cores() const { 
+    return m_params.m_unsat_core;
 }
 
 bool cmd_context::well_sorted_check_enabled() const {
-    // PARAM-TODO
-    return true;
+    return m_params.m_well_sorted_check;
 }
 
 bool cmd_context::validate_model_enabled() const {
-    // PARAM-TODO
-    return false;
+    return m_params.m_validate_model;
 }
 
-
 cmd_context::check_sat_state cmd_context::cs_state() const {
     if (m_check_sat_result.get() == 0)
         return css_clear;
@@ -593,10 +588,7 @@ void cmd_context::init_manager_core(bool new_manager) {
         insert(pm().mk_plist_decl());
     }
     if (m_solver) {
-        m_solver->set_produce_unsat_cores(produce_unsat_cores());
-        m_solver->set_produce_models(produce_models());
-        m_solver->set_produce_proofs(produce_proofs());
-        m_solver->init(m(), m_logic);
+        init_solver_options(m_solver.get());
     }
     m_check_logic.set_logic(m(), m_logic);
 }
@@ -1455,14 +1447,23 @@ 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());
+    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) {
     m_check_sat_result = 0;
     m_solver = s;
     if (has_manager() && s != 0) {
-        m_solver->set_produce_unsat_cores(produce_unsat_cores());
-        m_solver->set_produce_models(produce_models());
-        m_solver->set_produce_proofs(produce_proofs());
-        m_solver->init(m(), m_logic);
+        init_solver_options(s);
         // assert formulas and create scopes in the new solver.
         unsigned lim = 0;
         svector<scope>::iterator it  = m_scopes.begin();

src/cmd_context/cmd_context.h

@@ -36,6 +36,7 @@ Notes:
 #include"check_logic.h"
 #include"progress_callback.h"
 #include"scoped_ptr_vector.h"
+#include"context_params.h"
 
 /**
    \brief Auxiliary function for converting SMT2 keywords into Z3 internal parameter names.
@@ -135,6 +136,7 @@ public:
     };
 
 protected:
+    context_params               m_params;
     bool                         m_main_ctx;
     symbol                       m_logic;
     bool                         m_interactive_mode;
@@ -246,9 +248,12 @@ protected:
     void print_unsupported_msg() { regular_stream() << "unsupported" << std::endl; }
     void print_unsupported_info(symbol const& s) { if (s != symbol::null) diagnostic_stream() << "; " << s << std::endl;}
 
+    void init_solver_options(solver * s);
+
 public:
     cmd_context(bool main_ctx = true, ast_manager * m = 0, symbol const & l = symbol::null);
     ~cmd_context(); 
+    context_params  & params() { return m_params; }
     void set_logic(symbol const & s);
     bool has_logic() const { return m_logic != symbol::null; }
     symbol const & get_logic() const { return m_logic; }
@@ -270,7 +275,7 @@ public:
     void set_random_seed(unsigned s) { m_random_seed = s; }
     bool produce_models() const;
     bool produce_proofs() const;
-    bool produce_unsat_cores() const { return m_produce_unsat_cores; }
+    bool produce_unsat_cores() const;
     bool well_sorted_check_enabled() const;
     bool validate_model_enabled() const;
     void set_produce_models(bool flag);

src/cmd_context/context_params.cpp

@@ -0,0 +1,114 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    context_params.cpp
+
+Abstract:
+
+    Goodies for managing context parameters in the cmd_context and
+    api_context
+
+Author:
+
+    Leonardo (leonardo) 2012-12-01
+
+Notes:
+
+--*/
+#include"context_params.h"
+#include"gparams.h"
+#include"params.h"
+
+context_params::context_params() {
+    updt_params();
+}
+
+void context_params::set_bool(bool & opt, char const * param, char const * value) {
+    if (strcmp(value, "true") == 0) {
+        opt = true;
+    }
+    else if (strcmp(value, "false") == 0) {
+        opt = false;
+    }
+    else {
+        throw default_exception("invalid value '%s' for Boolean parameter '%s'", value, param);
+    }
+}
+
+void context_params::set(char const * param, char const * value) {
+    std::string p = param;
+    unsigned n = p.size();
+    for (unsigned i = 0; i < n; i++) {
+        if (p[i] >= 'A' && p[i] <= 'Z')
+            p[i] = p[i] - 'A' + 'a';
+        else if (p[i] == '-')
+            p[i] = '_';
+    }
+    if (p == "timeout") {
+        long val = strtol(value, 0, 10);
+        m_timeout = static_cast<unsigned>(val);
+    }
+    else if (p == "type_check" || p == "well_sorted_check") {
+        set_bool(m_well_sorted_check, param, value);
+    }
+    else if (p == "auto_config") {
+        set_bool(m_auto_config, param, value);
+    }
+    else if (p == "proof") {
+        set_bool(m_proof, param, value);
+    }
+    else if (p == "model") {
+        set_bool(m_model, param, value);
+    }
+    else if (p == "validate_model") {
+        set_bool(m_validate_model, param, value);
+    }
+    else if (p == "trace") {
+        set_bool(m_trace, param, value);
+    }
+    else if (p == "trace_file_name") {
+        m_trace_file_name = value;
+    }
+    else if (p == "unsat_core") {
+        set_bool(m_unsat_core, param, value);
+    }
+    else if (p == "debug_ref_count") {
+        set_bool(m_debug_ref_count, param, value);
+    }
+    else {
+        throw default_exception("unknown parameter '%s'", p.c_str());
+    }
+}
+
+void context_params::updt_params() {
+    updt_params(gparams::get());
+}
+
+void context_params::updt_params(params_ref const & p) {
+    m_timeout           = p.get_uint("timeout", UINT_MAX);
+    m_well_sorted_check = p.get_bool("type_check", p.get_bool("well_sorted_check", true));
+    m_auto_config       = p.get_bool("auto_config", true);
+    m_proof             = p.get_bool("proof", false);
+    m_model             = p.get_bool("model", true);
+    m_validate_model    = p.get_bool("validate_model", false);
+    m_trace             = p.get_bool("trace", false);
+    m_trace_file_name   = p.get_str("trace_file_name", "z3.log");
+    m_unsat_core        = p.get_bool("unsat_core", false);
+    m_debug_ref_count   = p.get_bool("debug_ref_count", false);
+}
+
+void context_params::collect_param_descrs(param_descrs & d) {
+    d.insert("timeout", CPK_UINT, "default timeout (in milliseconds) used for solvers", "4294967295");
+    d.insert("well_sorted_check", CPK_BOOL, "type checker", "true");
+    d.insert("type_check", CPK_BOOL, "type checker (alias for well_sorted_check)", "true");
+    d.insert("auto_config", CPK_BOOL, "use heuristics to automatically select solver and configure it", "true");
+    d.insert("proof", CPK_BOOL, "proof generation, it must be enabled when the Z3 context is created", "false");
+    d.insert("model", CPK_BOOL, "model generation for solvers, this parameter can be overwritten when creating a solver", "true");
+    d.insert("validate_model", CPK_BOOL, "validate models produced by solvers", "false");
+    d.insert("trace", CPK_BOOL, "trace generation for VCC", "false");
+    d.insert("trace_file_name", CPK_STRING, "trace out file name (see option 'trace')", "z3.log");
+    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");
+}

src/cmd_context/context_params.h

@@ -0,0 +1,52 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    context_params.h
+
+Abstract:
+
+    Goodies for managing context parameters in the cmd_context and
+    api_context
+
+Author:
+
+    Leonardo (leonardo) 2012-12-01
+
+Notes:
+
+--*/
+#ifndef _CONTEXT_PARAMS_H_
+#define _CONTEXT_PARAMS_H_
+
+#include"params.h"
+
+class context_params {
+    void set_bool(bool & opt, char const * param, char const * value);
+        
+public:
+    bool        m_auto_config;
+    bool        m_proof;
+    bool        m_debug_ref_count;
+    bool        m_trace;
+    std::string m_trace_file_name;
+    bool        m_well_sorted_check;
+    bool        m_model;
+    bool        m_validate_model;
+    bool        m_unsat_core;
+    unsigned    m_timeout;
+    bool        m_statistics;
+
+    context_params();
+    void set(char const * param, char const * value);
+    void updt_params();
+    void updt_params(params_ref const & p);
+    static void collect_param_descrs(param_descrs & d);
+    /*
+      REG_PARAMS('context_params::collect_param_descrs')
+    */
+};
+
+
+#endif

src/front_end_params/front_end_params.cpp

@@ -32,10 +32,6 @@ void front_end_params::register_params(ini_params & p) {
     p.register_bool_param("well_sorted_check", m_well_sorted_check, "enable/disable type checker");
     p.register_unsigned_param("soft_timeout", m_soft_timeout, "set approximate timeout for each solver query (milliseconds), the value 0 represents no timeout", true);
     p.register_double_param("instruction_max", m_instr_out, "set the (approximate) maximal number of instructions per invocation of check", true);
-    p.register_bool_param("auto_config", m_auto_config, "use heuristics to set Z3 configuration parameters, it is only available for the SMT-LIB input format");
-    p.register_int_param("proof_mode", 0, 2, reinterpret_cast<int&>(m_proof_mode), "select proof generation mode: 0 - disabled, 1 - coarse grain, 2 - fine grain");
-    p.register_bool_param("trace", m_trace, "enable tracing for the Axiom Profiler tool");
-    p.register_string_param("trace_file_name", m_trace_file_name, "tracing file name");
 
 #ifdef _WINDOWS
     // The non-windows memory manager does not have access to memory sizes.
@@ -47,7 +43,6 @@ void front_end_params::register_params(ini_params & p) {
 
 
     PRIVATE_PARAMS({
-        p.register_bool_param("debug_ref_count", m_debug_ref_count);
     });
 
 }

src/shell/datalog_frontend.h

@@ -23,7 +23,6 @@ struct datalog_params {
     symbol m_default_table;
     bool   m_default_table_checked;
     datalog_params();
-    // virtual void register_params(ini_params& p);        
 };
 
 unsigned read_datalog(char const * file, datalog_params const& dl_params, front_end_params & front_end_params);

src/shell/main.cpp

@@ -116,10 +116,7 @@ void init_params() {
     if (!g_params_initialized) {
         z3_bound_num_procs();
         g_front_end_params = new front_end_params();
-        // g_params = new ini_params();
         g_extra_params = new extra_params();
-        // g_front_end_params->register_params(*g_params);
-        // g_extra_params->register_params(*g_params);
         g_params_initialized = true;
     }
 }

src/solver/strategic_solver.cpp

@@ -99,8 +99,6 @@ void strategic_solver::updt_params(params_ref const & p) {
         m_inc_solver->updt_params(p);
     m_params = p;
     m_auto_config = p.get_bool("auto_config", true);
-    // PARAM-TODO
-    // PROOFS, MODELS, UNSATCORES
 }
 
 void strategic_solver::collect_param_descrs(param_descrs & r) {

src/util/env_params.cpp

@@ -24,7 +24,7 @@ Notes:
 
 void env_params::updt_params() {
     params_ref p = gparams::get();
-    set_verbosity_level(p.get_uint("verbose", 0));
+    set_verbosity_level(p.get_uint("verbose", get_verbosity_level()));
     enable_warning_messages(p.get_bool("warning", true));
     memory::set_max_size(p.get_uint("memory_max_size", 0));
 }

src/util/gparams.cpp

@@ -86,7 +86,9 @@ public:
     void display(std::ostream & out, unsigned indent, bool smt2_style) {
         #pragma omp critical (gparams)
         {
-            m_param_descrs.display(out, indent, smt2_style);
+            out << "Global parameters\n";
+            m_param_descrs.display(out, indent + 4, smt2_style);
+            out << "\n";
             dictionary<param_descrs*>::iterator it  = m_module_param_descrs.begin();
             dictionary<param_descrs*>::iterator end = m_module_param_descrs.end();
             for (; it != end; ++it) {