diff --git a/src/clingexplaid/cli/clingo_app.py b/src/clingexplaid/cli/clingo_app.py index 34b17f0..83fdb00 100644 --- a/src/clingexplaid/cli/clingo_app.py +++ b/src/clingexplaid/cli/clingo_app.py @@ -183,7 +183,11 @@ def _method_mus( # Case: Finding a single MUS if max_models == -1: - control.solve(assumptions=list(assumptions), on_core=cc.shrink) + + def shrink_on_model(core: Sequence[int]) -> None: + _ = cc.shrink(core) + + control.solve(assumptions=list(assumptions), on_core=shrink_on_model) if cc.minimal is None: print("SATISFIABLE: Instance has no MUS") diff --git a/src/clingexplaid/cli/textual_gui.py b/src/clingexplaid/cli/textual_gui.py index 2027571..cac4d12 100644 --- a/src/clingexplaid/cli/textual_gui.py +++ b/src/clingexplaid/cli/textual_gui.py @@ -53,6 +53,8 @@ class Modes(Enum): + """Representation of the Clingo-Explaid Modes""" + MODE_MUS = "Minimal Unsatisfiable Subsets" MODE_UNSAT_CONSTRAINTS = "Unsatisfiable Constraints" MODE_SHOW_DECISIONS = "Show Decisions" @@ -429,6 +431,7 @@ class ClingexplaidTextualApp(App[int]): """A textual app for a terminal GUI to use the clingexplaid functionality""" # pylint: disable=too-many-instance-attributes + # pylint: disable=too-many-public-methods # pylint: disable=duplicate-code CSS = MAIN_CSS @@ -671,8 +674,8 @@ async def action_mode_show_decisions(self) -> None: self.tree_cursor.add(end_string) async def action_mode_explain(self) -> None: - # TODO: Add implementation - pass + """Action for Explain Mode""" + # Add implementation async def action_solve(self) -> None: """ diff --git a/tests/clingexplaid/test_muc.py b/tests/clingexplaid/test_muc.py index 2ca9224..3c6ecb4 100644 --- a/tests/clingexplaid/test_muc.py +++ b/tests/clingexplaid/test_muc.py @@ -3,7 +3,7 @@ """ import random -from typing import List, Optional, Set, Tuple +from typing import List, Optional, Sequence, Set, Tuple from unittest import TestCase import clingo @@ -34,7 +34,11 @@ def get_mus_of_program( assumptions = at.get_assumption_literals(ctl) cc = CoreComputer(ctl, assumptions) - ctl.solve(assumptions=list(assumptions), on_core=cc.shrink) + + def shrink_on_model(core: Sequence[int]) -> None: + _ = cc.shrink(core) + + ctl.solve(assumptions=list(assumptions), on_core=shrink_on_model) # 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()