Metadata-Version: 2.4
Name: logicedit
Version: 0.1.9
Summary: Extensible JSONL task editing library for code and formula inputs.
License: CC-BY-4.0
Keywords: csp,jsonl,logic-programs,formula-editing,data-augmentation
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Developers
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Requires-Python: >=3.10
Description-Content-Type: text/markdown
License-File: LICENSE
Requires-Dist: func-timeout
Requires-Dist: nltk
Requires-Dist: ply
Requires-Dist: python-constraint
Requires-Dist: Unidecode
Requires-Dist: z3-solver
Provides-Extra: dev
Requires-Dist: build>=1.2.2; extra == "dev"
Requires-Dist: pytest>=8.0; extra == "dev"
Requires-Dist: twine>=5.1.1; extra == "dev"
Provides-Extra: release
Requires-Dist: build>=1.2.2; extra == "release"
Requires-Dist: twine>=5.1.1; extra == "release"
Dynamic: license-file

# logicedit

`logicedit` processes JSON or JSONL task records, applies controlled line edits, runs edited variants through registered tools, evaluates tool outputs, and writes successful variants back as JSONL.

## Features

- Dataclass-based record models with `extra_options` for forward-compatible schema changes.
- `single_edit` mode for independent edits from the original input.
- `cumulative_edit` mode for greedy accepted edits applied on top of prior edits.
- Tool registry with in-memory tools, Python-file adapters, and built-in Z3 and Prover9 solver adapters.
- Explicit required tool selection via `tool`.
- Configurable label comparison strategies for label-preserving and label-variation workflows.
- Minimal examples with a mock tool and mock editor.

## Install

```bash
python3 -m pip install -e .[dev]
```

This installs the library dependencies, including `z3-solver`, `nltk`, `ply`, and `Unidecode` for the built-in Z3 and Prover9 backends.

## PyPI Release Flow

Build and upload to PyPI:

```bash
make publish-pypi
```

Install the published package from PyPI:

```bash
make install-pypi
```

If you prefer the raw commands:

```bash
python3 -m build
python3 -m twine upload --repository-url https://upload.pypi.org/legacy/ dist/*
python3 -m pip install logicedit
```

## Run

```bash
python3 -m logicedit.cli \
  --input /path/to/tasks.jsonl \
  --output /path/to/successes.jsonl \
  --tool csp_solver.py \
  --edit-mode single_edit \
  --number-of-edits 3 \
  --label-variation \
  --single-edit-ids 0,2,4
```

`number_of_edits` accepts either a positive integer or `"all"`.

- In `single_edit` mode, the library evaluates independent edits from the original input and saves every successful independent edit. `number_of_edits` is ignored in this mode. Use `--single-edit-ids` or `extra_options.selected_edit_ids` to restrict which editable units are considered.
- In `cumulative_edit` mode, `number_of_edits` controls how many accepted cumulative edits are saved. `"all"` means the runner walks the editable statements from first to last, tries the available operator edits for each statement against the `label_variation` condition, applies the first acceptable edit, and then moves to the next statement.
- `--tool` is mandatory on the CLI. The library no longer defaults silently to `csp_solver`.
- `--no-label-variation` is the default behavior: only save records whose tool output matches the original label.
- `--label-variation` inverts that rule: only save records whose tool output differs from the original label.

Available tool families:

- `csp_solver.py` or another Python tool file: uses the Python-file adapter. Point `extra_options.tool_search_paths` at the folder containing it. The adapter can call plain functions such as `run(input_text)` and also supports the `CSP_Program` class shape found in the source files.
- `z3_solver`: uses the built-in vendored Z3 backend and Z3-specific operator edits in the `# Constraints` section: `AND -> OR`, `XOR -> OR`, `OR -> XOR`, and `NOT` removal.
- `prover9_solver` or `tool_inference.py`: uses the built-in vendored Prover9 backend and Prover9-specific premise edits such as `∨ -> ∧`, `⊕ -> ∨`, `∨ -> ⊕`, and `¬` removal.

The library only searches tool paths you provide or the input file directory added by the CLI.

Example Z3 run:

```bash
python3 -m logicedit.cli \
  --input /path/to/z3_tasks.jsonl \
  --output /path/to/z3_successes.jsonl \
  --tool z3_solver \
  --edit-mode cumulative_edit \
  --number-of-edits all
```

Example Prover9 run:

```bash
export PROVER9=/path/to/LADR-2009-11A/bin/prover9

python3 -m logicedit.cli \
  --input /path/to/prover9_tasks.jsonl \
  --output /path/to/prover9_successes.jsonl \
  --tool prover9_solver \
  --edit-mode single_edit
```

`prover9_solver` expects each record to provide:

- `premise_translations`: a list of `"English ::: FOL"` premise strings
- `conclusion_translation`: one `"English ::: FOL"` conclusion string

You can point Prover9 at the LADR binary in any of these ways:

- Set `PROVER9=/path/to/LADR-2009-11A/bin/prover9`
- Put `extra_options.prover9_path` or `extra_options.prover9_executable` in each record
- Place an extracted `LADR-2009-11A/bin/prover9` directory at the repo root or current working directory

Ways to include `LADR-2009-11A.tar` with the library:

- Recommended: keep the extracted `LADR-2009-11A` directory outside the wheel and configure `PROVER9` or `extra_options.prover9_path`. This avoids shipping a large platform-specific binary inside the package.
- Repo-local vendor: commit an extracted `LADR-2009-11A/` directory next to the project and let `logicedit` discover `LADR-2009-11A/bin/prover9` automatically. This is simple but makes the repo much larger.
- Managed bootstrap: add a separate setup script that unpacks `LADR-2009-11A.tar` into a known cache or vendor directory before running Prover9. This keeps the wheel cleaner while still supporting a self-contained checkout.
- Platform-specific packaging: include the extracted executable as package data in a macOS/Linux-specific build. This is the most self-contained option, but it is heavier and harder to maintain across platforms.

## Example Record

```json
{
  "id": "logical_deduction_0",
  "tool": "csp_solver.py",
  "input_type": "code",
  "edit_mode": "single_edit",
  "number_of_edits": 2,
  "label_variation": false,
  "expected_answer": "D",
  "logic_program": "Domain:\n...\nConstraints:\nThe blue book is to the right of the yellow book. ::: blue_book > yellow_book\n...\n\nQuery:\n..."
}
```

Example Z3 record:

```json
{
  "id": "ar_lsat_0",
  "tool": "z3_solver",
  "input_type": "code",
  "edit_mode": "single_edit",
  "number_of_edits": 2,
  "label_variation": true,
  "expected_answer": "B",
  "logic_program": "# Declarations\n...\n\n# Constraints\nrule ::: A AND B\n...\n\n# Options\nQuestion ::: ...\n..."
}
```

Example Prover9 record:

```json
{
  "id": "folio_0",
  "tool": "prover9_solver",
  "input_type": "code",
  "edit_mode": "single_edit",
  "number_of_edits": 2,
  "label_variation": true,
  "expected_answer": "A",
  "question": "Is the conclusion entailed?",
  "premise_translations": [
    "All cats are either pets or strays. ::: ∀x (Cat(x) → (Pet(x) ∨ Stray(x)))",
    "Milo is not a stray. ::: ¬Stray(Milo)"
  ],
  "conclusion_translation": "Milo is a pet. ::: Pet(Milo)",
  "extra_options": {
    "prover9_path": "/path/to/LADR-2009-11A/bin/prover9"
  }
}
```

## Test

```bash
python3 -m pytest
```
