From 3dc4286b1bcfa103bdcf56797305b903de502145 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Tue, 19 Jul 2022 14:59:05 +0000 Subject: [PATCH 01/48] a predicate assumption class --- tilings/assumptions.py | 185 ++++++++++++++++++++++++++++------------- tilings/tiling.py | 106 +++++++++++++++-------- 2 files changed, 201 insertions(+), 90 deletions(-) diff --git a/tilings/assumptions.py b/tilings/assumptions.py index f476a5d6..eed5d58e 100644 --- a/tilings/assumptions.py +++ b/tilings/assumptions.py @@ -13,17 +13,19 @@ from tilings import Tiling -class TrackingAssumption: +class Assumption: """ - An assumption used to keep track of the occurrences of a set of gridded - permutations. + An abstract class for assumption made on tilings. This consists of + a set of cells that are passed around according to forward and + backward maps of strategies. """ def __init__(self, gps: Iterable[GriddedPerm]): self.gps = tuple(sorted(set(gps))) + self.cells = frozenset(gp.pos[0] for gp in self.gps) @classmethod - def from_cells(cls, cells: Iterable[Cell]) -> "TrackingAssumption": + def from_cells(cls, cells: Iterable[Cell]) -> "Assumption": gps = [GriddedPerm.single_cell((0,), cell) for cell in cells] return cls(gps) @@ -31,7 +33,7 @@ def avoiding( self, obstructions: Iterable[GriddedPerm], active_cells: Optional[Iterable[Cell]] = None, - ) -> "TrackingAssumption": + ) -> "Assumption": """ Return the tracking absumption where all of the gridded perms avoiding the obstructions are removed. If active_cells is not None, then any @@ -49,30 +51,6 @@ def avoiding( ) return self.__class__(tuple(gp for gp in self.gps if gp.avoids(*obstructions))) - def get_value(self, gp: GriddedPerm) -> int: - """ - Return the number of occurrences of each of the gridded perms being track in - the gridded perm gp. - """ - return len(list(chain.from_iterable(p.occurrences_in(gp) for p in self.gps))) - - def get_components(self, tiling: "Tiling") -> List[List[GriddedPerm]]: - """ - Return the lists of gps that count exactly one occurrence. - Only implemented for when a size one gp is in a point cell. - """ - return [ - [gp] for gp in self.gps if len(gp) == 1 and gp.pos[0] in tiling.point_cells - ] - - def remove_components(self, tiling: "Tiling") -> "TrackingAssumption": - """ - Return the TrackingAssumption found by removing all the components - found by the get_components method. - """ - gps_to_remove = set(chain.from_iterable(self.get_components(tiling))) - return self.__class__(gp for gp in self.gps if gp not in gps_to_remove) - def to_jsonable(self) -> dict: """Return a dictionary form of the assumption.""" c = self.__class__ @@ -87,31 +65,60 @@ def from_dict(cls, d: dict) -> "TrackingAssumption": """Return the assumption from the json dict representation.""" module = import_module(d["class_module"]) AssClass: Type["TrackingAssumption"] = getattr(module, d["assumption"]) - assert issubclass( - AssClass, TrackingAssumption - ), "Not a valid TrackingAssumption" + assert issubclass(AssClass, Assumption), "Not a valid Assumption" gps = [GriddedPerm.from_dict(gp) for gp in d["gps"]] return AssClass(gps) def __eq__(self, other) -> bool: - if other.__class__ == TrackingAssumption: + if other.__class__ == self.__class__: return bool(self.gps == other.gps) return NotImplemented def __lt__(self, other) -> bool: - if isinstance(other, TrackingAssumption): + if isinstance(other, Assumption): key_self = (self.__class__.__name__, self.gps) key_other = (other.__class__.__name__, other.gps) return key_self < key_other return NotImplemented def __hash__(self) -> int: - return hash(self.gps) + return hash(hash(self.gps) + hash(self.__class__.__name__)) def __repr__(self) -> str: return self.__class__.__name__ + f"({self.gps})" - def __str__(self): + +class TrackingAssumption(Assumption): + """ + An assumption used to keep track of the occurrences of a set of gridded + permutations. + """ + + def get_value(self, gp: GriddedPerm) -> int: + """ + Return the number of occurrences of each of the gridded perms being track in + the gridded perm gp. + """ + return len(list(chain.from_iterable(p.occurrences_in(gp) for p in self.gps))) + + def get_components(self, tiling: "Tiling") -> List[List[GriddedPerm]]: + """ + Return the lists of gps that count exactly one occurrence. + Only implemented for when a size one gp is in a point cell. + """ + return [ + [gp] for gp in self.gps if len(gp) == 1 and gp.pos[0] in tiling.point_cells + ] + + def remove_components(self, tiling: "Tiling") -> "TrackingAssumption": + """ + Return the TrackingAssumption found by removing all the components + found by the get_components method. + """ + gps_to_remove = set(chain.from_iterable(self.get_components(tiling))) + return self.__class__(gp for gp in self.gps if gp not in gps_to_remove) + + def __str__(self) -> str: if all(len(gp) == 1 for gp in self.gps): cells = ", ".join(str(gp.pos[0]) for gp in self.gps) return f"can count points in cell{'s' if len(self.gps) > 1 else ''} {cells}" @@ -131,7 +138,6 @@ class ComponentAssumption(TrackingAssumption): def __init__(self, gps: Iterable[GriddedPerm]): super().__init__(gps) assert all(len(gp) == 1 for gp in self.gps) - self.cells = frozenset(gp.pos[0] for gp in self.gps) @abc.abstractmethod def decomposition(self, perm: Perm) -> List[Perm]: @@ -202,20 +208,9 @@ def get_value(self, gp: GriddedPerm) -> int: subgp = gp.get_gridded_perm_in_cells(self.cells) return len(self.decomposition(subgp.patt)) - def __eq__(self, other) -> bool: - if isinstance(other, ComponentAssumption) and self.__class__ == other.__class__: - return bool(self.gps == other.gps) - return NotImplemented - - def __repr__(self) -> str: - return self.__class__.__name__ + f"({self.gps})" - - def __str__(self): + def __str__(self) -> str: return f"can count components in cells {self.cells}" - def __hash__(self) -> int: - return hash(self.gps) - class SumComponentAssumption(ComponentAssumption): @staticmethod @@ -234,12 +229,9 @@ def opposite_tiling_decomposition(tiling: "Tiling") -> List[List[Cell]]: def one_or_fewer_components(tiling: "Tiling", cell: Cell) -> bool: return GriddedPerm.single_cell(Perm((0, 1)), cell) in tiling.obstructions - def __str__(self): + def __str__(self) -> str: return f"can count sum components in cells {self.cells}" - def __hash__(self) -> int: - return hash(self.gps) - class SkewComponentAssumption(ComponentAssumption): @staticmethod @@ -258,8 +250,89 @@ def opposite_tiling_decomposition(tiling: "Tiling") -> List[List[Cell]]: def one_or_fewer_components(tiling: "Tiling", cell: Cell) -> bool: return GriddedPerm.single_cell(Perm((1, 0)), cell) in tiling.obstructions - def __str__(self): + def __str__(self) -> str: return f"can count skew components in cells {self.cells}" - def __hash__(self) -> int: - return hash(self.gps) + +class PredicateAssumption(Assumption): + """ + An assumption that checks some boolean holds for the sub gridded + permutation at the cells. + """ + + def satisfies(self, gp: GriddedPerm) -> bool: + """Return True if sub gp at cells satisfies the predicate.""" + return self._gp_satisfies(gp.get_gridded_perm_in_cells(self.cells)) + + @abc.abstractmethod + def _gp_satisfies(self, gp: GriddedPerm) -> bool: + """Return True if gp satisfies the predicate.""" + + @abc.abstractmethod + def can_be_satisfied(self, tiling: "Tiling") -> bool: + """ + Return True if the predicate can be satisfied by some gridded + perm on the tiling. + """ + + +class OddCountAssumption(PredicateAssumption): + """There is an odd number of points at the cells""" + + def can_be_satisfied(self, tiling: "Tiling") -> bool: + return True + + def _gp_satisfies(self, gp: GriddedPerm) -> bool: + return bool(len(gp) % 2) + + def __str__(self) -> str: + return "odd number of points in cells {self.cells}" + + +class EvenCountAssumption(PredicateAssumption): + """There is an even number of points at the cells""" + + def can_be_satisfied(self, tiling: "Tiling") -> bool: + return True + + def _gp_satisfies(self, gp: GriddedPerm) -> bool: + return not bool(len(gp) % 2) + + def __str__(self) -> str: + return "even number of points in cells {self.cells}" + + +class EqualParityAssumption(PredicateAssumption): + def can_be_satisfied(self, tiling: "Tiling") -> bool: + return True + + def satisfies(self, gp: GriddedPerm) -> bool: + return all( + idx % 2 == val % 2 + for idx, val in enumerate(gp.patt) + if gp.pos[idx] in self.cells + ) + + def _gp_satisies(self, gp: GriddedPerm) -> bool: + raise NotImplementedError + + def __str__(self) -> str: + return "points are equal parity in cells {self.cells}" + + +class OppositeParityAssumption(PredicateAssumption): + def can_be_satisfied(self, tiling: "Tiling") -> bool: + return True + + def satisfies(self, gp: GriddedPerm) -> bool: + return all( + idx % 2 != val % 2 + for idx, val in enumerate(gp.patt) + if gp.pos[idx] in self.cells + ) + + def _gp_satisies(self, gp: GriddedPerm) -> bool: + raise NotImplementedError + + def __str__(self) -> str: + return "points are opposite parity in cells {self.cells}" diff --git a/tilings/tiling.py b/tilings/tiling.py index bccd36a3..b2d39231 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -46,7 +46,13 @@ guess_obstructions, ) from .assumptions import ( + Assumption, ComponentAssumption, + EqualParityAssumption, + EvenCountAssumption, + OddCountAssumption, + OppositeParityAssumption, + PredicateAssumption, SkewComponentAssumption, SumComponentAssumption, TrackingAssumption, @@ -82,6 +88,16 @@ total=False, ) +Assumptions = [ + TrackingAssumption, + SumComponentAssumption, + SkewComponentAssumption, + EvenCountAssumption, + OddCountAssumption, + EqualParityAssumption, + OppositeParityAssumption, +] + class Tiling(CombinatorialClass): """Tiling class. @@ -97,7 +113,7 @@ def __init__( self, obstructions: Iterable[GriddedPerm] = tuple(), requirements: Iterable[Iterable[GriddedPerm]] = tuple(), - assumptions: Iterable[TrackingAssumption] = tuple(), + assumptions: Iterable[Assumption] = tuple(), remove_empty_rows_and_cols: bool = True, derive_empty: bool = True, simplify: bool = True, @@ -420,14 +436,11 @@ def split_16bit(n) -> Tuple[int, int]: if self.assumptions: result.extend(split_16bit(len(self.assumptions))) for assumption in self.assumptions: - if isinstance(assumption, SkewComponentAssumption): - result.append(2) - elif isinstance(assumption, SumComponentAssumption): - result.append(1) - elif isinstance(assumption, TrackingAssumption): - result.append(0) - else: - raise ValueError("Not a valid assumption.") + try: + ass_idx = Assumptions.index(type(assumption)) + except ValueError as e: + raise ValueError("Not a valid assumption.") from e + result.append(ass_idx) result.extend(split_16bit(len(assumption.gps))) result.extend( chain.from_iterable( @@ -484,17 +497,11 @@ def recreate_gp_list(offset): assumption_type = arr[offset] offset += 1 gps, offset = recreate_gp_list(offset) - if assumption_type == 0: - # tracking - assumptions.append(TrackingAssumption(gps)) - elif assumption_type == 1: - # sum - assumptions.append(SumComponentAssumption(gps)) - elif assumption_type == 2: - # skew - assumptions.append(SkewComponentAssumption(gps)) - else: - raise ValueError("Invalid assumption type.") + try: + ass_class = Assumptions[assumption_type] + except IndexError as e: + raise IndexError("Invalid assumption type.") from e + assumptions.append(ass_class(gps)) return cls( obstructions=obstructions, requirements=requirements, @@ -541,7 +548,7 @@ def from_dict(cls, d: dict) -> "Tiling": serialized Tiling object.""" obstructions = map(GriddedPerm.from_dict, d["obstructions"]) requirements = map(lambda x: map(GriddedPerm.from_dict, x), d["requirements"]) - assumptions = map(TrackingAssumption.from_dict, d.get("assumptions", [])) + assumptions = map(Assumption.from_dict, d.get("assumptions", [])) return cls( obstructions=obstructions, requirements=requirements, @@ -642,11 +649,11 @@ def remove_requirement(self, requirement: Tuple[GriddedPerm, ...]) -> "Tiling": sorted_input=True, ) - def add_assumption(self, assumption: TrackingAssumption) -> "Tiling": + def add_assumption(self, assumption: Assumption) -> "Tiling": """Returns a new tiling with the added assumption.""" return self.add_assumptions((assumption,)) - def add_assumptions(self, assumptions: Iterable[TrackingAssumption]) -> "Tiling": + def add_assumptions(self, assumptions: Iterable[Assumption]) -> "Tiling": """Returns a new tiling with the added assumptions.""" tiling = Tiling( self._obstructions, @@ -700,7 +707,10 @@ def remove_components_from_assumptions(self): """ if not self.assumptions: return self - assumptions = [ass.remove_components(self) for ass in self.assumptions] + assumptions = [ + ass.remove_components(self) if isinstance(ass, TrackingAssumption) else ass + for ass in self.assumptions + ] tiling = self.__class__( self._obstructions, self._requirements, @@ -1390,21 +1400,23 @@ def to_html_representation(self) -> str: @property def extra_parameters(self) -> Tuple[str, ...]: - return tuple(f"k_{i}" for i in range(len(self._assumptions))) + return tuple(f"k_{i}" for i in range(len(self.tracking_assumptions))) def get_parameters(self, obj: GriddedPerm) -> Parameters: - return tuple(ass.get_value(obj) for ass in self.assumptions) + return tuple(ass.get_value(obj) for ass in self.tracking_assumptions) def possible_parameters(self, n: int) -> Iterator[Dict[str, int]]: if any( len(gp) > 1 - for gp in chain.from_iterable(ass.gps for ass in self.assumptions) + for gp in chain.from_iterable(ass.gps for ass in self.tracking_assumptions) ): raise NotImplementedError( "possible parameters only implemented for assumptions with " "size one gridded perms" ) - parameters = [self.get_assumption_parameter(ass) for ass in self.assumptions] + parameters = [ + self.get_assumption_parameter(ass) for ass in self.tracking_assumptions + ] for values in product(*[range(n + 1) for _ in parameters]): yield dict(zip(parameters, values)) @@ -1415,7 +1427,7 @@ def get_assumption_parameter(self, assumption: TrackingAssumption) -> str: Raise ValueError if the assumptions is not on the tiling. """ try: - idx = self._assumptions.index(assumption) + idx = self.tracking_assumptions.index(assumption) except ValueError as e: raise ValueError( f"following assumption not on tiling: '{assumption}'" @@ -1424,7 +1436,7 @@ def get_assumption_parameter(self, assumption: TrackingAssumption) -> str: def get_assumption(self, parameter: str) -> TrackingAssumption: idx = parameter.split("_")[1] - return self.assumptions[int(idx)] + return self.tracking_assumptions[int(idx)] def get_minimum_value(self, parameter: str) -> int: """ @@ -1442,6 +1454,7 @@ def get_minimum_value(self, parameter: str) -> int: def maximum_length_of_minimum_gridded_perm(self) -> int: """Returns the maximum length of the minimum gridded permutation that can be gridded on the tiling. + TODO: this method ignores predicates so is a lower bound """ return sum(max(map(len, reqs)) for reqs in self.requirements) @@ -1451,8 +1464,12 @@ def is_empty(self) -> bool: Tiling is empty if it has been inferred to be contradictory due to contradicting requirements and obstructions or no gridded permutation can be gridded on the tiling. + + TODO: this method ignores predicates """ - if any(ob.is_empty() for ob in self.obstructions): + if any(ob.is_empty() for ob in self.obstructions) or any( + not ass.can_be_satisfied(self) for ass in self.predicate_assumptions + ): return True if len(self.requirements) <= 1: return False @@ -1544,7 +1561,12 @@ def gridded_perms(self, maxlen: Optional[int] = None) -> Iterator[GriddedPerm]: if maxlen is not None else self.maximum_length_of_minimum_gridded_perm() ) - yield from GriddedPermsOnTiling(self).gridded_perms(maxlen) + yield from filter( + self._satisfies_predicates, GriddedPermsOnTiling(self).gridded_perms(maxlen) + ) + + def _satisfies_predicates(self, gp: GriddedPerm) -> bool: + return all(ass.satisfies(gp) for ass in self.predicate_assumptions) def enmerate_gp_up_to(self, max_length: int) -> List[int]: """Count gridded perms of each length up to a max length.""" @@ -1565,6 +1587,7 @@ def merge(self) -> "Tiling": def minimal_gridded_perms(self) -> Iterator[GriddedPerm]: """ An iterator over all minimal gridded permutations. + TODO: this method ignores predicates """ MGP = MinimalGriddedPerms(self.obstructions, self.requirements) yield from MGP.minimal_gridded_perms() @@ -1597,7 +1620,10 @@ def is_atom(self) -> bool: ) def minimum_size_of_object(self) -> int: - """Return the size of the smallest gridded perm contained on the tiling.""" + """ + Return the size of the smallest gridded perm contained on the tiling. + TODO: this ignores predicates + """ if not self.requirements: return 0 if len(self.requirements) == 1: @@ -1730,9 +1756,21 @@ def total_requirements(self) -> int: return len(self._requirements) @property - def assumptions(self) -> Tuple[TrackingAssumption, ...]: + def assumptions(self) -> Tuple[Assumption, ...]: return self._assumptions + @property + def tracking_assumptions(self) -> Tuple[TrackingAssumption, ...]: + return tuple( + ass for ass in self._assumptions if isinstance(ass, TrackingAssumption) + ) + + @property + def predicate_assumptions(self) -> Tuple[PredicateAssumption, ...]: + return tuple( + ass for ass in self._assumptions if isinstance(ass, PredicateAssumption) + ) + def total_assumptions(self) -> int: return len(self._assumptions) From 2ea58d33370803767185ccd3a5623b0f38efe2b9 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Tue, 19 Jul 2022 16:52:26 +0000 Subject: [PATCH 02/48] update strategies (except fusion and factor) with predicates --- tilings/algorithms/map.py | 4 +-- tilings/algorithms/requirement_placement.py | 8 +++--- tilings/algorithms/sliding.py | 6 ++++- tilings/assumptions.py | 14 +++++++---- tilings/bijections.py | 13 +++++++--- tilings/strategies/assumption_insertion.py | 17 +++++++------ tilings/strategies/assumption_splitting.py | 12 ++++++--- tilings/strategies/cell_reduction.py | 2 ++ tilings/strategies/deflation.py | 2 ++ tilings/strategies/detect_components.py | 6 ++--- tilings/strategies/monotone_sliding.py | 4 ++- tilings/strategies/obstruction_inferral.py | 2 +- tilings/strategies/point_jumping.py | 11 ++++++--- tilings/strategies/pointing.py | 11 ++++++--- tilings/strategies/rearrange_assumption.py | 21 ++++++++++------ tilings/strategies/requirement_insertion.py | 2 +- tilings/strategies/requirement_placement.py | 6 +++-- tilings/strategies/row_and_col_separation.py | 7 +++--- tilings/strategies/sliding.py | 4 ++- tilings/strategies/symmetry.py | 26 ++++++++++++-------- tilings/strategies/unfusion.py | 2 +- tilings/strategies/verification.py | 16 ++++++------ tilings/tiling.py | 10 ++++---- 23 files changed, 130 insertions(+), 76 deletions(-) diff --git a/tilings/algorithms/map.py b/tilings/algorithms/map.py index feaf2d21..a8d63a7e 100644 --- a/tilings/algorithms/map.py +++ b/tilings/algorithms/map.py @@ -3,7 +3,7 @@ from tilings.exception import InvalidOperationError if TYPE_CHECKING: - from tilings.assumptions import TrackingAssumption + from tilings.assumptions import AssumptionClass from tilings.griddedperm import GriddedPerm Cell = Tuple[int, int] @@ -70,7 +70,7 @@ def map_gp(self, gp: "GriddedPerm") -> "GriddedPerm": """ return gp.__class__(gp.patt, map(self.map_cell, gp.pos)) - def map_assumption(self, assumption: "TrackingAssumption") -> "TrackingAssumption": + def map_assumption(self, assumption: "AssumptionClass") -> "AssumptionClass": """ Map the assumption according to the map. diff --git a/tilings/algorithms/requirement_placement.py b/tilings/algorithms/requirement_placement.py index 458e0625..7e97c6e3 100644 --- a/tilings/algorithms/requirement_placement.py +++ b/tilings/algorithms/requirement_placement.py @@ -3,7 +3,7 @@ from permuta.misc import DIR_EAST, DIR_NONE, DIR_NORTH, DIR_SOUTH, DIR_WEST, DIRS from tilings import GriddedPerm -from tilings.assumptions import TrackingAssumption +from tilings.assumptions import Assumption if TYPE_CHECKING: from tilings import Tiling @@ -13,7 +13,7 @@ ListRequirement = List[GriddedPerm] ObsCache = Dict[Cell, List[GriddedPerm]] ReqsCache = Dict[Cell, List[ListRequirement]] -AssCache = Dict[Cell, List[TrackingAssumption]] +AssCache = Dict[Cell, List[Assumption]] class RequirementPlacement: @@ -244,7 +244,7 @@ def stretched_requirements(self, cell: Cell) -> List[ListRequirement]: ] return self._stretched_requirements_cache[cell] - def stretched_assumptions(self, cell: Cell) -> List[TrackingAssumption]: + def stretched_assumptions(self, cell: Cell) -> List[Assumption]: """ Return all of the stretched assumptions that are created if placing a point in the given cell. @@ -258,7 +258,7 @@ def stretched_assumptions(self, cell: Cell) -> List[TrackingAssumption]: def _stretched_obstructions_requirements_and_assumptions( self, cell: Cell - ) -> Tuple[List[GriddedPerm], List[ListRequirement], List[TrackingAssumption]]: + ) -> Tuple[List[GriddedPerm], List[ListRequirement], List[Assumption]]: """ Return all of the stretched obstruction and requirements assuming that a point is placed in cell. diff --git a/tilings/algorithms/sliding.py b/tilings/algorithms/sliding.py index 2780e652..fcbdb8e5 100644 --- a/tilings/algorithms/sliding.py +++ b/tilings/algorithms/sliding.py @@ -13,7 +13,8 @@ Tuple, ) -from tilings import GriddedPerm, TrackingAssumption +from tilings import GriddedPerm +from tilings.assumptions import TrackingAssumption if TYPE_CHECKING: # pylint: disable=cyclic-import @@ -34,6 +35,8 @@ def __eq__(self, other: object) -> bool: def slidable_pairs(self) -> Iterable[Tuple[int, int]]: """Yield the column pairs possible to slide.""" + if self.tiling.predicate_assumptions: + raise NotImplementedError("Not implemented sliding for predicates") for av_12, av_123 in product(*self._fast_filter()): if self._slide_check_for_pair(av_12, av_123): yield av_12, av_123 @@ -384,6 +387,7 @@ def _av12_one_point( def _swap_assumptions(self, c1: int, c2: int) -> Iterable[TrackingAssumption]: for assumption in self.tiling.assumptions: + assert isinstance(assumption, TrackingAssumption) assert all(len(gp) == 1 for gp in assumption.gps) yield Sliding.slide_assumption(assumption, c1, c2) diff --git a/tilings/assumptions.py b/tilings/assumptions.py index eed5d58e..6f4b3f33 100644 --- a/tilings/assumptions.py +++ b/tilings/assumptions.py @@ -1,7 +1,7 @@ import abc from importlib import import_module from itertools import chain -from typing import TYPE_CHECKING, Iterable, List, Optional, Tuple, Type +from typing import TYPE_CHECKING, Iterable, List, Optional, Tuple, Type, TypeVar from permuta import Perm @@ -12,6 +12,8 @@ if TYPE_CHECKING: from tilings import Tiling +AssumptionClass = TypeVar("AssumptionClass", bound="Assumption") + class Assumption: """ @@ -25,15 +27,17 @@ def __init__(self, gps: Iterable[GriddedPerm]): self.cells = frozenset(gp.pos[0] for gp in self.gps) @classmethod - def from_cells(cls, cells: Iterable[Cell]) -> "Assumption": + def from_cells( + cls: Type[AssumptionClass], cells: Iterable[Cell] + ) -> AssumptionClass: gps = [GriddedPerm.single_cell((0,), cell) for cell in cells] return cls(gps) def avoiding( - self, + self: AssumptionClass, obstructions: Iterable[GriddedPerm], active_cells: Optional[Iterable[Cell]] = None, - ) -> "Assumption": + ) -> AssumptionClass: """ Return the tracking absumption where all of the gridded perms avoiding the obstructions are removed. If active_cells is not None, then any @@ -61,7 +65,7 @@ def to_jsonable(self) -> dict: } @classmethod - def from_dict(cls, d: dict) -> "TrackingAssumption": + def from_dict(cls, d: dict) -> "Assumption": """Return the assumption from the json dict representation.""" module = import_module(d["class_module"]) AssClass: Type["TrackingAssumption"] = getattr(module, d["assumption"]) diff --git a/tilings/bijections.py b/tilings/bijections.py index 81f08574..b59387ca 100644 --- a/tilings/bijections.py +++ b/tilings/bijections.py @@ -78,13 +78,18 @@ def __init__( self.assumptions1, self.assumptions2 = self._init_assumptions() def _init_assumptions(self) -> Tuple[AssumptionLabels, AssumptionLabels]: + if ( + self.r1.comb_class.predicate_assumptions + or self.r2.comb_class.predicate_assumptions + ): + raise NotImplementedError("not implemented bijections for predicates") a1: AssumptionLabels = {} a2: AssumptionLabels = {} # If any label at root, we store them at the first label if self.r1.comb_class.assumptions: - a1[self.nxt_label] = set(self.r1.comb_class.assumptions) + a1[self.nxt_label] = set(self.r1.comb_class.tracking_assumptions) if self.r2.comb_class.assumptions: - a2[self.nxt_label] = set(self.r2.comb_class.assumptions) + a2[self.nxt_label] = set(self.r2.comb_class.tracking_assumptions) # Increment next label if root had any assumptions self.nxt_label = max(len(a1), len(a2)) return a1, a2 @@ -171,9 +176,11 @@ def _find_new_assumptions( assumptions: AssumptionLabels, ) -> Set[TrackingAssumption]: """The assumption in the current class that don't correspond to any label.""" + if rule.comb_class.predicate_assumptions: + raise NotImplementedError("Not implemented bijections for predicates") return set( assumption - for assumption in rule.comb_class.assumptions + for assumption in rule.comb_class.tracking_assumptions if all(assumption not in v for v in assumptions.values()) ) diff --git a/tilings/strategies/assumption_insertion.py b/tilings/strategies/assumption_insertion.py index 1274066e..d48e9ab7 100644 --- a/tilings/strategies/assumption_insertion.py +++ b/tilings/strategies/assumption_insertion.py @@ -1,7 +1,7 @@ from collections import Counter from itertools import product from random import randint -from typing import Callable, Dict, Iterable, Iterator, List, Optional, Tuple +from typing import Callable, Dict, Iterable, Iterator, List, Optional, Tuple, cast from sympy import Eq, Expr, Function, Number, Symbol, var @@ -19,7 +19,7 @@ Terms, ) from tilings import GriddedPerm, Tiling -from tilings.assumptions import ComponentAssumption, TrackingAssumption +from tilings.assumptions import Assumption, ComponentAssumption, TrackingAssumption Cell = Tuple[int, int] @@ -257,7 +257,7 @@ def constructor( if children is None: children = self.decomposition_function(comb_class) if children is None: - raise StrategyDoesNotApply("Can't split the tracking assumption") + raise StrategyDoesNotApply("Can't add the tracking assumption") new_parameters = [ children[0].get_assumption_parameter(ass) for ass in self.assumptions ] @@ -286,7 +286,7 @@ def reverse_constructor( child.get_assumption_parameter(ass): comb_class.get_assumption_parameter( ass ) - for ass in child.assumptions + for ass in child.tracking_assumptions if ass != assumption } @@ -305,7 +305,7 @@ def extra_parameters( comb_class.get_assumption_parameter( ass ): child.get_assumption_parameter(ass) - for ass in comb_class.assumptions + for ass in comb_class.tracking_assumptions }, ) @@ -354,7 +354,10 @@ def to_jsonable(self) -> dict: @classmethod def from_dict(cls, d: dict) -> "AddAssumptionsStrategy": - assumptions = [TrackingAssumption.from_dict(ass) for ass in d["assumptions"]] + assumptions = [ + cast(TrackingAssumption, Assumption.from_dict(ass)) + for ass in d["assumptions"] + ] return cls(assumptions) @staticmethod @@ -370,7 +373,7 @@ def __repr__(self): class AddAssumptionFactory(StrategyFactory[Tiling]): def __call__(self, comb_class: Tiling) -> Iterator[Rule]: - for assumption in comb_class.assumptions: + for assumption in comb_class.tracking_assumptions: without = comb_class.remove_assumption(assumption) strategy = AddAssumptionsStrategy((assumption,)) yield strategy(without) diff --git a/tilings/strategies/assumption_splitting.py b/tilings/strategies/assumption_splitting.py index d45ba87c..e657a0d5 100644 --- a/tilings/strategies/assumption_splitting.py +++ b/tilings/strategies/assumption_splitting.py @@ -21,6 +21,7 @@ from tilings import GriddedPerm, Tiling from tilings.algorithms import factor from tilings.assumptions import ( + Assumption, SkewComponentAssumption, SumComponentAssumption, TrackingAssumption, @@ -178,14 +179,17 @@ def shifts( return (0,) def decomposition_function(self, comb_class: Tiling) -> Optional[Tuple[Tiling]]: - if not comb_class.assumptions: + if not comb_class.tracking_assumptions: return None components = self.factor_class(comb_class.remove_assumptions()).get_components() if len(components) == 1: return None - new_assumptions: List[TrackingAssumption] = [] + new_assumptions: List[Assumption] = [] for ass in comb_class.assumptions: - new_assumptions.extend(self._split_assumption(ass, components)) + if not isinstance(ass, TrackingAssumption): + new_assumptions.append(ass) + else: + new_assumptions.extend(self._split_assumption(ass, components)) new_tiling = Tiling( comb_class.obstructions, comb_class.requirements, @@ -297,7 +301,7 @@ def constructor( child = children[0] split_parameters: Dict[str, Tuple[str, ...]] = {"n": ("n",)} components = self.factor_class(comb_class.remove_assumptions()).get_components() - for idx, assumption in enumerate(comb_class.assumptions): + for idx, assumption in enumerate(comb_class.tracking_assumptions): split_assumptions = self._split_assumption(assumption, components) child_vars = tuple( sorted(f"k_{child.assumptions.index(ass)}" for ass in split_assumptions) diff --git a/tilings/strategies/cell_reduction.py b/tilings/strategies/cell_reduction.py index 899729f2..843d0331 100644 --- a/tilings/strategies/cell_reduction.py +++ b/tilings/strategies/cell_reduction.py @@ -236,6 +236,8 @@ def __init__(self, tracked: bool): def __call__(self, comb_class: Tiling) -> Iterator[CellReductionStrategy]: if comb_class.dimensions == (1, 1): return + if comb_class.predicate_assumptions: + raise NotImplementedError("Not implemented cell reduction for predicates") cell_bases = comb_class.cell_basis() for cell in self.reducible_cells(comb_class): if not ( # a finite cell diff --git a/tilings/strategies/deflation.py b/tilings/strategies/deflation.py index 458ff911..6c21d30e 100644 --- a/tilings/strategies/deflation.py +++ b/tilings/strategies/deflation.py @@ -227,6 +227,8 @@ def __init__(self, tracked: bool): super().__init__() def __call__(self, comb_class: Tiling) -> Iterator[DeflationStrategy]: + if comb_class.predicate_assumptions: + raise NotImplementedError("Not implemented deflation for predicates") for cell in comb_class.active_cells: if not self._can_deflate_requirements_and_assumptions(comb_class, cell): continue diff --git a/tilings/strategies/detect_components.py b/tilings/strategies/detect_components.py index 10f023ee..af6048dc 100644 --- a/tilings/strategies/detect_components.py +++ b/tilings/strategies/detect_components.py @@ -122,7 +122,7 @@ def shifts( @staticmethod def decomposition_function(comb_class: Tiling) -> Optional[Tuple[Tiling]]: - if not comb_class.assumptions: + if not comb_class.tracking_assumptions: return None return (comb_class.remove_components_from_assumptions(),) @@ -135,7 +135,7 @@ def constructor( raise StrategyDoesNotApply("Can't detect components") removed_components: Dict[str, int] = {} - for ass in comb_class.assumptions: + for ass in comb_class.tracking_assumptions: value = len(ass.get_components(comb_class)) if value: k = comb_class.get_assumption_parameter(ass) @@ -164,7 +164,7 @@ def extra_parameters( raise StrategyDoesNotApply("Strategy does not apply") extra_parameters: Dict[str, str] = {} child = children[0] - for assumption in comb_class.assumptions: + for assumption in comb_class.tracking_assumptions: mapped_assumption = assumption.remove_components(comb_class) if mapped_assumption.gps: extra_parameters[ diff --git a/tilings/strategies/monotone_sliding.py b/tilings/strategies/monotone_sliding.py index c256d556..1a1f034b 100644 --- a/tilings/strategies/monotone_sliding.py +++ b/tilings/strategies/monotone_sliding.py @@ -67,7 +67,7 @@ def extra_parameters( ): child.get_assumption_parameter( ass.__class__(self.slide_gps(ass.gps)) ) - for ass in comb_class.assumptions + for ass in comb_class.tracking_assumptions }, ) @@ -108,6 +108,8 @@ class MonotoneSlidingFactory(StrategyFactory[Tiling]): """ def __call__(self, comb_class: Tiling) -> Iterator[GeneralizedSlidingStrategy]: + if comb_class.predicate_assumptions: + raise NotImplementedError("Not implemented sliding for predicates") rotate = False if ( not comb_class.dimensions[1] == 1 diff --git a/tilings/strategies/obstruction_inferral.py b/tilings/strategies/obstruction_inferral.py index a0704f89..491a1b18 100644 --- a/tilings/strategies/obstruction_inferral.py +++ b/tilings/strategies/obstruction_inferral.py @@ -45,7 +45,7 @@ def extra_parameters( raise StrategyDoesNotApply("Strategy does not apply") child = children[0] params: Dict[str, str] = {} - for assumption in comb_class.assumptions: + for assumption in comb_class.tracking_assumptions: mapped_assumption = child.forward_map.map_assumption(assumption).avoiding( child.obstructions ) diff --git a/tilings/strategies/point_jumping.py b/tilings/strategies/point_jumping.py index 6869944a..5dabc4d5 100644 --- a/tilings/strategies/point_jumping.py +++ b/tilings/strategies/point_jumping.py @@ -1,6 +1,6 @@ import abc from itertools import chain -from typing import Dict, Iterator, Optional, Tuple +from typing import Dict, Iterator, Optional, Tuple, cast from comb_spec_searcher import Constructor from comb_spec_searcher.exception import StrategyDoesNotApply @@ -39,7 +39,8 @@ def swapped_requirements( def swapped_assumptions(self, tiling: Tiling) -> Tuple[TrackingAssumption, ...]: return tuple( - ass.__class__(map(self._swapped_gp, ass.gps)) for ass in tiling.assumptions + cast(TrackingAssumption, ass.__class__(map(self._swapped_gp, ass.gps))) + for ass in tiling.assumptions ) def _swapped_gp(self, gp: GriddedPerm) -> GriddedPerm: @@ -164,7 +165,7 @@ def extra_parameters( comb_class.get_assumption_parameter( ass ): child.get_assumption_parameter(self._swap_assumption(ass)) - for ass in comb_class.assumptions + for ass in comb_class.tracking_assumptions }, ) @@ -342,6 +343,10 @@ class AssumptionAndPointJumpingFactory(StrategyFactory[Tiling]): def __call__( self, comb_class: Tiling ) -> Iterator[AssumptionOrPointJumpingStrategy]: + if comb_class.predicate_assumptions: + raise NotImplementedError( + "not implemented jumping strategies for predicates" + ) cols, rows = comb_class.dimensions gps_to_be_swapped = chain( *comb_class.requirements, *[ass.gps for ass in comb_class.assumptions] diff --git a/tilings/strategies/pointing.py b/tilings/strategies/pointing.py index c9f60a29..e6354242 100644 --- a/tilings/strategies/pointing.py +++ b/tilings/strategies/pointing.py @@ -25,7 +25,7 @@ from permuta.misc import DIR_NONE from tilings import GriddedPerm, Tiling from tilings.algorithms import RequirementPlacement -from tilings.assumptions import ComponentAssumption, TrackingAssumption +from tilings.assumptions import Assumption, ComponentAssumption, TrackingAssumption from tilings.strategies.assumption_insertion import AddAssumptionsStrategy from tilings.strategies.obstruction_inferral import ObstructionInferralStrategy from tilings.tiling import Cell @@ -155,8 +155,11 @@ def extra_parameters( mapped_assumptions = [ child.forward_map.map_assumption(ass).avoiding(child.obstructions) for ass in algo.stretched_assumptions(cell) + if isinstance(ass, TrackingAssumption) ] - for ass, mapped_ass in zip(comb_class.assumptions, mapped_assumptions): + for ass, mapped_ass in zip( + comb_class.tracking_assumptions, mapped_assumptions + ): if mapped_ass.gps: params[ comb_class.get_assumption_parameter(ass) @@ -352,7 +355,7 @@ def to_jsonable(self) -> dict: def from_dict(cls, d: dict) -> "AssumptionPointingStrategy": if "max_cells" in d: d.pop("max_cells") - assumption = TrackingAssumption.from_dict(d.pop("assumption")) + assumption = cast(TrackingAssumption, Assumption.from_dict(d.pop("assumption"))) return cls(assumption=assumption, **d) def __repr__(self) -> str: @@ -370,7 +373,7 @@ def __init__(self, max_cells: int = 4) -> None: def __call__(self, comb_class: Tiling) -> Iterator[AssumptionPointingStrategy]: if len(comb_class.active_cells) <= self.max_cells: - for assumption in comb_class.assumptions: + for assumption in comb_class.tracking_assumptions: if not isinstance(assumption, ComponentAssumption): yield AssumptionPointingStrategy(assumption) diff --git a/tilings/strategies/rearrange_assumption.py b/tilings/strategies/rearrange_assumption.py index 6cb9969b..85054601 100644 --- a/tilings/strategies/rearrange_assumption.py +++ b/tilings/strategies/rearrange_assumption.py @@ -1,7 +1,7 @@ from collections import Counter from functools import partial from itertools import combinations -from typing import Callable, Dict, Iterator, List, Optional, Tuple, Union +from typing import Callable, Dict, Iterator, List, Optional, Tuple, Union, cast import sympy @@ -24,6 +24,7 @@ ) from tilings import GriddedPerm, Tiling from tilings.assumptions import ( + Assumption, ComponentAssumption, SkewComponentAssumption, SumComponentAssumption, @@ -353,11 +354,13 @@ def extra_parameters( res: Dict[str, str] = {} child = children[0] for parent_ass, parent_param in zip( - comb_class.assumptions, comb_class.extra_parameters + comb_class.tracking_assumptions, comb_class.extra_parameters ): if parent_ass == self.assumption: continue - child_param = child.extra_parameters[child.assumptions.index(parent_ass)] + child_param = child.extra_parameters[ + child.tracking_assumptions.index(parent_ass) + ] res[parent_param] = child_param return (res,) @@ -410,8 +413,10 @@ def __repr__(self) -> str: @classmethod def from_dict(cls, d: dict) -> "RearrangeAssumptionStrategy": - assumption = TrackingAssumption.from_dict(d.pop("assumption")) - sub_assumption = TrackingAssumption.from_dict(d.pop("sub_assumption")) + assumption = cast(TrackingAssumption, Assumption.from_dict(d.pop("assumption"))) + sub_assumption = cast( + TrackingAssumption, Assumption.from_dict(d.pop("sub_assumption")) + ) assert not d return cls(assumption, sub_assumption) @@ -485,7 +490,7 @@ def extra_parameters( ): child.get_assumption_parameter( self.new_assumption if ass == self.assumption else ass ) - for ass in comb_class.assumptions + for ass in comb_class.tracking_assumptions }, ) @@ -501,7 +506,7 @@ def to_jsonable(self) -> dict: @classmethod def from_dict(cls, d: dict) -> "ComponentToPointAssumptionStrategy": return cls( - assumption=TrackingAssumption.from_dict(d["assumption"]), + assumption=cast(TrackingAssumption, Assumption.from_dict(d["assumption"])), ignore_parent=d["ignore_parent"], workable=d["workable"], ) @@ -515,7 +520,7 @@ def __call__( ]: points: List[TrackingAssumption] = [] components: List[TrackingAssumption] = [] - for ass in comb_class.assumptions: + for ass in comb_class.tracking_assumptions: (points, components)[isinstance(ass, ComponentAssumption)].append(ass) for ass1, ass2 in combinations(points, 2): diff --git a/tilings/strategies/requirement_insertion.py b/tilings/strategies/requirement_insertion.py index 82e5b29b..31c1bd19 100644 --- a/tilings/strategies/requirement_insertion.py +++ b/tilings/strategies/requirement_insertion.py @@ -90,7 +90,7 @@ def extra_parameters( av, co = children av_params: Dict[str, str] = {} co_params: Dict[str, str] = {} - for assumption in comb_class.assumptions: + for assumption in comb_class.tracking_assumptions: parent_var = comb_class.get_assumption_parameter(assumption) av_mapped_assumption = av.forward_map.map_assumption(assumption).avoiding( av.obstructions diff --git a/tilings/strategies/requirement_placement.py b/tilings/strategies/requirement_placement.py index 27a2aff7..67d80ff6 100644 --- a/tilings/strategies/requirement_placement.py +++ b/tilings/strategies/requirement_placement.py @@ -11,6 +11,7 @@ from tilings import GriddedPerm, Tiling from tilings.algorithms import RequirementPlacement from tilings.algorithms.fusion import Fusion +from tilings.assumptions import TrackingAssumption __all__ = [ "PatternPlacementFactory", @@ -91,7 +92,7 @@ def extra_parameters( extra_parameters: Tuple[Dict[str, str], ...] = tuple({} for _ in children) if self.include_empty: child = children[0] - for assumption in comb_class.assumptions: + for assumption in comb_class.tracking_assumptions: mapped_assumption = child.forward_map.map_assumption( assumption ).avoiding(child.obstructions) @@ -105,9 +106,10 @@ def extra_parameters( mapped_assumptions = [ child.forward_map.map_assumption(ass).avoiding(child.obstructions) for ass in algo.stretched_assumptions(cell) + if isinstance(ass, TrackingAssumption) ] for assumption, mapped_assumption in zip( - comb_class.assumptions, mapped_assumptions + comb_class.tracking_assumptions, mapped_assumptions ): if mapped_assumption.gps: parent_var = comb_class.get_assumption_parameter(assumption) diff --git a/tilings/strategies/row_and_col_separation.py b/tilings/strategies/row_and_col_separation.py index 36a6b719..fcec91cd 100644 --- a/tilings/strategies/row_and_col_separation.py +++ b/tilings/strategies/row_and_col_separation.py @@ -8,6 +8,7 @@ from comb_spec_searcher.exception import StrategyDoesNotApply from tilings import GriddedPerm, Tiling from tilings.algorithms import RowColSeparation +from tilings.assumptions import TrackingAssumption __all__ = ["RowColumnSeparationStrategy"] @@ -60,7 +61,7 @@ def extra_parameters( if children is None: raise StrategyDoesNotApply("Strategy does not apply") child = children[0] - mapped_assumptions = tuple( + mapped_assumptions: Tuple[TrackingAssumption, ...] = tuple( ass.__class__( tuple( self.forward_map(comb_class, gp, children)[0] @@ -68,7 +69,7 @@ def extra_parameters( if all(cell in self.forward_cell_map(comb_class) for cell in gp.pos) ) ).avoiding(child.obstructions) - for ass in comb_class.assumptions + for ass in comb_class.tracking_assumptions ) return ( { @@ -76,7 +77,7 @@ def extra_parameters( assumption ): child.get_assumption_parameter(mapped_assumption) for assumption, mapped_assumption in zip( - comb_class.assumptions, mapped_assumptions + comb_class.tracking_assumptions, mapped_assumptions ) if mapped_assumption.gps }, diff --git a/tilings/strategies/sliding.py b/tilings/strategies/sliding.py index 40a9c840..6728d17e 100644 --- a/tilings/strategies/sliding.py +++ b/tilings/strategies/sliding.py @@ -211,7 +211,7 @@ def extra_parameters( ass, self.av_12, self.av_123, maps.g_map, maps.g_inv ) ) - for ass in comb_class.assumptions + for ass in comb_class.tracking_assumptions }, ) @@ -262,6 +262,8 @@ def __init__(self, use_symmetries: bool = False): self.use_symmetries = use_symmetries def __call__(self, comb_class: Tiling) -> Iterator[Rule]: + if comb_class.predicate_assumptions: + raise NotImplementedError("Not implemented sliding for predicates") if comb_class.dimensions[0] > 1 and comb_class.dimensions[1] == 1: sliding = Sliding(comb_class) for pair in sliding.slidable_pairs(): diff --git a/tilings/strategies/symmetry.py b/tilings/strategies/symmetry.py index 2fa88e68..9a9e6ef3 100644 --- a/tilings/strategies/symmetry.py +++ b/tilings/strategies/symmetry.py @@ -8,6 +8,7 @@ from permuta import Perm from tilings import GriddedPerm, Tiling from tilings.assumptions import ( + Assumption, ComponentAssumption, SkewComponentAssumption, SumComponentAssumption, @@ -28,14 +29,14 @@ def inverse_gp_transform(self, tiling: Tiling, gp: GriddedPerm) -> GriddedPerm: @staticmethod def assumption_type_transform( - assumption: TrackingAssumption, - ) -> Type[TrackingAssumption]: + assumption: Assumption, + ) -> Type[Assumption]: pass @staticmethod def _assumption_type_swap( - assumption: TrackingAssumption, - ) -> Type[TrackingAssumption]: + assumption: Assumption, + ) -> Type[Assumption]: if isinstance(assumption, ComponentAssumption): if isinstance(assumption, SumComponentAssumption): return SkewComponentAssumption @@ -44,8 +45,8 @@ def _assumption_type_swap( @staticmethod def _assumption_type_identity( - assumption: TrackingAssumption, - ) -> Type[TrackingAssumption]: + assumption: Assumption, + ) -> Type[Assumption]: return assumption.__class__ def decomposition_function(self, comb_class: Tiling) -> Tuple[Tiling, ...]: @@ -81,10 +82,13 @@ def extra_parameters( raise StrategyDoesNotApply("Strategy does not apply") child = children[0] mapped_assumptions = tuple( - self.__class__.assumption_type_transform(ass)( - tuple(self.gp_transform(comb_class, gp) for gp in ass.gps) + cast( + TrackingAssumption, + self.__class__.assumption_type_transform(ass)( + tuple(self.gp_transform(comb_class, gp) for gp in ass.gps) + ), ) - for ass in comb_class.assumptions + for ass in comb_class.tracking_assumptions ) return ( { @@ -92,7 +96,7 @@ def extra_parameters( assumption ): child.get_assumption_parameter(mapped_assumption) for assumption, mapped_assumption in zip( - comb_class.assumptions, mapped_assumptions + comb_class.tracking_assumptions, mapped_assumptions ) }, ) @@ -343,6 +347,8 @@ def __init__( super().__init__() def __call__(self, tiling: Tiling) -> Iterator[TilingSymmetryStrategy]: + if tiling.predicate_assumptions: + raise NotImplementedError("Not implemented symmetries for predicates") underlying_patts = set(gp.patt for gp in tiling.obstructions) if ( self._basis is None diff --git a/tilings/strategies/unfusion.py b/tilings/strategies/unfusion.py index 041c1ea7..a9ac38f3 100644 --- a/tilings/strategies/unfusion.py +++ b/tilings/strategies/unfusion.py @@ -270,7 +270,7 @@ def extra_parameters( else: algo = Fusion(comb_class, row_idx=idx) params: Dict[str, str] = {} - for ass in comb_class.assumptions: + for ass in comb_class.tracking_assumptions: mapped_ass = ass.__class__( [ children[idx].forward_map.map_gp(gp) diff --git a/tilings/strategies/verification.py b/tilings/strategies/verification.py index f5c0591d..569aac0a 100644 --- a/tilings/strategies/verification.py +++ b/tilings/strategies/verification.py @@ -63,25 +63,27 @@ class BasicVerificationStrategy(AtomStrategy): @staticmethod def get_terms(comb_class: CombinatorialClass, n: int) -> Terms: - if not isinstance(comb_class, Tiling): + if not isinstance(comb_class, Tiling) or comb_class.predicate_assumptions: raise NotImplementedError gp = next(comb_class.minimal_gridded_perms()) if n == len(gp): parameters = tuple( - assumption.get_value(gp) for assumption in comb_class.assumptions + assumption.get_value(gp) + for assumption in comb_class.tracking_assumptions ) return Counter([parameters]) return Counter() @staticmethod def get_objects(comb_class: CombinatorialClass, n: int) -> Objects: - if not isinstance(comb_class, Tiling): + if not isinstance(comb_class, Tiling) or comb_class.predicate_assumptions: raise NotImplementedError res: Objects = defaultdict(list) gp = next(comb_class.minimal_gridded_perms()) if n == len(gp): parameters = tuple( - assumption.get_value(gp) for assumption in comb_class.assumptions + assumption.get_value(gp) + for assumption in comb_class.tracking_assumptions ) res[parameters].append(gp) return res @@ -113,12 +115,12 @@ def get_genf( ) -> Expr: if not self.verified(comb_class): raise StrategyDoesNotApply("Can't find generating functon for non-atom.") - if not isinstance(comb_class, Tiling): + if not isinstance(comb_class, Tiling) or comb_class.predicate_assumptions: raise NotImplementedError cast(Tiling, comb_class) gp = next(comb_class.minimal_gridded_perms()) expected = {"x": len(gp)} - for assumption in comb_class.assumptions: + for assumption in comb_class.tracking_assumptions: expected[ comb_class.get_assumption_parameter(assumption) ] = assumption.get_value(gp) @@ -151,7 +153,7 @@ def get_equation( # for the class with requirements. eq = Eq(self.without_req_genf(self.comb_class), get_function(self.comb_class)) subs = solve([eq], var("F"), dict=True)[0] - if self.comb_class.assumptions: + if self.comb_class.tracking_assumptions: subs["x"] = var("x") * var("k_0") res, _ = sympify(lhs).subs(subs, simultaneous=True).as_numer_denom() # Pick the unique factor that contains F diff --git a/tilings/tiling.py b/tilings/tiling.py index b2d39231..ec276005 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -88,7 +88,7 @@ total=False, ) -Assumptions = [ +ASSUMPTIONS = [ TrackingAssumption, SumComponentAssumption, SkewComponentAssumption, @@ -96,7 +96,7 @@ OddCountAssumption, EqualParityAssumption, OppositeParityAssumption, -] +] # DO NOT CHANGE THE ORDER OF THIS LIST class Tiling(CombinatorialClass): @@ -332,7 +332,7 @@ def clean_assumptions(self) -> None: TODO: this should remove points that are placed, and other requirements that are contained in every gridded perm. """ - res: List[TrackingAssumption] = [] + res: List[Assumption] = [] for assumption in self.assumptions: ass = assumption.avoiding(self._obstructions, self.active_cells) if ass.gps: @@ -437,7 +437,7 @@ def split_16bit(n) -> Tuple[int, int]: result.extend(split_16bit(len(self.assumptions))) for assumption in self.assumptions: try: - ass_idx = Assumptions.index(type(assumption)) + ass_idx = ASSUMPTIONS.index(type(assumption)) except ValueError as e: raise ValueError("Not a valid assumption.") from e result.append(ass_idx) @@ -498,7 +498,7 @@ def recreate_gp_list(offset): offset += 1 gps, offset = recreate_gp_list(offset) try: - ass_class = Assumptions[assumption_type] + ass_class = ASSUMPTIONS[assumption_type] except IndexError as e: raise IndexError("Invalid assumption type.") from e assumptions.append(ass_class(gps)) From 929aa630df388c55189a5f1b9411bba64b7c1120 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Wed, 20 Jul 2022 10:41:32 +0000 Subject: [PATCH 03/48] a predicate refinement strategy --- tilings/assumptions.py | 69 +++++++++++++++++++++++++++++++++++++++--- 1 file changed, 64 insertions(+), 5 deletions(-) diff --git a/tilings/assumptions.py b/tilings/assumptions.py index 6f4b3f33..2146dfbc 100644 --- a/tilings/assumptions.py +++ b/tilings/assumptions.py @@ -1,7 +1,17 @@ import abc from importlib import import_module from itertools import chain -from typing import TYPE_CHECKING, Iterable, List, Optional, Tuple, Type, TypeVar +from typing import ( + TYPE_CHECKING, + Iterable, + Iterator, + List, + Optional, + Tuple, + Type, + TypeVar, + Union, +) from permuta import Perm @@ -13,6 +23,7 @@ from tilings import Tiling AssumptionClass = TypeVar("AssumptionClass", bound="Assumption") +CountAssumption = Union["OddCountAssumption", "EvenCountAssumption"] class Assumption: @@ -78,6 +89,9 @@ def __eq__(self, other) -> bool: return bool(self.gps == other.gps) return NotImplemented + def __len__(self) -> int: + return len(self.gps) + def __lt__(self, other) -> bool: if isinstance(other, Assumption): key_self = (self.__class__.__name__, self.gps) @@ -279,6 +293,13 @@ def can_be_satisfied(self, tiling: "Tiling") -> bool: perm on the tiling. """ + def refinements(self) -> Iterator[Tuple["PredicateAssumption", ...]]: + """ + Yield tuples of Assumption that such that the predicate + satisfies a gp iff all refined predicates satisfies a gp. + """ + yield (self,) + class OddCountAssumption(PredicateAssumption): """There is an odd number of points at the cells""" @@ -289,8 +310,33 @@ def can_be_satisfied(self, tiling: "Tiling") -> bool: def _gp_satisfies(self, gp: GriddedPerm) -> bool: return bool(len(gp) % 2) + def refinements(self) -> Iterator[Tuple[CountAssumption, ...]]: + """ + Yield tuples of single cell Odd/Even CountAssumption that + combine to match the parity. + """ + yield from self._refinements(list(self.cells), True) + + @staticmethod + def helper_refinements( + cells: List[Cell], odd: bool + ) -> Iterator[Tuple[CountAssumption, ...]]: + cell = cells.pop() + if cells: + for refinement in OddCountAssumption.helper_refinements(list(cells), odd): + yield (EvenCountAssumption.from_cells([cell]),) + refinement + for refinement in OddCountAssumption.helper_refinements( + list(cells), not odd + ): + yield (OddCountAssumption.from_cells([cell]),) + refinement + + elif odd: + yield (OddCountAssumption.from_cells([cell]),) + else: + yield (EvenCountAssumption.from_cells([cell]),) + def __str__(self) -> str: - return "odd number of points in cells {self.cells}" + return f"odd number of points in cells {self.cells}" class EvenCountAssumption(PredicateAssumption): @@ -302,8 +348,15 @@ def can_be_satisfied(self, tiling: "Tiling") -> bool: def _gp_satisfies(self, gp: GriddedPerm) -> bool: return not bool(len(gp) % 2) + def refinements(self) -> Iterator[Tuple[CountAssumption, ...]]: + """ + Yield tuples of single cell Odd/Even CountAssumption that + combine to match the parity. + """ + yield from OddCountAssumption.helper_refinements(list(self.cells), False) + def __str__(self) -> str: - return "even number of points in cells {self.cells}" + return f"even number of points in cells {self.cells}" class EqualParityAssumption(PredicateAssumption): @@ -320,8 +373,11 @@ def satisfies(self, gp: GriddedPerm) -> bool: def _gp_satisies(self, gp: GriddedPerm) -> bool: raise NotImplementedError + def refinements(self) -> Iterator[Tuple["EqualParityAssumption", ...]]: + yield tuple(EqualParityAssumption.from_cells([cell]) for cell in self.cells) + def __str__(self) -> str: - return "points are equal parity in cells {self.cells}" + return f"points are equal parity in cells {self.cells}" class OppositeParityAssumption(PredicateAssumption): @@ -338,5 +394,8 @@ def satisfies(self, gp: GriddedPerm) -> bool: def _gp_satisies(self, gp: GriddedPerm) -> bool: raise NotImplementedError + def refinements(self) -> Iterator[Tuple["OppositeParityAssumption", ...]]: + yield tuple(OppositeParityAssumption.from_cells([cell]) for cell in self.cells) + def __str__(self) -> str: - return "points are opposite parity in cells {self.cells}" + return f"points are opposite parity in cells {self.cells}" From 4dfb74a23f8e7f94e6be1b84cbe9c3a0adc13fa8 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Wed, 20 Jul 2022 10:43:18 +0000 Subject: [PATCH 04/48] the refinement strategy --- tilings/strategies/predicate_refinement.py | 74 ++++++++++++++++++++++ 1 file changed, 74 insertions(+) create mode 100644 tilings/strategies/predicate_refinement.py diff --git a/tilings/strategies/predicate_refinement.py b/tilings/strategies/predicate_refinement.py new file mode 100644 index 00000000..6797c2c1 --- /dev/null +++ b/tilings/strategies/predicate_refinement.py @@ -0,0 +1,74 @@ +from itertools import chain, product +from typing import Dict, Iterator, Optional, Tuple + +from comb_spec_searcher import DisjointUnionStrategy +from comb_spec_searcher.exception import StrategyDoesNotApply +from tilings import GriddedPerm, Tiling + + +class RefinePredicatesStrategy(DisjointUnionStrategy[Tiling, GriddedPerm]): + def __init__( + self, + ignore_parent: bool = True, + inferrable: bool = False, + possibly_empty: bool = True, + workable: bool = True, + ): + super().__init__(ignore_parent, inferrable, possibly_empty, workable) + + def decomposition_function(self, comb_class: Tiling) -> Tuple[Tiling, ...]: + if comb_class.predicate_assumptions: + without_predicates = comb_class.remove_assumptions().add_assumptions( + comb_class.tracking_assumptions + ) + children = [] + for assumptions in product( + *[ass.refinements() for ass in comb_class.predicate_assumptions] + ): + children.append(without_predicates.add_assumptions(chain(*assumptions))) + return tuple(children) + raise StrategyDoesNotApply + + def formal_step(self) -> str: + return "odd/even analysis" + + def backward_map( + self, + comb_class: Tiling, + objs: Tuple[Optional[GriddedPerm], ...], + children: Optional[Tuple[Tiling, ...]] = None, + ) -> Iterator[GriddedPerm]: + if children is None: + children = self.decomposition_function(comb_class) + raise NotImplementedError + + def forward_map( + self, + comb_class: Tiling, + obj: GriddedPerm, + children: Optional[Tuple[Tiling, ...]] = None, + ) -> Tuple[Optional[GriddedPerm], ...]: + if children is None: + children = self.decomposition_function(comb_class) + raise NotImplementedError + + def extra_parameters( + self, + comb_class: Tiling, + children: Optional[Tuple[Tiling, ...]] = None, + ) -> Tuple[Dict[str, str], ...]: + if children is None: + children = self.decomposition_function(comb_class) + return tuple( + { + comb_class.get_assumption_parameter( + ass + ): child.get_assumption_parameter(ass) + for ass in comb_class.tracking_assumptions + } + for child in children + ) + + @classmethod + def from_dict(cls, d: dict) -> "RefinePredicatesStrategy": + return cls(**d) From b3ce42ba9b6c55d7f80e30667df308a07b4b500c Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Thu, 21 Jul 2022 11:30:20 +0000 Subject: [PATCH 05/48] a parity scope class --- tilings/assumptions.py | 2 +- tilings/strategies/predicate_refinement.py | 2 +- tilings/tilescope.py | 141 ++++++++++++++++++--- tilings/tiling.py | 42 +++--- 4 files changed, 154 insertions(+), 33 deletions(-) diff --git a/tilings/assumptions.py b/tilings/assumptions.py index 2146dfbc..ed553de7 100644 --- a/tilings/assumptions.py +++ b/tilings/assumptions.py @@ -315,7 +315,7 @@ def refinements(self) -> Iterator[Tuple[CountAssumption, ...]]: Yield tuples of single cell Odd/Even CountAssumption that combine to match the parity. """ - yield from self._refinements(list(self.cells), True) + yield from self.helper_refinements(list(self.cells), True) @staticmethod def helper_refinements( diff --git a/tilings/strategies/predicate_refinement.py b/tilings/strategies/predicate_refinement.py index 6797c2c1..b649920f 100644 --- a/tilings/strategies/predicate_refinement.py +++ b/tilings/strategies/predicate_refinement.py @@ -30,7 +30,7 @@ def decomposition_function(self, comb_class: Tiling) -> Tuple[Tiling, ...]: raise StrategyDoesNotApply def formal_step(self) -> str: - return "odd/even analysis" + return "predicate refinement" def backward_map( self, diff --git a/tilings/tilescope.py b/tilings/tilescope.py index 25b4e906..7f41be25 100644 --- a/tilings/tilescope.py +++ b/tilings/tilescope.py @@ -23,9 +23,16 @@ ) from comb_spec_searcher.class_queue import CSSQueue, DefaultQueue, WorkPacket from comb_spec_searcher.rule_db.abstract import RuleDBAbstract +from comb_spec_searcher.strategies.strategy import DisjointUnionStrategy from comb_spec_searcher.typing import CombinatorialClassType, CSSstrategy from permuta import Basis, Perm from tilings import GriddedPerm, Tiling +from tilings.assumptions import ( + EqualParityAssumption, + EvenCountAssumption, + OddCountAssumption, +) +from tilings.strategies.predicate_refinement import RefinePredicatesStrategy from tilings.strategy_pack import TileScopePack __all__ = ("TileScope", "TileScopePack", "LimitedAssumptionTileScope", "GuidedSearcher") @@ -45,13 +52,34 @@ def __init__( expand_verified: bool = False, debug: bool = False, ) -> None: - """Initialise TileScope.""" + start_tiling, basis = self._get_start_tiling(start_class) + + if start_tiling.dimensions == (1, 1): + logger.debug("Fixing basis in basis aware verification strategies.") + assert isinstance(basis, Basis) + strategy_pack = strategy_pack.add_basis(basis) + strategy_pack = strategy_pack.setup_subclass_verification(start_tiling) + + super().__init__( + start_class=start_tiling, + strategy_pack=strategy_pack, + ruledb=ruledb, + expand_verified=expand_verified, + debug=debug, + ) + + def _get_start_tiling( + self, start_class: Union[str, Iterable[Perm], Tiling] + ) -> Tuple[Tiling, Optional[Basis]]: + """Return the start tiling implied by the input.""" if isinstance(start_class, str): basis = Basis.from_string(start_class) elif isinstance(start_class, Tiling): if start_class.dimensions == (1, 1): basis = Basis(*[o.patt for o in start_class.obstructions]) + else: + basis = None start_tiling = start_class else: try: @@ -65,19 +93,7 @@ def __init__( start_tiling = Tiling( obstructions=[GriddedPerm.single_cell(patt, (0, 0)) for patt in basis] ) - - if start_tiling.dimensions == (1, 1): - logger.debug("Fixing basis in basis aware verification strategies.") - strategy_pack = strategy_pack.add_basis(basis) - strategy_pack = strategy_pack.setup_subclass_verification(start_tiling) - - super().__init__( - start_class=start_tiling, - strategy_pack=strategy_pack, - ruledb=ruledb, - expand_verified=expand_verified, - debug=debug, - ) + return start_tiling, basis class LimitedAssumptionTileScope(TileScope): @@ -114,7 +130,7 @@ def _expand( def num_child_assumptions(child: Tiling) -> int: return sum( 1 - for ass in child.assumptions + for ass in child.tracking_assumptions if (not self.ignore_full_tiling_assumptions) or len(ass.gps) != len(child.active_cells) ) @@ -386,3 +402,98 @@ def __next__(self) -> WorkPacket: return next(queue) except StopIteration: continue + + +class OddOrEvenStrategy(DisjointUnionStrategy[Tiling, GriddedPerm]): + def __init__(self): + super().__init__(True, True, True, True) + + def decomposition_function(self, comb_class: Tiling) -> Tuple[Tiling, Tiling]: + return ( + comb_class.add_assumption( + EvenCountAssumption.from_cells(comb_class.active_cells) + ), + comb_class.add_assumption( + OddCountAssumption.from_cells(comb_class.active_cells) + ), + ) + + def formal_step(self) -> str: + return "has an odd or even number of points" + + def backward_map( + self, + comb_class: Tiling, + objs: Tuple[Optional[GriddedPerm], ...], + children: Optional[Tuple[Tiling, ...]] = None, + ) -> Iterator[GriddedPerm]: + if children is None: + children = self.decomposition_function(comb_class) + gp = objs[0] + assert gp is not None + yield gp + + def forward_map( + self, + comb_class: Tiling, + obj: GriddedPerm, + children: Optional[Tuple[Tiling, ...]] = None, + ) -> Tuple[Optional[GriddedPerm], ...]: + if children is None: + children = self.decomposition_function(comb_class) + if len(obj) % 2: + return (obj, None) + return (None, obj) + + def extra_parameters( + self, + comb_class: Tiling, + children: Optional[Tuple[Tiling, ...]] = None, + ) -> Tuple[Dict[str, str], ...]: + if children is None: + children = self.decomposition_function(comb_class) + return tuple( + { + comb_class.get_assumption_parameter( + ass + ): child.get_assumption_parameter(ass) + for ass in comb_class.tracking_assumptions + } + for child in children + ) + + @classmethod + def from_dict(cls, d: dict) -> "OddOrEvenStrategy": + return cls(**d) + + +class ParityScope(TrackedSearcher): + def __init__( + self, + start_class: Union[str, Iterable[Perm], Tiling], + strategy_pack: TileScopePack, + max_assumptions: int, + delay_next: bool = False, + **kwargs, + ) -> None: + super().__init__( + start_class, + strategy_pack.add_initial(RefinePredicatesStrategy(), apply_first=True), + max_assumptions, + delay_next, + **kwargs, + ) + rule = OddOrEvenStrategy()(self.start_class) + end_labels = tuple(self.classdb.get_label(child) for child in rule.children) + self.add_rule(self.start_label, end_labels, rule) + + def _get_start_tiling( + self, start_class: Union[str, Iterable[Perm], Tiling] + ) -> Tiling: + start_tiling, basis = super()._get_start_tiling(start_class) + return ( + start_tiling.add_assumption( + EqualParityAssumption.from_cells(start_tiling.active_cells) + ), + basis, + ) diff --git a/tilings/tiling.py b/tilings/tiling.py index ec276005..8484781b 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -163,20 +163,23 @@ def __init__( # Remove empty rows and empty columns if remove_empty_rows_and_cols: self._remove_empty_rows_and_cols() - + # TODO: check predicates and set_empty if relevant else: - self._obstructions = (GriddedPerm.empty_perm(),) - self._requirements = tuple() - self._assumptions = tuple() - self._cached_properties["active_cells"] = frozenset() - self._cached_properties["backward_map"] = RowColMap.identity((0, 0)) - self._cached_properties["cell_basis"] = {(0, 0): ([Perm()], [])} - self._cached_properties["dimensions"] = (1, 1) - self._cached_properties["empty_cells"] = frozenset([(0, 0)]) - self._cached_properties["forward_map"] = RowColMap.identity((0, 0)) - self._cached_properties["point_cells"] = frozenset() - self._cached_properties["positive_cells"] = frozenset() - self._cached_properties["possibly_empty"] = frozenset() + self.set_empty() + + def set_empty(self): + self._obstructions = (GriddedPerm.empty_perm(),) + self._requirements = tuple() + self._assumptions = tuple() + self._cached_properties["active_cells"] = frozenset() + self._cached_properties["backward_map"] = RowColMap.identity((0, 0)) + self._cached_properties["cell_basis"] = {(0, 0): ([Perm()], [])} + self._cached_properties["dimensions"] = (1, 1) + self._cached_properties["empty_cells"] = frozenset([(0, 0)]) + self._cached_properties["forward_map"] = RowColMap.identity((0, 0)) + self._cached_properties["point_cells"] = frozenset() + self._cached_properties["positive_cells"] = frozenset() + self._cached_properties["possibly_empty"] = frozenset() @classmethod def from_perms( @@ -249,15 +252,22 @@ def _simplify_griddedperms(self, already_minimized_obs=False) -> None: respective lists. If any requirement list is empty, then the tiling is empty. """ + GPR = GriddedPermReduction( self.obstructions, self.requirements, sorted_input=True, already_minimized_obs=already_minimized_obs, ) - - self._obstructions = GPR.obstructions - self._requirements = GPR.requirements + if any( + all(GriddedPerm.point_perm(cell) in GPR.obstructions for cell in ass.cells) + for ass in self.predicate_assumptions + if isinstance(ass, OddCountAssumption) + ): + self.set_empty() + else: + self._obstructions = GPR.obstructions + self._requirements = GPR.requirements def _remove_empty_rows_and_cols(self) -> None: """Remove empty rows and columns.""" From 3ebe3f47255561c437a68ecd3befa6f280de0462 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Thu, 21 Jul 2022 11:37:05 +0000 Subject: [PATCH 06/48] some tidy up --- tilings/tilescope.py | 22 ++++++++++++---------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/tilings/tilescope.py b/tilings/tilescope.py index 7f41be25..1471885a 100644 --- a/tilings/tilescope.py +++ b/tilings/tilescope.py @@ -53,7 +53,7 @@ def __init__( debug: bool = False, ) -> None: """Initialise TileScope.""" - start_tiling, basis = self._get_start_tiling(start_class) + start_tiling, basis = self.get_start_tiling(start_class) if start_tiling.dimensions == (1, 1): logger.debug("Fixing basis in basis aware verification strategies.") @@ -69,17 +69,17 @@ def __init__( debug=debug, ) - def _get_start_tiling( - self, start_class: Union[str, Iterable[Perm], Tiling] + @staticmethod + def get_start_tiling( + start_class: Union[str, Iterable[Perm], Tiling] ) -> Tuple[Tiling, Optional[Basis]]: """Return the start tiling implied by the input.""" + basis: Optional[Basis] = None if isinstance(start_class, str): basis = Basis.from_string(start_class) elif isinstance(start_class, Tiling): if start_class.dimensions == (1, 1): basis = Basis(*[o.patt for o in start_class.obstructions]) - else: - basis = None start_tiling = start_class else: try: @@ -90,6 +90,7 @@ def _get_start_tiling( ) from e if not isinstance(start_class, Tiling): + assert basis is not None start_tiling = Tiling( obstructions=[GriddedPerm.single_cell(patt, (0, 0)) for patt in basis] ) @@ -464,7 +465,7 @@ def extra_parameters( @classmethod def from_dict(cls, d: dict) -> "OddOrEvenStrategy": - return cls(**d) + return cls() class ParityScope(TrackedSearcher): @@ -487,10 +488,11 @@ def __init__( end_labels = tuple(self.classdb.get_label(child) for child in rule.children) self.add_rule(self.start_label, end_labels, rule) - def _get_start_tiling( - self, start_class: Union[str, Iterable[Perm], Tiling] - ) -> Tiling: - start_tiling, basis = super()._get_start_tiling(start_class) + @staticmethod + def get_start_tiling( + start_class: Union[str, Iterable[Perm], Tiling] + ) -> Tuple[Tiling, Optional[Basis]]: + start_tiling, basis = TileScope.get_start_tiling(start_class) return ( start_tiling.add_assumption( EqualParityAssumption.from_cells(start_tiling.active_cells) From 14f74bba4b904940edc463d36b1e83d730372ca3 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Thu, 21 Jul 2022 11:37:24 +0000 Subject: [PATCH 07/48] an experimental is empty check --- tilings/tiling.py | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/tilings/tiling.py b/tilings/tiling.py index 8484781b..51427ac6 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -1481,10 +1481,11 @@ def is_empty(self) -> bool: not ass.can_be_satisfied(self) for ass in self.predicate_assumptions ): return True - if len(self.requirements) <= 1: - return False - MGP = MinimalGriddedPerms(self.obstructions, self.requirements) - return all(False for _ in MGP.minimal_gridded_perms(yield_non_minimal=True)) + # if len(self.requirements) <= 1: + # return False + # MGP = MinimalGriddedPerms(self.obstructions, self.requirements) + # return all(False for _ in MGP.minimal_gridded_perms(yield_non_minimal=True)) + return all(False for _ in self.gridded_perms(self.minimum_size_of_object() + 4)) def is_finite(self) -> bool: """Returns True if all active cells have finite basis.""" From cdae45e3ce7f1ef4cba43ea798faf850ede67f70 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Thu, 21 Jul 2022 12:44:03 +0000 Subject: [PATCH 08/48] factor toggles parity --- tilings/algorithms/factor.py | 4 ++++ tilings/strategies/verification.py | 2 +- tilings/tiling.py | 35 ++++++++++++++++++++++++------ 3 files changed, 33 insertions(+), 8 deletions(-) diff --git a/tilings/algorithms/factor.py b/tilings/algorithms/factor.py index 16ed9cf2..c9b401bc 100644 --- a/tilings/algorithms/factor.py +++ b/tilings/algorithms/factor.py @@ -76,6 +76,10 @@ def _unite_assumptions(self) -> None: """ For each TrackingAssumption unite all the positions of the gridded perms. """ + if any(len(ass.cells) > 1 for ass in self._tiling.predicate_assumptions): + # DO NOT FACTOR + self._unite_cells(self._tiling.active_cells) + return for assumption in self._tiling.assumptions: if isinstance(assumption, ComponentAssumption): for cells in assumption.cell_decomposition(self._tiling): diff --git a/tilings/strategies/verification.py b/tilings/strategies/verification.py index 569aac0a..7c9bda3b 100644 --- a/tilings/strategies/verification.py +++ b/tilings/strategies/verification.py @@ -63,7 +63,7 @@ class BasicVerificationStrategy(AtomStrategy): @staticmethod def get_terms(comb_class: CombinatorialClass, n: int) -> Terms: - if not isinstance(comb_class, Tiling) or comb_class.predicate_assumptions: + if not isinstance(comb_class, Tiling): raise NotImplementedError gp = next(comb_class.minimal_gridded_perms()) if n == len(gp): diff --git a/tilings/tiling.py b/tilings/tiling.py index 51427ac6..6d58dc94 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -1117,22 +1117,43 @@ def sub_tiling( or all(c in cells for c in chain.from_iterable(r.pos for r in req)) ) assumptions = tuple( - ass.__class__( - gp - for gp in ass.gps - if (factors and gp.pos[0] in cells) or all(c in cells for c in gp.pos) - ) - for ass in self.assumptions + self.factored_assumption(ass, cells, factors) for ass in self.assumptions ) + tuple(add_assumptions) # TODO: check sum/skew assumptions return self.__class__( obstructions, requirements, tuple(sorted(set(ass for ass in assumptions if ass.gps))), - simplify=False, + simplify=bool(self.predicate_assumptions), sorted_input=True, ) + def factored_assumption( + self, assumption: Assumption, cells: Iterable[Cell], factors: bool = False + ) -> Assumption: + if isinstance( + assumption, (TrackingAssumption, OddCountAssumption, EvenCountAssumption) + ): + return assumption.__class__( + gp + for gp in assumption.gps + if (factors and gp.pos[0] in cells) or all(c in cells for c in gp.pos) + ) + assert all(len(ass.cells) == 1 for ass in self.predicate_assumptions) + ass_x, ass_y = next(iter(assumption.cells)) + odd_cells = set( + cell + for cell in self.active_cells + if OddCountAssumption.from_cells([cell]) in self.assumptions + ) - set(cells) + odd_below = bool(sum(1 for _, y in odd_cells if y < ass_y) % 2) + odd_left = bool(sum(1 for x, _ in odd_cells if x < ass_x) % 2) + if odd_below == odd_left: + return assumption + elif isinstance(assumption, EqualParityAssumption): + return OppositeParityAssumption(assumption.gps) + return EqualParityAssumption(assumption.gps) + def find_factors(self, interleaving: str = "none") -> Tuple["Tiling", ...]: """ Return list with the factors of the tiling. From 61ac5cb186a5b831bc11f82ec823f87221693e35 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Thu, 21 Jul 2022 15:05:59 +0000 Subject: [PATCH 09/48] add to fusion strategy --- tilings/algorithms/fusion.py | 81 ++++++++++++++++++++++++++--- tilings/assumptions.py | 10 ++-- tilings/strategies/factor.py | 2 +- tilings/strategies/fusion/fusion.py | 10 ++-- tilings/tiling.py | 2 +- 5 files changed, 89 insertions(+), 16 deletions(-) diff --git a/tilings/algorithms/fusion.py b/tilings/algorithms/fusion.py index 6e471e3c..d7d04fd1 100644 --- a/tilings/algorithms/fusion.py +++ b/tilings/algorithms/fusion.py @@ -6,6 +6,7 @@ from typing import ( TYPE_CHECKING, Counter, + Dict, FrozenSet, Iterable, Iterator, @@ -15,7 +16,14 @@ ) from tilings.assumptions import ( + Assumption, + AssumptionClass, ComponentAssumption, + EqualParityAssumption, + EvenCountAssumption, + OddCountAssumption, + OppositeParityAssumption, + PredicateAssumption, SkewComponentAssumption, SumComponentAssumption, TrackingAssumption, @@ -248,7 +256,7 @@ def assumptions_fuse_counters(self) -> List[Counter[GriddedPerm]]: return self._assumptions_fuse_counters counters = [ self._fuse_counter(assumption.gps) - for assumption in self._tiling.assumptions + for assumption in self._tiling.tracking_assumptions ] self._assumptions_fuse_counters = counters return self._assumptions_fuse_counters @@ -359,7 +367,7 @@ def _num_fusing_assumptions(self) -> int: return len( [ assumption - for assumption in self._tiling.assumptions + for assumption in self._tiling.tracking_assumptions if all(cell in fusing_cells for gp in assumption.gps for cell in gp.pos) ] ) @@ -394,7 +402,7 @@ def fusable(self) -> bool: ass_fusable = all( self._can_fuse_assumption(assumption, counter) for assumption, counter in zip( - self._tiling.assumptions, self.assumptions_fuse_counters + self._tiling.tracking_assumptions, self.assumptions_fuse_counters ) ) return ( @@ -402,19 +410,44 @@ def fusable(self) -> bool: and req_fusable and ass_fusable and self._check_isolation_level() + and self.predicate_fusable() ) + def predicate_fusable(self) -> bool: + if any(len(ass.cells) > 1 for ass in self._tiling.predicate_assumptions): + return False + equal, opposite = set(), set() + for ass in self._tiling.predicate_assumptions: + if isinstance(ass, EqualParityAssumption): + equal.add(next(iter(ass.cells))) + elif isinstance(ass, OppositeParityAssumption): + opposite.add(next(iter(ass.cells))) + left = self._left_fuse_region() + for (x, y) in left: + xn, yn = x, y + if self._fuse_row: + yn += 1 + else: + xn += 1 + cell, neighbour = (x, y), (xn, yn) + if (cell in equal and neighbour in opposite) or ( + cell in opposite and neighbour in equal + ): + return False + return True + def fused_tiling(self) -> "Tiling": """ Return the fused tiling. """ if self._fused_tiling is None: - assumptions = [ + assumptions: List[Assumption] = [ ass.__class__(gps) for ass, gps in zip( - self._tiling.assumptions, self.assumptions_fuse_counters + self._tiling.tracking_assumptions, self.assumptions_fuse_counters ) ] + assumptions.extend(self.fused_predicates()) if self._tracked: assumptions.append(self.new_assumption()) requirements = list(list(fc) for fc in self.requirements_fuse_counters) @@ -430,6 +463,36 @@ def fused_tiling(self) -> "Tiling": ) return self._fused_tiling + def fuse_assumption(self, assumption: AssumptionClass) -> AssumptionClass: + return assumption.__class__(self.fuse_gridded_perm(gp) for gp in assumption.gps) + + def fused_predicates(self) -> Iterator[PredicateAssumption]: + left, right = self._left_fuse_region(), self._right_fuse_region() + odd_fused_cells: Dict[Cell, bool] = collections.defaultdict(bool) + for predicate in self._tiling.predicate_assumptions: + if isinstance(predicate, (EqualParityAssumption, OppositeParityAssumption)): + yield self.fuse_assumption(predicate) + else: + assert isinstance(predicate, (OddCountAssumption, EvenCountAssumption)) + cell = next(iter(predicate.cells), None) + assert cell is not None + if cell in left: + odd_fused_cells[cell] |= isinstance(predicate, OddCountAssumption) + elif cell in right: + (x, y) = cell + if self._fuse_row: + y -= 1 + else: + x -= 1 + odd_fused_cells[(x, y)] |= isinstance(predicate, OddCountAssumption) + else: + yield self.fuse_assumption(predicate) + for cell, odd in odd_fused_cells.items(): + if odd: + yield OddCountAssumption.from_cells([cell]) + else: + yield EvenCountAssumption.from_cells([cell]) + class ComponentFusion(Fusion): """ @@ -629,7 +692,11 @@ def fusable(self) -> bool: Return True if adjacent rows can be viewed as one row where you draw a horizontal line through the components. """ - if not self._pre_check() or not self.has_crossing_len2_ob(): + if ( + not self._pre_check() + or not self.has_crossing_len2_ob() + or self._tiling.predicate_assumptions + ): return False new_tiling = self._tiling.add_obstructions(self.obstructions_to_add()) @@ -638,7 +705,7 @@ def fusable(self) -> bool: and self._check_isolation_level() and all( self._can_component_fuse_assumption(assumption) - for assumption in self._tiling.assumptions + for assumption in self._tiling.tracking_assumptions ) ) diff --git a/tilings/assumptions.py b/tilings/assumptions.py index ed553de7..7fcf5351 100644 --- a/tilings/assumptions.py +++ b/tilings/assumptions.py @@ -295,8 +295,10 @@ def can_be_satisfied(self, tiling: "Tiling") -> bool: def refinements(self) -> Iterator[Tuple["PredicateAssumption", ...]]: """ - Yield tuples of Assumption that such that the predicate - satisfies a gp iff all refined predicates satisfies a gp. + A refinement is a tuple of Assumptions. This yields a set + of refinements with the property that a gp satisfies this + predicate if and only if it satisfies exactly one refinement + in the set. """ yield (self,) @@ -370,7 +372,7 @@ def satisfies(self, gp: GriddedPerm) -> bool: if gp.pos[idx] in self.cells ) - def _gp_satisies(self, gp: GriddedPerm) -> bool: + def _gp_satisfies(self, gp: GriddedPerm) -> bool: raise NotImplementedError def refinements(self) -> Iterator[Tuple["EqualParityAssumption", ...]]: @@ -391,7 +393,7 @@ def satisfies(self, gp: GriddedPerm) -> bool: if gp.pos[idx] in self.cells ) - def _gp_satisies(self, gp: GriddedPerm) -> bool: + def _gp_satisfies(self, gp: GriddedPerm) -> bool: raise NotImplementedError def refinements(self) -> Iterator[Tuple["OppositeParityAssumption", ...]]: diff --git a/tilings/strategies/factor.py b/tilings/strategies/factor.py index 1b139552..8a5fbf1e 100644 --- a/tilings/strategies/factor.py +++ b/tilings/strategies/factor.py @@ -90,7 +90,7 @@ def extra_parameters( raise StrategyDoesNotApply("Strategy does not apply") extra_parameters: Tuple[Dict[str, str], ...] = tuple({} for _ in children) for parent_var, assumption in zip( - comb_class.extra_parameters, comb_class.assumptions + comb_class.extra_parameters, comb_class.tracking_assumptions ): for idx, child in enumerate(children): new_assumption = child.forward_map.map_assumption(assumption).avoiding( diff --git a/tilings/strategies/fusion/fusion.py b/tilings/strategies/fusion/fusion.py index 932b117f..991ef637 100644 --- a/tilings/strategies/fusion/fusion.py +++ b/tilings/strategies/fusion/fusion.py @@ -176,7 +176,9 @@ def is_reversible(self, comb_class: Tiling) -> bool: new_ass = algo.new_assumption() fused_assumptions = ( ass.__class__(gps) - for ass, gps in zip(comb_class.assumptions, algo.assumptions_fuse_counters) + for ass, gps in zip( + comb_class.tracking_assumptions, algo.assumptions_fuse_counters + ) ) return new_ass in fused_assumptions @@ -270,7 +272,9 @@ def extra_parameters( child = children[0] mapped_assumptions = [ child.forward_map.map_assumption(ass.__class__(gps)) - for ass, gps in zip(comb_class.assumptions, algo.assumptions_fuse_counters) + for ass, gps in zip( + comb_class.tracking_assumptions, algo.assumptions_fuse_counters + ) ] return ( { @@ -287,7 +291,7 @@ def left_right_both_sided_parameters( right_sided_params: Set[str] = set() both_sided_params: Set[str] = set() algo = self.fusion_algorithm(comb_class) - for assumption in comb_class.assumptions: + for assumption in comb_class.tracking_assumptions: parent_var = comb_class.get_assumption_parameter(assumption) left_sided = algo.is_left_sided_assumption(assumption) right_sided = algo.is_right_sided_assumption(assumption) diff --git a/tilings/tiling.py b/tilings/tiling.py index 6d58dc94..53b130f5 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -1150,7 +1150,7 @@ def factored_assumption( odd_left = bool(sum(1 for x, _ in odd_cells if x < ass_x) % 2) if odd_below == odd_left: return assumption - elif isinstance(assumption, EqualParityAssumption): + if isinstance(assumption, EqualParityAssumption): return OppositeParityAssumption(assumption.gps) return EqualParityAssumption(assumption.gps) From 96fedd1ffcce3c4dfb124102f7aafac32cb8a166 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Thu, 21 Jul 2022 15:22:46 +0000 Subject: [PATCH 10/48] fix experimental check --- tilings/tiling.py | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/tilings/tiling.py b/tilings/tiling.py index 53b130f5..c3baa676 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -1502,11 +1502,12 @@ def is_empty(self) -> bool: not ass.can_be_satisfied(self) for ass in self.predicate_assumptions ): return True - # if len(self.requirements) <= 1: - # return False - # MGP = MinimalGriddedPerms(self.obstructions, self.requirements) - # return all(False for _ in MGP.minimal_gridded_perms(yield_non_minimal=True)) - return all(False for _ in self.gridded_perms(self.minimum_size_of_object() + 4)) + if len(self.requirements) <= 1: + return False + MGP = MinimalGriddedPerms(self.obstructions, self.requirements) + return all( + False for _ in MGP.minimal_gridded_perms(yield_non_minimal=True) + ) or all(False for _ in self.gridded_perms(self.minimum_size_of_object() + 2)) def is_finite(self) -> bool: """Returns True if all active cells have finite basis.""" From e43524e4fbe2a4f9534301f45a1fcd67b02dfbcd Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Thu, 21 Jul 2022 15:24:22 +0000 Subject: [PATCH 11/48] plus 4 for experimental check --- tilings/tiling.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tilings/tiling.py b/tilings/tiling.py index c3baa676..172e3ced 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -1507,7 +1507,7 @@ def is_empty(self) -> bool: MGP = MinimalGriddedPerms(self.obstructions, self.requirements) return all( False for _ in MGP.minimal_gridded_perms(yield_non_minimal=True) - ) or all(False for _ in self.gridded_perms(self.minimum_size_of_object() + 2)) + ) or all(False for _ in self.gridded_perms(self.minimum_size_of_object() + 4)) def is_finite(self) -> bool: """Returns True if all active cells have finite basis.""" From cd43afa0880f1ef152d1aa7405aed7a9d0b64904 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Thu, 21 Jul 2022 15:36:16 +0000 Subject: [PATCH 12/48] experimental check --- tilings/tiling.py | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/tilings/tiling.py b/tilings/tiling.py index 172e3ced..77c15ddc 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -1502,12 +1502,12 @@ def is_empty(self) -> bool: not ass.can_be_satisfied(self) for ass in self.predicate_assumptions ): return True - if len(self.requirements) <= 1: - return False + # if len(self.requirements) <= 1: + # return False MGP = MinimalGriddedPerms(self.obstructions, self.requirements) - return all( - False for _ in MGP.minimal_gridded_perms(yield_non_minimal=True) - ) or all(False for _ in self.gridded_perms(self.minimum_size_of_object() + 4)) + if all(False for _ in MGP.minimal_gridded_perms(yield_non_minimal=True)): + return True + return all(False for _ in self.gridded_perms(self.minimum_size_of_object() + 4)) def is_finite(self) -> bool: """Returns True if all active cells have finite basis.""" From a26cb7e8e39a6aee94c3f357b7ea439a9711e6d1 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Thu, 21 Jul 2022 16:19:55 +0000 Subject: [PATCH 13/48] some atom counting --- tilings/strategies/verification.py | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/tilings/strategies/verification.py b/tilings/strategies/verification.py index 7c9bda3b..983c2404 100644 --- a/tilings/strategies/verification.py +++ b/tilings/strategies/verification.py @@ -66,7 +66,9 @@ def get_terms(comb_class: CombinatorialClass, n: int) -> Terms: if not isinstance(comb_class, Tiling): raise NotImplementedError gp = next(comb_class.minimal_gridded_perms()) - if n == len(gp): + if all( + pred.satisfies(gp) for pred in comb_class.predicate_assumptions + ) and n == len(gp): parameters = tuple( assumption.get_value(gp) for assumption in comb_class.tracking_assumptions @@ -80,7 +82,9 @@ def get_objects(comb_class: CombinatorialClass, n: int) -> Objects: raise NotImplementedError res: Objects = defaultdict(list) gp = next(comb_class.minimal_gridded_perms()) - if n == len(gp): + if all( + pred.satisfies(gp) for pred in comb_class.predicate_assumptions + ) and n == len(gp): parameters = tuple( assumption.get_value(gp) for assumption in comb_class.tracking_assumptions @@ -115,10 +119,12 @@ def get_genf( ) -> Expr: if not self.verified(comb_class): raise StrategyDoesNotApply("Can't find generating functon for non-atom.") - if not isinstance(comb_class, Tiling) or comb_class.predicate_assumptions: + if not isinstance(comb_class, Tiling): raise NotImplementedError cast(Tiling, comb_class) gp = next(comb_class.minimal_gridded_perms()) + if not all(pred.satisfies(gp) for pred in comb_class.predicate_assumptions): + return Expr(0) expected = {"x": len(gp)} for assumption in comb_class.tracking_assumptions: expected[ From 23a497e3b4494d817f7b35145642761eaaf4d43e Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Thu, 21 Jul 2022 18:01:03 +0000 Subject: [PATCH 14/48] add predicate strategy to verified packs --- tilings/strategies/verification.py | 35 +++++++++++++++++++++++------- 1 file changed, 27 insertions(+), 8 deletions(-) diff --git a/tilings/strategies/verification.py b/tilings/strategies/verification.py index 983c2404..8ba3b691 100644 --- a/tilings/strategies/verification.py +++ b/tilings/strategies/verification.py @@ -37,6 +37,7 @@ RemoveRequirementFactory, RequirementCorroborationFactory, ) +from tilings.strategies.predicate_refinement import RefinePredicatesStrategy from .abstract import BasisAwareVerificationStrategy @@ -219,13 +220,19 @@ def pack(comb_class: Tiling) -> StrategyPack: ] ): # subclass of Av(231) or a symmetry, use point placements! - return TileScopePack.point_and_row_and_col_placements().add_verification( - BasicVerificationStrategy(), replace=True + return ( + TileScopePack.point_and_row_and_col_placements() + .add_verification(BasicVerificationStrategy(), replace=True) + .add_initial(RefinePredicatesStrategy(), apply_first=True) ) if is_insertion_encodable_maximum(basis): - return TileScopePack.regular_insertion_encoding(3) + return TileScopePack.regular_insertion_encoding(3).add_initial( + RefinePredicatesStrategy(), apply_first=True + ) if is_insertion_encodable_rightmost(basis): - return TileScopePack.regular_insertion_encoding(2) + return TileScopePack.regular_insertion_encoding(2).add_initial( + RefinePredicatesStrategy(), apply_first=True + ) # if it is the class or positive class if not comb_class.requirements or ( len(comb_class.requirements) == 1 @@ -239,7 +246,11 @@ def pack(comb_class: Tiling) -> StrategyPack: ): # is a subclass of Av(123) avoiding patterns of length <= 4 # experimentally showed that such clsses always terminates - return TileScopePack.row_and_col_placements().add_basis(basis) + return ( + TileScopePack.row_and_col_placements() + .add_basis(basis) + .add_initial(RefinePredicatesStrategy(), apply_first=True) + ) raise InvalidOperationError( "Cannot get a specification for one by one verification for " f"subclass Av({basis})" @@ -626,7 +637,11 @@ def pack(self, comb_class: Tiling) -> StrategyPack: f"Cannot get a simpler specification for\n{comb_class}" ) return StrategyPack( - initial_strats=[FactorFactory(), DetectComponentsStrategy()], + initial_strats=[ + RefinePredicatesStrategy(), + FactorFactory(), + DetectComponentsStrategy(), + ], inferral_strats=[], expansion_strats=[], ver_strats=[ @@ -715,9 +730,13 @@ def pack(self, comb_class: Tiling) -> StrategyPack: from tilings.strategy_pack import TileScopePack if self.has_rightmost_insertion_encoding(comb_class): - pack = TileScopePack.regular_insertion_encoding(2) + pack = TileScopePack.regular_insertion_encoding(2).add_initial( + RefinePredicatesStrategy(), apply_first=True + ) elif self.has_topmost_insertion_encoding(comb_class): - pack = TileScopePack.regular_insertion_encoding(3) + pack = TileScopePack.regular_insertion_encoding(3).add_initial( + RefinePredicatesStrategy(), apply_first=True + ) else: raise StrategyDoesNotApply( "tiling does not has a regular insertion encoding" From 718d431139c6bcb4853d91db5e871a0d148a241f Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Thu, 21 Jul 2022 21:15:05 +0000 Subject: [PATCH 15/48] code to count fusion --- tilings/algorithms/fusion.py | 14 +++++++------- tilings/strategies/fusion/constructor.py | 21 +++++++++++++++++---- tilings/strategies/fusion/fusion.py | 4 ++++ tilings/tilescope.py | 5 +++-- 4 files changed, 31 insertions(+), 13 deletions(-) diff --git a/tilings/algorithms/fusion.py b/tilings/algorithms/fusion.py index d7d04fd1..f2553074 100644 --- a/tilings/algorithms/fusion.py +++ b/tilings/algorithms/fusion.py @@ -295,7 +295,7 @@ def _can_fuse_assumption( are all contained entirely on the left of the fusion region, entirely on the right, or split in every possible way. """ - left, right = self._left_fuse_region(), self._right_fuse_region() + left, right = self.left_fuse_region(), self.right_fuse_region() cells = set(gp.pos[0] for gp in assumption.gps) if (left.intersection(cells) and not left.issubset(cells)) or ( right.intersection(cells) and not right.issubset(cells) @@ -309,12 +309,12 @@ def _can_fuse_assumption( ) ) - def _left_fuse_region(self) -> FrozenSet[Cell]: + def left_fuse_region(self) -> FrozenSet[Cell]: if self._fuse_row: return self._tiling.cells_in_row(self._row_idx) return self._tiling.cells_in_col(self._col_idx) - def _right_fuse_region(self) -> FrozenSet[Cell]: + def right_fuse_region(self) -> FrozenSet[Cell]: if self._fuse_row: return self._tiling.cells_in_row(self._row_idx + 1) return self._tiling.cells_in_col(self._col_idx + 1) @@ -422,7 +422,7 @@ def predicate_fusable(self) -> bool: equal.add(next(iter(ass.cells))) elif isinstance(ass, OppositeParityAssumption): opposite.add(next(iter(ass.cells))) - left = self._left_fuse_region() + left = self.left_fuse_region() for (x, y) in left: xn, yn = x, y if self._fuse_row: @@ -467,7 +467,7 @@ def fuse_assumption(self, assumption: AssumptionClass) -> AssumptionClass: return assumption.__class__(self.fuse_gridded_perm(gp) for gp in assumption.gps) def fused_predicates(self) -> Iterator[PredicateAssumption]: - left, right = self._left_fuse_region(), self._right_fuse_region() + left, right = self.left_fuse_region(), self.right_fuse_region() odd_fused_cells: Dict[Cell, bool] = collections.defaultdict(bool) for predicate in self._tiling.predicate_assumptions: if isinstance(predicate, (EqualParityAssumption, OppositeParityAssumption)): @@ -477,14 +477,14 @@ def fused_predicates(self) -> Iterator[PredicateAssumption]: cell = next(iter(predicate.cells), None) assert cell is not None if cell in left: - odd_fused_cells[cell] |= isinstance(predicate, OddCountAssumption) + odd_fused_cells[cell] ^= isinstance(predicate, OddCountAssumption) elif cell in right: (x, y) = cell if self._fuse_row: y -= 1 else: x -= 1 - odd_fused_cells[(x, y)] |= isinstance(predicate, OddCountAssumption) + odd_fused_cells[(x, y)] ^= isinstance(predicate, OddCountAssumption) else: yield self.fuse_assumption(predicate) for cell, odd in odd_fused_cells.items(): diff --git a/tilings/strategies/fusion/constructor.py b/tilings/strategies/fusion/constructor.py index 6e9d0592..92e7bd75 100644 --- a/tilings/strategies/fusion/constructor.py +++ b/tilings/strategies/fusion/constructor.py @@ -74,7 +74,10 @@ def __init__( both_sided_parameters: Iterable[str], min_left: int, min_right: int, + odd_left: Optional[bool] = None, + odd_right: Optional[bool] = None, ): + self.odd_left_right = odd_left, odd_right # parent -> child parameters self.extra_parameters = extra_parameters # the reverse of the above list, although different parent parameters could @@ -130,11 +133,9 @@ def __init__( if k in self.right_sided_parameters ) self.fuse_parameter_index = child.extra_parameters.index(self.fuse_parameter) - child_pos_to_parent_pos = tuple( - index_mapping[idx] for idx in range(len(child.extra_parameters)) - ) self.children_param_map = self.build_param_map( - child_pos_to_parent_pos, len(parent.extra_parameters) + tuple(index_mapping[idx] for idx in range(len(child.extra_parameters))), + len(parent.extra_parameters), ) def _init_checked(self): @@ -256,6 +257,18 @@ def add_new_term( params: List[int], value: int, left_points: int, fuse_region_points: int ) -> None: """Update new terms if there is enough points on the left and right.""" + odd_left, odd_right = self.odd_left_right + if odd_left is not None: + if odd_left and left_points % 2 == 0: + return + if not odd_left and left_points % 2 == 1: + return + if odd_right is not None: + right_points = fuse_region_points - left_points + if odd_right and right_points % 2 == 0: + return + if not odd_right and right_points % 2 == 1: + return if ( min_left <= left_points and min_right <= fuse_region_points - left_points diff --git a/tilings/strategies/fusion/fusion.py b/tilings/strategies/fusion/fusion.py index 991ef637..8e02b905 100644 --- a/tilings/strategies/fusion/fusion.py +++ b/tilings/strategies/fusion/fusion.py @@ -9,6 +9,7 @@ from comb_spec_searcher.typing import Objects from tilings import GriddedPerm, Tiling from tilings.algorithms import Fusion +from tilings.assumptions import OddCountAssumption from ..pointing import DivideByK from .constructor import FusionConstructor, ReverseFusionConstructor @@ -201,6 +202,7 @@ def constructor( child = algo.fused_tiling() assert children is None or children == (child,) min_left, min_right = algo.min_left_right_points() + left, right = algo.left_fuse_region(), algo.right_fuse_region() return FusionConstructor( comb_class, child, @@ -209,6 +211,8 @@ def constructor( *self.left_right_both_sided_parameters(comb_class), min_left, min_right, + odd_left=(OddCountAssumption.from_cells(left) in comb_class.assumptions), + odd_right=(OddCountAssumption.from_cells(right) in comb_class.assumptions), ) def reverse_constructor( # pylint: disable=no-self-use diff --git a/tilings/tilescope.py b/tilings/tilescope.py index 1471885a..91a0a48b 100644 --- a/tilings/tilescope.py +++ b/tilings/tilescope.py @@ -373,11 +373,12 @@ def status(self) -> str: f"Queue {idx}" for idx in range(len(self.queues) - 1) ) underlying = ("underlying",) + tuple( - self._underlyng_labels_per_level[level] for level in range(len(self.queues)) + str(self._underlyng_labels_per_level[level]) + for level in range(len(self.queues)) ) table.append(underlying) all_labels = ("all labels",) + tuple( - self._all_labels_per_level[level] for level in range(len(self.queues)) + str(self._all_labels_per_level[level]) for level in range(len(self.queues)) ) table.append(all_labels) table = [headers] + table From 0dcffb4441eaffa18035a022857f9b8a4e88ef1e Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Fri, 22 Jul 2022 16:00:06 +0000 Subject: [PATCH 16/48] experimental is empty used to determine if factor is reversible --- tilings/strategies/factor.py | 5 ++++- tilings/strategies/verification.py | 4 ++-- tilings/tiling.py | 10 ++++++---- 3 files changed, 12 insertions(+), 7 deletions(-) diff --git a/tilings/strategies/factor.py b/tilings/strategies/factor.py index 8a5fbf1e..6e29503e 100644 --- a/tilings/strategies/factor.py +++ b/tilings/strategies/factor.py @@ -280,7 +280,10 @@ def is_two_way(self, comb_class: Tiling) -> bool: # type: ignore return self.is_reversible(comb_class) def is_reversible(self, comb_class: Tiling) -> bool: # type: ignore - return not bool(self.assumptions_to_add(comb_class)) + return ( + not bool(self.assumptions_to_add(comb_class)) + and not comb_class.experimental_is_empty() + ) def formal_step(self) -> str: return "interleaving " + super().formal_step() diff --git a/tilings/strategies/verification.py b/tilings/strategies/verification.py index 8ba3b691..90c8dea3 100644 --- a/tilings/strategies/verification.py +++ b/tilings/strategies/verification.py @@ -5,7 +5,7 @@ from typing import Callable, Dict, Iterator, Optional, Tuple, cast import requests -from sympy import Eq, Expr, Function, solve, sympify, var +from sympy import Eq, Expr, Function, Number, solve, sympify, var from comb_spec_searcher import ( AtomStrategy, @@ -125,7 +125,7 @@ def get_genf( cast(Tiling, comb_class) gp = next(comb_class.minimal_gridded_perms()) if not all(pred.satisfies(gp) for pred in comb_class.predicate_assumptions): - return Expr(0) + return Number(0) expected = {"x": len(gp)} for assumption in comb_class.tracking_assumptions: expected[ diff --git a/tilings/tiling.py b/tilings/tiling.py index 77c15ddc..77eb81fa 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -1502,11 +1502,13 @@ def is_empty(self) -> bool: not ass.can_be_satisfied(self) for ass in self.predicate_assumptions ): return True - # if len(self.requirements) <= 1: - # return False + # return self.experimental_is_empty() + if len(self.requirements) <= 1: + return False MGP = MinimalGriddedPerms(self.obstructions, self.requirements) - if all(False for _ in MGP.minimal_gridded_perms(yield_non_minimal=True)): - return True + return all(False for _ in MGP.minimal_gridded_perms(yield_non_minimal=True)) + + def experimental_is_empty(self) -> bool: return all(False for _ in self.gridded_perms(self.minimum_size_of_object() + 4)) def is_finite(self) -> bool: From 0f1f060e20a3357928798428f5cf7f97ad91d3e3 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Fri, 22 Jul 2022 16:34:13 +0000 Subject: [PATCH 17/48] points cells can not be even --- tilings/tiling.py | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/tilings/tiling.py b/tilings/tiling.py index 77eb81fa..f1fc499e 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -263,6 +263,10 @@ def _simplify_griddedperms(self, already_minimized_obs=False) -> None: all(GriddedPerm.point_perm(cell) in GPR.obstructions for cell in ass.cells) for ass in self.predicate_assumptions if isinstance(ass, OddCountAssumption) + ) or any( + next(iter(ass.cells)) in self.point_cells + for ass in self.predicate_assumptions + if isinstance(ass, EvenCountAssumption) and len(ass) == 1 ): self.set_empty() else: From 19a5d05bdb8ed925b667b603d086e72ee2ad71d1 Mon Sep 17 00:00:00 2001 From: Jay Pantone Date: Fri, 22 Jul 2022 11:40:13 -0500 Subject: [PATCH 18/48] creates requirements covering odd cells --- tilings/tiling.py | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/tilings/tiling.py b/tilings/tiling.py index f1fc499e..442ead5b 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -130,6 +130,20 @@ def __init__( """ self._cached_properties: CachedProperties = {} + reqs = list(requirements) + assumptions = list(assumptions) + for ass in assumptions: + if isinstance(ass, OddCountAssumption): + to_add = tuple(map(GriddedPerm.point_perm, ass.cells)) + if to_add not in requirements: + reqs.append(to_add) + sorted_input = False + simplify = True + derive_empty = True + remove_empty_rows_and_cols = True + + requirements = reqs + super().__init__() if sorted_input: # Set of obstructions From 27e01a4da5929a78b3893e1bd668d6f9b17898e9 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Fri, 22 Jul 2022 22:29:47 +0000 Subject: [PATCH 19/48] more accurate shifts --- tilings/assumptions.py | 4 ++-- tilings/strategies/factor.py | 23 ++++++++++++++++++++++ tilings/strategies/predicate_refinement.py | 3 ++- 3 files changed, 27 insertions(+), 3 deletions(-) diff --git a/tilings/assumptions.py b/tilings/assumptions.py index 7fcf5351..d0bc83f2 100644 --- a/tilings/assumptions.py +++ b/tilings/assumptions.py @@ -317,7 +317,7 @@ def refinements(self) -> Iterator[Tuple[CountAssumption, ...]]: Yield tuples of single cell Odd/Even CountAssumption that combine to match the parity. """ - yield from self.helper_refinements(list(self.cells), True) + yield from self.helper_refinements(sorted(self.cells), True) @staticmethod def helper_refinements( @@ -355,7 +355,7 @@ def refinements(self) -> Iterator[Tuple[CountAssumption, ...]]: Yield tuples of single cell Odd/Even CountAssumption that combine to match the parity. """ - yield from OddCountAssumption.helper_refinements(list(self.cells), False) + yield from OddCountAssumption.helper_refinements(sorted(self.cells), False) def __str__(self) -> str: return f"even number of points in cells {self.cells}" diff --git a/tilings/strategies/factor.py b/tilings/strategies/factor.py index 5ffa0543..ae89982d 100644 --- a/tilings/strategies/factor.py +++ b/tilings/strategies/factor.py @@ -81,6 +81,29 @@ def __init__( def decomposition_function(self, comb_class: Tiling) -> Tuple[Tiling, ...]: return tuple(comb_class.sub_tiling(cells) for cells in self.partition) + def shifts( + self, comb_class: Tiling, children: Optional[Tuple[Tiling, ...]] = None + ) -> Tuple[int, ...]: + if children is None: + children = self.decomposition_function(comb_class) + if children is None: + raise StrategyDoesNotApply("Strategy does not apply") + min_points = [] + for child in children: + try: + min_point = len( + next( + child.gridded_perms( + child.maximum_length_of_minimum_gridded_perm() + 4 + ) + ) + ) + except StopIteration: + min_point = child.minimum_size_of_object() + min_points.append(min_point) + point_sum = sum(min_points) + return tuple(point_sum - mpoint for mpoint in min_points) + def extra_parameters( self, comb_class: Tiling, children: Optional[Tuple[Tiling, ...]] = None ) -> Tuple[Dict[str, str], ...]: diff --git a/tilings/strategies/predicate_refinement.py b/tilings/strategies/predicate_refinement.py index b649920f..636d26b8 100644 --- a/tilings/strategies/predicate_refinement.py +++ b/tilings/strategies/predicate_refinement.py @@ -63,8 +63,9 @@ def extra_parameters( { comb_class.get_assumption_parameter( ass - ): child.get_assumption_parameter(ass) + ): child.get_assumption_parameter(child.forward_map.map_assumption(ass)) for ass in comb_class.tracking_assumptions + if child.forward_map.map_assumption(ass).gps } for child in children ) From 1377acc52edd928bd5ea14474e5d707302920e48 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Mon, 25 Jul 2022 15:26:52 +0000 Subject: [PATCH 20/48] reset cached properties --- tilings/tiling.py | 1 + 1 file changed, 1 insertion(+) diff --git a/tilings/tiling.py b/tilings/tiling.py index 442ead5b..a1f1afb8 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -286,6 +286,7 @@ def _simplify_griddedperms(self, already_minimized_obs=False) -> None: else: self._obstructions = GPR.obstructions self._requirements = GPR.requirements + self._cached_properties = {} def _remove_empty_rows_and_cols(self) -> None: """Remove empty rows and columns.""" From a985f26ee2d7881c08e16250a569230a785eb28e Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Mon, 25 Jul 2022 16:47:42 +0000 Subject: [PATCH 21/48] check if empty before and after simplify --- tilings/tiling.py | 29 ++++++++++++++++++++--------- 1 file changed, 20 insertions(+), 9 deletions(-) diff --git a/tilings/tiling.py b/tilings/tiling.py index a1f1afb8..1360c5aa 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -235,6 +235,10 @@ def _prepare_properties(self) -> None: cell for cell in product(range(dimensions[0]), range(dimensions[1])) if cell not in active_cells + ) + tuple( + gp.pos[0] + for gp in self.obstructions + if len(gp) == 1 and gp.pos[0] in active_cells ) # If the first obstruction is the empty perm, we shouldn't do any of this. @@ -266,27 +270,34 @@ def _simplify_griddedperms(self, already_minimized_obs=False) -> None: respective lists. If any requirement list is empty, then the tiling is empty. """ - + if self._predicates_imply_empty(): + self.set_empty() + return + else: + self._cached_properties = {} GPR = GriddedPermReduction( self.obstructions, self.requirements, sorted_input=True, already_minimized_obs=already_minimized_obs, ) - if any( - all(GriddedPerm.point_perm(cell) in GPR.obstructions for cell in ass.cells) + self._obstructions = GPR.obstructions + self._requirements = GPR.requirements + if self._predicates_imply_empty(): + self.set_empty() + else: + self._cached_properties = {} + + def _predicates_imply_empty(self) -> bool: + return any( + all(cell in self.empty_cells for cell in ass.cells) for ass in self.predicate_assumptions if isinstance(ass, OddCountAssumption) ) or any( next(iter(ass.cells)) in self.point_cells for ass in self.predicate_assumptions if isinstance(ass, EvenCountAssumption) and len(ass) == 1 - ): - self.set_empty() - else: - self._obstructions = GPR.obstructions - self._requirements = GPR.requirements - self._cached_properties = {} + ) def _remove_empty_rows_and_cols(self) -> None: """Remove empty rows and columns.""" From 2efa45c270ebc9c03c693883aa4ebeca819f2986 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Mon, 25 Jul 2022 16:54:34 +0000 Subject: [PATCH 22/48] check preds after clean assumptions --- tilings/tiling.py | 29 ++++++++++++++--------------- 1 file changed, 14 insertions(+), 15 deletions(-) diff --git a/tilings/tiling.py b/tilings/tiling.py index 1360c5aa..05851b99 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -168,16 +168,17 @@ def __init__( # Remove gridded perms that avoid obstructions from assumptions if simplify: self.clean_assumptions() - - # Fill empty - if derive_empty: - if "empty_cells" not in self._cached_properties: - self._prepare_properties() - - # Remove empty rows and empty columns - if remove_empty_rows_and_cols: - self._remove_empty_rows_and_cols() - # TODO: check predicates and set_empty if relevant + if self._predicates_imply_empty(): + self.set_empty() + else: + # Fill empty + if derive_empty: + if "empty_cells" not in self._cached_properties: + self._prepare_properties() + + # Remove empty rows and empty columns + if remove_empty_rows_and_cols: + self._remove_empty_rows_and_cols() else: self.set_empty() @@ -273,8 +274,6 @@ def _simplify_griddedperms(self, already_minimized_obs=False) -> None: if self._predicates_imply_empty(): self.set_empty() return - else: - self._cached_properties = {} GPR = GriddedPermReduction( self.obstructions, self.requirements, @@ -285,11 +284,9 @@ def _simplify_griddedperms(self, already_minimized_obs=False) -> None: self._requirements = GPR.requirements if self._predicates_imply_empty(): self.set_empty() - else: - self._cached_properties = {} def _predicates_imply_empty(self) -> bool: - return any( + res = any( all(cell in self.empty_cells for cell in ass.cells) for ass in self.predicate_assumptions if isinstance(ass, OddCountAssumption) @@ -298,6 +295,8 @@ def _predicates_imply_empty(self) -> bool: for ass in self.predicate_assumptions if isinstance(ass, EvenCountAssumption) and len(ass) == 1 ) + self._cached_properties = {} + return res def _remove_empty_rows_and_cols(self) -> None: """Remove empty rows and columns.""" From 43b7340fcb194ef8029833ae455d77e4fa4bf59e Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Mon, 25 Jul 2022 17:05:31 +0000 Subject: [PATCH 23/48] is reversible in Factor class --- tilings/strategies/factor.py | 18 +++++++++--------- tilings/tiling.py | 1 + 2 files changed, 10 insertions(+), 9 deletions(-) diff --git a/tilings/strategies/factor.py b/tilings/strategies/factor.py index ae89982d..0031ccd7 100644 --- a/tilings/strategies/factor.py +++ b/tilings/strategies/factor.py @@ -81,6 +81,15 @@ def __init__( def decomposition_function(self, comb_class: Tiling) -> Tuple[Tiling, ...]: return tuple(comb_class.sub_tiling(cells) for cells in self.partition) + def is_two_way(self, comb_class: Tiling) -> bool: # type: ignore + return self.is_reversible(comb_class) + + def is_reversible(self, comb_class: Tiling) -> bool: # type: ignore + return ( + not bool(self.assumptions_to_add(comb_class)) + and not comb_class.experimental_is_empty() + ) + def shifts( self, comb_class: Tiling, children: Optional[Tuple[Tiling, ...]] = None ) -> Tuple[int, ...]: @@ -299,15 +308,6 @@ def __repr__(self) -> str: ) return f"{self.__class__.__name__}({args})" - def is_two_way(self, comb_class: Tiling) -> bool: # type: ignore - return self.is_reversible(comb_class) - - def is_reversible(self, comb_class: Tiling) -> bool: # type: ignore - return ( - not bool(self.assumptions_to_add(comb_class)) - and not comb_class.experimental_is_empty() - ) - def formal_step(self) -> str: return "interleaving " + super().formal_step() diff --git a/tilings/tiling.py b/tilings/tiling.py index 05851b99..ccc1fb89 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -128,6 +128,7 @@ def __init__( - already_minimized_obs indicates if the obstructions are already minimized we pass this through to GriddedPermReduction """ + simplify = True # TODO: this is too strong self._cached_properties: CachedProperties = {} reqs = list(requirements) From a02faef2b5694a48118f4944d4642ccd7ebd0354 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Tue, 26 Jul 2022 19:15:27 +0000 Subject: [PATCH 24/48] split parity cells in initialiser, and refine one pred at a time --- tilings/assumptions.py | 17 +++++++++++++ tilings/strategies/factor.py | 8 +++---- tilings/strategies/predicate_refinement.py | 17 ++++++------- tilings/tiling.py | 28 ++++++++++++++++------ 4 files changed, 51 insertions(+), 19 deletions(-) diff --git a/tilings/assumptions.py b/tilings/assumptions.py index d0bc83f2..b990a58b 100644 --- a/tilings/assumptions.py +++ b/tilings/assumptions.py @@ -293,6 +293,11 @@ def can_be_satisfied(self, tiling: "Tiling") -> bool: perm on the tiling. """ + def can_be_refined(self) -> bool: + """Return True if it can be refined, i.e., refinements yields at + least one new thing.""" + return False + def refinements(self) -> Iterator[Tuple["PredicateAssumption", ...]]: """ A refinement is a tuple of Assumptions. This yields a set @@ -312,6 +317,9 @@ def can_be_satisfied(self, tiling: "Tiling") -> bool: def _gp_satisfies(self, gp: GriddedPerm) -> bool: return bool(len(gp) % 2) + def can_be_refined(self) -> bool: + return len(self) > 1 + def refinements(self) -> Iterator[Tuple[CountAssumption, ...]]: """ Yield tuples of single cell Odd/Even CountAssumption that @@ -350,6 +358,9 @@ def can_be_satisfied(self, tiling: "Tiling") -> bool: def _gp_satisfies(self, gp: GriddedPerm) -> bool: return not bool(len(gp) % 2) + def can_be_refined(self) -> bool: + return len(self) > 1 + def refinements(self) -> Iterator[Tuple[CountAssumption, ...]]: """ Yield tuples of single cell Odd/Even CountAssumption that @@ -375,6 +386,9 @@ def satisfies(self, gp: GriddedPerm) -> bool: def _gp_satisfies(self, gp: GriddedPerm) -> bool: raise NotImplementedError + def can_be_refined(self) -> bool: + return len(self) > 1 + def refinements(self) -> Iterator[Tuple["EqualParityAssumption", ...]]: yield tuple(EqualParityAssumption.from_cells([cell]) for cell in self.cells) @@ -396,6 +410,9 @@ def satisfies(self, gp: GriddedPerm) -> bool: def _gp_satisfies(self, gp: GriddedPerm) -> bool: raise NotImplementedError + def can_be_refined(self) -> bool: + return len(self) > 1 + def refinements(self) -> Iterator[Tuple["OppositeParityAssumption", ...]]: yield tuple(OppositeParityAssumption.from_cells([cell]) for cell in self.cells) diff --git a/tilings/strategies/factor.py b/tilings/strategies/factor.py index 0031ccd7..3067fdb3 100644 --- a/tilings/strategies/factor.py +++ b/tilings/strategies/factor.py @@ -85,10 +85,7 @@ def is_two_way(self, comb_class: Tiling) -> bool: # type: ignore return self.is_reversible(comb_class) def is_reversible(self, comb_class: Tiling) -> bool: # type: ignore - return ( - not bool(self.assumptions_to_add(comb_class)) - and not comb_class.experimental_is_empty() - ) + return not comb_class.experimental_is_empty() def shifts( self, comb_class: Tiling, children: Optional[Tuple[Tiling, ...]] = None @@ -308,6 +305,9 @@ def __repr__(self) -> str: ) return f"{self.__class__.__name__}({args})" + def is_reversible(self, comb_class: Tiling) -> bool: # type: ignore + return not bool(self.assumptions_to_add(comb_class)) + def formal_step(self) -> str: return "interleaving " + super().formal_step() diff --git a/tilings/strategies/predicate_refinement.py b/tilings/strategies/predicate_refinement.py index 636d26b8..9da9cc24 100644 --- a/tilings/strategies/predicate_refinement.py +++ b/tilings/strategies/predicate_refinement.py @@ -4,6 +4,7 @@ from comb_spec_searcher import DisjointUnionStrategy from comb_spec_searcher.exception import StrategyDoesNotApply from tilings import GriddedPerm, Tiling +from tilings.assumptions import EvenCountAssumption, OddCountAssumption class RefinePredicatesStrategy(DisjointUnionStrategy[Tiling, GriddedPerm]): @@ -17,17 +18,17 @@ def __init__( super().__init__(ignore_parent, inferrable, possibly_empty, workable) def decomposition_function(self, comb_class: Tiling) -> Tuple[Tiling, ...]: - if comb_class.predicate_assumptions: - without_predicates = comb_class.remove_assumptions().add_assumptions( - comb_class.tracking_assumptions + try: + assumption_to_refine = next( + ass for ass in comb_class.predicate_assumptions if ass.can_be_refined() ) + without_predicate = comb_class.remove_assumption(assumption_to_refine) children = [] - for assumptions in product( - *[ass.refinements() for ass in comb_class.predicate_assumptions] - ): - children.append(without_predicates.add_assumptions(chain(*assumptions))) + for assumptions in assumption_to_refine.refinements(): + children.append(without_predicate.add_assumptions(assumptions)) return tuple(children) - raise StrategyDoesNotApply + except StopIteration: + raise StrategyDoesNotApply def formal_step(self) -> str: return "predicate refinement" diff --git a/tilings/tiling.py b/tilings/tiling.py index ccc1fb89..64d3f16e 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -151,16 +151,24 @@ def __init__( self._obstructions = tuple(obstructions) # Set of requirement lists self._requirements = tuple(tuple(r) for r in requirements) - # Set of assumptions - self._assumptions = tuple(assumptions) else: # Set of obstructions self._obstructions = tuple(sorted(obstructions)) # Set of requirement lists self._requirements = Tiling.sort_requirements(requirements) - # Set of assumptions - self._assumptions = tuple(sorted(assumptions)) - + # Set of assumptions + _assumptions: List[Assumption] = [] + for ass in assumptions: + if ( + isinstance(ass, (EqualParityAssumption, OppositeParityAssumption)) + and len(ass) > 1 + ): + _assumptions.extend( + ass.__class__.from_cells([cell]) for cell in ass.cells + ) + else: + _assumptions.append(ass) + self._assumptions = tuple(sorted(_assumptions)) # Simplify the set of obstructions and the set of requirement lists if simplify: self._simplify_griddedperms(already_minimized_obs=already_minimized_obs) @@ -707,7 +715,7 @@ def add_assumptions(self, assumptions: Iterable[Assumption]) -> "Tiling": tiling.clean_assumptions() return tiling - def remove_assumption(self, assumption: TrackingAssumption): + def remove_assumption(self, assumption: Assumption): """Returns a new tiling with assumption removed.""" try: idx = self._assumptions.index(assumption) @@ -1539,7 +1547,13 @@ def is_empty(self) -> bool: return all(False for _ in MGP.minimal_gridded_perms(yield_non_minimal=True)) def experimental_is_empty(self) -> bool: - return all(False for _ in self.gridded_perms(self.minimum_size_of_object() + 4)) + try: + return all( + False for _ in self.gridded_perms(self.minimum_size_of_object() + 4) + ) + except StopIteration: + # underlying tiling is empty + return True def is_finite(self) -> bool: """Returns True if all active cells have finite basis.""" From 022f7b0db9d42549d27ed05c6a236e5f65e5b0c6 Mon Sep 17 00:00:00 2001 From: Jay Pantone Date: Tue, 26 Jul 2022 14:57:42 -0500 Subject: [PATCH 25/48] catches corner cases --- tilings/tiling.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/tilings/tiling.py b/tilings/tiling.py index 64d3f16e..626abed2 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -296,7 +296,10 @@ def _simplify_griddedperms(self, already_minimized_obs=False) -> None: def _predicates_imply_empty(self) -> bool: res = any( - all(cell in self.empty_cells for cell in ass.cells) + all( + cell in self.empty_cells or cell not in self.active_cells + for cell in ass.cells + ) for ass in self.predicate_assumptions if isinstance(ass, OddCountAssumption) ) or any( From 7f1e990ba42f51bfac5046ea7447a7ab5fd46da8 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Wed, 27 Jul 2022 13:27:08 +0000 Subject: [PATCH 26/48] fusion constructor considers odd left better, add assumption simplifies --- tilings/strategies/fusion/constructor.py | 26 +++++++++++------------- tilings/strategies/fusion/fusion.py | 6 +++++- tilings/tiling.py | 20 ++++++++++++------ 3 files changed, 31 insertions(+), 21 deletions(-) diff --git a/tilings/strategies/fusion/constructor.py b/tilings/strategies/fusion/constructor.py index 92e7bd75..9c05713a 100644 --- a/tilings/strategies/fusion/constructor.py +++ b/tilings/strategies/fusion/constructor.py @@ -242,6 +242,12 @@ def get_equation( def reliance_profile(self, n: int, **parameters: int) -> RelianceProfile: raise NotImplementedError + def odd_even_left_right_satisfied(self, left_points: int, right_points: int): + odd_left, odd_right = self.odd_left_right + return (odd_left is None or bool(left_points % 2) == odd_left) and ( + odd_right is None or bool(right_points % 2) == odd_right + ) + def get_terms( self, parent_terms: Callable[[int], Terms], subterms: SubTerms, n: int ) -> Terms: @@ -257,21 +263,11 @@ def add_new_term( params: List[int], value: int, left_points: int, fuse_region_points: int ) -> None: """Update new terms if there is enough points on the left and right.""" - odd_left, odd_right = self.odd_left_right - if odd_left is not None: - if odd_left and left_points % 2 == 0: - return - if not odd_left and left_points % 2 == 1: - return - if odd_right is not None: - right_points = fuse_region_points - left_points - if odd_right and right_points % 2 == 0: - return - if not odd_right and right_points % 2 == 1: - return + right_points = fuse_region_points - left_points if ( min_left <= left_points - and min_right <= fuse_region_points - left_points + and min_right <= right_points + and self.odd_even_left_right_satisfied(left_points, right_points) ): new_terms[tuple(params)] += value @@ -369,7 +365,9 @@ def determine_number_of_points_in_fuse_region( for number_left_points in range(min_left_points, max_left_points + 1): for number_right_points in range(min_right_points, max_right_points + 1): both = number_left_points + number_right_points - if both < min_both_points: + if both < min_both_points or self.odd_even_left_right_satisfied( + number_left_points, number_right_points + ): continue if both > max_both_points: break diff --git a/tilings/strategies/fusion/fusion.py b/tilings/strategies/fusion/fusion.py index 1eed42e2..c7fca3d0 100644 --- a/tilings/strategies/fusion/fusion.py +++ b/tilings/strategies/fusion/fusion.py @@ -50,9 +50,13 @@ def add_new_gp( ) -> None: """Update new terms if there is enough points on the left and right.""" gp = next(unfused_gps) + right_points = fuse_region_points - left_points if ( min_left <= left_points - and min_right <= fuse_region_points - left_points + and min_right <= right_points + and self.constructor.odd_even_left_right_satisfied( + left_points, right_points + ) ): res[tuple(params)].append(gp) diff --git a/tilings/tiling.py b/tilings/tiling.py index 626abed2..6bc5abe5 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -706,16 +706,24 @@ def add_assumption(self, assumption: Assumption) -> "Tiling": def add_assumptions(self, assumptions: Iterable[Assumption]) -> "Tiling": """Returns a new tiling with the added assumptions.""" + assumptions = tuple(assumptions) + remove_empty_rows_and_cols = False + derive_empty = False + simplify = False + if any(isinstance(ass, PredicateAssumption) for ass in assumptions): + remove_empty_rows_and_cols = True + derive_empty = True + simplify = True tiling = Tiling( self._obstructions, self._requirements, - self._assumptions + tuple(assumptions), - remove_empty_rows_and_cols=False, - derive_empty=False, - simplify=False, - sorted_input=True, + self._assumptions + assumptions, + remove_empty_rows_and_cols=remove_empty_rows_and_cols, + derive_empty=derive_empty, + simplify=simplify, ) - tiling.clean_assumptions() + if not simplify: + tiling.clean_assumptions() return tiling def remove_assumption(self, assumption: Assumption): From 73e00bb70e18b79f25e567e72bf701b54a66bd5f Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Wed, 27 Jul 2022 14:11:26 +0000 Subject: [PATCH 27/48] fusion sampling --- tilings/strategies/fusion/constructor.py | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/tilings/strategies/fusion/constructor.py b/tilings/strategies/fusion/constructor.py index 9c05713a..7c9f3198 100644 --- a/tilings/strategies/fusion/constructor.py +++ b/tilings/strategies/fusion/constructor.py @@ -365,13 +365,14 @@ def determine_number_of_points_in_fuse_region( for number_left_points in range(min_left_points, max_left_points + 1): for number_right_points in range(min_right_points, max_right_points + 1): both = number_left_points + number_right_points - if both < min_both_points or self.odd_even_left_right_satisfied( - number_left_points, number_right_points - ): + if both < min_both_points: continue if both > max_both_points: break - yield number_left_points, number_right_points + if self.odd_even_left_right_satisfied( + number_left_points, number_right_points + ): + yield number_left_points, number_right_points def _min_max_points_by_fuse_parameters( self, n: int, **parameters: int From 20005d9b372c48663f9b0a6033a35b48a69907c5 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Wed, 27 Jul 2022 14:37:40 +0000 Subject: [PATCH 28/48] maps in pred refinement --- tilings/strategies/predicate_refinement.py | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/tilings/strategies/predicate_refinement.py b/tilings/strategies/predicate_refinement.py index 9da9cc24..db0af61d 100644 --- a/tilings/strategies/predicate_refinement.py +++ b/tilings/strategies/predicate_refinement.py @@ -1,5 +1,5 @@ from itertools import chain, product -from typing import Dict, Iterator, Optional, Tuple +from typing import Dict, Iterator, List, Optional, Tuple, cast from comb_spec_searcher import DisjointUnionStrategy from comb_spec_searcher.exception import StrategyDoesNotApply @@ -41,7 +41,8 @@ def backward_map( ) -> Iterator[GriddedPerm]: if children is None: children = self.decomposition_function(comb_class) - raise NotImplementedError + idx = DisjointUnionStrategy.backward_map_index(objs) + yield children[idx].backward_map.map_gp(cast(GriddedPerm, objs[idx])) def forward_map( self, @@ -51,7 +52,15 @@ def forward_map( ) -> Tuple[Optional[GriddedPerm], ...]: if children is None: children = self.decomposition_function(comb_class) - raise NotImplementedError + res: List[Optional[GriddedPerm]] = [] + for child in children: + if child.forward_map.is_mappable_gp(obj): + gp = child.forward_map.map_gp(obj) + if all(ass.satisfies(gp) for ass in child.predicate_assumptions): + res.append(gp) + continue + res.append(None) + return tuple(res) def extra_parameters( self, From 9d730609896d690bc808487fe5db31924abaf1a8 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Wed, 27 Jul 2022 15:02:30 +0000 Subject: [PATCH 29/48] tidy code, add debug setting in tiling.py --- tilings/algorithms/factor.py | 4 +- tilings/assumptions.py | 2 + tilings/strategies/predicate_refinement.py | 6 +- tilings/tilescope.py | 3 + tilings/tiling.py | 73 +++++++++++++++------- 5 files changed, 61 insertions(+), 27 deletions(-) diff --git a/tilings/algorithms/factor.py b/tilings/algorithms/factor.py index c9b401bc..b513aa17 100644 --- a/tilings/algorithms/factor.py +++ b/tilings/algorithms/factor.py @@ -159,6 +159,8 @@ def _get_factors_obs_and_reqs( Returns a list of all the irreducible factors of the tiling. Each factor is a tuple (obstructions, requirements) """ + if self._tiling.predicate_assumptions: + raise NotImplementedError if self._factors_obs_and_reqs is not None: return self._factors_obs_and_reqs if self._tiling.is_empty(): @@ -174,7 +176,7 @@ def _get_factors_obs_and_reqs( # TODO: consider skew/sum assumptions assumptions = tuple( ass.__class__(gp for gp in ass.gps if gp.pos[0] in component) - for ass in self._tiling.assumptions + for ass in self._tiling.tracking_assumptions ) factors.append( ( diff --git a/tilings/assumptions.py b/tilings/assumptions.py index b990a58b..3ddef417 100644 --- a/tilings/assumptions.py +++ b/tilings/assumptions.py @@ -293,11 +293,13 @@ def can_be_satisfied(self, tiling: "Tiling") -> bool: perm on the tiling. """ + @abc.abstractmethod def can_be_refined(self) -> bool: """Return True if it can be refined, i.e., refinements yields at least one new thing.""" return False + @abc.abstractmethod def refinements(self) -> Iterator[Tuple["PredicateAssumption", ...]]: """ A refinement is a tuple of Assumptions. This yields a set diff --git a/tilings/strategies/predicate_refinement.py b/tilings/strategies/predicate_refinement.py index db0af61d..0948d403 100644 --- a/tilings/strategies/predicate_refinement.py +++ b/tilings/strategies/predicate_refinement.py @@ -1,10 +1,8 @@ -from itertools import chain, product from typing import Dict, Iterator, List, Optional, Tuple, cast from comb_spec_searcher import DisjointUnionStrategy from comb_spec_searcher.exception import StrategyDoesNotApply from tilings import GriddedPerm, Tiling -from tilings.assumptions import EvenCountAssumption, OddCountAssumption class RefinePredicatesStrategy(DisjointUnionStrategy[Tiling, GriddedPerm]): @@ -27,8 +25,8 @@ def decomposition_function(self, comb_class: Tiling) -> Tuple[Tiling, ...]: for assumptions in assumption_to_refine.refinements(): children.append(without_predicate.add_assumptions(assumptions)) return tuple(children) - except StopIteration: - raise StrategyDoesNotApply + except StopIteration as e: + raise StrategyDoesNotApply from e def formal_step(self) -> str: return "predicate refinement" diff --git a/tilings/tilescope.py b/tilings/tilescope.py index 91a0a48b..cfad62be 100644 --- a/tilings/tilescope.py +++ b/tilings/tilescope.py @@ -34,6 +34,7 @@ ) from tilings.strategies.predicate_refinement import RefinePredicatesStrategy from tilings.strategy_pack import TileScopePack +from tilings.tiling import set_debug __all__ = ("TileScope", "TileScopePack", "LimitedAssumptionTileScope", "GuidedSearcher") @@ -53,6 +54,8 @@ def __init__( debug: bool = False, ) -> None: """Initialise TileScope.""" + if debug: + set_debug() start_tiling, basis = self.get_start_tiling(start_class) if start_tiling.dimensions == (1, 1): diff --git a/tilings/tiling.py b/tilings/tiling.py index 6bc5abe5..ffda9339 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -64,6 +64,14 @@ __all__ = ["Tiling"] +DEBUG = False + + +def set_debug(debug: bool = True): + # pylint: disable=global-statement + global DEBUG + DEBUG = debug + Cell = Tuple[int, int] ReqList = Tuple[GriddedPerm, ...] @@ -119,6 +127,7 @@ def __init__( simplify: bool = True, sorted_input: bool = False, already_minimized_obs: bool = False, + checked: bool = False, ) -> None: """ - if remove_empty_rows_and_cols, then remove empty rows and columns. @@ -128,7 +137,6 @@ def __init__( - already_minimized_obs indicates if the obstructions are already minimized we pass this through to GriddedPermReduction """ - simplify = True # TODO: this is too strong self._cached_properties: CachedProperties = {} reqs = list(requirements) @@ -145,7 +153,39 @@ def __init__( requirements = reqs - super().__init__() + self._set_obstructions_requirements_and_assumptions( + obstructions, requirements, assumptions, sorted_input + ) + # Simplify the set of obstructions and the set of requirement lists + if simplify: + self._simplify_griddedperms(already_minimized_obs=already_minimized_obs) + + if not any(ob.is_empty() for ob in self.obstructions): + # Remove gridded perms that avoid obstructions from assumptions + if simplify: + self.clean_assumptions() + if self._predicates_imply_empty(): + self.set_empty() + else: + # Fill empty + if derive_empty: + if "empty_cells" not in self._cached_properties: + self._prepare_properties() + + # Remove empty rows and empty columns + if remove_empty_rows_and_cols: + self._remove_empty_rows_and_cols() + else: + self.set_empty() + self._check_init(checked) + + def _set_obstructions_requirements_and_assumptions( + self, + obstructions: Iterable[GriddedPerm], + requirements: Iterable[Iterable[GriddedPerm]], + assumptions: Iterable[Assumption], + sorted_input: bool, + ): if sorted_input: # Set of obstructions self._obstructions = tuple(obstructions) @@ -169,27 +209,16 @@ def __init__( else: _assumptions.append(ass) self._assumptions = tuple(sorted(_assumptions)) - # Simplify the set of obstructions and the set of requirement lists - if simplify: - self._simplify_griddedperms(already_minimized_obs=already_minimized_obs) - - if not any(ob.is_empty() for ob in self.obstructions): - # Remove gridded perms that avoid obstructions from assumptions - if simplify: - self.clean_assumptions() - if self._predicates_imply_empty(): - self.set_empty() - else: - # Fill empty - if derive_empty: - if "empty_cells" not in self._cached_properties: - self._prepare_properties() - # Remove empty rows and empty columns - if remove_empty_rows_and_cols: - self._remove_empty_rows_and_cols() - else: - self.set_empty() + def _check_init(self, checked: bool): + if DEBUG and not checked: + redone = Tiling( + self._obstructions, self._requirements, self._assumptions, checked=True + ) + if redone != self: + print(self) + print(redone) + assert 0 def set_empty(self): self._obstructions = (GriddedPerm.empty_perm(),) From 65cb3f59860f7a81d554b580036536da5ad65aa9 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Wed, 27 Jul 2022 17:00:07 +0000 Subject: [PATCH 30/48] possibly empty has to be set since our is empty check is not perfect --- tilings/strategies/factor.py | 5 ++++- tilings/strategies/requirement_placement.py | 4 ++-- tilings/strategies/row_and_col_separation.py | 2 +- 3 files changed, 7 insertions(+), 4 deletions(-) diff --git a/tilings/strategies/factor.py b/tilings/strategies/factor.py index 3067fdb3..921e2c8c 100644 --- a/tilings/strategies/factor.py +++ b/tilings/strategies/factor.py @@ -75,7 +75,10 @@ def __init__( FactorWithInterleavingStrategy.interleaving_rows_and_cols(self.partition) ) super().__init__( - ignore_parent=ignore_parent, workable=workable, inferrable=inferrable + ignore_parent=ignore_parent, + workable=workable, + inferrable=inferrable, + possibly_empty=True, ) def decomposition_function(self, comb_class: Tiling) -> Tuple[Tiling, ...]: diff --git a/tilings/strategies/requirement_placement.py b/tilings/strategies/requirement_placement.py index 67d80ff6..2dba00c4 100644 --- a/tilings/strategies/requirement_placement.py +++ b/tilings/strategies/requirement_placement.py @@ -56,8 +56,8 @@ def __init__( self._placed_cells = tuple( sorted(set(gp.pos[idx] for idx, gp in zip(self.indices, self.gps))) ) - possibly_empty = self.include_empty or len(self.gps) > 1 - super().__init__(ignore_parent=ignore_parent, possibly_empty=possibly_empty) + # possibly_empty = self.include_empty or len(self.gps) > 1 + super().__init__(ignore_parent=ignore_parent, possibly_empty=True) def _placed_cell(self, idx: int) -> Cell: """Return the cell placed given the index of the child.""" diff --git a/tilings/strategies/row_and_col_separation.py b/tilings/strategies/row_and_col_separation.py index fcec91cd..5a99cddf 100644 --- a/tilings/strategies/row_and_col_separation.py +++ b/tilings/strategies/row_and_col_separation.py @@ -26,7 +26,7 @@ class RowColumnSeparationStrategy(DisjointUnionStrategy[Tiling, GriddedPerm]): def __init__(self): super().__init__( - ignore_parent=True, inferrable=True, possibly_empty=False, workable=True + ignore_parent=True, inferrable=True, possibly_empty=True, workable=True ) def forward_cell_map(self, tiling: Tiling) -> CellMap: From b81aa85cbcc8458651f1dca1b65981e5e4c51991 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Wed, 27 Jul 2022 19:43:19 +0000 Subject: [PATCH 31/48] obsinferral is possibly empty; --- tilings/strategies/obstruction_inferral.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tilings/strategies/obstruction_inferral.py b/tilings/strategies/obstruction_inferral.py index 491a1b18..35020ce9 100644 --- a/tilings/strategies/obstruction_inferral.py +++ b/tilings/strategies/obstruction_inferral.py @@ -21,7 +21,7 @@ class ObstructionInferralStrategy(DisjointUnionStrategy[Tiling, GriddedPerm]): def __init__(self, gps: Iterable[GriddedPerm]): self.gps = tuple(sorted(gps)) super().__init__( - ignore_parent=True, inferrable=True, possibly_empty=False, workable=True + ignore_parent=True, inferrable=True, possibly_empty=True, workable=True ) def decomposition_function(self, comb_class: Tiling) -> Tuple[Tiling]: From c7c5729d2501f2f78f1d77b6de4f4342273cba51 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Thu, 28 Jul 2022 16:06:13 +0000 Subject: [PATCH 32/48] a local expansion in is empty --- tilings/algorithms/factor.py | 8 ++++++- tilings/tiling.py | 43 ++++++++++++++++++++++++++++++++++-- 2 files changed, 48 insertions(+), 3 deletions(-) diff --git a/tilings/algorithms/factor.py b/tilings/algorithms/factor.py index b513aa17..34777c29 100644 --- a/tilings/algorithms/factor.py +++ b/tilings/algorithms/factor.py @@ -4,7 +4,11 @@ from permuta.misc import UnionFind from tilings import GriddedPerm -from tilings.assumptions import ComponentAssumption, TrackingAssumption +from tilings.assumptions import ( + ComponentAssumption, + PredicateAssumption, + TrackingAssumption, +) from tilings.misc import partitions_iterator if TYPE_CHECKING: @@ -84,6 +88,8 @@ def _unite_assumptions(self) -> None: if isinstance(assumption, ComponentAssumption): for cells in assumption.cell_decomposition(self._tiling): self._unite_cells(cells) + elif isinstance(assumption, PredicateAssumption): + self._unite_cells(assumption.cells) else: for gp in assumption.gps: self._unite_cells(gp.pos) diff --git a/tilings/tiling.py b/tilings/tiling.py index ffda9339..109aa0db 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -1243,6 +1243,8 @@ def find_factors(self, interleaving: str = "none") -> Tuple["Tiling", ...]: set 'all' then cells on the same row or columns don't need to be in the same factor. """ + if any(len(ass) > 1 for ass in self.predicate_assumptions): + return (self,) factor_class = { "none": Factor, "monotone": FactorWithMonotoneInterleaving, @@ -1254,7 +1256,9 @@ def find_factors(self, interleaving: str = "none") -> Tuple["Tiling", ...]: raise InvalidOperationError( f"interleaving option must be in {list(factor_class.keys())}" ) - return factor.factors() + return tuple( + self.sub_tiling(component) for component in factor.get_components() + ) def row_and_column_separation(self) -> "Tiling": """ @@ -1584,7 +1588,42 @@ def is_empty(self) -> bool: if len(self.requirements) <= 1: return False MGP = MinimalGriddedPerms(self.obstructions, self.requirements) - return all(False for _ in MGP.minimal_gridded_perms(yield_non_minimal=True)) + if all(False for _ in MGP.minimal_gridded_perms(yield_non_minimal=True)): + return True + factors = self.find_factors() + if len(factors) > 1: + return any(f.is_empty() for f in factors) + + rcs = self.row_and_column_separation() + if rcs != self: + return rcs.is_empty() + + try: + assumption_to_refine = next( + ass for ass in self.predicate_assumptions if ass.can_be_refined() + ) + without_predicate = self.remove_assumption(assumption_to_refine) + return all( + without_predicate.add_assumptions(assumptions).is_empty() + for assumptions in assumption_to_refine.refinements() + ) + except StopIteration: + # nothing can be refined + pass + + for ass in self._assumptions: + GPR = GriddedPermReduction( + tuple(), self._requirements, manual=True, sorted_input=True + ) + if isinstance(ass, OddCountAssumption): + to_add = tuple(map(GriddedPerm.point_perm, ass.cells)) + if not GPR._requirement_implied_by_some_requirement( + to_add, self._requirements + ): + return self.add_list_requirement(to_add).is_empty() + # if self.experimental_is_empty(): + # print(self) + return False def experimental_is_empty(self) -> bool: try: From 31b6ea5d8ea1406347656547a02657fcfbfb1cc4 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Thu, 28 Jul 2022 18:22:24 +0000 Subject: [PATCH 33/48] a smarter predicates imply empty method (#493) * a smarter predicates imply empty method * remove req skip in new empty check * tidying code --- tilings/algorithms/gridded_perm_reduction.py | 4 +- tilings/tiling.py | 189 +++++++++++++++---- 2 files changed, 159 insertions(+), 34 deletions(-) diff --git a/tilings/algorithms/gridded_perm_reduction.py b/tilings/algorithms/gridded_perm_reduction.py index 990b0f6e..0a6edb5f 100644 --- a/tilings/algorithms/gridded_perm_reduction.py +++ b/tilings/algorithms/gridded_perm_reduction.py @@ -162,7 +162,7 @@ def remove_redundant(self, requirements: List[Requirement]) -> List[Requirement] for idx, requirement in enumerate(requirements): if not all(requirement): continue - if self._requirement_implied_by_some_requirement( + if self.requirement_implied_by_some_requirement( requirement, chain( islice(requirements, idx), @@ -306,7 +306,7 @@ def _griddedperm_implied_by_some_requirement( for requirement in requirements ) - def _requirement_implied_by_some_requirement( + def requirement_implied_by_some_requirement( self, requirement: Requirement, requirements: Iterable[Requirement], diff --git a/tilings/tiling.py b/tilings/tiling.py index 109aa0db..cc426cd1 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -2,7 +2,7 @@ import json from array import array from collections import Counter, defaultdict -from functools import reduce +from functools import lru_cache, reduce from itertools import chain, filterfalse, product from operator import mul, xor from typing import ( @@ -139,20 +139,6 @@ def __init__( """ self._cached_properties: CachedProperties = {} - reqs = list(requirements) - assumptions = list(assumptions) - for ass in assumptions: - if isinstance(ass, OddCountAssumption): - to_add = tuple(map(GriddedPerm.point_perm, ass.cells)) - if to_add not in requirements: - reqs.append(to_add) - sorted_input = False - simplify = True - derive_empty = True - remove_empty_rows_and_cols = True - - requirements = reqs - self._set_obstructions_requirements_and_assumptions( obstructions, requirements, assumptions, sorted_input ) @@ -177,6 +163,7 @@ def __init__( self._remove_empty_rows_and_cols() else: self.set_empty() + self._check_init(checked) def _set_obstructions_requirements_and_assumptions( @@ -309,9 +296,6 @@ def _simplify_griddedperms(self, already_minimized_obs=False) -> None: respective lists. If any requirement list is empty, then the tiling is empty. """ - if self._predicates_imply_empty(): - self.set_empty() - return GPR = GriddedPermReduction( self.obstructions, self.requirements, @@ -324,21 +308,160 @@ def _simplify_griddedperms(self, already_minimized_obs=False) -> None: self.set_empty() def _predicates_imply_empty(self) -> bool: - res = any( - all( - cell in self.empty_cells or cell not in self.active_cells - for cell in ass.cells + res = ( + any( + all( + cell in self.empty_cells or cell not in self.active_cells + for cell in ass.cells + ) + for ass in self.predicate_assumptions + if isinstance(ass, OddCountAssumption) + ) + or any( + next(iter(ass.cells)) in self.point_cells + for ass in self.predicate_assumptions + if isinstance(ass, EvenCountAssumption) and len(ass) == 1 ) - for ass in self.predicate_assumptions - if isinstance(ass, OddCountAssumption) - ) or any( - next(iter(ass.cells)) in self.point_cells - for ass in self.predicate_assumptions - if isinstance(ass, EvenCountAssumption) and len(ass) == 1 + or self._rectangular_predicate_implications() ) self._cached_properties = {} return res + def _rectangular_predicate_implications(self) -> bool: + predicates = self.predicate_assumptions + if not predicates or any(len(pred) > 1 for pred in predicates): + return False + + def _get_cells(predicate_type): + return set( + chain.from_iterable( + pred.cells + for pred in predicates + if isinstance(pred, predicate_type) + ) + ) + + odd_cells = _get_cells(OddCountAssumption) + even_cells = _get_cells(EvenCountAssumption) + if odd_cells.intersection(even_cells): + return True + if odd_cells.union(even_cells) != set(self.active_cells): + return False + equal_cells = _get_cells(EqualParityAssumption) + opposite_cells = _get_cells(OppositeParityAssumption) + if equal_cells.intersection(opposite_cells): + return True + if equal_cells.union(opposite_cells) != set(self.active_cells): + return False + return any( + self._contradictory_rectangle( + rectangle, odd_cells, even_cells, opposite_cells, equal_cells + ) + for rectangle in self._get_rectangular_regions() + ) + + def _contradictory_rectangle( + self, + rectangle: Set[Cell], + odd_cells: Set[Cell], + even_cells: Set[Cell], + opposite_cells: Set[Cell], + equal_cells: Set[Cell], + ) -> bool: + odd = bool(sum(1 for cell in rectangle if cell in odd_cells) % 2) + mindex = min(x for x, _ in rectangle) + minval = min(y for _, y in rectangle) + toggle = bool( + ( + sum(1 for x, _ in odd_cells if x < mindex) + + sum(1 for _, y in odd_cells if y < minval) + ) + % 2 + ) + # opposite parity => even length + if (not toggle and all(cell in opposite_cells for cell in rectangle)) or ( + toggle and all(cell in equal_cells for cell in rectangle) + ): + if odd: + return True + if len(rectangle) == 1: + cell = next(iter(rectangle)) + basis = self.cell_basis()[cell][0] + if Perm((0, 1)) in basis: + # equal parity implies odd size or size 0 + if cell in self.positive_cells: + if (toggle and cell in opposite_cells) or ( + not toggle and cell in equal_cells + ): + if cell in even_cells: + return True + # TODO: this implies that the cell is empty. add ob? + if Perm((1, 0)) in basis: + # equal parity unless size 0 + if cell in self.positive_cells: + if (not toggle and cell in opposite_cells) or ( + toggle and cell in equal_cells + ): + return True + return False + + def _get_rectangular_regions(self) -> Iterator[Set[Cell]]: + """ + Yield rectangular regions which do not interleave with + other cells in its cols or rows outside of the region. + """ + to_process = set(self.active_cells) + rectangle_by_cells: Dict[Cell, Set[Cell]] = {} + filled_rectangles: List[Set[Cell]] = [] + while to_process: + rectangle: Set[Cell] = set() + cells_to_process = set([to_process.pop()]) + processed_rows: Set[int] = set() + processed_cols: Set[int] = set() + while cells_to_process: + cell = cells_to_process.pop() + if cell[0] not in processed_cols: + processed_cols.add(cell[0]) + cells = self.cells_in_col(cell[0]) + rectangle.update(cells) + cells_to_process.update(cells) + if cell[1] not in processed_rows: + processed_rows.add(cell[1]) + cells = self.cells_in_row(cell[1]) + rectangle.update(cells) + cells_to_process.update(cells) + to_process -= rectangle + filled_in_rectangle = self._fill_rectangle(rectangle) + for cell in rectangle: + rectangle_by_cells[cell] = filled_in_rectangle + filled_rectangles.append(filled_in_rectangle) + for filled_rectangle in filled_rectangles: + res = filled_rectangle + old_res: Optional[Set[Cell]] = None + while old_res != res: + old_res = res + res = self._fill_rectangle( + union_reduce((rectangle_by_cells[cell] for cell in res)) + ) + yield res + # TODO: consider the unions of the above? + + def _fill_rectangle(self, rectangle: Set[Cell]) -> Set[Cell]: + """ + Return the smallest rectangular region that contains all of + the cells and does not interleave with any cell in its rows + or columns outside the rectangle. + """ + min_x = min(x for x, _ in rectangle) + max_x = max(x for x, _ in rectangle) + min_y = min(y for _, y in rectangle) + max_y = max(y for _, y in rectangle) + return set( + (x, y) + for (x, y) in self.active_cells + if min_x <= x <= max_x or min_y <= y <= max_y + ) + def _remove_empty_rows_and_cols(self) -> None: """Remove empty rows and columns.""" # Produce the mapping between the two tilings @@ -1571,6 +1694,7 @@ def maximum_length_of_minimum_gridded_perm(self) -> int: """ return sum(max(map(len, reqs)) for reqs in self.requirements) + @lru_cache(10000) def is_empty(self) -> bool: """Checks if the tiling is empty. @@ -1585,11 +1709,14 @@ def is_empty(self) -> bool: ): return True # return self.experimental_is_empty() - if len(self.requirements) <= 1: + if not self.predicate_assumptions and len(self.requirements) <= 1: return False MGP = MinimalGriddedPerms(self.obstructions, self.requirements) if all(False for _ in MGP.minimal_gridded_perms(yield_non_minimal=True)): return True + return self._is_empty_after_expansion() + + def _is_empty_after_expansion(self) -> bool: factors = self.find_factors() if len(factors) > 1: return any(f.is_empty() for f in factors) @@ -1617,12 +1744,10 @@ def is_empty(self) -> bool: ) if isinstance(ass, OddCountAssumption): to_add = tuple(map(GriddedPerm.point_perm, ass.cells)) - if not GPR._requirement_implied_by_some_requirement( + if not GPR.requirement_implied_by_some_requirement( to_add, self._requirements ): return self.add_list_requirement(to_add).is_empty() - # if self.experimental_is_empty(): - # print(self) return False def experimental_is_empty(self) -> bool: From 2174602f470b71ae6caa1aafcc8b9ea128bc188b Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Thu, 28 Jul 2022 21:54:43 +0000 Subject: [PATCH 34/48] add length 2 reqs in is empty call --- tilings/tiling.py | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/tilings/tiling.py b/tilings/tiling.py index cc426cd1..6e494496 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -1748,6 +1748,30 @@ def _is_empty_after_expansion(self) -> bool: to_add, self._requirements ): return self.add_list_requirement(to_add).is_empty() + if isinstance(ass, (EvenCountAssumption, OddCountAssumption)): + min_size = sum(1 for cell in ass.cells if cell in self.positive_cells) + odd = bool(min_size % 2) + if (odd and isinstance(ass, OddCountAssumption)) or ( + not odd and isinstance(ass, EvenCountAssumption) + ): + continue + min_size += 1 + tiling = Tiling( + [ + GriddedPerm.single_cell(Perm.identity(min_size + 1), cell) + for cell in ass.cells + ], + remove_empty_rows_and_cols=False, + simplify=False, + ) + reqs = tuple(tiling.objects_of_size(min_size)) + if not GPR.requirement_implied_by_some_requirement( + reqs, self._requirements + ): + return self.add_list_requirement( + tiling.objects_of_size(min_size) + ).is_empty() + return False def experimental_is_empty(self) -> bool: From 59d49b649de0e1508ed8021f97c4080e9a771f23 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Thu, 28 Jul 2022 23:51:10 +0000 Subject: [PATCH 35/48] smarter min sizes, and bound to experimental --- tilings/tiling.py | 25 +++++++++++++++++++------ 1 file changed, 19 insertions(+), 6 deletions(-) diff --git a/tilings/tiling.py b/tilings/tiling.py index 6e494496..54a7472c 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -1749,7 +1749,10 @@ def _is_empty_after_expansion(self) -> bool: ): return self.add_list_requirement(to_add).is_empty() if isinstance(ass, (EvenCountAssumption, OddCountAssumption)): - min_size = sum(1 for cell in ass.cells if cell in self.positive_cells) + min_size = sum( + min(map(len, self.cell_basis()[cell][1]), default=0) + for cell in ass.cells + ) odd = bool(min_size % 2) if (odd and isinstance(ass, OddCountAssumption)) or ( not odd and isinstance(ass, EvenCountAssumption) @@ -1768,16 +1771,26 @@ def _is_empty_after_expansion(self) -> bool: if not GPR.requirement_implied_by_some_requirement( reqs, self._requirements ): - return self.add_list_requirement( - tiling.objects_of_size(min_size) - ).is_empty() + return self.add_list_requirement(reqs).is_empty() + + # if self.experimental_is_empty(4): + # if not self.experimental_is_empty(5): + # print(self) + # print(repr(self)) + # print(5) + # elif not self.experimental_is_empty(6): + # print(self) + # print(repr(self)) + # print(6) + # else: + # return True return False - def experimental_is_empty(self) -> bool: + def experimental_is_empty(self, bound: int = 4) -> bool: try: return all( - False for _ in self.gridded_perms(self.minimum_size_of_object() + 4) + False for _ in self.gridded_perms(self.minimum_size_of_object() + bound) ) except StopIteration: # underlying tiling is empty From d472e6e44f920832ba4f6485418127c0d71366e4 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Fri, 29 Jul 2022 14:11:54 +0000 Subject: [PATCH 36/48] not implemented reverse fusion counting --- tilings/strategies/fusion/fusion.py | 2 ++ tilings/tilescope.py | 3 +-- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/tilings/strategies/fusion/fusion.py b/tilings/strategies/fusion/fusion.py index c7fca3d0..a646f9d0 100644 --- a/tilings/strategies/fusion/fusion.py +++ b/tilings/strategies/fusion/fusion.py @@ -228,6 +228,8 @@ def reverse_constructor( # pylint: disable=no-self-use if not self.tracked: # constructor only enumerates when tracked. raise NotImplementedError("The fusion strategy was not tracked.") + if comb_class.predicate_assumptions: + raise NotImplementedError("can't handle predicates") if children is None: children = self.decomposition_function(comb_class) # Need to recompute some info to count, so ignoring passed in children diff --git a/tilings/tilescope.py b/tilings/tilescope.py index cfad62be..b04e8e3a 100644 --- a/tilings/tilescope.py +++ b/tilings/tilescope.py @@ -434,8 +434,7 @@ def backward_map( ) -> Iterator[GriddedPerm]: if children is None: children = self.decomposition_function(comb_class) - gp = objs[0] - assert gp is not None + gp = next((gp for gp in objs if gp is not None)) yield gp def forward_map( From 9e6f9528de2e7cc5fb388a87f8b8210656d7973d Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Fri, 29 Jul 2022 14:20:11 +0000 Subject: [PATCH 37/48] dont check init for dummy tiling --- tilings/tiling.py | 1 + 1 file changed, 1 insertion(+) diff --git a/tilings/tiling.py b/tilings/tiling.py index 54a7472c..ffc98dd3 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -1766,6 +1766,7 @@ def _is_empty_after_expansion(self) -> bool: ], remove_empty_rows_and_cols=False, simplify=False, + checked=True, ) reqs = tuple(tiling.objects_of_size(min_size)) if not GPR.requirement_implied_by_some_requirement( From de521ae896e5969f0c9d850a5d7003e5e3b5fbe5 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Fri, 29 Jul 2022 15:10:36 +0000 Subject: [PATCH 38/48] insert mgps to satisfy odd even in is empty --- tilings/algorithms/minimal_gridded_perms.py | 39 +++++++++++ tilings/tiling.py | 77 ++++++++++----------- 2 files changed, 75 insertions(+), 41 deletions(-) diff --git a/tilings/algorithms/minimal_gridded_perms.py b/tilings/algorithms/minimal_gridded_perms.py index 0d3e87ac..8e3dc839 100644 --- a/tilings/algorithms/minimal_gridded_perms.py +++ b/tilings/algorithms/minimal_gridded_perms.py @@ -543,3 +543,42 @@ def _process_work_packet( if not yielded_subgridded_perm(gp): yielded.add(gp) yield gp + + def odd_even_minimal_gridded_perms( + self, odd_cells: Set[Cell], even_cells: Set[Cell] + ) -> Set[GriddedPerm]: + if odd_cells.intersection(even_cells): + return + + def cell_count(gp: GriddedPerm, cell: Cell) -> int: + return sum(1 for _ in filter(cell.__eq__, gp.pos)) + + def satisfies_odd_even(gp: GriddedPerm): + return all(bool(cell_count(gp, cell) % 2) for cell in odd_cells) and all( + not bool(cell_count(gp, cell) % 2) for cell in even_cells + ) + + def insert_point(gp: GriddedPerm, cell: Cell) -> Iterator[GriddedPerm]: + for _, griddedperm in self.insert_point(gp, cell, -1): + yield griddedperm + + to_process = set(self.minimal_gridded_perms()) + res: Set[GriddedPerm] = set() + while to_process: + gp = to_process.pop() + if satisfies_odd_even(gp): + res.add(gp) + insert = set() + for cell in odd_cells: + if not bool(cell_count(gp, cell) % 2): + insert.add(cell) + for cell in even_cells: + if bool(cell_count(gp, cell) % 2): + insert.add(cell) + gps = set([gp]) + while insert: + cell = insert.pop() + gps = set(chain.from_iterable(insert_point(gp, cell) for gp in gps)) + res.update(gps) + assert all(satisfies_odd_even(gp) for gp in res) + return res diff --git a/tilings/tiling.py b/tilings/tiling.py index ffc98dd3..667d452e 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -1737,52 +1737,47 @@ def _is_empty_after_expansion(self) -> bool: except StopIteration: # nothing can be refined pass - - for ass in self._assumptions: - GPR = GriddedPermReduction( - tuple(), self._requirements, manual=True, sorted_input=True + odd_cells = set( + chain.from_iterable( + ass.cells + for ass in self._assumptions + if isinstance(ass, OddCountAssumption) ) - if isinstance(ass, OddCountAssumption): - to_add = tuple(map(GriddedPerm.point_perm, ass.cells)) - if not GPR.requirement_implied_by_some_requirement( - to_add, self._requirements - ): - return self.add_list_requirement(to_add).is_empty() - if isinstance(ass, (EvenCountAssumption, OddCountAssumption)): - min_size = sum( - min(map(len, self.cell_basis()[cell][1]), default=0) - for cell in ass.cells - ) - odd = bool(min_size % 2) - if (odd and isinstance(ass, OddCountAssumption)) or ( - not odd and isinstance(ass, EvenCountAssumption) - ): - continue - min_size += 1 - tiling = Tiling( - [ - GriddedPerm.single_cell(Perm.identity(min_size + 1), cell) - for cell in ass.cells - ], - remove_empty_rows_and_cols=False, - simplify=False, - checked=True, - ) - reqs = tuple(tiling.objects_of_size(min_size)) - if not GPR.requirement_implied_by_some_requirement( - reqs, self._requirements - ): - return self.add_list_requirement(reqs).is_empty() - - # if self.experimental_is_empty(4): - # if not self.experimental_is_empty(5): + ) + even_cells = set( + chain.from_iterable( + ass.cells + for ass in self._assumptions + if isinstance(ass, EvenCountAssumption) + ) + ) + MGP = MinimalGriddedPerms(self._obstructions, self._requirements) + MGPS = MGP.odd_even_minimal_gridded_perms(odd_cells, even_cells) + tiling = self.add_list_requirement(MGPS) + if self != tiling: + return tiling.is_empty() + + # if self.experimental_is_empty(0): + # if not self.experimental_is_empty(1): + # bound = 1 + # print(self) + # print(repr(self)) + # print("+", bound, "smallest:", self.minimum_size_of_object() + bound) + # elif not self.experimental_is_empty(2): + # bound = 2 + # print(self) + # print(repr(self)) + # print("+", bound, "smallest:", self.minimum_size_of_object() + bound) + # elif not self.experimental_is_empty(3): + # bound = 3 # print(self) # print(repr(self)) - # print(5) - # elif not self.experimental_is_empty(6): + # print("+", bound, "smallest:", self.minimum_size_of_object() + bound) + # elif not self.experimental_is_empty(4): + # bound = 4 # print(self) # print(repr(self)) - # print(6) + # print("+", bound, "smallest:", self.minimum_size_of_object() + bound) # else: # return True From d09daf169b50567787c6f08d18f9182d7dd380df Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Fri, 29 Jul 2022 17:36:32 +0000 Subject: [PATCH 39/48] place points not on own row and col in is empty --- tilings/tiling.py | 86 ++++++++++++++++++++++++++++++++++------------- 1 file changed, 62 insertions(+), 24 deletions(-) diff --git a/tilings/tiling.py b/tilings/tiling.py index 667d452e..56a5b209 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -1712,16 +1712,23 @@ def is_empty(self) -> bool: if not self.predicate_assumptions and len(self.requirements) <= 1: return False MGP = MinimalGriddedPerms(self.obstructions, self.requirements) - if all(False for _ in MGP.minimal_gridded_perms(yield_non_minimal=True)): + gps = MGP.minimal_gridded_perms(yield_non_minimal=True) + try: + if self._satisfies_predicates(next(gps)): + return False + except StopIteration: return True + if any(self._satisfies_predicates(gp) for gp in gps): + return False return self._is_empty_after_expansion() def _is_empty_after_expansion(self) -> bool: + # TODO: consider doing all this as an initial factory factors = self.find_factors() if len(factors) > 1: return any(f.is_empty() for f in factors) - - rcs = self.row_and_column_separation() + rcs = self.obstruction_transitivity() + rcs = rcs.row_and_column_separation() if rcs != self: return rcs.is_empty() @@ -1757,32 +1764,63 @@ def _is_empty_after_expansion(self) -> bool: if self != tiling: return tiling.is_empty() - # if self.experimental_is_empty(0): - # if not self.experimental_is_empty(1): - # bound = 1 - # print(self) - # print(repr(self)) - # print("+", bound, "smallest:", self.minimum_size_of_object() + bound) - # elif not self.experimental_is_empty(2): - # bound = 2 - # print(self) - # print(repr(self)) - # print("+", bound, "smallest:", self.minimum_size_of_object() + bound) - # elif not self.experimental_is_empty(3): - # bound = 3 - # print(self) - # print(repr(self)) - # print("+", bound, "smallest:", self.minimum_size_of_object() + bound) - # elif not self.experimental_is_empty(4): - # bound = 4 - # print(self) - # print(repr(self)) - # print("+", bound, "smallest:", self.minimum_size_of_object() + bound) + for cell in tiling.point_cells: + if not tiling.only_cell_in_row_and_col(cell): + return self.place_point_in_cell(cell, 0).is_empty() + + # def print_bound(bound): + # print(self) + # print(repr(self)) + # print( + # "+", + # bound, + # "smallest:", + # self.maximum_length_of_minimum_gridded_perm() + bound, + # ) + # GP = GriddedPermsOnTiling(self, yield_non_minimal=True) + # for gp in filter( + # self._satisfies_predicates, + # GP.gridded_perms( + # self.maximum_length_of_minimum_gridded_perm() + bound, + # place_at_most=bound, + # ), + # ): + # print(gp) + # break + + # if self.smarter_experimental_is_empty(0): + # if not self.smarter_experimental_is_empty(1): + # print_bound(1) + # elif not self.smarter_experimental_is_empty(2): + # print_bound(2) + # elif not self.smarter_experimental_is_empty(3): + # print_bound(3) + # elif not self.smarter_experimental_is_empty(4): + # print_bound(4) + # elif not self.smarter_experimental_is_empty(5): + # print_bound(5) + # elif not self.smarter_experimental_is_empty(6): + # print_bound(6) # else: # return True + # else: + # print_bound(0) return False + def smarter_experimental_is_empty(self, bound: int = 4) -> bool: + GP = GriddedPermsOnTiling(self, yield_non_minimal=True) + return all( + False + for _ in filter( + self._satisfies_predicates, + GP.gridded_perms( + self.maximum_length_of_minimum_gridded_perm() + bound, + place_at_most=bound, + ), + ) + ) + def experimental_is_empty(self, bound: int = 4) -> bool: try: return all( From 0e617ea073831d0efe2839fa352a11afde12e488 Mon Sep 17 00:00:00 2001 From: Jay Pantone Date: Fri, 29 Jul 2022 13:49:10 -0500 Subject: [PATCH 40/48] remove point placement in is_empty and adds experimental_bound argument --- tilings/tiling.py | 23 +++++++++++++++-------- 1 file changed, 15 insertions(+), 8 deletions(-) diff --git a/tilings/tiling.py b/tilings/tiling.py index 56a5b209..6d328541 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -1722,15 +1722,17 @@ def is_empty(self) -> bool: return False return self._is_empty_after_expansion() - def _is_empty_after_expansion(self) -> bool: + def _is_empty_after_expansion( + self, experimental_bound: Optional[int] = None + ) -> bool: # TODO: consider doing all this as an initial factory factors = self.find_factors() if len(factors) > 1: - return any(f.is_empty() for f in factors) + return any(f.is_empty(experimental_bound) for f in factors) rcs = self.obstruction_transitivity() rcs = rcs.row_and_column_separation() if rcs != self: - return rcs.is_empty() + return rcs.is_empty(experimental_bound) try: assumption_to_refine = next( @@ -1738,7 +1740,9 @@ def _is_empty_after_expansion(self) -> bool: ) without_predicate = self.remove_assumption(assumption_to_refine) return all( - without_predicate.add_assumptions(assumptions).is_empty() + without_predicate.add_assumptions(assumptions).is_empty( + experimental_bound + ) for assumptions in assumption_to_refine.refinements() ) except StopIteration: @@ -1762,11 +1766,11 @@ def _is_empty_after_expansion(self) -> bool: MGPS = MGP.odd_even_minimal_gridded_perms(odd_cells, even_cells) tiling = self.add_list_requirement(MGPS) if self != tiling: - return tiling.is_empty() + return tiling.is_empty(experimental_bound) - for cell in tiling.point_cells: - if not tiling.only_cell_in_row_and_col(cell): - return self.place_point_in_cell(cell, 0).is_empty() + # for cell in tiling.point_cells: + # if not tiling.only_cell_in_row_and_col(cell): + # return self.place_point_in_cell(cell, 0).is_empty() # def print_bound(bound): # print(self) @@ -1806,6 +1810,9 @@ def _is_empty_after_expansion(self) -> bool: # else: # print_bound(0) + if experimental_bound is not None: + return self.smarter_experimental_is_empty(bound=experimental_bound) + return False def smarter_experimental_is_empty(self, bound: int = 4) -> bool: From d9ac524c3742a13d99c60ddd0d1f29f2698d20f6 Mon Sep 17 00:00:00 2001 From: Jay Pantone Date: Fri, 29 Jul 2022 21:01:25 -0500 Subject: [PATCH 41/48] fixes experimental bound flag --- tilings/tiling.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tilings/tiling.py b/tilings/tiling.py index 6d328541..bdc1b726 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -1695,7 +1695,7 @@ def maximum_length_of_minimum_gridded_perm(self) -> int: return sum(max(map(len, reqs)) for reqs in self.requirements) @lru_cache(10000) - def is_empty(self) -> bool: + def is_empty(self, experimental_bound: Optional[int] = None) -> bool: """Checks if the tiling is empty. Tiling is empty if it has been inferred to be contradictory due to @@ -1720,7 +1720,7 @@ def is_empty(self) -> bool: return True if any(self._satisfies_predicates(gp) for gp in gps): return False - return self._is_empty_after_expansion() + return self._is_empty_after_expansion(experimental_bound) def _is_empty_after_expansion( self, experimental_bound: Optional[int] = None From e1a005f92c79e31e76579f15636a55234b483004 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Wed, 25 Jan 2023 13:20:34 +0000 Subject: [PATCH 42/48] mypy/pylint/flake8 tidying up --- tilings/algorithms/minimal_gridded_perms.py | 2 +- tilings/strategies/detect_components.py | 3 +- tilings/strategies/monotone_sliding.py | 3 +- tilings/strategies/symmetry.py | 2 +- tilings/strategies/verification.py | 32 ++++++++++++++------- tilings/tilescope.py | 19 ++++++------ tilings/tiling.py | 10 ++++--- 7 files changed, 42 insertions(+), 29 deletions(-) diff --git a/tilings/algorithms/minimal_gridded_perms.py b/tilings/algorithms/minimal_gridded_perms.py index 8e3dc839..985ff5a6 100644 --- a/tilings/algorithms/minimal_gridded_perms.py +++ b/tilings/algorithms/minimal_gridded_perms.py @@ -548,7 +548,7 @@ def odd_even_minimal_gridded_perms( self, odd_cells: Set[Cell], even_cells: Set[Cell] ) -> Set[GriddedPerm]: if odd_cells.intersection(even_cells): - return + return set() def cell_count(gp: GriddedPerm, cell: Cell) -> int: return sum(1 for _ in filter(cell.__eq__, gp.pos)) diff --git a/tilings/strategies/detect_components.py b/tilings/strategies/detect_components.py index 9a46f409..d5c21ecb 100644 --- a/tilings/strategies/detect_components.py +++ b/tilings/strategies/detect_components.py @@ -117,8 +117,7 @@ def shifts( raise StrategyDoesNotApply return (0,) - @staticmethod - def decomposition_function(comb_class: Tiling) -> Optional[Tuple[Tiling]]: + def decomposition_function(self, comb_class: Tiling) -> Optional[Tuple[Tiling]]: if not comb_class.tracking_assumptions: return None return (comb_class.remove_components_from_assumptions(),) diff --git a/tilings/strategies/monotone_sliding.py b/tilings/strategies/monotone_sliding.py index beddf310..e58b791d 100644 --- a/tilings/strategies/monotone_sliding.py +++ b/tilings/strategies/monotone_sliding.py @@ -3,6 +3,7 @@ from comb_spec_searcher import DisjointUnionStrategy, StrategyFactory from comb_spec_searcher.exception import StrategyDoesNotApply +from comb_spec_searcher.strategies import Rule from permuta import Perm from tilings import GriddedPerm, Tiling from tilings.algorithms import Fusion @@ -118,7 +119,7 @@ class MonotoneSlidingFactory(StrategyFactory[Tiling]): This is only looks at n x 1 and 1 x n tilings. """ - def __call__(self, comb_class: Tiling) -> Iterator[GeneralizedSlidingStrategy]: + def __call__(self, comb_class: Tiling) -> Iterator[Rule[Tiling, GriddedPerm]]: if comb_class.predicate_assumptions: raise NotImplementedError("Not implemented sliding for predicates") parent = comb_class diff --git a/tilings/strategies/symmetry.py b/tilings/strategies/symmetry.py index 3953bdbf..580b7af8 100644 --- a/tilings/strategies/symmetry.py +++ b/tilings/strategies/symmetry.py @@ -31,7 +31,7 @@ def inverse_gp_transform(self, tiling: Tiling, gp: GriddedPerm) -> GriddedPerm: def assumption_type_transform( assumption: Assumption, ) -> Type[Assumption]: - pass + raise NotImplementedError @staticmethod def _assumption_type_swap( diff --git a/tilings/strategies/verification.py b/tilings/strategies/verification.py index 15619b2a..b1280964 100644 --- a/tilings/strategies/verification.py +++ b/tilings/strategies/verification.py @@ -5,7 +5,18 @@ from typing import Any, Callable, Dict, Iterable, Iterator, Optional, Tuple, cast import requests -from sympy import Eq, Expr, Function, Symbol, collect, degree, solve, sympify, var +from sympy import ( + Eq, + Expr, + Function, + Number, + Symbol, + collect, + degree, + solve, + sympify, + var, +) from comb_spec_searcher import ( AtomStrategy, @@ -60,10 +71,6 @@ class BasicVerificationStrategy(AtomStrategy): - """ - TODO: can this be moved to the CSS atom strategy? - """ - def get_terms(self, comb_class: CombinatorialClass, n: int) -> Terms: if not isinstance(comb_class, Tiling): raise NotImplementedError @@ -78,8 +85,7 @@ def get_terms(self, comb_class: CombinatorialClass, n: int) -> Terms: return Counter([parameters]) return Counter() - @staticmethod - def get_objects(comb_class: CombinatorialClass, n: int) -> Objects: + def get_objects(self, comb_class: CombinatorialClass, n: int) -> Objects: if not isinstance(comb_class, Tiling) or comb_class.predicate_assumptions: raise NotImplementedError res: Objects = defaultdict(list) @@ -284,7 +290,11 @@ def get_specification( try: self._spec[comb_class] = super().get_specification(comb_class) except InvalidOperationError as e: - if len(comb_class.requirements) > 1 or comb_class.dimensions != (1, 1): + if ( + len(comb_class.requirements) > 1 + or comb_class.dimensions != (1, 1) + or comb_class.predicate_assumptions + ): raise e self._spec[comb_class] = self._spec_from_permpal(comb_class) return self._spec[comb_class] @@ -438,9 +448,11 @@ def random_sample_object_of_size( ) -> GriddedPerm: if comb_class.assumptions: assert ( - len(comb_class.assumptions) == 1 + len(comb_class.tracking_assumptions) == 1 and parameters[ - comb_class.get_assumption_parameter(comb_class.assumptions[0]) + comb_class.get_assumption_parameter( + comb_class.tracking_assumptions[0] + ) ] == n ) diff --git a/tilings/tilescope.py b/tilings/tilescope.py index 4f415a5f..929c6f85 100644 --- a/tilings/tilescope.py +++ b/tilings/tilescope.py @@ -34,6 +34,7 @@ from permuta import Basis, Perm from tilings import GriddedPerm, Tiling from tilings.assumptions import ( + Assumption, EqualParityAssumption, EvenCountAssumption, OddCountAssumption, @@ -77,11 +78,6 @@ def __init__( strategy_pack = strategy_pack.add_basis(basis) strategy_pack = strategy_pack.setup_subclass_verification(start_tiling) - if start_tiling.dimensions == (1, 1): - logger.debug("Fixing basis in basis aware verification strategies.") - strategy_pack = strategy_pack.add_basis(basis) - strategy_pack = strategy_pack.setup_subclass_verification(start_tiling) - super().__init__( start_class=start_tiling, strategy_pack=strategy_pack, @@ -434,8 +430,8 @@ def __init__(self) -> None: self.classdb = ClassDB(Tiling) self.label_to_tilings: List[bytes] = [] self.tilings_to_label: Dict[bytes, int] = {} - self.assumption_type_to_int: Dict[Type[TrackingAssumption], int] = {} - self.int_to_assumption_type: List[Type[TrackingAssumption]] = [] + self.assumption_type_to_int: Dict[Type[Assumption], int] = {} + self.int_to_assumption_type: List[Type[Assumption]] = [] def __iter__(self) -> Iterator[int]: for key in self.label_to_info: @@ -469,7 +465,7 @@ def tiling_to_key(self, tiling: Tiling) -> TrackedClassDBKey: ) return (underlying_label, assumption_keys) - def assumption_to_key(self, ass: TrackingAssumption) -> TrackedClassAssumption: + def assumption_to_key(self, ass: Assumption) -> TrackedClassAssumption: """ Determines the type of the assumption and retrieves the int representing that type from the appropriate class variables, and then apprends the cells. @@ -690,8 +686,11 @@ def backward_map( ) -> Iterator[GriddedPerm]: if children is None: children = self.decomposition_function(comb_class) - gp = next((gp for gp in objs if gp is not None)) - yield gp + try: + gp = next((gp for gp in objs if gp is not None)) + yield gp + except StopIteration: + return StopIteration def forward_map( self, diff --git a/tilings/tiling.py b/tilings/tiling.py index dce924eb..5e5b518a 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -853,17 +853,19 @@ def remove_requirement(self, requirement: Tuple[GriddedPerm, ...]) -> "Tiling": sorted_input=True, ) - def add_assumption(self, assumption: Assumption) -> "Tiling": + def add_assumption(self, assumption: Assumption, clean: bool = True) -> "Tiling": """Returns a new tiling with the added assumption.""" - return self.add_assumptions((assumption,)) + return self.add_assumptions((assumption,), clean) - def add_assumptions(self, assumptions: Iterable[Assumption]) -> "Tiling": + def add_assumptions( + self, assumptions: Iterable[Assumption], clean: bool = True + ) -> "Tiling": """Returns a new tiling with the added assumptions.""" assumptions = tuple(assumptions) remove_empty_rows_and_cols = False derive_empty = False simplify = False - if any(isinstance(ass, PredicateAssumption) for ass in assumptions): + if clean and any(isinstance(ass, PredicateAssumption) for ass in assumptions): remove_empty_rows_and_cols = True derive_empty = True simplify = True From a176b0800ffcbb1588699d7bb3a9802b07c03af8 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Mon, 30 Jan 2023 21:15:20 +0000 Subject: [PATCH 43/48] override pack in parity scope --- tilings/tilescope.py | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/tilings/tilescope.py b/tilings/tilescope.py index 929c6f85..c3e03830 100644 --- a/tilings/tilescope.py +++ b/tilings/tilescope.py @@ -41,6 +41,7 @@ TrackingAssumption, ) from tilings.strategies.predicate_refinement import RefinePredicatesStrategy +from tilings.strategies.verification import BasicVerificationStrategy from tilings.strategy_pack import TileScopePack from tilings.tiling import set_debug @@ -735,9 +736,14 @@ def __init__( delay_next: bool = False, **kwargs, ) -> None: + strategy_pack = strategy_pack.add_initial( + RefinePredicatesStrategy(), apply_first=True + ) + strategy_pack.ver_strats = (BasicVerificationStrategy(),) + strategy_pack.name = "parity_" + strategy_pack.name super().__init__( start_class, - strategy_pack.add_initial(RefinePredicatesStrategy(), apply_first=True), + strategy_pack, max_assumptions, delay_next, **kwargs, From 4dd068f65a02591f5d77ecae10ac8312f88c7e4a Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Mon, 20 Mar 2023 15:07:42 +0000 Subject: [PATCH 44/48] possibly empty is an argument to some strategies --- tests/strategies/test_encoding.py | 47 ++++++++++++++----- tests/strategies/test_factors.py | 3 ++ tests/strategies/test_inferral.py | 2 +- .../strategies/test_row_column_separation.py | 2 +- tests/strategies/test_verification.py | 25 ++++++++-- tilings/strategies/factor.py | 32 ++++++++++--- tilings/strategies/fusion/fusion.py | 15 ++++-- tilings/strategies/obstruction_inferral.py | 20 +++++--- tilings/strategies/requirement_placement.py | 10 ++-- tilings/strategies/verification.py | 1 + tilings/tilescope.py | 3 +- tilings/tiling.py | 2 +- 12 files changed, 121 insertions(+), 41 deletions(-) diff --git a/tests/strategies/test_encoding.py b/tests/strategies/test_encoding.py index 28274614..3f15233d 100644 --- a/tests/strategies/test_encoding.py +++ b/tests/strategies/test_encoding.py @@ -236,29 +236,36 @@ def pointonly_partial_ignoreparent_dirs(strategy): ] -def partition_ignoreparent_workable(strategy): +def partition_ignoreparent_workable_possibly_empty(strategy): return [ - strategy(partition=partition, ignore_parent=ignore_parent, workable=workable) - for partition, ignore_parent, workable in product( + strategy( + partition=partition, + ignore_parent=ignore_parent, + workable=workable, + possibly_empty=possibly_empty, + ) + for partition, ignore_parent, workable, possibly_empty in product( ( [[(2, 1), (0, 1)], [(1, 0)]], (((0, 0), (0, 2)), ((0, 1),), ((3, 3), (4, 3))), ), (True, False), (True, False), + (True, False), ) ] -def partition_ignoreparent_workable_tracked(strategy): +def partition_ignoreparent_workable_possibly_empty_tracked(strategy): return [ strategy( partition=partition, ignore_parent=ignore_parent, workable=workable, + possibly_empty=possibly_empty, tracked=tracked, ) - for partition, ignore_parent, workable, tracked in product( + for partition, ignore_parent, workable, possibly_empty, tracked in product( ( [[(2, 1), (0, 1)], [(1, 0)]], (((0, 0), (0, 2)), ((0, 1),), ((3, 3), (4, 3))), @@ -266,6 +273,7 @@ def partition_ignoreparent_workable_tracked(strategy): (True, False), (True, False), (True, False), + (True, False), ) ] @@ -302,7 +310,9 @@ def gps_ignoreparent_limited(factory): ] -def gps_indices_direction_owncol_ownrow_ignoreparent_includeempty(strategy): +def gps_indices_direction_owncol_ownrow_ignoreparent_includeempty_possibly_empty( + strategy, +): return [ strategy( gps=gps, @@ -312,11 +322,12 @@ def gps_indices_direction_owncol_ownrow_ignoreparent_includeempty(strategy): own_row=own_row, ignore_parent=ignore_parent, include_empty=include_empty, + possibly_empty=possibly_empty, ) for ( gps, indices, - ), direction, own_col, own_row, ignore_parent, include_empty in product( + ), direction, own_col, own_row, ignore_parent, include_empty, possibly_empty in product( ( ((GriddedPerm((0,), ((0, 0),)),), (0,)), ((GriddedPerm.single_cell((0, 1, 2), (2, 1)),), (1,)), @@ -333,6 +344,7 @@ def gps_indices_direction_owncol_ownrow_ignoreparent_includeempty(strategy): (True, False), (True, False), (True, False), + (True, False), ) ] @@ -401,9 +413,13 @@ def indices_and_row(strategy): + maxreqlen_extrabasis_ignoreparent(RequirementInsertionFactory) + subreqs_partial_ignoreparent_dirs(RequirementPlacementFactory) + [SymmetriesFactory(), BasicVerificationStrategy(), EmptyCellInferralFactory()] - + partition_ignoreparent_workable(FactorStrategy) - + partition_ignoreparent_workable_tracked(FactorWithInterleavingStrategy) - + partition_ignoreparent_workable_tracked(FactorWithMonotoneInterleavingStrategy) + + partition_ignoreparent_workable_possibly_empty(FactorStrategy) + + partition_ignoreparent_workable_possibly_empty_tracked( + FactorWithInterleavingStrategy + ) + + partition_ignoreparent_workable_possibly_empty_tracked( + FactorWithMonotoneInterleavingStrategy + ) + ignoreparent(DatabaseVerificationStrategy) + ignoreparent(LocallyFactorableVerificationStrategy) + ignoreparent(ElementaryVerificationStrategy) @@ -445,7 +461,7 @@ def indices_and_row(strategy): + ignoreparent(RequirementCorroborationFactory) + gps_ignoreparent(RequirementInsertionStrategy) + gps_ignoreparent_limited(RequirementInsertionFactory) - + gps_indices_direction_owncol_ownrow_ignoreparent_includeempty( + + gps_indices_direction_owncol_ownrow_ignoreparent_includeempty_possibly_empty( RequirementPlacementStrategy ) + maxreqlen_extrabasis_ignoreparent_maxnumreq(RootInsertionFactory) @@ -475,7 +491,14 @@ def indices_and_row(strategy): DeflationStrategy((4, 1), False, False), ] + [ComponentFusionFactory()] - + [ObstructionInferralStrategy([GriddedPerm((0, 1, 2), ((0, 0), (1, 1), (1, 2)))])] + + [ + ObstructionInferralStrategy( + [GriddedPerm((0, 1, 2), ((0, 0), (1, 1), (1, 2)))], possibly_empty=True + ), + ObstructionInferralStrategy( + [GriddedPerm((0, 1, 2), ((0, 0), (1, 1), (1, 2)))], possibly_empty=False + ), + ] + [ SplittingStrategy(), SplittingStrategy("none"), diff --git a/tests/strategies/test_factors.py b/tests/strategies/test_factors.py index ff1adb3e..01d6c3d6 100644 --- a/tests/strategies/test_factors.py +++ b/tests/strategies/test_factors.py @@ -200,6 +200,9 @@ def test_rule( assert all(rule.inferrable for rule in factor_with_int_rules) assert all(len(rule.strategy.partition) == len(rule.children) for rule in all_rules) assert all(rule.workable for rule in all_rules) + for rule in all_rules: + print(rule) + print(rule.possibly_empty) assert all(not rule.possibly_empty for rule in all_rules) assert all(rule.ignore_parent for rule in all_rules) assert not list(FactorFactory(interleaving="all")(not_fact_tiling)) diff --git a/tests/strategies/test_inferral.py b/tests/strategies/test_inferral.py index db57ec29..0d205a95 100644 --- a/tests/strategies/test_inferral.py +++ b/tests/strategies/test_inferral.py @@ -191,7 +191,7 @@ def test_row_col_sep(tiling1): assert isinstance(rule.constructor, DisjointUnion) assert rule.formal_step == "row and column separation" assert rule.inferrable - assert not rule.possibly_empty + assert rule.possibly_empty assert rule.ignore_parent assert rule.workable assert rule.children[0] == Tiling( diff --git a/tests/strategies/test_row_column_separation.py b/tests/strategies/test_row_column_separation.py index e0698c45..59e272f7 100644 --- a/tests/strategies/test_row_column_separation.py +++ b/tests/strategies/test_row_column_separation.py @@ -203,7 +203,7 @@ def test_rule(seperable_tiling1, not_separable_tilings): assert rule.ignore_parent assert rule.workable assert isinstance(rule.constructor, DisjointUnion) - assert not rule.possibly_empty + assert rule.possibly_empty assert ( RowColumnSeparationStrategy().decomposition_function(not_separable_tilings[0]) is None diff --git a/tests/strategies/test_verification.py b/tests/strategies/test_verification.py index e605a037..b9e79932 100644 --- a/tests/strategies/test_verification.py +++ b/tests/strategies/test_verification.py @@ -24,6 +24,7 @@ ) from tilings.strategies.detect_components import DetectComponentsStrategy from tilings.strategies.experimental_verification import SubclassVerificationStrategy +from tilings.strategies.predicate_refinement import RefinePredicatesStrategy from tilings.tilescope import TileScopePack @@ -472,6 +473,8 @@ def test_pack(self, strategy, enum_verified): enum_verified[0] ) == TileScopePack.regular_insertion_encoding(3).add_initial( DetectComponentsStrategy() + ).add_initial( + RefinePredicatesStrategy(), apply_first=True ) assert strategy.pack(enum_verified[1]).name == "factor pack" assert strategy.pack(enum_verified[2]).name == "factor pack" @@ -663,6 +666,8 @@ def test_pack(self, strategy, enum_verified): enum_verified[1] ) == TileScopePack.regular_insertion_encoding(3).add_initial( DetectComponentsStrategy() + ).add_initial( + RefinePredicatesStrategy(), apply_first=True ) @pytest.mark.timeout(30) @@ -999,23 +1004,35 @@ def test_pack(self, strategy, enum_verified): enum_verified[0] ) == TileScopePack.point_and_row_and_col_placements().add_verification( BasicVerificationStrategy(), replace=True + ).add_initial( + RefinePredicatesStrategy(), apply_first=True ) assert strategy.pack(enum_verified[1]) in ( - TileScopePack.regular_insertion_encoding(2), - TileScopePack.regular_insertion_encoding(3), + TileScopePack.regular_insertion_encoding(2).add_initial( + RefinePredicatesStrategy(), apply_first=True + ), + TileScopePack.regular_insertion_encoding(3).add_initial( + RefinePredicatesStrategy(), apply_first=True + ), ) assert strategy.pack( enum_verified[2] - ) == TileScopePack.regular_insertion_encoding(3) + ) == TileScopePack.regular_insertion_encoding(3).add_initial( + RefinePredicatesStrategy(), apply_first=True + ) assert strategy.pack( enum_verified[3] - ) == TileScopePack.regular_insertion_encoding(2) + ) == TileScopePack.regular_insertion_encoding(2).add_initial( + RefinePredicatesStrategy(), apply_first=True + ) assert strategy.pack( enum_verified[4] ) == TileScopePack.row_and_col_placements().add_basis( [Perm((0, 1, 2)), Perm((2, 3, 0, 1))] + ).add_initial( + RefinePredicatesStrategy(), apply_first=True ) # assert strategy.pack( diff --git a/tilings/strategies/factor.py b/tilings/strategies/factor.py index 145077fd..aaa20e54 100644 --- a/tilings/strategies/factor.py +++ b/tilings/strategies/factor.py @@ -69,6 +69,7 @@ def __init__( partition: Iterable[Iterable[Cell]], ignore_parent: bool = True, workable: bool = True, + possibly_empty: bool = False, ): self.partition = tuple(sorted(tuple(sorted(p)) for p in partition)) inferrable = any( @@ -78,7 +79,7 @@ def __init__( ignore_parent=ignore_parent, workable=workable, inferrable=inferrable, - possibly_empty=True, + possibly_empty=possibly_empty, ) def decomposition_function(self, comb_class: Tiling) -> Tuple[Tiling, ...]: @@ -185,6 +186,7 @@ def __repr__(self) -> str: [ f"partition={self.partition}", f"ignore_parent={self.ignore_parent}", + f"possibly_empty={self.possibly_empty}", f"workable={self.workable}", ] ) @@ -196,7 +198,6 @@ def to_jsonable(self) -> dict: """Return a dictionary form of the strategy.""" d: dict = super().to_jsonable() d.pop("inferrable") - d.pop("possibly_empty") d["partition"] = self.partition return d @@ -285,9 +286,10 @@ def __init__( partition: Iterable[Iterable[Cell]], ignore_parent: bool = True, workable: bool = True, + possibly_empty: bool = False, tracked: bool = True, ): - super().__init__(partition, ignore_parent, workable) + super().__init__(partition, ignore_parent, workable, possibly_empty) self.tracked = tracked self.cols, self.rows = self.interleaving_rows_and_cols(self.partition) @@ -302,6 +304,7 @@ def __repr__(self) -> str: f"partition={self.partition}", f"ignore_parent={self.ignore_parent}", f"workable={self.workable}", + f"possibly_empty={self.possibly_empty}", f"tracked={self.tracked}", ] ) @@ -629,11 +632,22 @@ def __call__(self, comb_class: Tiling) -> Iterator[FactorStrategy]: components = tuple( tuple(chain.from_iterable(part)) for part in partition ) - yield self._build_strategy(components, workable=False) - yield self._build_strategy(min_comp, workable=self.workable) + yield self._build_strategy( + components, + workable=False, + possibly_empty=bool(comb_class.predicate_assumptions), + ) + yield self._build_strategy( + min_comp, + workable=self.workable, + possibly_empty=bool(comb_class.predicate_assumptions), + ) def _build_strategy( - self, components: Tuple[Tuple[Cell, ...], ...], workable: bool + self, + components: Tuple[Tuple[Cell, ...], ...], + workable: bool, + possibly_empty: bool, ) -> FactorStrategy: """ Build the factor strategy for the given components. @@ -651,11 +665,15 @@ def _build_strategy( components, ignore_parent=self.ignore_parent, workable=workable, + possibly_empty=possibly_empty, tracked=self.tracked, ), ) return FactorStrategy( - components, ignore_parent=self.ignore_parent, workable=workable + components, + ignore_parent=self.ignore_parent, + workable=workable, + possibly_empty=possibly_empty, ) def __str__(self) -> str: diff --git a/tilings/strategies/fusion/fusion.py b/tilings/strategies/fusion/fusion.py index eb8de334..6dd7812a 100644 --- a/tilings/strategies/fusion/fusion.py +++ b/tilings/strategies/fusion/fusion.py @@ -9,7 +9,7 @@ from comb_spec_searcher.typing import Objects from tilings import GriddedPerm, Tiling from tilings.algorithms import Fusion -from tilings.assumptions import OddCountAssumption +from tilings.assumptions import EvenCountAssumption, OddCountAssumption from ..pointing import DivideByK from .constructor import FusionConstructor, ReverseFusionConstructor @@ -207,6 +207,15 @@ def constructor( assert children is None or children == (child,) min_left, min_right = algo.min_left_right_points() left, right = algo.left_fuse_region(), algo.right_fuse_region() + odd_left, odd_right = None, None + if OddCountAssumption.from_cells(left) in comb_class.assumptions: + odd_left = True + elif EvenCountAssumption.from_cells(left) in comb_class.assumptions: + odd_left = False + if OddCountAssumption.from_cells(right) in comb_class.assumptions: + odd_right = True + elif EvenCountAssumption.from_cells(right) in comb_class.assumptions: + odd_right = False return FusionConstructor( comb_class, child, @@ -215,8 +224,8 @@ def constructor( *self.left_right_both_sided_parameters(comb_class), min_left, min_right, - odd_left=(OddCountAssumption.from_cells(left) in comb_class.assumptions), - odd_right=(OddCountAssumption.from_cells(right) in comb_class.assumptions), + odd_left=odd_left, + odd_right=odd_right, ) def reverse_constructor( # pylint: disable=no-self-use diff --git a/tilings/strategies/obstruction_inferral.py b/tilings/strategies/obstruction_inferral.py index 92389de5..6e0cc677 100644 --- a/tilings/strategies/obstruction_inferral.py +++ b/tilings/strategies/obstruction_inferral.py @@ -18,10 +18,13 @@ class ObstructionInferralStrategy(DisjointUnionStrategy[Tiling, GriddedPerm]): - def __init__(self, gps: Iterable[GriddedPerm]): + def __init__(self, gps: Iterable[GriddedPerm], possibly_empty: bool = False): self.gps = tuple(sorted(gps)) super().__init__( - ignore_parent=True, inferrable=True, possibly_empty=True, workable=True + ignore_parent=True, + inferrable=True, + possibly_empty=possibly_empty, + workable=True, ) def decomposition_function(self, comb_class: Tiling) -> Tuple[Tiling]: @@ -76,7 +79,10 @@ def forward_map( return (children[0].forward_map.map_gp(obj),) def __repr__(self) -> str: - return f"{self.__class__.__name__}(gps={self.gps})" + return ( + f"{self.__class__.__name__}(gps={self.gps}, " + f"possibly_empty={self.possibly_empty})" + ) def __str__(self) -> str: return self.formal_step() @@ -88,7 +94,6 @@ def to_jsonable(self) -> dict: d: dict = super().to_jsonable() d.pop("ignore_parent") d.pop("inferrable") - d.pop("possibly_empty") d.pop("workable") d["gps"] = [gp.to_jsonable() for gp in self.gps] return d @@ -96,8 +101,7 @@ def to_jsonable(self) -> dict: @classmethod def from_dict(cls, d: dict) -> "ObstructionInferralStrategy": gps = [GriddedPerm.from_dict(gp) for gp in d.pop("gps")] - assert not d - return cls(gps=gps) + return cls(gps=gps, **d) class ObstructionInferralFactory(StrategyFactory[Tiling]): @@ -124,7 +128,9 @@ def new_obs(self, tiling: Tiling) -> Sequence[GriddedPerm]: def __call__(self, comb_class: Tiling) -> Iterator[ObstructionInferralStrategy]: gps = self.new_obs(comb_class) if gps: - yield ObstructionInferralStrategy(gps) + yield ObstructionInferralStrategy( + gps, possibly_empty=bool(comb_class.predicate_assumptions) + ) def to_jsonable(self) -> dict: d: dict = super().to_jsonable() diff --git a/tilings/strategies/requirement_placement.py b/tilings/strategies/requirement_placement.py index 2dba00c4..d5a44b0b 100644 --- a/tilings/strategies/requirement_placement.py +++ b/tilings/strategies/requirement_placement.py @@ -47,6 +47,7 @@ def __init__( own_row: bool = True, ignore_parent: bool = False, include_empty: bool = False, + possibly_empty: bool = False, ): self.gps = tuple(gps) self.indices = tuple(indices) @@ -56,8 +57,8 @@ def __init__( self._placed_cells = tuple( sorted(set(gp.pos[idx] for idx, gp in zip(self.indices, self.gps))) ) - # possibly_empty = self.include_empty or len(self.gps) > 1 - super().__init__(ignore_parent=ignore_parent, possibly_empty=True) + possibly_empty = self.include_empty or len(self.gps) > 1 or possibly_empty + super().__init__(ignore_parent=ignore_parent, possibly_empty=possibly_empty) def _placed_cell(self, idx: int) -> Cell: """Return the cell placed given the index of the child.""" @@ -244,7 +245,8 @@ def __repr__(self) -> str: f"indices={self.indices}, direction={self.direction}, " f"own_col={self.own_col}, own_row={self.own_row}, " f"ignore_parent={self.ignore_parent}, " - f"include_empty={self.include_empty})" + f"include_empty={self.include_empty}," + f"possibly_empty={self.possibly_empty})" ) def to_jsonable(self) -> dict: @@ -252,7 +254,6 @@ def to_jsonable(self) -> dict: d: dict = super().to_jsonable() d.pop("workable") d.pop("inferrable") - d.pop("possibly_empty") d["gps"] = tuple(gp.to_jsonable() for gp in self.gps) d["indices"] = self.indices d["direction"] = self.direction @@ -329,6 +330,7 @@ def __call__(self, comb_class: Tiling) -> Iterator[Rule]: own_col=req_placement.own_col, ignore_parent=self.ignore_parent, include_empty=self.include_empty, + possibly_empty=bool(comb_class.predicate_assumptions), ) children = req_placement.place_point_of_req(gps, indices, direction) if self.include_empty: diff --git a/tilings/strategies/verification.py b/tilings/strategies/verification.py index e6ac2346..7e97653e 100644 --- a/tilings/strategies/verification.py +++ b/tilings/strategies/verification.py @@ -1,3 +1,4 @@ +# pylint: disable=too-many-lines from collections import Counter, defaultdict from functools import reduce from itertools import chain diff --git a/tilings/tilescope.py b/tilings/tilescope.py index c3e03830..f318d687 100644 --- a/tilings/tilescope.py +++ b/tilings/tilescope.py @@ -38,7 +38,6 @@ EqualParityAssumption, EvenCountAssumption, OddCountAssumption, - TrackingAssumption, ) from tilings.strategies.predicate_refinement import RefinePredicatesStrategy from tilings.strategies.verification import BasicVerificationStrategy @@ -719,6 +718,8 @@ def extra_parameters( ): child.get_assumption_parameter(ass) for ass in comb_class.tracking_assumptions } + if not child.is_empty() + else {} for child in children ) diff --git a/tilings/tiling.py b/tilings/tiling.py index 5e5b518a..93398559 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -196,7 +196,7 @@ def _set_obstructions_requirements_and_assumptions( ) else: _assumptions.append(ass) - self._assumptions = tuple(sorted(_assumptions)) + self._assumptions = tuple(sorted(set(_assumptions))) def _check_init(self, checked: bool): if DEBUG and not checked: From ba707332088dee89e30e3d31efaae4fc18eed107 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Wed, 22 Mar 2023 11:43:32 +0000 Subject: [PATCH 45/48] moving css stuff that was specific to tilings --- tilings/tilescope.py | 10 ++++++++++ tilings/tiling.py | 13 +++++++++++++ 2 files changed, 23 insertions(+) diff --git a/tilings/tilescope.py b/tilings/tilescope.py index f318d687..287ff83e 100644 --- a/tilings/tilescope.py +++ b/tilings/tilescope.py @@ -764,3 +764,13 @@ def get_start_tiling( ), basis, ) + + def _get_specification_rules( + self, smallest: bool = False, minimization_time_limit: float = 10 + ) -> Iterator[AbstractRule]: + pack = self.strategy_pack + self.strategy_pack = pack.add_initial(OddOrEvenStrategy(), apply_first=True) + yield from self.ruledb.get_specification_rules( + smallest=smallest, minimization_time_limit=minimization_time_limit + ) + self.strategy_pack = pack diff --git a/tilings/tiling.py b/tilings/tiling.py index 93398559..e9eaffe4 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -1994,6 +1994,19 @@ def minimum_size_of_object(self) -> int: return min(len(gp) for gp in self.requirements[0]) return len(next(self.minimal_gridded_perms())) + def min_size(self) -> int: + try: + min_point = len( + next( + self.gridded_perms( + self.maximum_length_of_minimum_gridded_perm() + 4 + ) + ) + ) + except StopIteration: + min_point = self.minimum_size_of_object() + return min_point + def is_point_or_empty_cell(self, cell: Cell) -> bool: point_or_empty_obs = ( GriddedPerm((0, 1), (cell, cell)), From c44d7bc01bf7359cd1b483a513ad408dd110d169 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Wed, 22 Mar 2023 11:54:29 +0000 Subject: [PATCH 46/48] adding a test for av(132) --- tests/test_predicates.py | 33 ++++++++++++++++++++++++++++++ tilings/strategies/verification.py | 2 +- 2 files changed, 34 insertions(+), 1 deletion(-) create mode 100644 tests/test_predicates.py diff --git a/tests/test_predicates.py b/tests/test_predicates.py new file mode 100644 index 00000000..1c526840 --- /dev/null +++ b/tests/test_predicates.py @@ -0,0 +1,33 @@ +import pytest +import sympy + +from comb_spec_searcher import CombinatorialSpecification +from tilings.tilescope import ParityScope, TileScopePack + +point_placements = TileScopePack.point_placements() + + +@pytest.mark.timeout(20) +def test_132(): + searcher = ParityScope("132", point_placements, max_assumptions=100) + spec = searcher.auto_search(smallest=True) + assert isinstance(spec, CombinatorialSpecification) + spec = spec.expand_verified() + for i in range(10): + actual = set(spec.root.objects_of_size(i)) + assert actual == set(spec.generate_objects_of_size(i)) + assert spec.random_sample_object_of_size(i) in actual + assert [ + 1, + 1, + 1, + 2, + 3, + 7, + 12, + 30, + 55, + 143, + 273, + 728, + ] == [spec.count_objects_of_size(i) for i in range(12)] diff --git a/tilings/strategies/verification.py b/tilings/strategies/verification.py index 7e97653e..eb5a6d92 100644 --- a/tilings/strategies/verification.py +++ b/tilings/strategies/verification.py @@ -87,7 +87,7 @@ def get_terms(self, comb_class: CombinatorialClass, n: int) -> Terms: return Counter() def get_objects(self, comb_class: CombinatorialClass, n: int) -> Objects: - if not isinstance(comb_class, Tiling) or comb_class.predicate_assumptions: + if not isinstance(comb_class, Tiling): raise NotImplementedError res: Objects = defaultdict(list) gp = next(comb_class.minimal_gridded_perms()) From 5ec1e7f8e2b845d6ae93fb10a028876a30c8c417 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Wed, 22 Mar 2023 12:32:19 +0000 Subject: [PATCH 47/48] only do more complicated empty if necessary --- tilings/strategies/factor.py | 4 ++++ tilings/tiling.py | 4 +++- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/tilings/strategies/factor.py b/tilings/strategies/factor.py index aaa20e54..b9ea86b2 100644 --- a/tilings/strategies/factor.py +++ b/tilings/strategies/factor.py @@ -86,9 +86,13 @@ def decomposition_function(self, comb_class: Tiling) -> Tuple[Tiling, ...]: return tuple(comb_class.sub_tiling(cells) for cells in self.partition) def is_two_way(self, comb_class: Tiling) -> bool: # type: ignore + if not comb_class.predicate_assumptions: + return True return self.is_reversible(comb_class) def is_reversible(self, comb_class: Tiling) -> bool: # type: ignore + if not comb_class.predicate_assumptions: + return True return not comb_class.experimental_is_empty() def shifts( diff --git a/tilings/tiling.py b/tilings/tiling.py index e9eaffe4..5fa18962 100644 --- a/tilings/tiling.py +++ b/tilings/tiling.py @@ -1723,7 +1723,9 @@ def is_empty(self, experimental_bound: Optional[int] = None) -> bool: return True if any(self._satisfies_predicates(gp) for gp in gps): return False - return self._is_empty_after_expansion(experimental_bound) + if self.predicate_assumptions: + return self._is_empty_after_expansion(experimental_bound) + return True def _is_empty_after_expansion( self, experimental_bound: Optional[int] = None From 98f2a9e7766b98b14adbc64803b6d87962e54931 Mon Sep 17 00:00:00 2001 From: Christian Bean Date: Thu, 23 Mar 2023 16:09:57 +0000 Subject: [PATCH 48/48] tidying up --- tests/strategies/test_encoding.py | 8 ++++---- tests/test_predicates.py | 1 - 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/tests/strategies/test_encoding.py b/tests/strategies/test_encoding.py index 3f15233d..2f3675d3 100644 --- a/tests/strategies/test_encoding.py +++ b/tests/strategies/test_encoding.py @@ -320,14 +320,14 @@ def gps_indices_direction_owncol_ownrow_ignoreparent_includeempty_possibly_empty direction=direction, own_col=own_col, own_row=own_row, - ignore_parent=ignore_parent, - include_empty=include_empty, - possibly_empty=possibly_empty, + ignore_parent=ign_par, + include_empty=inc_empty, + possibly_empty=pos_empty, ) for ( gps, indices, - ), direction, own_col, own_row, ignore_parent, include_empty, possibly_empty in product( + ), direction, own_col, own_row, ign_par, inc_empty, pos_empty in product( ( ((GriddedPerm((0,), ((0, 0),)),), (0,)), ((GriddedPerm.single_cell((0, 1, 2), (2, 1)),), (1,)), diff --git a/tests/test_predicates.py b/tests/test_predicates.py index 1c526840..2c7cdbe2 100644 --- a/tests/test_predicates.py +++ b/tests/test_predicates.py @@ -1,5 +1,4 @@ import pytest -import sympy from comb_spec_searcher import CombinatorialSpecification from tilings.tilescope import ParityScope, TileScopePack