From b3091376794397d1998306c3bcf726b6b6ea2eec Mon Sep 17 00:00:00 2001 From: Hannes Weichelt Date: Tue, 11 Jun 2024 23:08:24 +0200 Subject: [PATCH] added MUS mode to textual gui --- src/clingexplaid/cli/textual_gui.py | 263 +++++++++++++++++++++++--- src/clingexplaid/cli/textual_style.py | 1 + 2 files changed, 240 insertions(+), 24 deletions(-) diff --git a/src/clingexplaid/cli/textual_gui.py b/src/clingexplaid/cli/textual_gui.py index 91a8fd2..8f2e947 100644 --- a/src/clingexplaid/cli/textual_gui.py +++ b/src/clingexplaid/cli/textual_gui.py @@ -6,6 +6,7 @@ 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 @@ -14,6 +15,7 @@ from textual import on from textual.app import App, ComposeResult from textual.containers import HorizontalScroll, Vertical, VerticalScroll +from textual.screen import Screen from textual.validation import Number from textual.widget import Widget from textual.widgets import ( @@ -31,13 +33,33 @@ ) 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 .textual_style import MAIN_CSS +MODE_MUS = "Minimal Unsatisfiable Subsets" +MODE_UNSAT_CONSTRAINTS = "Unsatisfiable Constraints" +MODE_SHOW_DECISIONS = "Show Decisions" +MODES = ( + MODE_MUS, + MODE_UNSAT_CONSTRAINTS, + MODE_SHOW_DECISIONS, +) ACTIVE_CLASS = "active" +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. @@ -78,14 +100,18 @@ def __init__(self, compose_widgets: List[Widget], update_value_function: Callabl 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 toggle_active(self) -> None: + def set_active(self, active: bool) -> None: """ - Toggles the `SelectorWidget`'s active property. + Sets the active property to the provided value while updating the Selector's style """ - self.active = not self.active + 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() @@ -120,8 +146,12 @@ async def selector_changed(self, event: Checkbox.Changed) -> None: """ # Updating the UI to show the reasons why validation failed if event.checkbox == self.query_one(Checkbox): - self.toggle_active() - await self.run_action("app.update_config") + 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): @@ -276,7 +306,7 @@ def compose(self) -> ComposeResult: yield FilesWidget(self.files) with TabPane("Constants"): yield ConstantsWidget(self.constants) - with TabPane("Decision Signatures"): + with TabPane("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]) @@ -284,12 +314,20 @@ def compose(self) -> ComposeResult: 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, line) for line in ["SHOW DECISIONS"]), allow_blank=False) + yield Select( + ((line, line) for line in MODES), + allow_blank=False, + id="mode-select", + ) yield Label("Models") yield Input( placeholder="Number", @@ -303,6 +341,14 @@ def compose(self) -> ComposeResult: 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: """ @@ -312,7 +358,8 @@ async def input_changed(self, event: Input.Changed) -> None: if event.input == self.query_one("#model-number-input"): if event.validation_result is None: return - if not event.validation_result.is_valid: + 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) @@ -321,6 +368,15 @@ async def input_changed(self, event: Input.Changed) -> None: 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: """ @@ -360,6 +416,7 @@ def __init__(self, files: List[str], constants: Dict[str, str]) -> None: 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() @@ -396,9 +453,7 @@ async def on_model(self, model: List[str]) -> None: self.model_count += 1 if self.tree_cursor is None: return - model_node = self.tree_cursor.add_leaf(f" MODEL {self.model_count} {' '.join(model)}") - cast(Text, model_node.label).stylize("#000000 on #CCCCCC", 0, 7) - cast(Text, model_node.label).stylize("#000000 on #999999", 7, 7 + 2 + len(str(self.model_count))) + await self.add_model_node(" ".join(model), ModelType.MODEL) # add some small sleep time to make ux seem more interactive await asyncio.sleep(0.1) @@ -466,23 +521,67 @@ async def action_update_config(self) -> None: signatures.add((name, int(arity))) self._loaded_signatures = signatures - async def action_solve(self) -> None: + async def action_mode_mus(self) -> None: """ - Action to exit the textual application + Action for MUS Mode """ - self.refresh_bindings() + if not self._loaded_files: + # TODO: Maybe raise an exception here? + return - tree_view = self.query_one(SolverTreeView) - solve_button = self.query_one("#solve-button") + ctl = clingo.Control() - tree = tree_view.solve_tree - tree.reset(tree.root.label) - self.tree_cursor = tree.root - self.model_count = 0 + # transform matching facts to choices to allow assumptions + at = AssumptionTransformer(signatures=self._loaded_signatures) + program_transformed = at.parse_files(list(self._loaded_files)) - solve_button.disabled = True - tree_view.add_class("solving") + # 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) + # TODO: 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 + if not program_unsat: + if self.tree_cursor is None: + return + self.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: + if self.tree_cursor is None: + return + self.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 + """ + return None + 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, @@ -508,12 +607,128 @@ async def action_solve(self) -> None: 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_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") + + if self._selected_mode == MODE_MUS: + await self.action_mode_mus() + elif self._selected_mode == MODE_UNSAT_CONSTRAINTS: + pass + elif self._selected_mode == MODE_SHOW_DECISIONS: + await self.action_mode_show_decisions() + 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) + if selected_mode == MODE_MUS: + 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") + elif selected_mode == MODE_UNSAT_CONSTRAINTS: + self.set_mode_class(self.query_one(Screen), "mode-unsat-constraints") + await self.reset_solve_tree("Unsatisfiable Constraints") + elif selected_mode == MODE_SHOW_DECISIONS: + 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") + + async def action_debug(self, msg: str) -> None: + """ + Action to add a leaf with custom message to the solve tree for debugging purposes + """ + if self.tree_cursor is None: + # TODO: Extract this into a function that does this once so I don't have to do it always >:( + return + self.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) -> None: + """ + 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 = ("#000000", "#CCCCCC", "#999999") + 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("_", " ") + if self.tree_cursor is None: + # TODO: again extract this !!! + return + model_node = self.tree_cursor.add_leaf(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)) + ) + + 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 - end_string = "SAT" if self.model_count > 0 else "UNSAT" - self.tree_cursor.add(end_string) def check_action(self, action: str, parameters: tuple[object, ...]) -> bool | None: """ diff --git a/src/clingexplaid/cli/textual_style.py b/src/clingexplaid/cli/textual_style.py index 6254be4..ca2b4c4 100644 --- a/src/clingexplaid/cli/textual_style.py +++ b/src/clingexplaid/cli/textual_style.py @@ -9,6 +9,7 @@ grid-columns: 1fr 2fr; grid-rows: 1fr auto; } + #debug{ column-span: 2; }