# deal-solver
[z3](https://github.com/Z3Prover/z3)-powered solver (theorem prover) for [deal](https://github.com/life4/deal).
```bash
python3 -m pip install deal-solver
```
## CLI
For CLI usage, see the [deal documentation](https://deal.readthedocs.io/). 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](./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.
Raw data
{
"_id": null,
"home_page": "https://github.com/life4/deal-solver",
"name": "deal-solver",
"maintainer": null,
"docs_url": null,
"requires_python": ">=3.7",
"maintainer_email": null,
"keywords": "deal,contracts,verification",
"author": "Gram",
"author_email": "gram@orsinium.dev",
"download_url": "https://files.pythonhosted.org/packages/6c/47/af5b3cb61f455d8102a6af1e5b11ef515e0073d0ec9a3cc0218ac87e6fba/deal_solver-0.1.2.tar.gz",
"platform": null,
"description": "# deal-solver\n\n[z3](https://github.com/Z3Prover/z3)-powered solver (theorem prover) for [deal](https://github.com/life4/deal).\n\n```bash\npython3 -m pip install deal-solver\n```\n\n## CLI\n\nFor CLI usage, see the [deal documentation](https://deal.readthedocs.io/). The solver doesn't provide a CLI on its own.\n\n## API\n\nDeal-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](./tests/helpers.py).\n\n## The project state\n\nThis 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.\n",
"bugtrack_url": null,
"license": "MIT",
"summary": "z3-powered solver (theorem prover) for deal.",
"version": "0.1.2",
"project_urls": {
"Homepage": "https://github.com/life4/deal-solver"
},
"split_keywords": [
"deal",
"contracts",
"verification"
],
"urls": [
{
"comment_text": null,
"digests": {
"blake2b_256": "8e7f7716ba99fd0199a6c33d12ae537866da4dcabc61668091875a10343b8b41",
"md5": "cefe396297d8c4cce0a3bf81af52c80e",
"sha256": "0d657a28368acd416f4031d3f42a86cc7db1b6ce3c08621e9895c6f41a85f3ec"
},
"downloads": -1,
"filename": "deal_solver-0.1.2-py3-none-any.whl",
"has_sig": false,
"md5_digest": "cefe396297d8c4cce0a3bf81af52c80e",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": ">=3.7",
"size": 47958,
"upload_time": "2023-09-28T13:31:20",
"upload_time_iso_8601": "2023-09-28T13:31:20.901656Z",
"url": "https://files.pythonhosted.org/packages/8e/7f/7716ba99fd0199a6c33d12ae537866da4dcabc61668091875a10343b8b41/deal_solver-0.1.2-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": null,
"digests": {
"blake2b_256": "6c47af5b3cb61f455d8102a6af1e5b11ef515e0073d0ec9a3cc0218ac87e6fba",
"md5": "34a57cec93d2e6301c5585739407e587",
"sha256": "7feac330346fd28f41b04ad62da9b1f1419aa7d9e37eaa4e5098de9ff2d5d66f"
},
"downloads": -1,
"filename": "deal_solver-0.1.2.tar.gz",
"has_sig": false,
"md5_digest": "34a57cec93d2e6301c5585739407e587",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.7",
"size": 46788,
"upload_time": "2023-09-28T13:31:23",
"upload_time_iso_8601": "2023-09-28T13:31:23.226309Z",
"url": "https://files.pythonhosted.org/packages/6c/47/af5b3cb61f455d8102a6af1e5b11ef515e0073d0ec9a3cc0218ac87e6fba/deal_solver-0.1.2.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2023-09-28 13:31:23",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "life4",
"github_project": "deal-solver",
"travis_ci": false,
"coveralls": false,
"github_actions": true,
"lcname": "deal-solver"
}
JSON
