From d431030b418edd5971e22a850428f5d6b1d11022 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Sun, 9 Feb 2025 11:28:09 -0500 Subject: [PATCH] Added case for when negation is defined --- vsp.py | 7 ++++++- vspursuer.py | 11 ++++++----- 2 files changed, 12 insertions(+), 6 deletions(-) diff --git a/vsp.py b/vsp.py index df18341..26d9d28 100644 --- a/vsp.py +++ b/vsp.py @@ -107,7 +107,10 @@ Subalgebra 1: {set_to_str(self.subalgebra1)} Subalgebra 2: {set_to_str(self.subalgebra2)} """ -def has_vsp(model: Model, impfunction: ModelFunction, mconjunction: Optional[ModelFunction] = None, mdisjunction: Optional[ModelFunction] = None) -> VSP_Result: +def has_vsp(model: Model, impfunction: ModelFunction, + mconjunction: Optional[ModelFunction] = None, + mdisjunction: Optional[ModelFunction] = None, + mnegation: Optional[ModelFunction] = None) -> VSP_Result: """ Checks whether a model has the variable sharing property. @@ -173,6 +176,8 @@ def has_vsp(model: Model, impfunction: ModelFunction, mconjunction: Optional[Mod # If the subalgebras are order-dependent, skip this pair if order_dependent(xs, ys, model.ordering): continue + if mnegation is not None and order_dependent(ys, xs, model.ordering): + continue # Compute the closure of all operations # with just the xs diff --git a/vspursuer.py b/vspursuer.py index 66716a3..72b4615 100755 --- a/vspursuer.py +++ b/vspursuer.py @@ -3,7 +3,7 @@ from os import cpu_count import argparse import multiprocessing as mp -from logic import Conjunction, Disjunction, Implication +from logic import Conjunction, Disjunction, Negation, Implication from parse_magic import SourceFile, parse_matrices from vsp import has_vsp, VSP_Result @@ -24,19 +24,20 @@ if __name__ == "__main__": # NOTE: When subprocess gets spawned, the logical operations will # have a different memory address than what's expected in interpretation. - # This will make it so that we can pass the model functions directly instead. + # Therefore, we need to pass the model functions directly instead. solutions_expanded = [] for model, interpretation in solutions: impfunction = interpretation[Implication] mconjunction = interpretation.get(Conjunction) mdisjunction = interpretation.get(Disjunction) - solutions_expanded.append((model, impfunction, mconjunction, mdisjunction)) + mnegation = interpretation.get(Negation) + solutions_expanded.append((model, impfunction, mconjunction, mdisjunction, mnegation)) num_has_vsp = 0 with mp.Pool(processes=max(cpu_count() - 2, 1)) as pool: results = [ - pool.apply_async(has_vsp, (model, impfunction, mconjunction, mdisjunction,)) - for model, impfunction, mconjunction, mdisjunction in solutions_expanded + pool.apply_async(has_vsp, (model, impfunction, mconjunction, mdisjunction, mnegation)) + for model, impfunction, mconjunction, mdisjunction, mnegation in solutions_expanded ] for i, result in enumerate(results):