migrate verification to new algo

Author: enadeau

gen_rec_prog.py

@@ -5,12 +5,12 @@
 from comb_spec_searcher import *
 from permuta import *
 from tilescopethree import *
-from tilescopethree.strategies import one_by_one_verification
+from tilescopethree.strategies import one_by_one_verified
 from tilescopethree.strategy_packs import point_placements_db
 from tilings import *
 
 pack = point_placements_db
-pack.ver_strats = [one_by_one_verification]
+pack.ver_strats = [one_by_one_verified]
 
 if len(sys.argv) > 1:
     inp = sys.argv[1]

setup.py

@@ -34,5 +34,6 @@ def read(fname):
         'pytest-cov==2.7.1',
         'pytest-pep8==1.0.6',
         'pytest-isort==0.3.1',
+        'pytest-timeout==1.3.4',
     ],
 )

tests/test_tilescope.py

@@ -4,8 +4,8 @@
 from comb_spec_searcher import ProofTree
 from tilescopethree import TileScopeTHREE
 from tilescopethree.strategy_packs_v2 import (
-    point_placements, point_placements_fusion,
-    point_placements_fusion_with_interleaving,
+    all_the_strategies_database_verified, point_placements,
+    point_placements_fusion, point_placements_fusion_with_interleaving,
     row_and_col_placements_fusion_with_interleaving_fusion)
 
 
@@ -14,6 +14,12 @@ def test_132():
     searcher = TileScopeTHREE('132', point_placements)
     t = searcher.auto_search(smallest=True)
     assert isinstance(t, ProofTree)
+
+
+@pytest.mark.xfail(reason='Generating function finding not implemented')
+def test_132_genf():
+    searcher = TileScopeTHREE('132', point_placements)
+    t = searcher.auto_search(smallest=True)
     gf = sympy.series(t.get_genf(), n=15)
     x = sympy.Symbol('x')
     assert ([gf.coeff(x, n) for n in range(13)] ==
@@ -22,6 +28,13 @@ def test_132():
 
 @pytest.mark.timeout(20)
 def test_123():
+    searcher = TileScopeTHREE('123', all_the_strategies_database_verified)
+    t = searcher.auto_search(smallest=True)
+    assert isinstance(t, ProofTree)
+
+
+@pytest.mark.timeout(20)
+def test_123_with_db():
     searcher = TileScopeTHREE('123', point_placements_fusion)
     t = searcher.auto_search(smallest=True)
     assert isinstance(t, ProofTree)

tilescopethree/strategies/verification_strategies/__init__.py

@@ -2,6 +2,6 @@
 from .globally_verified import elementary_verified, globally_verified
 from .miner_verification import miner_verified
 from .subclass_verified import subclass_verified
-from .subset_verified import one_by_one_verification, subset_verified
-from .verify_points import verify_points
+from .subset_verified import one_by_one_verified, subset_verified
+from .verify_atoms import verify_atoms
 from .verify_short_obs import verify_short_obstructions

tilescopethree/strategies/verification_strategies/database_verification.py

@@ -1,27 +1,5 @@
-"""A strategy for checking if a tiling is a subset of the class."""
-import os
-from base64 import b64decode, b64encode
-
-from logzero import logger
-
-from comb_spec_searcher import VerificationRule
-from tilings import Tiling
-
-dir_path = os.path.dirname(os.path.realpath(__file__))
-filenames = ["012_depth_5_database_twisted.txt"]
-database = set()
+from tilings.algorithms.enumeration import DatabaseEnumeration
 
 
 def database_verified(tiling, **kwargs):
-    if not database and filenames:
-        for filename in filenames:
-            logger.info("Importing database from '{}'.".format(filename),
-                        extra=kwargs['logger'])
-            f = open(dir_path + "/" + filename, 'r')
-            for line in f.readlines():
-                compression = b64decode(line.encode())
-                dbtiling = Tiling.decompress(compression)
-                database.add(dbtiling)
-            f.close()
-    if tiling in database:
-        return VerificationRule("Already in database!")
+    return DatabaseEnumeration(tiling).verification_rule()

tilescopethree/strategies/verification_strategies/globally_verified.py

@@ -1,42 +1,20 @@
-from comb_spec_searcher import VerificationRule
-
-from .subset_verified import subset_verified
+from tilings.algorithms.enumeration import (ElementaryEnumeration,
+                                            LocallyFactorableEnumeration)
 
 
 def globally_verified(tiling, **kwargs):
-    """The globally verified strategy.
+    """
+    The globally verified strategy.
 
     A tiling is globally verified if every requirement and obstruction is
     non-interleaving.
     """
-    if not tiling.dimensions == (1, 1):
-        if all(not ob.is_interleaving() for ob in tiling.obstructions):
-            if (all(all(not r.is_interleaving() for r in req)
-                    for req in tiling.requirements) and
-                    not possible_tautology(tiling)):
-                return VerificationRule(formal_step="Globally verified.")
-    else:
-        return subset_verified(tiling, **kwargs)
-
-
-def possible_tautology(tiling):
-    """Return True if possibly equivalent to a 1x1 tiling through empty cell
-    inferral. (It just checks if two cells are non-empty - nothing exciting)"""
-    if len(tiling.positive_cells) > 1:
-        return False
-    cells = set()
-    maxlen = max(tiling.maximum_length_of_minimum_gridded_perm(), 1) + 1
-    for gp in tiling.gridded_perms(maxlen=maxlen):
-        cells.update(gp.pos)
-        if len(cells) > 1:
-            return False
-    return True
+    return LocallyFactorableEnumeration(tiling).verification_rule()
 
 
 def elementary_verified(tiling, **kwargs):
-    """A tiling is elementary verified if it is globally verified and has no
-    interleaving cells."""
-    if tiling.fully_isolated():
-        if tiling.dimensions == (1, 1):
-            return subset_verified(tiling, **kwargs)
-        return globally_verified(tiling, **kwargs)
+    """
+    A tiling is elementary verified if it is globally verified and has no
+    interleaving cells.
+    """
+    return ElementaryEnumeration(tiling).verification_rule()

tilescopethree/strategies/verification_strategies/subset_verified.py

@@ -1,50 +1,17 @@
-"""A strategy for checking if a tiling is a subset of the class."""
+from tilings.algorithms.enumeration import (LocalEnumeration,
+                                            OneByOneEnumeration)
 
-from comb_spec_searcher import VerificationRule
-from permuta.descriptors import Basis
-from permuta.permutils import all_symmetry_sets
 
-
-def subset_verified(tiling, basis, **kwargs):
-    """The subset verified strategy.
+def subset_verified(tiling, no_reqs=False, **kwargs):
+    """
+    The subset verified strategy.
 
     A tiling is subset verified if every obstruction and every requirement is
-    localized.
+    localized and the tiling is not 1x1.
     """
-    if kwargs.get("no_factors", False):
-        if len(tiling.find_factors()) > 1:
-            return
-    if kwargs.get("no_reqs", False):
-        if tiling.requirements:
-            return
-    if tiling.dimensions == (1, 1):
-        if one_by_one_verified(tiling, basis, **kwargs):
-            return VerificationRule(
-                formal_step="The tiling is a subset of the class.")
-    elif (all(ob.is_single_cell() for ob in tiling.obstructions) and
-          all(all(r.is_single_cell() for r in req)
-              for req in tiling.requirements)):
-            return VerificationRule(
-                formal_step="The tiling is a subset of the class.")
+    return LocalEnumeration(tiling, no_reqs).verification_rule()
 
 
 def one_by_one_verified(tiling, basis, **kwargs):
-    """Return true if tiling is a subset of the Av(basis)."""
-    if basis is None or tiling.dimensions != (1, 1):
-        return False
-    rootbasis = [ob.patt for ob in tiling.obstructions]
-    if kwargs.get('symmetry'):
-        all_patts = [Basis(sym_set)
-                     for sym_set in all_symmetry_sets(rootbasis)]
-    else:
-        all_patts = [Basis(rootbasis)]
-    if any(basis == patts for patts in all_patts):
-        return False
-    return True
-
-
-def one_by_one_verification(tiling, basis, **kwargs):
     """Return a verification if one-by-one verified."""
-    if one_by_one_verified(tiling, basis, **kwargs):
-        return VerificationRule(
-                        formal_step="The tiling is a subclass of the class.")
+    return OneByOneEnumeration(tiling, basis).verification_rule()

tilescopethree/strategies/verification_strategies/verify_atoms.py

@@ -0,0 +1,9 @@
+"""A strategy for checking if a tiling is a point."""
+from tilings.algorithms.enumeration import BasicEnumeration
+
+
+def verify_atoms(tiling, **kwargs):
+    """
+    Verify the most basics tilings.
+    """
+    return BasicEnumeration(tiling).verification_rule()

tilescopethree/strategies/verification_strategies/verify_points.py

@@ -11,7 +11,7 @@
                                        fusion_with_interleaving,
                                        globally_verified,
                                        obstruction_transitivity,
-                                       one_by_one_verification,
+                                       one_by_one_verified,
                                        partial_requirement_placement,
                                        point_placement,
                                        requirement_corroboration,
@@ -584,7 +584,7 @@
 
 point_placements_one_by_one = Pack(
     initial_strats=[requirement_placement],
-    ver_strats=[one_by_one_verification],
+    ver_strats=[one_by_one_verified],
     inferral_strats=[row_and_column_separation, obstruction_transitivity],
     expansion_strats=[[factor], [all_point_insertions],
                       [requirement_corroboration]],