Output the solution to out_file. Args: g: gh.Graph object, containing the proof state. p: pr.Problem object, containing the theorem. out_file: file to write to, empty string to skip writing to file.
(g: gh.Graph, p: pr.Problem, out_file: str)
| 129 | |
| 130 | |
| 131 | def write_solution(g: gh.Graph, p: pr.Problem, out_file: str) -> None: |
| 132 | """Output the solution to out_file. |
| 133 | |
| 134 | Args: |
| 135 | g: gh.Graph object, containing the proof state. |
| 136 | p: pr.Problem object, containing the theorem. |
| 137 | out_file: file to write to, empty string to skip writing to file. |
| 138 | """ |
| 139 | setup, aux, proof_steps, refs = ddar.get_proof_steps( |
| 140 | g, p.goal, merge_trivials=False |
| 141 | ) |
| 142 | |
| 143 | solution = '\n==========================' |
| 144 | solution += '\n * From theorem premises:\n' |
| 145 | premises_nl = [] |
| 146 | for premises, [points] in setup: |
| 147 | solution += ' '.join([p.name.upper() for p in points]) + ' ' |
| 148 | if not premises: |
| 149 | continue |
| 150 | premises_nl += [ |
| 151 | natural_language_statement(p) + ' [{:02}]'.format(refs[p.hashed()]) |
| 152 | for p in premises |
| 153 | ] |
| 154 | solution += ': Points\n' + '\n'.join(premises_nl) |
| 155 | |
| 156 | solution += '\n\n * Auxiliary Constructions:\n' |
| 157 | aux_premises_nl = [] |
| 158 | for premises, [points] in aux: |
| 159 | solution += ' '.join([p.name.upper() for p in points]) + ' ' |
| 160 | aux_premises_nl += [ |
| 161 | natural_language_statement(p) + ' [{:02}]'.format(refs[p.hashed()]) |
| 162 | for p in premises |
| 163 | ] |
| 164 | solution += ': Points\n' + '\n'.join(aux_premises_nl) |
| 165 | |
| 166 | # some special case where the deduction rule has a well known name. |
| 167 | r2name = { |
| 168 | 'r32': '(SSS)', |
| 169 | 'r33': '(SAS)', |
| 170 | 'r34': '(Similar Triangles)', |
| 171 | 'r35': '(Similar Triangles)', |
| 172 | 'r36': '(ASA)', |
| 173 | 'r37': '(ASA)', |
| 174 | 'r38': '(Similar Triangles)', |
| 175 | 'r39': '(Similar Triangles)', |
| 176 | 'r40': '(Congruent Triangles)', |
| 177 | 'a00': '(Distance chase)', |
| 178 | 'a01': '(Ratio chase)', |
| 179 | 'a02': '(Angle chase)', |
| 180 | } |
| 181 | |
| 182 | solution += '\n\n * Proof steps:\n' |
| 183 | for i, step in enumerate(proof_steps): |
| 184 | _, [con] = step |
| 185 | nl = proof_step_string(step, refs, last_step=i == len(proof_steps) - 1) |
| 186 | rule_name = r2name.get(con.rule_name, '') |
| 187 | nl = nl.replace('\u21d2', f'{rule_name}\u21d2 ') |
| 188 | solution += '{:03}. '.format(i + 1) + nl + '\n' |
no test coverage detected