diff --git a/tests/strategies/test_encoding.py b/tests/strategies/test_encoding.py index 28274614..2f3675d3 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, @@ -310,13 +320,14 @@ def gps_indices_direction_owncol_ownrow_ignoreparent_includeempty(strategy): direction=direction, own_col=own_col, own_row=own_row, - ignore_parent=ignore_parent, - include_empty=include_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 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,)), @@ -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/tests/test_predicates.py b/tests/test_predicates.py new file mode 100644 index 00000000..2c7cdbe2 --- /dev/null +++ b/tests/test_predicates.py @@ -0,0 +1,32 @@ +import pytest + +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/algorithms/factor.py b/tilings/algorithms/factor.py index 16ed9cf2..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: @@ -76,10 +80,16 @@ 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): self._unite_cells(cells) + elif isinstance(assumption, PredicateAssumption): + self._unite_cells(assumption.cells) else: for gp in assumption.gps: self._unite_cells(gp.pos) @@ -155,6 +165,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(): @@ -170,7 +182,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/algorithms/fusion.py b/tilings/algorithms/fusion.py index f5092357..33d4d6fe 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 @@ -287,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) @@ -301,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) @@ -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/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/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/minimal_gridded_perms.py b/tilings/algorithms/minimal_gridded_perms.py index 0d3e87ac..985ff5a6 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 set() + + 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/algorithms/requirement_placement.py b/tilings/algorithms/requirement_placement.py index a3997518..4d90279e 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 93ed2b9e..d30855b5 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 +from typing import ( + TYPE_CHECKING, + Iterable, + Iterator, + List, + Optional, + Tuple, + Type, + TypeVar, + Union, +) from permuta import Perm @@ -12,18 +22,25 @@ if TYPE_CHECKING: from tilings import Tiling +AssumptionClass = TypeVar("AssumptionClass", bound="Assumption") +CountAssumption = Union["OddCountAssumption", "EvenCountAssumption"] -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: Type[AssumptionClass], cells: Iterable[Cell] + ) -> AssumptionClass: gps = [GriddedPerm.single_cell((0,), cell) for cell in cells] return cls(gps) @@ -32,10 +49,10 @@ def get_cells(self) -> Tuple[Cell, ...]: return tuple(gp.pos[0] for gp in self.gps) def avoiding( - self, + self: AssumptionClass, obstructions: Iterable[GriddedPerm], active_cells: Optional[Iterable[Cell]] = None, - ) -> "TrackingAssumption": + ) -> AssumptionClass: """ Return the tracking absumption where all of the gridded perms avoiding the obstructions are removed. If active_cells is not None, then any @@ -53,30 +70,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,35 +80,67 @@ 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"]) - 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 __len__(self) -> int: + return len(self.gps) + 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}" @@ -135,7 +160,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]: @@ -206,20 +230,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): def decomposition(self, perm: Perm) -> List[Perm]: @@ -234,12 +247,9 @@ def opposite_tiling_decomposition(self, tiling: "Tiling") -> List[List[Cell]]: def one_or_fewer_components(self, 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): def decomposition(self, perm: Perm) -> List[Perm]: @@ -254,8 +264,155 @@ def opposite_tiling_decomposition(self, tiling: "Tiling") -> List[List[Cell]]: def one_or_fewer_components(self, 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. + """ + + @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 + 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,) + + +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 can_be_refined(self) -> bool: + return len(self) > 1 + + 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(sorted(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 f"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 can_be_refined(self) -> bool: + return len(self) > 1 + + 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(sorted(self.cells), False) + + def __str__(self) -> str: + return f"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_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) + + def __str__(self) -> str: + return f"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_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) + + def __str__(self) -> str: + return f"points are opposite parity in cells {self.cells}" 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 524f69f0..3f5bad7e 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 Any, Callable, Dict, Iterable, Iterator, List, Optional, Tuple +from typing import Any, 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] @@ -254,7 +254,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 ] @@ -283,7 +283,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 } @@ -302,7 +302,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 }, ) @@ -351,7 +351,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 @@ -367,7 +370,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 e82cb1bc..ce6f1e23 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, @@ -175,14 +176,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, @@ -294,7 +298,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 9ff68ea9..5e0c5efb 100644 --- a/tilings/strategies/cell_reduction.py +++ b/tilings/strategies/cell_reduction.py @@ -232,6 +232,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 4a8a2f6a..b3c3c65e 100644 --- a/tilings/strategies/deflation.py +++ b/tilings/strategies/deflation.py @@ -223,6 +223,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 4b06d77d..d5c21ecb 100644 --- a/tilings/strategies/detect_components.py +++ b/tilings/strategies/detect_components.py @@ -118,7 +118,7 @@ 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 return (comb_class.remove_components_from_assumptions(),) @@ -131,7 +131,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) @@ -160,7 +160,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/factor.py b/tilings/strategies/factor.py index f256b85f..b9ea86b2 100644 --- a/tilings/strategies/factor.py +++ b/tilings/strategies/factor.py @@ -69,18 +69,55 @@ 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( 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=possibly_empty, ) 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( + 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], ...]: @@ -90,7 +127,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( @@ -153,6 +190,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}", ] ) @@ -164,7 +202,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 @@ -253,9 +290,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) @@ -270,6 +308,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}", ] ) @@ -597,11 +636,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. @@ -619,11 +669,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/constructor.py b/tilings/strategies/fusion/constructor.py index 5cf811de..6b18820b 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): @@ -241,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: @@ -256,9 +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.""" + 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 @@ -360,7 +369,10 @@ def determine_number_of_points_in_fuse_region( 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 diff --git a/tilings/strategies/fusion/fusion.py b/tilings/strategies/fusion/fusion.py index 18644cfd..6dd7812a 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 EvenCountAssumption, OddCountAssumption from ..pointing import DivideByK from .constructor import FusionConstructor, ReverseFusionConstructor @@ -50,9 +51,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) @@ -177,7 +182,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 @@ -199,6 +206,16 @@ 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() + 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, @@ -207,6 +224,8 @@ def constructor( *self.left_right_both_sided_parameters(comb_class), min_left, min_right, + odd_left=odd_left, + odd_right=odd_right, ) def reverse_constructor( # pylint: disable=no-self-use @@ -218,6 +237,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 @@ -273,7 +294,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 ( { @@ -290,7 +313,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/strategies/monotone_sliding.py b/tilings/strategies/monotone_sliding.py index e40d2651..a3e63ea5 100644 --- a/tilings/strategies/monotone_sliding.py +++ b/tilings/strategies/monotone_sliding.py @@ -91,7 +91,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 }, ) @@ -131,7 +131,9 @@ class MonotoneSlidingFactory(StrategyFactory[Tiling]): This is only looks at n x 1 and 1 x n tilings. """ - def __call__(self, comb_class: Tiling) -> Iterator[Rule]: + 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 rotate = False if ( diff --git a/tilings/strategies/obstruction_inferral.py b/tilings/strategies/obstruction_inferral.py index 26d39e79..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=False, workable=True + ignore_parent=True, + inferrable=True, + possibly_empty=possibly_empty, + workable=True, ) def decomposition_function(self, comb_class: Tiling) -> Tuple[Tiling]: @@ -45,7 +48,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 ) @@ -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/point_jumping.py b/tilings/strategies/point_jumping.py index 8f15c61c..714efe4b 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: @@ -162,7 +163,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 }, ) @@ -330,6 +331,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/predicate_refinement.py b/tilings/strategies/predicate_refinement.py new file mode 100644 index 00000000..0948d403 --- /dev/null +++ b/tilings/strategies/predicate_refinement.py @@ -0,0 +1,83 @@ +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 + + +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, ...]: + 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 assumption_to_refine.refinements(): + children.append(without_predicate.add_assumptions(assumptions)) + return tuple(children) + except StopIteration as e: + raise StrategyDoesNotApply from e + + def formal_step(self) -> str: + return "predicate refinement" + + 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) + idx = DisjointUnionStrategy.backward_map_index(objs) + yield children[idx].backward_map.map_gp(cast(GriddedPerm, objs[idx])) + + 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) + 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, + 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(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 + ) + + @classmethod + def from_dict(cls, d: dict) -> "RefinePredicatesStrategy": + return cls(**d) diff --git a/tilings/strategies/rearrange_assumption.py b/tilings/strategies/rearrange_assumption.py index a8353443..1ae04d1f 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, @@ -349,11 +350,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,) @@ -406,8 +409,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) @@ -481,7 +486,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 }, ) @@ -497,7 +502,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"], ) @@ -511,7 +516,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 332de52d..7b850dca 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..d5a44b0b 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", @@ -46,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) @@ -55,7 +57,7 @@ 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 + 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: @@ -91,7 +93,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 +107,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) @@ -242,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: @@ -250,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 @@ -327,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/row_and_col_separation.py b/tilings/strategies/row_and_col_separation.py index 7ac3ce9c..81de6f75 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"] @@ -25,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: @@ -63,7 +64,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] @@ -71,7 +72,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 ( { @@ -79,7 +80,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 7e051a87..580b7af8 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]: raise NotImplementedError @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 ) }, ) @@ -336,6 +340,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 faa4e667..eb5a6d92 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 @@ -5,7 +6,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, @@ -39,6 +51,7 @@ RequirementCorroborationFactory, SymmetriesFactory, ) +from tilings.strategies.predicate_refinement import RefinePredicatesStrategy from .abstract import BasisAwareVerificationStrategy @@ -59,17 +72,16 @@ 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 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.assumptions + assumption.get_value(gp) + for assumption in comb_class.tracking_assumptions ) return Counter([parameters]) return Counter() @@ -79,9 +91,12 @@ def get_objects(self, 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.assumptions + assumption.get_value(gp) + for assumption in comb_class.tracking_assumptions ) res[parameters].append(gp) return res @@ -121,8 +136,10 @@ def get_genf( 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 Number(0) 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) @@ -158,7 +175,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 @@ -276,7 +293,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] @@ -306,13 +327,19 @@ def pack(self, 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 @@ -326,7 +353,11 @@ def pack(self, 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})" @@ -420,9 +451,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 ) @@ -748,7 +781,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=[ @@ -835,9 +872,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" diff --git a/tilings/tilescope.py b/tilings/tilescope.py index 238563a7..287ff83e 100644 --- a/tilings/tilescope.py +++ b/tilings/tilescope.py @@ -29,11 +29,20 @@ from comb_spec_searcher.class_queue import CSSQueue, DefaultQueue, WorkPacket from comb_spec_searcher.rule_db.abstract import RuleDBAbstract from comb_spec_searcher.strategies.rule import AbstractRule +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 TrackingAssumption +from tilings.assumptions import ( + Assumption, + EqualParityAssumption, + EvenCountAssumption, + OddCountAssumption, +) +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 __all__ = ("TileScope", "TileScopePack", "LimitedAssumptionTileScope", "GuidedSearcher") @@ -58,8 +67,33 @@ def __init__( expand_verified: bool = False, 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): + 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, + classdb=classdb, + ruledb=ruledb, + classqueue=classqueue, + expand_verified=expand_verified, + debug=debug, + ) + + @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): @@ -75,24 +109,11 @@ def __init__( ) 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] ) - - 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, - classdb=classdb, - ruledb=ruledb, - classqueue=classqueue, - expand_verified=expand_verified, - debug=debug, - ) + return start_tiling, basis class LimitedAssumptionTileScope(TileScope): @@ -129,7 +150,7 @@ def _rules_from_strategy( # type: ignore 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) ) @@ -409,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: @@ -444,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. @@ -638,3 +659,118 @@ def status(self) -> str: tilings += f" {len(self.label_to_tilings):,d}" status = status.replace("ClassDB status:", "TrackedClassDB status:" + tilings) return status + "\n" + + +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) + try: + gp = next((gp for gp in objs if gp is not None)) + yield gp + except StopIteration: + return StopIteration + + 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 + } + if not child.is_empty() + else {} + for child in children + ) + + @classmethod + def from_dict(cls, d: dict) -> "OddOrEvenStrategy": + return cls() + + +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: + 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, + 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) + + @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) + ), + 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 4e32ebad..5fa18962 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 ( @@ -47,7 +47,13 @@ guess_obstructions, ) from .assumptions import ( + Assumption, ComponentAssumption, + EqualParityAssumption, + EvenCountAssumption, + OddCountAssumption, + OppositeParityAssumption, + PredicateAssumption, SkewComponentAssumption, SumComponentAssumption, TrackingAssumption, @@ -59,6 +65,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, ...] @@ -83,6 +97,16 @@ total=False, ) +ASSUMPTIONS = [ + TrackingAssumption, + SumComponentAssumption, + SkewComponentAssumption, + EvenCountAssumption, + OddCountAssumption, + EqualParityAssumption, + OppositeParityAssumption, +] # DO NOT CHANGE THE ORDER OF THIS LIST + class Tiling(CombinatorialClass): """Tiling class. @@ -98,12 +122,13 @@ 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, 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. @@ -115,22 +140,9 @@ def __init__( """ self._cached_properties: CachedProperties = {} - super().__init__() - if sorted_input: - # Set of obstructions - 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)) - + 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) @@ -139,29 +151,76 @@ def __init__( # 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() - # 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() + 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) + # Set of requirement lists + self._requirements = tuple(tuple(r) for r in requirements) 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() + # Set of obstructions + self._obstructions = tuple(sorted(obstructions)) + # Set of requirement lists + self._requirements = Tiling.sort_requirements(requirements) + # 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(set(_assumptions))) + + 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(),) + 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( @@ -203,6 +262,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. @@ -240,9 +303,165 @@ def _simplify_griddedperms(self, already_minimized_obs=False) -> None: sorted_input=True, already_minimized_obs=already_minimized_obs, ) - self._obstructions = GPR.obstructions self._requirements = GPR.requirements + if self._predicates_imply_empty(): + 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 + ) + 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.""" @@ -317,7 +536,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: @@ -421,14 +640,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( @@ -485,17 +701,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, @@ -542,7 +752,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, @@ -643,28 +853,35 @@ def remove_requirement(self, requirement: Tuple[GriddedPerm, ...]) -> "Tiling": sorted_input=True, ) - def add_assumption(self, assumption: TrackingAssumption) -> "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[TrackingAssumption], clean: bool = True + 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 clean and 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, ) - if clean: + if simplify: 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) @@ -704,7 +921,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, @@ -1101,22 +1321,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 + if 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. @@ -1128,6 +1369,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, @@ -1139,7 +1382,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": """ @@ -1394,21 +1639,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)) @@ -1419,7 +1666,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}'" @@ -1428,7 +1675,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: """ @@ -1446,22 +1693,154 @@ 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) - def is_empty(self) -> bool: + @lru_cache(10000) + 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 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 self.experimental_is_empty() + if not self.predicate_assumptions and 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)) + 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 + 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 + ) -> bool: + # TODO: consider doing all this as an initial factory + factors = self.find_factors() + if len(factors) > 1: + 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(experimental_bound) + + 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( + experimental_bound + ) + for assumptions in assumption_to_refine.refinements() + ) + except StopIteration: + # nothing can be refined + pass + odd_cells = set( + chain.from_iterable( + ass.cells + for ass in self._assumptions + if isinstance(ass, OddCountAssumption) + ) + ) + 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(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() + + # 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) + + 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: + 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( + False for _ in self.gridded_perms(self.minimum_size_of_object() + bound) + ) + except StopIteration: + # underlying tiling is empty + return True def is_finite(self) -> bool: """Returns True if all active cells have finite basis.""" @@ -1548,7 +1927,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.""" @@ -1569,6 +1953,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() @@ -1601,13 +1986,29 @@ 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: 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)), @@ -1734,9 +2135,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)