Updated AssumptionTransformer

- `get_assumptions` takes list of argument strings now instead of constant dict

src/clingexplaid/cli/clingo_app.py

@@ -15,7 +15,7 @@
 from ..mus import CoreComputer
 from ..transformers import AssumptionTransformer, OptimizationRemover
 from ..unsat_constraints import UnsatConstraintComputer
-from ..utils import get_constants_from_arguments
+from ..utils import get_constant_string, get_constants_from_arguments
 from ..utils.logging import BACKGROUND_COLORS, COLORS
 from .textual_gui import ClingexplaidTextualApp
 
@@ -173,7 +173,9 @@ def _method_mus(
         control.add("base", [], program_transformed)
         control.ground([("base", [])])
 
-        assumptions = at.get_assumption_literals(control, constants=self.argument_constants)
+        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

src/clingexplaid/transformers/transformer_assumption.py

@@ -8,7 +8,7 @@
 import clingo
 import clingo.ast as _ast
 
-from ..utils import match_ast_symbolic_atom_signature
+from ..utils import get_constant_string, match_ast_symbolic_atom_signature
 from .exceptions import NotGroundedException, UntransformedException
 
 
@@ -80,11 +80,11 @@ def parse_files(self, paths: Sequence[Union[str, Path]]) -> str:
         return "\n".join(out)
 
     def get_assumption_symbols(
-        self, control: clingo.Control, constants: Optional[Dict[str, str]] = None
+        self, control: clingo.Control, arguments: Optional[List[str]] = None
     ) -> Set[clingo.Symbol]:
         """
-        Returns the assumption symbols which were gathered during the transformation of the program. Has to be called after
-        a program has already been transformed.
+        Returns the assumption symbols which were gathered during the transformation of the program. Has to be called
+        after a program has already been transformed.
         """
         # Just taking the fact symbolic atoms of the control given doesn't work here since we anticipate that
         # this control is ground on the already transformed program. This means that all facts are now choice rules
@@ -100,18 +100,16 @@ def get_assumption_symbols(
                 "The get_assumptions method cannot be called before the control has been grounded"
             )
 
-        constants = constants if constants is not None else {}
-
-        all_constants = dict(self.program_constants)
-        all_constants.update(constants)
-        constant_strings = [f"-c {k}={v}" for k, v in all_constants.items()] if constants is not None else []
-        fact_control = clingo.Control(constant_strings)
+        program_constant_strings = [get_constant_string(c, v, prefix="-c ") for c, v in self.program_constants.items()]
+        fact_control_arguments = arguments if arguments is not None else []
+        fact_control_arguments += program_constant_strings
+        fact_control = clingo.Control(fact_control_arguments)
         fact_control.add("base", [], "\n".join(self.fact_rules))
         fact_control.ground([("base", [])])
         fact_symbols = {sym.symbol for sym in fact_control.symbolic_atoms if sym.is_fact}
         return fact_symbols
 
-    def get_assumption_literals(self, control: clingo.Control, constants: Optional[Dict[str, str]] = None) -> Set[int]:
+    def get_assumption_literals(self, control: clingo.Control, constants: Optional[List[str]] = None) -> Set[int]:
         """
         Returns the assumption literals which were gathered during the transformation of the program. Has to be called
         after a program has already been transformed.

src/clingexplaid/utils/__init__.py

@@ -88,3 +88,14 @@ def get_constants_from_arguments(argument_vector: List[str]) -> Dict[str, str]:
             next_constant = True
 
     return constants
+
+
+def get_constant_string(name: str, value: str, prefix: str = "") -> str:
+    """
+    Create a constant string of the format "{prefix}{name}={value}".
+    """
+    constant_name_pattern = re.compile(r"^[a-zA-Z_].*")
+    if not constant_name_pattern.match(name):
+        raise ValueError("constant name does not abide to the naming standard")
+    constr_string = f"{name}={value}"
+    return prefix + constr_string

tests/clingexplaid/test_muc.py

@@ -31,7 +31,7 @@ def get_mus_of_program(
     ctl.add("base", [], transformed_program)
     ctl.ground([("base", [])])
 
-    assumptions = at.get_assumptions(ctl)
+    assumptions = at.get_assumption_literals(ctl)
 
     cc = CoreComputer(ctl, assumptions)
     ctl.solve(assumptions=list(assumptions), on_core=cc.shrink)
@@ -195,7 +195,7 @@ def test_core_computer_get_multiple_minimal(self) -> None:
         parsed = at.parse_files([program_path])
         ctl.add("base", [], parsed)
         ctl.ground([("base", [])])
-        cc = CoreComputer(ctl, at.get_assumptions(ctl))
+        cc = CoreComputer(ctl, at.get_assumption_literals(ctl))
 
         mus_generator = cc.get_multiple_minimal()
 
@@ -218,7 +218,7 @@ def test_core_computer_get_multiple_minimal_max_mus_2(self) -> None:
         parsed = at.parse_files([program_path])
         ctl.add("base", [], parsed)
         ctl.ground([("base", [])])
-        cc = CoreComputer(ctl, at.get_assumptions(ctl))
+        cc = CoreComputer(ctl, at.get_assumption_literals(ctl))
 
         mus_generator = cc.get_multiple_minimal(max_mus=2)
 

tests/clingexplaid/test_transformers.py

@@ -52,7 +52,7 @@ def test_assumption_transformer_get_assumptions_before_transformation(self) -> N
         """
         at = AssumptionTransformer()
         control = clingo.Control()
-        self.assertRaises(UntransformedException, lambda: at.get_assumptions(control))
+        self.assertRaises(UntransformedException, lambda: at.get_assumption_literals(control))
 
     def test_assumption_transformer_get_assumptions_before_grounding(self) -> None:
         """
@@ -62,7 +62,7 @@ def test_assumption_transformer_get_assumptions_before_grounding(self) -> None:
         at = AssumptionTransformer()
         control = clingo.Control()
         at.parse_files([program_path])
-        self.assertRaises(NotGroundedException, lambda: at.get_assumptions(control))
+        self.assertRaises(NotGroundedException, lambda: at.get_assumption_literals(control))
 
     def test_assumption_transformer_visit_definition(self) -> None:
         """

tests/clingexplaid/test_utils.py

@@ -4,7 +4,7 @@
 
 from unittest import TestCase
 
-from clingexplaid.utils import get_constants_from_arguments, get_signatures_from_model_string
+from clingexplaid.utils import get_constant_string, get_constants_from_arguments, get_signatures_from_model_string
 
 
 class TestUtils(TestCase):
@@ -27,3 +27,14 @@ def test_get_constants_from_arguments(self) -> None:
         self.assertEqual(get_constants_from_arguments(["-c", "a=42"]), {"a": "42"})
         self.assertEqual(get_constants_from_arguments(["test/dir/file.lp", "--const", "blob=value"]), {"blob": "value"})
         self.assertEqual(get_constants_from_arguments(["--const", "-a", "test/42"]), {})
+
+    def test_get_constant_strings(self) -> None:
+        """
+        Test getting constant strings
+        """
+        self.assertEqual(get_constant_string("test", "42"), "test=42")
+        self.assertEqual(get_constant_string("name", "value"), "name=value")
+        with self.assertRaises(ValueError):
+            get_constant_string("123", "value")
+        self.assertEqual(get_constant_string("name", "123", prefix="#const "), "#const name=123")
+        self.assertEqual(get_constant_string("name", "123", prefix="-c "), "-c name=123")