Metadata-Version: 2.4
Name: bitwuzla-pythonic
Version: 1.0.0
Summary: Pythonic interface for the Bitwuzla SMT solver
Project-URL: Homepage, https://github.com/es3n1n/bitwuzla-pythonic
Project-URL: Repository, https://github.com/es3n1n/bitwuzla-pythonic
Author: es3n1n
License-Expression: MIT
License-File: LICENSE
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Science/Research
Classifier: License :: OSI Approved :: MIT License
Classifier: Programming Language :: Python :: 3
Classifier: Topic :: Scientific/Engineering
Classifier: Topic :: Software Development :: Libraries :: Python Modules
Requires-Python: >=3.8
Requires-Dist: bitwuzla>=0.9.0
Description-Content-Type: text/markdown

# bitwuzla-pythonic

Pythonic interface for the [Bitwuzla](https://bitwuzla.github.io/) SMT solver.

## Installation

```bash
pip install bitwuzla-pythonic
```

## Usage

Same as `z3py` / `cvc5.pythonic`

```python
from bitwuzla_pythonic import *

s = Solver()
a = BitVec('a', 32)
b = BitVec('b', 32)

s.add((a * b ^ 1337) == 291710820)

assert s.check() == sat
m = s.model()
print(m)
# [a = 4003257763, b = 4294967295]
```

## Acknowledgements

- [cvc5/cvc5_pythonic_api](https://github.com/cvc5/cvc5_pythonic_api) - Reference
- [Z3Prover/z3](https://github.com/Z3Prover/z3) - Reference
- `opus4.6` - Authored most of the code in this repo :upside_down:
