mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 09:26:15 +00:00
Code Activity

add Python facility for int2bv, fix #1398

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-12-18 12:20:44 -08:00
parent 63951b815d
commit 399b27fda3
1 changed files with 8 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -3568,6 +3568,14 @@ def BV2Int(a, is_signed=False):
## investigate problem with bv2int ## investigate problem with bv2int
return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), is_signed), ctx) return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), is_signed), ctx)
def Int2BV(a, num_bits):
"""Return the z3 expression Int2BV(a, num_bits).
It is a bit-vector of width num_bits and represents the
modulo of a by 2^num_bits
"""
ctx = a.ctx
return BitVecRef(Z3_mk_int2bv(ctx.ref(), num_bits, a.as_ast()), 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.