mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 03:07:07 +00:00
Code Activity

add bit-vector over/underflow checks to Python API, #1364

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-21 15:14:49 -08:00
parent d520557ad9
commit 18200f55ed
1 changed files with 59 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

59
src/api/python/z3/z3.py
View file

@ -3993,6 +3993,65 @@ def BVRedOr(a):
_z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression")
return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx)
def BVAddNoOverflow(a, b, signed):
"""A predicate the determines that bit-vector addition does not overflow"""
if __debug__:
_z3_assert(is_bv(a), "Arguments should be bit-vectors")
_z3_assert(is_bv(b), "Arguments should be bit-vectors")
return BoolRef(Z3_mk_bvadd_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
def BVAddNoUnderflow(a, b, signed):
"""A predicate the determines that signed bit-vector addition does not underflow"""
if __debug__:
_z3_assert(is_bv(a), "Arguments should be bit-vectors")
_z3_assert(is_bv(b), "Arguments should be bit-vectors")
return BoolRef(Z3_mk_bvadd_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
def BVSubNoOverflow(a, b):
"""A predicate the determines that bit-vector subtraction does not overflow"""
if __debug__:
_z3_assert(is_bv(a), "Arguments should be bit-vectors")
_z3_assert(is_bv(b), "Arguments should be bit-vectors")
return BoolRef(Z3_mk_bvsub_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
def BVSubNoUnderflow(a, b, signed):
"""A predicate the determines that bit-vector subtraction does not underflow"""
if __debug__:
_z3_assert(is_bv(a), "Arguments should be bit-vectors")
_z3_assert(is_bv(b), "Arguments should be bit-vectors")
return BoolRef(Z3_mk_bvsub_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
def BVSDivNoOverflow(a, b):
"""A predicate the determines that bit-vector signed division does not overflow"""
if __debug__:
_z3_assert(is_bv(a), "Arguments should be bit-vectors")
_z3_assert(is_bv(b), "Arguments should be bit-vectors")
return BoolRef(Z3_mk_bvsdiv_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
def BVSNegNoOverflow(a):
"""A predicate the determines that bit-vector unary negation does not overflow"""
if __debug__:
_z3_assert(is_bv(a), "Arguments should be bit-vectors")
return BoolRef(Z3_mk_bvneg_no_overflow(a.ctx_ref(), a.as_ast()), a.ctx)
def BVMulNoOverflow(a, b, signed):
"""A predicate the determines that bit-vector multiplication does not overflow"""
if __debug__:
_z3_assert(is_bv(a), "Arguments should be bit-vectors")
_z3_assert(is_bv(b), "Arguments should be bit-vectors")
return BoolRef(Z3_mk_bvmul_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
def BVMulNoUnderflow(a, b, signed):
"""A predicate the determines that bit-vector signed multiplication does not underflow"""
if __debug__:
_z3_assert(is_bv(a), "Arguments should be bit-vectors")
_z3_assert(is_bv(b), "Arguments should be bit-vectors")
return BoolRef(Z3_mk_bvmul_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
#########################################
#
# Arrays