diff --git a/src/translate/constraints.py b/src/translate/constraints.py index 6190acc0f7..a26a2c9e7f 100644 --- a/src/translate/constraints.py +++ b/src/translate/constraints.py @@ -1,41 +1,30 @@ import itertools +from typing import Iterable, List, Tuple -class NegativeClause: - # disjunction of inequalities - def __init__(self, parts): +class InequalityDisjunction: + 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 - - 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) + disj = " or ".join([f"({v1} != {v2})" for (v1, v2) in self.parts]) + return f"({disj})" -class Assignment: - 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 +class EqualityConjunction: + 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. - 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(["(%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 = {} @@ -48,113 +37,141 @@ 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(): - 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 + # 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("?")] + objects = [item for item in eq_class if not isinstance(item, int) + and not item.startswith("?")] + + 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 = 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: + """A ConstraintSystem stores two parts, both talking about the equality or + 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 + 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. + + 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, + - for every disjunction in ineq_disjunctions there is at least one + inequality such that the two terms are in different equivalence + 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.combinatorial_assignments = [] - self.neg_clauses = [] + self.equality_DNFs = [] + self.ineq_disjunctions = [] + self.not_constant = [] 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) - - neg_clauses = [str(clause) for clause in self.neg_clauses] - neg_clauses = " and ".join(neg_clauses) - return assigs + "(" + neg_clauses + ")" - - 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(): - 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)) + equality_DNFs.append(disj) + eq_part = " and\n".join(equality_DNFs) + + ineq_disjunctions = [str(clause) for clause in self.ineq_disjunctions] + 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: + all_eq = itertools.chain.from_iterable(c.equalities + for c in eq_conjunctions) + return EqualityConjunction(list(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 add_not_constant(self, not_constant: str) -> None: + self.not_constant.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): - """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): - return True + # check whether with the finest equivalence relation induced by the + # 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(not isinstance(representative.get(s, s), int) and + representative.get(s, s)[0] != "?" + for s in self.not_constant): + continue + if any(not inequality_disjunction_ok(d, representative) + for d in self.ineq_disjunctions): + continue + return True return False diff --git a/src/translate/invariant_finder.py b/src/translate/invariant_finder.py index a8f32ffa59..8aaee3fb99 100755 --- a/src/translate/invariant_finder.py +++ b/src/translate/invariant_finder.py @@ -79,9 +79,12 @@ 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) + 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] + [invariants.COUNTED] + + all_args[omitted:-1]) + part = invariants.InvariantPart(predicate.name, inv_args, omitted) yield invariants.Invariant((part,)) def find_invariants(task, reachable_action_params): @@ -118,7 +121,13 @@ 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 + parameters_tuple = tuple(parameters[var] + for var in range(invariant.arity())) + + 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 ed98e4edca..f91eb11a68 100644 --- a/src/translate/invariants.py +++ b/src/translate/invariants.py @@ -8,38 +8,35 @@ # 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. - -def invert_list(alist): - result = defaultdict(list) - for pos, arg in enumerate(alist): - result[arg].append(pos) - return result +# 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)]. + For entry (preimg, img), preimg is a list of numbers and img a list of + 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 + preimgs and the union of imgs such that for every entry (preimg, 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. + """ + # 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] - return tools.cartesian_product(part_mappings) - - -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 + # all possibilities to pick one bijection for each entry + if not part_mappings: + yield [] + else: + for x in itertools.product(*part_mappings): + yield list(itertools.chain.from_iterable(x)) def get_literals(condition): @@ -54,17 +51,27 @@ 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 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 + a negative one (e.g. (not P(a, b, c))) and add a constraint + (x != a or y != b or z != c).""" pos = defaultdict(set) neg = defaultdict(set) 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]) - system.add_assignment_disjunction([a]) + a = constraints.EqualityConjunction([literal.args]) + system.add_equality_DNF([a]) else: if literal.negated: neg[literal.predicate].add(literal) @@ -77,125 +84,192 @@ 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, 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 would - # not be true but the depending code in parts relies on this assumption - system.add_assignment_disjunction(a) +def ensure_cover(system, literal, invariant): + """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): """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)""" - if (literal1.predicate == literal2.predicate and - literal1.args): + 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)) - system.add_negative_clause(constraints.NegativeClause(parts)) + system.add_inequality_disjunction(constraints.InequalityDisjunction(parts)) class InvariantPart: - def __init__(self, predicate, order, 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 COUNTED at the omitted position. + If no position is omitted, omitted_pos is None, otherwise it is the + index of COUNTED in args.""" self.predicate = predicate - self.order = order + self.args = tuple(args) 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.predicate == other.predicate and self.args == other.args def __ne__(self, other): - return self.predicate != other.predicate or self.order != other.order + return self.predicate != other.predicate or self.args != other.args def __le__(self, other): - return self.predicate <= other.predicate or self.order <= other.order + return (self.predicate, self.args) <= (other.predicate, other.args) def __lt__(self, other): - return self.predicate < other.predicate or self.order < other.order + return (self.predicate, self.args) < (other.predicate, other.args) def __hash__(self): - return hash((self.predicate, tuple(self.order))) + return hash((self.predicate, self.args)) 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.predicate}({self.args}) [omitted_pos = {self.omitted_pos}]" def arity(self): - return len(self.order) - - def get_assignment(self, parameters, literal): - equalities = [(arg, literal.args[argpos]) - for arg, argpos in zip(parameters, self.order)] - return constraints.Assignment(equalities) + if self.omitted_pos is None: + return len(self.args) + else: + return len(self.args) - 1 def get_parameters(self, 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 + """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.args) + if pos != self.omitted_pos) + + def instantiate(self, parameters_tuple): + args = [parameters_tuple[arg] if arg != COUNTED else "?X" + for arg in self.args] return pddl.Atom(self.predicate, args) def possible_mappings(self, own_literal, other_literal): - allowed_omissions = len(other_literal.args) - len(self.order) + """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. + + 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 from the positions of other to the invariant + 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 + # 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) - arg_to_ordered_pos = invert_list(own_parameters) - other_arg_to_pos = invert_list(other_literal.args) + # 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 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 + # 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 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 + # COUNTED if the position is omitted). for key, other_positions in other_arg_to_pos.items(): - own_positions = arg_to_ordered_pos.get(key, []) - len_diff = len(own_positions) - len(other_positions) + inv_params = ownarg_to_invariant_parameters[key] + # all positions at which key occurs as argument in own_literal + 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(COUNTED) 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): + """This method is used when an action had an unbalanced add effect + 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. + + 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 new 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 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 - 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 + args = [COUNTED] * len(other_literal.args) + omitted = None + for (other_pos, inv_var) in mapping: + if inv_var == COUNTED: + omitted = other_pos else: - new_order[value] = key - result.append(InvariantPart(other_literal.predicate, new_order, omitted)) - return result - - def matches(self, other, own_literal, other_literal): - return self.get_parameters(own_literal) == other.get_parameters(other_literal) + args[other_pos] = inv_var + yield InvariantPart(other_literal.predicate, args, omitted) 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, + # 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) - self.predicates = {part.predicate 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): @@ -214,7 +288,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 @@ -228,11 +302,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): - 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 + 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 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). + """ + part = self.predicate_to_part[literal.predicate] + 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). + # We assert earlier that this is not the case. def check_balance(self, balance_checker, enqueue_func): # Check balance for this hypothesis. @@ -241,17 +329,16 @@ def check_balance(self, balance_checker, enqueue_func): 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): + 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)] - inv_vars = find_unique_variables(h_action, self) if len(add_effects) <= 1: return False @@ -259,8 +346,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), @@ -270,8 +357,7 @@ def operator_too_heavy(self, h_action): return True return False - def operator_unbalanced(self, action, enqueue_func): - inv_vars = find_unique_variables(action, self) + 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 @@ -279,59 +365,80 @@ 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, - enqueue_func): + if self._add_effect_unbalanced(action, eff, del_effects, + 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 - assigs = self.get_covering_assignments(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) - 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) + 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 + # 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) + + # 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) + + # 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 + # 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 + # 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 + # add_cover. If the equivalence class contains an object, the + # representative is an object. + for param in params: + 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 + # information here. + 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)]) + param_system.add_inequality_disjunction(ineq_disj) 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: + if self._balances(del_effect, add_effect, + add_effect_produced_by_pred, add_cover, + param_system): return False - # Otherwise, 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): - """refines the candidate for an add effect that is unbalanced in the - action and adds the refined one to the queue""" + 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] 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: @@ -339,75 +446,79 @@ 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, produced_by_pred, + 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. + - 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) + 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 overall build a system that is solvable if the delete effect + # is guaranteed to balance the add effect for this invariant. 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) + system.add_equality_conjunction(add_cover) + # In every solution, the invariant parameters must equal the + # corresponding arguments of the add effect atom. - ensure_inequality(system, add_effect.literal, del_effect.literal) + ensure_cover(system, del_effect.literal, self) + # In every solution, the invariant parameters must equal the + # corresponding arguments of the delete effect atom. - 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 - new_sys = new_sys.combine(implies_system) - if not new_sys.is_solvable(): - still_unbalanced.append(renaming) - return still_unbalanced - - def lhs_satisfiable(self, renaming, lhs_by_pred): - system = renaming.copy() - ensure_conjunction_sat(system, *itertools.chain(lhs_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 - implies_system = constraints.ConstraintSystem() + system.extend(balance_system) + # In every solution a production by the add effect guarantees + # a consumption by the delete effect. + + system.extend(param_system) + # A solution may not restrict action parameters (must be balanced + # independent of the concrete action instantiation). + + if not system.is_solvable(): + return False + return True + + 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). + """ + 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]: - if match.negated != literal.negated: - continue - else: - a = constraints.Assignment(list(zip(literal.args, match.args))) - poss_assignments.append(a) - if not 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: + # match implies literal iff they agree on each argument + ec = constraints.EqualityConjunction(list(zip(literal.args, + match.args))) + possibilities.append(ec) + if not possibilities: return None - implies_system.add_assignment_disjunction(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 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.