SigmaGeometry/dd_test_complex.py at main · TeamSigmaGeometry/SigmaGeometry · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
from Problem import GeometricProblem
from relations import predicate, geometric
from dd import DeductiveDatabase

def test_rule_2():
    print("\n===== Running test_rule_2 =====")
    problem = GeometricProblem()
    # Add points
    for name in ['A', 'B', 'C', 'D', 'E', 'F']:
        problem.add_point(name, 0, 0)  # Coordinates are irrelevant for logic
    # Add assumptions
    problem.add_assumption(predicate.Cong(problem.points['A'], problem.points['B'], problem.points['D'], problem.points['E']))
    problem.add_assumption(predicate.Cong(problem.points['B'], problem.points['C'], problem.points['E'], problem.points['F']))
    problem.add_assumption(predicate.Eqangle(problem.points['A'], problem.points['B'], problem.points['C'], problem.points['D'], problem.points['E'], problem.points['F']))
    problem.add_assumption(predicate.Sameclock(problem.points['A'], problem.points['B'], problem.points['C'], problem.points['D'], problem.points['E'], problem.points['F']))
    # Goal: contri1 A B C D E F
    problem.add_goal(predicate.Contri1(problem.points['A'], problem.points['B'], problem.points['C'], problem.points['D'], problem.points['E'], problem.points['F']))
    dd = DeductiveDatabase()
    derived, rules = dd.apply_rules(problem)
    print('Test Rule 2:')
    print('Derived:', [str(p) for p in derived])
    print('Applied Rules:', rules)
    print()

def test_rule_3():
    print("\n===== Running test_rule_3 =====")
    problem = GeometricProblem()
    # Add points
    for name in ['A', 'B', 'C', 'D']:
        problem.add_point(name, 0, 0)
    # Add assumption
    problem.add_assumption(predicate.Para(problem.points['A'], problem.points['B'], problem.points['C'], problem.points['D']))
    # Goal: eqangle A B C D C B
    problem.add_goal(predicate.Eqangle(problem.points['A'], problem.points['B'], problem.points['C'], problem.points['D'], problem.points['C'], problem.points['B']))
    dd = DeductiveDatabase()
    derived, rules = dd.apply_rules(problem)
    print('Test Rule 3:')
    print('Derived:', [str(p) for p in derived])
    print('Applied Rules:', rules)
    print()

def test_cong_cong_to_perp():
    print("\n===== Running test_cong_cong_to_perp =====")
    # Test: cong A M B M, cong A Q B Q, goal perp A B M Q
    problem = GeometricProblem()
    for name in ['A', 'B', 'M', 'Q']:
        problem.add_point(name, 0, 0)
    problem.add_assumption(predicate.Cong(problem.points['A'], problem.points['M'], problem.points['B'], problem.points['M']))
    problem.add_assumption(predicate.Cong(problem.points['A'], problem.points['Q'], problem.points['B'], problem.points['Q']))
    problem.add_goal(predicate.Perp(problem.points['A'], problem.points['B'], problem.points['M'], problem.points['Q']))
    dd = DeductiveDatabase()
    derived, rules = dd.apply_rules(problem)
    print('Test Cong + Cong to Perp:')
    print('Derived:', [str(p) for p in derived])
    print('Applied Rules:', rules)
    print()
def test_perp_midp_to_cong():
    print("\n===== Running test_perp_midp_to_cong =====")
    # Test: perp A B B C, midp M A C, goal cong A M B M
    problem = GeometricProblem()
    for name in ['A', 'B', 'C', 'M']:
        problem.add_point(name, 0, 0)
    problem.add_assumption(predicate.Perp(problem.points['A'], problem.points['B'], problem.points['B'], problem.points['C']))
    problem.add_assumption(predicate.Midp(problem.points['M'], problem.points['A'], problem.points['C']))
    problem.add_goal(predicate.Cong(problem.points['A'], problem.points['M'], problem.points['B'], problem.points['M']))
    dd = DeductiveDatabase()
    derived, rules = dd.apply_rules(problem)
    print('Test Perp + Midp to Cong:')
    print('Derived:', [str(p) for p in derived])
    print('Applied Rules:', rules)
    print()

def test_chain_of_rules():
    print("\n===== Running test_chain_of_rules =====")
    # This test will require two rules to reach the goal.
    # Use: perp A B B C, midp M A C, ?cong A M B M
    # and then: cong A M B M, cong A Q B Q, ?perp A B M Q
    problem = GeometricProblem()
    for name in ['A', 'B', 'C', 'M', 'Q']:
        problem.add_point(name, 0, 0)
    # Step 1: Add assumptions for first rule
    problem.add_assumption(predicate.Perp(problem.points['A'], problem.points['B'], problem.points['B'], problem.points['C']))
    problem.add_assumption(predicate.Midp(problem.points['M'], problem.points['A'], problem.points['C']))
    # Step 2: Add assumption for second rule
    problem.add_assumption(predicate.Cong(problem.points['A'], problem.points['Q'], problem.points['B'], problem.points['Q']))
    # Goal: perp A B M Q (should require two rules)
    problem.add_goal(predicate.Perp(problem.points['A'], problem.points['B'], problem.points['M'], problem.points['Q']))
    dd = DeductiveDatabase()
    derived, rules = dd.apply_rules(problem)
    print('Test Chain of Rules:')
    print('Derived:', [str(p) for p in derived])
    print('Applied Rules:', rules)
    print()

def test_cyclic_para_eqangle():
    print("\n===== Running test_cyclic_para_eqangle =====")
    # This test will require using both a cyclic and a para rule to get eqangle
    # Use: cyclic A B C D, para A B C D, ?eqangle A D C D C D C B
    problem = GeometricProblem()
    for name in ['A', 'B', 'C', 'D']:
        problem.add_point(name, 0, 0)
    problem.add_assumption(predicate.Cyclic(problem.points['A'], problem.points['B'], problem.points['C'], problem.points['D']))
    problem.add_assumption(predicate.Para(problem.points['A'], problem.points['B'], problem.points['C'], problem.points['D']))
    # Goal: eqangle A D C D C B (6 points)
    problem.add_goal(predicate.Eqangle(problem.points['A'], problem.points['D'], problem.points['C'], problem.points['D'], problem.points['C'], problem.points['B']))
    dd = DeductiveDatabase()
    derived, rules = dd.apply_rules(problem)
    print('Test Cyclic + Para to Eqangle:')
    print('Derived:', [str(p) for p in derived])
    print('Applied Rules:', rules)
    print()

def test_para_cyclic_to_eqangle():
    print("\n===== Running test_para_cyclic_to_eqangle =====")
    # Rule: para A B C D, cyclic A B C D => eqangle A D C D C B
    problem = GeometricProblem()
    for name in ['A', 'B', 'C', 'D']:
        problem.add_point(name, 0, 0)
    problem.add_assumption(predicate.Para(problem.points['A'], problem.points['B'], problem.points['C'], problem.points['D']))
    problem.add_assumption(predicate.Cyclic(problem.points['A'], problem.points['B'], problem.points['C'], problem.points['D']))
    problem.add_goal(predicate.Eqangle(problem.points['A'], problem.points['D'], problem.points['C'], problem.points['D'], problem.points['C'], problem.points['B']))
    dd = DeductiveDatabase()
    derived, rules = dd.apply_rules(problem)
    print('Test Para + Cyclic to Eqangle:')
    print('Derived:', [str(p) for p in derived])
    print('Applied Rules:', rules)
    print()

def test_midp_para_para_to_midp():
    print("\n===== Running test_midp_para_para_to_midp =====")
    # Rule: midp M A B, para A C B D, para A D B C => midp M C D
    problem = GeometricProblem()
    for name in ['A', 'B', 'C', 'D', 'M']:
        problem.add_point(name, 0, 0)
    problem.add_assumption(predicate.Midp(problem.points['M'], problem.points['A'], problem.points['B']))
    problem.add_assumption(predicate.Para(problem.points['A'], problem.points['C'], problem.points['B'], problem.points['D']))
    problem.add_assumption(predicate.Para(problem.points['A'], problem.points['D'], problem.points['B'], problem.points['C']))
    problem.add_goal(predicate.Midp(problem.points['M'], problem.points['C'], problem.points['D']))
    dd = DeductiveDatabase()
    derived, rules = dd.apply_rules(problem)
    print('Test Midp + Para + Para to Midp:')
    print('Derived:', [str(p) for p in derived])
    print('Applied Rules:', rules)
    print()

def test_para_symmetry():
    problem = GeometricProblem()
    for name in ['A', 'B', 'C', 'D']:
        problem.add_point(name, 0, 0)
    problem.add_assumption(predicate.Para(problem.points['A'], problem.points['B'], problem.points['C'], problem.points['D']))
    problem.add_goal(predicate.Para(problem.points['C'], problem.points['D'], problem.points['A'], problem.points['B']))
    dd = DeductiveDatabase()
    derived, rules = dd.apply_rules(problem)
    print('Test Para Symmetry:')
    print('Derived:', [str(p) for p in derived])
    print('Applied Rules:', rules)
    print()

if __name__ == '__main__':
    test_rule_2()
    test_rule_3()
    test_chain_of_rules()
    test_cyclic_para_eqangle()
    test_perp_midp_to_cong()
    test_cong_cong_to_perp()
    test_para_cyclic_to_eqangle()
    test_midp_para_para_to_midp()
    test_para_symmetry()