Check VSP for non-MaGICal models via SMT

model.py

@@ -187,17 +187,24 @@ class Model:
             logical_operations: Set[ModelFunction],
             designated_values: Set[ModelValue],
             ordering: Optional[OrderTable] = None,
-            name: Optional[str] = None
+            name: Optional[str] = None,
+            is_magical: Optional[bool] = False
     ):
         assert designated_values <= carrier_set
         self.carrier_set = carrier_set
         self.logical_operations = logical_operations
         self.designated_values = designated_values
         self.ordering = ordering
+        # NOTE: is_magical denotes that the model
+        # comes from the software MaGIC which
+        # means we can assume several things about
+        # it's structure. See vsp.py for it's usage.
+        self.is_magical = is_magical
         self.name = str(abs(hash((
             frozenset(carrier_set),
             frozenset(logical_operations),
-            frozenset(designated_values)
+            frozenset(designated_values),
+            is_magical
         ))))[:5] if name is None else name
 
     def __str__(self):

parse_magic.py

@@ -107,7 +107,7 @@ class ModelBuilder:
                 op = Operation(custom_mf.operation_name, custom_mf.arity)
                 interpretation[op] = custom_mf
 
-        model = Model(set(self.carrier_list), logical_operations, self.designated_values, ordering=self.ordering, name=model_name)
+        model = Model(set(self.carrier_list), logical_operations, self.designated_values, ordering=self.ordering, name=model_name, is_magical=True)
         return (model, interpretation)
 
 

smt.py

@@ -322,4 +322,58 @@ def find_all_models(logic: Logic, size: int) -> Generator[Model, None, None]:
 
         # Add constraint to exclude this model from future solutions
         exclusion_constraint = encoder.create_exclusion_constraint(model)
-        encoder.solver.add(exclusion_constraint)
+        encoder.solver.add(exclusion_constraint)
+
+class SMTModelEncoder:
+    """
+    Creates an SMT encoding for a specific Model.
+    This can be used for checking whether a model satisfies
+    various constraints.
+    """
+
+    def __init__(self, model: Model):
+        self.model = model
+        self.size = len(model.carrier_set)
+
+        # Create the Z3 context and solver
+        self.ctx = Context()
+        self.solver = Solver(ctx=self.ctx)
+
+        # Encode model values
+        model_value_names = [model_value.name for model_value in model.carrier_set]
+        self.carrier_sort, self.smt_carrier_set = EnumSort(
+            "C", model_value_names, ctx=self.ctx
+        )
+
+        # Create mapping from ModelValue to SMT element
+        self.model_value_to_smt = {
+            ModelValue(str(smt_elem)): smt_elem
+            for smt_elem in self.smt_carrier_set
+        }
+
+        # Encode model functions
+        self.model_function_map: Dict[ModelFunction, z3.FuncDeclRel] = {}
+        for model_fn in model.logical_operations:
+            smt_fn = self.create_function(model_fn.operation_name, model_fn.arity)
+            self.model_function_map[model_fn] = smt_fn
+            self.add_function_constraints_from_table(smt_fn, model_fn)
+
+
+        # Encode designated values
+        self.is_designated = self.create_predicate("D", 1)
+
+        for model_value in model.carrier_set:
+            is_designated = model_value in model.designated_values
+            self.solver.add(self.is_designated(self.model_value_to_smt[model_value]) == is_designated)
+
+    def create_predicate(self, name: str, arity: int) -> z3.FuncDeclRef:
+        return Function(name, *(self.carrier_sort for _ in range(arity)), BoolSort(ctx=self.ctx))
+
+    def create_function(self, name: str, arity: int) -> z3.FuncDeclRef:
+        return Function(name, *(self.carrier_sort for _ in range(arity + 1)))
+
+    def add_function_constraints_from_table(self, smt_fn: z3.FuncDeclRef, model_fn: ModelFunction):
+        for inputs, output in model_fn.mapping.items():
+            smt_inputs = tuple(self.model_value_to_smt[inp] for inp in inputs)
+            smt_output = self.model_value_to_smt[output]
+            self.solver.add(smt_fn(*smt_inputs) == smt_output)

vsp.py

@@ -9,6 +9,13 @@ from model import (
     Model, model_closure, ModelFunction, ModelValue
 )
 
+SMT_LOADED = True
+try:
+    from z3 import And, Or, Implies, sat
+    from smt import SMTModelEncoder
+except ImportError:
+    SMT_LOADED = False
+
 class VSP_Result:
     def __init__(
             self, has_vsp: bool, model_name: Optional[str] = None,
@@ -27,10 +34,10 @@ Subalgebra 1: {set_to_str(self.subalgebra1)}
 Subalgebra 2: {set_to_str(self.subalgebra2)}
 """
 
-def has_vsp(model: Model, impfunction: ModelFunction,
+def has_vsp_magical(model: Model, impfunction: ModelFunction,
             negation_defined: bool) -> VSP_Result:
     """
-    Checks whether a model has the variable
+    Checks whether a MaGIC model has the variable
     sharing property.
     """
     # NOTE: No models with only one designated
@@ -121,3 +128,69 @@ def has_vsp(model: Model, impfunction: ModelFunction,
             return VSP_Result(True, model.name, carrier_set_left, carrier_set_right)
 
     return VSP_Result(False, model.name)
+
+def has_vsp_smt(model: Model, impfn: ModelFunction) -> VSP_Result:
+    """
+    Checks whether a given model satisfies the variable
+    sharing property via SMT
+    """
+    if not SMT_LOADED:
+        raise Exception("Z3 is not property installed, cannot check via SMT")
+
+    encoder = SMTModelEncoder(model)
+
+    # Create predicates for our two subalgebras
+    IsInK1 = encoder.create_predicate("IsInK1", 1)
+    IsInK2 = encoder.create_predicate("IsInK2", 1)
+
+    # Enforce that our two subalgebras 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 model_fn, smt_fn in encoder.model_function_map.items():
+        for xs in product(encoder.smt_carrier_set, repeat=model_fn.arity):
+            encoder.solver.add(
+                Implies(
+                    And([IsInK1(x) for x in xs]),
+                    IsInK1(smt_fn(*xs))
+                )
+            )
+            encoder.solver.add(
+                Implies(
+                    And([IsInK2(x) for x in xs]),
+                    IsInK2(smt_fn(*xs))
+                )
+            )
+
+    # x -> y is non-designated
+    smt_imp = encoder.model_function_map[impfn]
+    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(smt_imp(x, y)) == False
+            )
+        )
+
+    # Execute solver
+    if encoder.solver.check() == sat:
+        # Extract subalgebras
+        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 VSP_Result(True, model.name, K1, K2)
+    else:
+        return VSP_Result(False, model.name)
+
+
+def has_vsp(model: Model, impfunction: ModelFunction,
+            negation_defined: bool) -> VSP_Result:
+    if model.is_magical:
+        return has_vsp_magical(model, impfunction, negation_defined)
+
+    return has_vsp_smt(model)