Implement bvsdivo

Z3Prover · May 9, 2023 · 846b0e0 · 846b0e0
1 parent a436c02
commit 846b0e0
Show file tree

Hide file tree

Showing 4 changed files with 22 additions and 0 deletions.
diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp
@@ -133,6 +133,8 @@ void bv_decl_plugin::finalize() {
     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);
     DEC_REF(m_bv_ashr);
@@ -354,6 +356,7 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned 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);
@@ -720,6 +723,7 @@ void bv_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const
     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
@@ -96,6 +96,8 @@ enum bv_op_kind {
     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
@@ -207,6 +209,8 @@ class bv_decl_plugin : public decl_plugin {
     ptr_vector<func_decl> m_bv_mul_ovfl;
     ptr_vector<func_decl> m_bv_smul_ovfl;
 
+    ptr_vector<func_decl> m_bv_sdiv_ovfl;
+
     ptr_vector<func_decl> m_bv_neg_ovfl;
 
     ptr_vector<func_decl> m_bv_uadd_ovfl;
@@ -519,6 +523,7 @@ class bv_util : public bv_recognizers {
     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); }

diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
@@ -207,6 +207,8 @@ br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
         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:
@@ -3092,5 +3094,14 @@ br_status bv_rewriter::mk_bvssub_overflow(unsigned num, expr * const * args, exp
     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<bv_rewriter_core>;
diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h
@@ -143,6 +143,8 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
     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);