diff --git a/README.md b/README.md index dac396a..7f04a65 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ # clingexplaid -Tools to aid the development of explanation systems using clingo +API to aid the development of explanation systems using clingo ## Installation @@ -19,97 +19,6 @@ pip install clingexplaid Please refer to [DEVELOPEMENT](DEVELOPMENT.md) -## Usage - -Run the following for basic usage information: - -```bash -clingexplaid -h -``` - -### Interactive Mode - -We provide an interactive terminal user interface (textual) where all modes are -accessible in an interactive format. You can start this mode by using the -command below. - -```bash -clingexplaid --interactive -``` - -#### Example: MUS Sudoku - -Below is one Example call using our [Sudoku Example](examples/sudoku). - -```bash -clingexplaid examples/sudoku/encoding.lp examples/sudoku/instance.lp --interactive -``` - -![](example_mus.png) - -#### Example: Show Decisions - -This Example shows the interactive Solver Decision Tree generated from -[`examples/misc/sat_simple.lp`](examples/misc/sat_simple.lp). - -![](example_show_decisions.png) - -### Clingo Application Class - -The clingexplaid CLI (based on the `clingo.Application` class) extends clingo -with `` and ``. - -```bash -clingexplaid -``` - -- ``: specifies which Clingexplaid method is used (Required) - - Options: - - `--muc`: - - Computes the Minimal Unsatisfiable Cores (MUCs) of the provided - unsatisfiable program - - `--unsat-constraints`: - - Computes the Unsatisfiable Constraints of the unsatisfiable program - provided. - - `--show-decisions`: - - Visualizes the decision process of clasp -- ``: Additional options for the different methods - - For `--muc`: - - `-a`, `--assumption-signature`: limits which facts of the current program - are converted to choices/assumptions for finding the MUCs (Default: all - facts are converted) - - For `--show-decisions`: - - `--decision-signature`: limits which decisions are shown in the - visualization (Default: all atom's decisions are shown) - -### Examples - -Given the simple program below [`simple.lp`](examples/misc/simple.lp) we want -to find the contained MUC (Minimal Unsatisfiable Core). - -``` -a(1..5). -b(5..10). - -:- a(X), b(X). -``` - -For this we can call `clingexplaid` the following way: - -```bash -clingexplaid examples/misc/simple.lp --muc 0 -``` - -This converts all facts of the program to choices and assumptions and returns -the contained MUC from that. - -``` -MUC 1 -b(5) a(5) -``` - -A selection of more examples can be found [here](examples) - ## API Here are two example for using `clingexplaid`'s API. diff --git a/example_mus.png b/example_mus.png deleted file mode 100644 index 43524fb..0000000 Binary files a/example_mus.png and /dev/null differ diff --git a/example_show_decisions.png b/example_show_decisions.png deleted file mode 100644 index d0c256c..0000000 Binary files a/example_show_decisions.png and /dev/null differ diff --git a/pyproject.toml b/pyproject.toml index d3553ea..35323c5 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -20,7 +20,6 @@ readme = "README.md" dependencies = [ "clingo>=5.7.1", "autoflake", - "textual==0.65.1", ] classifiers = [ "Development Status :: 4 - Beta", @@ -51,9 +50,6 @@ test = [ "coverage[toml]" ] doc = [ "sphinx", "furo", "nbsphinx", "sphinx_copybutton", "myst-parser" ] dev = [ "clingexplaid[test,typecheck,lint_pylint]" ] -[project.scripts] -clingexplaid = "clingexplaid.__main__:main" - [tool.setuptools.packages.find] where = ["src"] @@ -97,8 +93,6 @@ good-names = ["_"] [tool.coverage.run] source = ["clingexplaid", "tests"] omit = [ - "*/clingexplaid/__main__.py", - "*/clingexplaid/cli/*", "*/clingexplaid/propagators/*", "*/clingexplaid/transformers/__init__.py", "*/clingexplaid/muc/__init__.py", diff --git a/src/clingexplaid/__main__.py b/src/clingexplaid/__main__.py deleted file mode 100644 index 7bd17d7..0000000 --- a/src/clingexplaid/__main__.py +++ /dev/null @@ -1,27 +0,0 @@ -""" -The main entry point for the application. -""" - -import sys - -from clingo.application import clingo_main - -from .cli.clingo_app import ClingoExplaidApp -from .cli.textual_gui import textual_main - -RUN_TEXTUAL_GUI = False - - -def main() -> None: - """ - Run the main function. - """ - - if RUN_TEXTUAL_GUI: - textual_main() - else: - clingo_main(ClingoExplaidApp(sys.argv[0]), sys.argv[1:] + ["-V0"]) - - -if __name__ == "__main__": - main() diff --git a/src/clingexplaid/cli/__init__.py b/src/clingexplaid/cli/__init__.py deleted file mode 100644 index e69de29..0000000 diff --git a/src/clingexplaid/cli/clingo_app.py b/src/clingexplaid/cli/clingo_app.py deleted file mode 100644 index 83fdb00..0000000 --- a/src/clingexplaid/cli/clingo_app.py +++ /dev/null @@ -1,340 +0,0 @@ -""" -App Module: clingexplaid CLI clingo app -""" - -import re -import sys -from importlib.metadata import version -from pathlib import Path -from typing import Callable, Dict, List, Optional, Sequence, Set, Tuple -from warnings import warn - -import clingo -from clingo.application import Application, Flag - -from ..mus import CoreComputer -from ..transformers import AssumptionTransformer, OptimizationRemover -from ..unsat_constraints import UnsatConstraintComputer -from ..utils import get_constant_string, get_constants_from_arguments -from ..utils.logging import BACKGROUND_COLORS, COLORS -from .textual_gui import ClingexplaidTextualApp - -HYPERLINK_MASK = "\033]8;{};{}\033\\{}\033]8;;\033\\" - - -class ClingoExplaidApp(Application): - """ - Application class for executing clingo-explaid functionality on the command line - """ - - # pylint: disable = too-many-instance-attributes - - CLINGEXPLAID_METHODS = { - "mus": "Description for MUS method", - "unsat-constraints": "Description for unsat-constraints method", - "interactive": "Interactive terminal user interface to interact with all modes", - } - - def __init__(self, name: str) -> None: - # pylint: disable = unused-argument - self.methods: Set[str] = set() - self.method_functions: Dict[str, Callable] = { # type: ignore - m: getattr(self, f'_method_{m.replace("-", "_")}') for m in self.CLINGEXPLAID_METHODS - } - self.method_flags: Dict[str, Flag] = {m: Flag() for m in self.CLINGEXPLAID_METHODS} - self.argument_constants: Dict[str, str] = {} - - # SHOW DECISIONS - self._show_decisions_decision_signatures: Dict[str, int] = {} - self._show_decisions_model_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 - for method, flag in self.method_flags.items(): - if flag.flag: - self.methods.add(method) - - if len(self.methods) == 0: - raise ValueError( - f"Clingexplaid was called without any method, please select at least one of the following methods: " - f"[{', '.join(['--' + str(m) for m in self.CLINGEXPLAID_METHODS])}]" - ) - - @staticmethod - def _parse_signature(signature_string: str) -> Tuple[str, int]: - match_result = re.match(r"^([a-zA-Z]+)/([0-9]+)$", signature_string) - if match_result is None: - raise ValueError("Wrong signature Format") - return match_result.group(1), int(match_result.group(2)) - - def _parse_assumption_signature(self, assumption_signature: str) -> bool: - 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: - signature, arity = self._parse_signature(assumption_signature_string) - except ValueError: - print( - "PARSE ERROR: Wrong signature format. The assumption signatures have to follow the format " - "/" - ) - return False - self._mus_assumption_signatures[signature] = arity - return True - - def _parse_decision_signature(self, decision_signature: str) -> bool: - if not self.method_flags["show-decisions"]: - print( - "PARSE ERROR: The decision signature option is only available if the flag --show-decisions is enabled" - ) - return False - decision_signature_string = decision_signature.replace("=", "").strip() - try: - signature, arity = self._parse_signature(decision_signature_string) - except ValueError: - print( - "PARSE ERROR: Wrong signature format. The decision signatures have to follow the format " - "/" - ) - return False - self._show_decisions_decision_signatures[signature] = arity - return True - - def register_options(self, options: clingo.ApplicationOptions) -> None: - group = "Clingo-Explaid Methods" - - for method, description in self.CLINGEXPLAID_METHODS.items(): - options.add_flag( - group=group, - option=f"{method},{method[0]}", # only works when none of the method's initial letter don't overlap - description=description, - target=self.method_flags[method], - ) - - group = "MUS Options" - - options.add( - group, - "assumption-signature,a", - "Facts matching with this signature will be converted to assumptions for finding a MUS " - "(default: all facts)", - self._parse_assumption_signature, - multi=True, - ) - - group = "Show Decisions Options" - - options.add( - group, - "decision-signature", - "When --show-decisions is enabled, show only decisions matching with this signature " - "(default: show all decisions)", - self._parse_decision_signature, - multi=True, - ) - - # group = "General Options" - - def _apply_assumption_transformer( - self, signatures: Dict[str, int], files: List[str] - ) -> Tuple[str, AssumptionTransformer]: - 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("-") - else: - program_transformed = at.parse_files(files) - return program_transformed, at - - 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_mus( - self, - control: clingo.Control, - files: List[str], - compute_unsat_constraints: bool = False, - ) -> None: - program_transformed, at = self._apply_assumption_transformer( - signatures=self._mus_assumption_signatures, files=files - ) - - # remove optimization statements - optr = OptimizationRemover() - program_transformed = optr.parse_string(program_transformed) - - control.add("base", [], program_transformed) - control.ground([("base", [])]) - - assumptions = at.get_assumption_literals( - control, constants=[get_constant_string(c, v, prefix="-c ") for c, v in self.argument_constants.items()] - ) - cc = CoreComputer(control, assumptions) - - max_models = int(control.configuration.solve.models) # type: ignore - print("Solving...") - - # Case: Finding a single MUS - if max_models == -1: - - 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") - return - if len(list(cc.minimal)) == 0: - print( - "NO MUS CONTAINED: The unsatisfiability of this program is not induced by the provided assumptions" - ) - return - - 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=mus_string, - output_prefix_active=f"{COLORS['RED']}├──{COLORS['NORMAL']}", - ) - - # Case: Finding multiple MUS - if max_models >= 0: - program_unsat = False - with control.solve(assumptions=list(assumptions), yield_=True) as solve_handle: - if not solve_handle.get().satisfiable: - program_unsat = True - - if program_unsat: - 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=mus_string, - output_prefix_active=f"{COLORS['RED']}├──{COLORS['NORMAL']}", - ) - if not n_mus: - print( - "NO MUS CONTAINED: The unsatisfiability of this program is not induced by the provided " - "assumptions" - ) - return - - def _print_unsat_constraints( - self, - unsat_constraints: Dict[int, str], - ucc: UnsatConstraintComputer, - prefix: Optional[str] = None, - ) -> None: - if prefix is None: - prefix = "" - print(f"{prefix}{BACKGROUND_COLORS['RED']} Unsat Constraints {COLORS['NORMAL']}") - for cid, constraint in unsat_constraints.items(): - location = ucc.get_constraint_location(cid) - if location is None: - warn(f"Couldn't find a corresponding file for constraint with id {cid}") - continue - relative_file_path = location.begin.filename - absolute_file_path = str(Path(relative_file_path).absolute().resolve()) - line_beginning = location.begin.line - line_end = location.end.line - line_string = ( - f"Line {line_beginning}" if line_beginning == line_end else f"Lines {line_beginning}-{line_end}" - ) - file_link = "file://" + absolute_file_path - if " " in absolute_file_path: - # If there's a space in the filename use a hyperlink - file_link = HYPERLINK_MASK.format("", file_link, file_link) - - if location is not None: - print( - f"{prefix}{COLORS['RED']}{constraint}" - f"{COLORS['GREY']} [ {file_link} ]({line_string}){COLORS['NORMAL']}" - ) - else: - print(f"{prefix}{COLORS['RED']}{constraint}{COLORS['NORMAL']}") - - def _method_unsat_constraints( - self, - control: clingo.Control, - files: List[str], - assumption_string: Optional[str] = None, - output_prefix_active: str = "", - ) -> None: - ucc = UnsatConstraintComputer(control=control) - ucc.parse_files(files) - unsat_constraints = ucc.get_unsat_constraints(assumption_string=assumption_string) - self._print_unsat_constraints(unsat_constraints, ucc=ucc, prefix=output_prefix_active) - - def _print_model( - self, - model: clingo.Model, - prefix_active: str = "", - prefix_passive: str = "", - ) -> None: - print(prefix_passive) - print( - f"{prefix_active}" - f"{BACKGROUND_COLORS['LIGHT-GREY']}{COLORS['BLACK']} Model {COLORS['NORMAL']}{BACKGROUND_COLORS['GREY']} " - f"{self._show_decisions_model_id} {COLORS['NORMAL']} " - f"{model}" - ) - # print(f"{COLORS['BLUE']}{model}{COLORS['NORMAL']}") - print(prefix_passive) - self._show_decisions_model_id += 1 - - def _method_interactive( - self, - control: clingo.Control, - files: List[str], - ) -> None: - print(control) # only for pylint - - app = ClingexplaidTextualApp(files=files, constants={}) - app.run() - - def print_model(self, model: clingo.Model, _) -> None: # type: ignore - return - - def main(self, control: clingo.Control, files: Sequence[str]) -> None: - print("clingexplaid", "version", version("clingexplaid")) - self._initialize() - - # printing the input files - if not files: - print("Reading from -") - else: - print(f"Reading from {files[0]} {'...' if len(files) > 1 else ''}") - - self.argument_constants = get_constants_from_arguments(sys.argv) - - # standard case: only one method - if len(self.methods) == 1: - method = list(self.methods)[0] - method_function = self.method_functions[method] - method_function(control, files) - # special cases where specific pipelines have to be configured - elif self.methods == {"mus", "unsat-constraints"}: - self.method_functions["mus"](control, files, compute_unsat_constraints=True) - else: - print( - f"METHOD ERROR: the combination of the methods {[f'--{m}' for m in self.methods]} is invalid. " - f"Please remove the conflicting method flags" - ) diff --git a/src/clingexplaid/cli/textual_gui.py b/src/clingexplaid/cli/textual_gui.py deleted file mode 100644 index cac4d12..0000000 --- a/src/clingexplaid/cli/textual_gui.py +++ /dev/null @@ -1,876 +0,0 @@ -""" -Module for a Command Line based GUI for clingexplaid -""" - -import argparse -import asyncio -import itertools -import re -from enum import Enum -from pathlib import Path -from typing import Any, Callable, Dict, Iterable, List, Optional, Set, Tuple, Union, cast - -import clingo -from rich.text import Text -from textual import on -from textual.app import App, ComposeResult -from textual.containers import Horizontal, HorizontalScroll, Vertical, VerticalScroll -from textual.screen import Screen -from textual.validation import Number -from textual.widget import Widget -from textual.widgets import ( - Button, - Checkbox, - Footer, - Input, - Label, - LoadingIndicator, - Select, - Static, - TabbedContent, - TabPane, - TextArea, - Tree, -) -from textual.widgets.tree import TreeNode - -from ..mus import CoreComputer -from ..propagators import SolverDecisionPropagator -from ..propagators.propagator_solver_decisions import INTERNAL_STRING, Decision -from ..transformers import AssumptionTransformer, OptimizationRemover -from ..unsat_constraints import UnsatConstraintComputer -from .textual_style import MAIN_CSS - -ACTIVE_CLASS = "active" - -COLORS = { - "BLACK": "#000000", - "GRAY-DARK": "#666666", - "GRAY": "#999999", - "GRAY-LIGHT": "#CCCCCC", - "RED": "#E53935", -} - - -class Modes(Enum): - """Representation of the Clingo-Explaid Modes""" - - MODE_MUS = "Minimal Unsatisfiable Subsets" - MODE_UNSAT_CONSTRAINTS = "Unsatisfiable Constraints" - MODE_SHOW_DECISIONS = "Show Decisions" - MODE_EXPLAIN = "Explain" - - -MODES = ( - Modes.MODE_EXPLAIN, - Modes.MODE_MUS, - Modes.MODE_UNSAT_CONSTRAINTS, - Modes.MODE_SHOW_DECISIONS, -) - - -class NoFilesException(Exception): - """ - Exception raised if a method requiring input files is called without any - """ - - -class ModelType(Enum): - """ - Types of Model that can be found (Stable Model, MUS, ...) - """ - - MODEL = 1 - UNSAT_CONSTRAINT = 2 - MUS = 3 - - -def read_file(path: Union[Path, str]) -> str: - """ - Helper function to get the contents of a file as a string. - """ - file_content = "" - with open(path, "r", encoding="utf-8") as f: - file_content = f.read() - return file_content - - -def flatten_list(ls: Optional[List[List[Any]]]) -> List[Any]: - """ - Helper function to flatten a list - """ - if ls is None: - ls = [] - return list(itertools.chain.from_iterable(ls)) - - -def parse_constants(constant_strings: List[str]) -> Dict[str, str]: - """ - Helper function to parse constants - """ - constants = {} - for const_string in constant_strings: - result = re.search(r"(^[a-zA-Z_][a-zA-Z0-9_]*)=([a-zA-Z_][a-zA-Z0-9_]*|[0-9]+)$", const_string) - if result is not None: - constants[result.group(1)] = result.group(2) - return constants - - -class SelectorWidget(Static): - """SelectorWidget Field""" - - def __init__(self, compose_widgets: List[Widget], update_value_function: Callable[[Any], str]) -> None: - super().__init__() - self.compose_widgets = compose_widgets - self.active = True - self.value = "" - self.update_value_function = update_value_function - # this is used when the value of the checkbox is set by the system to avoid the changed event callback - self.skip_checkbox_changed = False - - self.set_active_class() - - def set_active(self, active: bool) -> None: - """ - Sets the active property to the provided value while updating the Selector's style - """ - self.active = active - self.skip_checkbox_changed = True - self.query_one(Checkbox).value = active - if self.active: - self.apply_value_function() - self.set_active_class() - - def apply_value_function(self) -> None: - """ - Applies the on __init__ provided `update_value_function` to compute `SelectorWidget.value` - """ - self.value = self.update_value_function(self) - - def set_active_class(self) -> None: - """ - Sets the active class of the `SelectorWidget` according to `SelectorWidget.active` - """ - if self.active: - if ACTIVE_CLASS not in self.classes: - self.add_class(ACTIVE_CLASS) - else: - self.remove_class(ACTIVE_CLASS) - - def compose(self) -> ComposeResult: - """ - Composes the `SelectorWidget`'s components - """ - yield Checkbox(value=True) - yield from self.compose_widgets - - @on(Checkbox.Changed) - async def selector_changed(self, event: Checkbox.Changed) -> None: - """ - Callback for when the `SelectorWidget`'s Checkbox is changed. - """ - # Updating the UI to show the reasons why validation failed - if event.checkbox == self.query_one(Checkbox): - if self.skip_checkbox_changed: - self.skip_checkbox_changed = False - else: - self.active = event.checkbox.value - self.set_active_class() - await self.run_action("app.update_config") - - -class LabelInputWidget(SelectorWidget): - """LabelInputWidget Field""" - - def __init__(self, name: str, value: str, update_value_function: Callable[[SelectorWidget], str]) -> None: - super().__init__( - compose_widgets=[ - Label(name), - Input(placeholder="Value", value=value), - ], - update_value_function=update_value_function, - ) - - -class LabelWidget(SelectorWidget): - """LabelWidget Field""" - - def __init__(self, path: str, update_value_function: Callable[[SelectorWidget], str]) -> None: - super().__init__( - compose_widgets=[ - HorizontalScroll(Label(path)), - ], - update_value_function=update_value_function, - ) - - -class SelectorList(Static): - """Widget for selecting the program files""" - - def __init__(self, selectors: Optional[Iterable[Any]], classes: str = "") -> None: - super().__init__(classes=classes) - self.add_class("selectors") - if selectors is None: - selectors = [] - self.selectors = selectors - - def get_selectors(self) -> List[SelectorWidget]: - """ - Base function for getting selectors. This should be overwritten in any classes that inherit from this class. - """ - return [] - - def compose(self) -> ComposeResult: - """ - Composes the `SelectorList`'s components - """ - yield VerticalScroll( - *self.get_selectors(), - ) - - -class ConstantsWidget(SelectorList): - """List Widget for Constants""" - - def __init__(self, constants: Optional[Dict[str, str]]) -> None: - super().__init__(selectors={} if constants is None else constants) - - def get_selectors(self) -> List[SelectorWidget]: - """ - Fill the `ConstantsWidget` with `LabelInputWidget`s for each constant. - """ - return [ - LabelInputWidget(name, value, update_value_function=self.update_value) - for name, value in dict(self.selectors).items() - ] - - @staticmethod - def update_value(selector_object: SelectorWidget) -> str: - """ - Updates the value for each constant with its name and value - """ - label_string = str(selector_object.query_one(Label).renderable).strip() - input_string = str(selector_object.query_one(Input).value).strip() - return f"#const {label_string}={input_string}." - - -class FilesWidget(SelectorList): - """List Widget for Files""" - - def __init__(self, files: Optional[List[str]]) -> None: - super().__init__(selectors=[] if files is None else files) - - def get_selectors(self) -> List[SelectorWidget]: - """ - Fill the `FilesWidget` with `LabelWidget`s for each file. - """ - return [LabelWidget(name, update_value_function=self.update_value) for name in self.selectors] - - @staticmethod - def update_value(selector_object: SelectorWidget) -> str: - """ - Updates the value for each file with its name - """ - label_string = str(selector_object.query_one(Label).renderable).strip() - return label_string - - -class SignaturesWidget(SelectorList): - """List Widget for Signatures""" - - def __init__(self, signatures: Optional[List[str]]) -> None: - super().__init__(selectors=[] if signatures is None else signatures) - - def get_selectors(self) -> List[SelectorWidget]: - """ - Fill the `SignaturesWidget` with `LabelWidget`s for each signature. - """ - return [LabelWidget(name, update_value_function=self.update_value) for name in self.selectors] - - @staticmethod - def update_value(selector_object: SelectorWidget) -> str: - """ - Updates the value for each file with its name and arity - """ - label_string = str(selector_object.query_one(Label).renderable).strip() - return label_string - - -class Sidebar(Static): - """Widget for the clingexplaid sidebar""" - - def __init__( - self, - files: List[str], - constants: Optional[Dict[str, str]], - classes: str = "", - ) -> None: - super().__init__(classes=classes) - self.files = files - self.constants = {} if constants is None else constants - self.signatures = self.get_all_program_signatures() - - def get_all_program_signatures(self) -> Set[Tuple[str, int]]: - """ - Get all signatures occurring in all files provided. - """ - # This is done with grounding rn but doing a text processing would probably be more efficient for large - # programs! - ctl = clingo.Control() - for file in self.files: - ctl.load(file) - ctl.ground([("base", [])]) - return {(name, arity) for name, arity, _ in ctl.symbolic_atoms.signatures} - - def compose(self) -> ComposeResult: - """ - Composes the `Sidebar`'s components - """ - with TabbedContent(): - with TabPane("Files", id="tab-files"): - yield FilesWidget(self.files) - # with TabPane("Constants", id="tab-constants"): - # yield ConstantsWidget(self.constants) - with TabPane("Signatures", id="tab-signatures"): - sorted_signatures = list(sorted(self.signatures, key=lambda x: x[0])) - yield SignaturesWidget([INTERNAL_STRING] + [f"{name} / {arity}" for name, arity in sorted_signatures]) - - -class ControlPanel(Static): - """Widget for the clingexplaid sidebar""" - - def __init__(self, classes: str = ""): - super().__init__(classes=classes) - self.input_valid = True - - def compose(self) -> ComposeResult: - """ - Composes the `ControlPanel`'s components - """ - yield Label("Mode") - yield Select( - ((line.value, line.value) for line in MODES), - allow_blank=False, - id="mode-select", - ) - yield Label("Models") - yield Input( - placeholder="Number", - type="number", - value="1", - validate_on=["changed"], - validators=[Number(minimum=0)], - id="model-number-input", - ) - yield Static(classes="error") - yield Label("", classes="error") - yield Button("SOLVE", id="solve-button", variant="primary") - - @on(Select.Changed) - async def select_changed(self, event: Select.Changed) -> None: - """ - Callback for when the `ControlPanel`'s Mode Select is changed. - """ - if event.select == self.query_one("#mode-select"): - await self.run_action("app.update_mode") - - @on(Input.Changed) - async def input_changed(self, event: Input.Changed) -> None: - """ - Callback for when the `ControlPanel`'s Input is changed. - """ - # Updating the UI to show the reasons why validation failed - if event.input == self.query_one("#model-number-input"): - if event.validation_result is None: - return - self.input_valid = event.validation_result.is_valid - if not self.input_valid: - self.add_class("error") - first_error = event.validation_result.failure_descriptions[0] - cast(Label, self.query_one("Label.error")).update(first_error) - else: - self.remove_class("error") - cast(Label, self.query_one("Label.error")).update("") - await self.run_action("app.update_config") - - @on(Input.Submitted) - async def input_submitted(self, event: Input.Submitted) -> None: - """ - Callback for when the `ControlPanel`'s Input is submitted. - """ - if event.input == self.query_one("#model-number-input"): - if self.input_valid: - await self.run_action("app.solve") - - @on(Button.Pressed) - async def solve(self, event: Button.Pressed) -> None: - """ - Callback for when the `ControlPanel`'s Button is changed. - """ - if event.button == self.query_one("#solve-button"): - await self.run_action("app.solve") - - -class SolverTreeView(Static): - """Widget for the clingexplaid show decisions tree""" - - def __init__(self, classes: str = "") -> None: - super().__init__(classes=classes) - self.solve_tree: Tree[str] = Tree("Solver Decisions", id="explanation-tree") - - def compose(self) -> ComposeResult: - """ - Composes the `SolverTreeView`'s components - """ - self.solve_tree.root.expand() - yield self.solve_tree - yield LoadingIndicator() - - -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 - - def __init__(self, files: List[str], constants: Dict[str, str]) -> None: - super().__init__() - self.files = files - self.constants = constants - self.tree_cursor: Optional[TreeNode[str]] = None - self.model_count = 0 - - self._selected_mode: Optional[str] = None - self._config_model_number = 1 - self._config_show_internal = True - self._loaded_files: Set[str] = set() - self._loaded_signatures: Set[Tuple[str, int]] = set() - - self.bind("ctrl+x", "exit", description="Exit", key_display="CTRL+X") - - def compose(self) -> ComposeResult: - """ - Composes the `ClingexplaidTextualApp`'s components - """ - yield Vertical( - ControlPanel(classes="box"), - Sidebar(files=self.files, constants=self.constants, classes="box tabs"), - id="top-cell", - ) - input_answer_set = TextArea() - input_answer_set.border_title = "Answer Set" - input_query_atoms = TextArea() - input_query_atoms.border_title = "Query Atoms" - - yield Vertical( - VerticalScroll(SolverTreeView(), classes="box"), - Horizontal( - input_answer_set, - input_query_atoms, - classes="box", - id="explanation-inputs", - ), - id="content", - ) - yield Label(id="debug") - yield Footer() - - def action_exit(self) -> None: - """ - Action to exit the textual application - """ - self.exit(0) - - async def on_model(self, model: List[str]) -> None: - """ - Callback for when clingo finds a model. - """ - self.model_count += 1 - if self.tree_cursor is None: - return - await self.add_model_node(" ".join(model), ModelType.MODEL) - # add some small sleep time to make ux seem more interactive - await asyncio.sleep(0.01) - - def on_propagate(self, decisions: List[Union[Decision, List[Decision]]]) -> None: - """ - Callback for the registered propagator does a propagate step. - """ - if self.tree_cursor is None: - return - for element in decisions: - if isinstance(element, list): - for literal in element: - if literal.matches_any(self._loaded_signatures, show_internal=self._config_show_internal): - entailment = self.tree_cursor.add_leaf(str(literal)).expand() - cast(Text, entailment.label).stylize(COLORS["GRAY-DARK"]) - else: - new_node = self.tree_cursor.add(str(element)) - new_node.expand() - self.tree_cursor = new_node - - def on_undo(self) -> None: - """ - Callback for the registered propagator does an undo step. - """ - if self.tree_cursor is None: - return - undo = self.tree_cursor.add_leaf(f"UNDO {self.tree_cursor.label}") - cast(Text, undo.label).stylize(COLORS["RED"]) - self.tree_cursor = self.tree_cursor.parent - - async def action_update_config(self) -> None: - """ - Action to update the solving config - """ - self.refresh_bindings() - - # update model number - model_number_input = cast(Input, self.query_one("#model-number-input")) - model_number = int(model_number_input.value) - self._config_model_number = model_number - - # update loaded files - files_widget = self.query_one(FilesWidget) - files = set() - for selector in files_widget.query(SelectorWidget): - selector.apply_value_function() - if selector.active: - files.add(selector.value) - self._loaded_files = files - - # update program signatures - signatures_widget = self.query_one(SignaturesWidget) - signature_strings = set() - for selector in signatures_widget.query(SelectorWidget): - selector.apply_value_function() - if selector.active: - signature_strings.add(selector.value) - signatures = set() - self._config_show_internal = False - for signature_string in signature_strings: - if signature_string.startswith(INTERNAL_STRING): - self._config_show_internal = True - else: - name, arity = signature_string.split(" / ") - signatures.add((name, int(arity))) - self._loaded_signatures = signatures - - async def action_mode_mus(self) -> None: - """ - Action for MUS Mode - """ - if not self._loaded_files: - raise NoFilesException("No files are loaded so there is no MUS to be found") - - ctl = clingo.Control() - - # transform matching facts to choices to allow assumptions - at = AssumptionTransformer(signatures=self._loaded_signatures) - program_transformed = at.parse_files(list(self._loaded_files)) - - # remove optimization statements - opt_rm = OptimizationRemover() - program_no_opt = opt_rm.parse_string(program_transformed) - - ctl.add("base", [], program_no_opt) - ctl.ground([("base", [])]) - - # get assumption set - assumptions = at.get_assumption_literals(ctl) - # FIX: add program constants - # get_constant_string(c, v, prefix="-c ") for c, v in self.argument_constants.items() - - cc = CoreComputer(ctl, assumptions) - - # check if the program is unsat - program_unsat = False - with ctl.solve(assumptions=list(assumptions), yield_=True) as solve_handle: - if not solve_handle.get().satisfiable: - program_unsat = True - - tree_cursor = await self.get_tree_cursor() - if not program_unsat: - tree_cursor.add_leaf("SATISFIABLE PROGRAM") - return - - for mus in cc.get_multiple_minimal(max_mus=self._config_model_number): - self.model_count += 1 - mus_string = " ".join(cc.mus_to_string(mus)) - await self.add_model_node(mus_string, ModelType.MUS) - - if not self.model_count: - tree_cursor.add_leaf( - "NO MUS CONTAINED: The unsatisfiability of this program is not induced by the provided assumptions" - ) - - async def action_mode_unsat_constraints(self) -> None: - """ - Action for Unsat Constraints Mode - """ - control = clingo.Control() - ucc = UnsatConstraintComputer(control=control) - ucc.parse_files(list(self._loaded_files)) - unsat_constraints = ucc.get_unsat_constraints() - - for cid, constraint in unsat_constraints.items(): - self.model_count += 1 - location = ucc.get_constraint_location(cid) - if location is None: - await self.add_model_node("UNKNOWN CONSTRAINT LOCATION", ModelType.UNSAT_CONSTRAINT) - continue - relative_file_path = location.begin.filename - absolute_file_path = str(Path(relative_file_path).absolute().resolve()) - line_beginning = location.begin.line - line_end = location.end.line - constraint_string = constraint - line_string = ( - f" (line {line_beginning})" if line_beginning == line_end else f" (lines {line_beginning}-{line_end})" - ) - constraint_string += line_string - node = await self.add_model_node(constraint_string, ModelType.UNSAT_CONSTRAINT) - if node is not None: - cast(Text, node.label).stylize(COLORS["GRAY-DARK"], -len(line_string)) - node.expand() - node.add_leaf(f"File: {absolute_file_path}") - - async def action_mode_show_decisions(self) -> None: - """ - Action for Show Decisions Mode - """ - sdp = SolverDecisionPropagator( - callback_propagate=self.on_propagate, - callback_undo=self.on_undo, - ) - ctl = clingo.Control(f"{self._config_model_number}") - ctl.register_propagator(sdp) - for file in self._loaded_files: - ctl.load(file) - if not self._loaded_files: - ctl.add("base", [], "") - ctl.ground([("base", [])]) - - exhausted = False - - with ctl.solve(yield_=True) as solver_handle: - while not exhausted: - result = solver_handle.get() - if result.satisfiable: - model = solver_handle.model() - if model is None: - break - await self.on_model([str(a) for a in model.symbols(atoms=True)]) - exhausted = result.exhausted - if not exhausted: - solver_handle.resume() - - await self.reset_tree_cursor() - end_string = "SAT" if self.model_count > 0 else "UNSAT" - if self.tree_cursor is None: - return - self.tree_cursor.add(end_string) - - async def action_mode_explain(self) -> None: - """Action for Explain Mode""" - # Add implementation - - async def action_solve(self) -> None: - """ - Action to exit the textual application - """ - self.refresh_bindings() - - tree_view = self.query_one(SolverTreeView) - tree = tree_view.solve_tree - await self.reset_solve_tree(str(tree.root.label)) - - solve_button = self.query_one("#solve-button") - - self.model_count = 0 - - solve_button.disabled = True - tree_view.add_class("solving") - - match self._selected_mode: - case Modes.MODE_MUS.value: - try: - await self.action_mode_mus() - except NoFilesException as e: - tree_cursor = await self.get_tree_cursor() - tree_cursor.add_leaf(e.args[0]) - case Modes.MODE_UNSAT_CONSTRAINTS.value: - await self.action_mode_unsat_constraints() - case Modes.MODE_SHOW_DECISIONS.value: - await self.action_mode_show_decisions() - case Modes.MODE_EXPLAIN.value: - await self.action_mode_explain() - - tree_view.remove_class("solving") - solve_button.disabled = False - - await self.reset_tree_cursor() - - async def action_update_mode(self) -> None: - """ - Action that updates the currently selected mode - """ - selected_mode = cast(Select[str], self.query_one("#mode-select")).value - self._selected_mode = str(selected_mode) - match selected_mode: - case Modes.MODE_MUS.value: - self.set_mode_class(self.query_one(Screen), "mode-mus") - await self.set_all_selectors(self.query_one(SignaturesWidget), False) - await self.reset_solve_tree("Minimal Unsatisfiable Subsets") - await self.update_selector_tabs(disabled=["tab-constants"]) - case Modes.MODE_UNSAT_CONSTRAINTS.value: - self.set_mode_class(self.query_one(Screen), "mode-unsat-constraints") - await self.reset_solve_tree("Unsatisfiable Constraints") - await self.update_selector_tabs(disabled=["tab-constants", "tab-signatures"]) - case Modes.MODE_SHOW_DECISIONS.value: - self.set_mode_class(self.query_one(Screen), "mode-show-decisions") - await self.set_all_selectors(self.query_one(SignaturesWidget), True) - await self.reset_solve_tree("Solver Decisions") - await self.update_selector_tabs(disabled=["tab-constants"]) - case Modes.MODE_EXPLAIN.value: - self.set_mode_class(self.query_one(Screen), "mode-explain") - await self.reset_solve_tree("Explanation") - - async def action_debug(self, msg: str) -> None: - """ - Action to add a leaf with custom message to the solve tree for debugging purposes - """ - tree_cursor = await self.get_tree_cursor() - tree_cursor.add_leaf(f"DEBUG: {msg}") - - @staticmethod - def set_mode_class(widget: Widget, mode_class: str) -> None: - """ - Sets the provided mode class on the provided widget - """ - mode_classes = [c for c in widget.classes if c.startswith("mode-")] - for c in mode_classes: - widget.remove_class(c) - widget.add_class(mode_class) - - @staticmethod - async def set_all_selectors(parent: Widget, value: bool) -> None: - """ - Sets the values of all SelectorWidgets under the provided parent to value - """ - for selector in parent.query(SelectorWidget): - selector.set_active(value) - selector.skip_checkbox_changed = False - - async def add_model_node(self, value: str, model_type: ModelType) -> Optional[TreeNode[str]]: - """ - Adds a model node of type model_type to the solver tree - """ - match model_type: - case ModelType.MODEL: - color_fg, color_bg_1, color_bg_2 = (COLORS["BLACK"], COLORS["GRAY-LIGHT"], COLORS["GRAY"]) - case ModelType.UNSAT_CONSTRAINT: - color_fg, color_bg_1, color_bg_2 = ("#f27573", "#7c1313", "#610f0f") - case ModelType.MUS: - color_fg, color_bg_1, color_bg_2 = ("#66bdff", "#004578", "#003761") - case _: - raise ValueError("Model type not supported") - - model_name = model_type.name.replace("_", " ") - tree_cursor = await self.get_tree_cursor() - model_node = tree_cursor.add(f" {model_name} {self.model_count} {value}") - cast(Text, model_node.label).stylize(f"{color_fg} on {color_bg_1}", 0, len(model_name) + 2) - cast(Text, model_node.label).stylize( - f"{color_fg} on {color_bg_2}", len(model_name) + 2, len(model_name) + 4 + len(str(self.model_count)) - ) - return model_node - - async def reset_tree_cursor(self) -> None: - """ - Resets the tree cursor to the SolverTree root - """ - tree_view = self.query_one(SolverTreeView) - tree = tree_view.solve_tree - self.tree_cursor = tree.root - - async def reset_solve_tree(self, new_root_name: str) -> None: - """ - Resets the SolverTree - """ - tree_view = self.query_one(SolverTreeView) - tree = tree_view.solve_tree - tree.reset(new_root_name) - self.tree_cursor = tree.root - - async def get_tree_cursor(self) -> TreeNode[str]: - """ - Returns the current tree cursor or initializes it if it is set to None - """ - if self.tree_cursor is None: - self.tree_cursor = self.query_one(SolverTreeView).solve_tree.root - return self.tree_cursor - - async def update_selector_tabs(self, disabled: Optional[Iterable[str]] = None) -> None: - """ - Updates the selector tabs in the Sidebar depending on the provided `disabled` list. - """ - if disabled is None: - disabled = [] - sidebar = self.query_one(Sidebar) - tabbed_content = sidebar.query_one(TabbedContent) - tabs = sidebar.query(TabPane) - for tab in tabs: - if tab.id is None: - continue - if tab.id in disabled: - tab.disabled = True - else: - tab.disabled = False - if tabbed_content.active in disabled: - tabbed_content.active = str(tabs[0].id) - - def check_action(self, action: str, parameters: tuple[object, ...]) -> bool | None: - """ - Check if any action may run - """ - return True - - -def textual_main() -> None: - """ - Main function for the clingo-explaid textual app. This function includes a dedicated ArgumentParser - """ - - parser = argparse.ArgumentParser(prog="clingexplaid", description="What the program does", epilog="Epilog Text") - parser.add_argument( - "files", - type=str, - nargs="+", - action="append", - help="All logic program files", - ) - parser.add_argument( - "-c", - "--const", - type=str, - nargs="*", - action="append", - help="Specifies a clingo constant value", - ) - parser.add_argument( - "-d", - "--decision-signature", - type=str, - nargs="*", - action="append", - help="Defines shown signatures in solver decision tree", - ) - args = parser.parse_args() - - app = ClingexplaidTextualApp( - files=list(set(flatten_list(args.files))), - constants=parse_constants(flatten_list(args.const)), - ) - app.run() diff --git a/src/clingexplaid/cli/textual_style.py b/src/clingexplaid/cli/textual_style.py deleted file mode 100644 index a64050b..0000000 --- a/src/clingexplaid/cli/textual_style.py +++ /dev/null @@ -1,167 +0,0 @@ -""" -Module containing TCSS style strings for the textual TUI -""" - -MAIN_CSS = """ -Screen { - layout: grid; - grid-size: 2 2; - grid-columns: 1fr 2fr; - grid-rows: 1fr auto; -} - -#debug{ - column-span: 2; -} - -.box { - height: 100%; - border: round #455A64; - padding: 1; -} - -.box.tabs{ - padding: 0; -} - -#top-cell { - layout: grid; - grid-size: 1; - grid-rows: auto 1fr; -} - -ControlPanel { - layout: grid; - grid-size: 2; - grid-columns: auto 1fr; - grid-gutter: 1; -} - -ControlPanel Input{ - width: 100%; -} - -ControlPanel Label { - padding: 1 2; - background: #263238; - width: 100%; -} - -ControlPanel Label.error{ - border: tall rgb(235,64,52); - background: rgba(235,64,52,0.2); - padding: 0 2; - color: rgb(235,64,52); -} - -ControlPanel .error{ - display: none; -} - -ControlPanel.error .error{ - display: block -} - -ControlPanel #solve-button{ - column-span: 2; - width: 100%; -} - -ControlPanel.error #solve-button{ - display: none; -} - -ControlPanel #solve-button{ - display: block; - width: 100%; -} - -.selectors{ - background: #000; -} - -SelectorWidget{ - layout: grid; - grid-size: 2; - grid-columns: auto 1fr; -} - -LabelInputWidget{ - layout: grid; - grid-size: 3; - grid-columns: auto 1fr 1fr; -} - -SelectorWidget{ - background: transparent; -} - -SelectorWidget.active{ - background: $primary-darken-3; -} - -SelectorWidget Label{ - padding: 1; -} - -SelectorWidget Checkbox{ - background: transparent; -} - -SelectorWidget Input{ - border: none; - padding: 1 2; -} - -SelectorWidget HorizontalScroll{ - height: auto; - background: transparent; -} - -SolverTreeView{ - content-align: center middle; -} - -SolverTreeView Tree{ - display: block; - padding: 1 2; - background: #000; -} - -SolverTreeView LoadingIndicator{ - height: auto; - padding: 1; - background: #000; - display: none; -} - -SolverTreeView.solving LoadingIndicator{ - display: block; -} - -#content{ - layout: grid; - grid-size: 1 2; - grid-rows: 1fr auto; -} - -#explanation-inputs{ - layout: grid; - grid-size: 2 1; - grid-columns: 2fr 1fr; - display: none; -} - -.mode-explain #explanation-inputs{ - display: block; -} - -#explanation-inputs TextArea{ - border: tall #455A64; - background: #000; - border-title-color: #FFF; - border-title-background: #000; - min-height: 7; - max-height: 7; -} -"""