From bed3d09f4abcb9c4c98784af3df757dfeed9912c Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Thu, 24 Oct 2024 21:38:36 -0400
Subject: [PATCH] Check for top and bottom within subalgebra

---
 vsp.py | 49 ++++++++++++++++++++++++++++++-------------------
 1 file changed, 30 insertions(+), 19 deletions(-)

diff --git a/vsp.py b/vsp.py
index 52d9f43..27994c0 100644
--- a/vsp.py
+++ b/vsp.py
@@ -38,31 +38,38 @@ def preseed(
     same_set = candidate_preseed[1] == 0
     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
-    contains a top or bottom element.
-
-    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
+    Find the top of the order lattice.
+    T || a = T, T && a = a for all a in the carrier set
     """
     if mconjunction is None or mdisjunction is None:
-        return False
+        return None
 
-    for x in subalgebra:
-        if mconjunction(x, x) == x:
-            # print("Bottom Element Found")
-            return True
+    for x in algebra:
+        for y in algebra:
+            if mdisjunction(x, y) == x and mconjunction(x, y) == y:
+                return x
 
-        if mdisjunction(x, x) == x:
-            # print("Top Element Found")
-            return True
+    print("[Warning] Failed to find the top of the lattice")
+    return None
 
-    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:
@@ -91,6 +98,8 @@ def has_vsp(model: Model, interpretation: Dict[Operation, ModelFunction]) -> VSP
     impfunction = interpretation[Implication]
     mconjunction = interpretation.get(Conjunction)
     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
     # x -> y does not take a designiated value
@@ -133,7 +142,9 @@ def has_vsp(model: Model, interpretation: Dict[Operation, ModelFunction]) -> VSP
         # NOTE: Optimization
         # if either subalgebra contains top or bottom, move
         # 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
 
         # Compute the closure of all operations