1 /*++ 2 Copyright (c) 2012 Microsoft Corporation 3 4 Module Name: 5 6 api_bv.cpp 7 8 Abstract: 9 API for bv theory 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_log_macros.h" 20 #include "api/api_context.h" 21 #include "api/api_util.h" 22 #include "ast/bv_decl_plugin.h" 23 24 extern "C" { 25 26 Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz) { 27 Z3_TRY; 28 LOG_Z3_mk_bv_sort(c, sz); 29 RESET_ERROR_CODE(); 30 parameter p(sz); 31 Z3_sort r = of_sort(mk_c(c)->m().mk_sort(mk_c(c)->get_bv_fid(), BV_SORT, 1, &p)); 32 RETURN_Z3(r); 33 Z3_CATCH_RETURN(nullptr); 34 } 35 36 #define MK_BV_UNARY(NAME, OP) MK_UNARY(NAME, mk_c(c)->get_bv_fid(), OP, SKIP) 37 #define MK_BV_BINARY(NAME, OP) MK_BINARY(NAME, mk_c(c)->get_bv_fid(), OP, SKIP) 38 39 MK_BV_UNARY(Z3_mk_bvnot, OP_BNOT); 40 MK_BV_UNARY(Z3_mk_bvredand, OP_BREDAND); 41 MK_BV_UNARY(Z3_mk_bvredor, OP_BREDOR); 42 MK_BV_BINARY(Z3_mk_bvand, OP_BAND); 43 MK_BV_BINARY(Z3_mk_bvor, OP_BOR); 44 MK_BV_BINARY(Z3_mk_bvxor, OP_BXOR); 45 MK_BV_BINARY(Z3_mk_bvnand, OP_BNAND); 46 MK_BV_BINARY(Z3_mk_bvnor, OP_BNOR); 47 MK_BV_BINARY(Z3_mk_bvxnor, OP_BXNOR); 48 MK_BV_BINARY(Z3_mk_bvadd, OP_BADD); 49 MK_BV_BINARY(Z3_mk_bvmul, OP_BMUL); 50 MK_BV_BINARY(Z3_mk_bvudiv, OP_BUDIV); 51 MK_BV_BINARY(Z3_mk_bvsdiv, OP_BSDIV); 52 MK_BV_BINARY(Z3_mk_bvurem, OP_BUREM); 53 MK_BV_BINARY(Z3_mk_bvsrem, OP_BSREM); 54 MK_BV_BINARY(Z3_mk_bvsmod, OP_BSMOD); 55 MK_BV_BINARY(Z3_mk_bvule, OP_ULEQ); 56 MK_BV_BINARY(Z3_mk_bvsle, OP_SLEQ); 57 MK_BV_BINARY(Z3_mk_bvuge, OP_UGEQ); 58 MK_BV_BINARY(Z3_mk_bvsge, OP_SGEQ); 59 MK_BV_BINARY(Z3_mk_bvult, OP_ULT); 60 MK_BV_BINARY(Z3_mk_bvslt, OP_SLT); 61 MK_BV_BINARY(Z3_mk_bvugt, OP_UGT); 62 MK_BV_BINARY(Z3_mk_bvsgt, OP_SGT); 63 MK_BV_BINARY(Z3_mk_concat, OP_CONCAT); 64 MK_BV_BINARY(Z3_mk_bvshl, OP_BSHL); 65 MK_BV_BINARY(Z3_mk_bvlshr, OP_BLSHR); 66 MK_BV_BINARY(Z3_mk_bvashr, OP_BASHR); 67 MK_BV_BINARY(Z3_mk_ext_rotate_left, OP_EXT_ROTATE_LEFT); 68 MK_BV_BINARY(Z3_mk_ext_rotate_right, OP_EXT_ROTATE_RIGHT); 69 70 static Z3_ast mk_extract_core(Z3_context c, unsigned high, unsigned low, Z3_ast n) { 71 expr * _n = to_expr(n); 72 parameter params[2] = { parameter(high), parameter(low) }; 73 expr * a = mk_c(c)->m().mk_app(mk_c(c)->get_bv_fid(), OP_EXTRACT, 2, params, 1, &_n); 74 mk_c(c)->save_ast_trail(a); 75 check_sorts(c, a); 76 return of_ast(a); 77 } 78 79 Z3_ast Z3_API Z3_mk_extract(Z3_context c, unsigned high, unsigned low, Z3_ast n) { 80 Z3_TRY; 81 LOG_Z3_mk_extract(c, high, low, n); 82 RESET_ERROR_CODE(); 83 Z3_ast r = mk_extract_core(c, high, low, n); 84 RETURN_Z3(r); 85 Z3_CATCH_RETURN(nullptr); 86 } 87 88 #define MK_BV_PUNARY(NAME, OP) \ 89 Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ 90 Z3_TRY; \ 91 LOG_ ## NAME(c, i, n); \ 92 RESET_ERROR_CODE(); \ 93 expr * _n = to_expr(n); \ 94 parameter p(i); \ 95 ast* a = mk_c(c)->m().mk_app(mk_c(c)->get_bv_fid(), OP, 1, &p, 1, &_n); \ 96 mk_c(c)->save_ast_trail(a); \ 97 check_sorts(c, a); \ 98 RETURN_Z3(of_ast(a)); \ 99 Z3_CATCH_RETURN(0); \ 100 } 101 102 MK_BV_PUNARY(Z3_mk_sign_ext, OP_SIGN_EXT); 103 MK_BV_PUNARY(Z3_mk_zero_ext, OP_ZERO_EXT); 104 MK_BV_PUNARY(Z3_mk_repeat, OP_REPEAT); 105 MK_BV_PUNARY(Z3_mk_rotate_left, OP_ROTATE_LEFT); 106 MK_BV_PUNARY(Z3_mk_rotate_right, OP_ROTATE_RIGHT); 107 MK_BV_PUNARY(Z3_mk_int2bv, OP_INT2BV); 108 109 Z3_ast Z3_API Z3_mk_bv2int(Z3_context c, Z3_ast n, bool is_signed) { 110 Z3_TRY; 111 LOG_Z3_mk_bv2int(c, n, is_signed); 112 RESET_ERROR_CODE(); 113 Z3_sort int_s = Z3_mk_int_sort(c); 114 if (is_signed) { 115 Z3_ast r = Z3_mk_bv2int(c, n, false); 116 Z3_inc_ref(c, r); 117 Z3_sort s = Z3_get_sort(c, n); 118 unsigned sz = Z3_get_bv_sort_size(c, s); 119 rational max_bound = power(rational(2), sz); 120 auto str = max_bound.to_string(); 121 Z3_ast bound = Z3_mk_numeral(c, str.c_str(), int_s); 122 Z3_inc_ref(c, bound); 123 Z3_ast zero = Z3_mk_int(c, 0, s); 124 Z3_inc_ref(c, zero); 125 Z3_ast pred = Z3_mk_bvslt(c, n, zero); 126 Z3_inc_ref(c, pred); 127 // if n <_sigend 0 then r - s^sz else r 128 Z3_ast args[2] = { r, bound }; 129 Z3_ast sub = Z3_mk_sub(c, 2, args); 130 Z3_inc_ref(c, sub); 131 Z3_ast res = Z3_mk_ite(c, pred, sub, r); 132 Z3_dec_ref(c, bound); 133 Z3_dec_ref(c, pred); 134 Z3_dec_ref(c, sub); 135 Z3_dec_ref(c, zero); 136 Z3_dec_ref(c, r); 137 RETURN_Z3(res); 138 } 139 else { 140 expr * _n = to_expr(n); 141 parameter p(to_sort(int_s)); 142 ast* a = mk_c(c)->m().mk_app(mk_c(c)->get_bv_fid(), OP_BV2INT, 1, &p, 1, &_n); 143 mk_c(c)->save_ast_trail(a); 144 check_sorts(c, a); 145 RETURN_Z3(of_ast(a)); 146 } 147 Z3_CATCH_RETURN(nullptr); 148 } 149 150 /** 151 \brief Create a bit-vector of sort \s with 1 in the most significant bit position. 152 153 The sort \s must be a bit-vector sort. 154 155 This function is a shorthand for <tt>shl(1, N-1)</tt> 156 where <tt>N</tt> are the number of bits of \c s. 157 */ 158 Z3_ast Z3_API Z3_mk_bvmsb(Z3_context c, Z3_sort s) { 159 Z3_TRY; 160 RESET_ERROR_CODE(); 161 // Not logging this one, since it is just syntax sugar. 162 unsigned sz = Z3_get_bv_sort_size(c, s); 163 if (sz == 0) { 164 SET_ERROR_CODE(Z3_INVALID_ARG, "zero length bit-vector supplied"); 165 return nullptr; 166 } 167 Z3_ast x = Z3_mk_int64(c, 1, s); 168 Z3_inc_ref(c, x); 169 Z3_ast y = Z3_mk_int64(c, sz - 1, s); 170 Z3_inc_ref(c, y); 171 Z3_ast result = Z3_mk_bvshl(c, x, y); 172 Z3_dec_ref(c, x); 173 Z3_dec_ref(c, y); 174 return result; 175 Z3_CATCH_RETURN(nullptr); 176 } 177 178 static Z3_ast Z3_mk_bvsmin(Z3_context c, Z3_sort s) { 179 return Z3_mk_bvmsb(c, s); 180 } 181 182 Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed) { 183 Z3_TRY; 184 RESET_ERROR_CODE(); 185 if (is_signed) { 186 Z3_ast zero = Z3_mk_int(c, 0, Z3_get_sort(c, t1)); 187 Z3_inc_ref(c, zero); 188 Z3_ast r = Z3_mk_bvadd(c, t1, t2); 189 Z3_inc_ref(c, r); 190 Z3_ast l1 = Z3_mk_bvslt(c, zero, t1); 191 Z3_inc_ref(c, l1); 192 Z3_ast l2 = Z3_mk_bvslt(c, zero, t2); 193 Z3_inc_ref(c, l2); 194 Z3_ast args[2] = { l1, l2 }; 195 Z3_ast args_pos = Z3_mk_and(c, 2, args); 196 Z3_inc_ref(c, args_pos); 197 Z3_ast result = Z3_mk_implies(c, args_pos, Z3_mk_bvslt(c, zero, r)); 198 Z3_dec_ref(c, r); 199 Z3_dec_ref(c, l1); 200 Z3_dec_ref(c, l2); 201 Z3_dec_ref(c, args_pos); 202 Z3_dec_ref(c, zero); 203 return result; 204 } 205 else { 206 unsigned sz = Z3_get_bv_sort_size(c, Z3_get_sort(c, t1)); 207 t1 = Z3_mk_zero_ext(c, 1, t1); 208 Z3_inc_ref(c, t1); 209 t2 = Z3_mk_zero_ext(c, 1, t2); 210 Z3_inc_ref(c, t2); 211 Z3_ast r = Z3_mk_bvadd(c, t1, t2); 212 Z3_inc_ref(c, r); 213 Z3_ast ex = Z3_mk_extract(c, sz, sz, r); 214 Z3_inc_ref(c, ex); 215 Z3_ast result = Z3_mk_eq(c, ex, Z3_mk_int(c, 0, Z3_mk_bv_sort(c, 1))); 216 Z3_dec_ref(c, t1); 217 Z3_dec_ref(c, t2); 218 Z3_dec_ref(c, ex); 219 Z3_dec_ref(c, r); 220 return result; 221 } 222 Z3_CATCH_RETURN(nullptr); 223 } 224 225 // only for signed machine integers 226 Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2) { 227 Z3_TRY; 228 RESET_ERROR_CODE(); 229 Z3_ast zero = Z3_mk_int(c, 0, Z3_get_sort(c, t1)); 230 Z3_inc_ref(c, zero); 231 Z3_ast r = Z3_mk_bvadd(c, t1, t2); 232 Z3_inc_ref(c, r); 233 Z3_ast l1 = Z3_mk_bvslt(c, t1, zero); 234 Z3_inc_ref(c, l1); 235 Z3_ast l2 = Z3_mk_bvslt(c, t2, zero); 236 Z3_inc_ref(c, l2); 237 Z3_ast args[2] = { l1, l2 }; 238 Z3_ast args_neg = Z3_mk_and(c, 2, args); 239 Z3_inc_ref(c, args_neg); 240 Z3_ast lt = Z3_mk_bvslt(c, r, zero); 241 Z3_inc_ref(c, lt); 242 Z3_ast result = Z3_mk_implies(c, args_neg, lt); 243 Z3_dec_ref(c, lt); 244 Z3_dec_ref(c, l1); 245 Z3_dec_ref(c, l2); 246 Z3_dec_ref(c, r); 247 Z3_dec_ref(c, args_neg); 248 Z3_dec_ref(c, zero); 249 return result; 250 Z3_CATCH_RETURN(nullptr); 251 } 252 253 // only for signed machine integers 254 Z3_ast Z3_API Z3_mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2) { 255 Z3_TRY; 256 RESET_ERROR_CODE(); 257 Z3_ast minus_t2 = Z3_mk_bvneg(c, t2); 258 Z3_inc_ref(c, minus_t2); 259 Z3_sort s = Z3_get_sort(c, t2); 260 Z3_ast min = Z3_mk_bvsmin(c, s); 261 Z3_inc_ref(c, min); 262 Z3_ast x = Z3_mk_eq(c, t2, min); 263 Z3_inc_ref(c, x); 264 Z3_ast zero = Z3_mk_int(c, 0, s); 265 Z3_inc_ref(c, zero); 266 Z3_ast y = Z3_mk_bvslt(c, t1, zero); 267 Z3_inc_ref(c, y); 268 Z3_ast z = Z3_mk_bvadd_no_overflow(c, t1, minus_t2, true); 269 Z3_inc_ref(c, z); 270 Z3_ast result = Z3_mk_ite(c, x, y, z); 271 mk_c(c)->save_ast_trail(to_app(result)); 272 Z3_dec_ref(c, minus_t2); 273 Z3_dec_ref(c, min); 274 Z3_dec_ref(c, x); 275 Z3_dec_ref(c, y); 276 Z3_dec_ref(c, z); 277 Z3_dec_ref(c, zero); 278 return result; 279 Z3_CATCH_RETURN(nullptr); 280 } 281 282 Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed) { 283 Z3_TRY; 284 RESET_ERROR_CODE(); 285 if (is_signed) { 286 Z3_ast zero = Z3_mk_int(c, 0, Z3_get_sort(c, t1)); 287 Z3_inc_ref(c, zero); 288 Z3_ast minus_t2 = Z3_mk_bvneg(c, t2); 289 Z3_inc_ref(c, minus_t2); 290 Z3_ast x = Z3_mk_bvslt(c, zero, t2); 291 Z3_inc_ref(c, x); 292 Z3_ast y = Z3_mk_bvadd_no_underflow(c, t1, minus_t2); 293 Z3_inc_ref(c, y); 294 Z3_ast result = Z3_mk_implies(c, x, y); 295 Z3_dec_ref(c, zero); 296 Z3_dec_ref(c, minus_t2); 297 Z3_dec_ref(c, x); 298 Z3_dec_ref(c, y); 299 return result; 300 } 301 else { 302 return Z3_mk_bvule(c, t2, t1); 303 } 304 Z3_CATCH_RETURN(nullptr); 305 } 306 307 Z3_ast Z3_API Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast n1, Z3_ast n2, bool is_signed) { 308 LOG_Z3_mk_bvmul_no_overflow(c, n1, n2, is_signed); 309 RESET_ERROR_CODE(); 310 if (is_signed) { 311 MK_BINARY_BODY(Z3_mk_bvmul_no_overflow, mk_c(c)->get_bv_fid(), OP_BSMUL_NO_OVFL, SKIP); 312 } 313 else { 314 MK_BINARY_BODY(Z3_mk_bvmul_no_overflow, mk_c(c)->get_bv_fid(), OP_BUMUL_NO_OVFL, SKIP); 315 } 316 } 317 318 // only for signed machine integers 319 Z3_ast Z3_API Z3_mk_bvmul_no_underflow(Z3_context c, Z3_ast n1, Z3_ast n2) { 320 LOG_Z3_mk_bvmul_no_underflow(c, n1, n2); 321 MK_BINARY_BODY(Z3_mk_bvmul_no_underflow, mk_c(c)->get_bv_fid(), OP_BSMUL_NO_UDFL, SKIP); 322 } 323 324 // only for signed machine integers 325 Z3_ast Z3_API Z3_mk_bvneg_no_overflow(Z3_context c, Z3_ast t) { 326 Z3_TRY; 327 RESET_ERROR_CODE(); 328 Z3_ast min = Z3_mk_bvsmin(c, Z3_get_sort(c, t)); 329 if (Z3_get_error_code(c) != Z3_OK) return nullptr; 330 Z3_ast eq = Z3_mk_eq(c, t, min); 331 if (Z3_get_error_code(c) != Z3_OK) return nullptr; 332 return Z3_mk_not(c, eq); 333 Z3_CATCH_RETURN(nullptr); 334 } 335 336 // only for signed machine integers 337 Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2) { 338 Z3_TRY; 339 RESET_ERROR_CODE(); 340 Z3_sort s = Z3_get_sort(c, t1); 341 Z3_ast min = Z3_mk_bvmsb(c, s); 342 Z3_inc_ref(c, min); 343 Z3_ast x = Z3_mk_eq(c, t1, min); 344 Z3_inc_ref(c, x); 345 Z3_ast y = Z3_mk_int(c, -1, s); 346 Z3_inc_ref(c, y); 347 Z3_ast z = Z3_mk_eq(c, t2, y); 348 Z3_inc_ref(c, z); 349 Z3_ast args[2] = { x, z }; 350 Z3_ast u = Z3_mk_and(c, 2, args); 351 Z3_inc_ref(c, u); 352 Z3_ast result = Z3_mk_not(c, u); 353 Z3_dec_ref(c, min); 354 Z3_dec_ref(c, x); 355 Z3_dec_ref(c, y); 356 Z3_dec_ref(c, z); 357 Z3_dec_ref(c, u); 358 return result; 359 Z3_CATCH_RETURN(nullptr); 360 } 361 362 Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast n1, Z3_ast n2) { 363 Z3_TRY; 364 LOG_Z3_mk_bvsub(c, n1, n2); 365 RESET_ERROR_CODE(); 366 MK_BINARY_BODY(Z3_mk_bvsub, mk_c(c)->get_bv_fid(), OP_BSUB, SKIP); 367 Z3_CATCH_RETURN(nullptr); 368 } 369 370 Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast n) { 371 Z3_TRY; 372 LOG_Z3_mk_bvneg(c, n); 373 RESET_ERROR_CODE(); 374 MK_UNARY_BODY(Z3_mk_bvneg, mk_c(c)->get_bv_fid(), OP_BNEG, SKIP); 375 Z3_CATCH_RETURN(nullptr); 376 } 377 378 unsigned Z3_API Z3_get_bv_sort_size(Z3_context c, Z3_sort t) { 379 Z3_TRY; 380 LOG_Z3_get_bv_sort_size(c, t); 381 RESET_ERROR_CODE(); 382 CHECK_VALID_AST(t, 0); 383 if (to_sort(t)->get_family_id() == mk_c(c)->get_bv_fid() && to_sort(t)->get_decl_kind() == BV_SORT) { 384 return to_sort(t)->get_parameter(0).get_int(); 385 } 386 SET_ERROR_CODE(Z3_INVALID_ARG, "sort is not a bit-vector"); 387 return 0; 388 Z3_CATCH_RETURN(0); 389 } 390 391 }; 392