| 23 | |
| 24 | |
| 25 | class DDARTest(unittest.TestCase): |
| 26 | |
| 27 | @classmethod |
| 28 | def setUpClass(cls): |
| 29 | super().setUpClass() |
| 30 | cls.defs = pr.Definition.from_txt_file('defs.txt', to_dict=True) |
| 31 | cls.rules = pr.Theorem.from_txt_file('rules.txt', to_dict=True) |
| 32 | |
| 33 | def test_orthocenter_should_fail(self): |
| 34 | txt = 'a b c = triangle a b c; d = on_tline d b a c, on_tline d c a b ? perp a d b c' # pylint: disable=line-too-long |
| 35 | p = pr.Problem.from_txt(txt) |
| 36 | g, _ = gh.Graph.build_problem(p, DDARTest.defs) |
| 37 | |
| 38 | ddar.solve(g, DDARTest.rules, p, max_level=1000) |
| 39 | goal_args = g.names2nodes(p.goal.args) |
| 40 | self.assertFalse(g.check(p.goal.name, goal_args)) |
| 41 | |
| 42 | def test_orthocenter_aux_should_succeed(self): |
| 43 | txt = 'a b c = triangle a b c; d = on_tline d b a c, on_tline d c a b; e = on_line e a c, on_line e b d ? perp a d b c' # pylint: disable=line-too-long |
| 44 | p = pr.Problem.from_txt(txt) |
| 45 | g, _ = gh.Graph.build_problem(p, DDARTest.defs) |
| 46 | |
| 47 | ddar.solve(g, DDARTest.rules, p, max_level=1000) |
| 48 | goal_args = g.names2nodes(p.goal.args) |
| 49 | self.assertTrue(g.check(p.goal.name, goal_args)) |
| 50 | |
| 51 | def test_incenter_excenter_should_succeed(self): |
| 52 | # Note that this same problem should fail in dd_test.py |
| 53 | p = pr.Problem.from_txt( |
| 54 | 'a b c = triangle a b c; d = incenter d a b c; e = excenter e a b c ?' |
| 55 | ' perp d c c e' |
| 56 | ) # pylint: disable=line-too-long |
| 57 | g, _ = gh.Graph.build_problem(p, DDARTest.defs) |
| 58 | |
| 59 | ddar.solve(g, DDARTest.rules, p, max_level=1000) |
| 60 | goal_args = g.names2nodes(p.goal.args) |
| 61 | self.assertTrue(g.check(p.goal.name, goal_args)) |
| 62 | |
| 63 | |
| 64 | if __name__ == '__main__': |
nothing calls this directly
no outgoing calls
no test coverage detected