| 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__': |
nothing calls this directly
no outgoing calls
no test coverage detected