1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6     api_config_params.cpp
7 
8 Abstract:
9     Configuration parameters
10 
11 Author:
12 
13     Leonardo de Moura (leonardo) 2012-02-29.
14 
15 Revision History:
16 
17 --*/
18 #include "api/z3.h"
19 #include "api/api_context.h"
20 #include "ast/pp.h"
21 #include "api/api_log_macros.h"
22 #include "api/api_util.h"
23 #include "cmd_context/cmd_context.h"
24 #include "util/symbol.h"
25 #include "util/gparams.h"
26 #include "util/env_params.h"
27 #include "params/context_params.h"
28 
29 extern "C" {
Z3_global_param_set(Z3_string param_id,Z3_string param_value)30     void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value) {
31         memory::initialize(UINT_MAX);
32         LOG_Z3_global_param_set(param_id, param_value);
33         try {
34             gparams::set(param_id, param_value);
35             env_params::updt_params();
36         }
37         catch (z3_exception & ex) {
38             // The error handler is only available for contexts
39             // Just throw a warning.
40             warning_msg("%s", ex.msg());
41         }
42     }
43 
Z3_global_param_reset_all(void)44     void Z3_API Z3_global_param_reset_all(void) {
45         memory::initialize(UINT_MAX);
46         LOG_Z3_global_param_reset_all();
47         gparams::reset();
48         env_params::updt_params();
49     }
50 
51     static std::string g_Z3_global_param_get_buffer;
52 
Z3_global_param_get(Z3_string param_id,Z3_string_ptr param_value)53     Z3_bool_opt Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value) {
54         memory::initialize(UINT_MAX);
55         LOG_Z3_global_param_get(param_id, param_value);
56         *param_value = nullptr;
57         try {
58             g_Z3_global_param_get_buffer = gparams::get_value(param_id);
59             *param_value = g_Z3_global_param_get_buffer.c_str();
60             return true;
61         }
62         catch (z3_exception & ex) {
63             // The error handler is only available for contexts
64             // Just throw a warning.
65             warning_msg("%s", ex.msg());
66             return false;
67         }
68     }
69 
Z3_mk_config(void)70     Z3_config Z3_API Z3_mk_config(void) {
71         try {
72             memory::initialize(UINT_MAX);
73             LOG_Z3_mk_config();
74             Z3_config r = reinterpret_cast<Z3_config>(alloc(context_params));
75             RETURN_Z3(r);
76         } catch (z3_exception & ex) {
77             // The error handler is only available for contexts
78             // Just throw a warning.
79             warning_msg("%s", ex.msg());
80             return nullptr;
81         }
82     }
83 
Z3_del_config(Z3_config c)84     void Z3_API Z3_del_config(Z3_config c) {
85         LOG_Z3_del_config(c);
86         dealloc((reinterpret_cast<context_params*>(c)));
87     }
88 
Z3_set_param_value(Z3_config c,char const * param_id,char const * param_value)89     void Z3_API Z3_set_param_value(Z3_config c, char const * param_id, char const * param_value) {
90         LOG_Z3_set_param_value(c, param_id, param_value);
91         try {
92             context_params * p = reinterpret_cast<context_params*>(c);
93             p->set(param_id, param_value);
94         }
95         catch (z3_exception & ex) {
96             // The error handler is only available for contexts
97             // Just throw a warning.
98             warning_msg("%s", ex.msg());
99         }
100     }
101 
Z3_update_param_value(Z3_context c,Z3_string param_id,Z3_string param_value)102     void Z3_API Z3_update_param_value(Z3_context c, Z3_string param_id, Z3_string param_value) {
103         Z3_TRY;
104         LOG_Z3_update_param_value(c, param_id, param_value);
105         RESET_ERROR_CODE();
106         mk_c(c)->params().set(param_id, param_value);
107         Z3_CATCH;
108     }
109 
110 };
111