added context_params to API

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

src/api/api_ast.cpp

@@ -675,7 +675,7 @@ extern "C" {
         ast_manager & m = mk_c(c)->m();
         expr * a = to_expr(_a);
         params_ref p = to_param_ref(_p);
-        unsigned timeout     = p.get_uint("timeout", UINT_MAX);
+        unsigned timeout     = p.get_uint("timeout", mk_c(c)->get_timeout());
         bool     use_ctrl_c  = p.get_bool("ctrl_c", false);
         th_rewriter m_rw(m, p);
         expr_ref    result(m);

src/api/api_config_params.cpp

@@ -17,7 +17,6 @@ Revision History:
 --*/
 #include"z3.h"
 #include"api_context.h"
-#include"api_config_params.h"
 #include"pp.h"
 #include"api_log_macros.h"
 #include"api_util.h"
@@ -25,16 +24,7 @@ Revision History:
 #include"symbol.h"
 #include"gparams.h"
 #include"env_params.h"
-
+#include"context_params.h"
-namespace api {
-
-    config_params::config_params() {
-    }
-    
-    config_params::config_params(front_end_params const & p):m_params(p) {
-    }
-
-};
 
 extern "C" {
     void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value) {
@@ -68,7 +58,7 @@ extern "C" {
             // The error handler is only available for contexts
             // Just throw a warning.
             std::ostringstream buffer;
-            buffer << "Error setting " << param_id << ", " << ex.msg();
+            buffer << "Error setting " << param_id << ": " << ex.msg();
             warning_msg(buffer.str().c_str());
             return Z3_FALSE;
         }
@@ -77,28 +67,41 @@ extern "C" {
     Z3_config Z3_API Z3_mk_config() {
         memory::initialize(UINT_MAX);
         LOG_Z3_mk_config();
-        Z3_config r = reinterpret_cast<Z3_config>(alloc(api::config_params));
+        Z3_config r = reinterpret_cast<Z3_config>(alloc(context_params));
         RETURN_Z3(r);
     }
     
     void Z3_API Z3_del_config(Z3_config c) {
         LOG_Z3_del_config(c);
-        dealloc((reinterpret_cast<api::config_params*>(c)));
+        dealloc((reinterpret_cast<context_params*>(c)));
     }
     
     void Z3_API Z3_set_param_value(Z3_config c, char const * param_id, char const * param_value) {
         LOG_Z3_set_param_value(c, param_id, param_value);
-        // PARAM-TODO save the parameter
+        try {
+            context_params * p = reinterpret_cast<context_params*>(c);
+            p->set(param_id, param_value);
+        }
+        catch (z3_exception & ex) {
+            // The error handler is only available for contexts
+            // Just throw a warning.
+            std::ostringstream buffer;
+            buffer << "Error setting " << param_id << ": " << ex.msg();
+            warning_msg(buffer.str().c_str());
+        }
     }
 
     void Z3_API Z3_update_param_value(Z3_context c, Z3_string param_id, Z3_string param_value) {
+        Z3_TRY;
         LOG_Z3_update_param_value(c, param_id, param_value);
         RESET_ERROR_CODE();
-        // NOOP in the current version
+        mk_c(c)->params().set(param_id, param_value);
+        Z3_CATCH;
     }
 
     Z3_bool Z3_API Z3_get_param_value(Z3_context c, Z3_string param_id, Z3_string* param_value) {
         LOG_Z3_get_param_value(c, param_id, param_value);
+        // TODO
         return Z3_FALSE;
     }
 

src/api/api_config_params.h

@@ -1,34 +0,0 @@
-/*++
-Copyright (c) 2012 Microsoft Corporation
-
-Module Name:
-
-    api_config_params.h
-
-Abstract:
-    Configuration parameters
-
-Author:
-
-    Leonardo de Moura (leonardo) 2012-02-29.
-
-Revision History:
-
---*/
-#ifndef _API_CONFIG_PARAMS_H_
-#define _API_CONFIG_PARAMS_H_
-
-#include"front_end_params.h"
-
-namespace api {
-
-    class config_params {
-    public:
-        front_end_params m_params;
-        config_params();
-        config_params(front_end_params const & p);
-    };
-
-};
-
-#endif

src/api/api_context.cpp

@@ -18,7 +18,6 @@ Revision History:
 
 --*/
 #include"api_context.h"
-#include"api_config_params.h"
 #include"smtparser.h"
 #include"version.h"
 #include"ast_pp.h"
@@ -54,14 +53,6 @@ namespace api {
         return static_cast<Z3_search_failure>(f);
     }
 
-    context::param_ini::param_ini(front_end_params & p) : m_params(p) {
-        p.open_trace_file();
-    }
-
-    context::param_ini::~param_ini() {
-        m_params.close_trace_file();
-    }
-        
     context::add_plugins::add_plugins(ast_manager & m) {
         reg_decl_plugins(m);
     }
@@ -88,10 +79,10 @@ namespace api {
         }
     }
 
-    context::context(config_params * p, bool user_ref_count):
+    context::context(context_params * p, bool user_ref_count):
-        m_params(p ? p->m_params : front_end_params()),
+        m_params(*p),
         m_user_ref_count(user_ref_count),
-        m_manager(m_params.m_proof_mode, m_params.m_trace_stream),
+        m_manager(m_params.m_proof ? PGM_FINE : PGM_DISABLED), // PARAM-TODO , _fparams.m_proof_mode, m_fparams.m_trace_stream),
         m_plugins(m_manager),
         m_arith_util(m_manager),
         m_bv_util(m_manager),
@@ -114,8 +105,6 @@ namespace api {
         //
         // Configuration parameter settings.
         //
-        memory::set_high_watermark(static_cast<size_t>(m_params.m_memory_high_watermark)*1024*1024);
-        memory::set_max_size(static_cast<size_t>(m_params.m_memory_max_size)*1024*1024);
         if (m_params.m_debug_ref_count) {
             m_manager.debug_ref_count();
         }
@@ -334,7 +323,8 @@ namespace api {
 
     smt::kernel & context::get_smt_kernel() {
         if (!m_solver) {
-            m_solver = alloc(smt::kernel, m_manager, m_params);
+            // PARAM-TODO: copy config_params -> fparams
+            m_solver = alloc(smt::kernel, m_manager, m_fparams);
         }
         return *m_solver;
     }
@@ -419,15 +409,15 @@ extern "C" {
     
     Z3_context Z3_API Z3_mk_context(Z3_config c) {
         LOG_Z3_mk_context(c);
-        memory::initialize(0);
+        memory::initialize(UINT_MAX);
-        Z3_context r = reinterpret_cast<Z3_context>(alloc(api::context, reinterpret_cast<api::config_params*>(c), false));
+        Z3_context r = reinterpret_cast<Z3_context>(alloc(api::context, reinterpret_cast<context_params*>(c), false));
         RETURN_Z3(r);
     }
 
     Z3_context Z3_API Z3_mk_context_rc(Z3_config c) {
         LOG_Z3_mk_context_rc(c);
-        memory::initialize(0);
+        memory::initialize(UINT_MAX);
-        Z3_context r = reinterpret_cast<Z3_context>(alloc(api::context, reinterpret_cast<api::config_params*>(c), true));
+        Z3_context r = reinterpret_cast<Z3_context>(alloc(api::context, reinterpret_cast<context_params*>(c), true));
         RETURN_Z3(r);
     }
 
@@ -573,11 +563,4 @@ ast_manager & Z3_API Z3_get_manager(__in Z3_context c) {
     return mk_c(c)->m();
 }
 
-front_end_params& Z3_API Z3_get_parameters(__in Z3_context c) {
-    return mk_c(c)->fparams();
-}
 
-Z3_context Z3_mk_context_from_params(front_end_params const& p) {
-    api::config_params cp(p);
-    return reinterpret_cast<Z3_context>(alloc(api::context, &cp));
-}

src/api/api_context.h

@@ -31,28 +31,19 @@ Revision History:
 #include"front_end_params.h"
 #include"event_handler.h"
 #include"tactic_manager.h"
+#include"context_params.h"
 
 namespace smtlib {
     class parser;
 };
 
 namespace api {
-    class config_params;
-
     Z3_search_failure mk_Z3_search_failure(smt::failure f);
        
 
     class context : public tactic_manager {
-        class param_ini {
-            front_end_params & m_params;
-        public:
-            param_ini(front_end_params & p);
-            ~param_ini();
-        };
-        
         struct add_plugins {  add_plugins(ast_manager & m); };
-        
+        context_params             m_params;
-        front_end_params           m_params;
         bool                       m_user_ref_count; //!< if true, the user is responsible for managing referenc counters.
         ast_manager                m_manager;
         add_plugins                m_plugins;
@@ -61,7 +52,10 @@ namespace api {
         bv_util                    m_bv_util;
         datalog::dl_decl_util      m_datalog_util;
 
+        // Support for old solver API
+        front_end_params           m_fparams;
         smt::kernel *              m_solver;     // General purpose solver for backward compatibility
+        // -------------------------------
 
         ast_ref_vector             m_last_result; //!< used when m_user_ref_count == true
         ast_ref_vector             m_ast_trail;   //!< used when m_user_ref_count == false
@@ -102,11 +96,16 @@ namespace api {
         //
         // ------------------------
         
-        context(config_params * p, bool user_ref_count = false);
+        context(context_params * p, bool user_ref_count = false);
         ~context();
-
-        front_end_params & fparams() { return m_params; }
         ast_manager & m() { return m_manager; }
+
+        context_params & params() { return m_params; }
+        bool produce_proofs() const { return m_manager.proofs_enabled(); }
+        bool produce_models() const { return m_params.m_model; }
+        bool produce_unsat_cores() const { return m_params.m_unsat_core; }
+        bool use_auto_config() const { return m_params.m_auto_config; }
+        unsigned get_timeout() const { return m_params.m_timeout; }
         arith_util & autil() { return m_arith_util; }
         bv_util & bvutil() { return m_bv_util; }
         datalog::dl_decl_util & datalog_util() { return m_datalog_util; }
@@ -167,12 +166,13 @@ namespace api {
         static void out_of_memory_handler(void * _ctx);
 
         void check_sorts(ast * n);
+
         // ------------------------
         //
         // Solver interface for backward compatibility 
         //
         // ------------------------
-        
+        front_end_params & fparams() { return m_fparams; }
         bool has_solver() const { return m_solver != 0; }
         smt::kernel & get_smt_kernel();
         void assert_cnstr(expr * a);

src/api/api_datalog.cpp

@@ -265,7 +265,7 @@ extern "C" {
         RESET_ERROR_CODE();
         lbool r = l_undef;
         cancel_eh<api::fixedpoint_context> eh(*to_fixedpoint_ref(d));
-        unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", UINT_MAX);
+        unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
         api::context::set_interruptable(*(mk_c(c)), eh);        
         {
             scoped_timer timer(timeout, &eh);
@@ -289,7 +289,7 @@ extern "C" {
         LOG_Z3_fixedpoint_query_relations(c, d, num_relations, relations);
         RESET_ERROR_CODE();
         lbool r = l_undef;
-        unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", UINT_MAX);
+        unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
         cancel_eh<api::fixedpoint_context> eh(*to_fixedpoint_ref(d));
         api::context::set_interruptable(*(mk_c(c)), eh);
         {

src/api/api_solver.cpp

@@ -36,10 +36,17 @@ 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(m.proofs_enabled());
+        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", false));
+        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", true));
+        s->m_solver->set_produce_models(s->m_params.get_bool("model", mk_c(c)->produce_models()));
-        s->m_solver->updt_params(s->m_params);
+        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);
+        }
         s->m_solver->init(m, s->m_logic);
         s->m_initialized = true;
     }
@@ -237,7 +244,7 @@ extern "C" {
             }
         }
         expr * const * _assumptions = to_exprs(assumptions);
-        unsigned timeout     = to_solver(s)->m_params.get_uint("timeout", UINT_MAX);
+        unsigned timeout     = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
         bool     use_ctrl_c  = to_solver(s)->m_params.get_bool("ctrl_c", false);
         cancel_eh<solver> eh(*to_solver_ref(s));
         api::context::set_interruptable(*(mk_c(c)), eh);

src/api/z3_api.h

@@ -1308,6 +1308,12 @@ extern "C" {
           - debug_ref_count (Boolean)  Enable debug support for Z3_ast reference counting 
           - trace  (Boolean)           Tracing support for VCC
           - trace_file_name (String)   Trace out file for VCC traces
+          - timeout (unsigned)         default timeout (in milliseconds) used for solvers
+          - well_sorted_check          type checker
+          - auto_config                use heuristics to automatically select solver and configure it
+          - model                      model generation for solvers, this parameter can be overwritten when creating a solver
+          - validate_model             validate models produced by solvers
+          - unsat_core                 unsat-core generation for solvers, this parameter can be overwritten when creating a solver
 
        \sa Z3_set_param_value
        \sa Z3_del_config
@@ -1420,19 +1426,18 @@ extern "C" {
 #endif
 
     /**
-       \brief This is a deprecated function. This is a NOOP in the current version of Z3.
+       \brief Set a value of a context parameter.
 
-       \deprecated Use #Z3_global_param_set.
+       \sa Use #Z3_global_param_set.
 
        def_API('Z3_update_param_value', VOID, (_in(CONTEXT), _in(STRING), _in(STRING)))
     */
     void Z3_API Z3_update_param_value(__in Z3_context c, __in Z3_string param_id, __in Z3_string param_value);
 
     /**
-       \brief This is a deprecated function. This is a NOOP in the current version of Z3.
+       \brief Return the value of a context parameter.
-       It always return Z3_FALSE.
       
-       \deprecated Use #Z3_global_param_get
+       \sa Use #Z3_global_param_get
 
        def_API('Z3_get_param_value', BOOL, (_in(CONTEXT), _in(STRING), _out(STRING)))
     */