mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

z3.py: add overflow checks to PB API

Browse source
This commit is contained in:
Nuno Lopes 2018-06-07 15:40:04 +01:00
parent add8d26807
commit 9e916edcb0
1 changed files with 7 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -90,6 +90,9 @@ def _z3_assert(cond, msg):
if not cond:
raise Z3Exception(msg)
def _z3_check_cint_overflow(n, name):
_z3_assert(ctypes.c_int(n).value == n, name + " is too large")
def open_log(fname):
"""Log interaction to a file. This function must be invoked immediately after init(). """
Z3_open_log(fname)
@ -8128,6 +8131,7 @@ def _pb_args_coeffs(args, default_ctx = None):
_args, sz = _to_ast_array(args)
_coeffs = (ctypes.c_int * len(coeffs))()
for i in range(len(coeffs)):
_z3_check_cint_overflow(coeffs[i], "coefficient")
_coeffs[i] = coeffs[i]
return ctx, sz, _args, _coeffs
@ -8137,6 +8141,7 @@ def PbLe(args, k):
>>> a, b, c = Bools('a b c')
>>> f = PbLe(((a,1),(b,3),(c,2)), 3)
"""
_z3_check_cint_overflow(k, "k")
ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
return BoolRef(Z3_mk_pble(ctx.ref(), sz, _args, _coeffs, k), ctx)
@ -8146,6 +8151,7 @@ def PbGe(args, k):
>>> a, b, c = Bools('a b c')
>>> f = PbGe(((a,1),(b,3),(c,2)), 3)
"""
_z3_check_cint_overflow(k, "k")
ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
return BoolRef(Z3_mk_pbge(ctx.ref(), sz, _args, _coeffs, k), ctx)
@ -8155,6 +8161,7 @@ def PbEq(args, k, ctx = None):
>>> a, b, c = Bools('a b c')
>>> f = PbEq(((a,1),(b,3),(c,2)), 3)
"""
_z3_check_cint_overflow(k, "k")
ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
return BoolRef(Z3_mk_pbeq(ctx.ref(), sz, _args, _coeffs, k), ctx)