Spaces:
Runtime error
Runtime error
Update ag4masses/alphageometry/alphageometry.py
Browse files
ag4masses/alphageometry/alphageometry.py
CHANGED
|
@@ -150,8 +150,8 @@ def write_solution(g: gh.Graph, p: pr.Problem, out_file: str) -> None:
|
|
| 150 |
g, p.goal, merge_trivials=False
|
| 151 |
)
|
| 152 |
|
| 153 |
-
solution = '
|
| 154 |
-
solution += '
|
| 155 |
premises_nl = []
|
| 156 |
for premises, [points] in setup:
|
| 157 |
solution += ' '.join([p.name.upper() for p in points]) + ' '
|
|
@@ -163,15 +163,18 @@ def write_solution(g: gh.Graph, p: pr.Problem, out_file: str) -> None:
|
|
| 163 |
]
|
| 164 |
solution += ': Points\n' + '\n'.join(premises_nl)
|
| 165 |
|
| 166 |
-
solution += '\n\
|
| 167 |
aux_premises_nl = []
|
| 168 |
-
|
| 169 |
-
solution += '
|
| 170 |
-
|
| 171 |
-
|
| 172 |
-
|
| 173 |
-
|
| 174 |
-
|
|
|
|
|
|
|
|
|
|
| 175 |
|
| 176 |
# some special case where the deduction rule has a well known name.
|
| 177 |
r2name = {
|
|
@@ -189,15 +192,13 @@ def write_solution(g: gh.Graph, p: pr.Problem, out_file: str) -> None:
|
|
| 189 |
'a02': '(Angle chase)',
|
| 190 |
}
|
| 191 |
|
| 192 |
-
solution += '\n\
|
| 193 |
for i, step in enumerate(proof_steps):
|
| 194 |
_, [con] = step
|
| 195 |
nl = proof_step_string(step, refs, last_step=i == len(proof_steps) - 1)
|
| 196 |
rule_name = r2name.get(con.rule_name, '')
|
| 197 |
nl = nl.replace('\u21d2', f'{rule_name}\u21d2 ')
|
| 198 |
solution += '{:03}. '.format(i + 1) + nl + '\n'
|
| 199 |
-
|
| 200 |
-
solution += '==========================\n'
|
| 201 |
logging.info(solution)
|
| 202 |
if out_file:
|
| 203 |
with open(out_file, 'w') as f:
|
|
|
|
| 150 |
g, p.goal, merge_trivials=False
|
| 151 |
)
|
| 152 |
|
| 153 |
+
solution = ''
|
| 154 |
+
solution += 'Theo đề bài ta có:\n'
|
| 155 |
premises_nl = []
|
| 156 |
for premises, [points] in setup:
|
| 157 |
solution += ' '.join([p.name.upper() for p in points]) + ' '
|
|
|
|
| 163 |
]
|
| 164 |
solution += ': Points\n' + '\n'.join(premises_nl)
|
| 165 |
|
| 166 |
+
solution += '\n\nCác điểm cần dựng thêm:\n'
|
| 167 |
aux_premises_nl = []
|
| 168 |
+
if len(aux) == 0:
|
| 169 |
+
solution += 'Không cần dựng thêm điểm nào.'
|
| 170 |
+
else:
|
| 171 |
+
for premises, [points] in aux:
|
| 172 |
+
solution += ' '.join([p.name.upper() for p in points]) + ' '
|
| 173 |
+
aux_premises_nl += [
|
| 174 |
+
natural_language_statement(p) + ' [{:02}]'.format(refs[p.hashed()])
|
| 175 |
+
for p in premises
|
| 176 |
+
]
|
| 177 |
+
solution += ': Points\n' + '\n'.join(aux_premises_nl)
|
| 178 |
|
| 179 |
# some special case where the deduction rule has a well known name.
|
| 180 |
r2name = {
|
|
|
|
| 192 |
'a02': '(Angle chase)',
|
| 193 |
}
|
| 194 |
|
| 195 |
+
solution += '\n\nCác bước chứng minh:\n'
|
| 196 |
for i, step in enumerate(proof_steps):
|
| 197 |
_, [con] = step
|
| 198 |
nl = proof_step_string(step, refs, last_step=i == len(proof_steps) - 1)
|
| 199 |
rule_name = r2name.get(con.rule_name, '')
|
| 200 |
nl = nl.replace('\u21d2', f'{rule_name}\u21d2 ')
|
| 201 |
solution += '{:03}. '.format(i + 1) + nl + '\n'
|
|
|
|
|
|
|
| 202 |
logging.info(solution)
|
| 203 |
if out_file:
|
| 204 |
with open(out_file, 'w') as f:
|