Construct the string from Problem object.
(self, definitions: list[Definition])
| 215 | ) |
| 216 | |
| 217 | def setup_str_from_problem(self, definitions: list[Definition]) -> str: |
| 218 | """Construct the <theorem_premises> string from Problem object.""" |
| 219 | ref = 0 |
| 220 | |
| 221 | string = [] |
| 222 | for clause in self.clauses: |
| 223 | group = {} |
| 224 | p2deps = defaultdict(list) |
| 225 | for c in clause.constructions: |
| 226 | cdef = definitions[c.name] |
| 227 | |
| 228 | if len(c.args) != len(cdef.construction.args): |
| 229 | assert len(c.args) + len(clause.points) == len(cdef.construction.args) |
| 230 | c.args = clause.points + c.args |
| 231 | |
| 232 | mapping = dict(zip(cdef.construction.args, c.args)) |
| 233 | for points, bs in cdef.basics: |
| 234 | points = tuple([mapping[x] for x in points]) |
| 235 | for p in points: |
| 236 | group[p] = points |
| 237 | |
| 238 | for b in bs: |
| 239 | args = [mapping[a] for a in b.args] |
| 240 | name = b.name |
| 241 | if b.name in ['s_angle', 'aconst']: |
| 242 | x, y, z, v = args |
| 243 | name = 'aconst' |
| 244 | v = int(v) |
| 245 | |
| 246 | if v < 0: |
| 247 | v = -v |
| 248 | x, z = z, x |
| 249 | |
| 250 | m, n = simplify(int(v), 180) |
| 251 | args = [y, z, y, x, f'{m}pi/{n}'] |
| 252 | |
| 253 | p2deps[points].append(hashed_txt(name, args)) |
| 254 | |
| 255 | for k, v in p2deps.items(): |
| 256 | p2deps[k] = sort_deps(v) |
| 257 | |
| 258 | points = clause.points |
| 259 | while points: |
| 260 | p = points[0] |
| 261 | gr = group[p] |
| 262 | points = [x for x in points if x not in gr] |
| 263 | |
| 264 | deps_str = [] |
| 265 | for dep in p2deps[gr]: |
| 266 | ref_str = '{:02}'.format(ref) |
| 267 | dep_str = pt.pretty(dep) |
| 268 | |
| 269 | if dep[0] == 'aconst': |
| 270 | m, n = map(int, dep[-1].split('pi/')) |
| 271 | mn = f'{m}. pi / {n}.' |
| 272 | dep_str = ' '.join(dep_str.split()[:-1] + [mn]) |
| 273 | |
| 274 | deps_str.append(dep_str + ' ' + ref_str) |