diff --git a/model.py b/model.py index 508fe84..39498f7 100644 --- a/model.py +++ b/model.py @@ -108,16 +108,58 @@ Interpretation = Dict[Operation, ModelFunction] # Something like x : (all elements less than x) class OrderTable: def __init__(self): - self.ordering = set() + # a : {x | x <= a } + self.ordering: Dict[ModelValue, Set[ModelValue]] = defaultdict(set) def add(self, x, y): """ Add x <= y """ - self.ordering.add((x, y)) + self.ordering[y].add(x) def is_lt(self, x, y): - return (x, y) in self.ordering + return y in self.ordering[x] + + def meet(self, x, y) -> Optional[ModelValue]: + X = self.ordering[x] + Y = self.ordering[y] + + candidates = X.intersection(Y) + + for m in candidates: + gt_all_candidates = True + for w in candidates: + if not self.is_lt(w, m): + gt_all_candidates = False + break + + if gt_all_candidates: + return m + + # Otherwise the meet does not exist + print("Meet does not exist", (x, y), candidates) + return None + + def join(self, x, y) -> Optional[ModelValue]: + # Grab the collection of elements greater than x and y + candidates = set() + for w in self.ordering: + if self.is_lt(x, w) and self.is_lt(y, w): + candidates.add(w) + + for j in candidates: + lt_all_candidates = True + for w in candidates: + if not self.is_lt(j, w): + lt_all_candidates = False + break + + if lt_all_candidates: + return j + + # Otherwise the join does not exist + print("Join does not exist", (x, y), candidates) + return None class Model: diff --git a/parse_magic.py b/parse_magic.py index e4f1daa..758d735 100644 --- a/parse_magic.py +++ b/parse_magic.py @@ -507,18 +507,23 @@ def parse_single_order(infile: SourceFile, size: int, carrier_list: List[ModelVa dmapping = {} for x, y in product(carrier_list, carrier_list): - cresult = determine_cresult(size, omapping, x, y) + cresult = ordering.meet(x, y) if cresult is None: print("[Warning] Conjunction and Disjunction are not well-defined") print(f"{x} ∧ {y} = ??") return None, None + else: + print(f"{x} ∧ {y} = {cresult}") cmapping[(x, y)] = cresult - dresult = determine_dresult(size, omapping, x, y) + dresult = ordering.join(x, y) + # dresult = determine_dresult(size, omapping, x, y) if dresult is None: print("[Warning] Conjunction and Disjunction are not well-defined") print(f"{x} ∨ {y} = ??") return None, None + else: + print(f"{x} ∨ {y} = {dresult}") dmapping[(x, y)] = dresult mconjunction = ModelFunction(2, cmapping, "∧")