Code cleanup

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]:
+def only_rules_with(rules: Set[Rule], operation: Operation) -> List[Rule]:
-    result_rules = []
+    """
+    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]):
+        designated_values: Set[ModelValue]):
-    operations = []
+    """
-    model_functions = []
+    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
+        Discard candidate functions that don't pass
-        in the rules with the operation by itself.
+        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)
 

logic.py

@@ -1,4 +1,4 @@
-from typing import Any, Set, Tuple
+from typing import Set, Tuple
 from functools import lru_cache
 
 class Operation:

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,