From 12e45c9d17aa48151b2c20573fb3b527b32fdb54 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antti=20Hyv=C3=A4rinen?= Date: Tue, 9 May 2023 19:37:46 +0200 Subject: [PATCH 1/9] Implement proposed smtlib2 bitvector overflow predicates (#6715) * Logical names for function declarations in c++ Currently, for example, the function declaration symbol member for checking whether multiplication *does not* overflow is called `m_bv_smul_ovfl`. Since we are introducing the upcoming smtlib2 symbols that check that multpliciation *does* overflow, the not overflow check symbols are renamed to `m_bv_smul_no_ovfl` etc. * Implement smtlib overflow preds for multiplication Smtlib2 is being extended to include overflow predicates for bit vectors (see https://groups.google.com/u/1/g/smt-lib/c/J4D99wT0aKI). This commit introduces the predicates `bvumulo` and `bvsmulo` that return `true` if the unsigned multiplication overflows or the signed multiplication underflows or overflows, respectively. * Move mul overflow predicates to BV logic * Add a todo on illogical argument order * Implement mk_unary_pred for bv * Implement bvnego * Implement bvuaddo * Implement bvsaddo * Implement bvusubo * Implement bvssubo * Implement bvsdivo --- src/ast/bv_decl_plugin.cpp | 47 +++++++++++- src/ast/bv_decl_plugin.h | 43 ++++++++++- src/ast/rewriter/bv_rewriter.cpp | 123 +++++++++++++++++++++++++++++++ src/ast/rewriter/bv_rewriter.h | 16 ++++ 4 files changed, 222 insertions(+), 7 deletions(-) diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 351d037cb..4d38327a5 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -118,9 +118,22 @@ void bv_decl_plugin::finalize() { DEC_REF(m_bv_redand); DEC_REF(m_bv_comp); + DEC_REF(m_bv_mul_no_ovfl); + DEC_REF(m_bv_smul_no_ovfl); + DEC_REF(m_bv_smul_no_udfl); + DEC_REF(m_bv_mul_ovfl); DEC_REF(m_bv_smul_ovfl); - DEC_REF(m_bv_smul_udfl); + + DEC_REF(m_bv_neg_ovfl); + + DEC_REF(m_bv_uadd_ovfl); + DEC_REF(m_bv_sadd_ovfl); + + DEC_REF(m_bv_usub_ovfl); + DEC_REF(m_bv_ssub_ovfl); + + DEC_REF(m_bv_sdiv_ovfl); DEC_REF(m_bv_shl); DEC_REF(m_bv_lshr); @@ -245,6 +258,16 @@ func_decl * bv_decl_plugin::mk_bv2int(unsigned bv_size, unsigned num_parameters, return m_bv2int[bv_size]; } +func_decl * bv_decl_plugin::mk_unary_pred(ptr_vector & decls, decl_kind k, char const * name, unsigned bv_size) { + force_ptr_array_size(decls, bv_size+1); + + if (decls[bv_size] == 0) { + decls[bv_size] = m_manager->mk_func_decl(symbol(name), get_bv_sort(bv_size), m_manager->mk_bool_sort(), func_decl_info(m_family_id, k)); + m_manager->inc_ref(decls[bv_size]); + } + return decls[bv_size]; +} + func_decl * bv_decl_plugin::mk_pred(ptr_vector & decls, decl_kind k, char const * name, unsigned bv_size) { force_ptr_array_size(decls, bv_size + 1); @@ -289,6 +312,7 @@ func_decl * bv_decl_plugin::mk_comp(unsigned bv_size) { func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned bv_size) { switch (k) { case OP_BNEG: return mk_unary(m_bv_neg, k, "bvneg", bv_size); + case OP_BNEG_OVFL: return mk_unary_pred(m_bv_neg_ovfl, k, "bvnego", bv_size); case OP_BADD: return mk_binary(m_bv_add, k, "bvadd", bv_size, true); case OP_BSUB: return mk_binary(m_bv_sub, k, "bvsub", bv_size, false); case OP_BMUL: return mk_binary(m_bv_mul, k, "bvmul", bv_size, true); @@ -327,9 +351,16 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned bv_size) { case OP_BREDOR: return mk_reduction(m_bv_redor, k, "bvredor", bv_size); case OP_BREDAND: return mk_reduction(m_bv_redand, k, "bvredand", bv_size); case OP_BCOMP: return mk_comp(bv_size); - case OP_BUMUL_NO_OVFL: return mk_pred(m_bv_mul_ovfl, k, "bvumul_noovfl", bv_size); - case OP_BSMUL_NO_OVFL: return mk_pred(m_bv_smul_ovfl, k, "bvsmul_noovfl", bv_size); - case OP_BSMUL_NO_UDFL: return mk_pred(m_bv_smul_udfl, k, "bvsmul_noudfl", bv_size); + case OP_BUMUL_NO_OVFL: return mk_pred(m_bv_mul_no_ovfl, k, "bvumul_noovfl", bv_size); + case OP_BSMUL_NO_OVFL: return mk_pred(m_bv_smul_no_ovfl, k, "bvsmul_noovfl", bv_size); + case OP_BSMUL_NO_UDFL: return mk_pred(m_bv_smul_no_udfl, k, "bvsmul_noudfl", bv_size); + case OP_BUMUL_OVFL: return mk_pred(m_bv_mul_ovfl, k, "bvumulo", bv_size); + case OP_BSMUL_OVFL: return mk_pred(m_bv_smul_ovfl, k, "bvsmulo", bv_size); + case OP_BSDIV_OVFL: return mk_pred(m_bv_sdiv_ovfl, k, "bvsdivo", bv_size); + case OP_BUADD_OVFL: return mk_pred(m_bv_uadd_ovfl, k, "bvuaddo", bv_size); + case OP_BSADD_OVFL: return mk_pred(m_bv_sadd_ovfl, k, "bvsaddo", bv_size); + case OP_BUSUB_OVFL: return mk_pred(m_bv_usub_ovfl, k, "bvusubo", bv_size); + case OP_BSSUB_OVFL: return mk_pred(m_bv_ssub_ovfl, k, "bvssubo", bv_size); case OP_BSHL: return mk_binary(m_bv_shl, k, "bvshl", bv_size, false); case OP_BLSHR: return mk_binary(m_bv_lshr, k, "bvlshr", bv_size, false); @@ -681,10 +712,18 @@ void bv_decl_plugin::get_op_names(svector & op_names, symbol const op_names.push_back(builtin_name("bit1",OP_BIT1)); op_names.push_back(builtin_name("bit0",OP_BIT0)); op_names.push_back(builtin_name("bvneg",OP_BNEG)); + op_names.push_back(builtin_name("bvnego", OP_BNEG_OVFL)); op_names.push_back(builtin_name("bvadd",OP_BADD)); + op_names.push_back(builtin_name("bvuaddo",OP_BUADD_OVFL)); + op_names.push_back(builtin_name("bvsaddo",OP_BSADD_OVFL)); op_names.push_back(builtin_name("bvsub",OP_BSUB)); + op_names.push_back(builtin_name("bvusubo",OP_BUSUB_OVFL)); + op_names.push_back(builtin_name("bvssubo",OP_BSSUB_OVFL)); op_names.push_back(builtin_name("bvmul",OP_BMUL)); + op_names.push_back(builtin_name("bvumulo",OP_BUMUL_OVFL)); + op_names.push_back(builtin_name("bvsmulo",OP_BSMUL_OVFL)); op_names.push_back(builtin_name("bvsdiv",OP_BSDIV)); + op_names.push_back(builtin_name("bvsdivo",OP_BSDIV_OVFL)); op_names.push_back(builtin_name("bvudiv",OP_BUDIV)); op_names.push_back(builtin_name("bvsrem",OP_BSREM)); op_names.push_back(builtin_name("bvurem",OP_BUREM)); diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index fc7e35245..51faca7ed 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -93,6 +93,19 @@ enum bv_op_kind { OP_BSMUL_NO_OVFL, // no signed multiplication overflow predicate OP_BSMUL_NO_UDFL, // no signed multiplication underflow predicate + OP_BUMUL_OVFL, // unsigned multiplication overflow predicate (negation of OP_BUMUL_NO_OVFL) + OP_BSMUL_OVFL, // signed multiplication over/underflow predicate + + OP_BSDIV_OVFL, // signed division overflow perdicate + + OP_BNEG_OVFL, // negation overflow predicate + + OP_BUADD_OVFL, // unsigned addition overflow predicate + OP_BSADD_OVFL, // signed addition overflow predicate + + OP_BUSUB_OVFL, // unsigned subtraction overflow predicate + OP_BSSUB_OVFL, // signed subtraction overflow predicate + OP_BIT2BOOL, // predicate OP_MKBV, // bools to bv OP_INT2BV, @@ -189,9 +202,22 @@ protected: ptr_vector m_bv_redand; ptr_vector m_bv_comp; - ptr_vector m_bv_mul_ovfl; - ptr_vector m_bv_smul_ovfl; - ptr_vector m_bv_smul_udfl; + ptr_vector m_bv_mul_no_ovfl; + ptr_vector m_bv_smul_no_ovfl; + ptr_vector m_bv_smul_no_udfl; + + ptr_vector m_bv_mul_ovfl; + ptr_vector m_bv_smul_ovfl; + + ptr_vector m_bv_sdiv_ovfl; + + ptr_vector m_bv_neg_ovfl; + + ptr_vector m_bv_uadd_ovfl; + ptr_vector m_bv_sadd_ovfl; + + ptr_vector m_bv_usub_ovfl; + ptr_vector m_bv_ssub_ovfl; ptr_vector m_bv_shl; ptr_vector m_bv_lshr; @@ -213,6 +239,7 @@ protected: func_decl * mk_unary(ptr_vector & decls, decl_kind k, char const * name, unsigned bv_size); func_decl * mk_pred(ptr_vector & decls, decl_kind k, char const * name, unsigned bv_size); + func_decl * mk_unary_pred(ptr_vector & decls, decl_kind k, char const * name, unsigned bv_size); func_decl * mk_reduction(ptr_vector & decls, decl_kind k, char const * name, unsigned bv_size); func_decl * mk_comp(unsigned bv_size); bool get_bv_size(sort * t, int & result); @@ -490,9 +517,19 @@ public: app * mk_bv2int(expr* e); + // TODO: all these binary ops commute (right?) but it'd be more logical to swap `n` & `m` in the `return` app * mk_bvsmul_no_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_NO_OVFL, n, m); } app * mk_bvsmul_no_udfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_NO_UDFL, n, m); } app * mk_bvumul_no_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUMUL_NO_OVFL, n, m); } + app * mk_bvsmul_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_OVFL, n, m); } + app * mk_bvumul_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUMUL_OVFL, n, m); } + app * mk_bvsdiv_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSDIV_OVFL, m, n); } + app * mk_bvneg_ovfl(expr* m) { return m_manager.mk_app(get_fid(), OP_BNEG_OVFL, m); } + app * mk_bvuadd_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUADD_OVFL, n, m); } + app * mk_bvsadd_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSADD_OVFL, n, m); } + app * mk_bvusub_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUSUB_OVFL, m, n); } + app * mk_bvssub_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSSUB_OVFL, m, n); } + app * mk_bit2bool(expr* e, unsigned idx) { parameter p(idx); return m_manager.mk_app(get_fid(), OP_BIT2BOOL, 1, &p, 1, &e); } private: diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 5f76d3fdd..751608e12 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -93,6 +93,10 @@ br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons case OP_BNEG: SASSERT(num_args == 1); return mk_uminus(args[0], result); + case OP_BNEG_OVFL: + SASSERT(num_args == 1); + return mk_bvneg_overflow(args[0], result); + case OP_BSHL: SASSERT(num_args == 2); return mk_bv_shl(args[0], args[1], result); @@ -199,6 +203,20 @@ br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons return mk_bvsmul_no_overflow(num_args, args, false, result); case OP_BUMUL_NO_OVFL: return mk_bvumul_no_overflow(num_args, args, result); + case OP_BSMUL_OVFL: + return mk_bvsmul_overflow(num_args, args, result); + case OP_BUMUL_OVFL: + return mk_bvumul_overflow(num_args, args, result); + case OP_BSDIV_OVFL: + return mk_bvsdiv_overflow(num_args, args, result); + case OP_BUADD_OVFL: + return mk_bvuadd_overflow(num_args, args, result); + case OP_BSADD_OVFL: + return mk_bvsadd_over_underflow(num_args, args, result); + case OP_BUSUB_OVFL: + return mk_bvusub_underflow(num_args, args, result); + case OP_BSSUB_OVFL: + return mk_bvssub_overflow(num_args, args, result); default: return BR_FAILED; } @@ -2921,6 +2939,21 @@ br_status bv_rewriter::mk_distinct(unsigned num_args, expr * const * args, expr_ return BR_DONE; } +br_status bv_rewriter::mk_bvsmul_overflow(unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 2); + result = m.mk_or( + m.mk_not(m_util.mk_bvsmul_no_ovfl(args[0], args[1])), + m.mk_not(m_util.mk_bvsmul_no_udfl(args[0], args[1])) + ); + return BR_REWRITE_FULL; +} + +br_status bv_rewriter::mk_bvumul_overflow(unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 2); + result = m.mk_not(m_util.mk_bvumul_no_ovfl(args[0], args[1])); + return BR_REWRITE2; +} + br_status bv_rewriter::mk_bvsmul_no_overflow(unsigned num, expr * const * args, bool is_overflow, expr_ref & result) { SASSERT(num == 2); unsigned bv_sz; @@ -2980,5 +3013,95 @@ br_status bv_rewriter::mk_bvumul_no_overflow(unsigned num, expr * const * args, return BR_FAILED; } +br_status bv_rewriter::mk_bvneg_overflow(expr * const arg, expr_ref & result) { + unsigned int sz = get_bv_size(arg); + auto maxUnsigned = mk_numeral(rational::power_of_two(sz)-1, sz); + result = m.mk_eq(arg, maxUnsigned); + return BR_REWRITE3; +} + +br_status bv_rewriter::mk_bvuadd_overflow(unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 2); + SASSERT(get_bv_size(args[0]) == get_bv_size(args[1])); + unsigned sz = get_bv_size(args[0]); + auto a1 = mk_zero_extend(1, args[0]); + auto a2 = mk_zero_extend(1, args[1]); + auto r = mk_bv_add(a1, a2); + auto extract = m_mk_extract(sz, sz, r); + result = m.mk_eq(extract, mk_one(1)); + return BR_REWRITE_FULL; +} + +br_status bv_rewriter::mk_bvsadd_overflow(unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 2); + SASSERT(get_bv_size(args[0]) == get_bv_size(args[1])); + unsigned sz = get_bv_size(args[0]); + auto zero = mk_zero(sz); + auto r = mk_bv_add(args[0], args[1]); + auto l1 = m_util.mk_slt(zero, args[0]); + auto l2 = m_util.mk_slt(zero, args[1]); + auto args_pos = m.mk_and(l1, l2); + auto non_pos_sum = m_util.mk_sle(r, zero); + result = m.mk_and(args_pos, non_pos_sum); + return BR_REWRITE_FULL; +} + +br_status bv_rewriter::mk_bvsadd_underflow(unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 2); + SASSERT(get_bv_size(args[0]) == get_bv_size(args[1])); + unsigned sz = get_bv_size(args[0]); + auto zero = mk_zero(sz); + auto r = mk_bv_add(args[0], args[1]); + auto l1 = m_util.mk_slt(args[0], zero); + auto l2 = m_util.mk_slt(args[1], zero); + auto args_neg = m.mk_and(l1, l2); + expr_ref non_neg_sum{m}; + auto res_rewrite = mk_sge(r, zero, non_neg_sum); + SASSERT(res_rewrite != BR_FAILED); (void)res_rewrite; + result = m.mk_and(args_neg, non_neg_sum); + return BR_REWRITE_FULL; +} + +br_status bv_rewriter::mk_bvsadd_over_underflow(unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 2); + SASSERT(get_bv_size(args[0]) == get_bv_size(args[1])); + expr_ref l1{m}; + expr_ref l2{m}; + (void)mk_bvsadd_overflow(2, args, l1); + (void)mk_bvsadd_underflow(2, args, l2); + result = m.mk_or(l1, l2); + return BR_REWRITE_FULL; +} + +br_status bv_rewriter::mk_bvusub_underflow(unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 2); + SASSERT(get_bv_size(args[0]) == get_bv_size(args[1])); + br_status status = mk_ult(args[0], args[1], result); + SASSERT(status != BR_FAILED); + return status; +} + +br_status bv_rewriter::mk_bvssub_overflow(unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 2); + SASSERT(get_bv_size(args[0]) == get_bv_size(args[1])); + auto sz = get_bv_size(args[0]); + auto minSigned = mk_numeral(-rational::power_of_two(sz-1), sz); + expr_ref bvsaddo {m}; + expr * args2[2] = { args[0], m_util.mk_bv_neg(args[1]) }; + auto bvsaddo_stat = mk_bvsadd_overflow(2, args2, bvsaddo); + SASSERT(bvsaddo_stat != BR_FAILED); (void)bvsaddo_stat; + auto first_arg_ge_zero = m_util.mk_sle(mk_zero(sz), args[0]); + result = m.mk_ite(m.mk_eq(args[1], minSigned), first_arg_ge_zero, bvsaddo); + return BR_REWRITE_FULL; +} +br_status bv_rewriter::mk_bvsdiv_overflow(unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 2); + SASSERT(get_bv_size(args[0]) == get_bv_size(args[1])); + auto sz = get_bv_size(args[1]); + auto minSigned = mk_numeral(-rational::power_of_two(sz-1), sz); + auto minusOne = mk_numeral(rational::power_of_two(sz) - 1, sz); + result = m.mk_and(m.mk_eq(args[0], minSigned), m.mk_eq(args[1], minusOne)); + return BR_REWRITE_FULL; +} template class poly_rewriter; diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h index 25bd65b61..09e7996c2 100644 --- a/src/ast/rewriter/bv_rewriter.h +++ b/src/ast/rewriter/bv_rewriter.h @@ -139,6 +139,22 @@ class bv_rewriter : public poly_rewriter { br_status mk_mkbv(unsigned num, expr * const * args, expr_ref & result); br_status mk_bvsmul_no_overflow(unsigned num, expr * const * args, bool is_overflow, expr_ref & result); br_status mk_bvumul_no_overflow(unsigned num, expr * const * args, expr_ref & result); + + br_status mk_bvsmul_overflow(unsigned num, expr * const * args, expr_ref & result); + br_status mk_bvumul_overflow(unsigned num, expr * const * args, expr_ref & result); + + br_status mk_bvsdiv_overflow(unsigned num, expr * const * args, expr_ref & result); + + br_status mk_bvneg_overflow(expr * const arg, expr_ref & result); + + br_status mk_bvuadd_overflow(unsigned num, expr * const * args, expr_ref & result); + br_status mk_bvsadd_overflow(unsigned num, expr * const * args, expr_ref & result); + br_status mk_bvsadd_underflow(unsigned num, expr * const * args, expr_ref & result); + br_status mk_bvsadd_over_underflow(unsigned num, expr * const * args, expr_ref & result); + + br_status mk_bvusub_underflow(unsigned num, expr * const * args, expr_ref & result); + br_status mk_bvssub_overflow(unsigned num, expr * const * args, expr_ref & result); + bool is_minus_one_times_t(expr * arg); void mk_t1_add_t2_eq_c(expr * t1, expr * t2, expr * c, expr_ref & result); From f6ab5a61ac8306a78e09a8a55110c6a125bc8652 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 9 May 2023 13:48:28 -0700 Subject: [PATCH 2/9] reformat code to remove brackets --- src/smt/proto_model/proto_model.cpp | 46 ++++++++++++----------------- 1 file changed, 19 insertions(+), 27 deletions(-) diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp index d61bcf028..4470f9cb8 100644 --- a/src/smt/proto_model/proto_model.cpp +++ b/src/smt/proto_model/proto_model.cpp @@ -288,42 +288,33 @@ bool proto_model::is_finite(sort * s) const { } expr * proto_model::get_some_value(sort * s) { - if (m.is_uninterp(s)) { - return m_user_sort_factory->get_some_value(s); - } - else if (value_factory * f = get_factory(s->get_family_id())) { - return f->get_some_value(s); - } - else { + if (m.is_uninterp(s)) + return m_user_sort_factory->get_some_value(s); + else if (value_factory * f = get_factory(s->get_family_id())) + return f->get_some_value(s); + else // there is no factory for the family id, then assume s is uninterpreted. - return m_user_sort_factory->get_some_value(s); - } + return m_user_sort_factory->get_some_value(s); } bool proto_model::get_some_values(sort * s, expr_ref & v1, expr_ref & v2) { - if (m.is_uninterp(s)) { - return m_user_sort_factory->get_some_values(s, v1, v2); - } - else if (value_factory * f = get_factory(s->get_family_id())) { - return f->get_some_values(s, v1, v2); - } - else { - return false; - } + if (m.is_uninterp(s)) + return m_user_sort_factory->get_some_values(s, v1, v2); + else if (value_factory * f = get_factory(s->get_family_id())) + return f->get_some_values(s, v1, v2); + else + return false; } expr * proto_model::get_fresh_value(sort * s) { - if (m.is_uninterp(s)) { - return m_user_sort_factory->get_fresh_value(s); - } - else if (value_factory * f = get_factory(s->get_family_id())) { - return f->get_fresh_value(s); - } - else { + if (m.is_uninterp(s)) + return m_user_sort_factory->get_fresh_value(s); + else if (value_factory * f = get_factory(s->get_family_id())) + return f->get_fresh_value(s); + else // Use user_sort_factory if the theory has no support for model construnction. // This is needed when dummy theories are used for arithmetic or arrays. - return m_user_sort_factory->get_fresh_value(s); - } + return m_user_sort_factory->get_fresh_value(s); } void proto_model::register_value(expr * n) { @@ -354,6 +345,7 @@ void proto_model::compress() { void proto_model::complete_partial_func(func_decl * f, bool use_fresh) { func_interp * fi = get_func_interp(f); if (fi && fi->is_partial()) { + verbose_stream() << "complete " << f->get_name() << " " << use_fresh << "\n"; expr * else_value; if (use_fresh) { else_value = get_fresh_value(f->get_range()); From 046b80f6a43af5ceff96dfc7114088aa625319b2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 May 2023 12:30:57 -0700 Subject: [PATCH 3/9] remove output Signed-off-by: Nikolaj Bjorner --- src/smt/proto_model/proto_model.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp index 4470f9cb8..f79f7851f 100644 --- a/src/smt/proto_model/proto_model.cpp +++ b/src/smt/proto_model/proto_model.cpp @@ -345,7 +345,6 @@ void proto_model::compress() { void proto_model::complete_partial_func(func_decl * f, bool use_fresh) { func_interp * fi = get_func_interp(f); if (fi && fi->is_partial()) { - verbose_stream() << "complete " << f->get_name() << " " << use_fresh << "\n"; expr * else_value; if (use_fresh) { else_value = get_fresh_value(f->get_range()); From ba911009e4fe9a823564bdf924cf559065739842 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 May 2023 16:54:40 -0700 Subject: [PATCH 4/9] disable publish Signed-off-by: Nikolaj Bjorner --- scripts/release.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/release.yml b/scripts/release.yml index 7d3ec1085..9a3fcae8c 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -558,7 +558,7 @@ stages: # Enable on release: - job: PyPIPublish - condition: eq(1,1) + condition: eq(1,0) displayName: "Publish to PyPI" pool: vmImage: "ubuntu-latest" From e417f7d78509b2d0c9ebc911fee7632e6ef546b6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 12 May 2023 12:59:04 -0700 Subject: [PATCH 5/9] updated release notes for 12.2 Signed-off-by: Nikolaj Bjorner --- RELEASE_NOTES.md | 4 ++++ scripts/release.yml | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index 6cac7cc49..68228df40 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -27,6 +27,10 @@ Version 4.12.2 and `elim-predicates` that go beyond incremental pre-processing used internally. The advantage of using `solve-eqs` during pre-processing can be significant. Incremental pre-processing simplification using `solve-eqs` and other simplifiers that change interpretations was not possible before. +- Optimize added to JS API, thanks to gbagan +- SMTLIB2 proposal for bit-vector overflow predicates added, thanks to aehyvari +- bug fixes, thanks to Clemens Eisenhofer, hgvk94, Lev Nachmanson, and others + Version 4.12.1 ============== diff --git a/scripts/release.yml b/scripts/release.yml index 9a3fcae8c..7d3ec1085 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -558,7 +558,7 @@ stages: # Enable on release: - job: PyPIPublish - condition: eq(1,0) + condition: eq(1,1) displayName: "Publish to PyPI" pool: vmImage: "ubuntu-latest" From f928b4460665410c83fbe2db2f202cba868fec56 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 12 May 2023 14:53:52 -0700 Subject: [PATCH 6/9] update version number Signed-off-by: Nikolaj Bjorner --- CMakeLists.txt | 2 +- RELEASE_NOTES.md | 3 +++ scripts/mk_project.py | 2 +- scripts/nightly.yaml | 2 +- scripts/release.yml | 2 +- 5 files changed, 7 insertions(+), 4 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 9299efe25..9164e8e28 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -2,7 +2,7 @@ cmake_minimum_required(VERSION 3.4) set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake") -project(Z3 VERSION 4.12.2.0 LANGUAGES CXX) +project(Z3 VERSION 4.12.3.0 LANGUAGES CXX) ################################################################################ # Project version diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index 68228df40..9e007d1a1 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -10,6 +10,9 @@ Version 4.next - native word level bit-vector solving. - introduction of simple induction lemmas to handle a limited repertoire of induction proofs. +Version 4.12.3 +============== + Version 4.12.2 ============== diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 44e436daf..876e0fd21 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -8,7 +8,7 @@ from mk_util import * def init_version(): - set_version(4, 12, 2, 0) # express a default build version or pick up ci build version + set_version(4, 12, 3, 0) # express a default build version or pick up ci build version # Z3 Project definition def init_project_def(): diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index 4aeb44b35..f4573877e 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -1,7 +1,7 @@ variables: Major: '4' Minor: '12' - Patch: '2' + Patch: '3' AssemblyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId) NightlyVersion: $(AssemblyVersion)-$(Build.DefinitionName) diff --git a/scripts/release.yml b/scripts/release.yml index 7d3ec1085..a1306d87f 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -6,7 +6,7 @@ trigger: none variables: - ReleaseVersion: '4.12.2' + ReleaseVersion: '4.12.3' stages: From 520e692a43c41e8981eb091494bef0297ecbe3c6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tomasz=20K=C5=82oczko?= <31284574+kloczek@users.noreply.github.com> Date: Sat, 13 May 2023 17:37:35 +0100 Subject: [PATCH 7/9] Fix building with gcc 13 (#6723) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Trivial fix to build with gcc 13 reported in #6722. Signed-off-by: Tomasz Kłoczko --- src/util/tptr.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/util/tptr.h b/src/util/tptr.h index 6213b2efa..2a35af535 100644 --- a/src/util/tptr.h +++ b/src/util/tptr.h @@ -20,6 +20,7 @@ Revision History: #pragma once #include "util/machine.h" +#include #define TAG_SHIFT PTR_ALIGNMENT #define ALIGNMENT_VALUE (1 << PTR_ALIGNMENT) From c9d8e646ed505a9cd4c84b2cb31d846b8588109f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Micha=C5=82=20G=C3=B3rny?= Date: Sat, 13 May 2023 18:37:57 +0200 Subject: [PATCH 8/9] fix missing include (#6720) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Fix missing include in src/util/tptr.h that causes build failure with GCC 13: ``` In file included from /tmp/z3/src/util/region.cpp:53: /tmp/z3/src/util/region.cpp: In member function ‘void* region::allocate(size_t)’: /tmp/z3/src/util/tptr.h:29:62: error: ‘uintptr_t’ does not name a type 29 | #define ALIGN(T, PTR) reinterpret_cast(((reinterpret_cast(PTR) >> PTR_ALIGNMENT) + \ | ^~~~~~~~~ /tmp/z3/src/util/region.cpp:82:22: note: in expansion of macro ‘ALIGN’ 82 | m_curr_ptr = ALIGN(char *, new_curr_ptr); | ^~~~~ /tmp/z3/src/util/region.cpp:57:1: note: ‘uintptr_t’ is defined in header ‘’; did you forget to ‘#include ’? 56 | #include "util/page.h" +++ |+#include 57 | ``` --- src/util/tptr.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/util/tptr.h b/src/util/tptr.h index 2a35af535..50e9417fe 100644 --- a/src/util/tptr.h +++ b/src/util/tptr.h @@ -19,6 +19,7 @@ Revision History: #pragma once +#include #include "util/machine.h" #include From 06ea765b8229ea784fe6f805379c9e508eb9fed6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 13 May 2023 09:46:49 -0700 Subject: [PATCH 9/9] fix #6721 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/elim_bounds.cpp | 1 + src/ast/rewriter/push_app_ite.cpp | 1 + 2 files changed, 2 insertions(+) diff --git a/src/ast/rewriter/elim_bounds.cpp b/src/ast/rewriter/elim_bounds.cpp index de23537ad..27c34463d 100644 --- a/src/ast/rewriter/elim_bounds.cpp +++ b/src/ast/rewriter/elim_bounds.cpp @@ -22,6 +22,7 @@ Revision History: #include "ast/used_vars.h" #include "util/obj_hashtable.h" +#include "ast/rewriter/rewriter_def.h" #include "ast/rewriter/var_subst.h" #include "ast/rewriter/elim_bounds.h" #include "ast/ast_pp.h" diff --git a/src/ast/rewriter/push_app_ite.cpp b/src/ast/rewriter/push_app_ite.cpp index 0282aa602..b993c29a5 100644 --- a/src/ast/rewriter/push_app_ite.cpp +++ b/src/ast/rewriter/push_app_ite.cpp @@ -18,6 +18,7 @@ Revision History: --*/ #include "ast/rewriter/push_app_ite.h" +#include "ast/rewriter/rewriter_def.h" #include "ast/ast_pp.h"