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 < examples/R6
+python3 parse_magic.py < UGLY_FILE_FROM_MAGIC
 ```
 
 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

@@ -1,32 +0,0 @@
- 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

@@ -1,78 +0,0 @@
- 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

@@ -1,11 +0,0 @@
-# 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,7 +3,6 @@ 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
 
@@ -26,133 +25,68 @@ 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]]:
-    solutions = [] # Reset
+    next(infile) # Skip header line
-    header = parse_header(infile)
+
-    current_model_parts = ModelBuilder()
+    solutions: List[Tuple[Model, Dict]] = []
-    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)
 
-def process_negations(infile: SourceFile, header: UglyHeader, current_model_parts: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
+        carrier_set = carrier_set_from_size(size)
-    """Stage 2 (Optional)"""
+
-    num_negation = 0
+        num_negation = 0
-    while True:
+        while True:
-        mnegation = None
+            mnegation = parse_negation(infile, size)
-        if header.negation:
-            mnegation = parse_single_negation(infile, current_model_parts.size)
             if mnegation is None:
                 break
             num_negation += 1
 
-        current_model_parts.num_negation = num_negation
+            num_order = 0
-        current_model_parts.mnegation = mnegation
+            while True:
+                result = parse_order(infile, size)
+                if result is None:
+                    break
+                mconjunction, mdisjunction = result
+                num_order += 1
 
-        process_orders(infile, header, current_model_parts, solutions)
+                num_designated = 0
+                while True:
+                    designated_values = parse_designated(infile, size)
+                    if designated_values is None:
+                        break
+                    num_designated += 1
 
-        if not header.negation:
+                    results = parse_implication(infile, size)
-            break
+                    if result is None:
+                        break
 
-def process_orders(infile: SourceFile, header: UglyHeader, current_model_parts: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
+                    num_implication = 0
-    """Stage 3"""
+                    for mimplication in results:
-    num_order = 0
+                        logical_operations = {
-    while True:
+                            mnegation, mimplication
-        result = parse_single_order(infile, current_model_parts.size)
+                        }
-        if result is None:
+                        num_implication += 1
-            break
+                        model_name = f"{size}.{num_negation}.{num_order}.{num_designated}.{num_implication}"
-        num_order += 1
+                        model = Model(carrier_set, logical_operations, designated_values, name=model_name)
-        mconjunction, mdisjunction = result
+                        interpretation = {
-        current_model_parts.num_order = num_order
+                            Negation: mnegation,
-        current_model_parts.mconjunction = mconjunction
+                            Implication: mimplication
-        current_model_parts.mdisjunction = mdisjunction
+                        }
-        process_designateds(infile, header, current_model_parts, solutions)
+                        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, current_model_parts: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
+                        solutions.append((model, interpretation))
-    """Stage 4"""
+                        print(f"Parsed Matrix {model.name}")
-    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)
 
-def process_implications(
+    return solutions
-    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):
     """
@@ -173,7 +107,7 @@ def parse_size(infile: SourceFile) -> Optional[int]:
     assert size > 0, f"Unexpected size at line {infile.current_line}"
     return size
 
-def parse_single_negation(infile: SourceFile, size: int) -> Optional[ModelFunction]:
+def parse_negation(infile: SourceFile, size: int) -> Optional[ModelFunction]:
     """
     Parse the line representing the negation table.
     """
@@ -254,7 +188,7 @@ def determine_dresult(size: int, ordering: Dict[ModelValue, ModelValue], a: Mode
         if not invalid:
             return c
 
-def parse_single_order(infile: TextIO, size: int) -> Optional[Tuple[ModelFunction, ModelFunction]]:
+def parse_order(infile: TextIO, size: int) -> Optional[Tuple[ModelFunction, ModelFunction]]:
     """
     Parse the line representing the ordering table
     """
@@ -305,7 +239,7 @@ def parse_single_order(infile: TextIO, size: int) -> Optional[Tuple[ModelFunctio
 
     return mconjunction, mdisjunction
 
-def parse_single_designated(infile: TextIO, size: int) -> Optional[Set[ModelValue]]:
+def parse_designated(infile: TextIO, size: int) -> Optional[Set[ModelValue]]:
     """
     Parse the line representing which model values are designated.
     """
@@ -326,12 +260,14 @@ def parse_single_designated(infile: TextIO, size: int) -> Optional[Set[ModelValu
     return designated_values
 
 
-def parse_implications(infile: TextIO, size: int) -> List[ModelFunction]:
+def parse_implication(infile: TextIO, size: int) -> Optional[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]
@@ -361,19 +297,8 @@ def parse_implications(infile: TextIO, size: int) -> List[ModelFunction]:
 
 
 if __name__ == "__main__":
-    parser = argparse.ArgumentParser(description="VSP Checker")
+    solutions: List[Model] = parse_matrices(SourceFile(sys.stdin))
-    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):
-        vsp_result = has_vsp(model, interpretation)
+        print(model)
-        print(vsp_result)
+        print(has_vsp(model, interpretation))
-
-        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,11 +63,6 @@ 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()