mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-30 04:15:51 +00:00
Code Activity

fix argument validation to new overflow/underflow functions #1364

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

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

@ -3995,59 +3995,52 @@ def BVRedOr(a):
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")
_check_bv_args(a, b)
a, b = _coerce_exprs(a, b)
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")
_check_bv_args(a, b)
a, b = _coerce_exprs(a, b)
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")
_check_bv_args(a, b)
a, b = _coerce_exprs(a, b)
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")
_check_bv_args(a, b)
a, b = _coerce_exprs(a, b)
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")
_check_bv_args(a, b)
a, b = _coerce_exprs(a, b)
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")
_z3_assert(is_bv(a), "Argument should be a bit-vector")
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")
_check_bv_args(a, b)
a, b = _coerce_exprs(a, b)
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")
_check_bv_args(a, b)
a, b = _coerce_exprs(a, b)
return BoolRef(Z3_mk_bvmul_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)