From 7e3dfb46173e4d7e2e69bbead080cb3881ca0875 Mon Sep 17 00:00:00 2001 From: Manuel Jacob Date: Fri, 13 May 2016 23:11:15 +0200 Subject: [PATCH] Expose Z3_mk_bv2int's is_signed parameter in Python API. --- src/api/python/z3.py | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 848883ba3..624cd18f2 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -3468,7 +3468,7 @@ def is_bv_value(a): """ return is_bv(a) and _is_numeral(a.ctx, a.as_ast()) -def BV2Int(a): +def BV2Int(a, is_signed=False): """Return the Z3 expression BV2Int(a). >>> b = BitVec('b', 3) @@ -3477,6 +3477,10 @@ def BV2Int(a): >>> x = Int('x') >>> x > BV2Int(b) x > BV2Int(b) + >>> x > BV2Int(b, is_signed=False) + x > BV2Int(b) + >>> x > BV2Int(b, is_signed=True) + x > If(b < 0, BV2Int(b) - 8, BV2Int(b)) >>> solve(x > BV2Int(b), b == 1, x < 3) [b = 1, x = 2] """ @@ -3484,7 +3488,7 @@ def BV2Int(a): _z3_assert(is_bv(a), "Z3 bit-vector expression expected") ctx = a.ctx ## investigate problem with bv2int - return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), 0), ctx) + return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), is_signed), ctx) def BitVecSort(sz, ctx=None): """Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used.