From 6bb863da9751cdddf346b1f9db34bac284a948b9 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Tue, 28 May 2024 16:05:06 -0400 Subject: [PATCH] Code cleanup --- generate_model.py | 83 +++++++++++++++++++++++++++++------------------ logic.py | 2 +- model.py | 5 ++- 3 files changed, 57 insertions(+), 33 deletions(-) diff --git a/generate_model.py b/generate_model.py index 2048b6e..79121ad 100644 --- a/generate_model.py +++ b/generate_model.py @@ -1,9 +1,13 @@ """ -File which generates all the models +Generate all the models for a given logic +with a specified number of elements. """ from common import set_to_str from logic import Logic, Operation, Rule, get_operations_from_term -from model import ModelValue, Model, satisfiable, ModelFunction, ModelOrderConstraint +from model import ( + Interpretation, ModelValue, Model, + satisfiable, ModelFunction +) from itertools import combinations, chain, product from typing import Set, List, Dict, Tuple @@ -13,6 +17,11 @@ def possible_designations(iterable): return chain.from_iterable(combinations(s, r) for r in range(1, len(s))) def possible_functions(operation, carrier_set): + """ + Create every possible input, output pair + for a given model function based on an + operation and a carrier set. + """ arity = operation.arity inputs = list(product(carrier_set, repeat=arity)) @@ -26,12 +35,19 @@ def possible_functions(operation, carrier_set): yield ModelFunction(arity, new_function, operation.symbol) -def only_rules_with(rules: Set[Rule], operation: Operation) -> Set[Rule]: - result_rules = [] +def only_rules_with(rules: Set[Rule], operation: Operation) -> List[Rule]: + """ + Filter the list of rules in a logic to those + that only contain the logical operation specified. + """ + result_rules: List[Rule] = [] for rule in rules: is_valid = True + # Go through every term in the premises and conclusion for t in (rule.premises | {rule.conclusion,}): t_operations = get_operations_from_term(t) + # Make sure there's only one operation + # and that it matches the operation specified if len(t_operations) > 1: is_valid = False break @@ -48,23 +64,32 @@ def only_rules_with(rules: Set[Rule], operation: Operation) -> Set[Rule]: def possible_interpretations( logic: Logic, carrier_set: Set[ModelValue], - designated_values: Set[ModelValue], ordering: Set[ModelOrderConstraint]): - operations = [] - model_functions = [] + designated_values: Set[ModelValue]): + """ + Consider every possible interpretation of operations + within the specified logic given the carrier set of + model values, and the set of designated values. + """ + operations: List[Operation] = [] + model_functions: List[List[ModelFunction]] = [] for operation in logic.operations: operations.append(operation) candidate_functions = list(possible_functions(operation, carrier_set)) - passed_functions = [] + passed_functions: List[ModelFunction] = [] """ - Only consider functions that at least pass - in the rules with the operation by itself. + Discard candidate functions that don't pass + the rules that only contain the given + logical operation. """ restricted_rules = only_rules_with(logic.rules, operation) if len(restricted_rules) > 0: small_logic = Logic({operation,}, restricted_rules) + # Add candidate functions whose small model + # and logic are satisfied given the restricted + # rule set. for f in candidate_functions: - small_model = Model(carrier_set, {f,}, designated_values, ordering) + small_model = Model(carrier_set, {f,}, designated_values) interp = {operation: f} if satisfiable(small_logic, small_model, interp): passed_functions.append(f) @@ -78,45 +103,42 @@ def possible_interpretations( ) model_functions.append(passed_functions) + # The model_functions variables contains + # the candidate functions for each operation. + functions_choice = product(*model_functions) + # Assign a function to each operation for functions in functions_choice: assert len(operations) == len(functions) - interpretation = dict() + interpretation: Interpretation = dict() for operation, function in zip(operations, functions): interpretation[operation] = function yield interpretation -def generate_model(logic: Logic, number_elements: int, num_solutions: int = -1, print_model=False) -> List[Tuple[Model, Dict[Operation, ModelFunction]]]: +def generate_model( + logic: Logic, number_elements: int, num_solutions: int = -1, + print_model=False) -> List[Tuple[Model, Interpretation]]: + """ + Generate the specified number of models that + satisfy a logic of a certain size. + """ assert number_elements > 0 carrier_set = { ModelValue("a" + str(i)) for i in range(number_elements) } - ordering = set() - - # a(0) is less than all other elements - a0 = ModelValue("a0") - for v in carrier_set: - if v != a0: - ordering.add(a0 < v) - - # Every other element is less than a(n - 1) - an = ModelValue(f"a{number_elements-1}") - for v in carrier_set: - if an != v: - ordering.add(v < an) - possible_designated_values = possible_designations(carrier_set) - solutions: List[Tuple[Model, Dict[Operation, ModelFunction]]] = [] + solutions: List[Tuple[Model, Interpretation]] = [] + for designated_values in possible_designated_values: designated_values = set(designated_values) print("Considering models for designated values", set_to_str(designated_values)) - possible_interps = possible_interpretations(logic, carrier_set, designated_values, ordering) + 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, ordering) + model = Model(carrier_set, set(interpretation.values()), designated_values) # Iteratively test possible interpretations # by adding one axiom at a time for rule in logic.rules: @@ -127,7 +149,6 @@ def generate_model(logic: Logic, number_elements: int, num_solutions: int = -1, if is_valid: solutions.append((model, interpretation)) - # satisfied_models.append(model) if print_model: print(model, flush=True) diff --git a/logic.py b/logic.py index b38bbdd..58511c6 100644 --- a/logic.py +++ b/logic.py @@ -1,4 +1,4 @@ -from typing import Any, Set, Tuple +from typing import Set, Tuple from functools import lru_cache class Operation: diff --git a/model.py b/model.py index 620c19b..ab5b11f 100644 --- a/model.py +++ b/model.py @@ -13,7 +13,8 @@ from itertools import combinations_with_replacement, permutations, product from typing import Dict, List, Set, Tuple -__all__ = ['ModelValue', 'ModelFunction', 'Model'] +__all__ = ['ModelValue', 'ModelFunction', 'Model', 'Interpretation'] + class ModelValue: def __init__(self, name): @@ -63,6 +64,8 @@ class ModelFunction: def __call__(self, *args): return self.mapping[args] +Interpretation = Dict[Operation, ModelFunction] + class Model: def __init__( self,