Predicates

tests/strategies/test_encoding.py

@@ -236,36 +236,44 @@ 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))),
             ),
             (True, False),
             (True, False),
             (True, False),
+            (True, False),
         )
     ]
 
@@ -302,21 +310,24 @@ 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,
             indices=indices,
             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"),

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))

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(

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

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(

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)]

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(
                 (