zbitvector is an efficient, well-typed interface to the Z3 and Bitwuzla SMT solvers. It can be used to represent and manipulate symbolic expressions in the theory of fixed-sized bitvectors and arrays (QF_BVA).
import typing
import zbitvector
Uint8 = zbitvector.Uint[typing.Literal[8]]
Uint64 = zbitvector.Uint[typing.Literal[64]]
Uint64("X") + Uint64(1)
# => Uint64(`(bvadd X #x01)`)
Uint64("X") + Uint8(1)
# fails to typecheck
Features¶
Arrays:
>>> A = Array[Uint8, Uint64](Uint64(0)) >>> A[Uint8(1)] = Uint64(2)
Simplification:
>>> (Uint8(2) + Uint8(3)).reveal() 5
Solving:
>>> s = Solver() >>> s.add(Uint8("X") + Uint8(1) == Uint8(0)) >>> s.check() True
Model Evaluation:
>>> s.evaluate(Uint8("X")) 255
Installation¶
Pre-built binary wheels are available on PyPI:
pip install zbitvector
Wheels are built for the x86-64 and AArch64 architectures and support these operating systems:
macOS 10.9+
Linux with glibc 2.17+ (manylinux2014)
Linux with musl 1.1+ (musllinux_1_1)
zbitvector requires Python 3.8 or later.
To build from source, first build Bitwuzla using ./configure --shared
and install the library by running make install
.
Runtime Options¶
zbitvector uses the Bitwuzla solver by default, but can be configured to use Z3 by setting an environment variable:
pip install z3-solver
ZBITVECTOR_SOLVER=z3 python ...