[issue1240] Keep axioms stratifiable in normalization edge case

src/translate/normalize.py

@@ -1,10 +1,13 @@
 #! /usr/bin/env python3
 
 import copy
+from collections import defaultdict
+from itertools import product
 from typing import Sequence
 
 from translate import pddl
 from translate.options import get_options
+from translate.sccs import get_sccs_adjacency_dict
 
 
 class ConditionProxy:
@@ -155,11 +158,59 @@ def all_conditions(task, actions=True, axioms=True, goal=True):
 # <not-all-phi> is defined as <not(forall(vars,phi))>, which is of course
 # translated to NNF. The parameters of the new axioms are exactly the free
 # variables of <forall(vars, phi)>.
-
+#
+# If an axiom mentions its head predicate, possibly recursively, in its (body)
+# condition under the scope of a universal quantifier, the universal quantifier
+# must be eliminated differently to keep the set of axioms stratifiable.
+#
+# In this case replace <forall(vars, phi)> by a conjunction where each conjunct
+# is phi with the variables from vars replaced by objects (of fitting types).
+# There is one such conjunct for each possible combination of objects.
 def eliminate_universal_quantifiers(task):
-    def recurse(condition):
+    def recurse(condition, axiom_head_dependencies=[]):
         # Uses new_axioms_by_condition and type_map from surrounding scope.
         if isinstance(condition, pddl.UniversalCondition):
+            pos_preds, neg_preds = condition.pos_and_neg_predicates()
+            head_dependencies = pos_preds.intersection(axiom_head_dependencies)
+            if head_dependencies:
+                # If condition is part of an axiom body and mentions the
+                # axiom's head predicate, possibly recursively, then we cannot
+                # eliminate universal quantifiers via double negation and a new
+                # axiom. This would make the axioms unstratifiable by
+                # introducing a cyclic dependency through negation. Instead
+                # replace the universally quantified part with a conjunction
+                # where in each conjunct the originally quantified variables
+                # are instantiated with objects (of fitting types).
+                conjunct_template = recurse(condition.parts[0], head_dependencies)
+
+                subtypes = defaultdict(set)
+                for t in task.types:
+                    if t.basetype_name:
+                        subtypes[t.basetype_name].add(t.name)
+                # TODO Is there a better way of saturating subtypes than the following?
+                stabilized = False
+                while not stabilized:
+                    stabilized = True
+                    for t in (t.name for t in task.types):
+                        updated_subtypes = subtypes[t].union(*(subtypes[sub_t] for sub_t in subtypes[t]))
+                        if updated_subtypes - subtypes[t] != set():
+                            stabilized = False
+                            subtypes[t] = updated_subtypes
+
+                objects_for_renaming = {}
+                for par in condition.parameters:
+                    fitting_types = {par.type_name} | subtypes[par.type_name]
+                    objects_for_renaming[par.name] = {obj.name for obj in task.objects if obj.type_name in fitting_types}
+
+                parameter_names = [par.name for par in condition.parameters]
+                conjuncts = []
+                for obj_tuple in product(*(objects_for_renaming.values())):
+                    renamings = dict(zip(parameter_names, obj_tuple))
+                    conjuncts.append(conjunct_template.rename_variables(renamings))
+                return pddl.Conjunction(conjuncts)
+
+            # Normal elimination replacing the universally quantified part via
+            # double negation and a new axiom
             axiom_condition = condition.negate()
             parameters = sorted(axiom_condition.free_variables())
             typed_parameters = tuple(pddl.TypedObject(v, type_map[v]) for v in parameters)
@@ -173,13 +224,43 @@ def recurse(condition):
             new_parts = [recurse(part) for part in condition.parts]
             return condition.change_parts(new_parts)
 
+    def stratifiability_sccs(axioms):
+        # Determine positive dependencies of derived predicates.
+        adjacency_dict = defaultdict(set)
+        for ax in axioms:
+            pos_preds, neg_preds = ax.condition.pos_and_neg_predicates()
+            adjacency_dict[ax.name].update(pos_preds)
+
+        # Remove non-derived predicates from the adjacency lists.
+        derived = set(adjacency_dict)
+        for name in adjacency_dict:
+            adjacency_dict[name] &= derived
+
+        scc_blocks = get_sccs_adjacency_dict(adjacency_dict)
+        sccs = {pred: block for block in scc_blocks for pred in block}
+        return sccs
+
     new_axioms_by_condition = {}
-    for proxy in tuple(all_conditions(task)):
+
+    # Remove universal quantifiers in actions and goal.
+    for proxy in tuple(all_conditions(task, actions=True, axioms=False,
+                                      goal=True)):
         # Cannot use generator because we add new axioms on the fly.
         if proxy.condition.has_universal_part():
             type_map = proxy.get_type_map()
             proxy.set(recurse(proxy.condition))
 
+    # Remove universal quantifiers in axioms.
+    sccs = stratifiability_sccs(task.axioms)
+    for proxy in tuple(all_conditions(task, actions=False, axioms=True,
+                                      goal=False)):
+        # Cannot use generator because we add new axioms on the fly.
+        if proxy.condition.has_universal_part():
+            type_map = proxy.get_type_map()
+            head_predicate = proxy.owner.name
+            proxy.set(recurse(proxy.condition,
+                              axiom_head_dependencies=sccs[head_predicate]))
+
 # [2] Simplifies conditions according to the selected strategy.
 # After the simplification only conjuncitons
 # and existential conditions remain (+ truth values, literals).

src/translate/pddl/conditions.py

@@ -73,6 +73,15 @@ def free_variables(self):
             result |= part.free_variables()
         return result
 
+    def pos_and_neg_predicates(self):
+        pos, neg = set(), set()
+        self._collect_predicates(pos, neg)
+        return (pos, neg)
+
+    def _collect_predicates(self, pos, neg):
+        for p in self.parts:
+            p._collect_predicates(pos, neg)
+
     def has_disjunction(self):
         for part in self.parts:
             if part.has_disjunction():
@@ -335,6 +344,9 @@ def free_variables(self):
 class Atom(Literal):
     negated = False
 
+    def _collect_predicates(self, pos, neg):
+        pos.add(self.predicate)
+
     def to_untyped_strips(self):
         return [self]
 
@@ -356,6 +368,9 @@ def positive(self):
 class NegatedAtom(Literal):
     negated = True
 
+    def _collect_predicates(self, pos, neg):
+        neg.add(self.predicate)
+
     def _relaxed(self, parts):
         return Truth()