From 955729a1d9f3d2929bf8ea641b2093517f06e1ad Mon Sep 17 00:00:00 2001 From: Hannes Weichelt Date: Tue, 8 Aug 2023 18:21:54 +0200 Subject: [PATCH 1/3] updated cli -a option name --- src/clingexplaid/utils/cli.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/clingexplaid/utils/cli.py b/src/clingexplaid/utils/cli.py index 9c12b4f..e3d76dc 100644 --- a/src/clingexplaid/utils/cli.py +++ b/src/clingexplaid/utils/cli.py @@ -43,8 +43,8 @@ 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, From 60f6dd27abe0b8b7cc3ad41ed5b04f196639d23f Mon Sep 17 00:00:00 2001 From: Hannes Weichelt Date: Tue, 8 Aug 2023 18:22:07 +0200 Subject: [PATCH 2/3] added small how to use for cli --- README.md | 9 +++++++++ 1 file changed, 9 insertions(+) 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 From 12c3e9deaa85c22646c9783d23b77bd8f19af954 Mon Sep 17 00:00:00 2001 From: Hannes Weichelt Date: Tue, 8 Aug 2023 19:46:42 +0200 Subject: [PATCH 3/3] added output header print for cli call --- src/clingexplaid/utils/cli.py | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/clingexplaid/utils/cli.py b/src/clingexplaid/utils/cli.py index e3d76dc..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 @@ -51,12 +54,19 @@ def register_options(self, options): ) 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: