From b06dd8ee013c6dbafa31fb3d40d5946d3b5a7f75 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Tue, 10 Dec 2024 17:17:14 -0800 Subject: [PATCH 01/29] Don't rely on shared memory for logic operators --- vsp.py | 5 +---- vspursuer.py | 16 ++++++++++++---- 2 files changed, 13 insertions(+), 8 deletions(-) diff --git a/vsp.py b/vsp.py index 6a50c63..ad2849b 100644 --- a/vsp.py +++ b/vsp.py @@ -98,14 +98,11 @@ Subalgebra 1: {set_to_str(self.subalgebra1)} Subalgebra 2: {set_to_str(self.subalgebra2)} """ -def has_vsp(model: Model, interpretation: Dict[Operation, ModelFunction]) -> VSP_Result: +def has_vsp(model: Model, impfunction: ModelFunction, mconjunction: Optional[ModelFunction] = None, mdisjunction: Optional[ModelFunction] = None) -> VSP_Result: """ Checks whether a model has the variable sharing property. """ - impfunction = interpretation[Implication] - mconjunction = interpretation.get(Conjunction) - mdisjunction = interpretation.get(Disjunction) top = find_top(model.carrier_set, mconjunction, mdisjunction) bottom = find_bottom(model.carrier_set, mconjunction, mdisjunction) diff --git a/vspursuer.py b/vspursuer.py index 5a6ee55..70e0f02 100755 --- a/vspursuer.py +++ b/vspursuer.py @@ -1,7 +1,8 @@ #!/usr/bin/env python3 from os import cpu_count import argparse -import multiprocessing +import multiprocessing as mp +from logic import Implication, Conjunction, Disjunction from parse_magic import ( SourceFile, @@ -24,11 +25,18 @@ if __name__ == "__main__": solutions = parse_matrices(SourceFile(data_file)) print(f"Parsed {len(solutions)} matrices") + solutions_prep = [] + for model, interpretation in solutions: + impfunction = interpretation[Implication] + mconjunction = interpretation.get(Conjunction) + mdisjunction = interpretation.get(Disjunction) + solutions_prep.append((model, impfunction, mconjunction, mdisjunction)) + num_has_vsp = 0 - with multiprocessing.Pool(processes=max(cpu_count() - 2, 1)) as pool: + with mp.Pool(processes=max(cpu_count() - 2, 1)) as pool: results = [ - pool.apply_async(has_vsp, (model, interpretation,)) - for model, interpretation in solutions + pool.apply_async(has_vsp, (model, impfunction, mconjunction, mdisjunction,)) + for model, impfunction, mconjunction, mdisjunction in solutions_prep ] for i, result in enumerate(results): From 70cd1cfa7f02bf737c9d6c9e48374571573792c4 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Tue, 10 Dec 2024 18:34:43 -0500 Subject: [PATCH 02/29] Small cleanup --- vspursuer.py | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/vspursuer.py b/vspursuer.py index 70e0f02..66716a3 100755 --- a/vspursuer.py +++ b/vspursuer.py @@ -2,12 +2,9 @@ from os import cpu_count import argparse import multiprocessing as mp -from logic import Implication, Conjunction, Disjunction -from parse_magic import ( - SourceFile, - parse_matrices -) +from logic import Conjunction, Disjunction, Implication +from parse_magic import SourceFile, parse_matrices from vsp import has_vsp, VSP_Result if __name__ == "__main__": @@ -25,18 +22,21 @@ if __name__ == "__main__": solutions = parse_matrices(SourceFile(data_file)) print(f"Parsed {len(solutions)} matrices") - solutions_prep = [] + # 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. + solutions_expanded = [] for model, interpretation in solutions: impfunction = interpretation[Implication] mconjunction = interpretation.get(Conjunction) mdisjunction = interpretation.get(Disjunction) - solutions_prep.append((model, impfunction, mconjunction, mdisjunction)) + solutions_expanded.append((model, impfunction, mconjunction, mdisjunction)) 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_prep + for model, impfunction, mconjunction, mdisjunction in solutions_expanded ] for i, result in enumerate(results): From 4b907281a55e3c71de66e81b4e98b425381b8757 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Fri, 31 Jan 2025 17:16:25 -0500 Subject: [PATCH 03/29] 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) From 2ff9f8134c969bb27ce49ca38e6a437e0787ac70 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Sun, 9 Feb 2025 10:57:52 -0500 Subject: [PATCH 04/29] Implemented optimization #29 --- vsp.py | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/vsp.py b/vsp.py index ad2849b..b223982 100644 --- a/vsp.py +++ b/vsp.py @@ -3,12 +3,11 @@ Check to see if the model has the variable sharing property. """ from itertools import chain, combinations, product -from typing import Dict, List, Optional, Set, Tuple +from typing import List, Optional, Set, Tuple from common import set_to_str from model import ( Model, model_closure, ModelFunction, ModelValue ) -from logic import Conjunction, Disjunction, Implication, Operation def preseed( initial_set: Set[ModelValue], @@ -145,10 +144,19 @@ def has_vsp(model: Model, impfunction: ModelFunction, mconjunction: Optional[Mod # NOTE: Optimziation before model_closure # If the two subalgebras intersect, move - # onto the next pair + # onto the next pair. if len(xs & ys) > 0: continue + # NOTE: Optimization + # If a subalgebra doesn't have at least one + # designated value, move onto the next pair. + if len(xs & model.designated_values) == 0: + continue + + if len(ys & model.designated_values) == 0: + continue + # NOTE: Optimization # If the left subalgebra contains bottom # or the right subalgebra contains top From f9d307969e9f3b4489a02bfab1159c11cb9f002f Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Sun, 9 Feb 2025 11:00:39 -0500 Subject: [PATCH 05/29] Added small note --- vsp.py | 1 + 1 file changed, 1 insertion(+) diff --git a/vsp.py b/vsp.py index b223982..d38ec42 100644 --- a/vsp.py +++ b/vsp.py @@ -151,6 +151,7 @@ def has_vsp(model: Model, impfunction: ModelFunction, mconjunction: Optional[Mod # NOTE: Optimization # If a subalgebra doesn't have at least one # designated value, move onto the next pair. + # Depends on no intersection between xs and ys if len(xs & model.designated_values) == 0: continue From 54dc6e503ce383cbc7f32d21dcade04b144111d0 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Sun, 9 Feb 2025 11:05:40 -0500 Subject: [PATCH 06/29] Configurable CPU usage --- vspursuer.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/vspursuer.py b/vspursuer.py index 66716a3..449cfa0 100755 --- a/vspursuer.py +++ b/vspursuer.py @@ -11,6 +11,7 @@ if __name__ == "__main__": parser = argparse.ArgumentParser(description="VSP Checker") parser.add_argument("--verbose", action='store_true', help="Print out all parsed matrices") parser.add_argument("-i", type=str, help="Path to MaGIC ugly data file") + parser.add_argument("-c", type=int, help="Number of CPUs to use. Default: MAX - 2.") args = vars(parser.parse_args()) data_file_path = args.get("i") @@ -33,7 +34,8 @@ if __name__ == "__main__": solutions_expanded.append((model, impfunction, mconjunction, mdisjunction)) num_has_vsp = 0 - with mp.Pool(processes=max(cpu_count() - 2, 1)) as pool: + num_cpu = args.get("c", max(cpu_count() - 2, 1)) + with mp.Pool(processes=num_cpu) as pool: results = [ pool.apply_async(has_vsp, (model, impfunction, mconjunction, mdisjunction,)) for model, impfunction, mconjunction, mdisjunction in solutions_expanded From cad3e85cd09df0785afbdcd03bdb9396922696ef Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Sun, 9 Feb 2025 11:14:27 -0500 Subject: [PATCH 07/29] Implemented feature #31 --- vspursuer.py | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/vspursuer.py b/vspursuer.py index 449cfa0..5e5e904 100755 --- a/vspursuer.py +++ b/vspursuer.py @@ -12,6 +12,7 @@ if __name__ == "__main__": parser.add_argument("--verbose", action='store_true', help="Print out all parsed matrices") parser.add_argument("-i", type=str, help="Path to MaGIC ugly data file") parser.add_argument("-c", type=int, help="Number of CPUs to use. Default: MAX - 2.") + parser.add_argument("--skip-to", type=str, help="Skip until a model name is found and process from then onwards.") args = vars(parser.parse_args()) data_file_path = args.get("i") @@ -23,11 +24,19 @@ if __name__ == "__main__": solutions = parse_matrices(SourceFile(data_file)) print(f"Parsed {len(solutions)} matrices") + start_processing = args.get("skip_to") is None + # 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. solutions_expanded = [] for model, interpretation in solutions: + # If skip_to is defined, then don't process models + # until then. + if not start_processing and model.name == args.get("skip_to"): + start_processing = True + if not start_processing: + continue impfunction = interpretation[Implication] mconjunction = interpretation.get(Conjunction) mdisjunction = interpretation.get(Disjunction) @@ -46,10 +55,10 @@ if __name__ == "__main__": print(vsp_result) if args['verbose'] or vsp_result.has_vsp: - model = solutions[i][0] + model = solutions_expanded[i][0] print(model) if vsp_result.has_vsp: num_has_vsp += 1 - print(f"Tested {len(solutions)} models, {num_has_vsp} of which satisfy VSP") + print(f"Tested {len(solutions_expanded)} models, {num_has_vsp} of which satisfy VSP") From b1a046b70b4f3a09fafcc280236b1a87bf00362c Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Sun, 9 Feb 2025 11:18:52 -0500 Subject: [PATCH 08/29] Removed unused inequality rules --- logic.py | 19 ------------------- 1 file changed, 19 deletions(-) diff --git a/logic.py b/logic.py index 5b2994c..7775590 100644 --- a/logic.py +++ b/logic.py @@ -27,8 +27,6 @@ class Operation: class Term: def __init__(self): pass - def __lt__(self, y): - return Inequation(self, y) class PropositionalVariable(Term): def __init__(self, name): @@ -70,23 +68,6 @@ Disjunction = Operation("∨", 2) Implication = Operation("→", 2) Necessitation = Operation("!", 1) -class Inequation: - def __init__(self, antecedant : Term, consequent: Term): - self.antecedant = antecedant - self.consequent = consequent - def __str__(self): - return str(self.antecedant) + "≤" + str(self.consequent) - -class InequalityRule: - def __init__(self, premises : Set[Inequation], conclusion: Inequation): - self.premises = premises - self.conclusion = conclusion - - def __str__(self): - str_premises = [str(p) for p in self.premises] - str_premises2 = "{" + ",".join(str_premises) + "}" - return str(str_premises2) + "=>" + str(self.conclusion) - class Rule: def __init__(self, premises : Set[Term], conclusion: Term): self.premises = premises From d431030b418edd5971e22a850428f5d6b1d11022 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Sun, 9 Feb 2025 11:28:09 -0500 Subject: [PATCH 09/29] 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): From 1a4857429f4d0c137a0019921bbdb3e5e4751b36 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Tue, 18 Feb 2025 13:38:39 -0500 Subject: [PATCH 10/29] Use partition instead of split/join --- parse_magic.py | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/parse_magic.py b/parse_magic.py index 78ca826..7980741 100644 --- a/parse_magic.py +++ b/parse_magic.py @@ -45,10 +45,7 @@ class SourceFile: self.reststr = next(self.fileobj).strip() self.current_line += 1 - tokens = self.reststr.split(" ") - next_token = tokens[0] - self.reststr = " ".join(tokens[1:]) - + next_token, _, self.reststr = self.reststr.partition(" ") return next_token class UglyHeader: From 4412b6c2dab59313fa7eb39e7de4cde24b29c172 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Tue, 18 Mar 2025 18:08:28 -0400 Subject: [PATCH 11/29] Redid parallel implementation - Made parse_matrices into a generator - Keep track of num_proccesses results and spawn new ones when done --- parse_magic.py | 16 +++--- vspursuer.py | 152 ++++++++++++++++++++++++++++++++++++------------- 2 files changed, 121 insertions(+), 47 deletions(-) diff --git a/parse_magic.py b/parse_magic.py index 7980741..b693c31 100644 --- a/parse_magic.py +++ b/parse_magic.py @@ -4,7 +4,7 @@ Parses the Magic Ugly Data File Format Assumes the base logic is R with no extra connectives """ import re -from typing import TextIO, List, Optional, Tuple, Set, Dict +from typing import TextIO, List, Iterator, Optional, Tuple, Set, Dict from model import Model, ModelValue, ModelFunction, OrderTable from logic import ( @@ -167,8 +167,7 @@ def derive_stages(header: UglyHeader) -> Stages: return stages -def parse_matrices(infile: SourceFile) -> List[Tuple[Model, Dict]]: - solutions = [] +def parse_matrices(infile: SourceFile) -> Iterator[Tuple[Model, Dict[Operation, ModelFunction]]]: header = parse_header(infile) stages = derive_stages(header) first_run = True @@ -179,7 +178,7 @@ def parse_matrices(infile: SourceFile) -> List[Tuple[Model, Dict]]: case "end": break case "process_model": - process_model(stages.name(), current_model_parts, solutions) + yield process_model(stages.name(), current_model_parts) stage = stage.next case "size": processed = process_sizes(infile, current_model_parts, first_run) @@ -245,8 +244,6 @@ def parse_matrices(infile: SourceFile) -> List[Tuple[Model, Dict]]: stages.reset_after(stage.name) stage = stage.previous - return solutions - def process_sizes(infile: SourceFile, current_model_parts: ModelBuilder, first_run: bool) -> bool: try: size = parse_size(infile, first_run) @@ -325,7 +322,7 @@ def process_custom_connective(infile: SourceFile, symbol: str, adicity: int, cur current_model_parts.custom_model_functions[symbol] = mfunction return True -def process_model(model_name: str, mp: ModelBuilder, solutions: List[Tuple[Model, Dict]]): +def process_model(model_name: str, mp: ModelBuilder) -> Tuple[Model, Dict[Operation, ModelFunction]]: """Create Model""" assert mp.size > 0 assert mp.size + 1 == len(mp.carrier_set) @@ -333,7 +330,6 @@ 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, ordering=mp.ordering, name=model_name) interpretation = { Implication: mp.mimplication } @@ -355,8 +351,10 @@ def process_model(model_name: str, mp: ModelBuilder, solutions: List[Tuple[Mode logical_operations.add(custom_mf) op = Operation(custom_mf.operation_name, custom_mf.arity) interpretation[op] = custom_mf + + model = Model(mp.carrier_set, logical_operations, mp.designated_values, ordering=mp.ordering, name=model_name) + return (model, interpretation) - solutions.append((model, interpretation)) def parse_header(infile: SourceFile) -> UglyHeader: """ diff --git a/vspursuer.py b/vspursuer.py index fc4d5f8..864568d 100755 --- a/vspursuer.py +++ b/vspursuer.py @@ -1,11 +1,69 @@ #!/usr/bin/env python3 -from os import cpu_count +from os import process_cpu_count +from time import sleep +from typing import Dict, Iterator, Optional, Tuple import argparse import multiprocessing as mp -from logic import Conjunction, Disjunction, Negation, Implication +from logic import Conjunction, Disjunction, Negation, Implication, Operation +from model import Model, ModelFunction from parse_magic import SourceFile, parse_matrices -from vsp import has_vsp, VSP_Result +from vsp import has_vsp + +def restructure_solutions(solutions: Iterator[Tuple[Model, Dict[Operation, ModelFunction]]], args) -> \ + Iterator[Tuple[Model, ModelFunction, Optional[ModelFunction], Optional[ModelFunction], Optional[ModelFunction]]]: + """ + When subprocess gets spawned, the logical operations will + have a different memory address than what's expected in interpretation. + Therefore, we need to pass the model functions directly instead. + + While we're at it, filter out models until we get to --skip-to + if applicable. + """ + start_processing = args.get("skip_to") is None + for model, interpretation in solutions: + # If skip_to is defined, then don't process models + # until then. + if not start_processing and model.name == args.get("skip_to"): + start_processing = True + if not start_processing: + continue + impfunction = interpretation[Implication] + mconjunction = interpretation.get(Conjunction) + mdisjunction = interpretation.get(Disjunction) + mnegation = interpretation.get(Negation) + yield (model, impfunction, mconjunction, mdisjunction, mnegation) + +def has_vsp_plus_model(model, impfunction, mconjunction, mdisjunction, mnegation): + """ + Wrapper so that we can save the model that satisfies VSP. + NOTE: At the time of writing, models that don't satisfy VSP + get discarded from memory for efficiency sake. + """ + vsp_result = has_vsp(model, impfunction, mconjunction, mdisjunction, mnegation) + if vsp_result.has_vsp: + return (model, vsp_result) + return (None, vsp_result) + +def create_chunks(data, chunk_size: int): + """ + Takes a stream of data and creates a new + stream where each element is a "chunk" of + several primitive elements. + Ex: create_chunks((1, 2, 3, 4, 5, 6), 2) -> + ((1, 2), (3, 4), (5, 6)) + """ + chunk = [] + for item in data: + chunk.append(item) + if len(chunk) == chunk_size: + yield tuple(chunk) + chunk = [] + + if len(chunk) > 0: + yield tuple(chunk) + + if __name__ == "__main__": parser = argparse.ArgumentParser(description="VSP Checker") @@ -19,47 +77,65 @@ if __name__ == "__main__": if data_file_path is None: data_file_path = input("Path to MaGIC Ugly Data File: ") - solutions = [] - with open(data_file_path, "r") as data_file: - solutions = parse_matrices(SourceFile(data_file)) - print(f"Parsed {len(solutions)} matrices") + data_file = open(data_file_path, "r") - start_processing = args.get("skip_to") is None + solutions = parse_matrices(SourceFile(data_file)) + solutions = restructure_solutions(solutions, args) - # NOTE: When subprocess gets spawned, the logical operations will - # have a different memory address than what's expected in interpretation. - # Therefore, we need to pass the model functions directly instead. - solutions_expanded = [] - for model, interpretation in solutions: - # If skip_to is defined, then don't process models - # until then. - if not start_processing and model.name == args.get("skip_to"): - start_processing = True - if not start_processing: - continue - impfunction = interpretation[Implication] - mconjunction = interpretation.get(Conjunction) - mdisjunction = interpretation.get(Disjunction) - mnegation = interpretation.get(Negation) - solutions_expanded.append((model, impfunction, mconjunction, mdisjunction, mnegation)) + num_cpu = args.get("c") + if num_cpu is None: + num_cpu = max(process_cpu_count() - 2, 1) + # solution_chunks = create_chunks(solutions, num_cpu * 2) + + # Set up parallel verification + num_tested = 0 num_has_vsp = 0 - num_cpu = args.get("c", max(cpu_count() - 2, 1)) with mp.Pool(processes=num_cpu) as pool: - results = [ - pool.apply_async(has_vsp, (model, impfunction, mconjunction, mdisjunction, mnegation)) - for model, impfunction, mconjunction, mdisjunction, mnegation in solutions_expanded - ] + task_pool = [] + done_parsing = False - for i, result in enumerate(results): - vsp_result: VSP_Result = result.get() - print(vsp_result) + # Populate initial task pool + for _ in range(num_cpu): + try: + model, impfunction, mconjunction, mdisjunction, mnegation = next(solutions) + except StopIteration: + done_parsing = True + break + result_async = pool.apply_async(has_vsp_plus_model, (model, impfunction, mconjunction, mdisjunction, mnegation)) + task_pool.append(result_async) - if args['verbose'] or vsp_result.has_vsp: - model = solutions_expanded[i][0] - print(model) + while len(task_pool) > 0: + next_task_pool = [] + # Check the status of all the tasks, and spawn + # new ones if finished + for result_async in task_pool: + if result_async.ready(): + model, vsp_result = result_async.get() + print(vsp_result) + num_tested += 1 - if vsp_result.has_vsp: - num_has_vsp += 1 + if args['verbose'] or vsp_result.has_vsp: + print(model) - print(f"Tested {len(solutions_expanded)} models, {num_has_vsp} of which satisfy VSP") + if vsp_result.has_vsp: + num_has_vsp += 1 + + if done_parsing: + continue + + # Submit new task if available + try: + model, impfunction, mconjunction, mdisjunction, mnegation = next(solutions) + next_result_async = pool.apply_async(has_vsp_plus_model, (model, impfunction, mconjunction, mdisjunction, mnegation)) + next_task_pool.append(next_result_async) + except StopIteration: + done_parsing = True + else: + next_task_pool.append(result_async) + task_pool = next_task_pool + sleep(0.01) + + print(f"Tested {num_tested} models, {num_has_vsp} of which satisfy VSP") + + data_file.close() From c554c531417c577db595aa2edf2aa7f3ca15322c Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Wed, 19 Mar 2025 09:22:54 -0400 Subject: [PATCH 12/29] Removed dead code --- vspursuer.py | 22 ---------------------- 1 file changed, 22 deletions(-) diff --git a/vspursuer.py b/vspursuer.py index 864568d..417a556 100755 --- a/vspursuer.py +++ b/vspursuer.py @@ -45,26 +45,6 @@ def has_vsp_plus_model(model, impfunction, mconjunction, mdisjunction, mnegation return (model, vsp_result) return (None, vsp_result) -def create_chunks(data, chunk_size: int): - """ - Takes a stream of data and creates a new - stream where each element is a "chunk" of - several primitive elements. - Ex: create_chunks((1, 2, 3, 4, 5, 6), 2) -> - ((1, 2), (3, 4), (5, 6)) - """ - chunk = [] - for item in data: - chunk.append(item) - if len(chunk) == chunk_size: - yield tuple(chunk) - chunk = [] - - if len(chunk) > 0: - yield tuple(chunk) - - - if __name__ == "__main__": parser = argparse.ArgumentParser(description="VSP Checker") parser.add_argument("--verbose", action='store_true', help="Print out all parsed matrices") @@ -86,8 +66,6 @@ if __name__ == "__main__": if num_cpu is None: num_cpu = max(process_cpu_count() - 2, 1) - # solution_chunks = create_chunks(solutions, num_cpu * 2) - # Set up parallel verification num_tested = 0 num_has_vsp = 0 From 154cee034915d32b57bd3ebdbcd1c6a92ebe23f2 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Wed, 19 Mar 2025 09:29:02 -0400 Subject: [PATCH 13/29] Switched to cpu_count --- vspursuer.py | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/vspursuer.py b/vspursuer.py index 417a556..7e42368 100755 --- a/vspursuer.py +++ b/vspursuer.py @@ -1,5 +1,7 @@ #!/usr/bin/env python3 -from os import process_cpu_count + +# NOTE: Perhaps we should use process_cpu_count but that's not available to all Python versions +from os import cpu_count from time import sleep from typing import Dict, Iterator, Optional, Tuple import argparse @@ -64,7 +66,7 @@ if __name__ == "__main__": num_cpu = args.get("c") if num_cpu is None: - num_cpu = max(process_cpu_count() - 2, 1) + num_cpu = max(cpu_count() - 2, 1) # Set up parallel verification num_tested = 0 @@ -110,6 +112,8 @@ if __name__ == "__main__": except StopIteration: done_parsing = True else: + # Otherwise the task is still working, + # add it to the next task pool next_task_pool.append(result_async) task_pool = next_task_pool sleep(0.01) From 502252676f6155f7df6a9bf0ba09780d6a9bbe13 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Tue, 8 Apr 2025 21:10:28 -0400 Subject: [PATCH 14/29] Rewrote multiprocessing as the prior approach was unreliable --- vspursuer.py | 145 +++++++++++++++++++++++++++++++++++---------------- 1 file changed, 99 insertions(+), 46 deletions(-) diff --git a/vspursuer.py b/vspursuer.py index 7e42368..be04ebc 100755 --- a/vspursuer.py +++ b/vspursuer.py @@ -2,8 +2,8 @@ # NOTE: Perhaps we should use process_cpu_count but that's not available to all Python versions from os import cpu_count -from time import sleep from typing import Dict, Iterator, Optional, Tuple +from queue import Empty as QueueEmpty import argparse import multiprocessing as mp @@ -38,14 +38,51 @@ def restructure_solutions(solutions: Iterator[Tuple[Model, Dict[Operation, Model def has_vsp_plus_model(model, impfunction, mconjunction, mdisjunction, mnegation): """ - Wrapper so that we can save the model that satisfies VSP. - NOTE: At the time of writing, models that don't satisfy VSP - get discarded from memory for efficiency sake. + Wrapper which also stores the models along with its vsp result """ vsp_result = has_vsp(model, impfunction, mconjunction, mdisjunction, mnegation) - if vsp_result.has_vsp: - return (model, vsp_result) - return (None, vsp_result) + return (model, vsp_result) + +def worker(task_queue, result_queue): + """ + Worker process which processes models from the task + queue and adds the result to the result_queue. + + Adds the sentinal value None when exception occurs and when there's + no more to process. + """ + try: + while True: + task = task_queue.get() + # If sentinal value, break + if task is None: + result_queue.put(None) + break + (model, impfunction, mconjunction, mdisjunction, mnegation) = task + result = has_vsp_plus_model(model, impfunction, mconjunction, mdisjunction, mnegation) + result_queue.put(result) + except Exception: + # Process failed somehow, push sentinal value + result_queue.put(None) + +def add_to_queue(gen, queue, num_sentinal_values) -> bool: + """ + Consumes an item from gen and puts + it in the queue. + + If there are no items left in gen, + return false and send sentinal values, + otherwise true. + """ + try: + item = next(gen) + queue.put(item) + return True + except StopIteration: + for _ in range(num_sentinal_values): + queue.put(None) + return False + if __name__ == "__main__": parser = argparse.ArgumentParser(description="VSP Checker") @@ -71,52 +108,68 @@ if __name__ == "__main__": # Set up parallel verification num_tested = 0 num_has_vsp = 0 - with mp.Pool(processes=num_cpu) as pool: - task_pool = [] - done_parsing = False - # Populate initial task pool - for _ in range(num_cpu): - try: - model, impfunction, mconjunction, mdisjunction, mnegation = next(solutions) - except StopIteration: - done_parsing = True + # Create queues + task_queue = mp.Queue() + result_queue = mp.Queue() + + # Create worker processes + processes = [] + for _ in range(num_cpu): + p = mp.Process(target=worker, args=(task_queue, result_queue)) + processes.append(p) + p.start() + + # Populate initial task queue + done_parsing = False + for _ in range(num_cpu): + added = add_to_queue(solutions, task_queue, num_cpu) + if not added: + done_parsing = True + break + + # Check results and add new tasks until finished + result_sentinal_count = 0 + while True: + + # Read a result + try: + result = result_queue.get(True, 60) + except QueueEmpty: + # Health check in case processes crashed + if all((not p.is_alive() for p in processes)): + print("[WARNING] No child processes remain") break - result_async = pool.apply_async(has_vsp_plus_model, (model, impfunction, mconjunction, mdisjunction, mnegation)) - task_pool.append(result_async) + # Otherwise continue + continue - while len(task_pool) > 0: - next_task_pool = [] - # Check the status of all the tasks, and spawn - # new ones if finished - for result_async in task_pool: - if result_async.ready(): - model, vsp_result = result_async.get() - print(vsp_result) - num_tested += 1 + # When we receive None, it means a child process has finished + if result is None: + result_sentinal_count += 1 + # If all workers have finished break + if result_sentinal_count == num_cpu: + break + continue - if args['verbose'] or vsp_result.has_vsp: - print(model) + # Process result + model, vsp_result = result + print(vsp_result) + num_tested += 1 - if vsp_result.has_vsp: - num_has_vsp += 1 + if vsp_result.has_vsp: + print(model) - if done_parsing: - continue + if vsp_result.has_vsp: + num_has_vsp += 1 + + # Submit new task if available + if done_parsing: + continue + + added = add_to_queue(solutions, task_queue, num_cpu) + if not added: + done_parsing = True - # Submit new task if available - try: - model, impfunction, mconjunction, mdisjunction, mnegation = next(solutions) - next_result_async = pool.apply_async(has_vsp_plus_model, (model, impfunction, mconjunction, mdisjunction, mnegation)) - next_task_pool.append(next_result_async) - except StopIteration: - done_parsing = True - else: - # Otherwise the task is still working, - # add it to the next task pool - next_task_pool.append(result_async) - task_pool = next_task_pool - sleep(0.01) print(f"Tested {num_tested} models, {num_has_vsp} of which satisfy VSP") From 806309b1ae7b470e5dedbf5826e23b6e88dd936d Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Wed, 9 Apr 2025 09:51:19 -0400 Subject: [PATCH 15/29] Adding more work to task queue and more detailed healthcheck --- vspursuer.py | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/vspursuer.py b/vspursuer.py index be04ebc..20c3004 100755 --- a/vspursuer.py +++ b/vspursuer.py @@ -121,8 +121,10 @@ if __name__ == "__main__": p.start() # Populate initial task queue + # NOTE: Adding more than number of processes + # to make sure there's always work to do. done_parsing = False - for _ in range(num_cpu): + for _ in range(num_cpu * 2): added = add_to_queue(solutions, task_queue, num_cpu) if not added: done_parsing = True @@ -137,9 +139,15 @@ if __name__ == "__main__": result = result_queue.get(True, 60) except QueueEmpty: # Health check in case processes crashed - if all((not p.is_alive() for p in processes)): - print("[WARNING] No child processes remain") + num_dead = 0 + for p in processes: + if not p.is_alive(): + num_dead += 1 + if num_dead == len(processes): + print("[ERROR] No child processes remain") break + elif num_dead > 0: + print("[WARNING] Number of dead processes:", num_dead) # Otherwise continue continue From cb00a82c678d5bee92f5e7bed16b7f29021f12c8 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Wed, 9 Apr 2025 10:59:02 -0400 Subject: [PATCH 16/29] Attempt at keeping workers busy --- vspursuer.py | 22 ++++++++++++++++++---- 1 file changed, 18 insertions(+), 4 deletions(-) diff --git a/vspursuer.py b/vspursuer.py index 20c3004..34c219d 100755 --- a/vspursuer.py +++ b/vspursuer.py @@ -139,7 +139,7 @@ if __name__ == "__main__": result = result_queue.get(True, 60) except QueueEmpty: # Health check in case processes crashed - num_dead = 0 + num_dead = 0 for p in processes: if not p.is_alive(): num_dead += 1 @@ -174,10 +174,24 @@ if __name__ == "__main__": if done_parsing: continue - added = add_to_queue(solutions, task_queue, num_cpu) - if not added: - done_parsing = True + # NOTE: We should attempt to maintain a decent amount + # of work in the task queue so that workers stay busy + task_queue_size: Optional[int] = None + try: + task_queue_size = task_queue.qsize() + except NotImplementedError: + # On MacOS this isn't implemented + pass + num_new_tasks = 1 + if task_queue_size is not None and task_queue_size < num_cpu * 2: + num_new_tasks = (num_cpu * 2) - task_queue_size + + for _ in range(num_new_tasks): + added = add_to_queue(solutions, task_queue, num_cpu) + if not added: + done_parsing = True + break print(f"Tested {num_tested} models, {num_has_vsp} of which satisfy VSP") From de8637bca4a71cd2466bcaad07738414ee87e907 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Wed, 9 Apr 2025 13:00:08 -0400 Subject: [PATCH 17/29] Dedicated process for file parsing --- vspursuer.py | 125 +++++++++++++++++++++++---------------------------- 1 file changed, 55 insertions(+), 70 deletions(-) diff --git a/vspursuer.py b/vspursuer.py index 34c219d..9c6537b 100755 --- a/vspursuer.py +++ b/vspursuer.py @@ -43,7 +43,7 @@ def has_vsp_plus_model(model, impfunction, mconjunction, mdisjunction, mnegation vsp_result = has_vsp(model, impfunction, mconjunction, mdisjunction, mnegation) return (model, vsp_result) -def worker(task_queue, result_queue): +def worker_vsp(task_queue, result_queue): """ Worker process which processes models from the task queue and adds the result to the result_queue. @@ -56,32 +56,39 @@ def worker(task_queue, result_queue): task = task_queue.get() # If sentinal value, break if task is None: - result_queue.put(None) break (model, impfunction, mconjunction, mdisjunction, mnegation) = task result = has_vsp_plus_model(model, impfunction, mconjunction, mdisjunction, mnegation) result_queue.put(result) - except Exception: - # Process failed somehow, push sentinal value + finally: + # Either an exception occured or the worker finished + # Push sentinal value result_queue.put(None) -def add_to_queue(gen, queue, num_sentinal_values) -> bool: +def worker_parser(data_file_path, num_sentinal_values, task_queue): """ - Consumes an item from gen and puts - it in the queue. + Function which parses the MaGIC file + and adds models to the task_queue. - If there are no items left in gen, - return false and send sentinal values, - otherwise true. + Intended to be deployed with a dedicated process. """ try: - item = next(gen) - queue.put(item) - return True - except StopIteration: + data_file = open(data_file_path, "r") + solutions = parse_matrices(SourceFile(data_file)) + solutions = restructure_solutions(solutions, args) + + while True: + try: + item = next(solutions) + task_queue.put(item) + except StopIteration: + break + finally: + data_file.close() for _ in range(num_sentinal_values): - queue.put(None) - return False + task_queue.put(None) + + if __name__ == "__main__": @@ -96,10 +103,6 @@ if __name__ == "__main__": if data_file_path is None: data_file_path = input("Path to MaGIC Ugly Data File: ") - data_file = open(data_file_path, "r") - - solutions = parse_matrices(SourceFile(data_file)) - solutions = restructure_solutions(solutions, args) num_cpu = args.get("c") if num_cpu is None: @@ -108,27 +111,23 @@ if __name__ == "__main__": # Set up parallel verification num_tested = 0 num_has_vsp = 0 + num_workers = max(num_cpu - 1, 1) # Create queues - task_queue = mp.Queue() + task_queue = mp.Queue(maxsize=1000) result_queue = mp.Queue() - # Create worker processes - processes = [] - for _ in range(num_cpu): - p = mp.Process(target=worker, args=(task_queue, result_queue)) - processes.append(p) + # Create dedicated process to parse the MaGIC file + process_parser = mp.Process(target=worker_parser, args=(data_file_path, num_workers, task_queue)) + process_parser.start() + + # Create dedicated processes which check VSP + process_workers = [] + for _ in range(num_workers): + p = mp.Process(target=worker_vsp, args=(task_queue, result_queue)) + process_workers.append(p) p.start() - # Populate initial task queue - # NOTE: Adding more than number of processes - # to make sure there's always work to do. - done_parsing = False - for _ in range(num_cpu * 2): - added = add_to_queue(solutions, task_queue, num_cpu) - if not added: - done_parsing = True - break # Check results and add new tasks until finished result_sentinal_count = 0 @@ -138,24 +137,32 @@ if __name__ == "__main__": try: result = result_queue.get(True, 60) except QueueEmpty: - # Health check in case processes crashed - num_dead = 0 - for p in processes: - if not p.is_alive(): - num_dead += 1 - if num_dead == len(processes): - print("[ERROR] No child processes remain") + if all((not p.is_alive() for p in process_workers)): + # All workers finished without us receiving all the + # sentinal values. break - elif num_dead > 0: - print("[WARNING] Number of dead processes:", num_dead) - # Otherwise continue - continue + + task_queue_size = 0 + try: + task_queue_size = task_queue.qsize() + except NotImplementedError: + # MacOS doesn't implement this + pass + + if task_queue_size == 0 and not process_parser.is_alive(): + # For Linux/Windows this means that the process_parser + # died before sending the sentinal values. + # For Mac, this doesn't guarentee anything but might + # as well push more sentinal values. + for _ in range(num_workers): + task_queue.put(None) + # When we receive None, it means a child process has finished if result is None: result_sentinal_count += 1 # If all workers have finished break - if result_sentinal_count == num_cpu: + if result_sentinal_count == len(process_workers): break continue @@ -170,29 +177,7 @@ if __name__ == "__main__": if vsp_result.has_vsp: num_has_vsp += 1 - # Submit new task if available - if done_parsing: - continue - - # NOTE: We should attempt to maintain a decent amount - # of work in the task queue so that workers stay busy - task_queue_size: Optional[int] = None - try: - task_queue_size = task_queue.qsize() - except NotImplementedError: - # On MacOS this isn't implemented - pass - - num_new_tasks = 1 - if task_queue_size is not None and task_queue_size < num_cpu * 2: - num_new_tasks = (num_cpu * 2) - task_queue_size - - for _ in range(num_new_tasks): - added = add_to_queue(solutions, task_queue, num_cpu) - if not added: - done_parsing = True - break print(f"Tested {num_tested} models, {num_has_vsp} of which satisfy VSP") - data_file.close() + From 6f5074584b4c6c8271addc3639d6faedb8b9cc2c Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Fri, 2 May 2025 12:08:15 -0400 Subject: [PATCH 18/29] Cleanup and small optimizations --- model.py | 3 ++ parse_magic.py | 127 ++++++++++++++++++++++++++----------------------- vspursuer.py | 25 +++++----- 3 files changed, 85 insertions(+), 70 deletions(-) diff --git a/model.py b/model.py index 0451cfc..508fe84 100644 --- a/model.py +++ b/model.py @@ -103,6 +103,9 @@ def binary_function_str(f: ModelFunction) -> str: Interpretation = Dict[Operation, ModelFunction] +# TODO: Replace with a nicer representation +# Include meet and join functions +# Something like x : (all elements less than x) class OrderTable: def __init__(self): self.ordering = set() diff --git a/parse_magic.py b/parse_magic.py index b693c31..e4f1daa 100644 --- a/parse_magic.py +++ b/parse_magic.py @@ -5,6 +5,7 @@ Assumes the base logic is R with no extra connectives """ import re from typing import TextIO, List, Iterator, Optional, Tuple, Set, Dict +from itertools import product from model import Model, ModelValue, ModelFunction, OrderTable from logic import ( @@ -19,7 +20,7 @@ from logic import ( class SourceFile: def __init__(self, fileobj: TextIO): self.fileobj = fileobj - self.current_line = 0 + self.line_in_file = 0 self.reststr = "" def next_line(self): @@ -34,7 +35,7 @@ class SourceFile: return reststr contents = next(self.fileobj).strip() - self.current_line += 1 + self.line_in_file += 1 return contents def __next__(self): @@ -43,7 +44,7 @@ class SourceFile: """ if self.reststr == "": self.reststr = next(self.fileobj).strip() - self.current_line += 1 + self.line_in_file += 1 next_token, _, self.reststr = self.reststr.partition(" ") return next_token @@ -60,7 +61,7 @@ class UglyHeader: class ModelBuilder: def __init__(self): self.size : int = 0 - self.carrier_set : Set[ModelValue] = set() + self.carrier_list : List[ModelValue] = [] self.mnegation: Optional[ModelFunction] = None self.ordering: Optional[OrderTable] = None self.mconjunction: Optional[ModelFunction] = None @@ -97,8 +98,6 @@ class Stages: def add(self, name: str): stage = Stage(name) - stage.next = stage - stage.previous = self.last_added_stage # End stage is a sink so don't @@ -115,11 +114,16 @@ class Stages: def reset_after(self, name): """ - Resets the stage counters after a given stage. - This is to accurately reflect the name of the - model within MaGIC. + Resets the counters of every stage after + a given stage. + + This is to accurately reflect how names are + generated within magic. + Example: 1.1, 1.2, (reset after 1), 2.1, 2.2 """ stage = self.stages[name] + # NOTE: The process_model stage doesn't + # have a counter associated with it. while stage.name != "process_model": stage.reset() stage = stage.next @@ -128,15 +132,26 @@ class Stages: return self.stages[name] def name(self): + """ + Get the full name of where we are within + the parsing process. Takes into account + the stage number of all the stages seen + so far. + """ + + # Stages haven't been added yet result = "" stage = self.first_stage if stage is None: return "" + # There's only one stage result = f"{stage.num}" if stage.next == "process_model": return result + # Add every subsequent stage counter + # by appending .stage_num stage = stage.next while stage is not None: result += f".{stage.num}" @@ -172,6 +187,7 @@ def parse_matrices(infile: SourceFile) -> Iterator[Tuple[Model, Dict[Operation, stages = derive_stages(header) first_run = True current_model_parts = ModelBuilder() + stage = stages.first_stage while True: match stage.name: @@ -245,22 +261,24 @@ def parse_matrices(infile: SourceFile) -> Iterator[Tuple[Model, Dict[Operation, stage = stage.previous def process_sizes(infile: SourceFile, current_model_parts: ModelBuilder, first_run: bool) -> bool: + size: Optional[int] = None try: size = parse_size(infile, first_run) except StopIteration: - return False + pass + if size is None: return False - carrier_set = carrier_set_from_size(size) - current_model_parts.carrier_set = carrier_set + carrier_list = carrier_list_from_size(size) + current_model_parts.carrier_list = carrier_list current_model_parts.size = size return True def process_negations(infile: SourceFile, current_model_parts: ModelBuilder) -> bool: """Stage 2 (Optional)""" - mnegation = parse_single_monadic_connective(infile, "¬", current_model_parts.size) + mnegation = parse_single_monadic_connective(infile, "¬", current_model_parts.size, current_model_parts.carrier_list) if mnegation is None: return False @@ -269,7 +287,7 @@ def process_negations(infile: SourceFile, current_model_parts: ModelBuilder) -> def process_orders(infile: SourceFile, current_model_parts: ModelBuilder) -> bool: """Stage 3""" - result = parse_single_order(infile, current_model_parts.size) + result = parse_single_order(infile, current_model_parts.size, current_model_parts.carrier_list) if result is None: return False @@ -299,7 +317,7 @@ def process_implications(infile: SourceFile, current_model_parts: ModelBuilder) return True def process_necessitations(infile: SourceFile, current_model_parts: ModelBuilder) -> bool: - mnecessitation = parse_single_monadic_connective(infile, "!", current_model_parts.size) + mnecessitation = parse_single_monadic_connective(infile, "!", current_model_parts.size, current_model_parts.carrier_list) if mnecessitation is None: return False @@ -310,7 +328,7 @@ def process_custom_connective(infile: SourceFile, symbol: str, adicity: int, cur if adicity == 0: mfunction = parse_single_nullary_connective(infile, symbol) elif adicity == 1: - mfunction = parse_single_monadic_connective(infile, symbol, current_model_parts.size) + mfunction = parse_single_monadic_connective(infile, symbol, current_model_parts.size, current_model_parts.carrier_list) elif adicity == 2: mfunction = parse_single_dyadic_connective(infile, symbol, current_model_parts.size) else: @@ -325,8 +343,8 @@ def process_custom_connective(infile: SourceFile, symbol: str, adicity: int, cur def process_model(model_name: str, mp: ModelBuilder) -> Tuple[Model, Dict[Operation, ModelFunction]]: """Create Model""" assert mp.size > 0 - assert mp.size + 1 == len(mp.carrier_set) - assert len(mp.designated_values) <= len(mp.carrier_set) + assert mp.size + 1 == len(mp.carrier_list) + assert len(mp.designated_values) <= len(mp.carrier_list) assert mp.mimplication is not None logical_operations = { mp.mimplication } @@ -351,8 +369,8 @@ def process_model(model_name: str, mp: ModelBuilder) -> Tuple[Model, Dict[Operat logical_operations.add(custom_mf) op = Operation(custom_mf.operation_name, custom_mf.arity) interpretation[op] = custom_mf - - model = Model(mp.carrier_set, logical_operations, mp.designated_values, ordering=mp.ordering, name=model_name) + + model = Model(set(mp.carrier_list), logical_operations, mp.designated_values, ordering=mp.ordering, name=model_name) return (model, interpretation) @@ -375,14 +393,14 @@ def parse_header(infile: SourceFile) -> UglyHeader: custom_model_functions.append((arity, symbol)) return UglyHeader(negation_defined, necessitation_defined, custom_model_functions) -def carrier_set_from_size(size: int) -> Set[ModelValue]: +def carrier_list_from_size(size: int) -> List[ModelValue]: """ Construct a carrier set of model values based on the desired size. """ - return { + return [ mvalue_from_index(i) for i in range(size + 1) - } + ] def parse_size(infile: SourceFile, first_run: bool) -> Optional[int]: """ @@ -399,7 +417,7 @@ def parse_size(infile: SourceFile, first_run: bool) -> Optional[int]: if size == -1: return None - assert size > 0, f"Unexpected size at line {infile.current_line}" + assert size > 0, f"Unexpected size at line {infile.line_in_file}" return size def mvalue_from_index(i: int) -> ModelValue: @@ -463,7 +481,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[OrderTable, ModelFunction, ModelFunction]]: +def parse_single_order(infile: SourceFile, size: int, carrier_list: List[ModelValue]) -> Optional[Tuple[OrderTable, ModelFunction, ModelFunction]]: """ Parse the line representing the ordering table """ @@ -473,43 +491,35 @@ def parse_single_order(infile: SourceFile, size: int) -> Optional[Tuple[OrderTab table = line.split(" ") - assert len(table) == (size + 1)**2, f"Order table doesn't match expected size at line {infile.current_line}" + assert len(table) == (size + 1)**2, f"Order table doesn't match expected size at line {infile.line_in_file}" ordering = OrderTable() omapping = {} table_i = 0 - for i in range(size + 1): - x = mvalue_from_index(i) - 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 + for x, y in product(carrier_list, carrier_list): + omapping[(x, y)] = table[table_i] == '1' + if table[table_i] == '1': + ordering.add(x, y) + table_i += 1 cmapping = {} dmapping = {} - for i in range(size + 1): - x = mvalue_from_index(i) - for j in range(size + 1): - y = mvalue_from_index(j) - - cresult = determine_cresult(size, omapping, x, y) - if cresult is None: - print("[Warning] Conjunction and Disjunction are not well-defined") - print(f"{x} ∧ {y} = ??") - return None, None - cmapping[(x, y)] = cresult - - dresult = determine_dresult(size, omapping, x, y) - if dresult is None: - print("[Warning] Conjunction and Disjunction are not well-defined") - print(f"{x} ∨ {y} = ??") - return None, None - dmapping[(x, y)] = dresult + for x, y in product(carrier_list, carrier_list): + cresult = determine_cresult(size, omapping, x, y) + if cresult is None: + print("[Warning] Conjunction and Disjunction are not well-defined") + print(f"{x} ∧ {y} = ??") + return None, None + cmapping[(x, y)] = cresult + dresult = determine_dresult(size, omapping, x, y) + if dresult is None: + print("[Warning] Conjunction and Disjunction are not well-defined") + print(f"{x} ∨ {y} = ??") + return None, None + dmapping[(x, y)] = dresult mconjunction = ModelFunction(2, cmapping, "∧") mdisjunction = ModelFunction(2, dmapping, "∨") @@ -525,7 +535,7 @@ def parse_single_designated(infile: SourceFile, size: int) -> Optional[Set[Model return None row = line.split(" ") - assert len(row) == size + 1, f"Designated table doesn't match expected size at line {infile.current_line}" + assert len(row) == size + 1, f"Designated table doesn't match expected size at line {infile.line_in_file}" designated_values = set() @@ -543,23 +553,22 @@ def parse_single_nullary_connective(infile: SourceFile, symbol: str) -> Optional return None row = line.split(" ") - assert len(row) == 1, f"More than one assignment for a nullary connective was provided at line {infile.current_line}" + assert len(row) == 1, f"More than one assignment for a nullary connective was provided at line {infile.line_in_file}" mapping = {} mapping[()] = parse_mvalue(row[0]) return ModelFunction(0, mapping, symbol) -def parse_single_monadic_connective(infile: SourceFile, symbol: str, size: int) -> Optional[ModelFunction]: +def parse_single_monadic_connective(infile: SourceFile, symbol: str, size: int, carrier_list: List[ModelValue]) -> Optional[ModelFunction]: line = infile.next_line() if line == '-1': return None row = line.split(" ") - assert len(row) == size + 1, f"{symbol} table doesn't match size at line {infile.current_line}" + assert len(row) == size + 1, f"{symbol} table doesn't match size at line {infile.line_in_file}" mapping = {} - for i, j in zip(range(size + 1), row): - x = mvalue_from_index(i) + for x, j in zip(carrier_list, row): y = parse_mvalue(j) mapping[(x, )] = y @@ -576,7 +585,7 @@ def parse_single_dyadic_connective(infile: SourceFile, symbol: str, size: int) - except StopIteration: pass - assert len(table) == (size + 1)**2, f"{symbol} table does not match expected size at line {infile.current_line}" + assert len(table) == (size + 1)**2, f"{symbol} table does not match expected size at line {infile.line_in_file}" mapping = {} table_i = 0 diff --git a/vspursuer.py b/vspursuer.py index 9c6537b..284c0ef 100755 --- a/vspursuer.py +++ b/vspursuer.py @@ -10,9 +10,9 @@ import multiprocessing as mp from logic import Conjunction, Disjunction, Negation, Implication, Operation from model import Model, ModelFunction from parse_magic import SourceFile, parse_matrices -from vsp import has_vsp +from vsp import has_vsp, VSP_Result -def restructure_solutions(solutions: Iterator[Tuple[Model, Dict[Operation, ModelFunction]]], args) -> \ +def restructure_solutions(solutions: Iterator[Tuple[Model, Dict[Operation, ModelFunction]]], skip_to: Optional[str]) -> \ Iterator[Tuple[Model, ModelFunction, Optional[ModelFunction], Optional[ModelFunction], Optional[ModelFunction]]]: """ When subprocess gets spawned, the logical operations will @@ -22,28 +22,31 @@ def restructure_solutions(solutions: Iterator[Tuple[Model, Dict[Operation, Model While we're at it, filter out models until we get to --skip-to if applicable. """ - start_processing = args.get("skip_to") is None + start_processing = skip_to is None for model, interpretation in solutions: # If skip_to is defined, then don't process models # until then. - if not start_processing and model.name == args.get("skip_to"): - start_processing = True - if not start_processing: + if not start_processing and model.name != skip_to: continue + start_processing = True + + # NOTE: Implication must be defined, the rest may not impfunction = interpretation[Implication] mconjunction = interpretation.get(Conjunction) mdisjunction = interpretation.get(Disjunction) mnegation = interpretation.get(Negation) yield (model, impfunction, mconjunction, mdisjunction, mnegation) -def has_vsp_plus_model(model, impfunction, mconjunction, mdisjunction, mnegation): +def has_vsp_plus_model(model, impfunction, mconjunction, mdisjunction, mnegation) -> Tuple[Optional[Model], VSP_Result]: """ Wrapper which also stores the models along with its vsp result """ vsp_result = has_vsp(model, impfunction, mconjunction, mdisjunction, mnegation) + # NOTE: Memory optimization - Don't return model if it doens't have VSP + model = model if vsp_result.has_vsp else None return (model, vsp_result) -def worker_vsp(task_queue, result_queue): +def worker_vsp(task_queue: mp.Queue, result_queue: mp.Queue): """ Worker process which processes models from the task queue and adds the result to the result_queue. @@ -65,7 +68,7 @@ def worker_vsp(task_queue, result_queue): # Push sentinal value result_queue.put(None) -def worker_parser(data_file_path, num_sentinal_values, task_queue): +def worker_parser(data_file_path: str, num_sentinal_values: int, task_queue: mp.Queue, skip_to: Optional[str]): """ Function which parses the MaGIC file and adds models to the task_queue. @@ -75,7 +78,7 @@ def worker_parser(data_file_path, num_sentinal_values, task_queue): try: data_file = open(data_file_path, "r") solutions = parse_matrices(SourceFile(data_file)) - solutions = restructure_solutions(solutions, args) + solutions = restructure_solutions(solutions, skip_to) while True: try: @@ -118,7 +121,7 @@ if __name__ == "__main__": result_queue = mp.Queue() # Create dedicated process to parse the MaGIC file - process_parser = mp.Process(target=worker_parser, args=(data_file_path, num_workers, task_queue)) + process_parser = mp.Process(target=worker_parser, args=(data_file_path, num_workers, task_queue, args.get("skip_to"))) process_parser.start() # Create dedicated processes which check VSP From fa9e5026caeae78f41805e4134ad54e716cc0a77 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Sat, 3 May 2025 12:54:37 -0400 Subject: [PATCH 19/29] [Draft] Changing OrderTable (Currently non-functional) --- model.py | 48 +++++++++++++++++++++++++++++++++++++++++++++--- parse_magic.py | 9 +++++++-- 2 files changed, 52 insertions(+), 5 deletions(-) diff --git a/model.py b/model.py index 508fe84..39498f7 100644 --- a/model.py +++ b/model.py @@ -108,16 +108,58 @@ Interpretation = Dict[Operation, ModelFunction] # Something like x : (all elements less than x) class OrderTable: def __init__(self): - self.ordering = set() + # a : {x | x <= a } + self.ordering: Dict[ModelValue, Set[ModelValue]] = defaultdict(set) def add(self, x, y): """ Add x <= y """ - self.ordering.add((x, y)) + self.ordering[y].add(x) def is_lt(self, x, y): - return (x, y) in self.ordering + return y in self.ordering[x] + + def meet(self, x, y) -> Optional[ModelValue]: + X = self.ordering[x] + Y = self.ordering[y] + + candidates = X.intersection(Y) + + for m in candidates: + gt_all_candidates = True + for w in candidates: + if not self.is_lt(w, m): + gt_all_candidates = False + break + + if gt_all_candidates: + return m + + # Otherwise the meet does not exist + print("Meet does not exist", (x, y), candidates) + return None + + def join(self, x, y) -> Optional[ModelValue]: + # Grab the collection of elements greater than x and y + candidates = set() + for w in self.ordering: + if self.is_lt(x, w) and self.is_lt(y, w): + candidates.add(w) + + for j in candidates: + lt_all_candidates = True + for w in candidates: + if not self.is_lt(j, w): + lt_all_candidates = False + break + + if lt_all_candidates: + return j + + # Otherwise the join does not exist + print("Join does not exist", (x, y), candidates) + return None class Model: diff --git a/parse_magic.py b/parse_magic.py index e4f1daa..758d735 100644 --- a/parse_magic.py +++ b/parse_magic.py @@ -507,18 +507,23 @@ def parse_single_order(infile: SourceFile, size: int, carrier_list: List[ModelVa dmapping = {} for x, y in product(carrier_list, carrier_list): - cresult = determine_cresult(size, omapping, x, y) + cresult = ordering.meet(x, y) if cresult is None: print("[Warning] Conjunction and Disjunction are not well-defined") print(f"{x} ∧ {y} = ??") return None, None + else: + print(f"{x} ∧ {y} = {cresult}") cmapping[(x, y)] = cresult - dresult = determine_dresult(size, omapping, x, y) + dresult = ordering.join(x, y) + # dresult = determine_dresult(size, omapping, x, y) if dresult is None: print("[Warning] Conjunction and Disjunction are not well-defined") print(f"{x} ∨ {y} = ??") return None, None + else: + print(f"{x} ∨ {y} = {dresult}") dmapping[(x, y)] = dresult mconjunction = ModelFunction(2, cmapping, "∧") From 01204a9551bb873f22116745182b77d620dc91a6 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Sat, 3 May 2025 16:42:15 -0400 Subject: [PATCH 20/29] Code cleanup --- model.py | 171 ++++++++++++++++++++---------------------- parse_magic.py | 169 ++++++++++++++--------------------------- vsp.py | 200 +++++++++++++++++++++---------------------------- vspursuer.py | 99 +++++++++++++++--------- 4 files changed, 286 insertions(+), 353 deletions(-) diff --git a/model.py b/model.py index 39498f7..b9b3af1 100644 --- a/model.py +++ b/model.py @@ -16,9 +16,9 @@ from typing import Dict, List, Optional, Set, Tuple __all__ = ['ModelValue', 'ModelFunction', 'Model', 'Interpretation'] class ModelValue: - def __init__(self, name): + def __init__(self, name: str, hashed_value: Optional[int] = None): self.name = name - self.hashed_value = hash(self.name) + self.hashed_value = hashed_value if hashed_value is not None else hash(self.name) self.__setattr__ = immutable def __str__(self): return self.name @@ -27,7 +27,7 @@ class ModelValue: def __eq__(self, other): return isinstance(other, ModelValue) and self.name == other.name def __deepcopy__(self, _): - return ModelValue(self.name) + return ModelValue(self.name, self.hashed_value) class ModelFunction: def __init__(self, arity: int, mapping, operation_name = ""): @@ -109,57 +109,75 @@ Interpretation = Dict[Operation, ModelFunction] class OrderTable: def __init__(self): # a : {x | x <= a } - self.ordering: Dict[ModelValue, Set[ModelValue]] = defaultdict(set) + self.le_map: Dict[ModelValue, Set[ModelValue]] = defaultdict(set) + # a : {x | x >= a} + self.ge_map: Dict[ModelValue, Set[ModelValue]] = defaultdict(set) def add(self, x, y): """ Add x <= y """ - self.ordering[y].add(x) + self.le_map[y].add(x) + self.ge_map[x].add(y) def is_lt(self, x, y): - return y in self.ordering[x] + return x in self.le_map[y] def meet(self, x, y) -> Optional[ModelValue]: - X = self.ordering[x] - Y = self.ordering[y] + X = self.le_map[x] + Y = self.le_map[y] candidates = X.intersection(Y) - for m in candidates: - gt_all_candidates = True - for w in candidates: - if not self.is_lt(w, m): - gt_all_candidates = False - break + # Grab all elements greater than each of the candidates + candidate_ge_maps = (self.ge_map[candidate] for candidate in candidates) + common_ge_values = reduce(set.intersection, candidate_ge_maps) - if gt_all_candidates: - return m + # Intersect with candidates to get the values that satisfy + # the meet properties + result_set = candidates.intersection(common_ge_values) - # Otherwise the meet does not exist - print("Meet does not exist", (x, y), candidates) - return None + # NOTE: The meet may not exist, in which case return None + result = next(iter(result_set), None) + return result def join(self, x, y) -> Optional[ModelValue]: - # Grab the collection of elements greater than x and y - candidates = set() - for w in self.ordering: - if self.is_lt(x, w) and self.is_lt(y, w): - candidates.add(w) + X = self.ge_map[x] + Y = self.ge_map[y] - for j in candidates: - lt_all_candidates = True - for w in candidates: - if not self.is_lt(j, w): - lt_all_candidates = False - break + candidates = X.intersection(Y) - if lt_all_candidates: - return j + # Grab all elements smaller than each of the candidates + candidate_le_maps = (self.le_map[candidate] for candidate in candidates) + common_le_values = reduce(set.intersection, candidate_le_maps) - # Otherwise the join does not exist - print("Join does not exist", (x, y), candidates) - return None + # Intersect with candidatse to get the values that satisfy + # the join properties + result_set = candidates.intersection(common_le_values) + + # NOTE: The join may not exist, in which case return None + result = next(iter(result_set), None) + return result + + def top(self) -> Optional[ModelValue]: + ge_maps = (self.ge_map[candidate] for candidate in self.ge_map) + result_set = reduce(set.intersection, ge_maps) + + # Either not unique or does not exist + if len(result_set) != 1: + return None + + return next(iter(result_set)) + + def bottom(self) -> Optional[ModelValue]: + le_maps = (self.le_map[candidate] for candidate in self.le_map) + result_set = reduce(set.intersection, le_maps) + + # Either not unique or does not exist + if len(result_set) != 1: + return None + + return next(iter(result_set)) class Model: @@ -276,86 +294,61 @@ def satisfiable(logic: Logic, model: Model, interpretation: Dict[Operation, Mode return True - def model_closure(initial_set: Set[ModelValue], mfunctions: Set[ModelFunction], forbidden_element: Optional[ModelValue]) -> Set[ModelValue]: """ Given an initial set of model values and a set of model functions, compute the complete set of model values that are closed under the operations. - If top or bottom is encountered, then we end the saturation procedure early. + If the forbidden element is encountered, then we end the saturation procedure early. """ closure_set: Set[ModelValue] = initial_set last_new: Set[ModelValue] = initial_set changed: bool = True forbidden_found = False + arities = set() + for mfun in mfunctions: + arities.add(mfun.arity) + while changed: changed = False new_elements: Set[ModelValue] = set() old_closure: Set[ModelValue] = closure_set - last_new # arity -> args - cached_args = defaultdict(list) + args_by_arity = defaultdict(list) - # Pass elements into each model function - for mfun in mfunctions: - - # If a previous function shared the same arity, - # we'll use the same set of computed arguments - # to pass into the model functions. - if mfun.arity in cached_args: - for args in cached_args[mfun.arity]: - # Compute the new elements - # given the cached arguments. - element = mfun(*args) - if element not in closure_set: - new_elements.add(element) - - # Optimization: Break out of computation - # early when forbidden element is found - if forbidden_element is not None and element == forbidden_element: - forbidden_found = True - break - - if forbidden_found: - break - - # We don't need to compute the arguments - # thanks to the cache, so move onto the - # next function. - continue - - # At this point, we don't have cached arguments, so we need - # to compute this set. - - # Each argument must have at least one new element to not repeat - # work. We'll range over the number of new model values within our - # argument. - for num_new in range(1, mfun.arity + 1): + # Motivation: We want to only compute arguments that we have not + # seen before + for arity in arities: + for num_new in range(1, arity + 1): new_args = combinations_with_replacement(last_new, r=num_new) - old_args = combinations_with_replacement(old_closure, r=mfun.arity - num_new) - # Determine every possible ordering of the concatenated - # new and old model values. + old_args = combinations_with_replacement(old_closure, r=arity - num_new) + # Determine every possible ordering of the concatenated new and + # old model values. for new_arg, old_arg in product(new_args, old_args): - for args in permutations(new_arg + old_arg): - cached_args[mfun.arity].append(args) - element = mfun(*args) - if element not in closure_set: - new_elements.add(element) + for combined_args in permutations(new_arg + old_arg): + args_by_arity[arity].append(combined_args) - # Optimization: Break out of computation - # early when forbidden element is found - if forbidden_element is not None and element == forbidden_element: - forbidden_found = True - break - if forbidden_found: - break + # Pass each argument into each model function + for mfun in mfunctions: + for args in args_by_arity[mfun.arity]: + # Compute the new elements + # given the cached arguments. + element = mfun(*args) + if element not in closure_set: + new_elements.add(element) - if forbidden_found: + # Optimization: Break out of computation + # early when forbidden element is found + if forbidden_element is not None and element == forbidden_element: + forbidden_found = True break + if forbidden_found: + break closure_set.update(new_elements) changed = len(new_elements) > 0 diff --git a/parse_magic.py b/parse_magic.py index 758d735..78fc495 100644 --- a/parse_magic.py +++ b/parse_magic.py @@ -72,6 +72,45 @@ class ModelBuilder: # Map symbol to model function self.custom_model_functions: Dict[str, ModelFunction] = {} + def build(self, model_name: str) -> Tuple[Model, Dict[Operation, ModelFunction]]: + """Create Model""" + assert self.size > 0 + assert self.size + 1 == len(self.carrier_list) + assert len(self.designated_values) <= len(self.carrier_list) + assert self.mimplication is not None + + # Implication is required to be present + logical_operations = { self.mimplication } + interpretation = { + Implication: self.mimplication + } + + # Other model functions and logical + # operations are optional + if self.mnegation is not None: + logical_operations.add(self.mnegation) + interpretation[Negation] = self.mnegation + if self.mconjunction is not None: + logical_operations.add(self.mconjunction) + interpretation[Conjunction] = self.mconjunction + if self.mdisjunction is not None: + logical_operations.add(self.mdisjunction) + interpretation[Disjunction] = self.mdisjunction + if self.mnecessitation is not None: + logical_operations.add(self.mnecessitation) + interpretation[Necessitation] = self.mnecessitation + + # Custom model function definitions + for custom_mf in self.custom_model_functions.values(): + if custom_mf is not None: + logical_operations.add(custom_mf) + op = Operation(custom_mf.operation_name, custom_mf.arity) + interpretation[op] = custom_mf + + model = Model(set(self.carrier_list), logical_operations, self.designated_values, ordering=self.ordering, name=model_name) + return (model, interpretation) + + class Stage: def __init__(self, name: str): self.name = name @@ -194,7 +233,7 @@ def parse_matrices(infile: SourceFile) -> Iterator[Tuple[Model, Dict[Operation, case "end": break case "process_model": - yield process_model(stages.name(), current_model_parts) + yield current_model_parts.build(stages.name()) stage = stage.next case "size": processed = process_sizes(infile, current_model_parts, first_run) @@ -300,7 +339,7 @@ def process_orders(infile: SourceFile, current_model_parts: ModelBuilder) -> boo def process_designateds(infile: SourceFile, current_model_parts: ModelBuilder) -> bool: """Stage 4""" - designated_values = parse_single_designated(infile, current_model_parts.size) + designated_values = parse_single_designated(infile, current_model_parts.size, current_model_parts.carrier_list) if designated_values is None: return False @@ -309,7 +348,7 @@ def process_designateds(infile: SourceFile, current_model_parts: ModelBuilder) - def process_implications(infile: SourceFile, current_model_parts: ModelBuilder) -> bool: """Stage 5""" - mimplication = parse_single_dyadic_connective(infile, "→", current_model_parts.size) + mimplication = parse_single_dyadic_connective(infile, "→", current_model_parts.size, current_model_parts.carrier_list) if mimplication is None: return False @@ -330,7 +369,7 @@ def process_custom_connective(infile: SourceFile, symbol: str, adicity: int, cur elif adicity == 1: mfunction = parse_single_monadic_connective(infile, symbol, current_model_parts.size, current_model_parts.carrier_list) elif adicity == 2: - mfunction = parse_single_dyadic_connective(infile, symbol, current_model_parts.size) + mfunction = parse_single_dyadic_connective(infile, symbol, current_model_parts.size, current_model_parts.carrier_list) else: raise NotImplementedError("Unable to process connectives of adicity greater than 2") @@ -340,39 +379,6 @@ def process_custom_connective(infile: SourceFile, symbol: str, adicity: int, cur current_model_parts.custom_model_functions[symbol] = mfunction return True -def process_model(model_name: str, mp: ModelBuilder) -> Tuple[Model, Dict[Operation, ModelFunction]]: - """Create Model""" - assert mp.size > 0 - assert mp.size + 1 == len(mp.carrier_list) - assert len(mp.designated_values) <= len(mp.carrier_list) - assert mp.mimplication is not None - - logical_operations = { mp.mimplication } - interpretation = { - Implication: mp.mimplication - } - if mp.mnegation is not None: - logical_operations.add(mp.mnegation) - interpretation[Negation] = mp.mnegation - if mp.mconjunction is not None: - logical_operations.add(mp.mconjunction) - interpretation[Conjunction] = mp.mconjunction - if mp.mdisjunction is not None: - logical_operations.add(mp.mdisjunction) - interpretation[Disjunction] = mp.mdisjunction - if mp.mnecessitation is not None: - logical_operations.add(mp.mnecessitation) - interpretation[Necessitation] = mp.mnecessitation - - for custom_mf in mp.custom_model_functions.values(): - if custom_mf is not None: - logical_operations.add(custom_mf) - op = Operation(custom_mf.operation_name, custom_mf.arity) - interpretation[op] = custom_mf - - model = Model(set(mp.carrier_list), logical_operations, mp.designated_values, ordering=mp.ordering, name=model_name) - return (model, interpretation) - def parse_header(infile: SourceFile) -> UglyHeader: """ @@ -406,7 +412,6 @@ def parse_size(infile: SourceFile, first_run: bool) -> Optional[int]: """ Parse the line representing the matrix size. """ - size = int(infile.next_line()) # HACK: When necessitation and custom connectives are enabled @@ -417,7 +422,9 @@ def parse_size(infile: SourceFile, first_run: bool) -> Optional[int]: if size == -1: return None + assert size > 0, f"Unexpected size at line {infile.line_in_file}" + return size def mvalue_from_index(i: int) -> ModelValue: @@ -433,55 +440,9 @@ def parse_mvalue(x: str) -> ModelValue: """ return mvalue_from_index(int(x)) -def determine_cresult(size: int, ordering: Dict[ModelValue, ModelValue], a: ModelValue, b: ModelValue) -> ModelValue: - """ - Determine what a ∧ b should be given the ordering table. - """ - for i in range(size + 1): - c = mvalue_from_index(i) - if not ordering[(c, a)]: - continue - if not ordering[(c, b)]: - continue - - invalid = False - for j in range(size + 1): - d = mvalue_from_index(j) - if c == d: - continue - if ordering[(c, d)]: - if ordering[(d, a)] and ordering [(d, b)]: - invalid = True - - if not invalid: - return c - -def determine_dresult(size: int, ordering: Dict[ModelValue, ModelValue], a: ModelValue, b: ModelValue) -> ModelValue: - """ - Determine what a ∨ b should be given the ordering table. - """ - for i in range(size + 1): - c = mvalue_from_index(i) - if not ordering[(a, c)]: - continue - if not ordering[(b, c)]: - continue - - invalid = False - - for j in range(size + 1): - d = mvalue_from_index(j) - if d == c: - continue - if ordering[(d, c)]: - if ordering[(a, d)] and ordering[(b, d)]: - invalid = True - - if not invalid: - return c - -def parse_single_order(infile: SourceFile, size: int, carrier_list: List[ModelValue]) -> Optional[Tuple[OrderTable, ModelFunction, ModelFunction]]: +def parse_single_order(infile: SourceFile, size: int, carrier_list: List[ModelValue]) -> Optional[ + Tuple[OrderTable, Optional[ModelFunction], Optional[ModelFunction]]]: """ Parse the line representing the ordering table """ @@ -509,21 +470,12 @@ def parse_single_order(infile: SourceFile, size: int, carrier_list: List[ModelVa for x, y in product(carrier_list, carrier_list): cresult = ordering.meet(x, y) if cresult is None: - print("[Warning] Conjunction and Disjunction are not well-defined") - print(f"{x} ∧ {y} = ??") - return None, None - else: - print(f"{x} ∧ {y} = {cresult}") + return ordering, None, None cmapping[(x, y)] = cresult dresult = ordering.join(x, y) - # dresult = determine_dresult(size, omapping, x, y) if dresult is None: - print("[Warning] Conjunction and Disjunction are not well-defined") - print(f"{x} ∨ {y} = ??") - return None, None - else: - print(f"{x} ∨ {y} = {dresult}") + return ordering, None, None dmapping[(x, y)] = dresult mconjunction = ModelFunction(2, cmapping, "∧") @@ -531,7 +483,7 @@ def parse_single_order(infile: SourceFile, size: int, carrier_list: List[ModelVa return ordering, mconjunction, mdisjunction -def parse_single_designated(infile: SourceFile, size: int) -> Optional[Set[ModelValue]]: +def parse_single_designated(infile: SourceFile, size: int, carrier_list: List[ModelValue]) -> Optional[Set[ModelValue]]: """ Parse the line representing which model values are designated. """ @@ -544,9 +496,8 @@ def parse_single_designated(infile: SourceFile, size: int) -> Optional[Set[Model designated_values = set() - for i, j in zip(range(size + 1), row): + for x, j in zip(carrier_list, row): if j == '1': - x = mvalue_from_index(i) designated_values.add(x) return designated_values @@ -579,7 +530,7 @@ def parse_single_monadic_connective(infile: SourceFile, symbol: str, size: int, return ModelFunction(1, mapping, symbol) -def parse_single_dyadic_connective(infile: SourceFile, symbol: str, size: int) -> Optional[ModelFunction]: +def parse_single_dyadic_connective(infile: SourceFile, symbol: str, size: int, carrier_list: List[ModelValue]) -> Optional[ModelFunction]: first_token = next(infile) if first_token == "-1": return None @@ -588,20 +539,14 @@ def parse_single_dyadic_connective(infile: SourceFile, symbol: str, size: int) - try: table = [first_token] + [next(infile) for _ in range((size + 1)**2 - 1)] except StopIteration: - pass - - assert len(table) == (size + 1)**2, f"{symbol} table does not match expected size at line {infile.line_in_file}" + raise Exception(f"{symbol} table does not match expected size at line {infile.line_in_file}") mapping = {} table_i = 0 - for i in range(size + 1): - x = mvalue_from_index(i) - for j in range(size + 1): - y = mvalue_from_index(j) - r = parse_mvalue(table[table_i]) - table_i += 1 - - mapping[(x, y)] = r + for x, y in product(carrier_list, carrier_list): + r = parse_mvalue(table[table_i]) + table_i += 1 + mapping[(x, y)] = r return ModelFunction(2, mapping, symbol) diff --git a/vsp.py b/vsp.py index 19b3d5d..1efd84c 100644 --- a/vsp.py +++ b/vsp.py @@ -2,6 +2,7 @@ Check to see if the model has the variable sharing property. """ +from collections import defaultdict from itertools import chain, combinations, product from typing import List, Optional, Set, Tuple from common import set_to_str @@ -9,75 +10,36 @@ from model import ( Model, model_closure, ModelFunction, ModelValue, OrderTable ) -def preseed( - initial_set: Set[ModelValue], - cache:List[Tuple[Set[ModelValue], Set[ModelValue]]]): - """ - Given a cache of previous model_closure calls, - use this to compute an initial model closure - set based on the initial set. +class Cache: + def __init__(self): + # input size -> cached (inputs, outputs) + self.c = defaultdict(list) - Basic Idea: - Let {1, 2, 3} -> X be in the cache. - If {1,2,3} is a subset of initial set, - then X is the subset of the output of model_closure. + def add(self, i: Set[ModelValue], o: Set[ModelValue]): + self.c[len(i)].append((i, o)) - This is used to speed up subsequent calls to model_closure - """ - candidate_preseed: Tuple[Set[ModelValue], int] = (None, None) + def get_closest(self, initial_set: Set[ModelValue]) -> Optional[Tuple[Set[ModelValue], bool]]: + """ + Iterate through our cache starting with the cached + inputs closest in size to the initial_set and + find the one that's a subset of initial_set. - for i, o in cache: - if i < initial_set: - cost = len(initial_set - i) - # If i is a subset with less missing elements than - # the previous candidate, then it's the new candidate. - if candidate_preseed[1] is None or cost < candidate_preseed[1]: - candidate_preseed = o, cost + Returns cached_output, and whether the initial_set is the same + as the cached_input. + """ + initial_set_size = len(initial_set) + sizes = range(initial_set_size, 0, -1) - same_set = candidate_preseed[1] == 0 - return candidate_preseed[0], same_set + for size in sizes: + if size not in self.c: + continue + for cached_input, cached_output in self.c[size]: + if cached_input <= initial_set: + return cached_output, size == initial_set_size -def find_top(algebra: Set[ModelValue], mconjunction: Optional[ModelFunction], mdisjunction: Optional[ModelFunction]) -> Optional[ModelValue]: - """ - Find the top of the order lattice. - T || a = T, T && a = a for all a in the carrier set - """ - if mconjunction is None or mdisjunction is None: return None - for x in algebra: - is_top = True - for y in algebra: - if mdisjunction(x, y) != x or mconjunction(x, y) != y: - is_top = False - break - if is_top: - return x - - print("[Warning] Failed to find the top of the lattice") - return None - -def find_bottom(algebra: Set[ModelValue], mconjunction: Optional[ModelFunction], mdisjunction: Optional[ModelFunction]) -> Optional[ModelValue]: - """ - Find the bottom of the order lattice - F || a = a, F && a = F for all a in the carrier set - """ - if mconjunction is None or mdisjunction is None: - return None - - for x in algebra: - is_bottom = True - for y in algebra: - if mdisjunction(x, y) != y or mconjunction(x, y) != x: - is_bottom = False - break - if is_bottom: - return x - - 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 @@ -106,17 +68,49 @@ Subalgebra 1: {set_to_str(self.subalgebra1)} Subalgebra 2: {set_to_str(self.subalgebra2)} """ +def quick_vsp_unsat_incomplete(xs, ys, model, top, bottom, negation_defined) -> bool: + """ + Return True if VSP cannot be satisfied + through some incomplete checks. + """ + # If the left subalgebra contains bottom + # or the right subalgebra contains top + # skip this pair + if top is not None and top in ys: + return True + if bottom is not None and bottom in xs: + return True + + # If a subalgebra doesn't have at least one + # designated value, move onto the next pair. + # Depends on no intersection between xs and ys + if xs.isdisjoint(model.designated_values): + return True + + if ys.isdisjoint(model.designated_values): + return True + + # If the two subalgebras intersect, move + # onto the next pair. + if not xs.isdisjoint(ys): + return True + + # If the subalgebras are order-dependent, skip this pair + if order_dependent(xs, ys, model.ordering): + return True + if negation_defined and order_dependent(ys, xs, model.ordering): + return True + + # We can't immediately rule out that these + # subalgebras don't exhibit VSP + return False + def has_vsp(model: Model, impfunction: ModelFunction, - mconjunction: Optional[ModelFunction] = None, - mdisjunction: Optional[ModelFunction] = None, - mnegation: Optional[ModelFunction] = None) -> VSP_Result: + negation_defined: bool) -> VSP_Result: """ Checks whether a model has the variable sharing property. """ - top = find_top(model.carrier_set, mconjunction, mdisjunction) - bottom = find_bottom(model.carrier_set, mconjunction, mdisjunction) - # NOTE: No models with only one designated # value satisfies VSP if len(model.designated_values) == 1: @@ -124,68 +118,44 @@ def has_vsp(model: Model, impfunction: ModelFunction, assert model.ordering is not None, "Expected ordering table in model" + top = model.ordering.top() + bottom = model.ordering.bottom() + # Compute I the set of tuples (x, y) where # x -> y does not take a designiated value - I: Set[Tuple[ModelValue, ModelValue]] = set() + I: List[Tuple[ModelValue, ModelValue]] = [] for (x, y) in product(model.carrier_set, model.carrier_set): if impfunction(x, y) not in model.designated_values: - I.add((x, y)) + I.append((x, y)) # Construct the powerset of I without the empty set - s = list(I) - I_power = chain.from_iterable(combinations(s, r) for r in range(1, len(s) + 1)) + I_power = chain.from_iterable(combinations(I, r) for r in range(1, len(I) + 1)) # ((x1, y1)), ((x1, y1), (x2, y2)), ... - # Closure cache - closure_cache: List[Tuple[Set[ModelValue], Set[ModelValue]]] = [] + closure_cache = Cache() # Find the subalgebras which falsify implication for xys in I_power: - xs = {xy[0] for xy in xys} + xs = { xy[0] for xy in xys } + ys = { xy[1] for xy in xys } + + if quick_vsp_unsat_incomplete(xs, ys, model, top, bottom, negation_defined): + continue + orig_xs = xs - cached_xs = preseed(xs, closure_cache) - if cached_xs[0] is not None: + cached_xs = closure_cache.get_closest(xs) + if cached_xs is not None: xs |= cached_xs[0] - ys = {xy[1] for xy in xys} orig_ys = ys - cached_ys = preseed(ys, closure_cache) - if cached_ys[0] is not None: + cached_ys = closure_cache.get_closest(ys) + if cached_ys is not None: ys |= cached_ys[0] - - # NOTE: Optimziation before model_closure - # If the two subalgebras intersect, move - # onto the next pair. - if len(xs & ys) > 0: - continue - - # NOTE: Optimization - # If a subalgebra doesn't have at least one - # designated value, move onto the next pair. - # Depends on no intersection between xs and ys - if len(xs & model.designated_values) == 0: - continue - - if len(ys & model.designated_values) == 0: - continue - - # NOTE: Optimization - # If the left subalgebra contains bottom - # or the right subalgebra contains top - # skip this pair - if top is not None and top in ys: - continue - 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 - if mnegation is not None and order_dependent(ys, xs, model.ordering): + xs_ys_updated = cached_xs is not None or cached_ys is not None + if xs_ys_updated and quick_vsp_unsat_incomplete(xs, ys, model, top, bottom, negation_defined): continue # Compute the closure of all operations @@ -193,8 +163,8 @@ def has_vsp(model: Model, impfunction: ModelFunction, carrier_set_left: Set[ModelValue] = model_closure(xs, model.logical_operations, bottom) # Save to cache - if cached_xs[0] is not None and not cached_ys[1]: - closure_cache.append((orig_xs, carrier_set_left)) + if cached_xs is None or (cached_xs is not None and not cached_xs[1]): + closure_cache.add(orig_xs, carrier_set_left) if bottom is not None and bottom in carrier_set_left: continue @@ -204,15 +174,15 @@ def has_vsp(model: Model, impfunction: ModelFunction, carrier_set_right: Set[ModelValue] = model_closure(ys, model.logical_operations, top) # Save to cache - if cached_ys[0] is not None and not cached_ys[1]: - closure_cache.append((orig_ys, carrier_set_right)) + if cached_ys is None or (cached_ys is not None and not cached_ys[1]): + closure_cache.add(orig_ys, carrier_set_right) if top is not None and top in carrier_set_right: continue # If the carrier set intersects, then move on to the next # subalgebra - if len(carrier_set_left & carrier_set_right) > 0: + if not carrier_set_left.isdisjoint(carrier_set_right): continue # See if for all pairs in the subalgebras, that diff --git a/vspursuer.py b/vspursuer.py index 284c0ef..02047e3 100755 --- a/vspursuer.py +++ b/vspursuer.py @@ -1,17 +1,20 @@ #!/usr/bin/env python3 -# NOTE: Perhaps we should use process_cpu_count but that's not available to all Python versions -from os import cpu_count +from datetime import datetime from typing import Dict, Iterator, Optional, Tuple from queue import Empty as QueueEmpty import argparse import multiprocessing as mp -from logic import Conjunction, Disjunction, Negation, Implication, Operation +from logic import Negation, Implication, Operation from model import Model, ModelFunction from parse_magic import SourceFile, parse_matrices from vsp import has_vsp, VSP_Result +def print_with_timestamp(message): + current_time = datetime.now().strftime("%Y-%m-%d %H:%M:%S") + print(f"[{current_time}] {message}") + def restructure_solutions(solutions: Iterator[Tuple[Model, Dict[Operation, ModelFunction]]], skip_to: Optional[str]) -> \ Iterator[Tuple[Model, ModelFunction, Optional[ModelFunction], Optional[ModelFunction], Optional[ModelFunction]]]: """ @@ -32,17 +35,15 @@ def restructure_solutions(solutions: Iterator[Tuple[Model, Dict[Operation, Model # NOTE: Implication must be defined, the rest may not impfunction = interpretation[Implication] - mconjunction = interpretation.get(Conjunction) - mdisjunction = interpretation.get(Disjunction) - mnegation = interpretation.get(Negation) - yield (model, impfunction, mconjunction, mdisjunction, mnegation) + negation_defined = Negation in interpretation + yield (model, impfunction, negation_defined) -def has_vsp_plus_model(model, impfunction, mconjunction, mdisjunction, mnegation) -> Tuple[Optional[Model], VSP_Result]: +def has_vsp_plus_model(model, impfunction, negation_defined) -> Tuple[Optional[Model], VSP_Result]: """ Wrapper which also stores the models along with its vsp result """ - vsp_result = has_vsp(model, impfunction, mconjunction, mdisjunction, mnegation) - # NOTE: Memory optimization - Don't return model if it doens't have VSP + vsp_result = has_vsp(model, impfunction, negation_defined) + # NOTE: Memory optimization - Don't return model if it doesn't have VSP model = model if vsp_result.has_vsp else None return (model, vsp_result) @@ -60,8 +61,8 @@ def worker_vsp(task_queue: mp.Queue, result_queue: mp.Queue): # If sentinal value, break if task is None: break - (model, impfunction, mconjunction, mdisjunction, mnegation) = task - result = has_vsp_plus_model(model, impfunction, mconjunction, mdisjunction, mnegation) + (model, impfunction, negation_defined) = task + result = has_vsp_plus_model(model, impfunction, negation_defined) result_queue.put(result) finally: # Either an exception occured or the worker finished @@ -91,37 +92,22 @@ def worker_parser(data_file_path: str, num_sentinal_values: int, task_queue: mp. for _ in range(num_sentinal_values): task_queue.put(None) +def multi_process_runner(num_cpu: int, data_file_path: str, skip_to: Optional[str]): + """ + Run VSPursuer in a multi-process configuration. + """ + assert num_cpu > 1 - - -if __name__ == "__main__": - parser = argparse.ArgumentParser(description="VSP Checker") - parser.add_argument("--verbose", action='store_true', help="Print out all parsed matrices") - parser.add_argument("-i", type=str, help="Path to MaGIC ugly data file") - parser.add_argument("-c", type=int, help="Number of CPUs to use. Default: MAX - 2.") - parser.add_argument("--skip-to", type=str, help="Skip until a model name is found and process from then onwards.") - args = vars(parser.parse_args()) - - data_file_path = args.get("i") - if data_file_path is None: - data_file_path = input("Path to MaGIC Ugly Data File: ") - - - num_cpu = args.get("c") - if num_cpu is None: - num_cpu = max(cpu_count() - 2, 1) - - # Set up parallel verification num_tested = 0 num_has_vsp = 0 - num_workers = max(num_cpu - 1, 1) + num_workers = num_cpu - 1 # Create queues task_queue = mp.Queue(maxsize=1000) result_queue = mp.Queue() # Create dedicated process to parse the MaGIC file - process_parser = mp.Process(target=worker_parser, args=(data_file_path, num_workers, task_queue, args.get("skip_to"))) + process_parser = mp.Process(target=worker_parser, args=(data_file_path, num_workers, task_queue, skip_to)) process_parser.start() # Create dedicated processes which check VSP @@ -135,7 +121,6 @@ if __name__ == "__main__": # Check results and add new tasks until finished result_sentinal_count = 0 while True: - # Read a result try: result = result_queue.get(True, 60) @@ -171,7 +156,7 @@ if __name__ == "__main__": # Process result model, vsp_result = result - print(vsp_result) + print_with_timestamp(vsp_result) num_tested += 1 if vsp_result.has_vsp: @@ -180,7 +165,47 @@ if __name__ == "__main__": if vsp_result.has_vsp: num_has_vsp += 1 + print_with_timestamp(f"Tested {num_tested} models, {num_has_vsp} of which satisfy VSP") - print(f"Tested {num_tested} models, {num_has_vsp} of which satisfy VSP") +def single_process_runner(data_file_path: str, skip_to: Optional[str]): + num_tested = 0 + num_has_vsp = 0 + + data_file = open(data_file_path, "r") + solutions = parse_matrices(SourceFile(data_file)) + solutions = restructure_solutions(solutions, skip_to) + + for model, impfunction, negation_defined in solutions: + model, vsp_result = has_vsp_plus_model(model, impfunction, negation_defined) + print_with_timestamp(vsp_result) + num_tested += 1 + + if vsp_result.has_vsp: + print(model) + + if vsp_result.has_vsp: + num_has_vsp += 1 + + print_with_timestamp(f"Tested {num_tested} models, {num_has_vsp} of which satisfy VSP") +if __name__ == "__main__": + parser = argparse.ArgumentParser(description="VSP Checker") + parser.add_argument("--verbose", action='store_true', help="Print out all parsed matrices") + parser.add_argument("-i", type=str, help="Path to MaGIC ugly data file") + parser.add_argument("-c", type=int, help="Number of CPUs to use. Default: 1") + parser.add_argument("--skip-to", type=str, help="Skip until a model name is found and process from then onwards.") + args = vars(parser.parse_args()) + + data_file_path = args.get("i") + if data_file_path is None: + data_file_path = input("Path to MaGIC Ugly Data File: ") + + num_cpu = args.get("c") + if num_cpu is None: + num_cpu = 1 + + if num_cpu == 1: + single_process_runner(data_file_path, args.get("skip_to")) + else: + multi_process_runner(num_cpu, data_file_path, args.get("skip_to")) From cd084812cc7097039d0404755df589345c23264a Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Sun, 4 May 2025 20:29:02 -0400 Subject: [PATCH 21/29] Removed a useless optimization and added one when negation is defined --- vsp.py | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/vsp.py b/vsp.py index 1efd84c..e5a715b 100644 --- a/vsp.py +++ b/vsp.py @@ -78,16 +78,11 @@ def quick_vsp_unsat_incomplete(xs, ys, model, top, bottom, negation_defined) -> # skip this pair if top is not None and top in ys: return True + if negation_defined and bottom is not None and bottom in ys: + return True if bottom is not None and bottom in xs: return True - - # If a subalgebra doesn't have at least one - # designated value, move onto the next pair. - # Depends on no intersection between xs and ys - if xs.isdisjoint(model.designated_values): - return True - - if ys.isdisjoint(model.designated_values): + if negation_defined and top is not None and top in xs: return True # If the two subalgebras intersect, move From 66393442803dd7c5e0f6d4936c621654018e248d Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Sun, 4 May 2025 21:07:20 -0400 Subject: [PATCH 22/29] Stopped bug triggered during timeout --- vspursuer.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/vspursuer.py b/vspursuer.py index 02047e3..4c788f2 100755 --- a/vspursuer.py +++ b/vspursuer.py @@ -145,6 +145,9 @@ def multi_process_runner(num_cpu: int, data_file_path: str, skip_to: Optional[st for _ in range(num_workers): task_queue.put(None) + # Don't do anymore work, wait again for a result + continue + # When we receive None, it means a child process has finished if result is None: From 4cccdc85b971a736bc2dd79603521ed2834f6dcd Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Tue, 13 May 2025 12:53:46 -0400 Subject: [PATCH 23/29] Flush print --- vspursuer.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/vspursuer.py b/vspursuer.py index 4c788f2..d9d9e53 100755 --- a/vspursuer.py +++ b/vspursuer.py @@ -13,7 +13,7 @@ from vsp import has_vsp, VSP_Result def print_with_timestamp(message): current_time = datetime.now().strftime("%Y-%m-%d %H:%M:%S") - print(f"[{current_time}] {message}") + print(f"[{current_time}] {message}", flush=True) def restructure_solutions(solutions: Iterator[Tuple[Model, Dict[Operation, ModelFunction]]], skip_to: Optional[str]) -> \ Iterator[Tuple[Model, ModelFunction, Optional[ModelFunction], Optional[ModelFunction], Optional[ModelFunction]]]: From ec451e007cd08f63a3ced1ced529c9699d34a6c9 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Tue, 13 May 2025 12:55:24 -0400 Subject: [PATCH 24/29] Removed comment --- model.py | 3 --- 1 file changed, 3 deletions(-) diff --git a/model.py b/model.py index b9b3af1..6a6df38 100644 --- a/model.py +++ b/model.py @@ -103,9 +103,6 @@ def binary_function_str(f: ModelFunction) -> str: Interpretation = Dict[Operation, ModelFunction] -# TODO: Replace with a nicer representation -# Include meet and join functions -# Something like x : (all elements less than x) class OrderTable: def __init__(self): # a : {x | x <= a } From 7b652f36eb753830b857e3d94da258e3b75f7860 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Tue, 13 May 2025 13:22:28 -0400 Subject: [PATCH 25/29] Transformed subalgebra generation from exponential to linear --- vsp.py | 153 ++++++++++++++++----------------------------------------- 1 file changed, 41 insertions(+), 112 deletions(-) diff --git a/vsp.py b/vsp.py index e5a715b..1a861f7 100644 --- a/vsp.py +++ b/vsp.py @@ -2,54 +2,13 @@ Check to see if the model has the variable sharing property. """ -from collections import defaultdict -from itertools import chain, combinations, product +from itertools import product from typing import List, Optional, Set, Tuple from common import set_to_str from model import ( - Model, model_closure, ModelFunction, ModelValue, OrderTable + Model, model_closure, ModelFunction, ModelValue ) -class Cache: - def __init__(self): - # input size -> cached (inputs, outputs) - self.c = defaultdict(list) - - def add(self, i: Set[ModelValue], o: Set[ModelValue]): - self.c[len(i)].append((i, o)) - - def get_closest(self, initial_set: Set[ModelValue]) -> Optional[Tuple[Set[ModelValue], bool]]: - """ - Iterate through our cache starting with the cached - inputs closest in size to the initial_set and - find the one that's a subset of initial_set. - - Returns cached_output, and whether the initial_set is the same - as the cached_input. - """ - initial_set_size = len(initial_set) - sizes = range(initial_set_size, 0, -1) - - for size in sizes: - if size not in self.c: - continue - - for cached_input, cached_output in self.c[size]: - if cached_input <= initial_set: - return cached_output, size == initial_set_size - - 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__( self, has_vsp: bool, model_name: Optional[str] = None, @@ -68,38 +27,6 @@ Subalgebra 1: {set_to_str(self.subalgebra1)} Subalgebra 2: {set_to_str(self.subalgebra2)} """ -def quick_vsp_unsat_incomplete(xs, ys, model, top, bottom, negation_defined) -> bool: - """ - Return True if VSP cannot be satisfied - through some incomplete checks. - """ - # If the left subalgebra contains bottom - # or the right subalgebra contains top - # skip this pair - if top is not None and top in ys: - return True - if negation_defined and bottom is not None and bottom in ys: - return True - if bottom is not None and bottom in xs: - return True - if negation_defined and top is not None and top in xs: - return True - - # If the two subalgebras intersect, move - # onto the next pair. - if not xs.isdisjoint(ys): - return True - - # If the subalgebras are order-dependent, skip this pair - if order_dependent(xs, ys, model.ordering): - return True - if negation_defined and order_dependent(ys, xs, model.ordering): - return True - - # We can't immediately rule out that these - # subalgebras don't exhibit VSP - return False - def has_vsp(model: Model, impfunction: ModelFunction, negation_defined: bool) -> VSP_Result: """ @@ -124,64 +51,66 @@ def has_vsp(model: Model, impfunction: ModelFunction, if impfunction(x, y) not in model.designated_values: I.append((x, y)) - # Construct the powerset of I without the empty set - I_power = chain.from_iterable(combinations(I, r) for r in range(1, len(I) + 1)) - # ((x1, y1)), ((x1, y1), (x2, y2)), ... - - closure_cache = Cache() - # Find the subalgebras which falsify implication - for xys in I_power: + for xys in I: - xs = { xy[0] for xy in xys } - ys = { xy[1] for xy in xys } + xi = xys[0] - if quick_vsp_unsat_incomplete(xs, ys, model, top, bottom, negation_defined): + # Discard ({⊥} ∪ A', B) subalgebras + if bottom is not None and xi == bottom: continue - orig_xs = xs - cached_xs = closure_cache.get_closest(xs) - if cached_xs is not None: - xs |= cached_xs[0] - - orig_ys = ys - cached_ys = closure_cache.get_closest(ys) - if cached_ys is not None: - ys |= cached_ys[0] - - xs_ys_updated = cached_xs is not None or cached_ys is not None - if xs_ys_updated and quick_vsp_unsat_incomplete(xs, ys, model, top, bottom, negation_defined): + # Discard ({⊤} ∪ A', B) subalgebras when negation is defined + if top is not None and negation_defined and xi == top: continue - # Compute the closure of all operations - # with just the xs - carrier_set_left: Set[ModelValue] = model_closure(xs, model.logical_operations, bottom) + yi = xys[1] - # Save to cache - if cached_xs is None or (cached_xs is not None and not cached_xs[1]): - closure_cache.add(orig_xs, carrier_set_left) + # Discard (A, {⊤} ∪ B') subalgebras + if top is not None and yi == top: + continue + # Discard (A, {⊥} ∪ B') subalgebras when negation is defined + if bottom is not None and negation_defined and yi == bottom: + continue + + # Discard ({a} ∪ A', {b} ∪ B') subalgebras when a <= b + if model.ordering.is_lt(xi, yi): + continue + + # Discard ({a} ∪ A', {b} ∪ B') subalgebras when b <= a and negation is defined + if negation_defined and model.ordering.is_lt(yi, xi): + continue + + # Compute the left closure of the set containing xi under all the operations + carrier_set_left: Set[ModelValue] = model_closure({xi,}, model.logical_operations, bottom) + + # Discard ({⊥} ∪ A', B) subalgebras if bottom is not None and bottom in carrier_set_left: continue + # Discard ({⊤} ∪ A', B) subalgebras when negation is defined + if top is not None and negation_defined and top in carrier_set_left: + continue + # Compute the closure of all operations # with just the ys - carrier_set_right: Set[ModelValue] = model_closure(ys, model.logical_operations, top) - - # Save to cache - if cached_ys is None or (cached_ys is not None and not cached_ys[1]): - closure_cache.add(orig_ys, carrier_set_right) + carrier_set_right: Set[ModelValue] = model_closure({yi,}, model.logical_operations, top) + # Discard (A, {⊤} ∪ B') subalgebras if top is not None and top in carrier_set_right: continue - # If the carrier set intersects, then move on to the next - # subalgebra + # Discard (A, {⊥} ∪ B') subalgebras when negation is defined + if bottom is not None and negation_defined and bottom in carrier_set_right: + continue + + # Discard subalgebras that intersect if not carrier_set_left.isdisjoint(carrier_set_right): continue - # See if for all pairs in the subalgebras, that - # implication is falsified + # Check whether for all pairs in the subalgebra, + # that implication is falsified. falsified = True for (x2, y2) in product(carrier_set_left, carrier_set_right): if impfunction(x2, y2) in model.designated_values: From 94a01dd3da253b928fa2a213f8caeb5932753696 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Mon, 26 May 2025 17:35:05 -0400 Subject: [PATCH 26/29] Fixed misusage of Model constructor --- R.py | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/R.py b/R.py index 426941a..4ce4b04 100644 --- a/R.py +++ b/R.py @@ -12,7 +12,7 @@ from logic import ( ) from model import Model, ModelFunction, ModelValue, satisfiable from generate_model import generate_model -from vsp import has_vsp +# from vsp import has_vsp # =================================================== @@ -106,7 +106,7 @@ designated_values = {a1} logical_operations = { mnegation, mimplication, mconjunction, mdisjunction } -R_model_2 = Model(carrier_set, logical_operations, designated_values, "R2") +R_model_2 = Model(carrier_set, logical_operations, designated_values, None, "R2") interpretation = { Negation: mnegation, @@ -132,8 +132,8 @@ solutions = generate_model(R_logic, model_size, print_model=False) print(f"Found {len(solutions)} satisfiable models") -for model, interpretation in solutions: - print(has_vsp(model, interpretation)) +# for model, interpretation in solutions: +# print(has_vsp(model, interpretation)) print("*" * 30) @@ -301,7 +301,7 @@ mdisjunction = ModelFunction(2, { logical_operations = { mnegation, mimplication, mconjunction, mdisjunction } -R_model_6 = Model(carrier_set, logical_operations, designated_values, "R6") +R_model_6 = Model(carrier_set, logical_operations, designated_values, None, "R6") interpretation = { Negation: mnegation, @@ -312,4 +312,4 @@ interpretation = { print(R_model_6) print(f"Model {R_model_6.name} satisfies logic {R_logic.name}?", satisfiable(R_logic, R_model_6, interpretation)) -print(has_vsp(R_model_6, interpretation)) +# print(has_vsp(R_model_6, interpretation)) From b16376e35c15df61f717c1a79d4c6524aec3aeaf Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Mon, 26 May 2025 17:36:03 -0400 Subject: [PATCH 27/29] Added model equivalence check --- model.py | 40 +++++++++++++++++++++++++++++++++++++++- 1 file changed, 39 insertions(+), 1 deletion(-) diff --git a/model.py b/model.py index 6a6df38..ffebfb1 100644 --- a/model.py +++ b/model.py @@ -9,7 +9,10 @@ from logic import ( ) from collections import defaultdict from functools import cached_property, lru_cache, reduce -from itertools import chain, combinations_with_replacement, permutations, product +from itertools import ( + chain, combinations_with_replacement, + permutations, product +) from typing import Dict, List, Optional, Set, Tuple @@ -355,3 +358,38 @@ def model_closure(initial_set: Set[ModelValue], mfunctions: Set[ModelFunction], break return closure_set + + +def model_equivalence(model1: Model, model2: Model) -> bool: + """ + Takes two models and determines if they are equivalent. + Assumes for the model to be equilvalent that their + value names are equivalent as well. + """ + + if model1.carrier_set != model2.carrier_set: + return False + + if model1.designated_values != model2.designated_values: + return False + + model1_fn_names = set((fn.operation_name for fn in model1.logical_operations)) + model2_fn_names = set((fn.operation_name for fn in model2.logical_operations)) + + if model1_fn_names != model2_fn_names: + return False + + for fn_name in model1_fn_names: + fn1 = next((fn for fn in model1.logical_operations if fn.operation_name == fn_name)) + fn2 = next((fn for fn in model2.logical_operations if fn.operation_name == fn_name)) + + if fn1.arity != fn2.arity: + return False + + # Check for functional equilvance + # That is for all inputs in the carrier set, the outputs are the same + for args in product(model1.carrier_set, repeat=fn1.arity): + if fn1(*args) != fn2(*args): + return False + + return True From 7305b358a9a57a2494eeb72990e339e2f807c674 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Mon, 26 May 2025 17:38:48 -0400 Subject: [PATCH 28/29] Added utility scripts --- utils/README.md | 1 + utils/compare_vsp_results.py | 102 +++++++++++++++++++++++++++++++++++ utils/hasse.py | 54 +++++++++++++++++++ utils/print_model.py | 30 +++++++++++ 4 files changed, 187 insertions(+) create mode 100644 utils/README.md create mode 100644 utils/compare_vsp_results.py create mode 100644 utils/hasse.py create mode 100644 utils/print_model.py diff --git a/utils/README.md b/utils/README.md new file mode 100644 index 0000000..6c0f260 --- /dev/null +++ b/utils/README.md @@ -0,0 +1 @@ +This folder contains scripts that may be used during experimentation. These are intended to be used ad-hoc and we do not guarentee the maitainance of these scripts. \ No newline at end of file diff --git a/utils/compare_vsp_results.py b/utils/compare_vsp_results.py new file mode 100644 index 0000000..daee3c5 --- /dev/null +++ b/utils/compare_vsp_results.py @@ -0,0 +1,102 @@ +""" +Given two MaGIC ugly data files that correspond to +the same logic. Report any differences in the models +that exhibit VSP. + +Overall process: +- Determine which models in file 1 have VSP +- Print if model does not exist in file 2 +- For models in file 2 that were not already encountered for, + check if they have VSP. +- Print models that do +""" +import argparse +import os +import sys +sys.path.append(os.path.dirname(os.path.dirname(os.path.abspath(__file__)))) + +import argparse + +from model import model_equivalence +from parse_magic import SourceFile, parse_matrices +from vsp import has_vsp +from vspursuer import restructure_solutions + +if __name__ == "__main__": + parser = argparse.ArgumentParser(description="Compare models that have VSP in two ugly files") + parser.add_argument("ugly1", type=str, help="First ugly data file") + parser.add_argument("ugly2", type=str, help="Second ugly data file") + args = vars(parser.parse_args()) + + data_file1 = open(args['ugly1'], "r") + solutions1 = parse_matrices(SourceFile(data_file1)) + solutions1 = restructure_solutions(solutions1, None) + + data_file2 = open(args['ugly2'], "r") + solutions2 = parse_matrices(SourceFile(data_file2)) + solutions2 = list(restructure_solutions(solutions2, None)) + + # Total count of models + total_models1 = 0 + total_models2 = 0 + + # Models that exhibit VSP + good_models1 = 0 + good_models2 = 0 + + # Models that don't exhibit VSP + bad_models1 = 0 + bad_models2 = 0 + + # Models that exhibit VSP but does + # not exist in the other file. + extra_models1 = 0 + extra_models2 = 0 + + for model, impfunction, negation_defined in solutions1: + total_models1 += 1 + vsp_result = has_vsp(model, impfunction, negation_defined) + + if vsp_result.has_vsp: + good_models1 += 1 + # Check to see if model exists in file 2 + match_found_index = (False, -1) + for i in range(len(solutions2) - 1, -1, -1): + if model_equivalence(model, solutions2[i][0]): + match_found_index = (True, i) + break + + if match_found_index[0]: + # If so, remove the model from the second set + total_models2 += 1 + good_models2 += 1 + del solutions2[match_found_index[1]] + else: + extra_models1 += 1 + print(f"VSP Model {model.name} not found in file 2.") + print(model) + else: + bad_models1 += 1 + + + # Check through the remaining models in the second set + for model, impfunction, negation_defined in solutions2: + total_models2 += 1 + vsp_result = has_vsp(model, impfunction, negation_defined) + + if not vsp_result.has_vsp: + bad_models2 += 1 + else: + print("VSP model", model.name, "does not appear in file 1") + good_models2 += 1 + extra_models2 += 1 + + + print("File 1 has a total of", total_models1, "models.") + print("Out of which,", good_models1, "exhibit VSP while", bad_models1, "do not.") + print("File 1 has a total of", extra_models1, "which exhibit VSP but do not appear in file 2.") + + print("") + print("File 2 has a total of", total_models2, "models") + print("Out of which,", good_models2, "exhibit VSP while", bad_models2, "do not.") + print("File 2 has a total of", extra_models2, "which exhibit VSP but do not appear in file 1.") diff --git a/utils/hasse.py b/utils/hasse.py new file mode 100644 index 0000000..97074bc --- /dev/null +++ b/utils/hasse.py @@ -0,0 +1,54 @@ +""" +Given a model, create a Hasse diagram. + +Note: This has a dependency on the hasse-diagram library +https://pypi.org/project/hasse-diagram/ +""" +import argparse +import os +import sys +sys.path.append(os.path.dirname(os.path.dirname(os.path.abspath(__file__)))) + +from model import Model +from parse_magic import SourceFile, parse_matrices + +import numpy as np +import hassediagram + +__all__ = ['plot_model_hassee'] + +def plot_model_hassee(model: Model): + assert model.ordering is not None + carrier_list = list(model.carrier_set) + hasse_ordering = [] + for elem1 in carrier_list: + elem_ordering = [] + for elem2 in carrier_list: + elem_ordering.append( + 1 if model.ordering.is_lt(elem1, elem2) else 0 + ) + hasse_ordering.append(elem_ordering) + hassediagram.plot_hasse(np.array(hasse_ordering), carrier_list) + + +if __name__ == "__main__": + parser = argparse.ArgumentParser(description="Show hassee diagram for model") + parser.add_argument("uglyfile", type=str, help="Path to ugly data file") + parser.add_argument("modelname", type=str, help="Name of model within file") + args = vars(parser.parse_args()) + + data_file = open(args['uglyfile'], "r") + solutions = parse_matrices(SourceFile(data_file)) + + requested_model = None + + for model, _ in solutions: + if model.name == args['modelname']: + requested_model = model + break + + if requested_model is None: + print("Model name", args['modelname'], "not found.") + sys.exit(0) + + plot_model_hassee(requested_model) diff --git a/utils/print_model.py b/utils/print_model.py new file mode 100644 index 0000000..027c0e3 --- /dev/null +++ b/utils/print_model.py @@ -0,0 +1,30 @@ +""" +Print a model given it's name +and ugly data file +""" +import argparse +import os +import sys +sys.path.append(os.path.dirname(os.path.dirname(os.path.abspath(__file__)))) + +from parse_magic import SourceFile, parse_matrices + +if __name__ == "__main__": + parser = argparse.ArgumentParser(description="Show hassee diagram for model") + parser.add_argument("uglyfile", type=str, help="Path to ugly data file") + parser.add_argument("modelname", type=str, help="Name of model within file") + args = vars(parser.parse_args()) + + data_file = open(args['uglyfile'], "r") + solutions = parse_matrices(SourceFile(data_file)) + + model_found = False + + for model, _ in solutions: + if model.name == args['modelname']: + model_found = True + print(model) + break + + if not model_found: + print("Model", args['modelname'], "not found.") From 6d7fc9094af0a136172fc52bc325580620385410 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Tue, 17 Jun 2025 22:05:45 -0400 Subject: [PATCH 29/29] Add flag to ignore constants during model equivalence --- model.py | 15 ++++++++++++--- utils/compare_vsp_results.py | 5 ++++- 2 files changed, 16 insertions(+), 4 deletions(-) diff --git a/model.py b/model.py index ffebfb1..429a26e 100644 --- a/model.py +++ b/model.py @@ -360,7 +360,7 @@ def model_closure(initial_set: Set[ModelValue], mfunctions: Set[ModelFunction], return closure_set -def model_equivalence(model1: Model, model2: Model) -> bool: +def model_equivalence(model1: Model, model2: Model, ignore_constants: bool = False) -> bool: """ Takes two models and determines if they are equivalent. Assumes for the model to be equilvalent that their @@ -373,8 +373,17 @@ def model_equivalence(model1: Model, model2: Model) -> bool: if model1.designated_values != model2.designated_values: return False - model1_fn_names = set((fn.operation_name for fn in model1.logical_operations)) - model2_fn_names = set((fn.operation_name for fn in model2.logical_operations)) + model1_fn_names = set() + for fn in model1.logical_operations: + if fn.arity == 0 and ignore_constants: + continue + model1_fn_names.add(fn.operation_name) + + model2_fn_names = set() + for fn in model2.logical_operations: + if fn.arity == 0 and ignore_constants: + continue + model2_fn_names.add(fn.operation_name) if model1_fn_names != model2_fn_names: return False diff --git a/utils/compare_vsp_results.py b/utils/compare_vsp_results.py index daee3c5..82c587d 100644 --- a/utils/compare_vsp_results.py +++ b/utils/compare_vsp_results.py @@ -26,6 +26,7 @@ if __name__ == "__main__": parser = argparse.ArgumentParser(description="Compare models that have VSP in two ugly files") parser.add_argument("ugly1", type=str, help="First ugly data file") parser.add_argument("ugly2", type=str, help="Second ugly data file") + parser.add_argument("--ignore-constants", action='store_true', help="When it comes to model equivalance, ignore constants") args = vars(parser.parse_args()) data_file1 = open(args['ugly1'], "r") @@ -36,6 +37,8 @@ if __name__ == "__main__": solutions2 = parse_matrices(SourceFile(data_file2)) solutions2 = list(restructure_solutions(solutions2, None)) + ignore_constants = args.get("ignore_constants", False) + # Total count of models total_models1 = 0 total_models2 = 0 @@ -62,7 +65,7 @@ if __name__ == "__main__": # Check to see if model exists in file 2 match_found_index = (False, -1) for i in range(len(solutions2) - 1, -1, -1): - if model_equivalence(model, solutions2[i][0]): + if model_equivalence(model, solutions2[i][0], ignore_constants): match_found_index = (True, i) break