# py-aiger-cnf
Python library to convert between AIGER and CNF
[](https://cloud.drone.io/mvcisback/py-aiger-cnf)
[](https://badge.fury.io/py/py-aiger-cnf)
[](https://opensource.org/licenses/MIT)
<!-- markdown-toc start - Don't edit this section. Run M-x markdown-toc-generate-toc again -->
**Table of Contents**
- [Installation](#installation)
- [Usage](#usage)
<!-- markdown-toc end -->
# Installation
If you just need to use `aiger_cnf`, you can just run:
`$ pip install py-aiger-cnf`
For developers, note that this project uses the
[poetry](https://poetry.eustace.io/) python package/dependency
management tool. Please familarize yourself with it and then
run:
`$ poetry install`
# Usage
The primary entry point for using `aiger_cnf` is the `aig2cnf`
function which, unsurprisingly, maps `AIG` objects to `CNF` objects.
```python
import aiger
from aiger_cnf import aig2cnf
x, y, z = map(aiger.atom, ('x', 'y', 'z'))
expr = (x & y) | ~z
cnf = aig2cnf(expr.aig)
```
Note that this library also supports `aiger` wrapper libraries so long
as they export a `.aig` attribute. Thus, could also
write:
```python
cnf = aig2cnf(expr)
```
The `CNF` object is a `NamedTuple` with the following three fields:
1. `clauses`: A list of tuples of ints, e.g., `[(1,2,3), (-1,
2)]`. Each integer represents a variable's id, with the sign
indicating the polarity of the variable.
2. `input2lit`: A [bidict](https://bidict.readthedocs.io/en/master/)
from input names to variable ids.
2. `output2lit`: A [bidict](https://bidict.readthedocs.io/en/master/)
from output names to variable ids.
Raw data
{
"_id": null,
"home_page": "https://github.com/mvcisback/py-aiger-cnf",
"name": "py-aiger-cnf",
"maintainer": "",
"docs_url": null,
"requires_python": ">=3.7,<4.0",
"maintainer_email": "",
"keywords": "",
"author": "Marcell Vazquez-Chanlatte",
"author_email": "mvc@linux.com",
"download_url": "https://files.pythonhosted.org/packages/0a/b1/a752728fae9365bfffb4f07aef287a2d843f6257d8742f12e3b443185c62/py_aiger_cnf-5.0.8.tar.gz",
"platform": null,
"description": "# py-aiger-cnf\nPython library to convert between AIGER and CNF\n\n[](https://cloud.drone.io/mvcisback/py-aiger-cnf)\n[](https://badge.fury.io/py/py-aiger-cnf)\n[](https://opensource.org/licenses/MIT)\n\n<!-- markdown-toc start - Don't edit this section. Run M-x markdown-toc-generate-toc again -->\n**Table of Contents**\n\n- [Installation](#installation)\n- [Usage](#usage)\n\n<!-- markdown-toc end -->\n\n# Installation\n\nIf you just need to use `aiger_cnf`, you can just run:\n\n`$ pip install py-aiger-cnf`\n\nFor developers, note that this project uses the\n[poetry](https://poetry.eustace.io/) python package/dependency\nmanagement tool. Please familarize yourself with it and then\nrun:\n\n`$ poetry install`\n\n# Usage\n\nThe primary entry point for using `aiger_cnf` is the `aig2cnf`\nfunction which, unsurprisingly, maps `AIG` objects to `CNF` objects.\n\n```python\nimport aiger\nfrom aiger_cnf import aig2cnf\n\nx, y, z = map(aiger.atom, ('x', 'y', 'z'))\nexpr = (x & y) | ~z\ncnf = aig2cnf(expr.aig)\n```\n\nNote that this library also supports `aiger` wrapper libraries so long\nas they export a `.aig` attribute. Thus, could also\nwrite:\n\n```python\ncnf = aig2cnf(expr)\n```\n\n\nThe `CNF` object is a `NamedTuple` with the following three fields:\n\n1. `clauses`: A list of tuples of ints, e.g., `[(1,2,3), (-1,\n 2)]`. Each integer represents a variable's id, with the sign\n indicating the polarity of the variable.\n2. `input2lit`: A [bidict](https://bidict.readthedocs.io/en/master/)\n from input names to variable ids.\n2. `output2lit`: A [bidict](https://bidict.readthedocs.io/en/master/)\n from output names to variable ids.\n",
"bugtrack_url": null,
"license": "MIT",
"summary": "Python library to convert between AIGER and CNF",
"version": "5.0.8",
"project_urls": {
"Homepage": "https://github.com/mvcisback/py-aiger-cnf",
"Repository": "https://github.com/mvcisback/py-aiger-cnf"
},
"split_keywords": [],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "0c95aa9738d1f2d7a4dd7e91554bdbe149f965d64740867ba3ca2fb50cc88273",
"md5": "b19c5005dbdc9fed7ff950bc772fc586",
"sha256": "ccda9b726d001e485b0c40f47024a601332cb6e37a45f8fbe69306c853a64eac"
},
"downloads": -1,
"filename": "py_aiger_cnf-5.0.8-py3-none-any.whl",
"has_sig": false,
"md5_digest": "b19c5005dbdc9fed7ff950bc772fc586",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": ">=3.7,<4.0",
"size": 5136,
"upload_time": "2024-03-16T20:12:14",
"upload_time_iso_8601": "2024-03-16T20:12:14.346143Z",
"url": "https://files.pythonhosted.org/packages/0c/95/aa9738d1f2d7a4dd7e91554bdbe149f965d64740867ba3ca2fb50cc88273/py_aiger_cnf-5.0.8-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "0ab1a752728fae9365bfffb4f07aef287a2d843f6257d8742f12e3b443185c62",
"md5": "81a1cb7e973e6ba5cc7402c7e218b5b0",
"sha256": "727a3a615016b1ce8ebc840ee37f73791d755e5be2883ba209db6d2c61de12a7"
},
"downloads": -1,
"filename": "py_aiger_cnf-5.0.8.tar.gz",
"has_sig": false,
"md5_digest": "81a1cb7e973e6ba5cc7402c7e218b5b0",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.7,<4.0",
"size": 4318,
"upload_time": "2024-03-16T20:12:16",
"upload_time_iso_8601": "2024-03-16T20:12:16.205807Z",
"url": "https://files.pythonhosted.org/packages/0a/b1/a752728fae9365bfffb4f07aef287a2d843f6257d8742f12e3b443185c62/py_aiger_cnf-5.0.8.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2024-03-16 20:12:16",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "mvcisback",
"github_project": "py-aiger-cnf",
"travis_ci": false,
"coveralls": false,
"github_actions": false,
"lcname": "py-aiger-cnf"
}
JSON
