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