From 4b907281a55e3c71de66e81b4e98b425381b8757 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Fri, 31 Jan 2025 17:16:25 -0500 Subject: [PATCH] Implementing optimization #14 Discard subalgebras which are order-dependent --- model.py | 16 ++++++++++++++++ parse_magic.py | 15 ++++++++++----- vsp.py | 18 +++++++++++++++++- 3 files changed, 43 insertions(+), 6 deletions(-) diff --git a/model.py b/model.py index 2fff5ac..0451cfc 100644 --- a/model.py +++ b/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), diff --git a/parse_magic.py b/parse_magic.py index bab221a..78ca826 100644 --- a/parse_magic.py +++ b/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]]: """ diff --git a/vsp.py b/vsp.py index ad2849b..df18341 100644 --- a/vsp.py +++ b/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)