mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

add comments for API versions of bit-vector overflow/underflow checks for #7011

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-11-28 13:36:41 -08:00
parent f90b10a0c8
commit f36f21fa8c
1 changed files with 10 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/api/api_bv.cpp
View file

@ -227,6 +227,9 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2) {
Z3_TRY;
RESET_ERROR_CODE();
// l1 := t1 <s 0
// l2 := t2 <s 0
// l1 & l2 => t1 + t2 <s 0
Z3_ast zero = Z3_mk_int(c, 0, Z3_get_sort(c, t1));
Z3_inc_ref(c, zero);
Z3_ast r = Z3_mk_bvadd(c, t1, t2);
@ -255,6 +258,10 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
Z3_ast Z3_API Z3_mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2) {
Z3_TRY;
RESET_ERROR_CODE();
// x := t2 = min_int
// y := t1 <s 0
// z := no_overflow(t1 + -t2)
// if x y z
Z3_ast minus_t2 = Z3_mk_bvneg(c, t2);
Z3_inc_ref(c, minus_t2);
Z3_sort s = Z3_get_sort(c, t2);
@ -284,6 +291,9 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
Z3_TRY;
RESET_ERROR_CODE();
if (is_signed) {
// x := 0 <s -t2
// y := no_underflow(x + -t2)
// x => y
Z3_ast zero = Z3_mk_int(c, 0, Z3_get_sort(c, t1));
Z3_inc_ref(c, zero);
Z3_ast minus_t2 = Z3_mk_bvneg(c, t2);