fix: make encoding of derived predicate invertible

with this change, we translate each formula special symbols (operator symbols, parenthesis etc.) into a sequence of characters that can be part of a valid derived predicate name.

This means that, given a name of a derived predicate, one can simply do the inverse replacement and recover the original formula.

This approach has two major drawbacks:
1) the output of the compiler is much more verbose; e.g. the formula 'Y(a)' gets translated into 'val__YLPAR__a__RPAR'
2) the new approach imposes restrictions on the allowed symbols in a PPLTL formula. E.g. symbols that start with 'VAL__' or 'Y__', or symbols that contain one of the following as substring:
  - "LPAR__" (left parenthesis)
  - "__RPAR" (right parenthesis)
  - "NOT__" (not symbol)
  - "__AND__" (and symbol)
  - "__OR__" (or symbol)
  - "__QUOTE__" (quote)
  are forbidden.

This policy might be more conservative than needed, but in this way we should have the guarantee that the encoding is an invertible mapping (such property basically proves non-ambiguity of the encoding, because it means there is a one-to-one relationship between 'string representation of pylogics formulas' and 'string representation encoded as PDDL predicate name').

plan4past/compiler.py

@@ -133,12 +133,13 @@ def _compile_problem(self):
 
 def _compute_whens(formula: Formula) -> Set[When]:
     """Compute conditional effects for formula progression."""
+    formula_predicates = predicates(formula)
     return {
         When(Predicate(add_val_prefix(remove_before_prefix(p.name))), p)
-        for p in predicates(formula)
+        for p in formula_predicates
     }.union(
         When(Not(Predicate(add_val_prefix(remove_before_prefix(p.name)))), Not(p))
-        for p in predicates(formula)
+        for p in formula_predicates
     )
 
 

plan4past/helpers/utils.py

@@ -22,52 +22,62 @@
 
 """Miscellanea utilities."""
 import re
+from typing import Collection, Type
 
 from pddl.logic import Predicate, constants
 
 _PDDL_NAME_REGEX = "[A-Za-z][-_A-Za-z0-9]*"
 _GROUND_FLUENT_REGEX = re.compile(
     rf"(\"({_PDDL_NAME_REGEX})( {_PDDL_NAME_REGEX})*\")|({_PDDL_NAME_REGEX})"
 )
-_VAL_PREFIX = "val__"
+VAL_PREFIX = "VAL__"
+_LEFT_PAR = "LPAR__"
+_RIGHT_PAR = "__RPAR"
+Y_PREFIX = "Y__"
+_NOT = "NOT__"
+_AND = "__AND__"
+_OR = "__OR__"
+_QUOTE = "__QUOTE__"
 
 
 def add_val_prefix(name: str):
     """Add the 'prime' prefix."""
-    return _VAL_PREFIX + name.replace('"', "")
+    return VAL_PREFIX + name.replace('"', _QUOTE)
 
 
 def remove_before_prefix(name: str):
     """Remove the 'Y' prefix."""
     return (
-        name.replace("Y-", "")
-        if name.startswith("Y-")
-        else name.replace("Y", "", 1)
-        if name.startswith("Y")
+        name.replace(Y_PREFIX, "")
+        if name.startswith(Y_PREFIX)
+        else re.sub(f"{_RIGHT_PAR}$", "", name.replace("Y" + _LEFT_PAR, "", 1))
+        if name.startswith("Y" + _LEFT_PAR)
         else name
     )
 
 
 def remove_val_prefix(name: str):
     """Remove the 'prime' prefix."""
-    return name.replace(_VAL_PREFIX, "") if name.startswith(_VAL_PREFIX) else name
+    return name.replace(VAL_PREFIX, "") if name.startswith(VAL_PREFIX) else name
 
 
 def replace_symbols(name: str):
     """Stringify symbols."""
     return (
-        name.replace('"', "")
-        .replace("(", "")
-        .replace(")", "")
-        .replace("&", "and")
-        .replace("|", "or")
-        .replace("~", "not-")
-        .replace("!", "not-")
+        name.replace('"', _QUOTE)
+        .replace("(", _LEFT_PAR)
+        .replace(")", _RIGHT_PAR)
+        .replace("&", _AND)
+        .replace("|", _OR)
+        .replace("~", _NOT)
+        .replace("!", _NOT)
         .replace(" ", "-")
     )
 
 
-def check_(condition: bool, message: str = "") -> None:
+def check_(
+    condition: bool, message: str = "", exception_cls: Type[Exception] = AssertionError
+) -> None:
     """
     User-defined assert.
 
@@ -76,7 +86,7 @@ def check_(condition: bool, message: str = "") -> None:
         https://bandit.readthedocs.io/en/1.7.5/plugins/b101_assert_used.html
     """
     if not condition:
-        raise AssertionError(message)
+        raise exception_cls(message)
 
 
 def parse_ground_fluent(symbol: str) -> Predicate:
@@ -99,17 +109,50 @@ def parse_ground_fluent(symbol: str) -> Predicate:
     return Predicate(symbol)
 
 
+def _check_does_not_start_with(symbol: str, prefixes: Collection[str]) -> None:
+    """
+    Check if a symbol does not start with a given prefix.
+
+    :param symbol: the symbol
+    :param prefixes: the prefixes to check
+    """
+    for prefix in prefixes:
+        check_(
+            not symbol.startswith(prefix),
+            f"invalid symbol: symbol '{symbol}' cannot start with {prefix}",
+            exception_cls=ValueError,
+        )
+
+
+def _check_not_in(symbol: str, forbidden_substrings: Collection[str]) -> None:
+    """
+    Check if a string is not in a set of symbols.
+
+    :param symbol: the symbol
+    :param forbidden_substrings: the set of forbidden substrings
+    """
+    for s in forbidden_substrings:
+        check_(
+            s not in symbol,
+            f"invalid symbol: symbol '{symbol}' contains {s}",
+            exception_cls=ValueError,
+        )
+
+
 def validate(symbol: str) -> None:
     """
     Validate a symbol.
 
     :param symbol: the symbol
     """
-    # check if the symbol does not start with the 'val__' prefix
-    if symbol.startswith(_VAL_PREFIX):
-        raise ValueError(
-            f"invalid symbol: symbol '{symbol}' cannot start with {_VAL_PREFIX}"
-        )
+    # remove the double quotes
+    symbol_unquoted = symbol.replace('"', "")
+
+    # check if the symbol does not start with the 'val__' or the 'Y__' prefix
+    _check_does_not_start_with(symbol_unquoted, [VAL_PREFIX, Y_PREFIX])
+
+    # check if the symbol does not contain forbidden substrings
+    _check_not_in(symbol_unquoted, [_LEFT_PAR, _RIGHT_PAR, _AND, _OR, _NOT, _QUOTE])
 
     # check if the symbol is a valid PDDL ground fluent
     parse_ground_fluent(symbol)

plan4past/utils/derived_visitor.py

@@ -39,7 +39,12 @@
 )
 from pylogics.utils.to_string import to_string
 
-from plan4past.helpers.utils import add_val_prefix, parse_ground_fluent, replace_symbols
+from plan4past.helpers.utils import (
+    Y_PREFIX,
+    add_val_prefix,
+    parse_ground_fluent,
+    replace_symbols,
+)
 
 
 @singledispatch
@@ -132,7 +137,7 @@ def derived_predicates_since(formula: Since) -> Set[DerivedPredicate]:
     op_or_1 = Predicate(add_val_prefix(replace_symbols(to_string(formula.operands[1]))))
     op_or_2 = And(
         Predicate(add_val_prefix(replace_symbols(to_string(formula.operands[0])))),
-        Predicate(f"Y-{replace_symbols(to_string(formula))}"),
+        Predicate(f"{Y_PREFIX}{replace_symbols(to_string(formula))}"),
     )
     condition = Or(op_or_1, op_or_2)
     der_pred_ops = [derived_predicates(op) for op in formula.operands]
@@ -146,7 +151,7 @@ def derived_predicates_once(formula: Once) -> Set[DerivedPredicate]:
     val = Predicate(add_val_prefix(replace_symbols(formula_name)))
     condition = Or(
         Predicate(add_val_prefix(replace_symbols(to_string(formula.argument)))),
-        Predicate(f"Y-{replace_symbols(to_string(formula))}"),
+        Predicate(f"{Y_PREFIX}{replace_symbols(to_string(formula))}"),
     )
     der_pred_arg = derived_predicates(formula.argument)
     return {DerivedPredicate(val, condition)}.union(der_pred_arg)

plan4past/utils/predicates_visitor.py

@@ -40,7 +40,7 @@
 )
 from pylogics.utils.to_string import to_string
 
-from plan4past.helpers.utils import replace_symbols
+from plan4past.helpers.utils import Y_PREFIX, replace_symbols
 
 
 def predicates_binaryop(formula: _BinaryOp):
@@ -113,7 +113,7 @@ def predicates_since(formula: Since) -> Set[Predicate]:
         tail = Since(*formula.operands[1:])
         return predicates(Since(head, tail))
     formula_name = replace_symbols(to_string(formula))
-    quoted = Predicate(f"Y-{formula_name}")
+    quoted = Predicate(f"{Y_PREFIX}{formula_name}")
     subsinces = predicates_binaryop(formula)
     return {quoted}.union(subsinces)
 
@@ -122,6 +122,6 @@ def predicates_since(formula: Since) -> Set[Predicate]:
 def predicates_once(formula: Once) -> Set[Predicate]:
     """Compute predicate for a Once formula."""
     formula_name = replace_symbols(to_string(formula))
-    quoted = Predicate(f"Y-{formula_name}")
+    quoted = Predicate(f"{Y_PREFIX}{formula_name}")
     sub = predicates_unaryop(formula)
     return sub.union({quoted})

tests/helpers/planutils/downward.py

@@ -68,7 +68,7 @@ def get_planner_cmd(
 
     def process_output(self, working_directory: Path, stdout: str) -> PlannerResult:
         """Process the output of the planner."""
-        logger.debug("Processing output of LAMA")
+        logger.debug("Processing output of Fast-Downward.")
 
         # the sas_plan file is in the /root directory
         sas_file = working_directory / "sas_plan"

tests/test_compiler/test_blocksworld_det.py

@@ -35,8 +35,8 @@ class TestBlocksworldDetSimpleSequence(BaseCompilerTest):
 
     PATH_TO_DOMAINS_DIR = BLOCKSWORLD_DIR
     PATH_TO_INSTANCES_DIR = BLOCKSWORLD_DIR
-    MIN_INSTANCE_ID = 2
-    MAX_INSTANCE_ID = 10
+    MIN_INSTANCE_ID = 3
+    MAX_INSTANCE_ID = 3
 
     def make_formula(self, instance_id: int, domain: Path, problem: Path) -> str:
         """

tests/test_helpers/test_utils.py

@@ -33,22 +33,22 @@
 
 def test_val_prefix() -> None:
     """Test the add_val_prefix function."""
-    assert add_val_prefix("Y-foo") == "val__Y-foo"
-    assert add_val_prefix("Yfoo") == "val__Yfoo"
-    assert add_val_prefix("foo") == "val__foo"
-    assert add_val_prefix("Y-foo-bar") == "val__Y-foo-bar"
+    assert add_val_prefix("Y-foo") == "VAL__Y-foo"
+    assert add_val_prefix("Yfoo") == "VAL__Yfoo"
+    assert add_val_prefix("foo") == "VAL__foo"
+    assert add_val_prefix("Y-foo-bar") == "VAL__Y-foo-bar"
 
 
 def test_remove_before_prefix() -> None:
     """Test the remove_before_prefix function."""
-    assert remove_before_prefix("Y-foo") == "foo"
-    assert remove_before_prefix("Yfoo") == "foo"
+    assert remove_before_prefix("Y__foo") == "foo"
+    assert remove_before_prefix("YLPAR__foo__RPAR") == "foo"
     assert remove_before_prefix("foo") == "foo"
 
 
 def test_remove_val_prefix() -> None:
     """Test the remove_val_prefix function."""
-    assert remove_val_prefix("val__foo") == "foo"
+    assert remove_val_prefix("VAL__foo") == "foo"
     assert remove_val_prefix("foo") == "foo"
 
 

tests/test_utils/test_derived_visitor.py

@@ -101,7 +101,7 @@ def test_derived_predicates_visitor_and():
     condition_a = Predicate("a")
     condition_b = Predicate("b")
 
-    val = Predicate(add_val_prefix("a-and-b"))
+    val = Predicate(add_val_prefix("LPAR__a__RPAR-__AND__-LPAR__b__RPAR"))
     val_a = Predicate(add_val_prefix("a"))
     val_b = Predicate(add_val_prefix("b"))
 
@@ -125,7 +125,7 @@ def test_derived_predicates_visitor_or():
     condition_a = Predicate("a")
     condition_b = Predicate("b")
 
-    val = Predicate(add_val_prefix("a-or-b"))
+    val = Predicate(add_val_prefix("LPAR__a__RPAR-__OR__-LPAR__b__RPAR"))
     val_a = Predicate(add_val_prefix("a"))
     val_b = Predicate(add_val_prefix("b"))
 
@@ -147,7 +147,7 @@ def test_derived_predicates_visitor_not():
 
     condition_a = Predicate("a")
 
-    val = Predicate(add_val_prefix("not-a"))
+    val = Predicate(add_val_prefix("NOT__LPAR__a__RPAR"))
     val_a = Predicate(add_val_prefix("a"))
 
     condition = Not(val_a)
@@ -165,10 +165,10 @@ def test_derived_predicates_visitor_before():
 
     condition_a = Predicate("a")
 
-    val = Predicate(add_val_prefix("Ya"))
+    val = Predicate(add_val_prefix("YLPAR__a__RPAR"))
     val_a = Predicate(add_val_prefix("a"))
 
-    condition = Predicate("Ya")
+    condition = Predicate("YLPAR__a__RPAR")
 
     expected = {DerivedPredicate(val, condition), DerivedPredicate(val_a, condition_a)}
 
@@ -186,10 +186,14 @@ def test_derived_predicates_visitor_since():
     val_a = Predicate(add_val_prefix("a"))
     val_b = Predicate(add_val_prefix("b"))
     val_c = Predicate(add_val_prefix("c"))
-    val_a_since_b_since_c = Predicate(add_val_prefix("a-S-b-S-c"))
-    val_b_since_c = Predicate(add_val_prefix("b-S-c"))
-    Y_a_since_b_since_c = Predicate("Y-a-S-b-S-c")
-    Y_b_since_c = Predicate("Y-b-S-c")
+    val_a_since_b_since_c = Predicate(
+        add_val_prefix("LPAR__a__RPAR-S-LPAR__LPAR__b__RPAR-S-LPAR__c__RPAR__RPAR")
+    )
+    val_b_since_c = Predicate(add_val_prefix("LPAR__b__RPAR-S-LPAR__c__RPAR"))
+    Y_a_since_b_since_c = Predicate(
+        "Y__LPAR__a__RPAR-S-LPAR__LPAR__b__RPAR-S-LPAR__c__RPAR__RPAR"
+    )
+    Y_b_since_c = Predicate("Y__LPAR__b__RPAR-S-LPAR__c__RPAR")
 
     condition_a = Predicate("a")
     condition_b = Predicate("b")
@@ -215,8 +219,8 @@ def test_derived_predicates_visitor_once():
     once_a = Once(a)
 
     val_a = Predicate(add_val_prefix("a"))
-    val_once_a = Predicate(add_val_prefix("Oa"))
-    Y_once_a = Predicate("Y-Oa")
+    val_once_a = Predicate(add_val_prefix("OLPAR__a__RPAR"))
+    Y_once_a = Predicate("Y__OLPAR__a__RPAR")
 
     condition_a = Predicate("a")
     condition_once_a = Or(val_a, Y_once_a)

tests/test_utils/test_predicates_visitor.py

@@ -84,7 +84,7 @@ def test_predicates_visitor_before():
     """Test the predicates visitor for the before formula."""
     a = PLTLAtomic("a")
     Ya = Before(a)
-    assert predicates(Ya) == {Predicate("Ya")}
+    assert predicates(Ya) == {Predicate("YLPAR__a__RPAR")}
 
 
 def test_predicates_visitor_since():
@@ -94,13 +94,13 @@ def test_predicates_visitor_since():
     c = PLTLAtomic("c")
     a_since_b_since_c = Since(a, b, c)
     assert predicates(a_since_b_since_c) == {
-        Predicate("Y-b-S-c"),
-        Predicate("Y-a-S-b-S-c"),
+        Predicate("Y__LPAR__a__RPAR-S-LPAR__LPAR__b__RPAR-S-LPAR__c__RPAR__RPAR"),
+        Predicate("Y__LPAR__b__RPAR-S-LPAR__c__RPAR"),
     }
 
 
 def test_predicates_visitor_once():
     """Test the predicates visitor for the once formula."""
     a = PLTLAtomic("a")
     once_a = Once(a)
-    assert predicates(once_a) == {Predicate("Y-Oa")}
+    assert predicates(once_a) == {Predicate("Y__OLPAR__a__RPAR")}