From 25bd83f0324009520c25547e0706c66572e9a0ef Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Mon, 12 Jan 2026 16:55:37 -0500 Subject: [PATCH] Check VSP for non-MaGICal models via SMT --- model.py | 11 ++++++-- parse_magic.py | 2 +- smt.py | 56 +++++++++++++++++++++++++++++++++++- vsp.py | 77 ++++++++++++++++++++++++++++++++++++++++++++++++-- 4 files changed, 140 insertions(+), 6 deletions(-) diff --git a/model.py b/model.py index 9c93c1e..807f1ec 100644 --- a/model.py +++ b/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): diff --git a/parse_magic.py b/parse_magic.py index 78fc495..29cec8b 100644 --- a/parse_magic.py +++ b/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) diff --git a/smt.py b/smt.py index f6f2c33..f94d49e 100644 --- a/smt.py +++ b/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) \ No newline at end of file + 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) diff --git a/vsp.py b/vsp.py index 034005f..86bad4d 100644 --- a/vsp.py +++ b/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)