From c0ef204e4823ec57fef4e36b6400abd83e417471 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Thu, 3 Oct 2024 21:06:23 -0400 Subject: [PATCH 01/12] Only print matrices when model shows VSP --- parse_magic.py | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/parse_magic.py b/parse_magic.py index 9ef9aaa..cdf3484 100644 --- a/parse_magic.py +++ b/parse_magic.py @@ -3,6 +3,7 @@ Parses the Magic Ugly Data File Format Assumes the base logic is R with no extra connectives """ +import argparse import sys from typing import TextIO, List, Optional, Tuple, Set, Dict @@ -297,8 +298,12 @@ def parse_implication(infile: TextIO, size: int) -> Optional[List[ModelFunction] if __name__ == "__main__": + parser = argparse.ArgumentParser(description="VSP Checker") + parser.add_argument("--verbose", action='store_true', help="Print out all parsed matrices") + args = vars(parser.parse_args()) solutions: List[Model] = parse_matrices(SourceFile(sys.stdin)) print(f"Parsed {len(solutions)} matrices") for i, (model, interpretation) in enumerate(solutions): - print(model) + if args['verbose']: + print(model) print(has_vsp(model, interpretation)) From 68788ecff600f6a3b246e2a1d3caea4a7fc4431e Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Thu, 3 Oct 2024 21:47:12 -0400 Subject: [PATCH 02/12] Print model when it shows VSP --- parse_magic.py | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/parse_magic.py b/parse_magic.py index cdf3484..deda575 100644 --- a/parse_magic.py +++ b/parse_magic.py @@ -304,6 +304,7 @@ if __name__ == "__main__": solutions: List[Model] = parse_matrices(SourceFile(sys.stdin)) print(f"Parsed {len(solutions)} matrices") for i, (model, interpretation) in enumerate(solutions): - if args['verbose']: + vsp_result = has_vsp(model, interpretation) + print(vsp_result) + if args['verbose'] or vsp_result.has_vsp: print(model) - print(has_vsp(model, interpretation)) From 83091c31ab4fb2fc82d4854ff4300f0b79e0fad5 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Thu, 3 Oct 2024 21:48:25 -0400 Subject: [PATCH 03/12] Example Ugly Data Format with models of R up to size 6 --- examples/R6 | 78 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 78 insertions(+) create mode 100644 examples/R6 diff --git a/examples/R6 b/examples/R6 new file mode 100644 index 0000000..9de08e8 --- /dev/null +++ b/examples/R6 @@ -0,0 +1,78 @@ + 1 1 1 1 1 1 0 0 + 1 + 1 0 + 1 1 0 1 + 0 1 + 1 1 0 1 -1 + -1 + -1 + -1 + 2 + 2 1 0 + 1 1 1 0 1 1 0 0 1 + 0 1 1 + 2 2 2 0 1 2 0 0 2 -1 + -1 + -1 + -1 + 3 + 3 2 1 0 + 1 1 1 1 0 1 0 1 0 0 1 1 0 0 0 1 + 0 1 0 1 + 3 3 3 3 0 1 2 3 0 0 1 3 0 0 0 3 -1 + 0 0 0 1 + 3 3 3 3 2 3 2 3 1 1 3 3 0 1 2 3 -1 + -1 + 1 1 1 1 0 1 1 1 0 0 1 1 0 0 0 1 + 0 1 1 1 + 3 3 3 3 0 1 2 3 0 0 1 3 0 0 0 3 -1 + 0 0 1 1 + 3 3 3 3 0 2 2 3 0 1 2 3 0 0 0 3 -1 + -1 + -1 + -1 + 4 + 4 3 2 1 0 + 1 1 1 1 1 0 1 1 1 1 0 0 1 1 1 0 0 0 1 1 0 0 0 0 1 + 0 1 1 1 1 + 4 4 4 4 4 0 1 2 3 4 0 0 1 2 4 0 0 0 1 4 0 0 0 0 4 4 4 4 4 4 0 1 2 3 4 0 0 2 2 4 0 0 0 1 4 0 0 0 0 4 -1 + 0 0 1 1 1 + 4 4 4 4 4 0 3 3 3 4 0 1 2 3 4 0 1 1 3 4 0 0 0 0 4 -1 + -1 + -1 + -1 + 5 + 5 4 3 2 1 0 + 1 1 1 1 1 1 0 1 0 1 0 1 0 0 1 1 1 1 0 0 0 1 0 1 0 0 0 0 1 1 0 0 0 0 0 1 + 0 1 0 1 0 1 + 5 5 5 5 5 5 0 1 2 3 4 5 0 0 1 1 3 5 0 0 0 1 2 5 0 0 0 0 1 5 0 0 0 0 0 5 5 5 5 5 5 5 0 1 2 3 4 5 0 0 3 3 3 5 0 0 2 3 2 5 0 0 0 0 1 5 0 0 0 0 0 5 -1 + 0 0 1 1 1 1 + 5 5 5 5 5 5 0 2 0 4 0 5 0 1 2 3 4 5 0 0 0 2 0 5 0 0 0 1 2 5 0 0 0 0 0 5 5 5 5 5 5 5 0 4 0 4 0 5 0 1 2 3 4 5 0 0 0 2 0 5 0 1 0 1 4 5 0 0 0 0 0 5 -1 + 0 0 0 1 0 1 + 5 5 5 5 5 5 4 5 4 5 4 5 1 1 3 3 5 5 0 1 2 3 4 5 1 1 1 1 5 5 0 1 0 1 4 5 -1 + -1 + 1 1 1 1 1 1 0 1 1 1 1 1 0 0 1 0 1 1 0 0 0 1 1 1 0 0 0 0 1 1 0 0 0 0 0 1 + 0 1 1 1 1 1 + 5 5 5 5 5 5 0 1 2 3 4 5 0 0 1 0 3 5 0 0 0 1 2 5 0 0 0 0 1 5 0 0 0 0 0 5 -1 + 0 0 1 0 1 1 + 5 5 5 5 5 5 0 2 2 4 4 5 0 1 2 3 4 5 0 0 0 2 2 5 0 0 0 1 2 5 0 0 0 0 0 5 5 5 5 5 5 5 0 4 4 4 4 5 0 1 2 3 4 5 0 1 1 2 4 5 0 1 1 1 4 5 0 0 0 0 0 5 -1 + 0 0 0 0 1 1 + 5 5 5 5 5 5 0 4 4 4 4 5 0 3 4 3 4 5 0 2 2 4 4 5 0 1 2 3 4 5 0 0 0 0 0 5 -1 + -1 + 1 1 1 1 1 1 0 1 1 1 1 1 0 0 1 1 1 1 0 0 0 1 1 1 0 0 0 0 1 1 0 0 0 0 0 1 + 0 1 1 1 1 1 + 5 5 5 5 5 5 0 1 2 3 4 5 0 0 1 1 3 5 0 0 0 1 2 5 0 0 0 0 1 5 0 0 0 0 0 5 5 5 5 5 5 5 0 1 2 3 4 5 0 0 1 2 3 5 0 0 0 1 2 5 0 0 0 0 1 5 0 0 0 0 0 5 5 5 5 5 5 5 0 1 2 3 4 5 0 0 2 3 3 5 0 0 0 2 2 5 0 0 0 0 1 5 0 0 0 0 0 5 -1 + 0 0 1 1 1 1 + 5 5 5 5 5 5 0 2 2 4 4 5 0 1 2 3 4 5 0 0 0 2 2 5 0 0 0 1 2 5 0 0 0 0 0 5 5 5 5 5 5 5 0 4 4 4 4 5 0 1 2 3 4 5 0 1 1 2 4 5 0 1 1 1 4 5 0 0 0 0 0 5 -1 + 0 0 0 1 1 1 + 5 5 5 5 5 5 0 4 4 4 4 5 0 1 3 3 4 5 0 1 2 3 4 5 0 1 1 1 4 5 0 0 0 0 0 5 -1 + -1 + -1 + 5 4 2 3 1 0 + 1 1 1 1 1 1 0 1 1 1 1 1 0 0 1 0 1 1 0 0 0 1 1 1 0 0 0 0 1 1 0 0 0 0 0 1 + 0 1 1 1 1 1 + 5 5 5 5 5 5 0 1 2 3 4 5 0 0 1 0 2 5 0 0 0 1 3 5 0 0 0 0 1 5 0 0 0 0 0 5 5 5 5 5 5 5 0 1 2 3 4 5 0 0 2 0 2 5 0 0 0 1 3 5 0 0 0 0 1 5 0 0 0 0 0 5 5 5 5 5 5 5 0 1 2 3 4 5 0 0 2 0 2 5 0 0 0 3 3 5 0 0 0 0 1 5 0 0 0 0 0 5 -1 + -1 + -1 + -1 + -1 From d86601c575bb4999bff90fd94191fd20d7b84ab6 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Thu, 3 Oct 2024 21:50:05 -0400 Subject: [PATCH 04/12] Edited example to check models of R up to size 6 --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 3dd895f..cb201d0 100644 --- a/README.md +++ b/README.md @@ -9,7 +9,7 @@ Interested in seeing which satisfiable models from [arranstewart/magic](https:// (2) Run our tool! It will first attempt to parse all the matrices in the output file and then check for the variable sharing property one-by-one. ``` -python3 parse_magic.py < UGLY_FILE_FROM_MAGIC +python3 parse_magic.py < examples/R6 ``` If you face any troubles, feel free to reach out. This tool also has capabilities to generate satisfiable models given a specification (see: R.py), however, it is much slower than magic so you're better off using that. From 2ed471c92ce8c58ee6972acecfe45ab118789684 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Thu, 3 Oct 2024 22:00:00 -0400 Subject: [PATCH 05/12] Discard models with only one designated value --- vsp.py | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/vsp.py b/vsp.py index 23d6beb..ff4bdae 100644 --- a/vsp.py +++ b/vsp.py @@ -63,6 +63,11 @@ def has_vsp(model: Model, interpretation: Dict[Operation, ModelFunction]) -> VSP """ impfunction = interpretation[Implication] + # NOTE: No models with only one designated + # value satisfies VSP + if len(model.designated_values) == 1: + return VSP_Result(False, model.name) + # Compute I the set of tuples (x, y) where # x -> y does not take a designiated value I: Set[Tuple[ModelValue, ModelValue]] = set() From d513656422059f186b3a982cf3ba430d368c9092 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Thu, 3 Oct 2024 23:34:59 -0400 Subject: [PATCH 06/12] Handle fragments without negation --- parse_magic.py | 145 ++++++++++++++++++++++++++++++++----------------- 1 file changed, 94 insertions(+), 51 deletions(-) diff --git a/parse_magic.py b/parse_magic.py index deda575..37ee58f 100644 --- a/parse_magic.py +++ b/parse_magic.py @@ -26,68 +26,113 @@ class SourceFile: self.current_line += 1 return contents +class UglyHeader: + def __init__(self, negation: bool, necessitation: bool): + self.negation = negation + self.necessitation = necessitation + +# NOTE: Global variable used to keep track of solution models +solutions: List[Tuple[Model, Dict]] = [] def parse_matrices(infile: SourceFile) -> List[Tuple[Model, Dict]]: - next(infile) # Skip header line - - solutions: List[Tuple[Model, Dict]] = [] + global solutions + solutions = [] # Reset + header = parse_header(infile) + process_sizes(infile, header) +def process_sizes(infile: SourceFile, header: UglyHeader): + """Stage 1""" while True: size = parse_size(infile) if size is None: break - carrier_set = carrier_set_from_size(size) + process_negations(infile, header, size, carrier_set) - num_negation = 0 - while True: - mnegation = parse_negation(infile, size) +def process_negations(infile: SourceFile, header: UglyHeader, size: int, carrier_set: Set[ModelValue]): + """Stage 2 (Optional)""" + num_negation = 0 + while True: + mnegation = None + if header.negation: + mnegation = parse_single_negation(infile, size) if mnegation is None: break num_negation += 1 - num_order = 0 - while True: - result = parse_order(infile, size) - if result is None: - break - mconjunction, mdisjunction = result - num_order += 1 + process_orders(infile, header, size, carrier_set, num_negation, mnegation) - num_designated = 0 - while True: - designated_values = parse_designated(infile, size) - if designated_values is None: - break - num_designated += 1 + if not header.negation: + break - results = parse_implication(infile, size) - if result is None: - break +def process_orders(infile: SourceFile, header: UglyHeader, size: int, carrier_set: Set[ModelValue], num_negation: int, mnegation: Optional[ModelFunction]): + """Stage 3""" + num_order = 0 + while True: + result = parse_single_order(infile, size) + if result is None: + break + mconjunction, mdisjunction = result + num_order += 1 + process_designateds(infile, header, size, carrier_set, num_negation, mnegation, num_order, mconjunction, mdisjunction) - num_implication = 0 - for mimplication in results: - logical_operations = { - mnegation, mimplication - } - num_implication += 1 - model_name = f"{size}.{num_negation}.{num_order}.{num_designated}.{num_implication}" - model = Model(carrier_set, logical_operations, designated_values, name=model_name) - interpretation = { - Negation: mnegation, - Implication: mimplication - } - if mconjunction is not None: - logical_operations.add(mconjunction) - interpretation[Conjunction] = mconjunction - if mdisjunction is not None: - logical_operations.add(mdisjunction) - interpretation[Disjunction] = mdisjunction +def process_designateds(infile: SourceFile, header: UglyHeader, size: int, carrier_set: Set[ModelValue], num_negation: int, mnegation: Optional[ModelFunction], num_order: int, mconjunction: Optional[ModelFunction], mdisjunction: Optional[ModelFunction]): + """Stage 4""" + num_designated = 0 + while True: + designated_values = parse_single_designated(infile, size) + if designated_values is None: + break + num_designated += 1 + process_implications(infile, header, size, carrier_set, num_negation, mnegation, num_order, mconjunction, mdisjunction, num_designated, designated_values) - solutions.append((model, interpretation)) - print(f"Parsed Matrix {model.name}") +def process_implications( + infile: SourceFile, header: UglyHeader, size: int, carrier_set: Set[ModelValue], num_negation: int, mnegation: Optional[ModelFunction], + num_order: int, mconjunction: Optional[ModelFunction], mdisjunction: Optional[ModelFunction], num_designated: int, designated_values: Set[ModelValue]): + """Stage 5""" + results = parse_implications(infile, size) + for num_implication, mimplication in enumerate(results, 1): + process_model(size, carrier_set, num_negation, mnegation, num_order, mconjunction, mdisjunction, num_designated, designated_values, num_implication, mimplication) - return solutions +def process_model( + size: int, carrier_set: Set[ModelValue], num_negation: int, mnegation: Optional[ModelFunction], + num_order: int, mconjunction: Optional[ModelFunction], mdisjunction: Optional[ModelFunction], num_designated: int, + designated_values: Set[ModelValue], num_implication: int, mimplication: ModelFunction): + """Create Model""" + global solutions + + logical_operations = { mimplication } + model_name = f"{size}{"." + str(num_negation) if num_negation != 0 else ""}.{num_order}.{num_designated}.{num_implication}" + model = Model(carrier_set, logical_operations, designated_values, name=model_name) + interpretation = { + Implication: mimplication + } + if mnegation is not None: + logical_operations.add(mnegation) + interpretation[Negation] = mnegation + if mconjunction is not None: + logical_operations.add(mconjunction) + interpretation[Conjunction] = mconjunction + if mdisjunction is not None: + logical_operations.add(mdisjunction) + interpretation[Disjunction] = mdisjunction + + solutions.append((model, interpretation)) + print(f"Parsed Matrix {model.name}") + +def parse_header(infile: SourceFile) -> UglyHeader: + """ + Parse the header line from the ugly data format. + NOTE: Currently Incomplete. + """ + header_line = next(infile).strip() + header_tokens = header_line.split(" ") + print(header_tokens) + assert header_tokens[0] in ["0", "1"] + assert header_tokens[6] in ["0", "1"] + negation_defined = bool(int(header_tokens[0])) + necessitation_defined = bool(int(header_tokens[6])) + return UglyHeader(negation_defined, necessitation_defined) def carrier_set_from_size(size: int): """ @@ -108,7 +153,7 @@ def parse_size(infile: SourceFile) -> Optional[int]: assert size > 0, f"Unexpected size at line {infile.current_line}" return size -def parse_negation(infile: SourceFile, size: int) -> Optional[ModelFunction]: +def parse_single_negation(infile: SourceFile, size: int) -> Optional[ModelFunction]: """ Parse the line representing the negation table. """ @@ -189,7 +234,7 @@ def determine_dresult(size: int, ordering: Dict[ModelValue, ModelValue], a: Mode if not invalid: return c -def parse_order(infile: TextIO, size: int) -> Optional[Tuple[ModelFunction, ModelFunction]]: +def parse_single_order(infile: TextIO, size: int) -> Optional[Tuple[ModelFunction, ModelFunction]]: """ Parse the line representing the ordering table """ @@ -240,7 +285,7 @@ def parse_order(infile: TextIO, size: int) -> Optional[Tuple[ModelFunction, Mode return mconjunction, mdisjunction -def parse_designated(infile: TextIO, size: int) -> Optional[Set[ModelValue]]: +def parse_single_designated(infile: TextIO, size: int) -> Optional[Set[ModelValue]]: """ Parse the line representing which model values are designated. """ @@ -261,14 +306,12 @@ def parse_designated(infile: TextIO, size: int) -> Optional[Set[ModelValue]]: return designated_values -def parse_implication(infile: TextIO, size: int) -> Optional[List[ModelFunction]]: +def parse_implications(infile: TextIO, size: int) -> List[ModelFunction]: """ Parse the line representing the list of implication tables. """ line = next(infile).strip() - if line == '-1': - return None # Split and remove the last '-1' character table = line.split(" ")[:-1] @@ -301,7 +344,7 @@ if __name__ == "__main__": parser = argparse.ArgumentParser(description="VSP Checker") parser.add_argument("--verbose", action='store_true', help="Print out all parsed matrices") args = vars(parser.parse_args()) - solutions: List[Model] = parse_matrices(SourceFile(sys.stdin)) + parse_matrices(SourceFile(sys.stdin)) print(f"Parsed {len(solutions)} matrices") for i, (model, interpretation) in enumerate(solutions): vsp_result = has_vsp(model, interpretation) From c8b3ca5900e5acacb8cd48004538e796555abe5e Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Fri, 4 Oct 2024 10:54:08 -0400 Subject: [PATCH 07/12] Fix for Python 3.10 --- parse_magic.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/parse_magic.py b/parse_magic.py index 37ee58f..9eb00fd 100644 --- a/parse_magic.py +++ b/parse_magic.py @@ -102,7 +102,7 @@ def process_model( global solutions logical_operations = { mimplication } - model_name = f"{size}{"." + str(num_negation) if num_negation != 0 else ""}.{num_order}.{num_designated}.{num_implication}" + model_name = f"{size}{'.' + str(num_negation) if num_negation != 0 else ''}.{num_order}.{num_designated}.{num_implication}" model = Model(carrier_set, logical_operations, designated_values, name=model_name) interpretation = { Implication: mimplication From 012323bcbc0759499768009d747bb99d5d93b19c Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Fri, 4 Oct 2024 13:16:09 -0400 Subject: [PATCH 08/12] Description of example files --- examples/README.md | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 examples/README.md diff --git a/examples/README.md b/examples/README.md new file mode 100644 index 0000000..115215f --- /dev/null +++ b/examples/README.md @@ -0,0 +1,8 @@ +# Example Ugly Data Format Files + +These are example files that you can use with the `parse_magic.py` script. + +## R6 + +Contains all models of R up to size 6. + From 5f3825cf72051425c213fd419afd119eee2d8ce3 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Fri, 4 Oct 2024 13:22:18 -0400 Subject: [PATCH 09/12] Added example fragment without negation --- examples/R4-MN | 32 ++++++++++++++++++++++++++++++++ examples/README.md | 3 +++ 2 files changed, 35 insertions(+) create mode 100644 examples/R4-MN diff --git a/examples/R4-MN b/examples/R4-MN new file mode 100644 index 0000000..0617984 --- /dev/null +++ b/examples/R4-MN @@ -0,0 +1,32 @@ + 0 1 1 1 1 1 0 0 + 1 + 1 1 0 1 + 0 1 + 1 1 0 1 -1 + -1 + -1 + 2 + 1 1 1 0 1 1 0 0 1 + 0 1 1 + 2 2 2 0 1 2 0 0 2 -1 + 0 0 1 + 2 2 2 0 2 2 0 1 2 -1 + -1 + -1 + 3 + 1 1 1 1 0 1 0 1 0 0 1 1 0 0 0 1 + 0 1 0 1 + 3 3 3 3 0 1 2 3 0 0 1 3 0 0 0 3 3 3 3 3 0 1 2 3 0 0 3 3 0 0 2 3 -1 + 0 0 0 1 + 3 3 3 3 2 3 2 3 1 1 3 3 0 1 2 3 -1 + -1 + 1 1 1 1 0 1 1 1 0 0 1 1 0 0 0 1 + 0 1 1 1 + 3 3 3 3 0 1 2 3 0 0 1 3 0 0 0 3 3 3 3 3 0 1 2 3 0 0 2 3 0 0 0 3 -1 + 0 0 1 1 + 3 3 3 3 0 2 2 3 0 1 2 3 0 0 0 3 3 3 3 3 0 3 3 3 0 1 2 3 0 1 1 3 -1 + 0 0 0 1 + 3 3 3 3 0 3 3 3 0 1 3 3 0 1 2 3 -1 + -1 + -1 + -1 diff --git a/examples/README.md b/examples/README.md index 115215f..7d82e22 100644 --- a/examples/README.md +++ b/examples/README.md @@ -6,3 +6,6 @@ These are example files that you can use with the `parse_magic.py` script. Contains all models of R up to size 6. +## R4-MN + +Contains all models of a fragment of R without negation up to size 4. From cd3b8f56df261982381f65fd469ace159f2a13da Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Fri, 4 Oct 2024 13:22:40 -0400 Subject: [PATCH 10/12] Added summary at end --- parse_magic.py | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/parse_magic.py b/parse_magic.py index 9eb00fd..6e35923 100644 --- a/parse_magic.py +++ b/parse_magic.py @@ -346,8 +346,14 @@ if __name__ == "__main__": args = vars(parser.parse_args()) parse_matrices(SourceFile(sys.stdin)) print(f"Parsed {len(solutions)} matrices") + num_has_vsp = 0 for i, (model, interpretation) in enumerate(solutions): vsp_result = has_vsp(model, interpretation) print(vsp_result) + if args['verbose'] or vsp_result.has_vsp: print(model) + + if vsp_result.has_vsp: + num_has_vsp += 1 + print(f"Tested {len(solutions)} models, {num_has_vsp} of which satisfy VSP") From 45ee3d546cacae4c41101148f4500016e5bf6f19 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Fri, 4 Oct 2024 13:27:57 -0400 Subject: [PATCH 11/12] Removed extraneous print --- parse_magic.py | 1 - 1 file changed, 1 deletion(-) diff --git a/parse_magic.py b/parse_magic.py index 6e35923..4bb4050 100644 --- a/parse_magic.py +++ b/parse_magic.py @@ -127,7 +127,6 @@ def parse_header(infile: SourceFile) -> UglyHeader: """ header_line = next(infile).strip() header_tokens = header_line.split(" ") - print(header_tokens) assert header_tokens[0] in ["0", "1"] assert header_tokens[6] in ["0", "1"] negation_defined = bool(int(header_tokens[0])) From b4b5a7d4e6eed7fb79d142e61f63299f65afe43e Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Fri, 4 Oct 2024 14:09:18 -0400 Subject: [PATCH 12/12] Refactored --- parse_magic.py | 99 ++++++++++++++++++++++++++++++-------------------- 1 file changed, 60 insertions(+), 39 deletions(-) diff --git a/parse_magic.py b/parse_magic.py index 4bb4050..07c4643 100644 --- a/parse_magic.py +++ b/parse_magic.py @@ -31,91 +31,112 @@ class UglyHeader: self.negation = negation self.necessitation = necessitation -# NOTE: Global variable used to keep track of solution models -solutions: List[Tuple[Model, Dict]] = [] +class ModelBuilder: + def __init__(self): + self.size : int = 0 + self.carrier_set : Set[ModelValue] = set() + self.num_negation: int = 0 + self.mnegation: Optional[ModelFunction] = None + self.num_order: int = 0 + self.mconjunction: Optional[ModelFunction] = None + self.mdisjunction: Optional[ModelFunction] = None + self.num_designated: int = 0 + self.designated_values: Set[ModelValue] = set() + self.num_implication: int = 0 + self.mimplication: Optional[ModelFunction] = None def parse_matrices(infile: SourceFile) -> List[Tuple[Model, Dict]]: - global solutions solutions = [] # Reset header = parse_header(infile) - process_sizes(infile, header) + current_model_parts = ModelBuilder() + process_sizes(infile, header, current_model_parts, solutions) + return solutions -def process_sizes(infile: SourceFile, header: UglyHeader): +def process_sizes(infile: SourceFile, header: UglyHeader, current_model_parts: ModelBuilder, solutions: List[Tuple[Model, Dict]]): """Stage 1""" while True: size = parse_size(infile) if size is None: break carrier_set = carrier_set_from_size(size) - process_negations(infile, header, size, carrier_set) + current_model_parts.size = size + current_model_parts.carrier_set = carrier_set + process_negations(infile, header, current_model_parts, solutions) -def process_negations(infile: SourceFile, header: UglyHeader, size: int, carrier_set: Set[ModelValue]): +def process_negations(infile: SourceFile, header: UglyHeader, current_model_parts: ModelBuilder, solutions: List[Tuple[Model, Dict]]): """Stage 2 (Optional)""" num_negation = 0 while True: mnegation = None if header.negation: - mnegation = parse_single_negation(infile, size) + mnegation = parse_single_negation(infile, current_model_parts.size) if mnegation is None: break num_negation += 1 - process_orders(infile, header, size, carrier_set, num_negation, mnegation) + current_model_parts.num_negation = num_negation + current_model_parts.mnegation = mnegation + + process_orders(infile, header, current_model_parts, solutions) if not header.negation: break -def process_orders(infile: SourceFile, header: UglyHeader, size: int, carrier_set: Set[ModelValue], num_negation: int, mnegation: Optional[ModelFunction]): +def process_orders(infile: SourceFile, header: UglyHeader, current_model_parts: ModelBuilder, solutions: List[Tuple[Model, Dict]]): """Stage 3""" num_order = 0 while True: - result = parse_single_order(infile, size) + result = parse_single_order(infile, current_model_parts.size) if result is None: break - mconjunction, mdisjunction = result num_order += 1 - process_designateds(infile, header, size, carrier_set, num_negation, mnegation, num_order, mconjunction, mdisjunction) + mconjunction, mdisjunction = result + current_model_parts.num_order = num_order + current_model_parts.mconjunction = mconjunction + current_model_parts.mdisjunction = mdisjunction + process_designateds(infile, header, current_model_parts, solutions) -def process_designateds(infile: SourceFile, header: UglyHeader, size: int, carrier_set: Set[ModelValue], num_negation: int, mnegation: Optional[ModelFunction], num_order: int, mconjunction: Optional[ModelFunction], mdisjunction: Optional[ModelFunction]): +def process_designateds(infile: SourceFile, header: UglyHeader, current_model_parts: ModelBuilder, solutions: List[Tuple[Model, Dict]]): """Stage 4""" num_designated = 0 while True: - designated_values = parse_single_designated(infile, size) + designated_values = parse_single_designated(infile, current_model_parts.size) if designated_values is None: break num_designated += 1 - process_implications(infile, header, size, carrier_set, num_negation, mnegation, num_order, mconjunction, mdisjunction, num_designated, designated_values) + current_model_parts.num_designated = num_designated + current_model_parts.designated_values = designated_values + process_implications(infile, header, current_model_parts, solutions) def process_implications( - infile: SourceFile, header: UglyHeader, size: int, carrier_set: Set[ModelValue], num_negation: int, mnegation: Optional[ModelFunction], - num_order: int, mconjunction: Optional[ModelFunction], mdisjunction: Optional[ModelFunction], num_designated: int, designated_values: Set[ModelValue]): + infile: SourceFile, header: UglyHeader, current_model_parts: ModelBuilder, solutions: List[Tuple[Model, Dict]]): """Stage 5""" - results = parse_implications(infile, size) + results = parse_implications(infile, current_model_parts.size) for num_implication, mimplication in enumerate(results, 1): - process_model(size, carrier_set, num_negation, mnegation, num_order, mconjunction, mdisjunction, num_designated, designated_values, num_implication, mimplication) + current_model_parts.num_implication = num_implication + current_model_parts.mimplication = mimplication + process_model(current_model_parts, solutions) -def process_model( - size: int, carrier_set: Set[ModelValue], num_negation: int, mnegation: Optional[ModelFunction], - num_order: int, mconjunction: Optional[ModelFunction], mdisjunction: Optional[ModelFunction], num_designated: int, - designated_values: Set[ModelValue], num_implication: int, mimplication: ModelFunction): +def process_model(mp: ModelBuilder, solutions: List[Tuple[Model, Dict]]): """Create Model""" - global solutions + assert mp.mimplication is not None + assert len(mp.carrier_set) > 0 - logical_operations = { mimplication } - model_name = f"{size}{'.' + str(num_negation) if num_negation != 0 else ''}.{num_order}.{num_designated}.{num_implication}" - model = Model(carrier_set, logical_operations, designated_values, name=model_name) + logical_operations = { mp.mimplication } + model_name = f"{mp.size}{'.' + str(mp.num_negation) if mp.num_negation != 0 else ''}.{mp.num_order}.{mp.num_designated}.{mp.num_implication}" + model = Model(mp.carrier_set, logical_operations, mp.designated_values, name=model_name) interpretation = { - Implication: mimplication + Implication: mp.mimplication } - if mnegation is not None: - logical_operations.add(mnegation) - interpretation[Negation] = mnegation - if mconjunction is not None: - logical_operations.add(mconjunction) - interpretation[Conjunction] = mconjunction - if mdisjunction is not None: - logical_operations.add(mdisjunction) - interpretation[Disjunction] = mdisjunction + 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 solutions.append((model, interpretation)) print(f"Parsed Matrix {model.name}") @@ -343,7 +364,7 @@ if __name__ == "__main__": parser = argparse.ArgumentParser(description="VSP Checker") parser.add_argument("--verbose", action='store_true', help="Print out all parsed matrices") args = vars(parser.parse_args()) - parse_matrices(SourceFile(sys.stdin)) + solutions = parse_matrices(SourceFile(sys.stdin)) print(f"Parsed {len(solutions)} matrices") num_has_vsp = 0 for i, (model, interpretation) in enumerate(solutions):