From f626b125b3f836d01f8fdc6add4953620bc23aa9 Mon Sep 17 00:00:00 2001 From: Hannes Weichelt Date: Wed, 15 May 2024 11:11:43 +0200 Subject: [PATCH] continued renaming MUC -> MUS --- src/clingexplaid/cli/clingo_app.py | 72 ++++++------ src/clingexplaid/{muc => mus}/__init__.py | 0 .../{muc => mus}/core_computer.py | 0 ...multi_muc.lp => test_program_multi_mus.lp} | 0 tests/clingexplaid/test_muc.py | 106 +++++++++--------- 5 files changed, 89 insertions(+), 89 deletions(-) rename src/clingexplaid/{muc => mus}/__init__.py (100%) rename src/clingexplaid/{muc => mus}/core_computer.py (100%) rename tests/clingexplaid/res/{test_program_multi_muc.lp => test_program_multi_mus.lp} (100%) diff --git a/src/clingexplaid/cli/clingo_app.py b/src/clingexplaid/cli/clingo_app.py index 733552a..11e420b 100644 --- a/src/clingexplaid/cli/clingo_app.py +++ b/src/clingexplaid/cli/clingo_app.py @@ -12,7 +12,7 @@ import clingo from clingo.application import Application, Flag -from ..muc import CoreComputer +from ..mus import CoreComputer from ..propagators import DecisionOrderPropagator from ..transformers import AssumptionTransformer, OptimizationRemover from ..unsat_constraints import UnsatConstraintComputer @@ -30,7 +30,7 @@ class ClingoExplaidApp(Application): # pylint: disable = too-many-instance-attributes CLINGEXPLAID_METHODS = { - "muc": "Description for MUC method", + "mus": "Description for MUS method", "unsat-constraints": "Description for unsat-constraints method", "show-decisions": "Visualize the decision process of clingo during solving", } @@ -48,9 +48,9 @@ def __init__(self, name: str) -> None: self._show_decisions_decision_signatures: Dict[str, int] = {} self._show_decisions_model_id: int = 1 - # MUC - self._muc_assumption_signatures: Dict[str, int] = {} - self._muc_id: int = 1 + # MUS + self._mus_assumption_signatures: Dict[str, int] = {} + self._mus_id: int = 1 def _initialize(self) -> None: # add enabled methods to self.methods @@ -72,8 +72,8 @@ def _parse_signature(signature_string: str) -> Tuple[str, int]: return match_result.group(1), int(match_result.group(2)) def _parse_assumption_signature(self, assumption_signature: str) -> bool: - if not self.method_flags["muc"]: - print("PARSE ERROR: The assumption signature option is only available if the flag --muc is enabled") + if not self.method_flags["mus"]: + print("PARSE ERROR: The assumption signature option is only available if the flag --mus is enabled") return False assumption_signature_string = assumption_signature.replace("=", "").strip() try: @@ -84,7 +84,7 @@ def _parse_assumption_signature(self, assumption_signature: str) -> bool: "/" ) return False - self._muc_assumption_signatures[signature] = arity + self._mus_assumption_signatures[signature] = arity return True def _parse_decision_signature(self, decision_signature: str) -> bool: @@ -116,12 +116,12 @@ def register_options(self, options: clingo.ApplicationOptions) -> None: target=self.method_flags[method], ) - group = "MUC Options" + group = "MUS Options" options.add( group, "assumption-signature,a", - "Facts matching with this signature will be converted to assumptions for finding a MUC " + "Facts matching with this signature will be converted to assumptions for finding a MUS " "(default: all facts)", self._parse_assumption_signature, multi=True, @@ -143,7 +143,7 @@ def register_options(self, options: clingo.ApplicationOptions) -> None: def _apply_assumption_transformer( self, signatures: Dict[str, int], files: List[str] ) -> Tuple[str, AssumptionTransformer]: - signature_set = set(self._muc_assumption_signatures.items()) if signatures else None + signature_set = set(self._mus_assumption_signatures.items()) if signatures else None at = AssumptionTransformer(signatures=signature_set) if not files: program_transformed = at.parse_files("-") @@ -151,19 +151,19 @@ def _apply_assumption_transformer( program_transformed = at.parse_files(files) return program_transformed, at - def _print_muc(self, muc_string: str) -> None: - print(f"{BACKGROUND_COLORS['BLUE']} MUC {BACKGROUND_COLORS['LIGHT_BLUE']} {self._muc_id} {COLORS['NORMAL']}") - print(f"{COLORS['BLUE']}{muc_string}{COLORS['NORMAL']}") - self._muc_id += 1 + def _print_mus(self, mus_string: str) -> None: + print(f"{BACKGROUND_COLORS['BLUE']} MUS {BACKGROUND_COLORS['LIGHT_BLUE']} {self._mus_id} {COLORS['NORMAL']}") + print(f"{COLORS['BLUE']}{mus_string}{COLORS['NORMAL']}") + self._mus_id += 1 - def _method_muc( + def _method_mus( self, control: clingo.Control, files: List[str], compute_unsat_constraints: bool = False, ) -> None: program_transformed, at = self._apply_assumption_transformer( - signatures=self._muc_assumption_signatures, files=files + signatures=self._mus_assumption_signatures, files=files ) # remove optimization statements @@ -179,32 +179,32 @@ def _method_muc( max_models = int(control.configuration.solve.models) # type: ignore print("Solving...") - # Case: Finding a single MUC + # Case: Finding a single MUS if max_models == -1: control.solve(assumptions=list(assumptions), on_core=cc.shrink) if cc.minimal is None: - print("SATISFIABLE: Instance has no MUCs") + print("SATISFIABLE: Instance has no MUS") return if len(list(cc.minimal)) == 0: print( - "NO MUCS CONTAINED: The unsatisfiability of this program is not induced by the provided assumptions" + "NO MUS CONTAINED: The unsatisfiability of this program is not induced by the provided assumptions" ) return - muc_string = " ".join(cc.mus_to_string(cc.minimal)) - self._print_muc(muc_string) + mus_string = " ".join(cc.mus_to_string(cc.minimal)) + self._print_mus(mus_string) if compute_unsat_constraints: self._method_unsat_constraints( control=clingo.Control(), files=files, - assumption_string=muc_string, + assumption_string=mus_string, output_prefix_active=f"{COLORS['RED']}├──{COLORS['NORMAL']}", output_prefix_passive=f"{COLORS['RED']}│ {COLORS['NORMAL']}", ) - # Case: Finding multiple MUCs + # Case: Finding multiple MUS if max_models >= 0: program_unsat = False with control.solve(assumptions=list(assumptions), yield_=True) as solve_handle: @@ -212,23 +212,23 @@ def _method_muc( program_unsat = True if program_unsat: - mucs = 0 - for muc in cc.get_multiple_minimal(max_mus=max_models): - mucs += 1 - muc_string = " ".join(cc.mus_to_string(muc)) - self._print_muc(muc_string) + n_mus = 0 + for mus in cc.get_multiple_minimal(max_mus=max_models): + n_mus += 1 + mus_string = " ".join(cc.mus_to_string(mus)) + self._print_mus(mus_string) if compute_unsat_constraints: self._method_unsat_constraints( control=clingo.Control(), files=files, - assumption_string=muc_string, + assumption_string=mus_string, output_prefix_active=f"{COLORS['RED']}├──{COLORS['NORMAL']}", output_prefix_passive=f"{COLORS['RED']}│ {COLORS['NORMAL']}", ) - if not mucs: + if not n_mus: print( - "NO MUCS CONTAINED: The unsatisfiability of this program is not induced by the provided " + "NO MUS CONTAINED: The unsatisfiability of this program is not induced by the provided " "assumptions" ) return @@ -339,10 +339,10 @@ def main(self, control: clingo.Control, files: Sequence[str]) -> None: method_function = self.method_functions[method] method_function(control, files) # special cases where specific pipelines have to be configured - elif self.methods == {"muc", "unsat-constraints"}: - self.method_functions["muc"](control, files, compute_unsat_constraints=True) - elif self.methods == {"muc", "unsat-constraints", "show-decisions"}: - self.method_functions["muc"](control, files, compute_unsat_constraints=True) + elif self.methods == {"mus", "unsat-constraints"}: + self.method_functions["mus"](control, files, compute_unsat_constraints=True) + elif self.methods == {"mus", "unsat-constraints", "show-decisions"}: + self.method_functions["mus"](control, files, compute_unsat_constraints=True) elif self.methods == {"unsat-constraints", "show-decisions"}: self.method_functions["unsat-constraints"](control, files) else: diff --git a/src/clingexplaid/muc/__init__.py b/src/clingexplaid/mus/__init__.py similarity index 100% rename from src/clingexplaid/muc/__init__.py rename to src/clingexplaid/mus/__init__.py diff --git a/src/clingexplaid/muc/core_computer.py b/src/clingexplaid/mus/core_computer.py similarity index 100% rename from src/clingexplaid/muc/core_computer.py rename to src/clingexplaid/mus/core_computer.py diff --git a/tests/clingexplaid/res/test_program_multi_muc.lp b/tests/clingexplaid/res/test_program_multi_mus.lp similarity index 100% rename from tests/clingexplaid/res/test_program_multi_muc.lp rename to tests/clingexplaid/res/test_program_multi_mus.lp diff --git a/tests/clingexplaid/test_muc.py b/tests/clingexplaid/test_muc.py index 1c69241..4bc3c93 100644 --- a/tests/clingexplaid/test_muc.py +++ b/tests/clingexplaid/test_muc.py @@ -1,5 +1,5 @@ """ -Tests for the muc package +Tests for the mus package """ import random @@ -8,20 +8,20 @@ import clingo -from clingexplaid.muc import CoreComputer +from clingexplaid.mus import CoreComputer from clingexplaid.transformers import AssumptionTransformer from clingexplaid.utils.types import AssumptionSet from .test_main import TEST_DIR -def get_muc_of_program( +def get_mus_of_program( program_string: str, assumption_signatures: Set[Tuple[str, int]], control: Optional[clingo.Control] = None, ) -> Tuple[AssumptionSet, CoreComputer]: """ - Helper function to directly get the MUC of a given program string. + Helper function to directly get the MUS of a given program string. """ ctl = control if control is not None else clingo.Control() @@ -36,32 +36,32 @@ def get_muc_of_program( cc = CoreComputer(ctl, assumptions) ctl.solve(assumptions=list(assumptions), on_core=cc.shrink) - # if the instance was satisfiable and the on_core function wasn't called an empty set is returned, else the muc. + # if the instance was satisfiable and the on_core function wasn't called an empty set is returned, else the mus. result = cc.minimal if cc.minimal is not None else set() return result, cc -class TestMUC(TestCase): +class TestMUS(TestCase): """ - Test cases for MUC functionality. + Test cases for MUS functionality. """ - def _assert_muc( + def _assert_mus( self, - muc: Set[str], - valid_mucs_string_lists: List[Set[str]], + mus: Set[str], + valid_mus_string_lists: List[Set[str]], ) -> None: """ - Asserts if a MUC is one of several valid MUC's. + Asserts if a MUS is one of several valid MUS's. """ - valid_mucs = [{clingo.parse_term(s) for s in lit_strings} for lit_strings in valid_mucs_string_lists] - parsed_muc = {clingo.parse_term(s) for s in muc} - self.assertIn(parsed_muc, valid_mucs) + valid_mus_list = [{clingo.parse_term(s) for s in lit_strings} for lit_strings in valid_mus_string_lists] + parsed_mus = {clingo.parse_term(s) for s in mus} + self.assertIn(parsed_mus, valid_mus_list) - def test_core_computer_shrink_single_muc(self) -> None: + def test_core_computer_shrink_single_mus(self) -> None: """ - Test the CoreComputer's `shrink` function with a single MUC. + Test the CoreComputer's `shrink` function with a single MUS. """ ctl = clingo.Control() @@ -72,15 +72,15 @@ def test_core_computer_shrink_single_muc(self) -> None: """ signatures = {("a", 1)} - muc, cc = get_muc_of_program(program_string=program, assumption_signatures=signatures, control=ctl) + mus, cc = get_mus_of_program(program_string=program, assumption_signatures=signatures, control=ctl) if cc.minimal is None: self.fail() - self._assert_muc(cc.muc_to_string(muc), [{"a(1)", "a(4)", "a(5)"}]) + self._assert_mus(cc.mus_to_string(mus), [{"a(1)", "a(4)", "a(5)"}]) - def test_core_computer_shrink_single_atomic_muc(self) -> None: + def test_core_computer_shrink_single_atomic_mus(self) -> None: """ - Test the CoreComputer's `shrink` function with a single atomic MUC. + Test the CoreComputer's `shrink` function with a single atomic MUS. """ ctl = clingo.Control() @@ -91,15 +91,15 @@ def test_core_computer_shrink_single_atomic_muc(self) -> None: """ signatures = {("a", 1)} - muc, cc = get_muc_of_program(program_string=program, assumption_signatures=signatures, control=ctl) + mus, cc = get_mus_of_program(program_string=program, assumption_signatures=signatures, control=ctl) if cc.minimal is None: self.fail() - self._assert_muc(cc.muc_to_string(muc), [{"a(3)"}]) + self._assert_mus(cc.mus_to_string(mus), [{"a(3)"}]) - def test_core_computer_shrink_multiple_atomic_mucs(self) -> None: + def test_core_computer_shrink_multiple_atomic_mus(self) -> None: """ - Test the CoreComputer's `shrink` function with multiple atomic MUC's. + Test the CoreComputer's `shrink` function with multiple atomic MUS's. """ ctl = clingo.Control() @@ -112,15 +112,15 @@ def test_core_computer_shrink_multiple_atomic_mucs(self) -> None: """ signatures = {("a", 1)} - muc, cc = get_muc_of_program(program_string=program, assumption_signatures=signatures, control=ctl) + mus, cc = get_mus_of_program(program_string=program, assumption_signatures=signatures, control=ctl) if cc.minimal is None: self.fail() - self._assert_muc(cc.muc_to_string(muc), [{"a(3)"}, {"a(5)"}, {"a(9)"}]) + self._assert_mus(cc.mus_to_string(mus), [{"a(3)"}, {"a(5)"}, {"a(9)"}]) - def test_core_computer_shrink_multiple_mucs(self) -> None: + def test_core_computer_shrink_multiple_mus(self) -> None: """ - Test the CoreComputer's `shrink` function with multiple MUC's. + Test the CoreComputer's `shrink` function with multiple MUS's. """ ctl = clingo.Control() @@ -133,12 +133,12 @@ def test_core_computer_shrink_multiple_mucs(self) -> None: """ signatures = {("a", 1)} - muc, cc = get_muc_of_program(program_string=program, assumption_signatures=signatures, control=ctl) + mus, cc = get_mus_of_program(program_string=program, assumption_signatures=signatures, control=ctl) if cc.minimal is None: self.fail() - self._assert_muc( - cc.muc_to_string(muc), + self._assert_mus( + cc.mus_to_string(mus), [ {"a(3)", "a(9)", "a(5)"}, {"a(5)", "a(1)", "a(2)"}, @@ -161,11 +161,11 @@ def test_core_computer_shrink_large_instance_random(self) -> None: """ signatures = {("a", 1)} - muc, cc = get_muc_of_program(program_string=program, assumption_signatures=signatures, control=ctl) + mus, cc = get_mus_of_program(program_string=program, assumption_signatures=signatures, control=ctl) if cc.minimal is None: self.fail() - self._assert_muc(cc.muc_to_string(muc), [{f"a({i})" for i in random_core}]) + self._assert_mus(cc.mus_to_string(mus), [{f"a({i})" for i in random_core}]) def test_core_computer_shrink_satisfiable(self) -> None: """ @@ -179,57 +179,57 @@ def test_core_computer_shrink_satisfiable(self) -> None: """ signatures = {("a", 1)} - muc, _ = get_muc_of_program(program_string=program, assumption_signatures=signatures, control=ctl) + mus, _ = get_mus_of_program(program_string=program, assumption_signatures=signatures, control=ctl) - self.assertEqual(muc, set()) + self.assertEqual(mus, set()) def test_core_computer_get_multiple_minimal(self) -> None: """ - Test the CoreComputer's `get_multiple_minimal` function to get multiple MUCs. + Test the CoreComputer's `get_multiple_minimal` function to get multiple MUS's. """ ctl = clingo.Control() - program_path = TEST_DIR.joinpath("res/test_program_multi_muc.lp") + program_path = TEST_DIR.joinpath("res/test_program_multi_mus.lp") at = AssumptionTransformer(signatures={("a", 1)}) parsed = at.parse_files([program_path]) ctl.add("base", [], parsed) ctl.ground([("base", [])]) cc = CoreComputer(ctl, at.get_assumptions(ctl)) - muc_generator = cc.get_multiple_minimal() + mus_generator = cc.get_multiple_minimal() - muc_string_sets = [cc.muc_to_string(muc) for muc in list(muc_generator)] - for muc_string_set in muc_string_sets: + mus_string_sets = [cc.mus_to_string(mus) for mus in list(mus_generator)] + for mus_string_set in mus_string_sets: self.assertIn( - muc_string_set, + mus_string_set, [{"a(1)", "a(2)"}, {"a(1)", "a(9)"}, {"a(3)", "a(5)", "a(8)"}], ) - def test_core_computer_get_multiple_minimal_max_mucs_2(self) -> None: + def test_core_computer_get_multiple_minimal_max_mus_2(self) -> None: """ - Test the CoreComputer's `get_multiple_minimal` function to get multiple MUCs. + Test the CoreComputer's `get_multiple_minimal` function to get multiple MUS's. """ ctl = clingo.Control() - program_path = TEST_DIR.joinpath("res/test_program_multi_muc.lp") + program_path = TEST_DIR.joinpath("res/test_program_multi_mus.lp") at = AssumptionTransformer(signatures={("a", 1)}) parsed = at.parse_files([program_path]) ctl.add("base", [], parsed) ctl.ground([("base", [])]) cc = CoreComputer(ctl, at.get_assumptions(ctl)) - muc_generator = cc.get_multiple_minimal(max_mucs=2) + mus_generator = cc.get_multiple_minimal(max_mus=2) - muc_string_sets = [cc.muc_to_string(muc) for muc in list(muc_generator)] - for muc_string_set in muc_string_sets: + mus_string_sets = [cc.mus_to_string(mus) for mus in list(mus_generator)] + for mus_string_set in mus_string_sets: self.assertIn( - muc_string_set, + mus_string_set, [{"a(1)", "a(2)"}, {"a(1)", "a(9)"}, {"a(3)", "a(5)", "a(8)"}], ) - self.assertEqual(len(muc_string_sets), 2) + self.assertEqual(len(mus_string_sets), 2) # INTERNAL @@ -254,8 +254,8 @@ def test_core_computer_internal_compute_single_minimal_satisfiable(self) -> None control.ground([("base", [])]) assumptions = {(clingo.parse_term(c), True) for c in "abc"} cc = CoreComputer(control, assumptions) - muc = cc._compute_single_minimal() # pylint: disable=W0212 - self.assertEqual(muc, set()) + mus = cc._compute_single_minimal() # pylint: disable=W0212 + self.assertEqual(mus, set()) def test_core_computer_internal_compute_single_minimal_no_assumptions(self) -> None: """ @@ -266,7 +266,7 @@ def test_core_computer_internal_compute_single_minimal_no_assumptions(self) -> N cc = CoreComputer(control, set()) self.assertRaises(ValueError, cc._compute_single_minimal) # pylint: disable=W0212 - def test_core_computer_muc_to_string(self) -> None: + def test_core_computer_mus_to_string(self) -> None: """ Test the CoreComputer's `_compute_single_minimal` function with no assumptions. """ @@ -274,6 +274,6 @@ def test_core_computer_muc_to_string(self) -> None: control = clingo.Control() cc = CoreComputer(control, set()) self.assertEqual( - cc.muc_to_string({(clingo.parse_term(string), True) for string in ["this", "is", "a", "test"]}), + cc.mus_to_string({(clingo.parse_term(string), True) for string in ["this", "is", "a", "test"]}), {"this", "is", "a", "test"}, ) # pylint: disable=W0212