diff --git a/R.py b/R.py index 1b0fa39..4ce4b04 100644 --- a/R.py +++ b/R.py @@ -12,8 +12,7 @@ from logic import ( ) from model import Model, ModelFunction, ModelValue, satisfiable from generate_model import generate_model -from vsp import has_vsp -from smt import smt_is_loaded +# from vsp import has_vsp # =================================================== @@ -57,17 +56,12 @@ 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, falsification_rules, "R") +R_logic = Logic(operations, logic_rules, "R") # =============================== @@ -75,36 +69,36 @@ R_logic = Logic(operations, logic_rules, falsification_rules, "R") Example 2-Element Model of R """ -a0 = ModelValue("0") -a1 = ModelValue("1") +a0 = ModelValue("a0") +a1 = ModelValue("a1") 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} @@ -123,18 +117,11 @@ 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 using the slow approach +Generate models of R of a specified size """ print("*" * 30) @@ -143,20 +130,14 @@ 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) -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") +print(f"Found {len(solutions)} satisfiable models") +# for model, interpretation in solutions: +# print(has_vsp(model, interpretation)) print("*" * 30) -# ================================= +###### """ Showing the smallest model for R that has the @@ -165,12 +146,12 @@ variable sharing property. This model has 6 elements. """ -a0 = ModelValue("0") -a1 = ModelValue("1") -a2 = ModelValue("2") -a3 = ModelValue("3") -a4 = ModelValue("4") -a5 = ModelValue("5") +a0 = ModelValue("a0") +a1 = ModelValue("a1") +a2 = ModelValue("a2") +a3 = ModelValue("a3") +a4 = ModelValue("a4") +a5 = ModelValue("a5") carrier_set = { a0, a1, a2, a3, a4, a5 } designated_values = {a1, a2, a3, a4, a5 } @@ -331,26 +312,4 @@ interpretation = { print(R_model_6) print(f"Model {R_model_6.name} satisfies logic {R_logic.name}?", satisfiable(R_logic, 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 +# print(has_vsp(R_model_6, interpretation)) diff --git a/generate_model.py b/generate_model.py index ceb9681..1306adc 100644 --- a/generate_model.py +++ b/generate_model.py @@ -1,9 +1,6 @@ """ 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 @@ -67,7 +64,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], debug: bool): + designated_values: Set[ModelValue]): """ Consider every possible interpretation of operations within the specified logic given the carrier set of @@ -100,7 +97,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)) - elif debug: + else: print( f"Operation {operation.symbol} has {len(passed_functions)} candidate functions" ) @@ -120,7 +117,7 @@ def possible_interpretations( def generate_model( logic: Logic, number_elements: int, num_solutions: int = -1, - print_model=False, debug=False) -> List[Tuple[Model, Interpretation]]: + print_model=False) -> List[Tuple[Model, Interpretation]]: """ Generate the specified number of models that satisfy a logic of a certain size. @@ -136,10 +133,9 @@ def generate_model( for designated_values in possible_designated_values: designated_values = set(designated_values) - if debug: - print("Considering models for designated values", set_to_str(designated_values)) + print("Considering models for designated values", set_to_str(designated_values)) - possible_interps = possible_interpretations(logic, carrier_set, designated_values, debug) + possible_interps = possible_interpretations(logic, carrier_set, designated_values) 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 1cb383e..7775590 100644 --- a/logic.py +++ b/logic.py @@ -81,11 +81,9 @@ 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 if falsifies is not None else set() self.name = str(abs(hash(( frozenset(operations), frozenset(rules) @@ -102,22 +100,17 @@ 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: - vars |= get_prop_vars_from_rule(rule) + # 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) return vars diff --git a/model.py b/model.py index 05a1a1d..6272d48 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, Rule, Term + Operation, PropositionalVariable, Term ) from collections import defaultdict from functools import cached_property, lru_cache, reduce @@ -13,7 +13,7 @@ from itertools import ( chain, combinations_with_replacement, permutations, product ) -from typing import Any, Dict, Generator, List, Optional, Set, Tuple +from typing import Dict, List, Optional, Set, Tuple __all__ = ['ModelValue', 'ModelFunction', 'Model', 'Interpretation'] @@ -199,24 +199,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): @@ -255,7 +248,7 @@ def evaluate_term( def all_model_valuations( pvars: Tuple[PropositionalVariable], - mvalues: Tuple[ModelValue]) -> Generator[Dict[PropositionalVariable, ModelValue], Any, None]: + mvalues: Tuple[ModelValue]): """ Given propositional variables and model values, produce every possible mapping between the two. @@ -277,51 +270,38 @@ 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. - - 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 valuation 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))) - valuations = all_model_valuations_cached(pvars, tuple(model.carrier_set)) + mappings = all_model_valuations_cached(pvars, tuple(model.carrier_set)) - for rule in logic.rules: - if not rule_satisfied(rule, valuations, interpretation, model.designated_values): - return False + for mapping in mappings: + # Make sure that the model satisfies each of the rules + for rule in logic.rules: + # The check only applies if the premises are designated + premise_met = True + premise_ts: Set[ModelValue] = set() - for rule in logic.falsifies: - if rule_satisfied(rule, valuations, interpretation, model.designated_values): - return False + 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 return True 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 deleted file mode 100644 index 9dbee99..0000000 --- a/smt.py +++ /dev/null @@ -1,398 +0,0 @@ -from functools import lru_cache -from itertools import product -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 - -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": - """Convert a logic term to its SMT representation.""" - if isinstance(t, PropositionalVariable): - return var_mapping[t] - - 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", - smt_carrier_set, - op_mapping: Dict[Operation, "z3.FuncDeclRef"] -) -> Generator["z3.BoolRef", None, None]: - """ - Encode a logic rule as SMT constraints. - - For all valuations: if premises are designated, then conclusion is designated. - """ - 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, valuation)) == True - for premise in rule.premises - ] - 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", - smt_carrier_set, - op_mapping: Dict[Operation, "z3.FuncDeclRef"] -) -> "z3.BoolRef": - """ - Encode a falsification rule as an SMT constraint. - - There exists at least one valuation where premises are designated - but conclusion is not designated. - """ - 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 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, valuation)) == True - for premise in rule.premises - ] - - conclusion = IsDesignated(term_to_smt(rule.conclusion, op_mapping, valuation)) == False - - if len(premises) == 0: - counter_examples.append(conclusion) - else: - premise = premises[0] - for p in premises[1:]: - premise = And(premise, p) - - counter_examples.append(And(premise, conclusion)) - - # At least one counter-example must exist (disjunction of all possibilities) - return Or(counter_examples) - - -class SMTLogicEncoder: - """ - Encapsulates the SMT encoding of a logic system with a fixed carrier set size. - """ - - 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] = self.create_function(operation.symbol, operation.arity) - - # Create designation function - 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 - 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) -> Tuple[Model, Dict[Operation, ModelFunction]]: - """ - Extract a Model object and interpretation from an SMT 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[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): - 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_function = ModelFunction(operation.arity, mapping, operation.symbol) - model_functions.add(model_function) - interpretation[operation] = model_function - - - return Model(carrier_set, model_functions, designated_values), interpretation - - - 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. - """ - 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 - } - - # 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] - - 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] - - # It may be the case that the output of f(input) differs - constraints.append(smt_func(*smt_inputs) != smt_output) - - 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 may 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[Tuple[Model, Dict[Operation, ModelFunction]]]: - """ - 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 __del__(self): - """Cleanup resources.""" - try: - self.solver.reset() - del self.ctx - except: - pass - - -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[Tuple[Model, Dict[Operation, ModelFunction]], 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 - solution = encoder.find_model() - if solution is None: - break - - 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) - -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 diff --git a/vsp.py b/vsp.py index c4fd398..2d3575c 100644 --- a/vsp.py +++ b/vsp.py @@ -5,18 +5,10 @@ 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 ) -from smt import SMTModelEncoder, SMTLogicEncoder, smt_is_loaded - -try: - from z3 import And, Or, Implies, sat -except ImportError: - pass - class VSP_Result: def __init__( self, has_vsp: bool, model_name: Optional[str] = None, @@ -35,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, conjunction_disjunction_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 @@ -133,141 +125,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_is_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 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( - 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, conjunction_disjunction_defined: bool) -> VSP_Result: - if model.is_magical: - return has_vsp_magical(model, impfunction, negation_defined, conjunction_disjunction_defined) - - return has_vsp_smt(model, impfunction) - - -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 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( - Implies( - And(IsInK1(x), IsInK2(y)), - encoder.is_designated(Impfn(x, y)) == False - ) - ) - - solution = encoder.find_model() - - # We failed to find a VSP witness - 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} - - 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)