From 3610335c1c12244f7a8cca85bfba0cb0f38fbbac Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Tue, 25 Nov 2025 17:22:59 -0500 Subject: [PATCH 01/13] Added an initial model finder via Z3 --- generate_model.py | 3 ++ logic.py | 17 +++++--- smt.py | 101 ++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 115 insertions(+), 6 deletions(-) create mode 100644 smt.py diff --git a/generate_model.py b/generate_model.py index 1306adc..5a46efc 100644 --- a/generate_model.py +++ b/generate_model.py @@ -1,6 +1,9 @@ """ Generate all the models for a given logic with a specified number of elements. + +NOTE: This uses a naive brute-force method which +is extremely slow. """ from common import set_to_str from logic import Logic, Operation, Rule, get_operations_from_term diff --git a/logic.py b/logic.py index 7775590..e2024da 100644 --- a/logic.py +++ b/logic.py @@ -100,17 +100,22 @@ def get_prop_var_from_term(t: Term) -> Set[PropositionalVariable]: return result +def get_prop_vars_from_rule(r: Rule) -> Set[PropositionalVariable]: + vars: Set[PropositionalVariable] = set() + + for premise in r.premises: + vars |= get_prop_var_from_term(premise) + + vars |= get_prop_var_from_term(r.conclusion) + + return vars + @lru_cache def get_propostional_variables(rules: Tuple[Rule]) -> Set[PropositionalVariable]: vars: Set[PropositionalVariable] = set() for rule in rules: - # Get all vars in premises - for premise in rule.premises: - vars |= get_prop_var_from_term(premise) - - # Get vars in conclusion - vars |= get_prop_var_from_term(rule.conclusion) + vars |= get_prop_vars_from_rule(rule) return vars diff --git a/smt.py b/smt.py new file mode 100644 index 0000000..5a238f7 --- /dev/null +++ b/smt.py @@ -0,0 +1,101 @@ +from itertools import product +from typing import Dict, Generator, Optional, Tuple + +from logic import Logic, Operation, Rule, PropositionalVariable, Term, OpTerm, get_prop_vars_from_rule +from model import Model, ModelValue, ModelFunction + +from z3 import EnumSort, Function, BoolSort, z3, And, Implies, Solver, sat, Context + +# TODO: Add an assumption that a partial order exists over the carrier set. +# This adds three restrictions to the logic +# 1) A -> A is always designated +# 2) If A -> B is designated and B -> C is designated then A -> C is designated +# 3) If A -> B is designated and B -> A is designated then A and B share the same truth value + +def term_to_smt(t: Term, op_mapping: Dict[Operation, z3.FuncDeclRef], var_mapping: Dict[PropositionalVariable, z3.DatatypeRef]) -> z3.DatatypeRef: + if isinstance(t, PropositionalVariable): + return var_mapping[t] + + assert isinstance(t, OpTerm) + + arguments = [term_to_smt(a, op_mapping, var_mapping) for a in t.arguments] + fn = op_mapping[t.operation] + + return fn(*arguments) + + +def logic_rule_to_smt_constraints(rule: Rule, IsDesignated: z3.FuncDeclRef, smt_carrier_set, op_mapping: Dict[Operation, z3.FuncDeclRef]) -> Generator[z3.BoolRef, None, None]: + prop_vars = get_prop_vars_from_rule(rule) + + for smt_vars in product(smt_carrier_set, repeat=len(prop_vars)): + assert len(prop_vars) == len(smt_vars) + + var_mapping = { + prop_var : smt_var + for (prop_var, smt_var) in zip(prop_vars, smt_vars) + } + + premises = [IsDesignated(term_to_smt(premise, op_mapping, var_mapping)) == True for premise in rule.premises] + conclusion = IsDesignated(term_to_smt(rule.conclusion, op_mapping, var_mapping)) == True + + if len(premises) == 0: + yield conclusion + else: + premise = premises[0] + for p in premises[1:]: + premise = And(premise, p) + + yield Implies(premise, conclusion) + + +def find_model(l: Logic, size: int) -> Optional[Model]: + assert size > 0 + + ctx = Context() + solver = Solver(ctx=ctx) + + element_names = [f'{i}' for i in range(size)] + Carrier_sort, smt_carrier_set = EnumSort("C", element_names, ctx=ctx) + + operation_function_map: Dict[Operation, z3.FuncDeclRef] = {} + + for operation in l.operations: + operation_function_map[operation] = Function( + operation.symbol, + *(Carrier_sort for _ in range(operation.arity + 1)) + ) + + IsDesignated = Function("D", Carrier_sort, BoolSort(ctx=ctx)) + + for rule in l.rules: + for constraint in logic_rule_to_smt_constraints(rule, IsDesignated, smt_carrier_set, operation_function_map): + solver.add(constraint) + + smt_result = solver.check() + + if smt_result == sat: + smt_model = solver.model() + + carrier_set = {ModelValue(f"{i}") for i in range(size)} + + smt_designated = [x for x in smt_carrier_set if smt_model.evaluate(IsDesignated(x))] + designated_values = {ModelValue(str(x)) for x in smt_designated} + + model_functions = set() + for (operation, smt_function) in operation_function_map.items(): + mapping: Dict[Tuple[ModelValue], ModelValue] = {} + for smt_inputs in product(smt_carrier_set, repeat=operation.arity): + model_inputs = tuple((ModelValue(str(i)) for i in smt_inputs)) + smt_output = smt_model.evaluate(smt_function(*smt_inputs)) + model_output = ModelValue(str(smt_output)) + mapping[model_inputs] = model_output + model_functions.add(ModelFunction(operation.arity, mapping, operation.symbol, )) + + solver.reset() + del ctx + + return Model(carrier_set, model_functions, designated_values) + + + else: + return None From a5fb1b92bba80e9c0c530725e7b76e6813742483 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Fri, 12 Dec 2025 18:17:47 -0500 Subject: [PATCH 02/13] Enumerate over all models --- logic.py | 2 + smt.py | 306 +++++++++++++++++++++++++++++++++++++++++++++++-------- 2 files changed, 267 insertions(+), 41 deletions(-) diff --git a/logic.py b/logic.py index e2024da..44c5c6b 100644 --- a/logic.py +++ b/logic.py @@ -81,9 +81,11 @@ class Rule: class Logic: def __init__(self, operations: Set[Operation], rules: Set[Rule], + falsifies: Optional[Set[Rule]] = None, name: Optional[str] = None): self.operations = operations self.rules = rules + self.falsifies = falsifies self.name = str(abs(hash(( frozenset(operations), frozenset(rules) diff --git a/smt.py b/smt.py index 5a238f7..f6f2c33 100644 --- a/smt.py +++ b/smt.py @@ -4,38 +4,52 @@ from typing import Dict, Generator, Optional, Tuple from logic import Logic, Operation, Rule, PropositionalVariable, Term, OpTerm, get_prop_vars_from_rule from model import Model, ModelValue, ModelFunction -from z3 import EnumSort, Function, BoolSort, z3, And, Implies, Solver, sat, Context +from z3 import ( + And, BoolSort, Context, EnumSort, Function, Implies, Or, sat, Solver, z3 +) -# TODO: Add an assumption that a partial order exists over the carrier set. -# This adds three restrictions to the logic -# 1) A -> A is always designated -# 2) If A -> B is designated and B -> C is designated then A -> C is designated -# 3) If A -> B is designated and B -> A is designated then A and B share the same truth value - -def term_to_smt(t: Term, op_mapping: Dict[Operation, z3.FuncDeclRef], var_mapping: Dict[PropositionalVariable, z3.DatatypeRef]) -> z3.DatatypeRef: +def term_to_smt( + t: Term, + op_mapping: Dict[Operation, z3.FuncDeclRef], + var_mapping: Dict[PropositionalVariable, z3.DatatypeRef] +) -> z3.DatatypeRef: + """Convert a logic term to its SMT representation.""" if isinstance(t, PropositionalVariable): return var_mapping[t] assert isinstance(t, OpTerm) - arguments = [term_to_smt(a, op_mapping, var_mapping) for a in t.arguments] + arguments = [term_to_smt(arg, op_mapping, var_mapping) for arg in t.arguments] fn = op_mapping[t.operation] return fn(*arguments) +def logic_rule_to_smt_constraints( + rule: Rule, + IsDesignated: z3.FuncDeclRef, + smt_carrier_set, + op_mapping: Dict[Operation, z3.FuncDeclRef] +) -> Generator[z3.BoolRef, None, None]: + """ + Encode a logic rule as SMT constraints. -def logic_rule_to_smt_constraints(rule: Rule, IsDesignated: z3.FuncDeclRef, smt_carrier_set, op_mapping: Dict[Operation, z3.FuncDeclRef]) -> Generator[z3.BoolRef, None, None]: + For all valuations: if premises are designated, then conclusion is designated. + """ prop_vars = get_prop_vars_from_rule(rule) + # Requires that the rule holds under all valuations for smt_vars in product(smt_carrier_set, repeat=len(prop_vars)): assert len(prop_vars) == len(smt_vars) var_mapping = { - prop_var : smt_var + prop_var: smt_var for (prop_var, smt_var) in zip(prop_vars, smt_vars) } - premises = [IsDesignated(term_to_smt(premise, op_mapping, var_mapping)) == True for premise in rule.premises] + premises = [ + IsDesignated(term_to_smt(premise, op_mapping, var_mapping)) == True + for premise in rule.premises + ] conclusion = IsDesignated(term_to_smt(rule.conclusion, op_mapping, var_mapping)) == True if len(premises) == 0: @@ -47,55 +61,265 @@ def logic_rule_to_smt_constraints(rule: Rule, IsDesignated: z3.FuncDeclRef, smt_ yield Implies(premise, conclusion) +def logic_falsification_rule_to_smt_constraints( + rule: Rule, + IsDesignated: z3.FuncDeclRef, + smt_carrier_set, + op_mapping: Dict[Operation, z3.FuncDeclRef] +) -> z3.BoolRef: + """ + Encode a falsification rule as an SMT constraint. -def find_model(l: Logic, size: int) -> Optional[Model]: - assert size > 0 + There exists at least one valuation where premises are designated + but conclusion is not designated. + """ + prop_vars = get_prop_vars_from_rule(rule) - ctx = Context() - solver = Solver(ctx=ctx) + # Collect all possible counter-examples (valuations that falsify the rule) + counter_examples = [] - element_names = [f'{i}' for i in range(size)] - Carrier_sort, smt_carrier_set = EnumSort("C", element_names, ctx=ctx) + for smt_vars in product(smt_carrier_set, repeat=len(prop_vars)): + assert len(prop_vars) == len(smt_vars) - operation_function_map: Dict[Operation, z3.FuncDeclRef] = {} + var_mapping = { + prop_var: smt_var + for (prop_var, smt_var) in zip(prop_vars, smt_vars) + } - for operation in l.operations: - operation_function_map[operation] = Function( - operation.symbol, - *(Carrier_sort for _ in range(operation.arity + 1)) - ) + premises = [ + IsDesignated(term_to_smt(premise, op_mapping, var_mapping)) == True + for premise in rule.premises + ] + conclusion = IsDesignated(term_to_smt(rule.conclusion, op_mapping, var_mapping)) == False - IsDesignated = Function("D", Carrier_sort, BoolSort(ctx=ctx)) + if len(premises) == 0: + counter_examples.append(conclusion) + else: + premise = premises[0] + for p in premises[1:]: + premise = And(premise, p) - for rule in l.rules: - for constraint in logic_rule_to_smt_constraints(rule, IsDesignated, smt_carrier_set, operation_function_map): - solver.add(constraint) + counter_examples.append(And(premise, conclusion)) - smt_result = solver.check() + # At least one counter-example must exist (disjunction of all possibilities) + return Or(counter_examples) - if smt_result == sat: - smt_model = solver.model() - carrier_set = {ModelValue(f"{i}") for i in range(size)} +class SMTLogicEncoder: + """ + Encapsulates the SMT encoding of a logic system with a fixed carrier set size. - smt_designated = [x for x in smt_carrier_set if smt_model.evaluate(IsDesignated(x))] + This class handles: + - Creating the SMT sorts and functions + - Encoding logic rules as SMT constraints + - Managing the solver state + - Converting between Model objects and SMT representations + """ + + def __init__(self, logic: Logic, size: int): + """ + Initialize the SMT encoding for a logic with given carrier set size. + + Args: + logic: The logic system to encode + size: The size of the carrier set + """ + assert size > 0 + + self.logic = logic + self.size = size + + # Create Z3 context and solver + self.ctx = Context() + self.solver = Solver(ctx=self.ctx) + + # Create carrier set + element_names = [f'{i}' for i in range(size)] + self.carrier_sort, self.smt_carrier_set = EnumSort("C", element_names, ctx=self.ctx) + + # Create operation functions + self.operation_function_map: Dict[Operation, z3.FuncDeclRef] = {} + for operation in logic.operations: + self.operation_function_map[operation] = Function( + operation.symbol, + *(self.carrier_sort for _ in range(operation.arity + 1)) + ) + + # Create designation function + self.is_designated = Function("D", self.carrier_sort, BoolSort(ctx=self.ctx)) + + # Add logic rules as constraints + self._add_logic_constraints() + self._add_designation_symmetry_constraints() + + def _add_logic_constraints(self): + """Add all logic rules and falsification rules as SMT constraints.""" + # Add regular rules + for rule in self.logic.rules: + for constraint in logic_rule_to_smt_constraints( + rule, + self.is_designated, + self.smt_carrier_set, + self.operation_function_map + ): + self.solver.add(constraint) + + # Add falsification rules + for falsification_rule in self.logic.falsifies: + constraint = logic_falsification_rule_to_smt_constraints( + falsification_rule, + self.is_designated, + self.smt_carrier_set, + self.operation_function_map + ) + self.solver.add(constraint) + + def extract_model(self, smt_model) -> Model: + """ + Extract a Model object from an SMT model. + + Args: + smt_model: The Z3 model to extract from + + Returns: + A Model object representing the logic model + """ + carrier_set = {ModelValue(f"{i}") for i in range(self.size)} + + # Extract designated values + smt_designated = [ + x for x in self.smt_carrier_set + if smt_model.evaluate(self.is_designated(x)) + ] designated_values = {ModelValue(str(x)) for x in smt_designated} + # Extract operation functions model_functions = set() - for (operation, smt_function) in operation_function_map.items(): + for (operation, smt_function) in self.operation_function_map.items(): mapping: Dict[Tuple[ModelValue], ModelValue] = {} - for smt_inputs in product(smt_carrier_set, repeat=operation.arity): - model_inputs = tuple((ModelValue(str(i)) for i in smt_inputs)) + for smt_inputs in product(self.smt_carrier_set, repeat=operation.arity): + model_inputs = tuple(ModelValue(str(i)) for i in smt_inputs) smt_output = smt_model.evaluate(smt_function(*smt_inputs)) model_output = ModelValue(str(smt_output)) mapping[model_inputs] = model_output - model_functions.add(ModelFunction(operation.arity, mapping, operation.symbol, )) - - solver.reset() - del ctx + model_functions.add(ModelFunction(operation.arity, mapping, operation.symbol)) return Model(carrier_set, model_functions, designated_values) - else: + def _add_designation_symmetry_constraints(self): + """ + Add symmetry breaking constraints to avoid isomorphic models. + + Strategy: Enforce a lexicographic ordering on designated values. + If element i is not designated, then no element j < i can be designated. + This ensures designated elements are "packed to the right". + """ + for i in range(1, len(self.smt_carrier_set)): + elem_i = self.smt_carrier_set[i] + elem_j = self.smt_carrier_set[i - 1] + + # If i is not designated, then j (which comes before i) cannot be designated + self.solver.add( + Implies( + self.is_designated(elem_i) == False, + self.is_designated(elem_j) == False + ) + ) + + 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 = [] + + # Create mapping from ModelValue to SMT element + model_value_to_smt = { + ModelValue(str(smt_elem)): smt_elem + for smt_elem in self.smt_carrier_set + } + + # Exclude operation function mappings + for model_func in model.logical_operations: + operation = Operation(model_func.operation_name, model_func.arity) + smt_func = self.operation_function_map[operation] + + for inputs, output in model_func.mapping.items(): + 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 + constraints.append(smt_func(*smt_inputs) != smt_output) + + # Exclude designated value set + for smt_elem in self.smt_carrier_set: + model_val = ModelValue(str(smt_elem)) + is_designated_in_model = model_val in model.designated_values + + # Designation should differ + if is_designated_in_model: + constraints.append(self.is_designated(smt_elem) == False) + else: + constraints.append(self.is_designated(smt_elem) == True) + + return Or(constraints) + + def find_model(self) -> Optional[Model]: + """ + Find a single model satisfying the logic constraints. + + Returns: + A Model if one exists, None otherwise + """ + if self.solver.check() == sat: + return self.extract_model(self.solver.model()) return None + + def reset(self): + """Reset the solver state.""" + self.solver.reset() + + def __del__(self): + """Cleanup resources.""" + try: + self.solver.reset() + del self.ctx + except: + pass + + +def find_model(logic: Logic, size: int) -> Optional[Model]: + """Find a single model for the given logic and size.""" + encoder = SMTLogicEncoder(logic, size) + return encoder.find_model() + +def find_all_models(logic: Logic, size: int) -> Generator[Model, None, None]: + """ + Find all models for the given logic and size. + + Args: + logic: The logic system to encode + size: The size of the carrier set + + Yields: + Model instances that satisfy the logic + """ + encoder = SMTLogicEncoder(logic, size) + + while True: + # Try to find a model + model = encoder.find_model() + if model is None: + break + + yield model + + # 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 From 84f1c1fd36236acd77b62bc04c882b104d180dd8 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Fri, 12 Dec 2025 18:21:29 -0500 Subject: [PATCH 03/13] Added check for falsification rules in satisfiable function --- model.py | 36 +++++++++++++++++++++++++++++++++--- 1 file changed, 33 insertions(+), 3 deletions(-) diff --git a/model.py b/model.py index 429a26e..9c93c1e 100644 --- a/model.py +++ b/model.py @@ -266,9 +266,9 @@ def satisfiable(logic: Logic, model: Model, interpretation: Dict[Operation, Mode pvars = tuple(get_propostional_variables(tuple(logic.rules))) mappings = all_model_valuations_cached(pvars, tuple(model.carrier_set)) - for mapping in mappings: - # Make sure that the model satisfies each of the rules - for rule in logic.rules: + for rule in logic.rules: + # The rule most hold for all valuations + for mapping in mappings: # The check only applies if the premises are designated premise_met = True premise_ts: Set[ModelValue] = set() @@ -291,6 +291,36 @@ def satisfiable(logic: Logic, model: Model, interpretation: Dict[Operation, Mode if consequent_t not in model.designated_values: return False + for rule in logic.falsifies: + # We must find one mapping where this does not hold + counterexample_found = False + for mapping in mappings: + # The check only applies if the premises are designated + premise_met = True + premise_ts: Set[ModelValue] = set() + + for premise in rule.premises: + premise_t = evaluate_term(premise, mapping, interpretation) + # As soon as one premise is not designated, + # move to the next rule. + if premise_t not in model.designated_values: + premise_met = False + break + # If designated, keep track of the evaluated term + premise_ts.add(premise_t) + + if not premise_met: + continue + + # With the premises designated, make sure the consequent is not designated + consequent_t = evaluate_term(rule.conclusion, mapping, interpretation) + if consequent_t not in model.designated_values: + counterexample_found = True + break + + if not counterexample_found: + return False + return True From 25bd83f0324009520c25547e0706c66572e9a0ef Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Mon, 12 Jan 2026 16:55:37 -0500 Subject: [PATCH 04/13] 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) From 95e482a265da435eaff1b02dade11a5b4db57800 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Mon, 12 Jan 2026 17:07:44 -0500 Subject: [PATCH 05/13] Cleanup --- smt.py | 37 ++++++++++++++++--------------------- 1 file changed, 16 insertions(+), 21 deletions(-) diff --git a/smt.py b/smt.py index f94d49e..73e2d67 100644 --- a/smt.py +++ b/smt.py @@ -108,12 +108,6 @@ def logic_falsification_rule_to_smt_constraints( class SMTLogicEncoder: """ Encapsulates the SMT encoding of a logic system with a fixed carrier set size. - - This class handles: - - Creating the SMT sorts and functions - - Encoding logic rules as SMT constraints - - Managing the solver state - - Converting between Model objects and SMT representations """ def __init__(self, logic: Logic, size: int): @@ -140,18 +134,21 @@ class SMTLogicEncoder: # Create operation functions self.operation_function_map: Dict[Operation, z3.FuncDeclRef] = {} for operation in logic.operations: - self.operation_function_map[operation] = Function( - operation.symbol, - *(self.carrier_sort for _ in range(operation.arity + 1)) - ) + self.operation_function_map[operation] = self.create_function(operation.symbol, operation.arity) # Create designation function - self.is_designated = Function("D", self.carrier_sort, BoolSort(ctx=self.ctx)) + self.is_designated = self.create_predicate("D", 1) # Add logic rules as constraints self._add_logic_constraints() self._add_designation_symmetry_constraints() + 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_logic_constraints(self): """Add all logic rules and falsification rules as SMT constraints.""" # Add regular rules @@ -177,12 +174,6 @@ class SMTLogicEncoder: def extract_model(self, smt_model) -> Model: """ Extract a Model object from an SMT model. - - Args: - smt_model: The Z3 model to extract from - - Returns: - A Model object representing the logic model """ carrier_set = {ModelValue(f"{i}") for i in range(self.size)} @@ -281,10 +272,6 @@ class SMTLogicEncoder: return self.extract_model(self.solver.model()) return None - def reset(self): - """Reset the solver state.""" - self.solver.reset() - def __del__(self): """Cleanup resources.""" try: @@ -377,3 +364,11 @@ class SMTModelEncoder: 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) + + def __del__(self): + """Cleanup resources.""" + try: + self.solver.reset() + del self.ctx + except: + pass \ No newline at end of file From 4150ac2a7a75974cf30492732127510e5a95b8a4 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Thu, 15 Jan 2026 15:03:18 -0500 Subject: [PATCH 06/13] 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) From f8eca388d4fe30359c73d2aa94342e7b7a7cdce9 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Tue, 27 Jan 2026 11:23:47 -0500 Subject: [PATCH 07/13] Some comment changes --- smt.py | 5 ++--- vsp.py | 2 +- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/smt.py b/smt.py index 0be7af6..3946975 100644 --- a/smt.py +++ b/smt.py @@ -230,7 +230,7 @@ class SMTLogicEncoder: for smt_elem in self.smt_carrier_set } - # Exclude operation function mappings + # Iterate over all logical operations for model_func in model.logical_operations: operation = Operation(model_func.operation_name, model_func.arity) smt_func = self.operation_function_map[operation] @@ -239,10 +239,9 @@ class SMTLogicEncoder: smt_inputs = tuple(model_value_to_smt[inp] for inp in inputs) smt_output = model_value_to_smt[output] - # For future models the input->output mapping may differ + # It may be the case that the output of f(input) differs constraints.append(smt_func(*smt_inputs) != smt_output) - # Exclude designated value set for smt_elem in self.smt_carrier_set: model_val = ModelValue(str(smt_elem)) is_designated_in_model = model_val in model.designated_values diff --git a/vsp.py b/vsp.py index 5ea2ae9..0de5b10 100644 --- a/vsp.py +++ b/vsp.py @@ -168,7 +168,7 @@ def has_vsp_smt(model: Model, impfn: ModelFunction) -> VSP_Result: ) ) - # x -> y is non-designated + # x -> y is non-designated for any x in K1 and y in K2 smt_imp = encoder.model_function_map[impfn] for (x, y) in product(encoder.smt_carrier_set, encoder.smt_carrier_set): encoder.solver.add( From 6d877938034c102ebab7aed03ecd261c357341ae Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Tue, 27 Jan 2026 12:48:33 -0500 Subject: [PATCH 08/13] Updated driver file R.py to showcase SMT techinques Fixed minor bugs concerning lack of falsification rules and interfaces between VSP and SMT --- R.py | 81 +++++++++++++++++++++++++++++++++++------------ generate_model.py | 11 ++++--- logic.py | 2 +- smt.py | 75 +++++++++++++++++++++++++------------------ vsp.py | 16 +++++----- 5 files changed, 120 insertions(+), 65 deletions(-) diff --git a/R.py b/R.py index 4ce4b04..1b0fa39 100644 --- a/R.py +++ b/R.py @@ -12,7 +12,8 @@ from logic import ( ) from model import Model, ModelFunction, ModelValue, satisfiable from generate_model import generate_model -# from vsp import has_vsp +from vsp import has_vsp +from smt import smt_is_loaded # =================================================== @@ -56,12 +57,17 @@ disjunction_rules = { Rule({Conjunction(x, Disjunction(y, z)),}, Disjunction(Conjunction(x, y), Conjunction(x, z))) } +falsification_rules = { + # At least one value is non-designated + Rule(set(), x) +} + logic_rules = implication_rules | negation_rules | conjunction_rules | disjunction_rules operations = {Negation, Conjunction, Disjunction, Implication} -R_logic = Logic(operations, logic_rules, "R") +R_logic = Logic(operations, logic_rules, falsification_rules, "R") # =============================== @@ -69,36 +75,36 @@ R_logic = Logic(operations, logic_rules, "R") Example 2-Element Model of R """ -a0 = ModelValue("a0") -a1 = ModelValue("a1") +a0 = ModelValue("0") +a1 = ModelValue("1") carrier_set = {a0, a1} mnegation = ModelFunction(1, { a0: a1, a1: a0 -}) +}, "¬") mimplication = ModelFunction(2, { (a0, a0): a1, (a0, a1): a1, (a1, a0): a0, (a1, a1): a1 -}) +}, "→") mconjunction = ModelFunction(2, { (a0, a0): a0, (a0, a1): a0, (a1, a0): a0, (a1, a1): a1 -}) +}, "∧") mdisjunction = ModelFunction(2, { (a0, a0): a0, (a0, a1): a1, (a1, a0): a1, (a1, a1): a1 -}) +}, "∨") designated_values = {a1} @@ -117,11 +123,18 @@ interpretation = { print(R_model_2) +print(f"Does {R_model_2.name} satisfy the logic R?", satisfiable(R_logic, R_model_2, interpretation)) + +if smt_is_loaded(): + print(has_vsp(R_model_2, mimplication, True, True)) +else: + print("Z3 not setup, skipping VSP check...") + # ================================= """ -Generate models of R of a specified size +Generate models of R of a specified size using the slow approach """ print("*" * 30) @@ -130,14 +143,20 @@ model_size = 2 print("Generating models of Logic", R_logic.name, "of size", model_size) solutions = generate_model(R_logic, model_size, print_model=False) -print(f"Found {len(solutions)} satisfiable models") +if smt_is_loaded(): + num_satisfies_vsp = 0 + for model, interpretation in solutions: + negation_defined = Negation in interpretation + conj_disj_defined = Conjunction in interpretation and Disjunction in interpretation + if has_vsp(model, interpretation[Implication], negation_defined, conj_disj_defined).has_vsp: + num_satisfies_vsp += 1 + + print(f"Found {len(solutions)} satisfiable models of size {model_size}, {num_satisfies_vsp} of which satisfy VSP") -# for model, interpretation in solutions: -# print(has_vsp(model, interpretation)) print("*" * 30) -###### +# ================================= """ Showing the smallest model for R that has the @@ -146,12 +165,12 @@ variable sharing property. This model has 6 elements. """ -a0 = ModelValue("a0") -a1 = ModelValue("a1") -a2 = ModelValue("a2") -a3 = ModelValue("a3") -a4 = ModelValue("a4") -a5 = ModelValue("a5") +a0 = ModelValue("0") +a1 = ModelValue("1") +a2 = ModelValue("2") +a3 = ModelValue("3") +a4 = ModelValue("4") +a5 = ModelValue("5") carrier_set = { a0, a1, a2, a3, a4, a5 } designated_values = {a1, a2, a3, a4, a5 } @@ -312,4 +331,26 @@ interpretation = { print(R_model_6) print(f"Model {R_model_6.name} satisfies logic {R_logic.name}?", satisfiable(R_logic, R_model_6, interpretation)) -# print(has_vsp(R_model_6, interpretation)) +if smt_is_loaded(): + print(has_vsp(R_model_6, mimplication, True, True)) +else: + print("Z3 not loaded, skipping VSP check...") + +""" +Generate models of R of a specified size using the SMT approach +""" + +from vsp import logic_has_vsp + +size = 7 +print(f"Searching for a model of size {size} which witness VSP...") +if smt_is_loaded(): + solution = logic_has_vsp(R_logic, size) + if solution is None: + print(f"No models found of size {size} which witness VSP") + else: + model, vsp_result = solution + print(vsp_result) + print(model) +else: + print("Z3 not setup, skipping...") \ No newline at end of file diff --git a/generate_model.py b/generate_model.py index 5a46efc..ceb9681 100644 --- a/generate_model.py +++ b/generate_model.py @@ -67,7 +67,7 @@ def only_rules_with(rules: Set[Rule], operation: Operation) -> List[Rule]: def possible_interpretations( logic: Logic, carrier_set: Set[ModelValue], - designated_values: Set[ModelValue]): + designated_values: Set[ModelValue], debug: bool): """ Consider every possible interpretation of operations within the specified logic given the carrier set of @@ -100,7 +100,7 @@ def possible_interpretations( passed_functions = candidate_functions if len(passed_functions) == 0: raise Exception("No interpretation satisfies the axioms for the operation " + str(operation)) - else: + elif debug: print( f"Operation {operation.symbol} has {len(passed_functions)} candidate functions" ) @@ -120,7 +120,7 @@ def possible_interpretations( def generate_model( logic: Logic, number_elements: int, num_solutions: int = -1, - print_model=False) -> List[Tuple[Model, Interpretation]]: + print_model=False, debug=False) -> List[Tuple[Model, Interpretation]]: """ Generate the specified number of models that satisfy a logic of a certain size. @@ -136,9 +136,10 @@ def generate_model( for designated_values in possible_designated_values: designated_values = set(designated_values) - print("Considering models for designated values", set_to_str(designated_values)) + if debug: + print("Considering models for designated values", set_to_str(designated_values)) - possible_interps = possible_interpretations(logic, carrier_set, designated_values) + possible_interps = possible_interpretations(logic, carrier_set, designated_values, debug) for interpretation in possible_interps: is_valid = True model = Model(carrier_set, set(interpretation.values()), designated_values) diff --git a/logic.py b/logic.py index 44c5c6b..1cb383e 100644 --- a/logic.py +++ b/logic.py @@ -85,7 +85,7 @@ class Logic: name: Optional[str] = None): self.operations = operations self.rules = rules - self.falsifies = falsifies + self.falsifies = falsifies if falsifies is not None else set() self.name = str(abs(hash(( frozenset(operations), frozenset(rules) diff --git a/smt.py b/smt.py index 3946975..4394713 100644 --- a/smt.py +++ b/smt.py @@ -1,18 +1,26 @@ from itertools import product -from typing import Dict, Generator, Optional, Tuple +from typing import Dict, Generator, Optional, Set, Tuple, TYPE_CHECKING from logic import Logic, Operation, Rule, PropositionalVariable, Term, OpTerm, get_prop_vars_from_rule from model import Model, ModelValue, ModelFunction -from z3 import ( - And, BoolSort, Context, EnumSort, Function, Implies, Or, sat, Solver, z3 -) +SMT_LOADED = True +try: + from z3 import ( + And, BoolSort, Context, EnumSort, Function, Implies, Or, sat, Solver, z3 + ) +except ImportError: + SMT_LOADED = False + +def smt_is_loaded() -> bool: + global SMT_LOADED + return SMT_LOADED def term_to_smt( t: Term, - op_mapping: Dict[Operation, z3.FuncDeclRef], - var_mapping: Dict[PropositionalVariable, z3.DatatypeRef] -) -> z3.DatatypeRef: + op_mapping: Dict[Operation, "z3.FuncDeclRef"], + var_mapping: Dict[PropositionalVariable, "z3.DatatypeRef"] +) -> "z3.DatatypeRef": """Convert a logic term to its SMT representation.""" if isinstance(t, PropositionalVariable): return var_mapping[t] @@ -26,10 +34,10 @@ def term_to_smt( def logic_rule_to_smt_constraints( rule: Rule, - IsDesignated: z3.FuncDeclRef, + IsDesignated: "z3.FuncDeclRef", smt_carrier_set, - op_mapping: Dict[Operation, z3.FuncDeclRef] -) -> Generator[z3.BoolRef, None, None]: + op_mapping: Dict[Operation, "z3.FuncDeclRef"] +) -> Generator["z3.BoolRef", None, None]: """ Encode a logic rule as SMT constraints. @@ -63,10 +71,10 @@ def logic_rule_to_smt_constraints( def logic_falsification_rule_to_smt_constraints( rule: Rule, - IsDesignated: z3.FuncDeclRef, + IsDesignated: "z3.FuncDeclRef", smt_carrier_set, - op_mapping: Dict[Operation, z3.FuncDeclRef] -) -> z3.BoolRef: + op_mapping: Dict[Operation, "z3.FuncDeclRef"] +) -> "z3.BoolRef": """ Encode a falsification rule as an SMT constraint. @@ -132,7 +140,7 @@ class SMTLogicEncoder: self.carrier_sort, self.smt_carrier_set = EnumSort("C", element_names, ctx=self.ctx) # Create operation functions - self.operation_function_map: Dict[Operation, z3.FuncDeclRef] = {} + self.operation_function_map: Dict[Operation, "z3.FuncDeclRef"] = {} for operation in logic.operations: self.operation_function_map[operation] = self.create_function(operation.symbol, operation.arity) @@ -143,10 +151,10 @@ class SMTLogicEncoder: self._add_logic_constraints() self._add_designation_symmetry_constraints() - def create_predicate(self, name: str, arity: int) -> z3.FuncDeclRef: + 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: + def create_function(self, name: str, arity: int) -> "z3.FuncDeclRef": return Function(name, *(self.carrier_sort for _ in range(arity + 1))) def _add_logic_constraints(self): @@ -171,9 +179,9 @@ class SMTLogicEncoder: ) self.solver.add(constraint) - def extract_model(self, smt_model) -> Model: + def extract_model(self, smt_model) -> Tuple[Model, Dict[Operation, ModelFunction]]: """ - Extract a Model object from an SMT model. + Extract a Model object and interpretation from an SMT model. """ carrier_set = {ModelValue(f"{i}") for i in range(self.size)} @@ -185,7 +193,8 @@ class SMTLogicEncoder: designated_values = {ModelValue(str(x)) for x in smt_designated} # Extract operation functions - model_functions = set() + model_functions: Set[ModelFunction] = set() + interpretation: Dict[Operation, ModelFunction] = dict() for (operation, smt_function) in self.operation_function_map.items(): mapping: Dict[Tuple[ModelValue], ModelValue] = {} for smt_inputs in product(self.smt_carrier_set, repeat=operation.arity): @@ -193,9 +202,12 @@ class SMTLogicEncoder: smt_output = smt_model.evaluate(smt_function(*smt_inputs)) model_output = ModelValue(str(smt_output)) mapping[model_inputs] = model_output - model_functions.add(ModelFunction(operation.arity, mapping, operation.symbol)) + model_function = ModelFunction(operation.arity, mapping, operation.symbol) + model_functions.add(model_function) + interpretation[operation] = model_function - return Model(carrier_set, model_functions, designated_values) + + return Model(carrier_set, model_functions, designated_values), interpretation def _add_designation_symmetry_constraints(self): @@ -218,7 +230,7 @@ class SMTLogicEncoder: ) ) - def create_exclusion_constraint(self, model: Model) -> z3.BoolRef: + def create_exclusion_constraint(self, model: Model) -> "z3.BoolRef": """ Create a constraint that excludes the given model from future solutions. """ @@ -254,7 +266,7 @@ class SMTLogicEncoder: return Or(constraints) - def find_model(self) -> Optional[Model]: + def find_model(self) -> Optional[Tuple[Model, Dict[Operation, ModelFunction]]]: """ Find a single model satisfying the logic constraints. @@ -274,12 +286,12 @@ class SMTLogicEncoder: pass -def find_model(logic: Logic, size: int) -> Optional[Model]: +def find_model(logic: Logic, size: int) -> Optional[Tuple[Model, Dict[Operation, ModelFunction]]]: """Find a single model for the given logic and size.""" encoder = SMTLogicEncoder(logic, size) return encoder.find_model() -def find_all_models(logic: Logic, size: int) -> Generator[Model, None, None]: +def find_all_models(logic: Logic, size: int) -> Generator[Tuple[Model, Dict[Operation, ModelFunction]], None, None]: """ Find all models for the given logic and size. @@ -294,13 +306,14 @@ def find_all_models(logic: Logic, size: int) -> Generator[Model, None, None]: while True: # Try to find a model - model = encoder.find_model() - if model is None: + solution = encoder.find_model() + if solution is None: break - yield model + yield solution # Add constraint to exclude this model from future solutions + model, _ = solution exclusion_constraint = encoder.create_exclusion_constraint(model) encoder.solver.add(exclusion_constraint) @@ -346,13 +359,13 @@ class SMTModelEncoder: 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: + 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: + 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): + 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] diff --git a/vsp.py b/vsp.py index 0de5b10..fe97ccb 100644 --- a/vsp.py +++ b/vsp.py @@ -10,12 +10,12 @@ from model import ( Model, model_closure, ModelFunction, ModelValue ) -SMT_LOADED = True +from smt import SMTModelEncoder, SMTLogicEncoder, smt_is_loaded + try: from z3 import And, Or, Implies, sat - from smt import SMTModelEncoder, SMTLogicEncoder except ImportError: - SMT_LOADED = False + pass class VSP_Result: def __init__( @@ -139,7 +139,7 @@ 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: + if not smt_is_loaded(): raise Exception("Z3 is not property installed, cannot check via SMT") encoder = SMTModelEncoder(model) @@ -198,7 +198,7 @@ def has_vsp(model: Model, impfunction: ModelFunction, if model.is_magical: return has_vsp_magical(model, impfunction, negation_defined, conjunction_disjunction_defined) - return has_vsp_smt(model) + return has_vsp_smt(model, impfunction) def logic_has_vsp(logic: Logic, size: int) -> Optional[Tuple[Model, VSP_Result]]: @@ -254,15 +254,15 @@ def logic_has_vsp(logic: Logic, size: int) -> Optional[Tuple[Model, VSP_Result]] ) ) - model = encoder.find_model() + solution = encoder.find_model() # We failed to find a VSP witness - if model is None: + if solution is None: return None # Otherwise, a matrix model and correspoding # subalgebras exist. - + model, _ = solution 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} From bf86bfd83ead5036ae5d2576e399a5a29ee5baf4 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Tue, 27 Jan 2026 14:11:41 -0500 Subject: [PATCH 09/13] Simplified satisfiable --- model.py | 87 +++++++++++++++++++++++--------------------------------- 1 file changed, 35 insertions(+), 52 deletions(-) diff --git a/model.py b/model.py index 41483f9..cd02e6e 100644 --- a/model.py +++ b/model.py @@ -5,7 +5,7 @@ a given logic. from common import set_to_str, immutable from logic import ( get_propostional_variables, Logic, - Operation, PropositionalVariable, Term + Operation, PropositionalVariable, Rule, Term ) from collections import defaultdict from functools import cached_property, lru_cache, reduce @@ -277,67 +277,50 @@ def all_model_valuations_cached( return list(all_model_valuations(pvars, mvalues)) +def rule_satisfied( + rule: Rule, valuations: List[Dict[PropositionalVariable, ModelValue]], + interpretation: Dict[Operation, ModelFunction], designated_values: Set[ModelValue]) -> bool: + """ + Checks whether a rule holds under all valuations listed in mapping. + + If there is a mapping where the premise holds but the consequent does + not then this returns False. + """ + for valuation in valuations: + premise_met = True + for premise in rule.premises: + premise_t = evaluate_term(premise, valuation, interpretation) + if premise_t not in designated_values: + premise_met = False + break + + # If any of the premises doesn't hold, then this won't serve as a counterexample + if not premise_met: + continue + + consequent_t = evaluate_term(rule.conclusion, valuation, interpretation) + if consequent_t not in designated_values: + # Counterexample found, return False + return False + + # No mapping found which contradicts our rule + return True + + def satisfiable(logic: Logic, model: Model, interpretation: Dict[Operation, ModelFunction]) -> bool: """ Determine whether a model satisfies a logic given an interpretation. """ pvars = tuple(get_propostional_variables(tuple(logic.rules))) - mappings = all_model_valuations_cached(pvars, tuple(model.carrier_set)) + valuations = all_model_valuations_cached(pvars, tuple(model.carrier_set)) for rule in logic.rules: - # The rule most hold for all valuations - for mapping in mappings: - # The check only applies if the premises are designated - premise_met = True - premise_ts: Set[ModelValue] = set() - - for premise in rule.premises: - premise_t = evaluate_term(premise, mapping, interpretation) - # As soon as one premise is not designated, - # move to the next rule. - if premise_t not in model.designated_values: - premise_met = False - break - # If designated, keep track of the evaluated term - premise_ts.add(premise_t) - - if not premise_met: - continue - - # With the premises designated, make sure the consequent is designated - consequent_t = evaluate_term(rule.conclusion, mapping, interpretation) - if consequent_t not in model.designated_values: - return False + if not rule_satisfied(rule, valuations, interpretation, model.designated_values): + return False for rule in logic.falsifies: - # We must find one mapping where this does not hold - counterexample_found = False - for mapping in mappings: - # The check only applies if the premises are designated - premise_met = True - premise_ts: Set[ModelValue] = set() - - for premise in rule.premises: - premise_t = evaluate_term(premise, mapping, interpretation) - # As soon as one premise is not designated, - # move to the next rule. - if premise_t not in model.designated_values: - premise_met = False - break - # If designated, keep track of the evaluated term - premise_ts.add(premise_t) - - if not premise_met: - continue - - # With the premises designated, make sure the consequent is not designated - consequent_t = evaluate_term(rule.conclusion, mapping, interpretation) - if consequent_t not in model.designated_values: - counterexample_found = True - break - - if not counterexample_found: + if rule_satisfied(rule, valuations, interpretation, model.designated_values): return False return True From 51f8adcd441d67a57200ff503d2dab631876d969 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Tue, 27 Jan 2026 14:13:19 -0500 Subject: [PATCH 10/13] Small comment change --- model.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/model.py b/model.py index cd02e6e..79cff8f 100644 --- a/model.py +++ b/model.py @@ -281,7 +281,7 @@ def rule_satisfied( rule: Rule, valuations: List[Dict[PropositionalVariable, ModelValue]], interpretation: Dict[Operation, ModelFunction], designated_values: Set[ModelValue]) -> bool: """ - Checks whether a rule holds under all valuations listed in mapping. + Checks whether a rule holds under all valuations. If there is a mapping where the premise holds but the consequent does not then this returns False. From 85ef364a5743dc8982410aa1d32ac7983fc5b0c7 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Tue, 27 Jan 2026 14:13:54 -0500 Subject: [PATCH 11/13] Small comment change --- model.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/model.py b/model.py index 79cff8f..855b320 100644 --- a/model.py +++ b/model.py @@ -303,7 +303,7 @@ def rule_satisfied( # Counterexample found, return False return False - # No mapping found which contradicts our rule + # No valuation found which contradicts our rule return True From 06cca7d32ecd3c69d36fbb3a50f2f4b7ebe4ddf3 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Tue, 27 Jan 2026 15:22:47 -0500 Subject: [PATCH 12/13] Refactored out valuation generation code in SMT --- model.py | 4 ++-- smt.py | 64 ++++++++++++++++++++++++++++++++++++-------------------- 2 files changed, 43 insertions(+), 25 deletions(-) diff --git a/model.py b/model.py index 855b320..05a1a1d 100644 --- a/model.py +++ b/model.py @@ -13,7 +13,7 @@ from itertools import ( chain, combinations_with_replacement, permutations, product ) -from typing import Dict, List, Optional, Set, Tuple +from typing import Any, Dict, Generator, List, Optional, Set, Tuple __all__ = ['ModelValue', 'ModelFunction', 'Model', 'Interpretation'] @@ -255,7 +255,7 @@ def evaluate_term( def all_model_valuations( pvars: Tuple[PropositionalVariable], - mvalues: Tuple[ModelValue]): + mvalues: Tuple[ModelValue]) -> Generator[Dict[PropositionalVariable, ModelValue], Any, None]: """ Given propositional variables and model values, produce every possible mapping between the two. diff --git a/smt.py b/smt.py index 4394713..9dbee99 100644 --- a/smt.py +++ b/smt.py @@ -1,5 +1,6 @@ +from functools import lru_cache from itertools import product -from typing import Dict, Generator, Optional, Set, Tuple, TYPE_CHECKING +from typing import Dict, Generator, Optional, Set, Tuple from logic import Logic, Operation, Rule, PropositionalVariable, Term, OpTerm, get_prop_vars_from_rule from model import Model, ModelValue, ModelFunction @@ -27,11 +28,32 @@ def term_to_smt( assert isinstance(t, OpTerm) + # Recursively convert all arguments to SMT arguments = [term_to_smt(arg, op_mapping, var_mapping) for arg in t.arguments] fn = op_mapping[t.operation] return fn(*arguments) +def all_smt_valuations(pvars: Tuple[PropositionalVariable], smtvalues): + """ + Generator which maps all the propositional variable to + smt variables representing the carrier set. + + Exhaust the generator to get all such mappings. + """ + all_possible_values = product(smtvalues, repeat=len(pvars)) + for valuation in all_possible_values: + mapping = dict() + assert len(pvars) == len(valuation) + for pvar, value in zip(pvars, valuation): + mapping[pvar] = value + yield mapping + + +@lru_cache +def all_smt_valuations_cached(pvars: Tuple[PropositionalVariable], smtvalues): + return list(all_smt_valuations(pvars, smtvalues)) + def logic_rule_to_smt_constraints( rule: Rule, IsDesignated: "z3.FuncDeclRef", @@ -43,32 +65,30 @@ def logic_rule_to_smt_constraints( For all valuations: if premises are designated, then conclusion is designated. """ - prop_vars = get_prop_vars_from_rule(rule) - - # Requires that the rule holds under all valuations - for smt_vars in product(smt_carrier_set, repeat=len(prop_vars)): - assert len(prop_vars) == len(smt_vars) - - var_mapping = { - prop_var: smt_var - for (prop_var, smt_var) in zip(prop_vars, smt_vars) - } + prop_vars = tuple(get_prop_vars_from_rule(rule)) + valuations = all_smt_valuations_cached(prop_vars, tuple(smt_carrier_set)) + for valuation in valuations: premises = [ - IsDesignated(term_to_smt(premise, op_mapping, var_mapping)) == True + IsDesignated(term_to_smt(premise, op_mapping, valuation)) == True for premise in rule.premises ] - conclusion = IsDesignated(term_to_smt(rule.conclusion, op_mapping, var_mapping)) == True + conclusion = IsDesignated(term_to_smt(rule.conclusion, op_mapping, valuation)) == True if len(premises) == 0: + # If there are no premises, then the conclusion must always be designated yield conclusion else: + # Otherwise, combine all the premises with and + # and have that if the premises are designated + # then the conclusion is designated premise = premises[0] for p in premises[1:]: premise = And(premise, p) yield Implies(premise, conclusion) + def logic_falsification_rule_to_smt_constraints( rule: Rule, IsDesignated: "z3.FuncDeclRef", @@ -81,24 +101,22 @@ def logic_falsification_rule_to_smt_constraints( There exists at least one valuation where premises are designated but conclusion is not designated. """ - prop_vars = get_prop_vars_from_rule(rule) + prop_vars = tuple(get_prop_vars_from_rule(rule)) + valuations = all_smt_valuations_cached(prop_vars, tuple(smt_carrier_set)) # Collect all possible counter-examples (valuations that falsify the rule) counter_examples = [] - for smt_vars in product(smt_carrier_set, repeat=len(prop_vars)): - assert len(prop_vars) == len(smt_vars) - - var_mapping = { - prop_var: smt_var - for (prop_var, smt_var) in zip(prop_vars, smt_vars) - } + for valuation in valuations: + # The rule is falsified when all of our premises + # are designated but our conclusion is not designated premises = [ - IsDesignated(term_to_smt(premise, op_mapping, var_mapping)) == True + IsDesignated(term_to_smt(premise, op_mapping, valuation)) == True for premise in rule.premises ] - conclusion = IsDesignated(term_to_smt(rule.conclusion, op_mapping, var_mapping)) == False + + conclusion = IsDesignated(term_to_smt(rule.conclusion, op_mapping, valuation)) == False if len(premises) == 0: counter_examples.append(conclusion) From 51bf1a44d9985ac5406938bc0e1b56ca21aed29b Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Tue, 27 Jan 2026 15:26:16 -0500 Subject: [PATCH 13/13] Small comment change --- vsp.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/vsp.py b/vsp.py index fe97ccb..c4fd398 100644 --- a/vsp.py +++ b/vsp.py @@ -244,7 +244,7 @@ def logic_has_vsp(logic: Logic, size: int) -> Optional[Tuple[Model, VSP_Result]] ) ) - # x -> y is non-designated + # x -> y is non-designated for any x in k1 and y in k2 Impfn = encoder.operation_function_map[Implication] for (x, y) in product(encoder.smt_carrier_set, encoder.smt_carrier_set): encoder.solver.add(