logicedit 0.1.9

Extensible JSONL task editing library for code and formula inputs.

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

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:

make publish-pypi

Install the published package from PyPI:

make install-pypi

If you prefer the raw commands:

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

Run

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:

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:

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

{
  "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:

{
  "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:

{
  "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

python3 -m pytest