Skip to content

Commit

Permalink
started implementing explain mode
Browse files Browse the repository at this point in the history
  • Loading branch information
@hweichelt
hweichelt committed Jun 27, 2024
1 parent 24019a4 commit be4eeef
Show file tree
Hide file tree
Showing 2 changed files with 93 additions and 37 deletions.
104 changes: 67 additions & 37 deletions src/clingexplaid/cli/textual_gui.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@
from rich.text import Text
from textual import on
from textual.app import App, ComposeResult
from textual.containers import HorizontalScroll, Vertical, VerticalScroll
from textual.containers import Horizontal, HorizontalScroll, Vertical, VerticalScroll
from textual.screen import Screen
from textual.validation import Number
from textual.widget import Widget
Expand All @@ -29,6 +29,7 @@
Static,
TabbedContent,
TabPane,
TextArea,
Tree,
)
from textual.widgets.tree import TreeNode
Expand All @@ -40,14 +41,6 @@
from ..unsat_constraints import UnsatConstraintComputer
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"

COLORS = {
Expand All @@ -59,6 +52,21 @@
}


class Modes(Enum):
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
Expand Down Expand Up @@ -339,7 +347,7 @@ def compose(self) -> ComposeResult:
"""
yield Label("Mode")
yield Select(
((line, line) for line in MODES),
((line.value, line.value) for line in MODES),
allow_blank=False,
id="mode-select",
)
Expand Down Expand Up @@ -449,9 +457,20 @@ def compose(self) -> ComposeResult:
Sidebar(files=self.files, constants=self.constants, classes="box tabs"),
id="top-cell",
)
yield VerticalScroll(
SolverTreeView(),
classes="box",
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()
Expand Down Expand Up @@ -651,6 +670,10 @@ async def action_mode_show_decisions(self) -> None:
return
self.tree_cursor.add(end_string)

async def action_mode_explain(self) -> None:
# TODO: Add implementation
pass

async def action_solve(self) -> None:
"""
Action to exit the textual application
Expand All @@ -668,16 +691,19 @@ async def action_solve(self) -> None:
solve_button.disabled = True
tree_view.add_class("solving")

if self._selected_mode == MODE_MUS:
try:
await self.action_mode_mus()
except NoFilesException as e:
tree_cursor = await self.get_tree_cursor()
tree_cursor.add_leaf(e.args[0])
elif self._selected_mode == MODE_UNSAT_CONSTRAINTS:
await self.action_mode_unsat_constraints()
elif self._selected_mode == MODE_SHOW_DECISIONS:
await self.action_mode_show_decisions()
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
Expand All @@ -690,20 +716,24 @@ async def action_update_mode(self) -> None:
"""
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")
await self.update_selector_tabs(disabled=["tab-constants"])
elif selected_mode == MODE_UNSAT_CONSTRAINTS:
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"])
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")
await self.update_selector_tabs(disabled=["tab-constants"])
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:
"""
Expand Down
26 changes: 26 additions & 0 deletions src/clingexplaid/cli/textual_style.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -138,4 +138,30 @@
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;
}
"""

0 comments on commit be4eeef

Please sign in to comment.