From df5b0f5161046d133ca7f662226e9ba24bba688b Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Wed, 29 May 2024 13:50:20 -0400 Subject: [PATCH] Pretty printing --- R.py | 50 ++++++++++++++++++++++++--------------- generate_model.py | 4 ++-- logic.py | 36 ++++++++++++++++------------ model.py | 60 ++++++++++++++++++++++++++++++++++++++++++----- vsp.py | 24 ++++++++++--------- 5 files changed, 121 insertions(+), 53 deletions(-) diff --git a/R.py b/R.py index 6e690bb..426941a 100644 --- a/R.py +++ b/R.py @@ -17,7 +17,9 @@ from vsp import has_vsp # =================================================== -# Defining the logic of R +""" +Defining the Logic of R +""" x = PropositionalVariable("x") y = PropositionalVariable("y") @@ -59,12 +61,13 @@ logic_rules = implication_rules | negation_rules | conjunction_rules | disjuncti operations = {Negation, Conjunction, Disjunction, Implication} -R_logic = Logic(operations, logic_rules) +R_logic = Logic(operations, logic_rules, "R") # =============================== -# Example 2-element Model of R - +""" +Example 2-Element Model of R +""" a0 = ModelValue("a0") a1 = ModelValue("a1") @@ -103,7 +106,7 @@ designated_values = {a1} logical_operations = { mnegation, mimplication, mconjunction, mdisjunction } -R_model_2 = Model(carrier_set, logical_operations, designated_values) +R_model_2 = Model(carrier_set, logical_operations, designated_values, "R2") interpretation = { Negation: mnegation, @@ -112,25 +115,36 @@ interpretation = { Implication: mimplication } +print(R_model_2) + # ================================= -# Generate models of R of a given size +""" +Generate models of R of a specified size +""" + +print("*" * 30) model_size = 2 -solutions = generate_model(R_logic, model_size, print_model=True) +print("Generating models of Logic", R_logic.name, "of size", model_size) +solutions = generate_model(R_logic, model_size, print_model=False) -print(f"There are {len(solutions)} satisfiable models of element length {model_size}") +print(f"Found {len(solutions)} satisfiable models") for model, interpretation in solutions: print(has_vsp(model, interpretation)) -print("-" * 5) +print("*" * 30) ###### -# Smallest model for R that has the variable sharing property -# This has 6 elements +""" +Showing the smallest model for R that has the +variable sharing property. + +This model has 6 elements. +""" a0 = ModelValue("a0") a1 = ModelValue("a1") @@ -149,7 +163,7 @@ mnegation = ModelFunction(1, { a2: a2, a1: a4, a0: a5 -}) +}, "¬") mimplication = ModelFunction(2, { (a5, a5): a5, @@ -193,7 +207,7 @@ mimplication = ModelFunction(2, { (a0, a2): a5, (a0, a1): a5, (a0, a0): a5 -}) +}, "→") mconjunction = ModelFunction(2, { @@ -238,7 +252,7 @@ mconjunction = ModelFunction(2, { (a0, a2): a0, (a0, a1): a0, (a0, a0): a0 -}) +}, "∧") mdisjunction = ModelFunction(2, { (a5, a5): a5, @@ -282,12 +296,12 @@ mdisjunction = ModelFunction(2, { (a0, a2): a2, (a0, a1): a1, (a0, a0): a0 -}) +}, "∨") logical_operations = { mnegation, mimplication, mconjunction, mdisjunction } -R_model_6 = Model(carrier_set, logical_operations, designated_values) +R_model_6 = Model(carrier_set, logical_operations, designated_values, "R6") interpretation = { Negation: mnegation, @@ -297,7 +311,5 @@ interpretation = { } print(R_model_6) - -print("Satisfiable", satisfiable(R_logic, R_model_6, interpretation)) - +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)) diff --git a/generate_model.py b/generate_model.py index 79121ad..1306adc 100644 --- a/generate_model.py +++ b/generate_model.py @@ -6,10 +6,10 @@ from common import set_to_str from logic import Logic, Operation, Rule, get_operations_from_term from model import ( Interpretation, ModelValue, Model, - satisfiable, ModelFunction + ModelFunction, satisfiable ) from itertools import combinations, chain, product -from typing import Set, List, Dict, Tuple +from typing import Set, List, Tuple def possible_designations(iterable): """Powerset without the empty and complete set""" diff --git a/logic.py b/logic.py index 58511c6..39eb95d 100644 --- a/logic.py +++ b/logic.py @@ -1,4 +1,4 @@ -from typing import Set, Tuple +from typing import Optional, Set, Tuple from functools import lru_cache class Operation: @@ -9,10 +9,10 @@ class Operation: def immutable(self, name, value): raise Exception("Operations are immutable") self.__setattr__ = immutable - + def __hash__(self): return self.hashed_value - + def __call__(self, *args): # Ensure the arity is met assert len(args) == self.arity @@ -20,7 +20,7 @@ class Operation: for t in args: assert isinstance(t, Term) return OpTerm(self, args) - + class Term: def __init__(self): @@ -35,7 +35,7 @@ class PropositionalVariable(Term): def immutable(self, name, value): raise Exception("Propositional variables are immutable") self.__setattr__ = immutable - + def __hash__(self): return self.hashed_value @@ -53,10 +53,10 @@ class OpTerm(Term): def immutable(self, name, value): raise Exception("Terms are immutable") self.__setattr__ = immutable - + def __hash__(self): return self.hashed_value - + def __str__(self): arg_strs = [str(a) for a in self.arguments] return self.operation.symbol + "(" + ",".join(arg_strs) + ")" @@ -72,13 +72,13 @@ class Inequation: self.antecedant = antecedant self.consequent = consequent def __str__(self): - return str(self.antecedant) + "≤" + str(self.consequent) + return str(self.antecedant) + "≤" + str(self.consequent) class InequalityRule: def __init__(self, premises : Set[Inequation], conclusion: Inequation): self.premises = premises self.conclusion = conclusion - + def __str__(self): str_premises = [str(p) for p in self.premises] str_premises2 = "{" + ",".join(str_premises) + "}" @@ -88,16 +88,22 @@ class Rule: def __init__(self, premises : Set[Term], conclusion: Term): self.premises = premises self.conclusion = conclusion - + def __str__(self): str_premises = [str(p) for p in self.premises] str_premises2 = "{" + ",".join(str_premises) + "}" return str(str_premises2) + "=>" + str(self.conclusion) class Logic: - def __init__(self, operations: Set[Operation], rules: Set[Rule]): + def __init__(self, + operations: Set[Operation], rules: Set[Rule], + name: Optional[str] = None): self.operations = operations self.rules = rules + self.name = str(abs(hash(( + frozenset(operations), + frozenset(rules) + ))))[:5] if name is None else name def get_prop_var_from_term(t: Term) -> Set[PropositionalVariable]: @@ -107,7 +113,7 @@ def get_prop_var_from_term(t: Term) -> Set[PropositionalVariable]: result: Set[PropositionalVariable] = set() for arg in t.arguments: result |= get_prop_var_from_term(arg) - + return result @lru_cache @@ -118,7 +124,7 @@ def get_propostional_variables(rules: Tuple[Rule]) -> Set[PropositionalVariable] # 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) @@ -127,9 +133,9 @@ def get_propostional_variables(rules: Tuple[Rule]) -> Set[PropositionalVariable] def get_operations_from_term(t: Term) -> Set[Operation]: if isinstance(t, PropositionalVariable): return set() - + result: Set[Operation] = {t.operation,} for arg in t.arguments: result |= get_operations_from_term(arg) - + return result diff --git a/model.py b/model.py index ab5b11f..46406b5 100644 --- a/model.py +++ b/model.py @@ -8,9 +8,9 @@ from logic import ( Operation, PropositionalVariable, Term ) from collections import defaultdict -from functools import lru_cache -from itertools import combinations_with_replacement, permutations, product -from typing import Dict, List, Set, Tuple +from functools import cached_property, lru_cache, reduce +from itertools import chain, combinations_with_replacement, permutations, product +from typing import Dict, List, Optional, Set, Tuple __all__ = ['ModelValue', 'ModelFunction', 'Model', 'Interpretation'] @@ -32,7 +32,6 @@ class ModelValue: def __deepcopy__(self, _): return ModelValue(self.name) - class ModelFunction: def __init__(self, arity: int, mapping, operation_name = ""): self.operation_name = operation_name @@ -54,7 +53,21 @@ class ModelFunction: self.mapping = corrected_mapping + @cached_property + def domain(self): + result_set: Set[ModelValue] = set() + for args in self.mapping.keys(): + for v in args: + result_set.add(v) + return result_set + def __str__(self): + if self.arity == 1: + return unary_function_str(self) + elif self.arity == 2: + return binary_function_str(self) + + # Default return dictionary representation str_dict = dict() for k, v in self.mapping.items(): inputstr = "(" + ", ".join(str(ki) for ki in k) + ")" @@ -64,6 +77,33 @@ class ModelFunction: def __call__(self, *args): return self.mapping[args] + +def unary_function_str(f: ModelFunction) -> str: + assert isinstance(f, ModelFunction) and f.arity == 1 + sorted_domain = sorted(f.domain, key=lambda v : v.name) + header_line = f" {f.operation_name} | " + " ".join((str(v) for v in sorted_domain)) + sep_line = "-" + ("-" * len(f.operation_name)) + "-+-" +\ + ("-" * len(sorted_domain)) +\ + ("-" * reduce(lambda sum, v : sum + len(v.name), sorted_domain, 0)) + data_line = (" " * (len(f.operation_name) + 2)) + "| " + " ".join((str(f.mapping[(v,)]) for v in sorted_domain)) + return "\n".join((header_line, sep_line, data_line)) + "\n" + +def binary_function_str(f: ModelFunction) -> str: + assert isinstance(f, ModelFunction) and f.arity == 2 + sorted_domain = sorted(f.domain, key=lambda v : v.name) + max_col_width = max(chain((len(v.name) for v in sorted_domain), (len(f.operation_name),))) + header_line = f" {f.operation_name} " +\ + (" " * (max_col_width - len(f.operation_name))) + "| " +\ + " ".join((str(v) for v in sorted_domain)) + sep_line = "-" + ("-" * max_col_width) + "-+-" +\ + ("-" * len(sorted_domain)) +\ + ("-" * reduce(lambda sum, v : sum + len(v.name), sorted_domain, 0)) + data_lines = "" + for row_v in sorted_domain: + data_line = f" {row_v.name} | " + " ".join((str(f.mapping[(row_v, col_v)]) for col_v in sorted_domain)) + data_lines += data_line + "\n" + return "\n".join((header_line, sep_line, data_lines)) + Interpretation = Dict[Operation, ModelFunction] class Model: @@ -72,20 +112,28 @@ class Model: carrier_set: Set[ModelValue], logical_operations: Set[ModelFunction], designated_values: Set[ModelValue], + 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.name = str(abs(hash(( + frozenset(carrier_set), + frozenset(logical_operations), + frozenset(designated_values) + ))))[:5] if name is None else name def __str__(self): - result = f"""Carrier Set: {set_to_str(self.carrier_set)} + result = ("=" * 25) + f""" +Model Name: {self.name} +Carrier Set: {set_to_str(self.carrier_set)} Designated Values: {set_to_str(self.designated_values)} """ for function in self.logical_operations: result += f"{str(function)}\n" - return result + return result + ("=" * 25) + "\n" def evaluate_term( diff --git a/vsp.py b/vsp.py index 094fadd..23d6beb 100644 --- a/vsp.py +++ b/vsp.py @@ -4,6 +4,7 @@ sharing property. """ from itertools import chain, combinations, product from typing import Dict, List, Optional, Set, Tuple +from common import set_to_str from model import ( Model, model_closure, ModelFunction, ModelValue ) @@ -39,20 +40,21 @@ def preseed( class VSP_Result: def __init__( - self, has_vsp: bool, subalgebra1: Optional[Set[ModelValue]] = None, - subalgebra2: Optional[Set[ModelValue]] = None, x: Optional[ModelValue] = None, - y: Optional[ModelValue] = None): + self, has_vsp: bool, model_name: Optional[str] = None, + subalgebra1: Optional[Set[ModelValue]] = None, + subalgebra2: Optional[Set[ModelValue]] = None): self.has_vsp = has_vsp + self.model_name = model_name self.subalgebra1 = subalgebra1 self.subalgebra2 = subalgebra2 - self.x = x - self.y = y def __str__(self): - if self.has_vsp: - return "Model has the variable sharing property." - else: - return "Model does not have the variable sharing property." + if not self.has_vsp: + return f"Model {self.model_name} does not have the variable sharing property." + return f"""Model {self.model_name} has the variable sharing property. +Subalgebra 1: {set_to_str(self.subalgebra1)} +Subalgebra 2: {set_to_str(self.subalgebra2)} +""" def has_vsp(model: Model, interpretation: Dict[Operation, ModelFunction]) -> VSP_Result: """ @@ -131,6 +133,6 @@ def has_vsp(model: Model, interpretation: Dict[Operation, ModelFunction]) -> VSP break if falsified: - return VSP_Result(True, carrier_set_left, carrier_set_right, x2, y2) + return VSP_Result(True, model.name, carrier_set_left, carrier_set_right) - return VSP_Result(False) + return VSP_Result(False, model.name)