diff --git a/README.md b/README.md index ab72196..463d734 100644 --- a/README.md +++ b/README.md @@ -19,6 +19,15 @@ pip install clingexplaid clingexplaid -h ``` +Compute Minimal Unsatisfiable Core from unsatisfiable program: + +```shell +clingexplaid --assumption-signature signature/arity +``` + ++ `--assumption-signature` is optional to allow for only specific facts to be transformed to assumptions + + if no such option is given all facts are transformed to assumptions regardless of their signature + ## Development To improve code quality, we run linters, type checkers, and unit tests. The diff --git a/src/clingexplaid/utils/cli.py b/src/clingexplaid/utils/cli.py index 9c12b4f..8a17f7f 100644 --- a/src/clingexplaid/utils/cli.py +++ b/src/clingexplaid/utils/cli.py @@ -2,6 +2,9 @@ Command Line Interface Utilities """ +import configparser +from pathlib import Path + from clingo.application import Application from clingexplaid.utils import get_solver_literal_lookup @@ -43,20 +46,27 @@ def register_options(self, options): options.add( group, - "assumption-signatures,a", - "All facts matching with this signature will be converted to assumptions for finding a MUC " + "assumption-signature,a", + "Facts matching with this signature will be converted to assumptions for finding a MUC " "(default: all facts)", self._parse_assumption_signature, multi=True, ) def main(self, control, files): + setup_file_path = Path(__file__).parent.joinpath("../../../setup.cfg") + setup_config = configparser.ConfigParser() + setup_config.read(setup_file_path) + metadata = setup_config["metadata"] + print(metadata["name"], "version", metadata["version"]) signature_set = set(self.signatures.items()) if self.signatures else None at = AssumptionTransformer(signatures=signature_set) if not files: program_transformed = at.parse_files("-") + print("Reading from -") else: program_transformed = at.parse_files(files) + print(f"Reading from {files[0]} {'...' if len(files) > 1 else ''}") control.add("base", [], program_transformed) control.ground([("base", [])]) @@ -66,6 +76,8 @@ def main(self, control, files): assumptions = at.get_assumptions(control) cc = CoreComputer(control, assumptions) + + print("Solving...") control.solve(assumptions=list(assumptions), on_core=cc.shrink) if cc.minimal is None: