pacfix


Namepacfix JSON
Version 0.0.4 PyPI version JSON
download
home_pageNone
SummaryPAC-learning-based program systhesizer
upload_time2025-09-03 02:53:34
maintainerNone
docs_urlNone
authorNone
requires_python>=3.6
licenseNone
keywords apr
VCS
bugtrack_url
requirements No requirements were recorded.
Travis-CI No Travis.
coveralls test coverage No coveralls.
            # pacfix-python
Python re-implementation of [pacfix](https://github.com/pslhy/pacfix/tree/main).

## Install
```shell
python3 -m pip install pacfix
# Or, you can install from source code
# python3 -m pip install .
pysmt-install --z3
```

## Usage
To see how it works, check out the examples in the [examples](./examples/) directory.

```shell
cd examples/example01
python3 -m pacfix run -i ./mem -l live-variables.txt
```

## Inputs
### live variables file
Specify the live variables file using `-l` or `--live-vars` [live-variables.txt](./examples/example01/live-variables.txt).

```
1 x int
2 y int
3 z bool
4 b int
5 c int
```
Each line lists a variable's ID, name, and type, separated by spaces.

### Input directory
Specify the input directory using `-i` or `--input-dir` [input-dir](./examples/example01/mem).

The input directory should contain neg and pos subdirectories, each with valuation files.
```
[begin]
1 7
2 1
3 0
4 8
5 6
[end]
[begin]
1 1
2 7
3 1
4 8
5 -6
[end]
```
Each file should list variable IDs and their corresponding values. Multiple iterations can be included, with each iteration separated by [begin] and [end].

## Output
Specify the output file using `-o` or `--output`. 

If not specified, the output will be printed to the standard output.

```
[metadata] [live-variables] [total 5] [int 4]
[metadata] [hypothesis-space] [original 1857] [final 1]
[metadata] [valuation] [neg 3] [pos 48] [uniq 51] [init-neg 4] [init-pos 54] [non-uniq 58]
[metadata] [pac] [delta 0.01] [eps 0.09029745462721749]
[metadata] [pac-no-uniq] [delta 0.01] [eps 0.07939948596531193]
[final] --------------
[invariant] [expr (c != 0)]
```

### Output as SMT format
Specify the output directory as `-s` or `--output-smt`.

If not specified, it will not be stored.


```
python3 -m pacfix run -i ./mem -l live-variables.txt -s ./smt
```
In `./smt/0.smt`

```
(set-logic QF_IDL)
(declare-fun c () Int)
(assert (let ((.def_0 (= c 0))) (let ((.def_1 (not .def_0))) .def_1)))
(check-sat)
```

### Debug log
You can enable debug log with `-d` option.

            

Raw data

            {
    "_id": null,
    "home_page": null,
    "name": "pacfix",
    "maintainer": null,
    "docs_url": null,
    "requires_python": ">=3.6",
    "maintainer_email": "Seungheon Han <shhan@unist.ac.kr>",
    "keywords": "apr",
    "author": null,
    "author_email": "Seungheon Han <shhan@unist.ac.kr>",
    "download_url": "https://files.pythonhosted.org/packages/f3/64/b7590256a4a995b87913f47d253640da7a5e0a8ab68d58e7288924c8e08a/pacfix-0.0.4.tar.gz",
    "platform": null,
    "description": "# pacfix-python\nPython re-implementation of [pacfix](https://github.com/pslhy/pacfix/tree/main).\n\n## Install\n```shell\npython3 -m pip install pacfix\n# Or, you can install from source code\n# python3 -m pip install .\npysmt-install --z3\n```\n\n## Usage\nTo see how it works, check out the examples in the [examples](./examples/) directory.\n\n```shell\ncd examples/example01\npython3 -m pacfix run -i ./mem -l live-variables.txt\n```\n\n## Inputs\n### live variables file\nSpecify the live variables file using `-l` or `--live-vars` [live-variables.txt](./examples/example01/live-variables.txt).\n\n```\n1 x int\n2 y int\n3 z bool\n4 b int\n5 c int\n```\nEach line lists a variable's ID, name, and type, separated by spaces.\n\n### Input directory\nSpecify the input directory using `-i` or `--input-dir` [input-dir](./examples/example01/mem).\n\nThe input directory should contain neg and pos subdirectories, each with valuation files.\n```\n[begin]\n1 7\n2 1\n3 0\n4 8\n5 6\n[end]\n[begin]\n1 1\n2 7\n3 1\n4 8\n5 -6\n[end]\n```\nEach file should list variable IDs and their corresponding values. Multiple iterations can be included, with each iteration separated by [begin] and [end].\n\n## Output\nSpecify the output file using `-o` or `--output`. \n\nIf not specified, the output will be printed to the standard output.\n\n```\n[metadata] [live-variables] [total 5] [int 4]\n[metadata] [hypothesis-space] [original 1857] [final 1]\n[metadata] [valuation] [neg 3] [pos 48] [uniq 51] [init-neg 4] [init-pos 54] [non-uniq 58]\n[metadata] [pac] [delta 0.01] [eps 0.09029745462721749]\n[metadata] [pac-no-uniq] [delta 0.01] [eps 0.07939948596531193]\n[final] --------------\n[invariant] [expr (c != 0)]\n```\n\n### Output as SMT format\nSpecify the output directory as `-s` or `--output-smt`.\n\nIf not specified, it will not be stored.\n\n\n```\npython3 -m pacfix run -i ./mem -l live-variables.txt -s ./smt\n```\nIn `./smt/0.smt`\n\n```\n(set-logic QF_IDL)\n(declare-fun c () Int)\n(assert (let ((.def_0 (= c 0))) (let ((.def_1 (not .def_0))) .def_1)))\n(check-sat)\n```\n\n### Debug log\nYou can enable debug log with `-d` option.\n",
    "bugtrack_url": null,
    "license": null,
    "summary": "PAC-learning-based program systhesizer",
    "version": "0.0.4",
    "project_urls": {
        "GitHub": "https://github.com/hsh814/pacfix-python"
    },
    "split_keywords": [
        "apr"
    ],
    "urls": [
        {
            "comment_text": null,
            "digests": {
                "blake2b_256": "3b0b8f71954cecd6db8739b4c0c352c5fff72093e035ce07d5d172e35a2bc507",
                "md5": "c102459e47ccbbf607f14d8aa50d2f81",
                "sha256": "6c3593bea9e0f4bac7222afee9ff56356e75b7019dd34ad1890b18beba54f5d3"
            },
            "downloads": -1,
            "filename": "pacfix-0.0.4-py3-none-any.whl",
            "has_sig": false,
            "md5_digest": "c102459e47ccbbf607f14d8aa50d2f81",
            "packagetype": "bdist_wheel",
            "python_version": "py3",
            "requires_python": ">=3.6",
            "size": 10878,
            "upload_time": "2025-09-03T02:53:32",
            "upload_time_iso_8601": "2025-09-03T02:53:32.559113Z",
            "url": "https://files.pythonhosted.org/packages/3b/0b/8f71954cecd6db8739b4c0c352c5fff72093e035ce07d5d172e35a2bc507/pacfix-0.0.4-py3-none-any.whl",
            "yanked": false,
            "yanked_reason": null
        },
        {
            "comment_text": null,
            "digests": {
                "blake2b_256": "f364b7590256a4a995b87913f47d253640da7a5e0a8ab68d58e7288924c8e08a",
                "md5": "336e4e22a35cf533292173dc991c4759",
                "sha256": "3779c8df6f849e3b67ada4f9a351cafdae924a27d0ffb77911e292a12e902e36"
            },
            "downloads": -1,
            "filename": "pacfix-0.0.4.tar.gz",
            "has_sig": false,
            "md5_digest": "336e4e22a35cf533292173dc991c4759",
            "packagetype": "sdist",
            "python_version": "source",
            "requires_python": ">=3.6",
            "size": 9852,
            "upload_time": "2025-09-03T02:53:34",
            "upload_time_iso_8601": "2025-09-03T02:53:34.032123Z",
            "url": "https://files.pythonhosted.org/packages/f3/64/b7590256a4a995b87913f47d253640da7a5e0a8ab68d58e7288924c8e08a/pacfix-0.0.4.tar.gz",
            "yanked": false,
            "yanked_reason": null
        }
    ],
    "upload_time": "2025-09-03 02:53:34",
    "github": true,
    "gitlab": false,
    "bitbucket": false,
    "codeberg": false,
    "github_user": "hsh814",
    "github_project": "pacfix-python",
    "travis_ci": false,
    "coveralls": false,
    "github_actions": false,
    "lcname": "pacfix"
}
        
Elapsed time: 1.89135s