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 
28 extern "C" {
Z3_global_param_set(Z3_string param_id,Z3_string param_value)29     void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value) {
30         memory::initialize(UINT_MAX);
31         LOG_Z3_global_param_set(param_id, param_value);
32         try {
33             gparams::set(param_id, param_value);
34             env_params::updt_params();
35         }
36         catch (z3_exception & ex) {
37             // The error handler is only available for contexts
38             // Just throw a warning.
39             warning_msg("%s", ex.msg());
40         }
41     }
42 
Z3_global_param_reset_all(void)43     void Z3_API Z3_global_param_reset_all(void) {
44         memory::initialize(UINT_MAX);
45         LOG_Z3_global_param_reset_all();
46         gparams::reset();
47         env_params::updt_params();
48     }
49 
Z3_global_param_get(Z3_string param_id,Z3_string_ptr param_value)50     Z3_bool_opt Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value) {
51         memory::initialize(UINT_MAX);
52         LOG_Z3_global_param_get(param_id, param_value);
53         *param_value = nullptr;
54         try {
55             gparams::g_buffer() = gparams::get_value(param_id);
56             *param_value = gparams::g_buffer().c_str();
57             return true;
58         }
59         catch (z3_exception & ex) {
60             // The error handler is only available for contexts
61             // Just throw a warning.
62             warning_msg("%s", ex.msg());
63             return false;
64         }
65     }
66 
Z3_mk_config(void)67     Z3_config Z3_API Z3_mk_config(void) {
68         try {
69             memory::initialize(UINT_MAX);
70             LOG_Z3_mk_config();
71             Z3_config r = reinterpret_cast<Z3_config>(alloc(ast_context_params));
72             RETURN_Z3(r);
73         } catch (z3_exception & ex) {
74             // The error handler is only available for contexts
75             // Just throw a warning.
76             warning_msg("%s", ex.msg());
77             return nullptr;
78         }
79     }
80 
Z3_del_config(Z3_config c)81     void Z3_API Z3_del_config(Z3_config c) {
82         LOG_Z3_del_config(c);
83         dealloc((reinterpret_cast<ast_context_params*>(c)));
84     }
85 
Z3_set_param_value(Z3_config c,char const * param_id,char const * param_value)86     void Z3_API Z3_set_param_value(Z3_config c, char const * param_id, char const * param_value) {
87         LOG_Z3_set_param_value(c, param_id, param_value);
88         try {
89             ast_context_params * p = reinterpret_cast<ast_context_params*>(c);
90             p->set(param_id, param_value);
91         }
92         catch (z3_exception & ex) {
93             // The error handler is only available for contexts
94             // Just throw a warning.
95             warning_msg("%s", ex.msg());
96         }
97     }
98 
Z3_update_param_value(Z3_context c,Z3_string param_id,Z3_string param_value)99     void Z3_API Z3_update_param_value(Z3_context c, Z3_string param_id, Z3_string param_value) {
100         Z3_TRY;
101         LOG_Z3_update_param_value(c, param_id, param_value);
102         RESET_ERROR_CODE();
103         mk_c(c)->params().set(param_id, param_value);
104         Z3_CATCH;
105     }
106 
107 };
108