From af81342a7421f006f7da73af3c0ded50aa55c9e2 Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Wed, 30 Oct 2024 16:11:03 -0400
Subject: [PATCH] Break out of saturation computation early when top/bottom are
 found

---
 model.py | 36 +++++++++++++++++++++++++++++++++++-
 vsp.py   | 13 +++++++++++--
 2 files changed, 46 insertions(+), 3 deletions(-)

diff --git a/model.py b/model.py
index 46406b5..d15d094 100644
--- a/model.py
+++ b/model.py
@@ -219,15 +219,18 @@ def satisfiable(logic: Logic, model: Model, interpretation: Dict[Operation, Mode
 
 
 
-def model_closure(initial_set: Set[ModelValue], mfunctions: Set[ModelFunction]):
+def model_closure(initial_set: Set[ModelValue], mfunctions: Set[ModelFunction], top: Optional[ModelValue], bottom: 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
     under the operations.
+
+    If top or bottom is encountered, then we end the saturation procedure early.
     """
     closure_set: Set[ModelValue] = initial_set
     last_new: Set[ModelValue] = initial_set
     changed: bool = True
+    topbottom_found = False
 
     while changed:
         changed = False
@@ -251,6 +254,18 @@ def model_closure(initial_set: Set[ModelValue], mfunctions: Set[ModelFunction]):
                     if element not in closure_set:
                         new_elements.add(element)
 
+                    # 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:
+                        break
+
+                if topbottom_found:
+                    break
+
                 # We don't need to compute the arguments
                 # thanks to the cache, so move onto the
                 # next function.
@@ -274,8 +289,27 @@ def model_closure(initial_set: Set[ModelValue], mfunctions: Set[ModelFunction]):
                         if element not in closure_set:
                             new_elements.add(element)
 
+                        # 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:
+                            break
+
+                    if topbottom_found:
+                        break
+
+                if topbottom_found:
+                    break
+
+
         closure_set.update(new_elements)
         changed = len(new_elements) > 0
         last_new = new_elements
 
+        if topbottom_found:
+            break
+
     return closure_set
diff --git a/vsp.py b/vsp.py
index 27994c0..6982c16 100644
--- a/vsp.py
+++ b/vsp.py
@@ -149,21 +149,30 @@ def has_vsp(model: Model, interpretation: Dict[Operation, ModelFunction]) -> VSP
 
         # Compute the closure of all operations
         # with just the xs
-        carrier_set_left: Set[ModelValue] = model_closure(xs, model.logical_operations)
+        carrier_set_left: Set[ModelValue] = model_closure(xs, model.logical_operations, top, 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)
+        carrier_set_right: Set[ModelValue] = model_closure(ys, model.logical_operations, top, bottom)
 
         # Save to cache
         if cached_ys[0] is not None and not cached_ys[1]:
             closure_cache.append((orig_ys, carrier_set_right))
 
+        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