Implementing optimization #14

Discard subalgebras which are order-dependent

model.py

@@ -103,18 +103,34 @@ def binary_function_str(f: ModelFunction) -> str:
 
 Interpretation = Dict[Operation, ModelFunction]
 
+class OrderTable:
+    def __init__(self):
+        self.ordering = set()
+
+    def add(self, x, y):
+        """
+        Add x <= y
+        """
+        self.ordering.add((x, y))
+
+    def is_lt(self, x, y):
+        return (x, y) in self.ordering
+
+
 class Model:
     def __init__(
             self,
             carrier_set: Set[ModelValue],
             logical_operations: Set[ModelFunction],
             designated_values: Set[ModelValue],
+            ordering: Optional[OrderTable] = None,
             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.ordering = ordering
         self.name = str(abs(hash((
             frozenset(carrier_set),
             frozenset(logical_operations),

parse_magic.py

@@ -6,7 +6,7 @@ Assumes the base logic is R with no extra connectives
 import re
 from typing import TextIO, List, Optional, Tuple, Set, Dict
 
-from model import Model, ModelValue, ModelFunction
+from model import Model, ModelValue, ModelFunction, OrderTable
 from logic import (
     Implication,
     Conjunction,
@@ -65,6 +65,7 @@ class ModelBuilder:
         self.size : int = 0
         self.carrier_set : Set[ModelValue] = set()
         self.mnegation: Optional[ModelFunction] = None
+        self.ordering: Optional[OrderTable] = None
         self.mconjunction: Optional[ModelFunction] = None
         self.mdisjunction: Optional[ModelFunction] = None
         self.designated_values: Set[ModelValue] = set()
@@ -278,7 +279,8 @@ def process_orders(infile: SourceFile, current_model_parts: ModelBuilder) -> boo
     if result is None:
         return False
 
-    mconjunction, mdisjunction = result
+    ordering, mconjunction, mdisjunction = result
+    current_model_parts.ordering = ordering
     current_model_parts.mconjunction = mconjunction
     current_model_parts.mdisjunction = mdisjunction
 
@@ -334,7 +336,7 @@ def process_model(model_name: str, mp: ModelBuilder,  solutions: List[Tuple[Mode
     assert mp.mimplication is not None
 
     logical_operations = { mp.mimplication }
-    model = Model(mp.carrier_set, logical_operations, mp.designated_values, name=model_name)
+    model = Model(mp.carrier_set, logical_operations, mp.designated_values, ordering=mp.ordering, name=model_name)
     interpretation = {
         Implication: mp.mimplication
     }
@@ -466,7 +468,7 @@ def determine_dresult(size: int, ordering: Dict[ModelValue, ModelValue], a: Mode
         if not invalid:
             return c
 
-def parse_single_order(infile: SourceFile, size: int) -> Optional[Tuple[ModelFunction, ModelFunction]]:
+def parse_single_order(infile: SourceFile, size: int) -> Optional[Tuple[OrderTable, ModelFunction, ModelFunction]]:
     """
     Parse the line representing the ordering table
     """
@@ -478,6 +480,7 @@ def parse_single_order(infile: SourceFile, size: int) -> Optional[Tuple[ModelFun
 
     assert len(table) == (size + 1)**2, f"Order table doesn't match expected size at line {infile.current_line}"
 
+    ordering = OrderTable()
     omapping = {}
     table_i = 0
 
@@ -486,6 +489,8 @@ def parse_single_order(infile: SourceFile, size: int) -> Optional[Tuple[ModelFun
         for j in range(size + 1):
             y = mvalue_from_index(j)
             omapping[(x, y)] = table[table_i] == '1'
+            if table[table_i] == '1':
+                ordering.add(x, y)
             table_i += 1
 
     cmapping = {}
@@ -514,7 +519,7 @@ def parse_single_order(infile: SourceFile, size: int) -> Optional[Tuple[ModelFun
     mconjunction = ModelFunction(2, cmapping, "∧")
     mdisjunction = ModelFunction(2, dmapping, "∨")
 
-    return mconjunction, mdisjunction
+    return ordering, mconjunction, mdisjunction
 
 def parse_single_designated(infile: SourceFile, size: int) -> Optional[Set[ModelValue]]:
     """

vsp.py

@@ -6,7 +6,7 @@ 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
+    Model, model_closure, ModelFunction, ModelValue, OrderTable
 )
 from logic import Conjunction, Disjunction, Implication, Operation
 
@@ -79,6 +79,15 @@ def find_bottom(algebra: Set[ModelValue], mconjunction: Optional[ModelFunction],
     print("[Warning] Failed to find the bottom of the lattice")
     return None
 
+def order_dependent(subalgebra1: Set[ModelValue], subalegbra2: Set[ModelValue], ordering: OrderTable):
+    """
+    Returns true if there exists a value in subalgebra1 that's less than a value in subalgebra2
+    """
+    for x in subalgebra1:
+        for y in subalegbra2:
+            if ordering.is_lt(x, y):
+                return True
+    return False
 
 class VSP_Result:
     def __init__(
@@ -111,6 +120,8 @@ def has_vsp(model: Model, impfunction: ModelFunction, mconjunction: Optional[Mod
     if len(model.designated_values) == 1:
         return VSP_Result(False, model.name)
 
+    assert model.ordering is not None, "Expected ordering table in model"
+
     # Compute I the set of tuples (x, y) where
     # x -> y does not take a designiated value
     I: Set[Tuple[ModelValue, ModelValue]] = set()
@@ -158,6 +169,11 @@ def has_vsp(model: Model, impfunction: ModelFunction, mconjunction: Optional[Mod
         if bottom is not None and bottom in xs:
             continue
 
+        # NOTE: Optimization
+        # If the subalgebras are order-dependent, skip this pair
+        if order_dependent(xs, ys, model.ordering):
+            continue
+
         # Compute the closure of all operations
         # with just the xs
         carrier_set_left: Set[ModelValue] = model_closure(xs, model.logical_operations, bottom)