From 39a6bf84fb6c37dfa973767827505f306949b1b2 Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Sun, 21 Apr 2024 17:37:21 -0400
Subject: [PATCH] Playing around with orderings

---
 generate_model.py |  8 ++++----
 model.py          | 40 +++++++++++++++++++++++++++++++++++-----
 2 files changed, 39 insertions(+), 9 deletions(-)

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: