From 30ad57c8670264f504fa9ef49d9201678fb91076 Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Tue, 12 Nov 2024 15:18:57 -0500
Subject: [PATCH] Only discard when top is in the right subalgebra or bottom is
 in the left

---
 model.py | 26 ++++++++++----------------
 vsp.py   | 18 +++++++-----------
 2 files changed, 17 insertions(+), 27 deletions(-)

diff --git a/model.py b/model.py
index d15d094..1860c70 100644
--- a/model.py
+++ b/model.py
@@ -219,7 +219,7 @@ def satisfiable(logic: Logic, model: Model, interpretation: Dict[Operation, Mode
 
 
 
-def model_closure(initial_set: Set[ModelValue], mfunctions: Set[ModelFunction], top: Optional[ModelValue], bottom: Optional[ModelValue]) -> Set[ModelValue]:
+def model_closure(initial_set: Set[ModelValue], mfunctions: Set[ModelFunction], forbidden_element: Optional[ModelValue]) -> Set[ModelValue]:
     """
     Given an initial set of model values and a set of model functions,
     compute the complete set of model values that are closed
@@ -230,7 +230,7 @@ def model_closure(initial_set: Set[ModelValue], mfunctions: Set[ModelFunction],
     closure_set: Set[ModelValue] = initial_set
     last_new: Set[ModelValue] = initial_set
     changed: bool = True
-    topbottom_found = False
+    forbidden_found = False
 
     while changed:
         changed = False
@@ -256,14 +256,11 @@ def model_closure(initial_set: Set[ModelValue], mfunctions: Set[ModelFunction],
 
                     # Optimization: Break out of computation
                     # early when top or bottom element is foun
-                    if top is not None and element == top:
-                        topbottom_found = True
-                    if bottom is not None and element == bottom:
-                        topbottom_found = True
-                    if topbottom_found:
+                    if forbidden_element is not None and element == forbidden_element:
+                        forbidden_found = True
                         break
 
-                if topbottom_found:
+                if forbidden_found:
                     break
 
                 # We don't need to compute the arguments
@@ -291,17 +288,14 @@ def model_closure(initial_set: Set[ModelValue], mfunctions: Set[ModelFunction],
 
                         # Optimization: Break out of computation
                         # early when top or bottom element is foun
-                        if top is not None and element == top:
-                            topbottom_found = True
-                        if bottom is not None and element == bottom:
-                            topbottom_found = True
-                        if topbottom_found:
+                        if forbidden_element is not None and element == forbidden_element:
+                            forbidden_found = True
                             break
 
-                    if topbottom_found:
+                    if forbidden_found:
                         break
 
-                if topbottom_found:
+                if forbidden_found:
                     break
 
 
@@ -309,7 +303,7 @@ def model_closure(initial_set: Set[ModelValue], mfunctions: Set[ModelFunction],
         changed = len(new_elements) > 0
         last_new = new_elements
 
-        if topbottom_found:
+        if forbidden_found:
             break
 
     return closure_set
diff --git a/vsp.py b/vsp.py
index 5c00aff..7420b68 100644
--- a/vsp.py
+++ b/vsp.py
@@ -145,30 +145,28 @@ def has_vsp(model: Model, interpretation: Dict[Operation, ModelFunction]) -> VSP
             continue
 
         # NOTE: Optimization
-        # if either subalgebra contains top or bottom, move
-        # onto the next pair
-        if top is not None and (top in xs or top in ys):
+        # If the left subalgebra contains bottom
+        # or the right subalgebra contains top
+        # skip this pair
+        if top is not None and top in ys:
             continue
-        if bottom is not None and (bottom in xs or bottom in ys):
+        if bottom is not None and bottom in xs:
             continue
 
         # Compute the closure of all operations
         # with just the xs
-        carrier_set_left: Set[ModelValue] = model_closure(xs, model.logical_operations, top, bottom)
+        carrier_set_left: Set[ModelValue] = model_closure(xs, model.logical_operations, bottom)
 
         # Save to cache
         if cached_xs[0] is not None and not cached_ys[1]:
             closure_cache.append((orig_xs, carrier_set_left))
 
-        if top is not None and top in carrier_set_left:
-            continue
         if bottom is not None and bottom in carrier_set_left:
             continue
 
-
         # Compute the closure of all operations
         # with just the ys
-        carrier_set_right: Set[ModelValue] = model_closure(ys, model.logical_operations, top, bottom)
+        carrier_set_right: Set[ModelValue] = model_closure(ys, model.logical_operations, top)
 
         # Save to cache
         if cached_ys[0] is not None and not cached_ys[1]:
@@ -176,8 +174,6 @@ def has_vsp(model: Model, interpretation: Dict[Operation, ModelFunction]) -> VSP
 
         if top is not None and top in carrier_set_right:
             continue
-        if bottom is not None and bottom in carrier_set_right:
-            continue
 
         # If the carrier set intersects, then move on to the next
         # subalgebra