(#40) Consider less subalgebras

vsp.py

@@ -2,54 +2,13 @@
 Check to see if the model has the variable
 sharing property.
 """
-from collections import defaultdict
+from itertools import product
-from itertools import chain, combinations, product
 from typing import List, Optional, Set, Tuple
 from common import set_to_str
 from model import (
-    Model, model_closure, ModelFunction, ModelValue, OrderTable
+    Model, model_closure, ModelFunction, ModelValue
 )
 
-class Cache:
-    def __init__(self):
-        # input size -> cached (inputs, outputs)
-        self.c = defaultdict(list)
-
-    def add(self, i: Set[ModelValue], o: Set[ModelValue]):
-        self.c[len(i)].append((i, o))
-
-    def get_closest(self, initial_set: Set[ModelValue]) -> Optional[Tuple[Set[ModelValue], bool]]:
-        """
-        Iterate through our cache starting with the cached
-        inputs closest in size to the initial_set and
-        find the one that's a subset of initial_set.
-
-        Returns cached_output, and whether the initial_set is the same
-        as the cached_input.
-        """
-        initial_set_size = len(initial_set)
-        sizes = range(initial_set_size, 0, -1)
-
-        for size in sizes:
-            if size not in self.c:
-                continue
-
-            for cached_input, cached_output in self.c[size]:
-                if cached_input <= initial_set:
-                    return cached_output, size == initial_set_size
-
-        return None
-
-def order_dependent(subalgebra1: Set[ModelValue], subalegbra2: Set[ModelValue], ordering: OrderTable):
-    """
-    Returns true if there exists a value in subalgebra1 that's less than a value in subalgebra2
-    """
-    for x in subalgebra1:
-        for y in subalegbra2:
-            if ordering.is_lt(x, y):
-                return True
-    return False
-
 class VSP_Result:
     def __init__(
             self, has_vsp: bool, model_name: Optional[str] = None,
@@ -68,38 +27,6 @@ Subalgebra 1: {set_to_str(self.subalgebra1)}
 Subalgebra 2: {set_to_str(self.subalgebra2)}
 """
 
-def quick_vsp_unsat_incomplete(xs, ys, model, top, bottom, negation_defined) -> bool:
-    """
-    Return True if VSP cannot be satisfied
-    through some incomplete checks.
-    """
-    # If the left subalgebra contains bottom
-    # or the right subalgebra contains top
-    # skip this pair
-    if top is not None and top in ys:
-        return True
-    if negation_defined and bottom is not None and bottom in ys:
-        return True
-    if bottom is not None and bottom in xs:
-        return True
-    if negation_defined and top is not None and top in xs:
-        return True
-
-    # If the two subalgebras intersect, move
-    # onto the next pair.
-    if not xs.isdisjoint(ys):
-        return True
-
-    # If the subalgebras are order-dependent, skip this pair
-    if order_dependent(xs, ys, model.ordering):
-        return True
-    if negation_defined and order_dependent(ys, xs, model.ordering):
-        return True
-
-    # We can't immediately rule out that these
-    # subalgebras don't exhibit VSP
-    return False
-
 def has_vsp(model: Model, impfunction: ModelFunction,
             negation_defined: bool) -> VSP_Result:
     """
@@ -124,64 +51,66 @@ def has_vsp(model: Model, impfunction: ModelFunction,
         if impfunction(x, y) not in model.designated_values:
             I.append((x, y))
 
-    # Construct the powerset of I without the empty set
-    I_power = chain.from_iterable(combinations(I, r) for r in range(1, len(I) + 1))
-    # ((x1, y1)), ((x1, y1), (x2, y2)), ...
-
-    closure_cache = Cache()
-
     # Find the subalgebras which falsify implication
-    for xys in I_power:
+    for xys in I:
 
-        xs = { xy[0] for xy in xys }
+        xi = xys[0]
-        ys = { xy[1] for xy in xys }
 
-        if quick_vsp_unsat_incomplete(xs, ys, model, top, bottom, negation_defined):
+        # Discard ({⊥} ∪ A', B) subalgebras
+        if bottom is not None and xi == bottom:
             continue
 
-        orig_xs = xs
+        # Discard ({⊤} ∪ A', B) subalgebras when negation is defined
-        cached_xs = closure_cache.get_closest(xs)
+        if top is not None and negation_defined and xi == top:
-        if cached_xs is not None:
-            xs |= cached_xs[0]
-
-        orig_ys = ys
-        cached_ys = closure_cache.get_closest(ys)
-        if cached_ys is not None:
-            ys |= cached_ys[0]
-
-        xs_ys_updated = cached_xs is not None or cached_ys is not None
-        if xs_ys_updated and quick_vsp_unsat_incomplete(xs, ys, model, top, bottom, negation_defined):
             continue
 
-        # Compute the closure of all operations
+        yi = xys[1]
-        # with just the xs
-        carrier_set_left: Set[ModelValue] = model_closure(xs, model.logical_operations, bottom)
 
-        # Save to cache
+        # Discard (A, {⊤} ∪ B') subalgebras
-        if cached_xs is None or (cached_xs is not None and not cached_xs[1]):
+        if top is not None and yi == top:
-            closure_cache.add(orig_xs, carrier_set_left)
+            continue
 
+        # Discard (A, {⊥} ∪ B') subalgebras when negation is defined
+        if bottom is not None and negation_defined and yi == bottom:
+            continue
+
+        # Discard ({a} ∪ A', {b} ∪ B') subalgebras when a <= b
+        if model.ordering.is_lt(xi, yi):
+            continue
+
+        # Discard ({a} ∪ A', {b} ∪ B') subalgebras when b <= a and negation is defined
+        if negation_defined and model.ordering.is_lt(yi, xi):
+            continue
+
+        # Compute the left closure of the set containing xi under all the operations
+        carrier_set_left: Set[ModelValue] = model_closure({xi,}, model.logical_operations, bottom)
+
+        # Discard ({⊥} ∪ A', B) subalgebras
         if bottom is not None and bottom in carrier_set_left:
             continue
 
+        # Discard ({⊤} ∪ A', B) subalgebras when negation is defined
+        if top is not None and negation_defined and top 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)
+        carrier_set_right: Set[ModelValue] = model_closure({yi,}, model.logical_operations, top)
-
-        # Save to cache
-        if cached_ys is None or (cached_ys is not None and not cached_ys[1]):
-            closure_cache.add(orig_ys, carrier_set_right)
 
+        # Discard (A, {⊤} ∪ B') subalgebras
         if top is not None and top in carrier_set_right:
             continue
 
-        # If the carrier set intersects, then move on to the next
+        # Discard (A, {⊥} ∪ B') subalgebras when negation is defined
-        # subalgebra
+        if bottom is not None and negation_defined and bottom in carrier_set_right:
+            continue
+
+        # Discard subalgebras that intersect
         if not carrier_set_left.isdisjoint(carrier_set_right):
             continue
 
-        # See if for all pairs in the subalgebras, that
+        # Check whether for all pairs in the subalgebra,
-        # implication is falsified
+        # that implication is falsified.
         falsified = True
         for (x2, y2) in product(carrier_set_left, carrier_set_right):
             if impfunction(x2, y2) in model.designated_values: