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

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-05-16 16:17:18 +01:00
parent 99f5269b78 121f79b198
commit 85366f247f
3 changed files with 8 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
scripts/mk_unix_dist.py
View file

@ -58,7 +58,7 @@ def display_help():
# Parse configuration option for mk_make script # Parse configuration option for mk_make script
def parse_options(): def parse_options():
global FORCE_MK, JAVA_ENABLED, GIT_HASH global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED
path = BUILD_DIR path = BUILD_DIR
options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=', options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=',
'help', 'help',

2
scripts/mk_win_dist.py
View file

@ -63,7 +63,7 @@ def display_help():
# Parse configuration option for mk_make script # Parse configuration option for mk_make script
def parse_options(): def parse_options():
global FORCE_MK, JAVA_ENABLED, GIT_HASH global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED
path = BUILD_DIR path = BUILD_DIR
options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=', options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=',
'help', 'help',

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

@ -3468,7 +3468,7 @@ def is_bv_value(a):
""" """
return is_bv(a) and _is_numeral(a.ctx, a.as_ast()) 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). """Return the Z3 expression BV2Int(a).
>>> b = BitVec('b', 3) >>> b = BitVec('b', 3)
@ -3477,6 +3477,10 @@ def BV2Int(a):
>>> x = Int('x') >>> x = Int('x')
>>> x > BV2Int(b) >>> x > BV2Int(b)
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) >>> solve(x > BV2Int(b), b == 1, x < 3)
[b = 1, x = 2] [b = 1, x = 2]
""" """
@ -3484,7 +3488,7 @@ def BV2Int(a):
_z3_assert(is_bv(a), "Z3 bit-vector expression expected") _z3_assert(is_bv(a), "Z3 bit-vector expression expected")
ctx = a.ctx ctx = a.ctx
## investigate problem with bv2int ## 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): def BitVecSort(sz, ctx=None):
"""Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used. """Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used.