False assume

clinguin/server/application/backends/clingo_backend.py

@@ -1,4 +1,5 @@
 # pylint: disable=R0801
+# pylint: disable=too-many-lines
 """
 Module that contains the ClingoMultishotBackend.
 """
@@ -158,9 +159,9 @@ def _ctl_arguments_list(self) -> list:
     @property
     def _assumption_list(self) -> list:
         """
-        A list of assumptions in the format [(a, True)]
+        A list of assumptions in the format of form (a, True) or (a, False)
         """
-        return [(a, True) for a in self._assumptions]
+        return self._assumptions
 
     # ---------------------------------------------
     # Initialization
@@ -213,14 +214,14 @@ def _init_ds_constructors(self):
         self._domain_state_constructors = []
         self._backup_ds_cache = {}
         self._add_domain_state_constructor("_ds_context")
-        self._add_domain_state_constructor("_ds_unsat")
         self._add_domain_state_constructor("_ds_browsing")
         self._add_domain_state_constructor("_ds_cautious_optimal")
         self._add_domain_state_constructor("_ds_brave_optimal")
         self._add_domain_state_constructor("_ds_cautious")
         self._add_domain_state_constructor("_ds_brave")
         self._add_domain_state_constructor("_ds_model")  # Keep after brave and cautious
         self._add_domain_state_constructor("_ds_opt")
+        self._add_domain_state_constructor("_ds_unsat")  # Keep after all solve calls
 
     def _init_command_line(self):
         """
@@ -281,7 +282,7 @@ def _init_interactive(self):
             _ui_state (:class:`UIState`): A UIState object used to handle the UI construction,
             set in every call to `_update_ui_state`.
             _atoms (set[str]): A set to store the atoms set dynamically in operations during the interaction.
-            _assumptions (set[str]): A set to store the assumptions set dynamically in operations during the
+            _assumptions (set[(str,bool)]): A set to store the assumptions set dynamically in operations during the
             interaction.
             _externals (dict): A dictionary with true, false and released sets of external atoms
             _model (list[clingo.Symbol]): The model set in `on_model`.
@@ -453,15 +454,19 @@ def _add_atom(self, predicate_symbol):
     # Solving
     # ---------------------------------------------
 
-    def _ground(self, program="base"):
+    def _ground(self, program="base", arguments=None):
         """
         Grounds the provided program
 
         Arguments:
             program (str): The name of the program to ground (defaults to "base")
+            arguments (list, optional): The list of arguments to ground the program. Defaults to an empty list.
         """
-        self._logger.debug(domctl_log(f"domctl.ground([({program}, [])])"))
-        self._ctl.ground([(program, [])])
+        arguments = arguments or []
+        arguments = [arguments] if not isinstance(arguments, list) else arguments
+        self._logger.debug(domctl_log(f"domctl.ground([({program}, {arguments})])"))
+        arguments_symbols = [parse_term(a) for a in arguments]
+        self._ctl.ground([(program, arguments_symbols)])
 
     def _prepare(self):
         """
@@ -751,7 +756,7 @@ def _ds_opt(self):
         Adds program to pass with optimality information.
 
         Includes predicates:
-         - ``_clinguin_cost/1``: With a single tuple indicating the cost
+         - ``_clinguin_cost/1``: With a single tuple indicating the cost of the current model
          - ``_clinguin_cost/2``: With the index and cost value, linearizing predicate ``_clinguin_cost/1``
          - ``_clinguin_optimal/0``: If the solution is optimal
          - ``_clinguin_optimizing/0``: If there is an optimization in the program
@@ -803,6 +808,18 @@ def restart(self):
         """
         self._restart()
 
+    def ground(self, program, arguments=None):
+        """
+        Grounds the given program. Notice that the base program is grounded when the server starts.
+        This operation can be used for grounding encodings with multiple programs in a multi-shot setting.
+
+        Arguments:
+            program (str): The name of the program to ground used in the #program directive
+            arguments (tuple, optional): The list of arguments to ground the program. Defaults to an empty list.
+            These are the arguments of your #program directive. For instance, in #program step(t). the argument is t.
+        """
+        self._ground(program, arguments)
+
     def update(self):
         """
         Updates the UI by clearing the cache and computing the models again.

clinguin/server/application/backends/clingo_multishot_backend.py

@@ -28,6 +28,7 @@ class ClingoMultishotBackend(ClingoBackend):
     def _init_ds_constructors(self):
         super()._init_ds_constructors()
         self._add_domain_state_constructor("_ds_assume")
+        self._add_domain_state_constructor("_ds_external")
 
     # ---------------------------------------------
     # Setters
@@ -73,14 +74,16 @@ def _set_external(self, symbol, name):
                 f"Invalid external value {name}. Must be true, false or relase"
             )
 
-    def _add_assumption(self, symbol):
+    def _add_assumption(self, symbol, value: str = "true"):
         """
         Adds an assumption to the list of assumptions.
 
         Args:
             symbol (clingo.Symbol): The clingo symbol to be added as a True assumption
+            value (true): The value of the assumption either "true" or "false" (Defaults to true)
         """
-        self._assumptions.add(symbol)
+        bool_val = value == "true"
+        self._assumptions.add((symbol, bool_val))
 
     # ---------------------------------------------
     # Domain state
@@ -91,11 +94,28 @@ def _ds_assume(self):
         """
         Adds information about the assumptions
 
-        Includes predicate  ``_clinguin_assume/1`` for every atom that was assumed.
+        Includes predicate  ``_clinguin_assume/2`` for every atom that was assumed.
         """
-        prg = "#defined _clinguin_assume/1. "
-        for a, _ in self._assumption_list:
-            prg += f"_clinguin_assume({str(a)}). "
+        prg = "#defined _clinguin_assume/2. "
+        for a, v in self._assumption_list:
+            v_str = "true" if v else "false"
+            prg += f"_clinguin_assume({str(a)},{v_str}). "
+        return prg + "\n"
+
+    @property
+    def _ds_external(self):
+        """
+        Adds information about the external atoms
+
+        Includes predicate  ``_clinguin_external/2`` for every external atom that has been set.
+        """
+        prg = "#defined _clinguin_external/2. "
+        for a in self._externals["true"]:
+            prg += f"_clinguin_external({str(a)},true). "
+        for a in self._externals["false"]:
+            prg += f"_clinguin_external({str(a)},false). "
+        for a in self._externals["released"]:
+            prg += f"_clinguin_external({str(a)},release). "
         return prg + "\n"
 
     ########################################################################################################
@@ -112,33 +132,39 @@ def clear_assumptions(self):
         self._outdate()
         self._assumptions = set()
 
-    def add_assumption(self, atom):
+    def add_assumption(self, atom, value: str = "true"):
         """
         Adds an atom `a` as an assumption.
+        If the value is True (which is the default), the atom is assumed to be true.
         This assumption can be considered as an integrity constraint:
         `:- not a.` forcing the program to entail the given atom.
+        If the value is False, the atom is assumed to be false:
+        This assumption can be considered as an integrity constraint:
+        `:- a.` forcing the program to never entail the given atom.
 
         Arguments:
 
             atom (str): The clingo symbol to be added as a true assumption
+            value (str): The value of the assumption either "true" or "false" (Defaults to true)
         """
         atom_symbol = parse_term(atom)
-        if atom_symbol not in self._assumptions:
-            self._add_assumption(atom_symbol)
+        if atom_symbol not in [a[0] for a in self._assumptions]:
+            self._add_assumption(atom_symbol, value)
             self._outdate()
 
     def remove_assumption(self, atom):
         """
-        Removes an atom from the assumptions list.
+        Removes an atom from the assumptions list regardless of its value.
 
         Arguments:
-
             atom (str): The clingo symbol to be removed
         """
         atom_symbol = parse_term(atom)
-        if atom_symbol in self._assumptions:
-            self._assumptions.remove(atom_symbol)
-            self._outdate()
+        for a, v in self._assumptions:
+            if a == atom_symbol:
+                self._assumptions.remove((a, v))
+                self._outdate()
+                return
 
     def remove_assumption_signature(self, atom):
         """
@@ -156,16 +182,16 @@ def remove_assumption_signature(self, atom):
         atom_symbol = parse_term(atom)
         arity = len(atom_symbol.arguments)
         to_remove = []
-        for s in self._assumptions:
+        for s, v in self._assumptions:
             if s.match(atom_symbol.name, arity):
                 for i, a in enumerate(atom_symbol.arguments):
                     if str(a) != "any" and s.arguments[i] != a:
                         break
                 else:
-                    to_remove.append(s)
+                    to_remove.append((s, v))
                     continue
-        for s in to_remove:
-            self._assumptions.remove(s)
+        for a in to_remove:
+            self._assumptions.remove(a)
         if len(to_remove) > 0:
             self._outdate()
 

clinguin/server/application/backends/explanation_backend.py

@@ -40,9 +40,7 @@ def _assumption_list(self):
 
             Overwrites :meth:`ClingoBackend._assumption_list`
         """
-        return [
-            (a, True) for a in self._assumptions.union(self._assumptions_from_signature)
-        ]
+        return self._assumptions.union(self._assumptions_from_signature)
 
     # ---------------------------------------------
     # Initialization
@@ -106,20 +104,20 @@ def _load_file(self, f):
     # Solving
     # ---------------------------------------------
     @extends(ClingoMultishotBackend)
-    def _ground(self, program="base"):
+    def _ground(self, program="base", arguments=None):
         """
         Sets the list of assumptions that were taken from the input files using the assumption_signature.
 
         Attributes:
-            _assumptions_from_signature (Set[clingo.Symbol]): The set of assumptions from the assumption signatures
+            _assumptions_from_signature (Set[Tuple(str,bool)]): The set of assumptions from the assumption signatures
+            arguments (list, optional): The list of arguments to ground the program. Defaults to an empty list.
         """
-        super()._ground(program)
+        super()._ground(program, arguments)
         # pylint: disable= attribute-defined-outside-init
-        self._assumptions_from_signature = (
-            self._assumption_transformer.get_assumption_symbols(
-                self._ctl, arguments=self._ctl_arguments_list
-            )
+        transformer_assumptions = self._assumption_transformer.get_assumption_symbols(
+            self._ctl, arguments=self._ctl_arguments_list
         )
+        self._assumptions_from_signature = [(a, True) for a in transformer_assumptions]
 
     # ---------------------------------------------
     # Class methods

clinguin/server/data/clinguin_context.py

@@ -0,0 +1,86 @@
+"""
+Clinguin Context passed to the clingo control object with helper python functions
+"""
+
+from clingo.symbol import String, SymbolType
+
+
+class ClinguinContext:
+    """
+    Makes available a set of python functions to be used in a UI encoding for handling strings.
+    """
+
+    def concat(self, *args):
+        """
+        Concatenates the given symbols as a string
+
+        Example:
+            .. code-block:: prolog
+
+                attr(s_l(I), label, @concat("Semester ",I)):-semester(I).
+
+            Label will be `Semester 1`
+        Args:
+            args: All symbols
+
+        Returns:
+            The string concatenating all symbols
+        """
+        return String("".join([str(x).strip('"') for x in args]))
+
+    def format(self, s, *args):
+        """
+        Formats the string with the given arguments
+
+        Example:
+            .. code-block:: prolog
+
+                attr(s_l(I), label, @format("Semester {}!",I)):-semester(I).
+
+            Label will be `Semester 1!`
+
+        Args:
+            s (str): The string to format, for example "{0} and {1}"
+            args: All symbols that can be accessed by the position starting in 0.
+                If there is a single tuple as an argument, then its arguments are considered one by one.
+        Returns:
+            The string obtained by formatting the string with the given arguments
+        """
+        if (
+            len(args) == 1
+            and args[0].type == SymbolType.Function
+            and args[0].name == ""
+        ):
+            args_str = [str(v).strip('"') for v in args[0].arguments]
+        else:
+            args_str = [str(v).strip('"') for v in args]
+        return String(s.string.format(*args_str))
+
+    def stringify(self, s, capitalize=False):
+        """
+        Turns a value into a string without underscore and capitalized if requested
+
+        Example:
+            .. code-block:: prolog
+
+                attr(s_l(I), label, @stringify(semester_1, true)). # Semester 1
+
+            Label will be `Semester 1`
+
+        Args:
+            s: The value to transform
+        Returns:
+            The string without _
+        """
+        val = str(s).strip('"')
+        val = val.replace("_", " ")
+        if capitalize:
+            val = val[0].upper() + val[1:]
+        return String(val)
+
+    def __getattr__(self, name):
+        # pylint: disable=import-outside-toplevel
+
+        import __main__
+
+        return getattr(__main__, name)

clinguin/server/data/ui_state.py

@@ -9,9 +9,9 @@
 import clorm
 from clingo import Control, parse_term
 from clingo.symbol import Function, Number, String
-from clingraph.clingo_utils import ClingraphContext
 from clorm import Raw
 
+from clinguin.server.data.clinguin_context import ClinguinContext
 from clinguin.utils import StandardTextProcessing, image_to_b64
 
 from ...utils.logger import uictl_log
@@ -93,8 +93,8 @@ def ui_control(self):
         )
         uictl.add("base", [], "#show elem/3. #show attr/3. #show when/4.")
 
-        log.debug(uictl_log('uictl.ground([("base", [])], ClingraphContext())'))
-        uictl.ground([("base", [])], ClingraphContext())
+        log.debug(uictl_log('uictl.ground([("base", [])], ClinguinContext())'))
+        uictl.ground([("base", [])], ClinguinContext())
         return uictl
 
     def update_ui_state(self):

docs/clinguin/development/api.rst

@@ -3,12 +3,25 @@ API
 
 Detailed API for all the classes and functions in the server of the clinguin package.
 
+ClinguinBackends
+----------------
+
 .. automodule:: clinguin.server.application.backends
    :members:
    :undoc-members:
    :show-inheritance:
    :private-members:
 
+
+ClinguinContext
+---------------
+
+.. autoclass:: clinguin.server.data.clinguin_context.ClinguinContext
+   :members:
+
+ClinguinUI
+----------
+
 .. autoclass:: clinguin.server.data.ui_state.UIState
    :members:
    :undoc-members: