diff --git a/src/translate/fast_downward/translate/normalize.py b/src/translate/fast_downward/translate/normalize.py index 18995846e1..53e7d5827e 100755 --- a/src/translate/fast_downward/translate/normalize.py +++ b/src/translate/fast_downward/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 fast_downward.translate import pddl from fast_downward.translate.options import get_options +from fast_downward.translate.sccs import get_sccs_adjacency_dict class ConditionProxy: @@ -155,11 +158,48 @@ def all_conditions(task, actions=True, axioms=True, goal=True): # is defined as , which is of course # translated to NNF. The parameters of the new axioms are exactly the free # variables of . - +# +# 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 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) + + subtype_names = defaultdict(set) + objects_for_renaming = {} + for par in condition.parameters: + if not subtype_names[par.type_name]: + subtype_names[par.type_name] = {t.name for t in task.types if par.type_name in t.supertype_names} + fitting_types = {par.type_name} | subtype_names[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 +213,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). diff --git a/src/translate/fast_downward/translate/pddl/conditions.py b/src/translate/fast_downward/translate/pddl/conditions.py index e1c8700a2e..ebdd65c209 100644 --- a/src/translate/fast_downward/translate/pddl/conditions.py +++ b/src/translate/fast_downward/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() diff --git a/src/translate/fast_downward/translate/pddl/pddl_types.py b/src/translate/fast_downward/translate/pddl/pddl_types.py index 4d67bb1c1c..0d01c011d9 100644 --- a/src/translate/fast_downward/translate/pddl/pddl_types.py +++ b/src/translate/fast_downward/translate/pddl/pddl_types.py @@ -18,9 +18,10 @@ def _get_type_predicate_name(type_name): class Type: - def __init__(self, name, basetype_name=None): + def __init__(self, name, basetype_name=None, supertype_names=None): self.name = name self.basetype_name = basetype_name + self.supertype_names = supertype_names def __str__(self): return self.name