diff --git a/generate_model.py b/generate_model.py index bae9e1a..11108b2 100644 --- a/generate_model.py +++ b/generate_model.py @@ -3,7 +3,7 @@ File which generates all the models """ from common import set_to_str from logic import Logic, Operation, Rule, get_operations_from_term, PropositionalVariable -from model import ModelValue, Model, satisfiable, ModelFunction +from model import ModelValue, Model, satisfiable, ModelFunction, ModelOrderConstraint from itertools import combinations, chain, product from typing import Set @@ -48,7 +48,7 @@ def only_rules_with(rules: Set[Rule], operation: Operation) -> Set[Rule]: def possible_interpretations( logic: Logic, carrier_set: Set[ModelValue], - designated_values: Set[ModelValue]): + designated_values: Set[ModelValue], ordering: Set[ModelOrderConstraint]): operations = [] model_functions = [] @@ -64,7 +64,7 @@ def possible_interpretations( if len(restricted_rules) > 0: small_logic = Logic({operation,}, restricted_rules) for f in candidate_functions: - small_model = Model(carrier_set, {f,}, designated_values) + small_model = Model(carrier_set, {f,}, designated_values, ordering) interp = {operation: f} if satisfiable(small_logic, small_model, interp): passed_functions.append(f) @@ -112,7 +112,7 @@ def generate_model(logic: Logic, number_elements: int, num_solutions: int = -1, 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) + possible_interps = possible_interpretations(logic, carrier_set, designated_values, ordering) for interpretation in possible_interps: is_valid = True diff --git a/model.py b/model.py index 513fdf5..b2a80ed 100644 --- a/model.py +++ b/model.py @@ -4,7 +4,7 @@ Defining what it means to be a model from common import set_to_str from logic import ( PropositionalVariable, get_propostional_variables, Logic, Term, -Operation +Operation, Conjunction, Disjunction ) from typing import Set, List, Dict, Tuple, Optional from itertools import product @@ -130,14 +130,44 @@ def all_model_valuations_cached( mvalues: Tuple[ModelValue]): return list(all_model_valuations(pvars, mvalues)) +def rule_ordering_satisfied(model: Model, interpretation: Dict[Operation, ModelFunction]) -> bool: + """ + Currently testing whether this function helps with runtime... + """ + if Conjunction in interpretation: + possible_inputs = ((a, b) for (a, b) in product(model.carrier_set, model.carrier_set)) + for a, b in possible_inputs: + output = interpretation[Conjunction](a, b) + if a < b in model.ordering and output != a: + print("RETURNING FALSE") + return False + if b < a in model.ordering and output != b: + print("RETURNING FALSE") + return False + + if Disjunction in interpretation: + possible_inputs = ((a, b) for (a, b) in product(model.carrier_set, model.carrier_set)) + for a, b in possible_inputs: + output = interpretation[Disjunction](a, b) + if a < b in model.ordering and output != b: + print("RETURNING FALSE") + return False + if b < a in model.ordering and output != a: + print("RETURNING FALSE") + return False + + return True + + + def satisfiable(logic: Logic, model: Model, interpretation: Dict[Operation, ModelFunction]) -> bool: pvars = tuple(get_propostional_variables(tuple(logic.rules))) mappings = all_model_valuations_cached(pvars, tuple(model.carrier_set)) - """ - TODO: Make sure that ordering for conjunction and disjunction - at the model function level. - """ + # NOTE: Does not look like rule ordering is helping for finding + # models of R... + if not rule_ordering_satisfied(model, interpretation): + return False for mapping in mappings: for rule in logic.rules: