mirror of
https://github.com/Brandon-Rozek/matmod.git
synced 2025-07-29 20:52:01 +00:00
[Draft] Changing OrderTable (Currently non-functional)
This commit is contained in:
parent
6f5074584b
commit
fa9e5026ca
2 changed files with 52 additions and 5 deletions
48
model.py
48
model.py
|
@ -108,16 +108,58 @@ Interpretation = Dict[Operation, ModelFunction]
|
||||||
# Something like x : (all elements less than x)
|
# Something like x : (all elements less than x)
|
||||||
class OrderTable:
|
class OrderTable:
|
||||||
def __init__(self):
|
def __init__(self):
|
||||||
self.ordering = set()
|
# a : {x | x <= a }
|
||||||
|
self.ordering: Dict[ModelValue, Set[ModelValue]] = defaultdict(set)
|
||||||
|
|
||||||
def add(self, x, y):
|
def add(self, x, y):
|
||||||
"""
|
"""
|
||||||
Add x <= y
|
Add x <= y
|
||||||
"""
|
"""
|
||||||
self.ordering.add((x, y))
|
self.ordering[y].add(x)
|
||||||
|
|
||||||
def is_lt(self, x, y):
|
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:
|
class Model:
|
||||||
|
|
|
@ -507,18 +507,23 @@ def parse_single_order(infile: SourceFile, size: int, carrier_list: List[ModelVa
|
||||||
dmapping = {}
|
dmapping = {}
|
||||||
|
|
||||||
for x, y in product(carrier_list, carrier_list):
|
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:
|
if cresult is None:
|
||||||
print("[Warning] Conjunction and Disjunction are not well-defined")
|
print("[Warning] Conjunction and Disjunction are not well-defined")
|
||||||
print(f"{x} ∧ {y} = ??")
|
print(f"{x} ∧ {y} = ??")
|
||||||
return None, None
|
return None, None
|
||||||
|
else:
|
||||||
|
print(f"{x} ∧ {y} = {cresult}")
|
||||||
cmapping[(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:
|
if dresult is None:
|
||||||
print("[Warning] Conjunction and Disjunction are not well-defined")
|
print("[Warning] Conjunction and Disjunction are not well-defined")
|
||||||
print(f"{x} ∨ {y} = ??")
|
print(f"{x} ∨ {y} = ??")
|
||||||
return None, None
|
return None, None
|
||||||
|
else:
|
||||||
|
print(f"{x} ∨ {y} = {dresult}")
|
||||||
dmapping[(x, y)] = dresult
|
dmapping[(x, y)] = dresult
|
||||||
|
|
||||||
mconjunction = ModelFunction(2, cmapping, "∧")
|
mconjunction = ModelFunction(2, cmapping, "∧")
|
||||||
|
|
Loading…
Add table
Reference in a new issue