Merge branch 'develop' into req-placements

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

@@ -19,20 +19,21 @@ def read(fname):
     packages=find_packages(),
     long_description=read("README.md"),
     install_requires=[
-        'permuta==1.2.1',
-        'comb_spec_searcher==0.2.2',
+        'permuta==1.3.0',
+        'comb_spec_searcher==0.3.0',
         'logzero==1.5.0',
         'tilings==1.0.1',
-        'sympy==1.4',
+        'sympy==1.5.1',
     ],
     dependency_links = [
         'https://github.com/PermutaTriangle/Tilings/tarball/develop#egg=tilings-1.0.1',
     ],
     setup_requires=['pytest-runner==5.1'],
     tests_require=[
-        'pytest==5.1.1',
-        'pytest-cov==2.7.1',
+        'pytest==5.3.3',
+        'pytest-cov==2.8.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

@@ -1,7 +1,4 @@
 from .database_verification import database_verified
 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 .verify_short_obs import verify_short_obstructions
+from .subset_verified import one_by_one_verified, subset_verified
+from .verify_atoms import verify_atoms

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