deal-solver0.1.2
deal-solver0.1.2
Published
z3-powered solver (theorem prover) for deal.
pip install deal-solver
Package Downloads
Authors
Project URLs
Requires Python
>=3.7
Dependencies
- astroid
- z3-solver
- flake8
; extra == "lint" - flake8-bugbear
; extra == "lint" - flake8-commas
; extra == "lint" - flake8-quotes
; extra == "lint" - isort
; extra == "lint" - unify
; extra == "lint" - mypy
>=0.910 ; extra == "lint" - hypothesis
; extra == "test" - pytest
; extra == "test" - pytest-cov
; extra == "test" - pytest-xdist
; extra == "test"
deal-solver
z3-powered solver (theorem prover) for deal.
python3 -m pip install deal-solver
CLI
For CLI usage, see the deal documentation. The solver doesn't provide a CLI on its own.
API
Deal-solver is created specifically for deal. So, if you want to use it with another tool, you have to mimic deal. It's not hard, though. See TestTheorem implementation in tests/helpers.py.
The project state
This is an experimental project. it supports only limited subset of syntax an types. Still, it works for some simple cases. So, give it a try, it is free.