| 12 | |
| 13 | |
| 14 | class UniverseSolver: |
| 15 | universe_vars: dict[Universe, int] |
| 16 | var_counter: Iterator[int] |
| 17 | solver: Solver |
| 18 | no_warn: set[Universe] |
| 19 | |
| 20 | def __init__(self): |
| 21 | self.solver = Solver(name="g4") |
| 22 | self.var_counter = itertools.count(start=1) |
| 23 | self.universe_vars = defaultdict(lambda: next(self.var_counter)) |
| 24 | self.no_warn = set() |
| 25 | |
| 26 | def register_as_equal(self, left: Universe, right: Universe) -> None: |
| 27 | self._register_as_equal(left, right) |
| 28 | self._validate_nonempty_universes() |
| 29 | |
| 30 | def _register_as_equal(self, left: Universe, right: Universe) -> None: |
| 31 | self._register_as_subset(left, right) |
| 32 | self._register_as_subset(right, left) |
| 33 | |
| 34 | def register_as_subset(self, subset: Universe, superset: Universe) -> None: |
| 35 | self._register_as_subset(subset, superset) |
| 36 | self._validate_nonempty_universes() |
| 37 | |
| 38 | def _register_as_subset(self, subset: Universe, superset: Universe) -> None: |
| 39 | varA = self.universe_vars[subset] |
| 40 | varB = self.universe_vars[superset] |
| 41 | # varA => varB |
| 42 | self.solver.add_clause([-varA, varB]) |
| 43 | |
| 44 | def get_subset(self, superset: Universe) -> Universe: |
| 45 | subset = Universe() |
| 46 | self.register_as_subset(subset, superset) |
| 47 | return subset |
| 48 | |
| 49 | def get_superset(self, subset: Universe) -> Universe: |
| 50 | superset = Universe() |
| 51 | self.register_as_subset(subset, superset) |
| 52 | return superset |
| 53 | |
| 54 | def register_as_difference( |
| 55 | self, result: Universe, setLeft: Universe, setRight: Universe |
| 56 | ) -> None: |
| 57 | self._register_as_difference(result, setLeft, setRight) |
| 58 | self._validate_nonempty_universes() |
| 59 | |
| 60 | def _register_as_difference( |
| 61 | self, result: Universe, setLeft: Universe, setRight: Universe |
| 62 | ) -> None: |
| 63 | """result = setLeft - setRight""" |
| 64 | self._register_as_subset(result, setLeft) |
| 65 | self._register_as_disjoint(result, setRight) |
| 66 | varResult = self.universe_vars[result] |
| 67 | varLeft = self.universe_vars[setLeft] |
| 68 | varRight = self.universe_vars[setRight] |
| 69 | # (varLeft and ~varRight) => varResult |
| 70 | self.solver.add_clause([varResult, -varLeft, varRight]) |
| 71 | |