Spaces:
Runtime error
Runtime error
Delete ag4masses/alphageometry/dd_test.py
Browse files
ag4masses/alphageometry/dd_test.py
DELETED
|
@@ -1,79 +0,0 @@
|
|
| 1 |
-
# Copyright 2023 DeepMind Technologies Limited
|
| 2 |
-
#
|
| 3 |
-
# Licensed under the Apache License, Version 2.0 (the "License");
|
| 4 |
-
# you may not use this file except in compliance with the License.
|
| 5 |
-
# You may obtain a copy of the License at
|
| 6 |
-
#
|
| 7 |
-
# http://www.apache.org/licenses/LICENSE-2.0
|
| 8 |
-
#
|
| 9 |
-
# Unless required by applicable law or agreed to in writing, software
|
| 10 |
-
# distributed under the License is distributed on an "AS IS" BASIS,
|
| 11 |
-
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
| 12 |
-
# See the License for the specific language governing permissions and
|
| 13 |
-
# limitations under the License.
|
| 14 |
-
# ==============================================================================
|
| 15 |
-
|
| 16 |
-
"""Unit tests for dd."""
|
| 17 |
-
import unittest
|
| 18 |
-
|
| 19 |
-
from absl.testing import absltest
|
| 20 |
-
import dd
|
| 21 |
-
import graph as gh
|
| 22 |
-
import problem as pr
|
| 23 |
-
|
| 24 |
-
|
| 25 |
-
MAX_LEVEL = 1000
|
| 26 |
-
|
| 27 |
-
|
| 28 |
-
class DDTest(unittest.TestCase):
|
| 29 |
-
|
| 30 |
-
@classmethod
|
| 31 |
-
def setUpClass(cls):
|
| 32 |
-
super().setUpClass()
|
| 33 |
-
cls.defs = pr.Definition.from_txt_file('defs.txt', to_dict=True)
|
| 34 |
-
cls.rules = pr.Theorem.from_txt_file('rules.txt', to_dict=True)
|
| 35 |
-
|
| 36 |
-
def test_imo_2022_p4_should_succeed(self):
|
| 37 |
-
p = pr.Problem.from_txt(
|
| 38 |
-
'a b = segment a b; g1 = on_tline g1 a a b; g2 = on_tline g2 b b a; m ='
|
| 39 |
-
' on_circle m g1 a, on_circle m g2 b; n = on_circle n g1 a, on_circle n'
|
| 40 |
-
' g2 b; c = on_pline c m a b, on_circle c g1 a; d = on_pline d m a b,'
|
| 41 |
-
' on_circle d g2 b; e = on_line e a c, on_line e b d; p = on_line p a'
|
| 42 |
-
' n, on_line p c d; q = on_line q b n, on_line q c d ? cong e p e q'
|
| 43 |
-
)
|
| 44 |
-
g, _ = gh.Graph.build_problem(p, DDTest.defs)
|
| 45 |
-
goal_args = g.names2nodes(p.goal.args)
|
| 46 |
-
|
| 47 |
-
success = False
|
| 48 |
-
for level in range(MAX_LEVEL):
|
| 49 |
-
added, _, _, _ = dd.bfs_one_level(g, DDTest.rules, level, p)
|
| 50 |
-
if g.check(p.goal.name, goal_args):
|
| 51 |
-
success = True
|
| 52 |
-
break
|
| 53 |
-
if not added: # saturated
|
| 54 |
-
break
|
| 55 |
-
|
| 56 |
-
self.assertTrue(success)
|
| 57 |
-
|
| 58 |
-
def test_incenter_excenter_should_fail(self):
|
| 59 |
-
p = pr.Problem.from_txt(
|
| 60 |
-
'a b c = triangle a b c; d = incenter d a b c; e = excenter e a b c ?'
|
| 61 |
-
' perp d c c e'
|
| 62 |
-
)
|
| 63 |
-
g, _ = gh.Graph.build_problem(p, DDTest.defs)
|
| 64 |
-
goal_args = g.names2nodes(p.goal.args)
|
| 65 |
-
|
| 66 |
-
success = False
|
| 67 |
-
for level in range(MAX_LEVEL):
|
| 68 |
-
added, _, _, _ = dd.bfs_one_level(g, DDTest.rules, level, p)
|
| 69 |
-
if g.check(p.goal.name, goal_args):
|
| 70 |
-
success = True
|
| 71 |
-
break
|
| 72 |
-
if not added: # saturated
|
| 73 |
-
break
|
| 74 |
-
|
| 75 |
-
self.assertFalse(success)
|
| 76 |
-
|
| 77 |
-
|
| 78 |
-
if __name__ == '__main__':
|
| 79 |
-
absltest.main()
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|