From 1ed4a59d663020f539ca3a3c8ca34e01d7aa9d92 Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Tue, 16 Jan 2024 09:49:59 +0100 Subject: [PATCH 01/27] [issue1133-invariants] remove source of non-determinism --- src/translate/invariants.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/translate/invariants.py b/src/translate/invariants.py index ed98e4edca..58711cd45c 100644 --- a/src/translate/invariants.py +++ b/src/translate/invariants.py @@ -239,7 +239,8 @@ def check_balance(self, balance_checker, enqueue_func): actions_to_check = set() for part in self.parts: actions_to_check |= balance_checker.get_threats(part.predicate) - for action in actions_to_check: + for action in sorted(actions_to_check, key=lambda a: (a.name, + a.parameters)): heavy_action = balance_checker.get_heavy_action(action) if self.operator_too_heavy(heavy_action): return False From 50603bb7f32ebb12aee387bad36ea3b392339fcc Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Tue, 16 Jan 2024 10:56:32 +0100 Subject: [PATCH 02/27] [issue1133-invariants] implement lt for typed objects --- src/translate/pddl/pddl_types.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/translate/pddl/pddl_types.py b/src/translate/pddl/pddl_types.py index 45d2a6286b..35054aa505 100644 --- a/src/translate/pddl/pddl_types.py +++ b/src/translate/pddl/pddl_types.py @@ -46,6 +46,9 @@ def __eq__(self, other): def __ne__(self, other): return not self == other + def __lt__(self, other): + return (self.name, self.type_name) < (other.name, other.type_name) + def __str__(self): return "%s: %s" % (self.name, self.type_name) From bde4387f1fb7f06df97490cc5e1a824453db378c Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Fri, 12 Jan 2024 13:33:41 +0100 Subject: [PATCH 03/27] [issue1133] add some comments and TODOs to invariant code --- src/translate/invariants.py | 137 +++++++++++++++++++++++++++++++++--- 1 file changed, 129 insertions(+), 8 deletions(-) diff --git a/src/translate/invariants.py b/src/translate/invariants.py index 58711cd45c..e24918a833 100644 --- a/src/translate/invariants.py +++ b/src/translate/invariants.py @@ -21,9 +21,28 @@ def invert_list(alist): def instantiate_factored_mapping(pairs): + """Input pairs is a list [(preimg1, img1), ..., (preimgn, imgn)]. + For entry (preimg, img), preimg and img is a list of numbers of the same + length. All preimages (and all imgage) are pairwise disjoint, as well as + the components of each preimage/image. + + The function determines all possible bijections between the union of + preimgs and the union of imgs such that for every entry (preimg, img), + values from preimg are mapped to values from img. + It yields one permutation after the other, each represented as a list + of pairs (x,y), meaning x is mapped to y. + """ + # for every entry (preimg, img) in pairs, determine all possible bijections + # from preimg to img. part_mappings = [[list(zip(preimg, perm_img)) for perm_img in itertools.permutations(img)] for (preimg, img) in pairs] + # all possibilities to pick one bijection for each entry return tools.cartesian_product(part_mappings) + # TODO: this has a TODO note in tools. It probably can simply be entirely + # replaced by using itertools.product and chain as follows: + # for x in itertools.product(*part_mapping): + # for y in itertools.chain(*x): + # yield list(y) def find_unique_variables(action, invariant): @@ -54,7 +73,16 @@ def ensure_conjunction_sat(system, *parts): conjunction of all parts is satisfiable. Each part must be an iterator, generator, or an iterable over - literals.""" + literals. + + We add the following constraints for each literal to the system: + + - for (not (= x y)): x != y (as a NegativeClause with one entry(x,y)), + - for (= x y): x = y + - for predicates that occur with a positive and negative literal, we + consider every combination of a positive one (e.g. P(x, y, z)) and + a negative one (e.g. (not P(a, b, c))) and add a constraint + (x != y or y != b or z != c).""" pos = defaultdict(set) neg = defaultdict(set) for literal in itertools.chain(*parts): @@ -64,6 +92,8 @@ def ensure_conjunction_sat(system, *parts): system.add_negative_clause(n) else: a = constraints.Assignment([literal.args]) + # TODO an assignment x=y expects x to be a variable, not an + # object. Do we need to handle this here? system.add_assignment_disjunction([a]) else: if literal.negated: @@ -86,15 +116,20 @@ def ensure_cover(system, literal, invariant, inv_vars): invariant covers the literal""" a = invariant.get_covering_assignments(inv_vars, literal) assert len(a) == 1 - # if invariants could contain several parts of one predicate, this would - # not be true but the depending code in parts relies on this assumption + # if invariants could contain several parts of one predicate, this + # assertion would not be true but the depending code in parts relies on + # this assumption. system.add_assignment_disjunction(a) def ensure_inequality(system, literal1, literal2): """Modifies the constraint system such that it is only solvable if the literal instantiations are not equal (ignoring whether one is negated and - the other is not)""" + the other is not). + + If the literals have different predicates, there is nothing to do. + Otherwise we add for P(x, y, z) and P(a, b, c) a contraint + (x != a or y != b or z != c)""" if (literal1.predicate == literal2.predicate and literal1.args): parts = list(zip(literal1.args, literal2.args)) @@ -103,6 +138,15 @@ def ensure_inequality(system, literal1, literal2): class InvariantPart: def __init__(self, predicate, order, omitted_pos=-1): + """There is one InvariantPart for every predicate mentioned in the + invariant. The parameters of the invariant do not have fixed names + in the code (to avoid conflicts with existing variable names in + operators), instead we think of the 0th, 1st, 2nd, ... parameter. + The order of the invariant part ties these parameters to the + arguments of the predicate: the i-th number n_i in order specifies + that the i-th invariant parameter occurs at position n_i as an + argument of the predicate. The omitted_pos is the remaining argument + position, or -1 if there is none.""" self.predicate = predicate self.order = order self.omitted_pos = omitted_pos @@ -134,11 +178,15 @@ def arity(self): return len(self.order) def get_assignment(self, parameters, literal): + """Returns an assignment constraint that requires the invariant + parameters to correspond to the values in which they occur in the + literal.""" equalities = [(arg, literal.args[argpos]) for arg, argpos in zip(parameters, self.order)] return constraints.Assignment(equalities) def get_parameters(self, literal): + """Returns the values of the invariant parameters in the literal.""" return [literal.args[pos] for pos in self.order] def instantiate(self, parameters): @@ -148,18 +196,68 @@ def instantiate(self, parameters): return pddl.Atom(self.predicate, args) def possible_mappings(self, own_literal, other_literal): + """This method is used when an action had an unbalanced add effect + own_literal. The action has a delete effect on literal + other_literal, so we try to refine the invariant such that it also + covers the delete effect. + + For this purpose, we need to identify all bijections m between + argument positions of of other_literal and argument positions of + own_literal, such that other_literal can balance own_literal + (possibly omitting one argument position of own_literal). + + In most cases this is straight-forward, e.g. with own_literal being + P(?a, ?b, ?c) and other_literal being Q(?b, ?a, ?c), we would need + to map the first position of Q to the second position of P, the + second one of Q to the first one of P, and the third to the third + one (with 0-indexing represented as [(0,1), (1,0), (2,2)]). + + Most complication stems from the fact that in rare cases arguments + in the literals can be repeated, e.g. P(?a, ?b, ?a) and Q(?b, ?a, + ?a). In invariants, we don't have repetitions, so we need to + identify the more general invariants for which this repetition is + a special case (if invariant parameters are equal in its + instantiation). So in this example, we need to consider two + possible mappings: [(0, 1), (1, 0), (2, 2)] and [(0, 1), (1, 2), (2, + 1)]. + + The method returns [] if there is no possible mapping and otherwise + yields the mappings one by one. + """ allowed_omissions = len(other_literal.args) - len(self.order) + # All parts of an invariant always use all non-counted variables, so + # len(self.order) corresponds to the number of invariant parameters + # (the arity of the invariant). So we can/must omit allowed_omissions + # many arguments of other_literal when matching invariant parameters + # with arguments. if allowed_omissions not in (0, 1): + # There may be at most one counted variable. return [] own_parameters = self.get_parameters(own_literal) + # own_parameters is a list containing at position i the value of the + # i-th invariant parameter in own_literal. arg_to_ordered_pos = invert_list(own_parameters) other_arg_to_pos = invert_list(other_literal.args) + # other_arg_to_pos maps every argument of other_literal to the + # lists of positions in which it is occuring in other_literal, e.g. + # for P(?a, ?b, ?a), other_arg_to_pos["?a"] = [0, 2]. factored_mapping = [] + # We iterate over all values occuring as arguments in other_literal + # and compare the number of occurrences in other_literal to those in + # own_literal. If the difference of these numbers allows us to cover + # other_literal with the (still) permitted number of counted variables, + # we remember the correspondance of positions for this value in + # factored_mapping. If all values can be covered, we instatiate the + # complete factored_mapping, computing all possibilities to map + # positions from own_literal to positions from other_literal. for key, other_positions in other_arg_to_pos.items(): own_positions = arg_to_ordered_pos.get(key, []) + # all positions at which key occurs as argument in own_literal len_diff = len(own_positions) - len(other_positions) if len_diff >= 1 or len_diff <= -2 or len_diff == -1 and not allowed_omissions: + # mapping of the literals is not possible with at most one + # counted variable. return [] if len_diff: own_positions.append(-1) @@ -168,16 +266,39 @@ def possible_mappings(self, own_literal, other_literal): return instantiate_factored_mapping(factored_mapping) def possible_matches(self, own_literal, other_literal): + """This method is used when an action had an unbalanced add effect + own_literal. The action has a delete effect on literal + other_literal, so we try to refine the invariant such that it also + covers the delete effect. + + For this purpose, we consider all possible mappings from the + parameter positions of other_literal to the parameter positions of + own_literal such that the extended invariant can use other_literal + to balance own_literal. From these position mapping, we can extract + the order field for the invariant part. + + Consider for an example of the "self" InvariantPart "forall ?u, + ?v, ?w(P(?u, ?v, ?w) is non-increasing" and let own_literal be P(?a, ?b, + ?c) and other_literal be Q(?b, ?c, ?d, ?a)). The only possible mapping + from positions of Q to positions of P (or -1) is [0->1, 1->2, 2->-1, + 3->0] for which we create a new Invariant Part Q(?v, ?w, _. ?u) with + the third argument being counted. + """ assert self.predicate == own_literal.predicate result = [] for mapping in self.possible_mappings(own_literal, other_literal): new_order = [None] * len(self.order) omitted = -1 - for (key, value) in mapping: - if value == -1: - omitted = key + for (other_pos, own_pos) in mapping: + if own_pos == -1: + omitted = other_pos else: - new_order[value] = key + new_order[own_pos] = other_pos + # TODO This only works because in the initial invariant + # candidates the numbering of invariant parameters matches + # the order of the corresponding arguments in the + # predicate. To make this work in general, we need to + # consider a potential order difference in self.order. result.append(InvariantPart(other_literal.predicate, new_order, omitted)) return result From bab9ea860ae80afa4d4cb77a37312e469925b6ee Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Fri, 12 Jan 2024 14:30:58 +0100 Subject: [PATCH 04/27] [issue1133] refactoring --- src/translate/invariants.py | 55 +++++++++++++++++++++---------------- 1 file changed, 32 insertions(+), 23 deletions(-) diff --git a/src/translate/invariants.py b/src/translate/invariants.py index e24918a833..8309a5b809 100644 --- a/src/translate/invariants.py +++ b/src/translate/invariants.py @@ -114,12 +114,8 @@ def ensure_conjunction_sat(system, *parts): def ensure_cover(system, literal, invariant, inv_vars): """Modifies the constraint system such that it is only solvable if the invariant covers the literal""" - a = invariant.get_covering_assignments(inv_vars, literal) - assert len(a) == 1 - # if invariants could contain several parts of one predicate, this - # assertion would not be true but the depending code in parts relies on - # this assumption. - system.add_assignment_disjunction(a) + a = invariant.get_covering_assignment(inv_vars, literal) + system.add_assignment_disjunction([a]) def ensure_inequality(system, literal1, literal2): @@ -349,11 +345,25 @@ def get_parameters(self, atom): def instantiate(self, parameters): return [part.instantiate(parameters) for part in self.parts] - def get_covering_assignments(self, parameters, atom): + def get_covering_assignment(self, parameters, atom): + """The parameters are the (current names of the) parameters of the + invariant, the atom is the one that should be covered. + This is only called for atoms with a predicate for which the + invariant has a part. It returns a constraint that requires that + each parameter of the invariant matches the corresponding argument + of the given atom. + + Example: If the atom is P(?a, ?b, ?c), the invariant part for P + is {P 0 2 [1]} and the invariant parameters are given by ["?v0", + "?v1"] then the invariant part expressed with these parameters would + be P(?v0 ?x ?v1) with ?x being the counted variable. The method thus + returns the constraint (?v0 = ?a and ?v2 = ?c). + """ part = self.predicate_to_part[atom.predicate] - return [part.get_assignment(parameters, atom)] - # if there were more parts for the same predicate the list - # contained more than one element + return part.get_assignment(parameters, atom) + # If there were more parts for the same predicate, we would have to + # consider more than one assignment (disjunctively). + # We assert earlier that this is not the case. def check_balance(self, balance_checker, enqueue_func): # Check balance for this hypothesis. @@ -407,26 +417,25 @@ def operator_unbalanced(self, action, enqueue_func): return False def minimal_covering_renamings(self, action, add_effect, inv_vars): - """computes the minimal renamings of the action parameters such + """Computes the minimal renamings of the action parameters such that the add effect is covered by the action. - Each renaming is an constraint system""" + Each renaming is an constraint system.""" # add_effect must be covered - assigs = self.get_covering_assignments(inv_vars, add_effect.literal) + assignment = self.get_covering_assignment(inv_vars, add_effect.literal) # renaming of operator parameters must be minimal minimal_renamings = [] params = [p.name for p in action.parameters] - for assignment in assigs: - system = constraints.ConstraintSystem() - system.add_assignment(assignment) - mapping = assignment.get_mapping() - if len(params) > 1: - for (n1, n2) in itertools.combinations(params, 2): - if mapping.get(n1, n1) != mapping.get(n2, n2): - negative_clause = constraints.NegativeClause([(n1, n2)]) - system.add_negative_clause(negative_clause) - minimal_renamings.append(system) + system = constraints.ConstraintSystem() + system.add_assignment(assignment) + mapping = assignment.get_mapping() + if len(params) > 1: + for (n1, n2) in itertools.combinations(params, 2): + if mapping.get(n1, n1) != mapping.get(n2, n2): + negative_clause = constraints.NegativeClause([(n1, n2)]) + system.add_negative_clause(negative_clause) + minimal_renamings.append(system) return minimal_renamings def add_effect_unbalanced(self, action, add_effect, del_effects, From 03b1288f2f789affcab331d4d8c961cf49f03110 Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Mon, 15 Jan 2024 13:56:30 +0100 Subject: [PATCH 05/27] [issue1133] significantly change the system for the balance check --- src/translate/invariants.py | 167 +++++++++++++++++++----------------- 1 file changed, 90 insertions(+), 77 deletions(-) diff --git a/src/translate/invariants.py b/src/translate/invariants.py index 8309a5b809..e5bb6d3951 100644 --- a/src/translate/invariants.py +++ b/src/translate/invariants.py @@ -416,53 +416,82 @@ def operator_unbalanced(self, action, enqueue_func): return True return False - def minimal_covering_renamings(self, action, add_effect, inv_vars): - """Computes the minimal renamings of the action parameters such - that the add effect is covered by the action. - Each renaming is an constraint system.""" - - # add_effect must be covered - assignment = self.get_covering_assignment(inv_vars, add_effect.literal) - - # renaming of operator parameters must be minimal - minimal_renamings = [] - params = [p.name for p in action.parameters] - system = constraints.ConstraintSystem() - system.add_assignment(assignment) - mapping = assignment.get_mapping() - if len(params) > 1: - for (n1, n2) in itertools.combinations(params, 2): - if mapping.get(n1, n1) != mapping.get(n2, n2): - negative_clause = constraints.NegativeClause([(n1, n2)]) - system.add_negative_clause(negative_clause) - minimal_renamings.append(system) - return minimal_renamings def add_effect_unbalanced(self, action, add_effect, del_effects, inv_vars, enqueue_func): - - minimal_renamings = self.minimal_covering_renamings(action, add_effect, - inv_vars) - - lhs_by_pred = defaultdict(list) + # We build for every delete effect that is possibly covered by this + # invariant a constraint system that will be unsolvable if the delete + # effect balances the add effect. Large parts of the constraint system + # are independent of the delete effect, so we precompute them first. + + # Dictionary add_effect_produced_by_pred describes what must be true so + # that the action is applicable and produces the add effect. It is + # stored as a map from predicate names to literals (overall + # representing a conjunction of these literals). + add_effect_produced_by_pred = defaultdict(list) for lit in itertools.chain(get_literals(action.precondition), get_literals(add_effect.condition), get_literals(add_effect.literal.negate())): - lhs_by_pred[lit.predicate].append(lit) - + add_effect_produced_by_pred[lit.predicate].append(lit) + + # Determine a constraint that minimally relates invariant parameters to + # variables and constants so that the add_effect is covered by the + # invariant. + threat_assignment = self.get_covering_assignment(inv_vars, add_effect.literal) + # The assignment can imply equivalences between variables (and with + # constants). For example if the invariant part is {p 1 2 3 [0]} and + # the add effect is p(?x ?y ?y a) then we would know that the invariant + # part is only threatened by the add effect if the first two invariant + # parameters are equal (and if ?x and ?y are the action parameters, it + # is equal to the second action parameter ?y) and the third invariant + # parameter is a. + + # The add effect must be balanced in all threatening action + # applications. We thus must adapt the constraint system such that it + # prevents restricting solution that set action parameters equal to + # each other or to a specific constant (if this is not already + # necessary for the threat). + constants = set(a for a in add_effect.literal.args if a[0] != "?") for del_effect in del_effects: - minimal_renamings = self.unbalanced_renamings( - del_effect, add_effect, inv_vars, lhs_by_pred, minimal_renamings) - if not minimal_renamings: + for a in del_effect.literal.args: + if a[0] != "?": + constants.add(a) + params = [p.name for p in action.parameters] + action_param_system = constraints.ConstraintSystem() + mapping = threat_assignment.get_mapping() + # The assignment is a conjunction of equalities between invariant + # parameters and the variables and constants occurring in the + # add_effect literal. The mapping maps every term to its representative + # in the coarsest equivalence class induced by the equalities. + for param in params: + if mapping.get(param, param)[0] == "?": + # for the add effect being a threat to the invariant, param + # does not need to be a specific constant. So we may not bind + # it to a constant when balancing the add effect. + for c in constants: + negative_clause = constraints.NegativeClause([(param, c)]) + action_param_system.add_negative_clause(negative_clause) + for (n1, n2) in itertools.combinations(params, 2): + if mapping.get(n1, n1) != mapping.get(n2, n2): + # n1 and n2 don't have to be equivalent to cover the add + # effect, so we require for the solutions that they do not + # set n1 and n2 equal. + negative_clause = constraints.NegativeClause([(n1, n2)]) + action_param_system.add_negative_clause(negative_clause) + + for del_effect in del_effects: + if self.balances(del_effect, add_effect, inv_vars, + add_effect_produced_by_pred, + threat_assignment, action_param_system): return False - # Otherwise, the balance check fails => Generate new candidates. + # The balance check fails => Generate new candidates. self.refine_candidate(add_effect, action, enqueue_func) return True def refine_candidate(self, add_effect, action, enqueue_func): - """refines the candidate for an add effect that is unbalanced in the - action and adds the refined one to the queue""" + """Refines the candidate for an add effect that is unbalanced in the + action and adds the refined one to the queue.""" part = self.predicate_to_part[add_effect.literal.predicate] for del_eff in [eff for eff in action.effects if eff.literal.negated]: if del_eff.literal.predicate not in self.predicate_to_part: @@ -470,57 +499,41 @@ def refine_candidate(self, add_effect, action, enqueue_func): del_eff.literal): enqueue_func(Invariant(self.parts.union((match,)))) - def unbalanced_renamings(self, del_effect, add_effect, inv_vars, - lhs_by_pred, unbalanced_renamings): - """returns the renamings from unbalanced renamings for which - the del_effect does not balance the add_effect.""" + def balances(self, del_effect, add_effect, inv_vars, produced_by_pred, + threat_assignment, action_param_system): + """Returns whether the del_effect is guaranteed to balance the add effect + if + - produced_by_pred must be true for the add_effect to be produced, + - threat_assignment is a constraint of equalities that must be true + for the add effect threatening the invariant, and + - action_param_system contains contraints that action parameters are + not fixed to be equivalent (except the add effect is otherwise not + threat).""" system = constraints.ConstraintSystem() ensure_cover(system, del_effect.literal, self, inv_vars) - # Since we may only rename the quantified variables of the delete effect - # we need to check that "renamings" of constants are already implied by - # the unbalanced_renaming (of the of the operator parameters). The - # following system is used as a helper for this. It builds a conjunction - # that formulates that the constants are NOT renamed accordingly. We - # below check that this is impossible with each unbalanced renaming. - check_constants = False - constant_test_system = constraints.ConstraintSystem() - for a, b in system.combinatorial_assignments[0][0].equalities: - # first 0 because the system was empty before we called ensure_cover - # second 0 because ensure_cover only adds assignments with one entry - if b[0] != "?": - check_constants = True - neg_clause = constraints.NegativeClause([(a, b)]) - constant_test_system.add_negative_clause(neg_clause) - ensure_inequality(system, add_effect.literal, del_effect.literal) - - still_unbalanced = [] - for renaming in unbalanced_renamings: - if check_constants: - new_sys = constant_test_system.combine(renaming) - if new_sys.is_solvable(): - # it is possible that the operator arguments are not - # mapped to constants as required for covering the delete - # effect - still_unbalanced.append(renaming) - continue - - new_sys = system.combine(renaming) - if self.lhs_satisfiable(renaming, lhs_by_pred): - implies_system = self.imply_del_effect(del_effect, lhs_by_pred) - if not implies_system: - still_unbalanced.append(renaming) - continue + # makes sure that the add and the delete effect do not affect the same + # atom (so that the delete effect is ignored due to the + # add-after-delete semantics). + + new_sys = system.combine(action_param_system) + new_sys.add_assignment(threat_assignment) + if self.add_effect_potentially_produced(threat_assignment, produced_by_pred): + implies_system = self.imply_del_effect(del_effect, produced_by_pred) + if not implies_system: + return False new_sys = new_sys.combine(implies_system) if not new_sys.is_solvable(): - still_unbalanced.append(renaming) - return still_unbalanced + return False + return True - def lhs_satisfiable(self, renaming, lhs_by_pred): - system = renaming.copy() - ensure_conjunction_sat(system, *itertools.chain(lhs_by_pred.values())) + + def add_effect_potentially_produced(self, threat_assignment, produced_by_pred): + system = constraints.ConstraintSystem() + system.add_assignment(threat_assignment) + ensure_conjunction_sat(system, *itertools.chain(produced_by_pred.values())) return system.is_solvable() def imply_del_effect(self, del_effect, lhs_by_pred): From d924865efd9dad08010afbd7dc25859f58a70703 Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Wed, 17 Jan 2024 14:08:03 +0100 Subject: [PATCH 06/27] [issue1133] fix bug (implies system was ignored) plus comments/logging --- src/translate/invariants.py | 27 ++++++++++++++++++--------- 1 file changed, 18 insertions(+), 9 deletions(-) diff --git a/src/translate/invariants.py b/src/translate/invariants.py index e5bb6d3951..50b412d98d 100644 --- a/src/translate/invariants.py +++ b/src/translate/invariants.py @@ -1,10 +1,12 @@ from collections import defaultdict import itertools +import logging import constraints import pddl import tools +#logging.basicConfig(level=logging.DEBUG) # Notes: # All parts of an invariant always use all non-counted variables # -> the arity of all predicates covered by an invariant is either the @@ -14,6 +16,7 @@ # in every invariant. def invert_list(alist): + """Example: invert_list([?a, ?b, ?a]) = {'?a': [0, 2], '?b': [1]}""" result = defaultdict(list) for pos, arg in enumerate(alist): result[arg].append(pos) @@ -23,12 +26,12 @@ def invert_list(alist): def instantiate_factored_mapping(pairs): """Input pairs is a list [(preimg1, img1), ..., (preimgn, imgn)]. For entry (preimg, img), preimg and img is a list of numbers of the same - length. All preimages (and all imgage) are pairwise disjoint, as well as + length. All preimages (and all images) are pairwise disjoint, as well as the components of each preimage/image. The function determines all possible bijections between the union of preimgs and the union of imgs such that for every entry (preimg, img), - values from preimg are mapped to values from img. + all values from preimg are mapped to values from img. It yields one permutation after the other, each represented as a list of pairs (x,y), meaning x is mapped to y. """ @@ -113,7 +116,7 @@ def ensure_conjunction_sat(system, *parts): def ensure_cover(system, literal, invariant, inv_vars): """Modifies the constraint system such that it is only solvable if the - invariant covers the literal""" + invariant covers the literal.""" a = invariant.get_covering_assignment(inv_vars, literal) system.add_assignment_disjunction([a]) @@ -125,9 +128,8 @@ def ensure_inequality(system, literal1, literal2): If the literals have different predicates, there is nothing to do. Otherwise we add for P(x, y, z) and P(a, b, c) a contraint - (x != a or y != b or z != c)""" - if (literal1.predicate == literal2.predicate and - literal1.args): + (x != a or y != b or z != c).""" + if (literal1.predicate == literal2.predicate and literal1.args): parts = list(zip(literal1.args, literal2.args)) system.add_negative_clause(constraints.NegativeClause(parts)) @@ -331,7 +333,7 @@ def __hash__(self): return hash(self.parts) def __str__(self): - return "{%s}" % ", ".join(str(part) for part in self.parts) + return "{%s}" % ", ".join(sorted(str(part) for part in self.parts)) def __repr__(self): return '' % self @@ -373,7 +375,9 @@ def check_balance(self, balance_checker, enqueue_func): for action in sorted(actions_to_check, key=lambda a: (a.name, a.parameters)): heavy_action = balance_checker.get_heavy_action(action) + logging.debug(f"Checking Invariant {self} wrt action {action.name}") if self.operator_too_heavy(heavy_action): + logging.debug("too heavy") return False if self.operator_unbalanced(action, enqueue_func): return False @@ -403,6 +407,7 @@ def operator_too_heavy(self, h_action): return False def operator_unbalanced(self, action, enqueue_func): + logging.debug(f"Checking Invariant {self} for action {action.name}") inv_vars = find_unique_variables(action, self) relevant_effs = [eff for eff in action.effects if self.predicate_to_part.get(eff.literal.predicate)] @@ -414,6 +419,7 @@ def operator_unbalanced(self, action, enqueue_func): if self.add_effect_unbalanced(action, eff, del_effects, inv_vars, enqueue_func): return True + logging.debug(f"Balanced") return False @@ -483,6 +489,7 @@ def add_effect_unbalanced(self, action, add_effect, del_effects, if self.balances(del_effect, add_effect, inv_vars, add_effect_produced_by_pred, threat_assignment, action_param_system): + logging.debug(f"Invariant {self}: add effect {add_effect.literal} balanced for action {action.name} by del effect {del_effect.literal}") return False # The balance check fails => Generate new candidates. @@ -502,7 +509,7 @@ def refine_candidate(self, add_effect, action, enqueue_func): def balances(self, del_effect, add_effect, inv_vars, produced_by_pred, threat_assignment, action_param_system): """Returns whether the del_effect is guaranteed to balance the add effect - if + where the input is such that: - produced_by_pred must be true for the add_effect to be produced, - threat_assignment is a constraint of equalities that must be true for the add effect threatening the invariant, and @@ -524,9 +531,11 @@ def balances(self, del_effect, add_effect, inv_vars, produced_by_pred, implies_system = self.imply_del_effect(del_effect, produced_by_pred) if not implies_system: return False - new_sys = new_sys.combine(implies_system) + new_sys = new_sys.combine(implies_system) if not new_sys.is_solvable(): return False + + logging.debug(f"{new_sys}") return True From 064a136e24683cb4ccb1cc5afd9bc6450a2f215c Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Wed, 17 Jan 2024 17:41:15 +0100 Subject: [PATCH 07/27] [issue1133] replace 'cartesian product' computation using itertools --- src/translate/invariants.py | 11 +++++------ src/translate/tools.py | 19 ------------------- 2 files changed, 5 insertions(+), 25 deletions(-) diff --git a/src/translate/invariants.py b/src/translate/invariants.py index 50b412d98d..680b6c268a 100644 --- a/src/translate/invariants.py +++ b/src/translate/invariants.py @@ -40,12 +40,11 @@ def instantiate_factored_mapping(pairs): part_mappings = [[list(zip(preimg, perm_img)) for perm_img in itertools.permutations(img)] for (preimg, img) in pairs] # all possibilities to pick one bijection for each entry - return tools.cartesian_product(part_mappings) - # TODO: this has a TODO note in tools. It probably can simply be entirely - # replaced by using itertools.product and chain as follows: - # for x in itertools.product(*part_mapping): - # for y in itertools.chain(*x): - # yield list(y) + if not part_mappings: + yield [] + else: + for x in itertools.product(*part_mappings): + yield list(itertools.chain.from_iterable(x)) def find_unique_variables(action, invariant): diff --git a/src/translate/tools.py b/src/translate/tools.py index ad244b8e99..12ac84a9b0 100644 --- a/src/translate/tools.py +++ b/src/translate/tools.py @@ -1,22 +1,3 @@ -def cartesian_product(sequences): - # TODO: Rename this. It's not good that we have two functions - # called "product" and "cartesian_product", of which "product" - # computes cartesian products, while "cartesian_product" does not. - - # This isn't actually a proper cartesian product because we - # concatenate lists, rather than forming sequences of atomic elements. - # We could probably also use something like - # map(itertools.chain, product(*sequences)) - # but that does not produce the same results - if not sequences: - yield [] - else: - temp = list(cartesian_product(sequences[1:])) - for item in sequences[0]: - for sequence in temp: - yield item + sequence - - def get_peak_memory_in_kb(): try: # This will only work on Linux systems. From 36e6af442a15dd90525fb098c8eb5b2008f6bc46 Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Wed, 17 Jan 2024 21:02:42 +0100 Subject: [PATCH 08/27] [issue1133] explicit representation of invariant parameters with variables ?@vi --- src/translate/invariant_finder.py | 23 ++- src/translate/invariants.py | 251 +++++++++++++----------------- 2 files changed, 123 insertions(+), 151 deletions(-) diff --git a/src/translate/invariant_finder.py b/src/translate/invariant_finder.py index a8f32ffa59..14993849a1 100755 --- a/src/translate/invariant_finder.py +++ b/src/translate/invariant_finder.py @@ -78,10 +78,14 @@ def get_fluents(task): def get_initial_invariants(task): for predicate in get_fluents(task): - all_args = list(range(len(predicate.arguments))) - for omitted_arg in [-1] + all_args: - order = [i for i in all_args if i != omitted_arg] - part = invariants.InvariantPart(predicate.name, order, omitted_arg) + all_args = list(f"?@v{i}" for i in range(len(predicate.arguments))) + atom = pddl.Atom(predicate.name, all_args) + part = invariants.InvariantPart(atom, -1) + yield invariants.Invariant((part,)) + for omitted in range(len(predicate.arguments)): + inv_args = all_args[0:omitted] + ["_"] + all_args[omitted:-1] + atom = pddl.Atom(predicate.name, inv_args) + part = invariants.InvariantPart(atom, omitted) yield invariants.Invariant((part,)) def find_invariants(task, reachable_action_params): @@ -118,7 +122,16 @@ def useful_groups(invariants, initial_facts): if isinstance(atom, pddl.Assign): continue for invariant in predicate_to_invariants.get(atom.predicate, ()): - group_key = (invariant, tuple(invariant.get_parameters(atom))) + parameters = invariant.get_parameters(atom) + # we need to make the parameters dictionary hashable, so + # we store the values as a tuple in the order of the numbering of + # the invariant parameters. + inv_vars = [f"?@v{i}" for i in range(invariant.arity())] + parameters_tuple = tuple((var, parameters[var]) + for var in inv_vars) + + parameters_tuple = tuple(sorted(x for x in parameters.items())) + group_key = (invariant, parameters_tuple) if group_key not in nonempty_groups: nonempty_groups.add(group_key) else: diff --git a/src/translate/invariants.py b/src/translate/invariants.py index 680b6c268a..e9c1c952cf 100644 --- a/src/translate/invariants.py +++ b/src/translate/invariants.py @@ -25,9 +25,10 @@ def invert_list(alist): def instantiate_factored_mapping(pairs): """Input pairs is a list [(preimg1, img1), ..., (preimgn, imgn)]. - For entry (preimg, img), preimg and img is a list of numbers of the same - length. All preimages (and all images) are pairwise disjoint, as well as - the components of each preimage/image. + For entry (preimg, img), preimg is a list of numbers and img a list of + invariant parameters or -1 of the same length. All preimages (and all + images) are pairwise disjoint, as well as the components of each + preimage/image. The function determines all possible bijections between the union of preimgs and the union of imgs such that for every entry (preimg, img), @@ -47,22 +48,6 @@ def instantiate_factored_mapping(pairs): yield list(itertools.chain.from_iterable(x)) -def find_unique_variables(action, invariant): - # find unique names for invariant variables - params = {p.name for p in action.parameters} - for eff in action.effects: - params.update([p.name for p in eff.parameters]) - inv_vars = [] - counter = itertools.count() - for _ in range(invariant.arity()): - while True: - new_name = "?v%i" % next(counter) - if new_name not in params: - inv_vars.append(new_name) - break - return inv_vars - - def get_literals(condition): if isinstance(condition, pddl.Literal): yield condition @@ -113,10 +98,10 @@ def ensure_conjunction_sat(system, *parts): system.add_negative_clause(negative_clause) -def ensure_cover(system, literal, invariant, inv_vars): +def ensure_cover(system, literal, invariant): """Modifies the constraint system such that it is only solvable if the invariant covers the literal.""" - a = invariant.get_covering_assignment(inv_vars, literal) + a = invariant.get_covering_assignment(literal) system.add_assignment_disjunction([a]) @@ -134,63 +119,51 @@ def ensure_inequality(system, literal1, literal2): class InvariantPart: - def __init__(self, predicate, order, omitted_pos=-1): + def __init__(self, atom, omitted_pos=-1): """There is one InvariantPart for every predicate mentioned in the - invariant. The parameters of the invariant do not have fixed names - in the code (to avoid conflicts with existing variable names in - operators), instead we think of the 0th, 1st, 2nd, ... parameter. - The order of the invariant part ties these parameters to the - arguments of the predicate: the i-th number n_i in order specifies - that the i-th invariant parameter occurs at position n_i as an - argument of the predicate. The omitted_pos is the remaining argument - position, or -1 if there is none.""" - self.predicate = predicate - self.order = order + invariant. The atom of the invariant part has arguments of the form + "?@vi" for the invariant parameters and "_" at the omitted position. + If no position is omitted, omitted_pos is -1.""" + self.atom = atom self.omitted_pos = omitted_pos def __eq__(self, other): # This implies equality of the omitted_pos component. - return self.predicate == other.predicate and self.order == other.order + return self.atom == other.atom def __ne__(self, other): - return self.predicate != other.predicate or self.order != other.order + return self.atom != other.atom def __le__(self, other): - return self.predicate <= other.predicate or self.order <= other.order + return self.atom <= other.atom def __lt__(self, other): - return self.predicate < other.predicate or self.order < other.order + return self.atom < other.atom def __hash__(self): - return hash((self.predicate, tuple(self.order))) + return hash(self.atom) def __str__(self): - var_string = " ".join(map(str, self.order)) - omitted_string = "" - if self.omitted_pos != -1: - omitted_string = " [%d]" % self.omitted_pos - return "%s %s%s" % (self.predicate, var_string, omitted_string) + return f"{self.atom} [omitted_pos = {self.omitted_pos}]" def arity(self): - return len(self.order) - - def get_assignment(self, parameters, literal): - """Returns an assignment constraint that requires the invariant - parameters to correspond to the values in which they occur in the - literal.""" - equalities = [(arg, literal.args[argpos]) - for arg, argpos in zip(parameters, self.order)] - return constraints.Assignment(equalities) + if self.omitted_pos == -1: + return len(self.atom.args) + else: + return len(self.atom.args) - 1 def get_parameters(self, literal): - """Returns the values of the invariant parameters in the literal.""" - return [literal.args[pos] for pos in self.order] - - def instantiate(self, parameters): - args = ["?X"] * (len(self.order) + (self.omitted_pos != -1)) - for arg, argpos in zip(parameters, self.order): - args[argpos] = arg - return pddl.Atom(self.predicate, args) + """Returns a dictionary, mapping the invariant parameters to the + corresponding values in the literal.""" + return dict((arg, literal.args[pos]) + for pos, arg in enumerate(self.atom.args) + if pos != self.omitted_pos) + + def instantiate(self, parameters_tuple): + parameters = dict(parameters_tuple) + args = [parameters[arg] if arg != "_" else "?X" + for arg in self.atom.args] + return pddl.Atom(self.atom.predicate, args) def possible_mappings(self, own_literal, other_literal): """This method is used when an action had an unbalanced add effect @@ -198,42 +171,36 @@ def possible_mappings(self, own_literal, other_literal): other_literal, so we try to refine the invariant such that it also covers the delete effect. - For this purpose, we need to identify all bijections m between - argument positions of of other_literal and argument positions of - own_literal, such that other_literal can balance own_literal - (possibly omitting one argument position of own_literal). - - In most cases this is straight-forward, e.g. with own_literal being - P(?a, ?b, ?c) and other_literal being Q(?b, ?a, ?c), we would need - to map the first position of Q to the second position of P, the - second one of Q to the first one of P, and the third to the third - one (with 0-indexing represented as [(0,1), (1,0), (2,2)]). - - Most complication stems from the fact that in rare cases arguments - in the literals can be repeated, e.g. P(?a, ?b, ?a) and Q(?b, ?a, - ?a). In invariants, we don't have repetitions, so we need to - identify the more general invariants for which this repetition is - a special case (if invariant parameters are equal in its - instantiation). So in this example, we need to consider two - possible mappings: [(0, 1), (1, 0), (2, 2)] and [(0, 1), (1, 2), (2, - 1)]. + From own_literal, we can determine a variable or object for every + invariant parameter, where potentially several invariant parameters + can have the same value. + + From the arguments of other_literal, we determine all possibilities + how we can use the invariant parameters as arguments of + other_literal so that the values match (possibly covering one + parameter with a placeholder/counted variable). Since there also can + be duplicates in the argumets of other_literal, we cannot operate on + the arguments directly, but instead operate on the positions. The method returns [] if there is no possible mapping and otherwise - yields the mappings one by one. + yields the mappings from the positions of other to the invariant + variables or -1 one by one. """ - allowed_omissions = len(other_literal.args) - len(self.order) - # All parts of an invariant always use all non-counted variables, so - # len(self.order) corresponds to the number of invariant parameters - # (the arity of the invariant). So we can/must omit allowed_omissions - # many arguments of other_literal when matching invariant parameters - # with arguments. + allowed_omissions = len(other_literal.args) - self.arity() + # All parts of an invariant always use all non-counted variables, of + # which we have arity many. So we must omit allowed_omissions many + # arguments of other_literal when matching invariant parameters with + # arguments. if allowed_omissions not in (0, 1): # There may be at most one counted variable. return [] own_parameters = self.get_parameters(own_literal) - # own_parameters is a list containing at position i the value of the - # i-th invariant parameter in own_literal. - arg_to_ordered_pos = invert_list(own_parameters) + # own_parameters is a dictionary mapping the invariant parameters to + # the corresponding parameter of own_literal + ownarg_to_invariant_parameters = defaultdict(list) + for x, y in own_parameters.items(): + ownarg_to_invariant_parameters[y].append(x) + other_arg_to_pos = invert_list(other_literal.args) # other_arg_to_pos maps every argument of other_literal to the # lists of positions in which it is occuring in other_literal, e.g. @@ -247,19 +214,20 @@ def possible_mappings(self, own_literal, other_literal): # we remember the correspondance of positions for this value in # factored_mapping. If all values can be covered, we instatiate the # complete factored_mapping, computing all possibilities to map - # positions from own_literal to positions from other_literal. + # positions from other_literal to invariant parameters (or -1 if the + # position is omitted). for key, other_positions in other_arg_to_pos.items(): - own_positions = arg_to_ordered_pos.get(key, []) + inv_params = ownarg_to_invariant_parameters[key] # all positions at which key occurs as argument in own_literal - len_diff = len(own_positions) - len(other_positions) + len_diff = len(inv_params) - len(other_positions) if len_diff >= 1 or len_diff <= -2 or len_diff == -1 and not allowed_omissions: # mapping of the literals is not possible with at most one # counted variable. return [] if len_diff: - own_positions.append(-1) + inv_params.append(-1) allowed_omissions = 0 - factored_mapping.append((other_positions, own_positions)) + factored_mapping.append((other_positions, inv_params)) return instantiate_factored_mapping(factored_mapping) def possible_matches(self, own_literal, other_literal): @@ -272,48 +240,42 @@ def possible_matches(self, own_literal, other_literal): parameter positions of other_literal to the parameter positions of own_literal such that the extended invariant can use other_literal to balance own_literal. From these position mapping, we can extract - the order field for the invariant part. - - Consider for an example of the "self" InvariantPart "forall ?u, - ?v, ?w(P(?u, ?v, ?w) is non-increasing" and let own_literal be P(?a, ?b, - ?c) and other_literal be Q(?b, ?c, ?d, ?a)). The only possible mapping - from positions of Q to positions of P (or -1) is [0->1, 1->2, 2->-1, - 3->0] for which we create a new Invariant Part Q(?v, ?w, _. ?u) with - the third argument being counted. + the new the invariant part. + + Consider for an example of the "self" InvariantPart "forall ?@v0, + ?@v1, ?@v2(P(?@v0, ?@v1, ?@v2) is non-increasing" and let + own_literal be P(?a, ?b, ?c) and other_literal be Q(?b, ?c, ?d, ?a). + The only possible mapping from positions of Q to invariant variables + of P (or -1) is [0->?@v1, 1->?@v2, 2->-1, 3->?@v0] for which we + create a new Invariant Part Q(?@v1, ?@v2, _. ?@v0) with the third + argument being counted. """ - assert self.predicate == own_literal.predicate + assert self.atom.predicate == own_literal.predicate result = [] for mapping in self.possible_mappings(own_literal, other_literal): - new_order = [None] * len(self.order) + args = ["_"] * len(other_literal.args) omitted = -1 - for (other_pos, own_pos) in mapping: - if own_pos == -1: + for (other_pos, inv_var) in mapping: + if inv_var == -1: omitted = other_pos else: - new_order[own_pos] = other_pos - # TODO This only works because in the initial invariant - # candidates the numbering of invariant parameters matches - # the order of the corresponding arguments in the - # predicate. To make this work in general, we need to - # consider a potential order difference in self.order. - result.append(InvariantPart(other_literal.predicate, new_order, omitted)) + args[other_pos] = inv_var + atom = pddl.Atom(other_literal.predicate, args) + result.append(InvariantPart(atom, omitted)) return result - def matches(self, other, own_literal, other_literal): - return self.get_parameters(own_literal) == other.get_parameters(other_literal) - class Invariant: # An invariant is a logical expression of the type - # forall V1...Vk: sum_(part in parts) weight(part, V1, ..., Vk) <= 1. + # forall ?@v1...?@vk: sum_(part in parts) weight(part, ?@v1, ..., ?@vk) <= 1. # k is called the arity of the invariant. - # A "part" is a symbolic fact only variable symbols in {V1, ..., Vk, X}; - # the symbol X may occur at most once. + # A "part" is an atom that only contains arguments from {?@v1, ..., ?@vk, _}; + # the symbol _ may occur at most once. def __init__(self, parts): self.parts = frozenset(parts) - self.predicates = {part.predicate for part in parts} - self.predicate_to_part = {part.predicate: part for part in parts} + self.predicates = {part.atom.predicate for part in parts} + self.predicate_to_part = {part.atom.predicate: part for part in parts} assert len(self.parts) == len(self.predicates) def __eq__(self, other): @@ -346,22 +308,21 @@ def get_parameters(self, atom): def instantiate(self, parameters): return [part.instantiate(parameters) for part in self.parts] - def get_covering_assignment(self, parameters, atom): - """The parameters are the (current names of the) parameters of the - invariant, the atom is the one that should be covered. - This is only called for atoms with a predicate for which the - invariant has a part. It returns a constraint that requires that - each parameter of the invariant matches the corresponding argument - of the given atom. - - Example: If the atom is P(?a, ?b, ?c), the invariant part for P - is {P 0 2 [1]} and the invariant parameters are given by ["?v0", - "?v1"] then the invariant part expressed with these parameters would - be P(?v0 ?x ?v1) with ?x being the counted variable. The method thus - returns the constraint (?v0 = ?a and ?v2 = ?c). + def get_covering_assignment(self, literal): + """This is only called for atoms with a predicate for which the + invariant has a part. It returns an assignment constraint that + requires that each parameter of the invariant matches the + corresponding argument of the given literal. + + Example: If the literal is P(?a, ?b, ?c), the invariant part for P + is P(?@v0, _, ?@v1) then the method returns the constraint (?@v0 = ?a + and ?@v1 = ?c). It is irrelevant whether the literal is negated. """ - part = self.predicate_to_part[atom.predicate] - return part.get_assignment(parameters, atom) + part = self.predicate_to_part[literal.predicate] + equalities = [(inv_param, literal.args[pos]) + for pos, inv_param in enumerate(part.atom.args) + if pos != part.omitted_pos] # alternatively inv_param != "_" + return constraints.Assignment(equalities) # If there were more parts for the same predicate, we would have to # consider more than one assignment (disjunctively). # We assert earlier that this is not the case. @@ -370,7 +331,7 @@ def check_balance(self, balance_checker, enqueue_func): # Check balance for this hypothesis. actions_to_check = set() for part in self.parts: - actions_to_check |= balance_checker.get_threats(part.predicate) + actions_to_check |= balance_checker.get_threats(part.atom.predicate) for action in sorted(actions_to_check, key=lambda a: (a.name, a.parameters)): heavy_action = balance_checker.get_heavy_action(action) @@ -386,7 +347,6 @@ def operator_too_heavy(self, h_action): add_effects = [eff for eff in h_action.effects if not eff.literal.negated and self.predicate_to_part.get(eff.literal.predicate)] - inv_vars = find_unique_variables(h_action, self) if len(add_effects) <= 1: return False @@ -394,8 +354,8 @@ def operator_too_heavy(self, h_action): for eff1, eff2 in itertools.combinations(add_effects, 2): system = constraints.ConstraintSystem() ensure_inequality(system, eff1.literal, eff2.literal) - ensure_cover(system, eff1.literal, self, inv_vars) - ensure_cover(system, eff2.literal, self, inv_vars) + ensure_cover(system, eff1.literal, self) + ensure_cover(system, eff2.literal, self) ensure_conjunction_sat(system, get_literals(h_action.precondition), get_literals(eff1.condition), get_literals(eff2.condition), @@ -407,7 +367,6 @@ def operator_too_heavy(self, h_action): def operator_unbalanced(self, action, enqueue_func): logging.debug(f"Checking Invariant {self} for action {action.name}") - inv_vars = find_unique_variables(action, self) relevant_effs = [eff for eff in action.effects if self.predicate_to_part.get(eff.literal.predicate)] add_effects = [eff for eff in relevant_effs @@ -415,7 +374,7 @@ def operator_unbalanced(self, action, enqueue_func): del_effects = [eff for eff in relevant_effs if eff.literal.negated] for eff in add_effects: - if self.add_effect_unbalanced(action, eff, del_effects, inv_vars, + if self.add_effect_unbalanced(action, eff, del_effects, enqueue_func): return True logging.debug(f"Balanced") @@ -423,7 +382,7 @@ def operator_unbalanced(self, action, enqueue_func): def add_effect_unbalanced(self, action, add_effect, del_effects, - inv_vars, enqueue_func): + enqueue_func): # We build for every delete effect that is possibly covered by this # invariant a constraint system that will be unsolvable if the delete # effect balances the add effect. Large parts of the constraint system @@ -442,7 +401,7 @@ def add_effect_unbalanced(self, action, add_effect, del_effects, # Determine a constraint that minimally relates invariant parameters to # variables and constants so that the add_effect is covered by the # invariant. - threat_assignment = self.get_covering_assignment(inv_vars, add_effect.literal) + threat_assignment = self.get_covering_assignment(add_effect.literal) # The assignment can imply equivalences between variables (and with # constants). For example if the invariant part is {p 1 2 3 [0]} and # the add effect is p(?x ?y ?y a) then we would know that the invariant @@ -485,7 +444,7 @@ def add_effect_unbalanced(self, action, add_effect, del_effects, action_param_system.add_negative_clause(negative_clause) for del_effect in del_effects: - if self.balances(del_effect, add_effect, inv_vars, + if self.balances(del_effect, add_effect, add_effect_produced_by_pred, threat_assignment, action_param_system): logging.debug(f"Invariant {self}: add effect {add_effect.literal} balanced for action {action.name} by del effect {del_effect.literal}") @@ -505,7 +464,7 @@ def refine_candidate(self, add_effect, action, enqueue_func): del_eff.literal): enqueue_func(Invariant(self.parts.union((match,)))) - def balances(self, del_effect, add_effect, inv_vars, produced_by_pred, + def balances(self, del_effect, add_effect, produced_by_pred, threat_assignment, action_param_system): """Returns whether the del_effect is guaranteed to balance the add effect where the input is such that: @@ -517,7 +476,7 @@ def balances(self, del_effect, add_effect, inv_vars, produced_by_pred, threat).""" system = constraints.ConstraintSystem() - ensure_cover(system, del_effect.literal, self, inv_vars) + ensure_cover(system, del_effect.literal, self) ensure_inequality(system, add_effect.literal, del_effect.literal) # makes sure that the add and the delete effect do not affect the same From 667a493454e07526c1f00ae7f1dffc7588e38dfa Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Thu, 18 Jan 2024 09:44:15 +0100 Subject: [PATCH 09/27] [issue1133] improving comments and names of method and parameter --- src/translate/invariants.py | 33 ++++++++++++++++++--------------- 1 file changed, 18 insertions(+), 15 deletions(-) diff --git a/src/translate/invariants.py b/src/translate/invariants.py index e9c1c952cf..5e5b8a7384 100644 --- a/src/translate/invariants.py +++ b/src/translate/invariants.py @@ -211,11 +211,12 @@ def possible_mappings(self, own_literal, other_literal): # and compare the number of occurrences in other_literal to those in # own_literal. If the difference of these numbers allows us to cover # other_literal with the (still) permitted number of counted variables, - # we remember the correspondance of positions for this value in - # factored_mapping. If all values can be covered, we instatiate the - # complete factored_mapping, computing all possibilities to map - # positions from other_literal to invariant parameters (or -1 if the - # position is omitted). + # we store the correspondance of all argument positions of + # other_literal for this value to the invariant parameters at these + # positions in factored_mapping. If all values can be covered, we + # instatiate the complete factored_mapping, computing all possibilities + # to map positions from other_literal to invariant parameters (or -1 if + # the position is omitted). for key, other_positions in other_arg_to_pos.items(): inv_params = ownarg_to_invariant_parameters[key] # all positions at which key occurs as argument in own_literal @@ -232,7 +233,7 @@ def possible_mappings(self, own_literal, other_literal): def possible_matches(self, own_literal, other_literal): """This method is used when an action had an unbalanced add effect - own_literal. The action has a delete effect on literal + on own_literal. The action has a delete effect on literal other_literal, so we try to refine the invariant such that it also covers the delete effect. @@ -240,10 +241,10 @@ def possible_matches(self, own_literal, other_literal): parameter positions of other_literal to the parameter positions of own_literal such that the extended invariant can use other_literal to balance own_literal. From these position mapping, we can extract - the new the invariant part. + the new invariant part. Consider for an example of the "self" InvariantPart "forall ?@v0, - ?@v1, ?@v2(P(?@v0, ?@v1, ?@v2) is non-increasing" and let + ?@v1, ?@v2 P(?@v0, ?@v1, ?@v2) is non-increasing" and let own_literal be P(?a, ?b, ?c) and other_literal be Q(?b, ?c, ?d, ?a). The only possible mapping from positions of Q to invariant variables of P (or -1) is [0->?@v1, 1->?@v2, 2->-1, 3->?@v0] for which we @@ -486,7 +487,7 @@ def balances(self, del_effect, add_effect, produced_by_pred, new_sys = system.combine(action_param_system) new_sys.add_assignment(threat_assignment) if self.add_effect_potentially_produced(threat_assignment, produced_by_pred): - implies_system = self.imply_del_effect(del_effect, produced_by_pred) + implies_system = self.imply_consumption(del_effect, produced_by_pred) if not implies_system: return False new_sys = new_sys.combine(implies_system) @@ -503,19 +504,21 @@ def add_effect_potentially_produced(self, threat_assignment, produced_by_pred): ensure_conjunction_sat(system, *itertools.chain(produced_by_pred.values())) return system.is_solvable() - def imply_del_effect(self, del_effect, lhs_by_pred): - """returns a constraint system that is solvable if lhs implies - the del effect (only if lhs is satisfiable). If a solvable - lhs never implies the del effect, return None.""" - # del_effect.cond and del_effect.atom must be implied by lhs + def imply_consumption(self, del_effect, literals_by_pred): + """Returns a constraint system that is solvable if the conjunction of + literals occurring as values in dictionary literals_by_pred implies + the consumption of the atom of the delete effect. We return None if + we detect that the constraint system would never be solvable. + """ implies_system = constraints.ConstraintSystem() for literal in itertools.chain(get_literals(del_effect.condition), [del_effect.literal.negate()]): poss_assignments = [] - for match in lhs_by_pred[literal.predicate]: + for match in literals_by_pred[literal.predicate]: if match.negated != literal.negated: continue else: + # match implies literal iff they agree on each argument a = constraints.Assignment(list(zip(literal.args, match.args))) poss_assignments.append(a) if not poss_assignments: From f61460344536f593d900dfda75ff949ff72c7297 Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Thu, 18 Jan 2024 14:26:49 +0100 Subject: [PATCH 10/27] [issue1133] restructure code to prevent unnecessary computations --- src/translate/constraints.py | 17 +++----- src/translate/invariants.py | 85 ++++++++++++++++++++++++------------ 2 files changed, 63 insertions(+), 39 deletions(-) diff --git a/src/translate/constraints.py b/src/translate/constraints.py index 6190acc0f7..a338120788 100644 --- a/src/translate/constraints.py +++ b/src/translate/constraints.py @@ -11,16 +11,6 @@ def __str__(self): for (v1, v2) in self.parts]) return "(%s)" % disj - def is_satisfiable(self): - for part in self.parts: - if part[0] != part[1]: - return True - return False - - def apply_mapping(self, m): - new_parts = [(m.get(v1, v1), m.get(v2, v2)) for (v1, v2) in self.parts] - return NegativeClause(new_parts) - class Assignment: def __init__(self, equalities): @@ -105,8 +95,11 @@ def __str__(self): def _all_clauses_satisfiable(self, assignment): mapping = assignment.get_mapping() for neg_clause in self.neg_clauses: - clause = neg_clause.apply_mapping(mapping) - if not clause.is_satisfiable(): + for inequality in neg_clause.parts: + a, b = inequality + if mapping.get(a, a) != mapping.get(b, b): + break + else: return False return True diff --git a/src/translate/invariants.py b/src/translate/invariants.py index 5e5b8a7384..aee04bb9bb 100644 --- a/src/translate/invariants.py +++ b/src/translate/invariants.py @@ -385,7 +385,7 @@ def operator_unbalanced(self, action, enqueue_func): def add_effect_unbalanced(self, action, add_effect, del_effects, enqueue_func): # We build for every delete effect that is possibly covered by this - # invariant a constraint system that will be unsolvable if the delete + # invariant a constraint system that will be solvable if the delete # effect balances the add effect. Large parts of the constraint system # are independent of the delete effect, so we precompute them first. @@ -399,17 +399,19 @@ def add_effect_unbalanced(self, action, add_effect, del_effects, get_literals(add_effect.literal.negate())): add_effect_produced_by_pred[lit.predicate].append(lit) - # Determine a constraint that minimally relates invariant parameters to - # variables and constants so that the add_effect is covered by the - # invariant. + # threat_assignment is a conjunction of equalities that sets each + # invariant parameter equal to its value in add_effect.literal. threat_assignment = self.get_covering_assignment(add_effect.literal) + + if not self._can_produce_threat(threat_assignment, + add_effect_produced_by_pred): + return False + # The assignment can imply equivalences between variables (and with - # constants). For example if the invariant part is {p 1 2 3 [0]} and - # the add effect is p(?x ?y ?y a) then we would know that the invariant - # part is only threatened by the add effect if the first two invariant - # parameters are equal (and if ?x and ?y are the action parameters, it - # is equal to the second action parameter ?y) and the third invariant - # parameter is a. + # constants). For example if the invariant part is P(_ ?@v0 ?@v1 ?@v2) + # and the add effect is P(?x ?y ?y a) then we would know that the + # invariant part is only threatened by the add effect if the first two + # invariant parameters are equal and the third parameter is a. # The add effect must be balanced in all threatening action # applications. We thus must adapt the constraint system such that it @@ -475,36 +477,65 @@ def balances(self, del_effect, add_effect, produced_by_pred, - action_param_system contains contraints that action parameters are not fixed to be equivalent (except the add effect is otherwise not threat).""" + + implies_system = self._imply_consumption(del_effect, produced_by_pred) + if not implies_system: + # it is impossible to guarantee that every production by add_effect + # implies a consumption by del effect. + return False + # We will build a system that is solvable if the delete effect is + # guaranteed to balance the add effect for this invariant. system = constraints.ConstraintSystem() + system.add_assignment(threat_assignment) + # invariant parameters equal the corresponding arguments of the add + # effect atom. + ensure_cover(system, del_effect.literal, self) - + # invariant parameters equal the corresponding arguments of the add + # effect atom. + + system = system.combine(implies_system) + # possible assignments such that a production by the add + # effect implies a consumption by the delete effect. + + # So far, the system implicitly represents all possibilities + # how every production of the add effect has a consumption by the + # delete effect while both atoms are covered by the invariant. However, + # we did not yet consider add-after-delete semantics and we include + # possibilities that restrict the action parameters. To prevent these, + # we in the following add a number of negative clauses. + + system = system.combine(action_param_system) + # prevent restricting assignments of action parameters (must be + # balanced independent of the concrete action instantiation). + ensure_inequality(system, add_effect.literal, del_effect.literal) - # makes sure that the add and the delete effect do not affect the same - # atom (so that the delete effect is ignored due to the - # add-after-delete semantics). - - new_sys = system.combine(action_param_system) - new_sys.add_assignment(threat_assignment) - if self.add_effect_potentially_produced(threat_assignment, produced_by_pred): - implies_system = self.imply_consumption(del_effect, produced_by_pred) - if not implies_system: - return False - new_sys = new_sys.combine(implies_system) - if not new_sys.is_solvable(): - return False + # if the add effect and the delete effect affect the same predicate + # then their arguments must differ in at least one position. + + if not system.is_solvable(): + # The system is solvable if there is a consistenst possibility to + return False - logging.debug(f"{new_sys}") + logging.debug(f"{system}") return True - def add_effect_potentially_produced(self, threat_assignment, produced_by_pred): + def _can_produce_threat(self, threat_assignment, produced_by_pred): + """Input threat_assignment contains an assignment constraint with + equalities between invariant parameters and variables or objects. + The values of produced_by_pred are literals (characterizing when an + add effect can produce its atom). + + Return whether it is possible that the add effect can produce + a threat for the invariant.""" system = constraints.ConstraintSystem() system.add_assignment(threat_assignment) ensure_conjunction_sat(system, *itertools.chain(produced_by_pred.values())) return system.is_solvable() - def imply_consumption(self, del_effect, literals_by_pred): + def _imply_consumption(self, del_effect, literals_by_pred): """Returns a constraint system that is solvable if the conjunction of literals occurring as values in dictionary literals_by_pred implies the consumption of the atom of the delete effect. We return None if From dfd6e300590dc85345fb096e00bee806feaf2142 Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Thu, 18 Jan 2024 17:19:18 +0100 Subject: [PATCH 11/27] [issue1133] remove logging, add output if threat test is relevant --- src/translate/invariants.py | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/src/translate/invariants.py b/src/translate/invariants.py index aee04bb9bb..0d1e3a0c03 100644 --- a/src/translate/invariants.py +++ b/src/translate/invariants.py @@ -336,9 +336,9 @@ def check_balance(self, balance_checker, enqueue_func): for action in sorted(actions_to_check, key=lambda a: (a.name, a.parameters)): heavy_action = balance_checker.get_heavy_action(action) - logging.debug(f"Checking Invariant {self} wrt action {action.name}") +# logging.debug(f"Checking Invariant {self} wrt action {action.name}") if self.operator_too_heavy(heavy_action): - logging.debug("too heavy") +# logging.debug("too heavy") return False if self.operator_unbalanced(action, enqueue_func): return False @@ -367,7 +367,7 @@ def operator_too_heavy(self, h_action): return False def operator_unbalanced(self, action, enqueue_func): - logging.debug(f"Checking Invariant {self} for action {action.name}") +# logging.debug(f"Checking Invariant {self} for action {action.name}") relevant_effs = [eff for eff in action.effects if self.predicate_to_part.get(eff.literal.predicate)] add_effects = [eff for eff in relevant_effs @@ -378,7 +378,7 @@ def operator_unbalanced(self, action, enqueue_func): if self.add_effect_unbalanced(action, eff, del_effects, enqueue_func): return True - logging.debug(f"Balanced") +# logging.debug(f"Balanced") return False @@ -405,6 +405,7 @@ def add_effect_unbalanced(self, action, add_effect, del_effects, if not self._can_produce_threat(threat_assignment, add_effect_produced_by_pred): + print("Threat cannot be produced.") return False # The assignment can imply equivalences between variables (and with @@ -450,7 +451,7 @@ def add_effect_unbalanced(self, action, add_effect, del_effects, if self.balances(del_effect, add_effect, add_effect_produced_by_pred, threat_assignment, action_param_system): - logging.debug(f"Invariant {self}: add effect {add_effect.literal} balanced for action {action.name} by del effect {del_effect.literal}") +# logging.debug(f"Invariant {self}: add effect {add_effect.literal} balanced for action {action.name} by del effect {del_effect.literal}") return False # The balance check fails => Generate new candidates. @@ -518,7 +519,7 @@ def balances(self, del_effect, add_effect, produced_by_pred, # The system is solvable if there is a consistenst possibility to return False - logging.debug(f"{system}") +# logging.debug(f"{system}") return True @@ -530,6 +531,8 @@ def _can_produce_threat(self, threat_assignment, produced_by_pred): Return whether it is possible that the add effect can produce a threat for the invariant.""" + # TODO after profiling: Can be benefit from implementing this directly? + # Is it even necessary at all? system = constraints.ConstraintSystem() system.add_assignment(threat_assignment) ensure_conjunction_sat(system, *itertools.chain(produced_by_pred.values())) From bc7c3d7f928e406040bfab14e9b2595f91817552 Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Thu, 18 Jan 2024 18:33:22 +0100 Subject: [PATCH 12/27] [issue1133] remove useless method _can_produce_threat --- src/translate/invariants.py | 20 -------------------- 1 file changed, 20 deletions(-) diff --git a/src/translate/invariants.py b/src/translate/invariants.py index 0d1e3a0c03..aec903b87a 100644 --- a/src/translate/invariants.py +++ b/src/translate/invariants.py @@ -403,11 +403,6 @@ def add_effect_unbalanced(self, action, add_effect, del_effects, # invariant parameter equal to its value in add_effect.literal. threat_assignment = self.get_covering_assignment(add_effect.literal) - if not self._can_produce_threat(threat_assignment, - add_effect_produced_by_pred): - print("Threat cannot be produced.") - return False - # The assignment can imply equivalences between variables (and with # constants). For example if the invariant part is P(_ ?@v0 ?@v1 ?@v2) # and the add effect is P(?x ?y ?y a) then we would know that the @@ -523,21 +518,6 @@ def balances(self, del_effect, add_effect, produced_by_pred, return True - def _can_produce_threat(self, threat_assignment, produced_by_pred): - """Input threat_assignment contains an assignment constraint with - equalities between invariant parameters and variables or objects. - The values of produced_by_pred are literals (characterizing when an - add effect can produce its atom). - - Return whether it is possible that the add effect can produce - a threat for the invariant.""" - # TODO after profiling: Can be benefit from implementing this directly? - # Is it even necessary at all? - system = constraints.ConstraintSystem() - system.add_assignment(threat_assignment) - ensure_conjunction_sat(system, *itertools.chain(produced_by_pred.values())) - return system.is_solvable() - def _imply_consumption(self, del_effect, literals_by_pred): """Returns a constraint system that is solvable if the conjunction of literals occurring as values in dictionary literals_by_pred implies From 51ccdcd75704fef7e5efec65d1a9def34eddc750 Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Thu, 18 Jan 2024 18:45:44 +0100 Subject: [PATCH 13/27] [issue1133] move computation from separate function into single caller --- src/translate/invariants.py | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/src/translate/invariants.py b/src/translate/invariants.py index aec903b87a..f6c629852a 100644 --- a/src/translate/invariants.py +++ b/src/translate/invariants.py @@ -15,13 +15,6 @@ # we currently keep the assumption that each predicate occurs at most once # in every invariant. -def invert_list(alist): - """Example: invert_list([?a, ?b, ?a]) = {'?a': [0, 2], '?b': [1]}""" - result = defaultdict(list) - for pos, arg in enumerate(alist): - result[arg].append(pos) - return result - def instantiate_factored_mapping(pairs): """Input pairs is a list [(preimg1, img1), ..., (preimgn, imgn)]. @@ -201,10 +194,13 @@ def possible_mappings(self, own_literal, other_literal): for x, y in own_parameters.items(): ownarg_to_invariant_parameters[y].append(x) - other_arg_to_pos = invert_list(other_literal.args) # other_arg_to_pos maps every argument of other_literal to the # lists of positions in which it is occuring in other_literal, e.g. # for P(?a, ?b, ?a), other_arg_to_pos["?a"] = [0, 2]. + other_arg_to_pos = defaultdict(list) + for pos, arg in enumerate(other_literal.args): + other_arg_to_pos[arg].append(pos) + factored_mapping = [] # We iterate over all values occuring as arguments in other_literal From cadca57f643f0a1fcffefa113c9efbacee33c7ef Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Thu, 18 Jan 2024 22:44:42 +0100 Subject: [PATCH 14/27] [issue1133] rename and restructure components of ConstraintSystem --- src/translate/constraints.py | 149 ++++++++++++++++++----------------- src/translate/invariants.py | 42 +++++----- 2 files changed, 99 insertions(+), 92 deletions(-) diff --git a/src/translate/constraints.py b/src/translate/constraints.py index a338120788..8647ba5569 100644 --- a/src/translate/constraints.py +++ b/src/translate/constraints.py @@ -1,18 +1,18 @@ import itertools +from typing import Iterable, List, Tuple -class NegativeClause: +class InequalityDisjunction: # disjunction of inequalities - def __init__(self, parts): + def __init__(self, parts: List[Tuple[str, str]]): self.parts = parts assert len(parts) def __str__(self): - disj = " or ".join(["(%s != %s)" % (v1, v2) - for (v1, v2) in self.parts]) - return "(%s)" % disj + disj = " or ".join([f"({v1} != {v2})" for (v1, v2) in self.parts]) + return f"({disj})" -class Assignment: +class EqualityConjunction: def __init__(self, equalities): self.equalities = tuple(equalities) # represents a conjunction of expressions ?x = ?y or ?x = d @@ -23,9 +23,8 @@ def __init__(self, equalities): self.eq_classes = None def __str__(self): - conj = " and ".join(["(%s = %s)" % (v1, v2) - for (v1, v2) in self.equalities]) - return "(%s)" % conj + conj = " and ".join([f"({v1} = {v2})" for (v1, v2) in self.equalities]) + return f"({conj})" def _compute_equivalence_classes(self): eq_classes = {} @@ -76,78 +75,84 @@ def get_mapping(self): class ConstraintSystem: + """A ConstraintSystem stores two parts, both talking about the equality or + inequality of strings (representing objects, variables or invariant + parameters): + - equality_DNFs is a list containing lists of EqualityConjunctions. + Each EqualityConjunction represents an expression of the form + (x1 = y1 and ... and xn = yn). A list of EqualityConjunctions can be + interpreted as a disjunction of such expressions. + - ineq_disjunctions is a list of InequalityDisjunctions. Each of them + represents a expression of the form (u1 != v1 or ... or um !=i vm). + + We say that the system is solvable if we can pick from each list of + EqualityConjunctions in equality_DNFs one EquivalenceConjunction such + that the finest equivalence relation induced by all the equivalences in + the conjunctions is + - consistent, i.e. no equivalence class contains more than one object, + and + - for every disjunction in ineq_disjunctions there is at least one + inequality such that the two terms are in different equivalence + classes.""" + def __init__(self): - self.combinatorial_assignments = [] - self.neg_clauses = [] + self.equality_DNFs = [] + self.ineq_disjunctions = [] def __str__(self): - combinatorial_assignments = [] - for comb_assignment in self.combinatorial_assignments: - disj = " or ".join([str(assig) for assig in comb_assignment]) + equality_DNFs = [] + for eq_DNF in self.equality_DNFs: + disj = " or ".join([str(eq_conjunction) + for eq_conjunction in eq_DNF]) disj = "(%s)" % disj - combinatorial_assignments.append(disj) - assigs = " and\n".join(combinatorial_assignments) + equality_DNFs.append(disj) + equality_part = " and\n".join(equality_DNFs) - neg_clauses = [str(clause) for clause in self.neg_clauses] - neg_clauses = " and ".join(neg_clauses) - return assigs + "(" + neg_clauses + ")" + ineq_disjunctions = [str(clause) for clause in self.ineq_disjunctions] + inequality_part = " and ".join(ineq_disjunctions) + return f"{equality_part} ({inequality_part})" - def _all_clauses_satisfiable(self, assignment): - mapping = assignment.get_mapping() - for neg_clause in self.neg_clauses: - for inequality in neg_clause.parts: - a, b = inequality - if mapping.get(a, a) != mapping.get(b, b): - break - else: - return False - return True - - def _combine_assignments(self, assignments): - new_equalities = [] - for a in assignments: - new_equalities.extend(a.equalities) - return Assignment(new_equalities) - - def add_assignment(self, assignment): - self.add_assignment_disjunction([assignment]) - - def add_assignment_disjunction(self, assignments): - self.combinatorial_assignments.append(assignments) - - def add_negative_clause(self, negative_clause): - self.neg_clauses.append(negative_clause) - - def combine(self, other): - """Combines two constraint systems to a new system""" - combined = ConstraintSystem() - combined.combinatorial_assignments = (self.combinatorial_assignments + - other.combinatorial_assignments) - combined.neg_clauses = self.neg_clauses + other.neg_clauses - return combined - - def copy(self): - other = ConstraintSystem() - other.combinatorial_assignments = list(self.combinatorial_assignments) - other.neg_clauses = list(self.neg_clauses) - return other - - def dump(self): - print("AssignmentSystem:") - for comb_assignment in self.combinatorial_assignments: - disj = " or ".join([str(assig) for assig in comb_assignment]) - print(" ASS: ", disj) - for neg_clause in self.neg_clauses: - print(" NEG: ", str(neg_clause)) + def _combine_equality_conjunctions(self, eq_conjunctions: + Iterable[EqualityConjunction]) -> None: + all_eq = itertools.chain.from_iterable(c.equalities + for c in eq_conjunctions) + return EqualityConjunction(all_eq) + + def add_equality_conjunction(self, eq_conjunction: EqualityConjunction): + self.add_equality_DNF([eq_conjunction]) + + def add_equality_DNF(self, equality_DNF: List[EqualityConjunction]) -> None: + self.equality_DNFs.append(equality_DNF) + + def add_inequality_disjunction(self, ineq_disj: InequalityDisjunction): + self.ineq_disjunctions.append(ineq_disj) + + def extend(self, other: "ConstraintSystem") -> None: + self.equality_DNFs.extend(other.equality_DNFs) + self.ineq_disjunctions.extend(other.ineq_disjunctions) def is_solvable(self): - """Check whether the combinatorial assignments include at least - one consistent assignment under which the negative clauses - are satisfiable""" - for assignments in itertools.product(*self.combinatorial_assignments): - combined = self._combine_assignments(assignments) + # cf. top of class for explanation + def inequality_disjunction_ok(ineq_disj, representative): + for inequality in ineq_disj.parts: + a, b = inequality + if representative.get(a, a) != representative.get(b, b): + return True + return False + + for eq_conjunction in itertools.product(*self.equality_DNFs): + combined = self._combine_equality_conjunctions(eq_conjunction) if not combined.is_consistent(): continue - if self._all_clauses_satisfiable(combined): + # check whether with the finest equivalence relation induced by the + # combined equality conjunction there is in each inequality + # disjunction an inequality where the two terms are in different + # equivalence classes. + representative = combined.get_mapping() + for ineq_disjunction in self.ineq_disjunctions: + if not inequality_disjunction_ok(ineq_disjunction, + representative): + break + else: return True return False diff --git a/src/translate/invariants.py b/src/translate/invariants.py index f6c629852a..a179993737 100644 --- a/src/translate/invariants.py +++ b/src/translate/invariants.py @@ -57,7 +57,8 @@ def ensure_conjunction_sat(system, *parts): We add the following constraints for each literal to the system: - - for (not (= x y)): x != y (as a NegativeClause with one entry(x,y)), + - for (not (= x y)): x != y (as an InequalityDisjunction with one entry + (x,y)), - for (= x y): x = y - for predicates that occur with a positive and negative literal, we consider every combination of a positive one (e.g. P(x, y, z)) and @@ -68,13 +69,14 @@ def ensure_conjunction_sat(system, *parts): for literal in itertools.chain(*parts): if literal.predicate == "=": # use (in)equalities in conditions if literal.negated: - n = constraints.NegativeClause([literal.args]) - system.add_negative_clause(n) + d = constraints.InequalityDisjunction([literal.args]) + system.add_inequality_disjunction(d) else: - a = constraints.Assignment([literal.args]) + a = constraints.EqualityConjunction([literal.args]) # TODO an assignment x=y expects x to be a variable, not an # object. Do we need to handle this here? - system.add_assignment_disjunction([a]) + print("Hier?", type(a)) + system.add_equality_DNF([a]) else: if literal.negated: neg[literal.predicate].add(literal) @@ -87,15 +89,15 @@ def ensure_conjunction_sat(system, *parts): for negatom in neg[pred]: parts = list(zip(negatom.args, posatom.args)) if parts: - negative_clause = constraints.NegativeClause(parts) - system.add_negative_clause(negative_clause) + ineq_disj = constraints.InequalityDisjunction(parts) + system.add_inequality_disjunction(ineq_disj) def ensure_cover(system, literal, invariant): """Modifies the constraint system such that it is only solvable if the invariant covers the literal.""" a = invariant.get_covering_assignment(literal) - system.add_assignment_disjunction([a]) + system.add_equality_DNF([a]) def ensure_inequality(system, literal1, literal2): @@ -108,7 +110,7 @@ def ensure_inequality(system, literal1, literal2): (x != a or y != b or z != c).""" if (literal1.predicate == literal2.predicate and literal1.args): parts = list(zip(literal1.args, literal2.args)) - system.add_negative_clause(constraints.NegativeClause(parts)) + system.add_inequality_disjunction(constraints.InequalityDisjunction(parts)) class InvariantPart: @@ -319,7 +321,7 @@ def get_covering_assignment(self, literal): equalities = [(inv_param, literal.args[pos]) for pos, inv_param in enumerate(part.atom.args) if pos != part.omitted_pos] # alternatively inv_param != "_" - return constraints.Assignment(equalities) + return constraints.EqualityConjunction(equalities) # If there were more parts for the same predicate, we would have to # consider more than one assignment (disjunctively). # We assert earlier that this is not the case. @@ -428,15 +430,15 @@ def add_effect_unbalanced(self, action, add_effect, del_effects, # does not need to be a specific constant. So we may not bind # it to a constant when balancing the add effect. for c in constants: - negative_clause = constraints.NegativeClause([(param, c)]) - action_param_system.add_negative_clause(negative_clause) + ineq_disj = constraints.InequalityDisjunction([(param, c)]) + action_param_system.add_inequality_disjunction(ineq_disj) for (n1, n2) in itertools.combinations(params, 2): if mapping.get(n1, n1) != mapping.get(n2, n2): # n1 and n2 don't have to be equivalent to cover the add # effect, so we require for the solutions that they do not # set n1 and n2 equal. - negative_clause = constraints.NegativeClause([(n1, n2)]) - action_param_system.add_negative_clause(negative_clause) + ineq_disj = constraints.InequalityDisjunction([(n1, n2)]) + action_param_system.add_inequality_disjunction(ineq_disj) for del_effect in del_effects: if self.balances(del_effect, add_effect, @@ -479,7 +481,7 @@ def balances(self, del_effect, add_effect, produced_by_pred, # We will build a system that is solvable if the delete effect is # guaranteed to balance the add effect for this invariant. system = constraints.ConstraintSystem() - system.add_assignment(threat_assignment) + system.add_equality_conjunction(threat_assignment) # invariant parameters equal the corresponding arguments of the add # effect atom. @@ -487,7 +489,7 @@ def balances(self, del_effect, add_effect, produced_by_pred, # invariant parameters equal the corresponding arguments of the add # effect atom. - system = system.combine(implies_system) + system.extend(implies_system) # possible assignments such that a production by the add # effect implies a consumption by the delete effect. @@ -496,9 +498,9 @@ def balances(self, del_effect, add_effect, produced_by_pred, # delete effect while both atoms are covered by the invariant. However, # we did not yet consider add-after-delete semantics and we include # possibilities that restrict the action parameters. To prevent these, - # we in the following add a number of negative clauses. + # we in the following add a number of inequality disjunctions. - system = system.combine(action_param_system) + system.extend(action_param_system) # prevent restricting assignments of action parameters (must be # balanced independent of the concrete action instantiation). @@ -529,9 +531,9 @@ def _imply_consumption(self, del_effect, literals_by_pred): continue else: # match implies literal iff they agree on each argument - a = constraints.Assignment(list(zip(literal.args, match.args))) + a = constraints.EqualityConjunction(list(zip(literal.args, match.args))) poss_assignments.append(a) if not poss_assignments: return None - implies_system.add_assignment_disjunction(poss_assignments) + implies_system.add_equality_DNF(poss_assignments) return implies_system From c0c55d83c002790e8bba1b7605b26f9c3c38d569 Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Thu, 18 Jan 2024 23:13:54 +0100 Subject: [PATCH 15/27] [issue1133] major revision constraints.py (mostly clearer names and comments) --- src/translate/constraints.py | 59 +++++++++++++++++++----------------- src/translate/invariants.py | 35 +++++++++++---------- 2 files changed, 49 insertions(+), 45 deletions(-) diff --git a/src/translate/constraints.py b/src/translate/constraints.py index 8647ba5569..7e34bc55d6 100644 --- a/src/translate/constraints.py +++ b/src/translate/constraints.py @@ -15,12 +15,12 @@ def __str__(self): class EqualityConjunction: def __init__(self, equalities): self.equalities = tuple(equalities) - # represents a conjunction of expressions ?x = ?y or ?x = d - # with ?x, ?y being variables and d being a domain value + # represents a conjunction of expressions x = y, where x,y are strings + # representing objects, variables or invariant parameters. - self.consistent = None - self.mapping = None - self.eq_classes = None + self._consistent = None + self._representative = None # dictionary + self._eq_classes = None def __str__(self): conj = " and ".join([f"({v1} = {v2})" for (v1, v2) in self.equalities]) @@ -37,41 +37,46 @@ def _compute_equivalence_classes(self): c1.update(c2) for elem in c2: eq_classes[elem] = c1 - self.eq_classes = eq_classes + self._eq_classes = eq_classes - def _compute_mapping(self): - if not self.eq_classes: + def _compute_representatives(self): + if not self._eq_classes: self._compute_equivalence_classes() - # create mapping: each key is mapped to the smallest - # element in its equivalence class (with objects being - # smaller than variables) - mapping = {} - for eq_class in self.eq_classes.values(): + # each element of an equivalence class gets the same representative. If + # the equivalence class contains a single object, the representative is + # this object. (If it contains more than one object, the assignment is + # inconsistent and we don't store representatives.) + # (with objects being smaller than variables) + representative = {} + for eq_class in self._eq_classes.values(): + if next(iter(eq_class)) in representative: + continue # we already processed this equivalence class variables = [item for item in eq_class if item.startswith("?")] constants = [item for item in eq_class if not item.startswith("?")] + if len(constants) >= 2: - self.consistent = False - self.mapping = None + self._consistent = False + self._representative = None return if constants: set_val = constants[0] else: - set_val = min(variables) + set_val = variables[0] for entry in eq_class: - mapping[entry] = set_val - self.consistent = True - self.mapping = mapping + representative[entry] = set_val + self._consistent = True + self._representative = representative def is_consistent(self): - if self.consistent is None: - self._compute_mapping() - return self.consistent + if self._consistent is None: + self._compute_representatives() + return self._consistent - def get_mapping(self): - if self.consistent is None: - self._compute_mapping() - return self.mapping + def get_representative(self): + if self._consistent is None: + self._compute_representatives() + return self._representative class ConstraintSystem: @@ -148,7 +153,7 @@ def inequality_disjunction_ok(ineq_disj, representative): # combined equality conjunction there is in each inequality # disjunction an inequality where the two terms are in different # equivalence classes. - representative = combined.get_mapping() + representative = combined.get_representative() for ineq_disjunction in self.ineq_disjunctions: if not inequality_disjunction_ok(ineq_disjunction, representative): diff --git a/src/translate/invariants.py b/src/translate/invariants.py index a179993737..9fea6458bf 100644 --- a/src/translate/invariants.py +++ b/src/translate/invariants.py @@ -6,7 +6,7 @@ import pddl import tools -#logging.basicConfig(level=logging.DEBUG) +# logging.basicConfig(level=logging.DEBUG) # Notes: # All parts of an invariant always use all non-counted variables # -> the arity of all predicates covered by an invariant is either the @@ -145,7 +145,7 @@ def arity(self): if self.omitted_pos == -1: return len(self.atom.args) else: - return len(self.atom.args) - 1 + return len(self.atom.args) - 1 def get_parameters(self, literal): """Returns a dictionary, mapping the invariant parameters to the @@ -156,7 +156,7 @@ def get_parameters(self, literal): def instantiate(self, parameters_tuple): parameters = dict(parameters_tuple) - args = [parameters[arg] if arg != "_" else "?X" + args = [parameters[arg] if arg != "_" else "?X" for arg in self.atom.args] return pddl.Atom(self.atom.predicate, args) @@ -202,7 +202,7 @@ def possible_mappings(self, own_literal, other_literal): other_arg_to_pos = defaultdict(list) for pos, arg in enumerate(other_literal.args): other_arg_to_pos[arg].append(pos) - + factored_mapping = [] # We iterate over all values occuring as arguments in other_literal @@ -379,7 +379,6 @@ def operator_unbalanced(self, action, enqueue_func): # logging.debug(f"Balanced") return False - def add_effect_unbalanced(self, action, add_effect, del_effects, enqueue_func): # We build for every delete effect that is possibly covered by this @@ -419,13 +418,14 @@ def add_effect_unbalanced(self, action, add_effect, del_effects, constants.add(a) params = [p.name for p in action.parameters] action_param_system = constraints.ConstraintSystem() - mapping = threat_assignment.get_mapping() + representative = threat_assignment.get_representative() # The assignment is a conjunction of equalities between invariant # parameters and the variables and constants occurring in the - # add_effect literal. The mapping maps every term to its representative - # in the coarsest equivalence class induced by the equalities. + # add_effect literal. Dictionary representative maps every term to its + # representative in the finest equivalence relation induced by the + # equalities. for param in params: - if mapping.get(param, param)[0] == "?": + if representative.get(param, param)[0] == "?": # for the add effect being a threat to the invariant, param # does not need to be a specific constant. So we may not bind # it to a constant when balancing the add effect. @@ -433,13 +433,13 @@ def add_effect_unbalanced(self, action, add_effect, del_effects, ineq_disj = constraints.InequalityDisjunction([(param, c)]) action_param_system.add_inequality_disjunction(ineq_disj) for (n1, n2) in itertools.combinations(params, 2): - if mapping.get(n1, n1) != mapping.get(n2, n2): + if representative.get(n1, n1) != representative.get(n2, n2): # n1 and n2 don't have to be equivalent to cover the add # effect, so we require for the solutions that they do not # set n1 and n2 equal. ineq_disj = constraints.InequalityDisjunction([(n1, n2)]) action_param_system.add_inequality_disjunction(ineq_disj) - + for del_effect in del_effects: if self.balances(del_effect, add_effect, add_effect_produced_by_pred, @@ -471,7 +471,7 @@ def balances(self, del_effect, add_effect, produced_by_pred, - action_param_system contains contraints that action parameters are not fixed to be equivalent (except the add effect is otherwise not threat).""" - + implies_system = self._imply_consumption(del_effect, produced_by_pred) if not implies_system: # it is impossible to guarantee that every production by add_effect @@ -484,15 +484,15 @@ def balances(self, del_effect, add_effect, produced_by_pred, system.add_equality_conjunction(threat_assignment) # invariant parameters equal the corresponding arguments of the add # effect atom. - + ensure_cover(system, del_effect.literal, self) # invariant parameters equal the corresponding arguments of the add # effect atom. - + system.extend(implies_system) # possible assignments such that a production by the add # effect implies a consumption by the delete effect. - + # So far, the system implicitly represents all possibilities # how every production of the add effect has a consumption by the # delete effect while both atoms are covered by the invariant. However, @@ -503,11 +503,11 @@ def balances(self, del_effect, add_effect, produced_by_pred, system.extend(action_param_system) # prevent restricting assignments of action parameters (must be # balanced independent of the concrete action instantiation). - + ensure_inequality(system, add_effect.literal, del_effect.literal) # if the add effect and the delete effect affect the same predicate # then their arguments must differ in at least one position. - + if not system.is_solvable(): # The system is solvable if there is a consistenst possibility to return False @@ -515,7 +515,6 @@ def balances(self, del_effect, add_effect, produced_by_pred, # logging.debug(f"{system}") return True - def _imply_consumption(self, del_effect, literals_by_pred): """Returns a constraint system that is solvable if the conjunction of literals occurring as values in dictionary literals_by_pred implies From a680c38328f99d6bb3d17d7796267870b66f3771 Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Sat, 20 Jan 2024 12:00:35 +0100 Subject: [PATCH 16/27] [issue1133] different way to forbid to bind variables to constants (and lots of renaming, comments, ...) --- src/translate/constraints.py | 29 +++-- src/translate/invariants.py | 199 ++++++++++++++++------------------- 2 files changed, 112 insertions(+), 116 deletions(-) diff --git a/src/translate/constraints.py b/src/translate/constraints.py index 7e34bc55d6..1f65f2fa0d 100644 --- a/src/translate/constraints.py +++ b/src/translate/constraints.py @@ -45,7 +45,7 @@ def _compute_representatives(self): # each element of an equivalence class gets the same representative. If # the equivalence class contains a single object, the representative is - # this object. (If it contains more than one object, the assignment is + # this object. (If it contains more than one object, the conjunction is # inconsistent and we don't store representatives.) # (with objects being smaller than variables) representative = {} @@ -89,20 +89,24 @@ class ConstraintSystem: interpreted as a disjunction of such expressions. - ineq_disjunctions is a list of InequalityDisjunctions. Each of them represents a expression of the form (u1 != v1 or ... or um !=i vm). + - not_constant is a list of strings. We say that the system is solvable if we can pick from each list of EqualityConjunctions in equality_DNFs one EquivalenceConjunction such that the finest equivalence relation induced by all the equivalences in the conjunctions is - consistent, i.e. no equivalence class contains more than one object, - and - for every disjunction in ineq_disjunctions there is at least one inequality such that the two terms are in different equivalence - classes.""" + classes. + - every element of not_constant is not in the same equivalence class + as a constant. + We refer to the equivalence relation as the solution of the system.""" def __init__(self): self.equality_DNFs = [] self.ineq_disjunctions = [] + self.not_constant = [] def __str__(self): equality_DNFs = [] @@ -111,11 +115,11 @@ def __str__(self): for eq_conjunction in eq_DNF]) disj = "(%s)" % disj equality_DNFs.append(disj) - equality_part = " and\n".join(equality_DNFs) + eq_part = " and\n".join(equality_DNFs) ineq_disjunctions = [str(clause) for clause in self.ineq_disjunctions] - inequality_part = " and ".join(ineq_disjunctions) - return f"{equality_part} ({inequality_part})" + ineq_part = " and ".join(ineq_disjunctions) + return f"{eq_part} ({ineq_part}) (not constant {self.not_constant}" def _combine_equality_conjunctions(self, eq_conjunctions: Iterable[EqualityConjunction]) -> None: @@ -132,9 +136,13 @@ def add_equality_DNF(self, equality_DNF: List[EqualityConjunction]) -> None: def add_inequality_disjunction(self, ineq_disj: InequalityDisjunction): self.ineq_disjunctions.append(ineq_disj) + def add_not_constant(self, not_constant: str) -> None: + self.not_constants.append(not_constant) + def extend(self, other: "ConstraintSystem") -> None: self.equality_DNFs.extend(other.equality_DNFs) self.ineq_disjunctions.extend(other.ineq_disjunctions) + self.not_constant.extend(other.not_constant) def is_solvable(self): # cf. top of class for explanation @@ -150,10 +158,13 @@ def inequality_disjunction_ok(ineq_disj, representative): if not combined.is_consistent(): continue # check whether with the finest equivalence relation induced by the - # combined equality conjunction there is in each inequality - # disjunction an inequality where the two terms are in different - # equivalence classes. + # combined equality conjunction there is no element of not_constant + # in the same equivalence class as a constant and that in each + # inequality disjunction there is an inequality where the two terms + # are in different equivalence classes. representative = combined.get_representative() + if any(representative[s][0] != "?" for s in self.not_constant): + continue for ineq_disjunction in self.ineq_disjunctions: if not inequality_disjunction_ok(ineq_disjunction, representative): diff --git a/src/translate/invariants.py b/src/translate/invariants.py index 9fea6458bf..fba535f477 100644 --- a/src/translate/invariants.py +++ b/src/translate/invariants.py @@ -1,19 +1,16 @@ from collections import defaultdict import itertools -import logging import constraints import pddl import tools -# logging.basicConfig(level=logging.DEBUG) # Notes: # All parts of an invariant always use all non-counted variables # -> the arity of all predicates covered by an invariant is either the -# number of the invariant variables or this value + 1 +# number of the invariant parameters or this value + 1 # -# we currently keep the assumption that each predicate occurs at most once -# in every invariant. +# We only consider invariants where each predicate occurs in at most one part. def instantiate_factored_mapping(pairs): @@ -73,9 +70,6 @@ def ensure_conjunction_sat(system, *parts): system.add_inequality_disjunction(d) else: a = constraints.EqualityConjunction([literal.args]) - # TODO an assignment x=y expects x to be a variable, not an - # object. Do we need to handle this here? - print("Hier?", type(a)) system.add_equality_DNF([a]) else: if literal.negated: @@ -94,10 +88,11 @@ def ensure_conjunction_sat(system, *parts): def ensure_cover(system, literal, invariant): - """Modifies the constraint system such that it is only solvable if the - invariant covers the literal.""" - a = invariant.get_covering_assignment(literal) - system.add_equality_DNF([a]) + """Modifies the constraint system such that in every solution the invariant + covers the literal (= invariant parameters are equivalent to the + corresponding argument in the literal).""" + cover = invariant._get_cover_equivalence_conjunction(literal) + system.add_equality_DNF([cover]) def ensure_inequality(system, literal1, literal2): @@ -307,15 +302,16 @@ def get_parameters(self, atom): def instantiate(self, parameters): return [part.instantiate(parameters) for part in self.parts] - def get_covering_assignment(self, literal): + def _get_cover_equivalence_conjunction(self, literal): """This is only called for atoms with a predicate for which the - invariant has a part. It returns an assignment constraint that - requires that each parameter of the invariant matches the - corresponding argument of the given literal. + invariant has a part. It returns an equivalence conjunction that + requires every invariant parameter to be equal to the corresponding + argument of the given literal. For the result, we do not consider + whether the literal is negated. Example: If the literal is P(?a, ?b, ?c), the invariant part for P is P(?@v0, _, ?@v1) then the method returns the constraint (?@v0 = ?a - and ?@v1 = ?c). It is irrelevant whether the literal is negated. + and ?@v1 = ?c). """ part = self.predicate_to_part[literal.predicate] equalities = [(inv_param, literal.args[pos]) @@ -334,15 +330,13 @@ def check_balance(self, balance_checker, enqueue_func): for action in sorted(actions_to_check, key=lambda a: (a.name, a.parameters)): heavy_action = balance_checker.get_heavy_action(action) -# logging.debug(f"Checking Invariant {self} wrt action {action.name}") - if self.operator_too_heavy(heavy_action): -# logging.debug("too heavy") + if self._operator_too_heavy(heavy_action): return False - if self.operator_unbalanced(action, enqueue_func): + if self._operator_unbalanced(action, enqueue_func): return False return True - def operator_too_heavy(self, h_action): + def _operator_too_heavy(self, h_action): add_effects = [eff for eff in h_action.effects if not eff.literal.negated and self.predicate_to_part.get(eff.literal.predicate)] @@ -364,8 +358,7 @@ def operator_too_heavy(self, h_action): return True return False - def operator_unbalanced(self, action, enqueue_func): -# logging.debug(f"Checking Invariant {self} for action {action.name}") + def _operator_unbalanced(self, action, enqueue_func): relevant_effs = [eff for eff in action.effects if self.predicate_to_part.get(eff.literal.predicate)] add_effects = [eff for eff in relevant_effs @@ -373,14 +366,13 @@ def operator_unbalanced(self, action, enqueue_func): del_effects = [eff for eff in relevant_effs if eff.literal.negated] for eff in add_effects: - if self.add_effect_unbalanced(action, eff, del_effects, - enqueue_func): + if self._add_effect_unbalanced(action, eff, del_effects, + enqueue_func): return True -# logging.debug(f"Balanced") return False - def add_effect_unbalanced(self, action, add_effect, del_effects, - enqueue_func): + def _add_effect_unbalanced(self, action, add_effect, del_effects, + enqueue_func): # We build for every delete effect that is possibly covered by this # invariant a constraint system that will be solvable if the delete # effect balances the add effect. Large parts of the constraint system @@ -396,11 +388,11 @@ def add_effect_unbalanced(self, action, add_effect, del_effects, get_literals(add_effect.literal.negate())): add_effect_produced_by_pred[lit.predicate].append(lit) - # threat_assignment is a conjunction of equalities that sets each - # invariant parameter equal to its value in add_effect.literal. - threat_assignment = self.get_covering_assignment(add_effect.literal) + # add_cover is an equality conjunction that sets each invariant + # parameter equal to its value in add_effect.literal. + add_cover = self._get_cover_equivalence_conjunction(add_effect.literal) - # The assignment can imply equivalences between variables (and with + # add_cover can imply equivalences between variables (and with # constants). For example if the invariant part is P(_ ?@v0 ?@v1 ?@v2) # and the add effect is P(?x ?y ?y a) then we would know that the # invariant part is only threatened by the add effect if the first two @@ -409,49 +401,41 @@ def add_effect_unbalanced(self, action, add_effect, del_effects, # The add effect must be balanced in all threatening action # applications. We thus must adapt the constraint system such that it # prevents restricting solution that set action parameters equal to - # each other or to a specific constant (if this is not already - # necessary for the threat). - constants = set(a for a in add_effect.literal.args if a[0] != "?") - for del_effect in del_effects: - for a in del_effect.literal.args: - if a[0] != "?": - constants.add(a) + # each other or to a specific constant if this is not already + # implied by the threat. params = [p.name for p in action.parameters] action_param_system = constraints.ConstraintSystem() - representative = threat_assignment.get_representative() - # The assignment is a conjunction of equalities between invariant - # parameters and the variables and constants occurring in the - # add_effect literal. Dictionary representative maps every term to its - # representative in the finest equivalence relation induced by the - # equalities. + representative = add_cover.get_representative() + # Dictionary representative maps every term to its representative in + # the finest equivalence relation induced by the equalities in + # add_cover. If the equivalence class contains an object, the + # representative is an object. for param in params: if representative.get(param, param)[0] == "?": # for the add effect being a threat to the invariant, param # does not need to be a specific constant. So we may not bind - # it to a constant when balancing the add effect. - for c in constants: - ineq_disj = constraints.InequalityDisjunction([(param, c)]) - action_param_system.add_inequality_disjunction(ineq_disj) + # it to a constant when balancing the add effect. We store this + # information here. + action_param_system.add_not_constant(param) for (n1, n2) in itertools.combinations(params, 2): if representative.get(n1, n1) != representative.get(n2, n2): # n1 and n2 don't have to be equivalent to cover the add # effect, so we require for the solutions that they do not - # set n1 and n2 equal. + # make n1 and n2 equvalent. ineq_disj = constraints.InequalityDisjunction([(n1, n2)]) action_param_system.add_inequality_disjunction(ineq_disj) for del_effect in del_effects: - if self.balances(del_effect, add_effect, - add_effect_produced_by_pred, - threat_assignment, action_param_system): -# logging.debug(f"Invariant {self}: add effect {add_effect.literal} balanced for action {action.name} by del effect {del_effect.literal}") + if self._balances(del_effect, add_effect, + add_effect_produced_by_pred, add_cover, + action_param_system): return False - # The balance check fails => Generate new candidates. - self.refine_candidate(add_effect, action, enqueue_func) + # The balance check failed => Generate new candidates. + self._refine_candidate(add_effect, action, enqueue_func) return True - def refine_candidate(self, add_effect, action, enqueue_func): + def _refine_candidate(self, add_effect, action, enqueue_func): """Refines the candidate for an add effect that is unbalanced in the action and adds the refined one to the queue.""" part = self.predicate_to_part[add_effect.literal.predicate] @@ -461,78 +445,79 @@ def refine_candidate(self, add_effect, action, enqueue_func): del_eff.literal): enqueue_func(Invariant(self.parts.union((match,)))) - def balances(self, del_effect, add_effect, produced_by_pred, - threat_assignment, action_param_system): + def _balances(self, del_effect, add_effect, produced_by_pred, + add_cover, action_param_system): """Returns whether the del_effect is guaranteed to balance the add effect where the input is such that: - produced_by_pred must be true for the add_effect to be produced, - - threat_assignment is a constraint of equalities that must be true - for the add effect threatening the invariant, and + - add_cover is an equality conjunction that sets each invariant + parameter equal to its value in add_effect. These equivalences + must be true for the add effect threatening the invariant. - action_param_system contains contraints that action parameters are - not fixed to be equivalent (except the add effect is otherwise not - threat).""" + not fixed to be equivalent or a certain constant (except the add + effect is otherwise not threat).""" - implies_system = self._imply_consumption(del_effect, produced_by_pred) - if not implies_system: + balance_system = self._balance_system(add_effect, del_effect, + produced_by_pred) + if not balance_system: # it is impossible to guarantee that every production by add_effect # implies a consumption by del effect. return False - # We will build a system that is solvable if the delete effect is - # guaranteed to balance the add effect for this invariant. + # We will overall build a system that is solvable if the delete effect + # is guaranteed to balance the add effect for this invariant. system = constraints.ConstraintSystem() - system.add_equality_conjunction(threat_assignment) - # invariant parameters equal the corresponding arguments of the add - # effect atom. + system.add_equality_conjunction(add_cover) + # In every solution, the invariant parameters must equal the + # corresponding arguments of the add effect atom. ensure_cover(system, del_effect.literal, self) - # invariant parameters equal the corresponding arguments of the add - # effect atom. - - system.extend(implies_system) - # possible assignments such that a production by the add - # effect implies a consumption by the delete effect. + # In every solution, the invariant parameters must equal the + # corresponding arguments of the delete effect atom. - # So far, the system implicitly represents all possibilities - # how every production of the add effect has a consumption by the - # delete effect while both atoms are covered by the invariant. However, - # we did not yet consider add-after-delete semantics and we include - # possibilities that restrict the action parameters. To prevent these, - # we in the following add a number of inequality disjunctions. + system.extend(balance_system) + # In every solution a production by the add effect guarantees + # a consumption by the delete effect. system.extend(action_param_system) - # prevent restricting assignments of action parameters (must be - # balanced independent of the concrete action instantiation). - - ensure_inequality(system, add_effect.literal, del_effect.literal) - # if the add effect and the delete effect affect the same predicate - # then their arguments must differ in at least one position. + # A solution may not restrict action parameters (must be balanced + # independent of the concrete action instantiation). if not system.is_solvable(): - # The system is solvable if there is a consistenst possibility to return False - -# logging.debug(f"{system}") return True - def _imply_consumption(self, del_effect, literals_by_pred): - """Returns a constraint system that is solvable if the conjunction of - literals occurring as values in dictionary literals_by_pred implies - the consumption of the atom of the delete effect. We return None if - we detect that the constraint system would never be solvable. + def _balance_system(self, add_effect, del_effect, literals_by_pred): + """Returns a constraint system that is solvable if + - the conjunction of literals occurring as values in dictionary + literals_by_pred (characterizing a threat for the invariant + through an actual production by add_effect) implies the + consumption of the atom of the delete effect, and + - the produced and consumed atom are different (otherwise by + add-after-delete semantics, the delete effect would not balance + the add effect). + + We return None if we detect that the constraint system would never + be solvable (by an incomplete cheap test). """ - implies_system = constraints.ConstraintSystem() + system = constraints.ConstraintSystem() for literal in itertools.chain(get_literals(del_effect.condition), [del_effect.literal.negate()]): - poss_assignments = [] + possibilities = [] + # possible equality conjunctions that establish that the literals + # in literals_by_pred logically imply the current literal. for match in literals_by_pred[literal.predicate]: - if match.negated != literal.negated: - continue - else: + if match.negated == literal.negated: # match implies literal iff they agree on each argument - a = constraints.EqualityConjunction(list(zip(literal.args, match.args))) - poss_assignments.append(a) - if not poss_assignments: + ec = constraints.EqualityConjunction(list(zip(literal.args, + match.args))) + possibilities.append(ec) + if not possibilities: return None - implies_system.add_equality_DNF(poss_assignments) - return implies_system + system.add_equality_DNF(possibilities) + + # if the add effect and the delete effect affect the same predicate + # then their arguments must differ in at least one position (because of + # the add-after-delete semantics). + ensure_inequality(system, add_effect.literal, del_effect.literal) + return system From d684077cd52de60036a1d45649a05c769f753f4c Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Sat, 20 Jan 2024 12:34:30 +0100 Subject: [PATCH 17/27] [issue1133] fix stupid typo --- src/translate/constraints.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/translate/constraints.py b/src/translate/constraints.py index 1f65f2fa0d..87ee0dc9a8 100644 --- a/src/translate/constraints.py +++ b/src/translate/constraints.py @@ -137,7 +137,7 @@ def add_inequality_disjunction(self, ineq_disj: InequalityDisjunction): self.ineq_disjunctions.append(ineq_disj) def add_not_constant(self, not_constant: str) -> None: - self.not_constants.append(not_constant) + self.not_constant.append(not_constant) def extend(self, other: "ConstraintSystem") -> None: self.equality_DNFs.extend(other.equality_DNFs) From 146ff80fb475d640967126de2d1bd4d8ff5d0461 Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Sat, 20 Jan 2024 13:09:42 +0100 Subject: [PATCH 18/27] [issue1133] fix another stupid typo --- src/translate/constraints.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/translate/constraints.py b/src/translate/constraints.py index 87ee0dc9a8..ed13be64a2 100644 --- a/src/translate/constraints.py +++ b/src/translate/constraints.py @@ -163,7 +163,7 @@ def inequality_disjunction_ok(ineq_disj, representative): # inequality disjunction there is an inequality where the two terms # are in different equivalence classes. representative = combined.get_representative() - if any(representative[s][0] != "?" for s in self.not_constant): + if any(representative.get(s,s)[0] != "?" for s in self.not_constant): continue for ineq_disjunction in self.ineq_disjunctions: if not inequality_disjunction_ok(ineq_disjunction, From 364eafcd2001f9a54fd9624fc3b0e8199e1f76a9 Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Sat, 20 Jan 2024 15:27:30 +0100 Subject: [PATCH 19/27] [issue1133] revert the expensive way to make the translator deterministic --- src/translate/invariants.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/translate/invariants.py b/src/translate/invariants.py index fba535f477..47e53a0173 100644 --- a/src/translate/invariants.py +++ b/src/translate/invariants.py @@ -327,8 +327,7 @@ def check_balance(self, balance_checker, enqueue_func): actions_to_check = set() for part in self.parts: actions_to_check |= balance_checker.get_threats(part.atom.predicate) - for action in sorted(actions_to_check, key=lambda a: (a.name, - a.parameters)): + for action in actions_to_check: heavy_action = balance_checker.get_heavy_action(action) if self._operator_too_heavy(heavy_action): return False From 79af53e8f336cccbed1aac8d35f643cdc0945306 Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Sat, 20 Jan 2024 15:27:34 +0100 Subject: [PATCH 20/27] Revert "[issue1133-invariants] implement lt for typed objects" It was included for the change reverted in the previous commit. This reverts commit 50603bb7f32ebb12aee387bad36ea3b392339fcc. --- src/translate/pddl/pddl_types.py | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/translate/pddl/pddl_types.py b/src/translate/pddl/pddl_types.py index 35054aa505..45d2a6286b 100644 --- a/src/translate/pddl/pddl_types.py +++ b/src/translate/pddl/pddl_types.py @@ -46,9 +46,6 @@ def __eq__(self, other): def __ne__(self, other): return not self == other - def __lt__(self, other): - return (self.name, self.type_name) < (other.name, other.type_name) - def __str__(self): return "%s: %s" % (self.name, self.type_name) From 849f4b810f34e19f53ce8a8b16e6293dffdd9899 Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Sat, 20 Jan 2024 15:31:35 +0100 Subject: [PATCH 21/27] [issue1133] style check --- src/translate/constraints.py | 3 ++- src/translate/invariant_finder.py | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/translate/constraints.py b/src/translate/constraints.py index ed13be64a2..c5a80b59dc 100644 --- a/src/translate/constraints.py +++ b/src/translate/constraints.py @@ -163,7 +163,8 @@ def inequality_disjunction_ok(ineq_disj, representative): # inequality disjunction there is an inequality where the two terms # are in different equivalence classes. representative = combined.get_representative() - if any(representative.get(s,s)[0] != "?" for s in self.not_constant): + if any(representative.get(s, s)[0] != "?" + for s in self.not_constant): continue for ineq_disjunction in self.ineq_disjunctions: if not inequality_disjunction_ok(ineq_disjunction, diff --git a/src/translate/invariant_finder.py b/src/translate/invariant_finder.py index 14993849a1..d771233ac0 100755 --- a/src/translate/invariant_finder.py +++ b/src/translate/invariant_finder.py @@ -129,7 +129,7 @@ def useful_groups(invariants, initial_facts): inv_vars = [f"?@v{i}" for i in range(invariant.arity())] parameters_tuple = tuple((var, parameters[var]) for var in inv_vars) - + parameters_tuple = tuple(sorted(x for x in parameters.items())) group_key = (invariant, parameters_tuple) if group_key not in nonempty_groups: From 7f7ef83db346c0e20eb447880c5414298eabef78 Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Sat, 20 Jan 2024 21:27:25 +0100 Subject: [PATCH 22/27] [issue1133] use int i as invariant parameters instead of ?@vi --- src/translate/constraints.py | 18 +++++---- src/translate/invariant_finder.py | 19 ++++------ src/translate/invariants.py | 62 ++++++++++++++++--------------- 3 files changed, 50 insertions(+), 49 deletions(-) diff --git a/src/translate/constraints.py b/src/translate/constraints.py index c5a80b59dc..b433078536 100644 --- a/src/translate/constraints.py +++ b/src/translate/constraints.py @@ -16,7 +16,8 @@ class EqualityConjunction: def __init__(self, equalities): self.equalities = tuple(equalities) # represents a conjunction of expressions x = y, where x,y are strings - # representing objects, variables or invariant parameters. + # representing objects or variables or ints, representing invariant + # parameters. self._consistent = None self._representative = None # dictionary @@ -47,13 +48,15 @@ def _compute_representatives(self): # the equivalence class contains a single object, the representative is # this object. (If it contains more than one object, the conjunction is # inconsistent and we don't store representatives.) - # (with objects being smaller than variables) + # (with objects being smaller than variables or invariant parameters) representative = {} for eq_class in self._eq_classes.values(): if next(iter(eq_class)) in representative: continue # we already processed this equivalence class - variables = [item for item in eq_class if item.startswith("?")] - constants = [item for item in eq_class if not item.startswith("?")] + variables = [item for item in eq_class if isinstance(item, int) or + item.startswith("?")] + constants = [item for item in eq_class if not isinstance(item, int) + and not item.startswith("?")] if len(constants) >= 2: self._consistent = False @@ -81,8 +84,8 @@ def get_representative(self): class ConstraintSystem: """A ConstraintSystem stores two parts, both talking about the equality or - inequality of strings (representing objects, variables or invariant - parameters): + inequality of strings and ints (strings representing objects or + variables, ints representing invariant parameters): - equality_DNFs is a list containing lists of EqualityConjunctions. Each EqualityConjunction represents an expression of the form (x1 = y1 and ... and xn = yn). A list of EqualityConjunctions can be @@ -163,7 +166,8 @@ def inequality_disjunction_ok(ineq_disj, representative): # inequality disjunction there is an inequality where the two terms # are in different equivalence classes. representative = combined.get_representative() - if any(representative.get(s, s)[0] != "?" + if any(not isinstance(representative.get(s, s), int) and + representative.get(s, s)[0] != "?" for s in self.not_constant): continue for ineq_disjunction in self.ineq_disjunctions: diff --git a/src/translate/invariant_finder.py b/src/translate/invariant_finder.py index d771233ac0..d016d2ec8a 100755 --- a/src/translate/invariant_finder.py +++ b/src/translate/invariant_finder.py @@ -78,14 +78,12 @@ def get_fluents(task): def get_initial_invariants(task): for predicate in get_fluents(task): - all_args = list(f"?@v{i}" for i in range(len(predicate.arguments))) - atom = pddl.Atom(predicate.name, all_args) - part = invariants.InvariantPart(atom, -1) + all_args = list(range(len(predicate.arguments))) + part = invariants.InvariantPart(predicate.name, all_args, -1) yield invariants.Invariant((part,)) for omitted in range(len(predicate.arguments)): - inv_args = all_args[0:omitted] + ["_"] + all_args[omitted:-1] - atom = pddl.Atom(predicate.name, inv_args) - part = invariants.InvariantPart(atom, omitted) + inv_args = all_args[0:omitted] + [-1] + all_args[omitted:-1] + part = invariants.InvariantPart(predicate.name, inv_args, omitted) yield invariants.Invariant((part,)) def find_invariants(task, reachable_action_params): @@ -124,13 +122,10 @@ def useful_groups(invariants, initial_facts): for invariant in predicate_to_invariants.get(atom.predicate, ()): parameters = invariant.get_parameters(atom) # we need to make the parameters dictionary hashable, so - # we store the values as a tuple in the order of the numbering of - # the invariant parameters. - inv_vars = [f"?@v{i}" for i in range(invariant.arity())] - parameters_tuple = tuple((var, parameters[var]) - for var in inv_vars) + # we store the values as a tuple + parameters_tuple = tuple(parameters[var] + for var in range(invariant.arity())) - parameters_tuple = tuple(sorted(x for x in parameters.items())) group_key = (invariant, parameters_tuple) if group_key not in nonempty_groups: nonempty_groups.add(group_key) diff --git a/src/translate/invariants.py b/src/translate/invariants.py index 47e53a0173..a7b605db4b 100644 --- a/src/translate/invariants.py +++ b/src/translate/invariants.py @@ -109,51 +109,52 @@ def ensure_inequality(system, literal1, literal2): class InvariantPart: - def __init__(self, atom, omitted_pos=-1): + def __init__(self, predicate, args, omitted_pos=-1): """There is one InvariantPart for every predicate mentioned in the - invariant. The atom of the invariant part has arguments of the form - "?@vi" for the invariant parameters and "_" at the omitted position. - If no position is omitted, omitted_pos is -1.""" - self.atom = atom + invariant. The arguments args contain numbers 0,1,... for the + invariant parameters and -1 at the omitted position. + If no position is omitted, omitted_pos is -1, otherwise it is the + index of -1 in args.""" + self.predicate = predicate + self.args = tuple(args) self.omitted_pos = omitted_pos def __eq__(self, other): # This implies equality of the omitted_pos component. - return self.atom == other.atom + return self.predicate == other.predicate and self.args == other.args def __ne__(self, other): - return self.atom != other.atom + return self.predicate != other.predicate or self.args != other.args def __le__(self, other): - return self.atom <= other.atom + return (self.predicate, self.args) <= (other.predicate, other.args) def __lt__(self, other): - return self.atom < other.atom + return (self.predicate, self.args) < (other.predicate, other.args) def __hash__(self): - return hash(self.atom) + return hash((self.predicate, self.args)) def __str__(self): - return f"{self.atom} [omitted_pos = {self.omitted_pos}]" + return f"{self.predicate}({self.args}) [omitted_pos = {self.omitted_pos}]" def arity(self): if self.omitted_pos == -1: - return len(self.atom.args) + return len(self.args) else: - return len(self.atom.args) - 1 + return len(self.args) - 1 def get_parameters(self, literal): """Returns a dictionary, mapping the invariant parameters to the corresponding values in the literal.""" return dict((arg, literal.args[pos]) - for pos, arg in enumerate(self.atom.args) + for pos, arg in enumerate(self.args) if pos != self.omitted_pos) def instantiate(self, parameters_tuple): - parameters = dict(parameters_tuple) - args = [parameters[arg] if arg != "_" else "?X" - for arg in self.atom.args] - return pddl.Atom(self.atom.predicate, args) + args = [parameters_tuple[arg] if arg != -1 else "?X" + for arg in self.args] + return pddl.Atom(self.predicate, args) def possible_mappings(self, own_literal, other_literal): """This method is used when an action had an unbalanced add effect @@ -244,18 +245,17 @@ def possible_matches(self, own_literal, other_literal): create a new Invariant Part Q(?@v1, ?@v2, _. ?@v0) with the third argument being counted. """ - assert self.atom.predicate == own_literal.predicate + assert self.predicate == own_literal.predicate result = [] for mapping in self.possible_mappings(own_literal, other_literal): - args = ["_"] * len(other_literal.args) + args = [-1] * len(other_literal.args) omitted = -1 for (other_pos, inv_var) in mapping: if inv_var == -1: omitted = other_pos else: args[other_pos] = inv_var - atom = pddl.Atom(other_literal.predicate, args) - result.append(InvariantPart(atom, omitted)) + result.append(InvariantPart(other_literal.predicate, args, omitted)) return result @@ -263,13 +263,14 @@ class Invariant: # An invariant is a logical expression of the type # forall ?@v1...?@vk: sum_(part in parts) weight(part, ?@v1, ..., ?@vk) <= 1. # k is called the arity of the invariant. - # A "part" is an atom that only contains arguments from {?@v1, ..., ?@vk, _}; - # the symbol _ may occur at most once. + # A "part" is an atom that only contains arguments from {?@v1, ..., ?@vk, -1} + # but instead of ?@vi, we store it as int i; + # the symbol -1 may occur at most once. def __init__(self, parts): self.parts = frozenset(parts) - self.predicates = {part.atom.predicate for part in parts} - self.predicate_to_part = {part.atom.predicate: part for part in parts} + self.predicate_to_part = {part.predicate: part for part in parts} + self.predicates = set(self.predicate_to_part.keys()) assert len(self.parts) == len(self.predicates) def __eq__(self, other): @@ -315,8 +316,8 @@ def _get_cover_equivalence_conjunction(self, literal): """ part = self.predicate_to_part[literal.predicate] equalities = [(inv_param, literal.args[pos]) - for pos, inv_param in enumerate(part.atom.args) - if pos != part.omitted_pos] # alternatively inv_param != "_" + for pos, inv_param in enumerate(part.args) + if inv_param != -1] # -1 if ommited return constraints.EqualityConjunction(equalities) # If there were more parts for the same predicate, we would have to # consider more than one assignment (disjunctively). @@ -326,7 +327,7 @@ def check_balance(self, balance_checker, enqueue_func): # Check balance for this hypothesis. actions_to_check = set() for part in self.parts: - actions_to_check |= balance_checker.get_threats(part.atom.predicate) + actions_to_check |= balance_checker.get_threats(part.predicate) for action in actions_to_check: heavy_action = balance_checker.get_heavy_action(action) if self._operator_too_heavy(heavy_action): @@ -410,7 +411,8 @@ def _add_effect_unbalanced(self, action, add_effect, del_effects, # add_cover. If the equivalence class contains an object, the # representative is an object. for param in params: - if representative.get(param, param)[0] == "?": + r = representative.get(param, param) + if isinstance(r, int) or r[0] == "?": # for the add effect being a threat to the invariant, param # does not need to be a specific constant. So we may not bind # it to a constant when balancing the add effect. We store this From e499d117349e047d97cb4badcf3d629fa49fa9af Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Tue, 30 Jan 2024 09:58:44 +0100 Subject: [PATCH 23/27] [issue1133] changes from code review --- src/translate/constraints.py | 38 +++++++++++++++++------------------- src/translate/invariants.py | 2 +- 2 files changed, 19 insertions(+), 21 deletions(-) diff --git a/src/translate/constraints.py b/src/translate/constraints.py index b433078536..f028607c3d 100644 --- a/src/translate/constraints.py +++ b/src/translate/constraints.py @@ -2,7 +2,6 @@ from typing import Iterable, List, Tuple class InequalityDisjunction: - # disjunction of inequalities def __init__(self, parts: List[Tuple[str, str]]): self.parts = parts assert len(parts) @@ -15,8 +14,8 @@ def __str__(self): class EqualityConjunction: def __init__(self, equalities): self.equalities = tuple(equalities) - # represents a conjunction of expressions x = y, where x,y are strings - # representing objects or variables or ints, representing invariant + # A conjunction of expressions x = y, where x,y are either strings + # that denote objects or variables, or ints that denote invariant # parameters. self._consistent = None @@ -44,26 +43,25 @@ def _compute_representatives(self): if not self._eq_classes: self._compute_equivalence_classes() - # each element of an equivalence class gets the same representative. If - # the equivalence class contains a single object, the representative is - # this object. (If it contains more than one object, the conjunction is - # inconsistent and we don't store representatives.) - # (with objects being smaller than variables or invariant parameters) + # Choose a representative for each equivalence class. Objects are + # prioritized over variables and ints, but at most one object per + # equivalence class is allowed (otherwise the conjunction is + # inconsistent). representative = {} for eq_class in self._eq_classes.values(): if next(iter(eq_class)) in representative: continue # we already processed this equivalence class variables = [item for item in eq_class if isinstance(item, int) or item.startswith("?")] - constants = [item for item in eq_class if not isinstance(item, int) - and not item.startswith("?")] + objects = [item for item in eq_class if not isinstance(item, int) + and not item.startswith("?")] - if len(constants) >= 2: + if len(objects) >= 2: self._consistent = False self._representative = None return - if constants: - set_val = constants[0] + if objects: + set_val = objects[0] else: set_val = variables[0] for entry in eq_class: @@ -89,7 +87,9 @@ class ConstraintSystem: - equality_DNFs is a list containing lists of EqualityConjunctions. Each EqualityConjunction represents an expression of the form (x1 = y1 and ... and xn = yn). A list of EqualityConjunctions can be - interpreted as a disjunction of such expressions. + interpreted as a disjunction of such expressions. So + self.equality_DNFs represents a formula of the form "⋀ ⋁ ⋀ (x = y)" + as a list of lists of EqualityConjunctions. - ineq_disjunctions is a list of InequalityDisjunctions. Each of them represents a expression of the form (u1 != v1 or ... or um !=i vm). - not_constant is a list of strings. @@ -170,10 +170,8 @@ def inequality_disjunction_ok(ineq_disj, representative): representative.get(s, s)[0] != "?" for s in self.not_constant): continue - for ineq_disjunction in self.ineq_disjunctions: - if not inequality_disjunction_ok(ineq_disjunction, - representative): - break - else: - return True + if any(not inequality_disjunction_ok(d, representative) + for d in self.ineq_disjunctions): + continue + return True return False diff --git a/src/translate/invariants.py b/src/translate/invariants.py index a7b605db4b..89591fee05 100644 --- a/src/translate/invariants.py +++ b/src/translate/invariants.py @@ -60,7 +60,7 @@ def ensure_conjunction_sat(system, *parts): - for predicates that occur with a positive and negative literal, we consider every combination of a positive one (e.g. P(x, y, z)) and a negative one (e.g. (not P(a, b, c))) and add a constraint - (x != y or y != b or z != c).""" + (x != a or y != b or z != c).""" pos = defaultdict(set) neg = defaultdict(set) for literal in itertools.chain(*parts): From beb24306761a3706e38d3beb9b8cbba41bb915ac Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Wed, 31 Jan 2024 08:34:00 +0100 Subject: [PATCH 24/27] [issue1133] more changes from code review --- src/translate/constraints.py | 6 +++--- src/translate/invariants.py | 4 +--- 2 files changed, 4 insertions(+), 6 deletions(-) diff --git a/src/translate/constraints.py b/src/translate/constraints.py index f028607c3d..a26a2c9e7f 100644 --- a/src/translate/constraints.py +++ b/src/translate/constraints.py @@ -12,8 +12,8 @@ def __str__(self): class EqualityConjunction: - def __init__(self, equalities): - self.equalities = tuple(equalities) + def __init__(self, equalities: List[Tuple[str, str]]): + self.equalities = equalities # A conjunction of expressions x = y, where x,y are either strings # that denote objects or variables, or ints that denote invariant # parameters. @@ -128,7 +128,7 @@ def _combine_equality_conjunctions(self, eq_conjunctions: Iterable[EqualityConjunction]) -> None: all_eq = itertools.chain.from_iterable(c.equalities for c in eq_conjunctions) - return EqualityConjunction(all_eq) + return EqualityConjunction(list(all_eq)) def add_equality_conjunction(self, eq_conjunction: EqualityConjunction): self.add_equality_DNF([eq_conjunction]) diff --git a/src/translate/invariants.py b/src/translate/invariants.py index 89591fee05..dec9d5ba5b 100644 --- a/src/translate/invariants.py +++ b/src/translate/invariants.py @@ -246,7 +246,6 @@ def possible_matches(self, own_literal, other_literal): argument being counted. """ assert self.predicate == own_literal.predicate - result = [] for mapping in self.possible_mappings(own_literal, other_literal): args = [-1] * len(other_literal.args) omitted = -1 @@ -255,8 +254,7 @@ def possible_matches(self, own_literal, other_literal): omitted = other_pos else: args[other_pos] = inv_var - result.append(InvariantPart(other_literal.predicate, args, omitted)) - return result + yield InvariantPart(other_literal.predicate, args, omitted) class Invariant: From 91e21e18159475a3f556c30a05a6eddfaaf7c3a0 Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Wed, 31 Jan 2024 08:41:46 +0100 Subject: [PATCH 25/27] [issue1133] use None intead of -1 for ommitted_pos if there is no ommission --- src/translate/invariant_finder.py | 2 +- src/translate/invariants.py | 9 +++++---- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/src/translate/invariant_finder.py b/src/translate/invariant_finder.py index d016d2ec8a..4cf5753a23 100755 --- a/src/translate/invariant_finder.py +++ b/src/translate/invariant_finder.py @@ -79,7 +79,7 @@ def get_fluents(task): def get_initial_invariants(task): for predicate in get_fluents(task): all_args = list(range(len(predicate.arguments))) - part = invariants.InvariantPart(predicate.name, all_args, -1) + part = invariants.InvariantPart(predicate.name, all_args, None) yield invariants.Invariant((part,)) for omitted in range(len(predicate.arguments)): inv_args = all_args[0:omitted] + [-1] + all_args[omitted:-1] diff --git a/src/translate/invariants.py b/src/translate/invariants.py index dec9d5ba5b..36a90216df 100644 --- a/src/translate/invariants.py +++ b/src/translate/invariants.py @@ -12,6 +12,7 @@ # # We only consider invariants where each predicate occurs in at most one part. +COUNTED = -1 def instantiate_factored_mapping(pairs): """Input pairs is a list [(preimg1, img1), ..., (preimgn, imgn)]. @@ -109,11 +110,11 @@ def ensure_inequality(system, literal1, literal2): class InvariantPart: - def __init__(self, predicate, args, omitted_pos=-1): + def __init__(self, predicate, args, omitted_pos=None): """There is one InvariantPart for every predicate mentioned in the invariant. The arguments args contain numbers 0,1,... for the invariant parameters and -1 at the omitted position. - If no position is omitted, omitted_pos is -1, otherwise it is the + If no position is omitted, omitted_pos is None, otherwise it is the index of -1 in args.""" self.predicate = predicate self.args = tuple(args) @@ -139,7 +140,7 @@ def __str__(self): return f"{self.predicate}({self.args}) [omitted_pos = {self.omitted_pos}]" def arity(self): - if self.omitted_pos == -1: + if self.omitted_pos is None: return len(self.args) else: return len(self.args) - 1 @@ -248,7 +249,7 @@ def possible_matches(self, own_literal, other_literal): assert self.predicate == own_literal.predicate for mapping in self.possible_mappings(own_literal, other_literal): args = [-1] * len(other_literal.args) - omitted = -1 + omitted = None for (other_pos, inv_var) in mapping: if inv_var == -1: omitted = other_pos From 9f31ebccab8ebf11808ae080f429b6b48543615b Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Wed, 31 Jan 2024 08:48:26 +0100 Subject: [PATCH 26/27] [issue1133] use name COUNTED instead of magical number -1 --- src/translate/invariant_finder.py | 3 ++- src/translate/invariants.py | 40 +++++++++++++++---------------- 2 files changed, 22 insertions(+), 21 deletions(-) diff --git a/src/translate/invariant_finder.py b/src/translate/invariant_finder.py index 4cf5753a23..8aaee3fb99 100755 --- a/src/translate/invariant_finder.py +++ b/src/translate/invariant_finder.py @@ -82,7 +82,8 @@ def get_initial_invariants(task): part = invariants.InvariantPart(predicate.name, all_args, None) yield invariants.Invariant((part,)) for omitted in range(len(predicate.arguments)): - inv_args = all_args[0:omitted] + [-1] + all_args[omitted:-1] + inv_args = (all_args[0:omitted] + [invariants.COUNTED] + + all_args[omitted:-1]) part = invariants.InvariantPart(predicate.name, inv_args, omitted) yield invariants.Invariant((part,)) diff --git a/src/translate/invariants.py b/src/translate/invariants.py index 36a90216df..64b8683fa3 100644 --- a/src/translate/invariants.py +++ b/src/translate/invariants.py @@ -17,8 +17,8 @@ def instantiate_factored_mapping(pairs): """Input pairs is a list [(preimg1, img1), ..., (preimgn, imgn)]. For entry (preimg, img), preimg is a list of numbers and img a list of - invariant parameters or -1 of the same length. All preimages (and all - images) are pairwise disjoint, as well as the components of each + invariant parameters or COUNTED of the same length. All preimages (and + all images) are pairwise disjoint, as well as the components of each preimage/image. The function determines all possible bijections between the union of @@ -113,9 +113,9 @@ class InvariantPart: def __init__(self, predicate, args, omitted_pos=None): """There is one InvariantPart for every predicate mentioned in the invariant. The arguments args contain numbers 0,1,... for the - invariant parameters and -1 at the omitted position. + invariant parameters and COUNTED at the omitted position. If no position is omitted, omitted_pos is None, otherwise it is the - index of -1 in args.""" + index of COUNTED in args.""" self.predicate = predicate self.args = tuple(args) self.omitted_pos = omitted_pos @@ -153,7 +153,7 @@ def get_parameters(self, literal): if pos != self.omitted_pos) def instantiate(self, parameters_tuple): - args = [parameters_tuple[arg] if arg != -1 else "?X" + args = [parameters_tuple[arg] if arg != COUNTED else "?X" for arg in self.args] return pddl.Atom(self.predicate, args) @@ -176,7 +176,7 @@ def possible_mappings(self, own_literal, other_literal): The method returns [] if there is no possible mapping and otherwise yields the mappings from the positions of other to the invariant - variables or -1 one by one. + variables or COUNTED one by one. """ allowed_omissions = len(other_literal.args) - self.arity() # All parts of an invariant always use all non-counted variables, of @@ -210,8 +210,8 @@ def possible_mappings(self, own_literal, other_literal): # other_literal for this value to the invariant parameters at these # positions in factored_mapping. If all values can be covered, we # instatiate the complete factored_mapping, computing all possibilities - # to map positions from other_literal to invariant parameters (or -1 if - # the position is omitted). + # to map positions from other_literal to invariant parameters (or + # COUNTED if the position is omitted). for key, other_positions in other_arg_to_pos.items(): inv_params = ownarg_to_invariant_parameters[key] # all positions at which key occurs as argument in own_literal @@ -221,7 +221,7 @@ def possible_mappings(self, own_literal, other_literal): # counted variable. return [] if len_diff: - inv_params.append(-1) + inv_params.append(COUNTED) allowed_omissions = 0 factored_mapping.append((other_positions, inv_params)) return instantiate_factored_mapping(factored_mapping) @@ -242,16 +242,16 @@ def possible_matches(self, own_literal, other_literal): ?@v1, ?@v2 P(?@v0, ?@v1, ?@v2) is non-increasing" and let own_literal be P(?a, ?b, ?c) and other_literal be Q(?b, ?c, ?d, ?a). The only possible mapping from positions of Q to invariant variables - of P (or -1) is [0->?@v1, 1->?@v2, 2->-1, 3->?@v0] for which we - create a new Invariant Part Q(?@v1, ?@v2, _. ?@v0) with the third - argument being counted. + of P (or COUNTED) is [0->?@v1, 1->?@v2, 2->COUNTED, 3->?@v0] for + which we create a new Invariant Part Q(?@v1, ?@v2, _. ?@v0) with the + third argument being counted. """ assert self.predicate == own_literal.predicate for mapping in self.possible_mappings(own_literal, other_literal): - args = [-1] * len(other_literal.args) + args = [COUNTED] * len(other_literal.args) omitted = None for (other_pos, inv_var) in mapping: - if inv_var == -1: + if inv_var == COUNTED: omitted = other_pos else: args[other_pos] = inv_var @@ -262,9 +262,9 @@ class Invariant: # An invariant is a logical expression of the type # forall ?@v1...?@vk: sum_(part in parts) weight(part, ?@v1, ..., ?@vk) <= 1. # k is called the arity of the invariant. - # A "part" is an atom that only contains arguments from {?@v1, ..., ?@vk, -1} - # but instead of ?@vi, we store it as int i; - # the symbol -1 may occur at most once. + # A "part" is an atom that only contains arguments from {?@v1, ..., ?@vk, + # COUNTED} but instead of ?@vi, we store it as int i; COUNTED may occur at + # most once. def __init__(self, parts): self.parts = frozenset(parts) @@ -314,9 +314,9 @@ def _get_cover_equivalence_conjunction(self, literal): and ?@v1 = ?c). """ part = self.predicate_to_part[literal.predicate] - equalities = [(inv_param, literal.args[pos]) - for pos, inv_param in enumerate(part.args) - if inv_param != -1] # -1 if ommited + equalities = [(arg, literal.args[pos]) + for pos, arg in enumerate(part.args) + if arg != COUNTED] return constraints.EqualityConjunction(equalities) # If there were more parts for the same predicate, we would have to # consider more than one assignment (disjunctively). From e219be8956e608bf9f68641fccbe76bf7292dee6 Mon Sep 17 00:00:00 2001 From: Gabriele Roeger Date: Wed, 31 Jan 2024 08:55:07 +0100 Subject: [PATCH 27/27] [issue1133] forbid restricting the quantified parameters of the add effect --- src/translate/invariants.py | 27 ++++++++++++++------------- 1 file changed, 14 insertions(+), 13 deletions(-) diff --git a/src/translate/invariants.py b/src/translate/invariants.py index 64b8683fa3..f91eb11a68 100644 --- a/src/translate/invariants.py +++ b/src/translate/invariants.py @@ -399,11 +399,12 @@ def _add_effect_unbalanced(self, action, add_effect, del_effects, # The add effect must be balanced in all threatening action # applications. We thus must adapt the constraint system such that it - # prevents restricting solution that set action parameters equal to - # each other or to a specific constant if this is not already - # implied by the threat. - params = [p.name for p in action.parameters] - action_param_system = constraints.ConstraintSystem() + # prevents restricting solution that set action parameters or + # quantified variables of the add effect equal to each other or to + # a specific constant if this is not already implied by the threat. + params = [p.name for p in itertools.chain(action.parameters, + add_effect.parameters)] + param_system = constraints.ConstraintSystem() representative = add_cover.get_representative() # Dictionary representative maps every term to its representative in # the finest equivalence relation induced by the equalities in @@ -416,19 +417,19 @@ def _add_effect_unbalanced(self, action, add_effect, del_effects, # does not need to be a specific constant. So we may not bind # it to a constant when balancing the add effect. We store this # information here. - action_param_system.add_not_constant(param) + param_system.add_not_constant(param) for (n1, n2) in itertools.combinations(params, 2): if representative.get(n1, n1) != representative.get(n2, n2): # n1 and n2 don't have to be equivalent to cover the add # effect, so we require for the solutions that they do not # make n1 and n2 equvalent. ineq_disj = constraints.InequalityDisjunction([(n1, n2)]) - action_param_system.add_inequality_disjunction(ineq_disj) + param_system.add_inequality_disjunction(ineq_disj) for del_effect in del_effects: if self._balances(del_effect, add_effect, add_effect_produced_by_pred, add_cover, - action_param_system): + param_system): return False # The balance check failed => Generate new candidates. @@ -446,16 +447,16 @@ def _refine_candidate(self, add_effect, action, enqueue_func): enqueue_func(Invariant(self.parts.union((match,)))) def _balances(self, del_effect, add_effect, produced_by_pred, - add_cover, action_param_system): + add_cover, param_system): """Returns whether the del_effect is guaranteed to balance the add effect where the input is such that: - produced_by_pred must be true for the add_effect to be produced, - add_cover is an equality conjunction that sets each invariant parameter equal to its value in add_effect. These equivalences must be true for the add effect threatening the invariant. - - action_param_system contains contraints that action parameters are - not fixed to be equivalent or a certain constant (except the add - effect is otherwise not threat).""" + - param_system contains contraints that action and add_effect + parameters are not fixed to be equivalent or a certain constant + (except the add effect is otherwise not threat).""" balance_system = self._balance_system(add_effect, del_effect, produced_by_pred) @@ -479,7 +480,7 @@ def _balances(self, del_effect, add_effect, produced_by_pred, # In every solution a production by the add effect guarantees # a consumption by the delete effect. - system.extend(action_param_system) + system.extend(param_system) # A solution may not restrict action parameters (must be balanced # independent of the concrete action instantiation).