Pretty printing

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(f"Model {R_model_6.name} satisfies logic {R_logic.name}?", satisfiable(R_logic, R_model_6, interpretation))
-print("Satisfiable", satisfiable(R_logic, R_model_6, interpretation))
-
 print(has_vsp(R_model_6, interpretation))

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"""

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

model.py

@@ -8,9 +8,9 @@ from logic import (
     Operation, PropositionalVariable, Term
 )
 from collections import defaultdict
-from functools import lru_cache
+from functools import cached_property, lru_cache, reduce
-from itertools import combinations_with_replacement, permutations, product
+from itertools import chain, combinations_with_replacement, permutations, product
-from typing import Dict, List, Set, Tuple
+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(

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,
+            self, has_vsp: bool, model_name: Optional[str] = None,
-            subalgebra2: Optional[Set[ModelValue]] = None, x: Optional[ModelValue] = None,
+            subalgebra1: Optional[Set[ModelValue]] = None,
-            y: Optional[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:
+        if not self.has_vsp:
-            return "Model has the variable sharing property."
+            return f"Model {self.model_name} does not have the variable sharing property."
-        else:
+        return f"""Model {self.model_name} has the variable sharing property.
-            return "Model does not have 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)