Added case for when negation is defined

vsp.py

@@ -107,7 +107,10 @@ Subalgebra 1: {set_to_str(self.subalgebra1)}
 Subalgebra 2: {set_to_str(self.subalgebra2)}
 """
 
-def has_vsp(model: Model, impfunction: ModelFunction, mconjunction: Optional[ModelFunction] = None, mdisjunction: Optional[ModelFunction] = None) -> VSP_Result:
+def has_vsp(model: Model, impfunction: ModelFunction,
+            mconjunction: Optional[ModelFunction] = None,
+            mdisjunction: Optional[ModelFunction] = None,
+            mnegation: Optional[ModelFunction] = None) -> VSP_Result:
     """
     Checks whether a model has the variable
     sharing property.
@@ -173,6 +176,8 @@ def has_vsp(model: Model, impfunction: ModelFunction, mconjunction: Optional[Mod
         # If the subalgebras are order-dependent, skip this pair
         if order_dependent(xs, ys, model.ordering):
             continue
+        if mnegation is not None and order_dependent(ys, xs, model.ordering):
+            continue
 
         # Compute the closure of all operations
         # with just the xs

vspursuer.py

@@ -3,7 +3,7 @@ from os import cpu_count
 import argparse
 import multiprocessing as mp
 
-from logic import Conjunction, Disjunction, Implication
+from logic import Conjunction, Disjunction, Negation, Implication
 from parse_magic import SourceFile, parse_matrices
 from vsp import has_vsp, VSP_Result
 
@@ -24,19 +24,20 @@ if __name__ == "__main__":
 
     # NOTE: When subprocess gets spawned, the logical operations will
     # have a different memory address than what's expected in interpretation.
-    # This will make it so that we can pass the model functions directly instead.
+    # Therefore, we need to pass the model functions directly instead.
     solutions_expanded = []
     for model, interpretation in solutions:
         impfunction = interpretation[Implication]
         mconjunction = interpretation.get(Conjunction)
         mdisjunction = interpretation.get(Disjunction)
-        solutions_expanded.append((model, impfunction, mconjunction, mdisjunction))
+        mnegation = interpretation.get(Negation)
+        solutions_expanded.append((model, impfunction, mconjunction, mdisjunction, mnegation))
 
     num_has_vsp = 0
     with mp.Pool(processes=max(cpu_count() - 2, 1)) as pool:
         results = [
-            pool.apply_async(has_vsp, (model, impfunction, mconjunction, mdisjunction,))
-            for model, impfunction, mconjunction, mdisjunction in solutions_expanded
+            pool.apply_async(has_vsp, (model, impfunction, mconjunction, mdisjunction, mnegation))
+            for model, impfunction, mconjunction, mdisjunction, mnegation in solutions_expanded
         ]
 
         for i, result in enumerate(results):