One construction (>= 1 predicate).
| 67 | |
| 68 | |
| 69 | class Clause: |
| 70 | """One construction (>= 1 predicate).""" |
| 71 | |
| 72 | @classmethod |
| 73 | def from_txt(cls, data: str) -> Clause: |
| 74 | if data == ' =': |
| 75 | return Clause([], []) |
| 76 | points, constructions = data.split(' = ') |
| 77 | return Clause( |
| 78 | points.split(' '), |
| 79 | [Construction.from_txt(c) for c in constructions.split(', ')], |
| 80 | ) |
| 81 | |
| 82 | def __init__(self, points: list[str], constructions: list[Construction]): |
| 83 | self.points = [] |
| 84 | self.nums = [] |
| 85 | |
| 86 | for p in points: |
| 87 | num = None |
| 88 | if isinstance(p, str) and '@' in p: |
| 89 | p, num = p.split('@') |
| 90 | x, y = num.split('_') |
| 91 | num = float(x), float(y) |
| 92 | self.points.append(p) |
| 93 | self.nums.append(num) |
| 94 | |
| 95 | self.constructions = constructions |
| 96 | |
| 97 | def translate(self, mapping: dict[str, str]) -> Clause: |
| 98 | points0 = [] |
| 99 | for p in self.points: |
| 100 | pcount = len(mapping) + 1 |
| 101 | name = chr(96 + pcount) |
| 102 | if name > 'z': # pcount = 26 -> name = 'z' |
| 103 | name = chr(97 + (pcount - 1) % 26) + str((pcount - 1) // 26) |
| 104 | |
| 105 | p0 = mapping.get(p, name) |
| 106 | mapping[p] = p0 |
| 107 | points0.append(p0) |
| 108 | return Clause(points0, [c.translate(mapping) for c in self.constructions]) |
| 109 | |
| 110 | def add(self, name: str, args: list[str]) -> None: |
| 111 | self.constructions.append(Construction(name, args)) |
| 112 | |
| 113 | def txt(self) -> str: |
| 114 | return ( |
| 115 | ' '.join(self.points) |
| 116 | + ' = ' |
| 117 | + ', '.join(c.txt() for c in self.constructions) |
| 118 | ) |
| 119 | |
| 120 | |
| 121 | def _gcd(x: int, y: int) -> int: |