1 /*++ 2 Copyright (c) 2012 Microsoft Corporation 3 4 Module Name: 5 6 api_params.cpp 7 8 Abstract: 9 API for creating parameter sets. 10 11 This is essentially a wrapper for params_ref. 12 13 Author: 14 15 Leonardo de Moura (leonardo) 2012-03-05. 16 17 Revision History: 18 19 --*/ 20 #include<iostream> 21 #include "api/z3.h" 22 #include "api/api_log_macros.h" 23 #include "api/api_context.h" 24 #include "api/api_util.h" 25 #include "util/params.h" 26 27 extern "C" { 28 Z3_mk_params(Z3_context c)29 Z3_params Z3_API Z3_mk_params(Z3_context c) { 30 Z3_TRY; 31 LOG_Z3_mk_params(c); 32 RESET_ERROR_CODE(); 33 Z3_params_ref * p = alloc(Z3_params_ref, *mk_c(c)); 34 mk_c(c)->save_object(p); 35 Z3_params r = of_params(p); 36 RETURN_Z3(r); 37 Z3_CATCH_RETURN(nullptr); 38 } 39 40 /** 41 \brief Increment the reference counter of the given parameter set. 42 */ Z3_params_inc_ref(Z3_context c,Z3_params p)43 void Z3_API Z3_params_inc_ref(Z3_context c, Z3_params p) { 44 Z3_TRY; 45 LOG_Z3_params_inc_ref(c, p); 46 RESET_ERROR_CODE(); 47 to_params(p)->inc_ref(); 48 Z3_CATCH; 49 } 50 51 /** 52 \brief Decrement the reference counter of the given parameter set. 53 */ Z3_params_dec_ref(Z3_context c,Z3_params p)54 void Z3_API Z3_params_dec_ref(Z3_context c, Z3_params p) { 55 Z3_TRY; 56 LOG_Z3_params_dec_ref(c, p); 57 RESET_ERROR_CODE(); 58 to_params(p)->dec_ref(); 59 Z3_CATCH; 60 } 61 62 /** 63 \brief Add a Boolean parameter \c k with value \c v to the parameter set \c p. 64 */ Z3_params_set_bool(Z3_context c,Z3_params p,Z3_symbol k,bool v)65 void Z3_API Z3_params_set_bool(Z3_context c, Z3_params p, Z3_symbol k, bool v) { 66 Z3_TRY; 67 LOG_Z3_params_set_bool(c, p, k, v); 68 RESET_ERROR_CODE(); 69 auto name = norm_param_name(to_symbol(k)); 70 to_params(p)->m_params.set_bool(name.c_str(), v); 71 Z3_CATCH; 72 } 73 74 /** 75 \brief Add a unsigned parameter \c k with value \c v to the parameter set \c p. 76 */ Z3_params_set_uint(Z3_context c,Z3_params p,Z3_symbol k,unsigned v)77 void Z3_API Z3_params_set_uint(Z3_context c, Z3_params p, Z3_symbol k, unsigned v) { 78 Z3_TRY; 79 LOG_Z3_params_set_uint(c, p, k, v); 80 RESET_ERROR_CODE(); 81 auto name = norm_param_name(to_symbol(k)); 82 to_params(p)->m_params.set_uint(name.c_str(), v); 83 Z3_CATCH; 84 } 85 86 /** 87 \brief Add a double parameter \c k with value \c v to the parameter set \c p. 88 */ Z3_params_set_double(Z3_context c,Z3_params p,Z3_symbol k,double v)89 void Z3_API Z3_params_set_double(Z3_context c, Z3_params p, Z3_symbol k, double v) { 90 Z3_TRY; 91 LOG_Z3_params_set_double(c, p, k, v); 92 RESET_ERROR_CODE(); 93 auto name = norm_param_name(to_symbol(k)); 94 to_params(p)->m_params.set_double(name.c_str(), v); 95 Z3_CATCH; 96 } 97 98 /** 99 \brief Add a symbol parameter \c k with value \c v to the parameter set \c p. 100 */ Z3_params_set_symbol(Z3_context c,Z3_params p,Z3_symbol k,Z3_symbol v)101 void Z3_API Z3_params_set_symbol(Z3_context c, Z3_params p, Z3_symbol k, Z3_symbol v) { 102 Z3_TRY; 103 LOG_Z3_params_set_symbol(c, p, k, v); 104 RESET_ERROR_CODE(); 105 auto name = norm_param_name(to_symbol(k)); 106 to_params(p)->m_params.set_sym(name.c_str(), to_symbol(v)); 107 Z3_CATCH; 108 } 109 110 /** 111 \brief Convert a parameter set into a string. This function is mainly used for printing the 112 contents of a parameter set. 113 */ Z3_params_to_string(Z3_context c,Z3_params p)114 Z3_string Z3_API Z3_params_to_string(Z3_context c, Z3_params p) { 115 Z3_TRY; 116 LOG_Z3_params_to_string(c, p); 117 RESET_ERROR_CODE(); 118 std::ostringstream buffer; 119 to_params(p)->m_params.display(buffer); 120 return mk_c(c)->mk_external_string(buffer.str()); 121 Z3_CATCH_RETURN(""); 122 } 123 Z3_params_validate(Z3_context c,Z3_params p,Z3_param_descrs d)124 void Z3_API Z3_params_validate(Z3_context c, Z3_params p, Z3_param_descrs d) { 125 Z3_TRY; 126 LOG_Z3_params_validate(c, p, d); 127 RESET_ERROR_CODE(); 128 to_params(p)->m_params.validate(*to_param_descrs_ptr(d)); 129 Z3_CATCH; 130 } 131 Z3_param_descrs_inc_ref(Z3_context c,Z3_param_descrs p)132 void Z3_API Z3_param_descrs_inc_ref(Z3_context c, Z3_param_descrs p) { 133 Z3_TRY; 134 LOG_Z3_param_descrs_inc_ref(c, p); 135 RESET_ERROR_CODE(); 136 to_param_descrs(p)->inc_ref(); 137 Z3_CATCH; 138 } 139 Z3_param_descrs_dec_ref(Z3_context c,Z3_param_descrs p)140 void Z3_API Z3_param_descrs_dec_ref(Z3_context c, Z3_param_descrs p) { 141 Z3_TRY; 142 LOG_Z3_param_descrs_dec_ref(c, p); 143 RESET_ERROR_CODE(); 144 to_param_descrs(p)->dec_ref(); 145 Z3_CATCH; 146 } 147 Z3_param_descrs_get_kind(Z3_context c,Z3_param_descrs p,Z3_symbol n)148 Z3_param_kind Z3_API Z3_param_descrs_get_kind(Z3_context c, Z3_param_descrs p, Z3_symbol n) { 149 Z3_TRY; 150 LOG_Z3_param_descrs_get_kind(c, p, n); 151 RESET_ERROR_CODE(); 152 param_kind k = to_param_descrs_ptr(p)->get_kind(to_symbol(n)); 153 switch (k) { 154 case CPK_UINT: return Z3_PK_UINT; 155 case CPK_BOOL: return Z3_PK_BOOL; 156 case CPK_DOUBLE: return Z3_PK_DOUBLE; 157 case CPK_STRING: return Z3_PK_STRING; 158 case CPK_SYMBOL: return Z3_PK_SYMBOL; 159 case CPK_INVALID: return Z3_PK_INVALID; 160 default: return Z3_PK_OTHER; 161 } 162 Z3_CATCH_RETURN(Z3_PK_INVALID); 163 } 164 Z3_param_descrs_size(Z3_context c,Z3_param_descrs p)165 unsigned Z3_API Z3_param_descrs_size(Z3_context c, Z3_param_descrs p) { 166 Z3_TRY; 167 LOG_Z3_param_descrs_size(c, p); 168 RESET_ERROR_CODE(); 169 return to_param_descrs_ptr(p)->size(); 170 Z3_CATCH_RETURN(0); 171 } 172 Z3_param_descrs_get_name(Z3_context c,Z3_param_descrs p,unsigned i)173 Z3_symbol Z3_API Z3_param_descrs_get_name(Z3_context c, Z3_param_descrs p, unsigned i) { 174 Z3_TRY; 175 LOG_Z3_param_descrs_get_name(c, p, i); 176 RESET_ERROR_CODE(); 177 if (i >= to_param_descrs_ptr(p)->size()) { 178 SET_ERROR_CODE(Z3_IOB, nullptr); 179 return of_symbol(symbol::null); 180 } 181 Z3_symbol result = of_symbol(to_param_descrs_ptr(p)->get_param_name(i)); 182 return result; 183 Z3_CATCH_RETURN(of_symbol(symbol::null)); 184 } 185 Z3_param_descrs_get_documentation(Z3_context c,Z3_param_descrs p,Z3_symbol s)186 Z3_string Z3_API Z3_param_descrs_get_documentation(Z3_context c, Z3_param_descrs p, Z3_symbol s) { 187 Z3_TRY; 188 LOG_Z3_param_descrs_get_documentation(c, p, s); 189 RESET_ERROR_CODE(); 190 char const* result = to_param_descrs_ptr(p)->get_descr(to_symbol(s)); 191 if (result == nullptr) { 192 SET_ERROR_CODE(Z3_IOB, nullptr); 193 RETURN_Z3(nullptr); 194 } 195 return mk_c(c)->mk_external_string(result); 196 Z3_CATCH_RETURN(nullptr); 197 } 198 Z3_param_descrs_to_string(Z3_context c,Z3_param_descrs p)199 Z3_string Z3_API Z3_param_descrs_to_string(Z3_context c, Z3_param_descrs p) { 200 Z3_TRY; 201 LOG_Z3_param_descrs_to_string(c, p); 202 RESET_ERROR_CODE(); 203 std::ostringstream buffer; 204 buffer << "("; 205 unsigned sz = to_param_descrs_ptr(p)->size(); 206 for (unsigned i = 0; i < sz; i++) { 207 if (i > 0) 208 buffer << ", "; 209 buffer << to_param_descrs_ptr(p)->get_param_name(i); 210 } 211 buffer << ")"; 212 return mk_c(c)->mk_external_string(buffer.str()); 213 Z3_CATCH_RETURN(""); 214 } 215 216 }; 217