New docs

clinguin/server/application/backends/clingo_backend.py

@@ -41,7 +41,6 @@ def __init__(self, args):
         self._domain_files = [] if args.domain_files is None else args.domain_files
         self._ui_files = args.ui_files
         self._constants = [f"-c {v}" for v in args.const] if args.const else []
-        self._include_unsat_msg = not args.ignore_unsat_msg
 
         self._domain_state_constructors = []
         self._backup_ds_cache = {}
@@ -51,10 +50,10 @@ def __init__(self, args):
         self._init_ctl()
         self._ground()
 
-        self._add_domain_state_constructor("_ds_context")
+        self._add_domain_state_constructor("_ds_model")
         self._add_domain_state_constructor("_ds_brave")
         self._add_domain_state_constructor("_ds_cautious")
-        self._add_domain_state_constructor("_ds_model")
+        self._add_domain_state_constructor("_ds_context")
         self._add_domain_state_constructor("_ds_unsat")
         self._add_domain_state_constructor("_ds_browsing")
 
@@ -89,11 +88,6 @@ def register_options(cls, parser):
             help="Constant passed to clingo, <id>=<term> replaces term occurrences of <id> with <term>",
             metavar="",
         )
-        parser.add_argument(
-            "--ignore-unsat-msg",
-            action="store_true",
-            help="The automatic pop-up message in the UI when the domain files are UNSAT, will be ignored.",
-        )
 
     # ---------------------------------------------
     # Context
@@ -227,9 +221,7 @@ def _update_ui_state(self):
         and creating a new control object (ui_control) using the ui_files provided
         """
         domain_state = self._domain_state
-        self._ui_state = UIState(
-            self._ui_files, domain_state, self._constants, self._include_unsat_msg
-        )
+        self._ui_state = UIState(self._ui_files, domain_state, self._constants)
         self._ui_state.update_ui_state()
         self._ui_state.replace_images_with_b64()
         for m in self._messages:
@@ -274,6 +266,7 @@ def _domain_state(self):
         ds = ""
         for f in self._domain_state_constructors:
             ds += getattr(self, f)
+        self._logger.debug("\nDomain state:\n==========\n %s", str(ds))
         return ds
 
     # -------- Domain state methods
@@ -283,7 +276,7 @@ def _ds_context(self):
         """
         Gets the context as facts ``_clinguin_context(KEY, VALUE)``
         """
-        prg = ""
+        prg = "#defined _clinguin_context/2. "
         for a in self.context:
             value = str(a.value)
             try:
@@ -293,7 +286,7 @@ def _ds_context(self):
             if symbol is None:
                 value = f'"{value}"'
             prg += f"_clinguin_context({str(a.key)},{value})."
-        return prg
+        return prg + "\n"
 
     @cached_property
     def _ds_brave(self):
@@ -323,7 +316,7 @@ def _ds_brave(self):
                 if "_ds_brave" in self._backup_ds_cache
                 else ""
             )
-        return "\n".join([str(s) + "." for s in list(tag(symbols, "_any"))])
+        return "\n".join([str(s) + "." for s in list(tag(symbols, "_any"))]) + "\n"
 
     @cached_property
     def _ds_cautious(self):
@@ -353,7 +346,7 @@ def _ds_cautious(self):
                 if "_ds_cautious" in self._backup_ds_cache
                 else ""
             )
-        return "\n".join([str(s) + "." for s in list(tag(symbols, "_all"))])
+        return "\n".join([str(s) + "." for s in list(tag(symbols, "_all"))]) + "\n"
 
     @cached_property
     def _ds_model(self):
@@ -377,12 +370,13 @@ def _ds_model(self):
                 )
                 return (
                     self._backup_ds_cache["_ds_model"]
+                    + "\n".join([str(a) + "." for a in self._atoms])
                     if "_ds_model" in self._backup_ds_cache
                     else ""
                 )
             self._model = symbols
 
-        return "\n".join([str(s) + "." for s in self._model])
+        return "\n".join([str(s) + "." for s in self._model]) + "\n"
 
     @property
     def _ds_unsat(self):
@@ -391,10 +385,10 @@ def _ds_unsat(self):
 
         Includes predicate ``_clinguin_unsat/0`` if the domain control is unsat
         """
-        prg = "#defined _clinguin_unsat/0."
-        if self._unsat_core:
+        prg = "#defined _clinguin_unsat/0. "
+        if self._unsat_core is not None:
             prg += "_clinguin_unsat."
-        return prg
+        return prg + "\n"
 
     @property
     def _ds_browsing(self):
@@ -403,10 +397,10 @@ def _ds_browsing(self):
 
         Includes predicate  ``_clinguin_browsing/0`` if the user is browsing solutions
         """
-        prg = "#defined _clinguin_browsing/0."
+        prg = "#defined _clinguin_browsing/0. "
         if self._is_browsing:
             prg += "_clinguin_browsing."
-        return prg
+        return prg + "\n"
 
     # ---------------------------------------------
     # Output

clinguin/server/application/backends/clingo_multishot_backend.py

@@ -58,10 +58,10 @@ def _ds_assume(self):
 
         Includes predicate  ``_clinguin_assume/1`` for every atom that was assumed.
         """
-        prg = "#defined _clinguin_assume/1."
+        prg = "#defined _clinguin_assume/1. "
         for a in self._assumptions:
-            prg += f"_clinguin_assume({str(a)})."
-        return prg
+            prg += f"_clinguin_assume({str(a)}). "
+        return prg + "\n"
 
     # ---------------------------------------------
     # Output

clinguin/server/application/backends/explanation_backend.py

@@ -29,18 +29,19 @@ def __init__(self, args):
 
         self._add_domain_state_constructor("_ds_muc")
 
-        for a in args.assumption_signature:
-            try:
-                name = a.split(",")[0]
-                arity = int(a.split(",")[1])
-            except Exception as ex:
-                raise ValueError(
-                    "Argument assumption_signature must have format name,arity"
-                ) from ex
-            for s in self._ctl.symbolic_atoms:
-                if s.symbol.match(name, arity):
-                    self._mc_base_assumptions.add(s.symbol)
-                    self._add_symbol_to_dict(s.symbol)
+        if args.assumption_signature:
+            for a in args.assumption_signature:
+                try:
+                    name = a.split(",")[0]
+                    arity = int(a.split(",")[1])
+                except Exception as ex:
+                    raise ValueError(
+                        "Argument assumption_signature must have format name,arity"
+                    ) from ex
+                for s in self._ctl.symbolic_atoms:
+                    if s.symbol.match(name, arity):
+                        self._mc_base_assumptions.add(s.symbol)
+                        self._add_symbol_to_dict(s.symbol)
         self._assumptions = self._mc_base_assumptions.copy()
 
     # ---------------------------------------------
@@ -87,6 +88,18 @@ def _add_assumption(self, predicate_symbol):
         super()._add_assumption(predicate_symbol)
         self._add_symbol_to_dict(predicate_symbol)
 
+    def _ground(self, program: str = "base"):
+        """
+        Grounds the provided program, takes care of finding the new literals for the assumptions
+
+        Arguments:
+            program (str): The name of the program to ground (defaults to "base")
+        """
+        self._lit2symbol = {}
+        super()._ground(program=program)
+        for a in self._assumptions:
+            self._add_symbol_to_dict(a)
+
     # ---------------------------------------------
     # Domain state
     # ---------------------------------------------
@@ -98,14 +111,14 @@ def _ds_muc(self):
         Includes predicate ``_clinguin_muc/1`` for every assumption in the MUC
         It uses a cache that is erased after an operation makes changes in the control.
         """
-        prg = "#defined _clinguin_muc/1."
+        prg = "#defined _clinguin_muc/1. "
         if self._unsat_core is not None:
             self._logger.info("UNSAT Answer, will add explanation")
             clingo_core = self._unsat_core
             clingo_core_symbols = [self._lit2symbol[s] for s in clingo_core if s != -1]
             muc_core = self._get_minimum_uc(clingo_core_symbols)
             for s in muc_core:
-                prg = prg + f"_clinguin_muc({str(s)})."
+                prg = prg + f"_clinguin_muc({str(s)}).\n"
         return prg
 
     # ---------------------------------------------
@@ -116,8 +129,13 @@ def _add_symbol_to_dict(self, symbol):
         """
         Adds a list of symbols to the mapping of symbols to literals
         """
-        lit = self._ctl.symbolic_atoms[symbol].literal
-        self._lit2symbol[lit] = symbol
+        try:
+            lit = self._ctl.symbolic_atoms[symbol].literal
+            self._lit2symbol[lit] = symbol
+        except Exception:
+            self._logger.error(
+                "Could not find symbol %s literal in control. Symbol ignored,", symbol
+            )
 
     def _solve_core(self, assumptions):
         """

clinguin/server/data/ui_state.py

@@ -28,21 +28,14 @@ class UIState:
 
     unifiers = [ElementDao, AttributeDao, WhenDao]
 
-    def __init__(
-        self,
-        ui_files,
-        domain_state,
-        constants,
-        include_unsat_msg=True,
-    ):
+    def __init__(self, ui_files, domain_state, constants):
         self._factbase = None
         self._ui_files = ui_files
         self._domain_state = domain_state
         self._constants = constants
-        self._include_unsat_msg = include_unsat_msg
 
     def __str__(self):
-        s = "\nUI Factbase:\n=========\n"
+        s = "\nUI State:\n=========\n"
         s += self._factbase.asp_str()
         return s
 
@@ -79,12 +72,9 @@ def ui_control(self):
                 log.critical(str(e))
                 raise e
 
-        if self._include_unsat_msg:
-            uictl.add("base", [], UIState.get_unsat_messages_ui_encoding())
-
         uictl.add("base", [], self._domain_state)
         uictl.add("base", [], "#show elem/3. #show attr/3. #show when/4.")
-        uictl.ground([("base", [])], ClingraphContext)
+        uictl.ground([("base", [])], ClingraphContext())
 
         return uictl
 
@@ -240,15 +230,3 @@ def replace_images_with_b64(self, image_attribute_key="image"):
                         Raw(String(str(encoded_string))),
                     )
                     self.replace_attribute(attribute, new_attribute)
-
-    @classmethod
-    def get_unsat_messages_ui_encoding(cls):
-        """
-        Get the standard unsat encoding for error messages.
-        """
-        return """
-element(message_unsat,message,window):-_clinguin_unsat.
-attribute(message_unsat,title,"Error"):-_clinguin_unsat.
-attribute(message_unsat,message,"Unsatisfiable output."):-_clinguin_unsat.
-attribute(message_unsat,type,error):-_clinguin_unsat.
-"""

docs/clinguin/development.rst

@@ -40,7 +40,7 @@ This allows to use the AngularFrontend by passing the ``--frontend`` argument to
 
 Be sure that you have `make` and all the dev-tools for the web-frontend installed (`Angular`), as detailed below! Then type:
 
-.. code-block:: bash
+.. code-block:: console
 
     $ make angular
 

docs/clinguin/frontends/AngularFrontend.rst

@@ -384,11 +384,6 @@ A label.
 
     *Values*: String
 
-``icon``
-    *Description*: The icon of the button
-
-    *Values*: `Font awesome <https://fontawesome.com/search?o=r&m=free>`_ symbol name
-
 
 ``textfield``
 .............

docs/clinguin/frontends/TkinterFrontend.rst

@@ -10,12 +10,12 @@ This frontend uses the standard Python interface `tkinter <https://docs.python.o
 
 One can look up the available elements, with the corresponding attributes and callback actions using:
 
-.. code-block:: bash
+.. code-block:: console
 
     $ clinguin client-server --frontend-syntax
 
 If one is also interested in what values one might set, one can also look at the full syntax:
 
-.. code-block:: bash
+.. code-block:: console
 
     $ clinguin client-server --frontend-syntax-full

docs/clinguin/installation.rst

@@ -5,7 +5,7 @@ Clinguin requires a Python version between 3.8 and 3.10 (recomend 3.10)
 
 You can check a successfull instalaltion by running
 
-.. code-block:: bash
+.. code-block:: console
 
     $ clinguin -h
 
@@ -14,7 +14,7 @@ Installing with pip
 
 The python clinguin package can be found `here <https://pypi.org/project/clinguin/>`_.
 
-.. code-block:: bash
+.. code-block:: console
 
     $ pip install clinguin
 
@@ -24,7 +24,7 @@ The following dependencies used in `clinguin` are optional.
 
 To include them in the installation use:
 
-.. code-block:: bash
+.. code-block:: console
 
     $ pip install clinguin[tkinter]
 
@@ -43,7 +43,7 @@ also be installed from source. We recommend this only for development purposes.
 
 Execute the following command in the top level clinguin directory:
 
-.. code-block:: bash
+.. code-block:: console
 
     $ git clone https://github.com/potassco/clinguin
     $ cd clinguin
@@ -89,7 +89,7 @@ This allows to use the AngularFrontend by passing the ``--frontend`` argument to
 
 Be sure that you have `make` and all the dev-tools for the web-frontend installed (`Angular`), as detailed below! Then type:
 
-.. code-block:: bash
+.. code-block:: console
 
     $ make angular