A well-typed library for symbolic bitvectors

Navigation

Verified details

These details have been verified by PyPI
Maintainers
Avatar for btidor from gravatar.com btidor

Unverified details

These details have not been verified by PyPI
Project links
GitHub Statistics

View statistics for this project via Libraries.io, or by using our public dataset on Google BigQuery

Meta

License: MIT License

Requires: Python >=3.8

Project description

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

Project homepage →

Project details

Verified details

These details have been verified by PyPI
Maintainers
Avatar for btidor from gravatar.com btidor

Unverified details

These details have not been verified by PyPI
Project links
GitHub Statistics

View statistics for this project via Libraries.io, or by using our public dataset on Google BigQuery

Meta

License: MIT License

Requires: Python >=3.8


Release history Release notifications | RSS feed

This version

1.3.0

1.2.0

1.0.0

Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

zbitvector-1.3.0.tar.gz (60.4 kB view hashes)

Uploaded Source

Built Distributions

zbitvector-1.3.0-pp310-pypy310_pp73-manylinux_2_17_x86_64.manylinux2014_x86_64.whl (1.6 MB view hashes)

Uploaded PyPy manylinux: glibc 2.17+ x86-64

zbitvector-1.3.0-pp310-pypy310_pp73-manylinux_2_17_aarch64.manylinux2014_aarch64.whl (1.4 MB view hashes)

Uploaded PyPy manylinux: glibc 2.17+ ARM64

zbitvector-1.3.0-pp310-pypy310_pp73-macosx_11_0_arm64.whl (1.3 MB view hashes)

Uploaded PyPy macOS 11.0+ ARM64

zbitvector-1.3.0-pp310-pypy310_pp73-macosx_10_9_x86_64.whl (1.5 MB view hashes)

Uploaded PyPy macOS 10.9+ x86-64

zbitvector-1.3.0-pp39-pypy39_pp73-manylinux_2_17_x86_64.manylinux2014_x86_64.whl (1.6 MB view hashes)

Uploaded PyPy manylinux: glibc 2.17+ x86-64

zbitvector-1.3.0-pp39-pypy39_pp73-manylinux_2_17_aarch64.manylinux2014_aarch64.whl (1.4 MB view hashes)

Uploaded PyPy manylinux: glibc 2.17+ ARM64

zbitvector-1.3.0-pp39-pypy39_pp73-macosx_11_0_arm64.whl (1.3 MB view hashes)

Uploaded PyPy macOS 11.0+ ARM64

zbitvector-1.3.0-pp39-pypy39_pp73-macosx_10_9_x86_64.whl (1.5 MB view hashes)

Uploaded PyPy macOS 10.9+ x86-64

zbitvector-1.3.0-pp38-pypy38_pp73-manylinux_2_17_x86_64.manylinux2014_x86_64.whl (1.6 MB view hashes)

Uploaded PyPy manylinux: glibc 2.17+ x86-64

zbitvector-1.3.0-pp38-pypy38_pp73-manylinux_2_17_aarch64.manylinux2014_aarch64.whl (1.4 MB view hashes)

Uploaded PyPy manylinux: glibc 2.17+ ARM64

zbitvector-1.3.0-pp38-pypy38_pp73-macosx_11_0_arm64.whl (1.3 MB view hashes)

Uploaded PyPy macOS 11.0+ ARM64

zbitvector-1.3.0-pp38-pypy38_pp73-macosx_10_9_x86_64.whl (1.5 MB view hashes)

Uploaded PyPy macOS 10.9+ x86-64

zbitvector-1.3.0-cp312-cp312-musllinux_1_1_x86_64.whl (2.7 MB view hashes)

Uploaded CPython 3.12 musllinux: musl 1.1+ x86-64

zbitvector-1.3.0-cp312-cp312-musllinux_1_1_aarch64.whl (2.6 MB view hashes)

Uploaded CPython 3.12 musllinux: musl 1.1+ ARM64

zbitvector-1.3.0-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl (2.2 MB view hashes)

Uploaded CPython 3.12 manylinux: glibc 2.17+ x86-64

zbitvector-1.3.0-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl (2.0 MB view hashes)

Uploaded CPython 3.12 manylinux: glibc 2.17+ ARM64

zbitvector-1.3.0-cp312-cp312-macosx_11_0_arm64.whl (1.3 MB view hashes)

Uploaded CPython 3.12 macOS 11.0+ ARM64

zbitvector-1.3.0-cp312-cp312-macosx_10_9_x86_64.whl (1.5 MB view hashes)

Uploaded CPython 3.12 macOS 10.9+ x86-64

zbitvector-1.3.0-cp311-cp311-musllinux_1_1_x86_64.whl (2.7 MB view hashes)

Uploaded CPython 3.11 musllinux: musl 1.1+ x86-64

zbitvector-1.3.0-cp311-cp311-musllinux_1_1_aarch64.whl (2.6 MB view hashes)

Uploaded CPython 3.11 musllinux: musl 1.1+ ARM64

zbitvector-1.3.0-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl (2.2 MB view hashes)

Uploaded CPython 3.11 manylinux: glibc 2.17+ x86-64

zbitvector-1.3.0-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl (2.0 MB view hashes)

Uploaded CPython 3.11 manylinux: glibc 2.17+ ARM64

zbitvector-1.3.0-cp311-cp311-macosx_11_0_arm64.whl (1.3 MB view hashes)

Uploaded CPython 3.11 macOS 11.0+ ARM64

zbitvector-1.3.0-cp311-cp311-macosx_10_9_x86_64.whl (1.5 MB view hashes)

Uploaded CPython 3.11 macOS 10.9+ x86-64

zbitvector-1.3.0-cp310-cp310-musllinux_1_1_x86_64.whl (2.7 MB view hashes)

Uploaded CPython 3.10 musllinux: musl 1.1+ x86-64

zbitvector-1.3.0-cp310-cp310-musllinux_1_1_aarch64.whl (2.5 MB view hashes)

Uploaded CPython 3.10 musllinux: musl 1.1+ ARM64

zbitvector-1.3.0-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl (2.1 MB view hashes)

Uploaded CPython 3.10 manylinux: glibc 2.17+ x86-64

zbitvector-1.3.0-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl (2.0 MB view hashes)

Uploaded CPython 3.10 manylinux: glibc 2.17+ ARM64

zbitvector-1.3.0-cp310-cp310-macosx_11_0_arm64.whl (1.3 MB view hashes)

Uploaded CPython 3.10 macOS 11.0+ ARM64

zbitvector-1.3.0-cp310-cp310-macosx_10_9_x86_64.whl (1.5 MB view hashes)

Uploaded CPython 3.10 macOS 10.9+ x86-64

zbitvector-1.3.0-cp39-cp39-musllinux_1_1_x86_64.whl (2.7 MB view hashes)

Uploaded CPython 3.9 musllinux: musl 1.1+ x86-64

zbitvector-1.3.0-cp39-cp39-musllinux_1_1_aarch64.whl (2.5 MB view hashes)

Uploaded CPython 3.9 musllinux: musl 1.1+ ARM64

zbitvector-1.3.0-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl (2.1 MB view hashes)

Uploaded CPython 3.9 manylinux: glibc 2.17+ x86-64

zbitvector-1.3.0-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl (2.0 MB view hashes)

Uploaded CPython 3.9 manylinux: glibc 2.17+ ARM64

zbitvector-1.3.0-cp39-cp39-macosx_11_0_arm64.whl (1.3 MB view hashes)

Uploaded CPython 3.9 macOS 11.0+ ARM64

zbitvector-1.3.0-cp39-cp39-macosx_10_9_x86_64.whl (1.5 MB view hashes)

Uploaded CPython 3.9 macOS 10.9+ x86-64

zbitvector-1.3.0-cp38-cp38-musllinux_1_1_x86_64.whl (2.8 MB view hashes)

Uploaded CPython 3.8 musllinux: musl 1.1+ x86-64

zbitvector-1.3.0-cp38-cp38-musllinux_1_1_aarch64.whl (2.6 MB view hashes)

Uploaded CPython 3.8 musllinux: musl 1.1+ ARM64

zbitvector-1.3.0-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl (2.1 MB view hashes)

Uploaded CPython 3.8 manylinux: glibc 2.17+ x86-64

zbitvector-1.3.0-cp38-cp38-manylinux_2_17_aarch64.manylinux2014_aarch64.whl (2.0 MB view hashes)

Uploaded CPython 3.8 manylinux: glibc 2.17+ ARM64

zbitvector-1.3.0-cp38-cp38-macosx_11_0_arm64.whl (1.3 MB view hashes)

Uploaded CPython 3.8 macOS 11.0+ ARM64

zbitvector-1.3.0-cp38-cp38-macosx_10_9_x86_64.whl (1.5 MB view hashes)

Uploaded CPython 3.8 macOS 10.9+ x86-64

Supported by

AWS AWS Cloud computing and Security Sponsor Datadog Datadog Monitoring Fastly Fastly CDN Google Google Download Analytics Microsoft Microsoft PSF Sponsor Pingdom Pingdom Monitoring Sentry Sentry Error logging StatusPage StatusPage Status page