Refactored

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.

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

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

examples/README.md

@@ -0,0 +1,11 @@
+# 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.
+
+## R4-MN
+
+Contains all models of a fragment of R without negation up to size 4.

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
 
@@ -25,68 +26,133 @@ class SourceFile:
         self.current_line += 1
         return contents
 
+class UglyHeader:
+    def __init__(self, negation: bool, necessitation: bool):
+        self.negation = negation
+        self.necessitation = necessitation
+
+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]]:
-    next(infile) # Skip header line
+    solutions = [] # Reset
-
+    header = parse_header(infile)
-    solutions: List[Tuple[Model, Dict]] = []
+    current_model_parts = ModelBuilder()
+    process_sizes(infile, header, current_model_parts, solutions)
+    return solutions
 
+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)
+        current_model_parts.size = size
+        current_model_parts.carrier_set = carrier_set
+        process_negations(infile, header, current_model_parts, solutions)
 
-        num_negation = 0
+def process_negations(infile: SourceFile, header: UglyHeader, current_model_parts: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
-        while True:
+    """Stage 2 (Optional)"""
-            mnegation = parse_negation(infile, size)
+    num_negation = 0
+    while True:
+        mnegation = None
+        if header.negation:
+            mnegation = parse_single_negation(infile, current_model_parts.size)
             if mnegation is None:
                 break
             num_negation += 1
 
-            num_order = 0
+        current_model_parts.num_negation = num_negation
-            while True:
+        current_model_parts.mnegation = mnegation
-                result = parse_order(infile, size)
-                if result is None:
-                    break
-                mconjunction, mdisjunction = result
-                num_order += 1
 
-                num_designated = 0
+        process_orders(infile, header, current_model_parts, solutions)
-                while True:
-                    designated_values = parse_designated(infile, size)
-                    if designated_values is None:
-                        break
-                    num_designated += 1
 
-                    results = parse_implication(infile, size)
+        if not header.negation:
-                    if result is None:
+            break
-                        break
 
-                    num_implication = 0
+def process_orders(infile: SourceFile, header: UglyHeader, current_model_parts: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
-                    for mimplication in results:
+    """Stage 3"""
-                        logical_operations = {
+    num_order = 0
-                            mnegation, mimplication
+    while True:
-                        }
+        result = parse_single_order(infile, current_model_parts.size)
-                        num_implication += 1
+        if result is None:
-                        model_name = f"{size}.{num_negation}.{num_order}.{num_designated}.{num_implication}"
+            break
-                        model = Model(carrier_set, logical_operations, designated_values, name=model_name)
+        num_order += 1
-                        interpretation = {
+        mconjunction, mdisjunction = result
-                            Negation: mnegation,
+        current_model_parts.num_order = num_order
-                            Implication: mimplication
+        current_model_parts.mconjunction = mconjunction
-                        }
+        current_model_parts.mdisjunction = mdisjunction
-                        if mconjunction is not None:
+        process_designateds(infile, header, current_model_parts, solutions)
-                            logical_operations.add(mconjunction)
-                            interpretation[Conjunction] = mconjunction
-                        if mdisjunction is not None:
-                            logical_operations.add(mdisjunction)
-                            interpretation[Disjunction] = mdisjunction
 
-                        solutions.append((model, interpretation))
+def process_designateds(infile: SourceFile, header: UglyHeader, current_model_parts: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
-                        print(f"Parsed Matrix {model.name}")
+    """Stage 4"""
+    num_designated = 0
+    while True:
+        designated_values = parse_single_designated(infile, current_model_parts.size)
+        if designated_values is None:
+            break
+        num_designated += 1
+        current_model_parts.num_designated = num_designated
+        current_model_parts.designated_values = designated_values
+        process_implications(infile, header, current_model_parts, solutions)
 
-    return solutions
+def process_implications(
+    infile: SourceFile, header: UglyHeader, current_model_parts: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
+    """Stage 5"""
+    results = parse_implications(infile, current_model_parts.size)
+    for num_implication, mimplication in enumerate(results, 1):
+        current_model_parts.num_implication = num_implication
+        current_model_parts.mimplication = mimplication
+        process_model(current_model_parts, solutions)
+
+def process_model(mp: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
+    """Create Model"""
+    assert mp.mimplication is not None
+    assert len(mp.carrier_set) > 0
+
+    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: 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
+
+    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(" ")
+    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):
     """
@@ -107,7 +173,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.
     """
@@ -188,7 +254,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
     """
@@ -239,7 +305,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.
     """
@@ -260,14 +326,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]
@@ -297,8 +361,19 @@ def parse_implication(infile: TextIO, size: int) -> Optional[List[ModelFunction]
 
 
 if __name__ == "__main__":
-    solutions: List[Model] = parse_matrices(SourceFile(sys.stdin))
+    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 = parse_matrices(SourceFile(sys.stdin))
     print(f"Parsed {len(solutions)} matrices")
+    num_has_vsp = 0
     for i, (model, interpretation) in enumerate(solutions):
-        print(model)
+        vsp_result = has_vsp(model, interpretation)
-        print(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")

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()