diff --git a/model.py b/model.py index 807f1ec..9c93c1e 100644 --- a/model.py +++ b/model.py @@ -187,24 +187,17 @@ class Model: logical_operations: Set[ModelFunction], designated_values: Set[ModelValue], ordering: Optional[OrderTable] = None, - name: Optional[str] = None, - is_magical: Optional[bool] = False + name: Optional[str] = None ): 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), - is_magical + frozenset(designated_values) ))))[:5] if name is None else name def __str__(self): diff --git a/parse_magic.py b/parse_magic.py index 29cec8b..78fc495 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, is_magical=True) + model = Model(set(self.carrier_list), logical_operations, self.designated_values, ordering=self.ordering, name=model_name) return (model, interpretation) diff --git a/smt.py b/smt.py index 73e2d67..f6f2c33 100644 --- a/smt.py +++ b/smt.py @@ -108,6 +108,12 @@ 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): @@ -134,21 +140,18 @@ class SMTLogicEncoder: # Create operation functions 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) + self.operation_function_map[operation] = Function( + operation.symbol, + *(self.carrier_sort for _ in range(operation.arity + 1)) + ) # Create designation function - self.is_designated = self.create_predicate("D", 1) + 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 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 @@ -174,6 +177,12 @@ 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)} @@ -272,6 +281,10 @@ 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: @@ -309,66 +322,4 @@ 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) - -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) - - def __del__(self): - """Cleanup resources.""" - try: - self.solver.reset() - del self.ctx - except: - pass \ No newline at end of file + encoder.solver.add(exclusion_constraint) \ No newline at end of file diff --git a/vsp.py b/vsp.py index 86bad4d..034005f 100644 --- a/vsp.py +++ b/vsp.py @@ -9,13 +9,6 @@ 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, @@ -34,10 +27,10 @@ Subalgebra 1: {set_to_str(self.subalgebra1)} Subalgebra 2: {set_to_str(self.subalgebra2)} """ -def has_vsp_magical(model: Model, impfunction: ModelFunction, +def has_vsp(model: Model, impfunction: ModelFunction, negation_defined: bool) -> VSP_Result: """ - Checks whether a MaGIC model has the variable + Checks whether a model has the variable sharing property. """ # NOTE: No models with only one designated @@ -128,69 +121,3 @@ def has_vsp_magical(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)