brozek/matmod
1
0
Fork 0
mirror of https://github.com/Brandon-Rozek/matmod.git synced 2024-11-20 21:56:29 -05:00
Code Issues Projects Releases Packages Wiki Activity

Check for top and bottom within subalgebra

Browse source
This commit is contained in:
Brandon Rozek 2024-10-24 21:38:36 -04:00
parent 3b535fdfa5
commit bed3d09f4a
1 changed files with 30 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

49
vsp.py
View file

@ -38,31 +38,38 @@ def preseed(
same_set = candidate_preseed[1] == 0 same_set = candidate_preseed[1] == 0
return candidate_preseed[0], same_set return candidate_preseed[0], same_set
def has_top_bottom(subalgebra: Set[ModelValue], mconjunction: Optional[ModelFunction], mdisjunction: Optional[ModelFunction]):
def find_top(algebra: Set[ModelValue], mconjunction: Optional[ModelFunction], mdisjunction: Optional[ModelFunction]) -> Optional[ModelValue]:
""" """
Checks the subalgebra to see whether it Find the top of the order lattice.
contains a top or bottom element. T || a = T, T && a = a for all a in the carrier set
Note: This does not compute the closure.
By definition,
The top element is any element x where x || x = x
The bottom element is any element x where x && x = x
""" """
if mconjunction is None or mdisjunction is None: if mconjunction is None or mdisjunction is None:
return False return None
for x in subalgebra: for x in algebra:
if mconjunction(x, x) == x: for y in algebra:
# print("Bottom Element Found") if mdisjunction(x, y) == x and mconjunction(x, y) == y:
return True return x
if mdisjunction(x, x) == x: print("[Warning] Failed to find the top of the lattice")
# print("Top Element Found") return None
return True
return False def find_bottom(algebra: Set[ModelValue], mconjunction: Optional[ModelFunction], mdisjunction: Optional[ModelFunction]) -> Optional[ModelValue]:
"""
Find the bottom of the order lattice
F || a = a, F && a = F for all a in the carrier set
"""
if mconjunction is None or mdisjunction is None:
return None
for x in algebra:
for y in algebra:
if mdisjunction(x, y) == y and mconjunction(x, y) == x:
return x
print("[Warning] Failed to find the bottom of the lattice")
return None
class VSP_Result: class VSP_Result:
@ -91,6 +98,8 @@ def has_vsp(model: Model, interpretation: Dict[Operation, ModelFunction]) -> VSP
impfunction = interpretation[Implication] impfunction = interpretation[Implication]
mconjunction = interpretation.get(Conjunction) mconjunction = interpretation.get(Conjunction)
mdisjunction = interpretation.get(Disjunction) mdisjunction = interpretation.get(Disjunction)
top = find_top(model.carrier_set, mconjunction, mdisjunction)
bottom = find_bottom(model.carrier_set, mconjunction, mdisjunction)
# Compute I the set of tuples (x, y) where # Compute I the set of tuples (x, y) where
# x -> y does not take a designiated value # x -> y does not take a designiated value
@ -133,7 +142,9 @@ def has_vsp(model: Model, interpretation: Dict[Operation, ModelFunction]) -> VSP
# NOTE: Optimization # NOTE: Optimization
# if either subalgebra contains top or bottom, move # if either subalgebra contains top or bottom, move
# onto the next pair # onto the next pair
if has_top_bottom(xs, mconjunction, mdisjunction) or has_top_bottom(ys, mconjunction, mdisjunction): if top is not None and (top in xs or top in ys):
continue
if bottom is not None and (bottom in xs or bottom in ys):
continue continue
# Compute the closure of all operations # Compute the closure of all operations