From 4150ac2a7a75974cf30492732127510e5a95b8a4 Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Thu, 15 Jan 2026 15:03:18 -0500
Subject: [PATCH] Added logic_has_vsp which uses the SMTLogicEncoder

---
 smt.py | 10 ++------
 vsp.py | 75 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++-
 2 files changed, 76 insertions(+), 9 deletions(-)

diff --git a/smt.py b/smt.py
index 73e2d67..0be7af6 100644
--- a/smt.py
+++ b/smt.py
@@ -221,12 +221,6 @@ class SMTLogicEncoder:
     def create_exclusion_constraint(self, model: Model) -> z3.BoolRef:
         """
         Create a constraint that excludes the given model from future solutions.
-
-        Args:
-            model: The model to exclude
-
-        Returns:
-            An SMT constraint ensuring at least one aspect differs
         """
         constraints = []
 
@@ -245,7 +239,7 @@ class SMTLogicEncoder:
                 smt_inputs = tuple(model_value_to_smt[inp] for inp in inputs)
                 smt_output = model_value_to_smt[output]
 
-                # This input->output mapping should differ
+                # For future models the input->output mapping may differ
                 constraints.append(smt_func(*smt_inputs) != smt_output)
 
         # Exclude designated value set
@@ -253,7 +247,7 @@ class SMTLogicEncoder:
             model_val = ModelValue(str(smt_elem))
             is_designated_in_model = model_val in model.designated_values
 
-            # Designation should differ
+            # Designation may differ
             if is_designated_in_model:
                 constraints.append(self.is_designated(smt_elem) == False)
             else:
diff --git a/vsp.py b/vsp.py
index 86bad4d..ee87657 100644
--- a/vsp.py
+++ b/vsp.py
@@ -5,6 +5,7 @@ sharing property.
 from itertools import product
 from typing import List, Optional, Set, Tuple
 from common import set_to_str
+from logic import Logic, Implication
 from model import (
     Model, model_closure, ModelFunction, ModelValue
 )
@@ -12,7 +13,7 @@ from model import (
 SMT_LOADED = True
 try:
     from z3 import And, Or, Implies, sat
-    from smt import SMTModelEncoder
+    from smt import SMTModelEncoder, SMTLogicEncoder
 except ImportError:
     SMT_LOADED = False
 
@@ -194,3 +195,75 @@ def has_vsp(model: Model, impfunction: ModelFunction,
         return has_vsp_magical(model, impfunction, negation_defined)
 
     return has_vsp_smt(model)
+
+
+def logic_has_vsp(logic: Logic, size: int) -> Optional[Tuple[Model, VSP_Result]]:
+    """
+    Checks whether a given logic satisfies
+    the variable sharing property by looking
+    for a many-valued matrix of a specific size.
+
+    If the logic does witness the VSP, then
+    this function will return the matrix model
+    and the subalgebras that witness it.
+
+    Otherwise, if no matrix model of that given
+    size can be found, it will return None
+    """
+    assert size > 0
+
+    encoder = SMTLogicEncoder(logic, size)
+
+    ## The following adds constraints which satisfy the VSP
+
+    # Membership Predicates for K1/K2
+    IsInK1 = encoder.create_predicate("IsInK1", 1)
+    IsInK2 = encoder.create_predicate("IsInK2", 1)
+
+    # K1 and K2 are non-empty
+    encoder.solver.add(Or([IsInK1(x) for x in encoder.smt_carrier_set]))
+    encoder.solver.add(Or([IsInK2(x) for x in encoder.smt_carrier_set]))
+
+    # K1/K2 are closed under the operations
+    for op, SmtOp in encoder.operation_function_map.items():
+        for xs in product(encoder.smt_carrier_set, repeat=op.arity):
+            encoder.solver.add(
+                Implies(
+                    And([IsInK1(x) for x in xs]),
+                    IsInK1(SmtOp(*xs))
+                )
+            )
+            encoder.solver.add(
+                Implies(
+                    And([IsInK2(x) for x in xs]),
+                    IsInK2(SmtOp(*xs))
+                )
+            )
+
+    # x -> y is non-designated
+    Impfn = encoder.operation_function_map[Implication]
+    for (x, y) in product(encoder.smt_carrier_set, encoder.smt_carrier_set):
+        encoder.solver.add(
+            Implies(
+                And(IsInK1(x), IsInK2(y)),
+                encoder.is_designated(Impfn(x, y)) == False
+            )
+        )
+
+    model = encoder.find_model()
+
+    # We failed to find a VSP witness
+    if model is None:
+        return None
+
+    # Otherwise, a matrix model and correspoding
+    # subalgebras exist.
+
+    smt_model = encoder.solver.model()
+    K1_smt = [x for x in encoder.smt_carrier_set if smt_model.evaluate(IsInK1(x))]
+    K1 = {ModelValue(str(x)) for x in K1_smt}
+
+    K2_smt = [x for x in encoder.smt_carrier_set if smt_model.evaluate(IsInK2(x))]
+    K2 = {ModelValue(str(x)) for x in K2_smt}
+
+    return model, VSP_Result(True, model.name, K1, K2)