matmod/parse_magic.py

305 lines
8.7 KiB
Python
Raw Permalink Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

"""
Parses the Magic Ugly Data File Format
Assumes the base logic is R with no extra connectives
"""
import sys
from typing import TextIO, List, Optional, Tuple, Set, Dict
from model import Model, ModelValue, ModelFunction
from logic import (
Implication,
Conjunction,
Negation,
Disjunction
)
from vsp import has_vsp
class SourceFile:
def __init__(self, fileobj: TextIO):
self.fileobj = fileobj
self.current_line = 0
def __next__(self):
contents = next(self.fileobj)
self.current_line += 1
return contents
def parse_matrices(infile: SourceFile) -> List[Tuple[Model, Dict]]:
next(infile) # Skip header line
solutions: List[Tuple[Model, Dict]] = []
while True:
size = parse_size(infile)
if size is None:
break
carrier_set = carrier_set_from_size(size)
num_negation = 0
while True:
mnegation = parse_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
num_designated = 0
while True:
designated_values = parse_designated(infile, size)
if designated_values is None:
break
num_designated += 1
results = parse_implication(infile, size)
if result is None:
break
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
solutions.append((model, interpretation))
print(f"Parsed Matrix {model.name}")
return solutions
def carrier_set_from_size(size: int):
"""
Construct a carrier set of model values
based on the desired size.
"""
return {
mvalue_from_index(i) for i in range(size + 1)
}
def parse_size(infile: SourceFile) -> Optional[int]:
"""
Parse the line representing the matrix size.
"""
size = int(next(infile))
if size == -1:
return None
assert size > 0, f"Unexpected size at line {infile.current_line}"
return size
def parse_negation(infile: SourceFile, size: int) -> Optional[ModelFunction]:
"""
Parse the line representing the negation table.
"""
line = next(infile).strip()
if line == '-1':
return None
row = line.split(" ")
assert len(row) == size + 1, f"Negation table doesn't match size at line {infile.current_line}"
mapping = {}
for i, j in zip(range(size + 1), row):
x = mvalue_from_index(i)
y = parse_mvalue(j)
mapping[(x, )] = y
return ModelFunction(1, mapping, "¬")
def mvalue_from_index(i: int):
"""
Given an index, return the
representation of the model value.
"""
return ModelValue(f"a{i}")
def parse_mvalue(x: str) -> ModelValue:
"""
Parse an element and return the model value.
"""
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_order(infile: TextIO, size: int) -> Optional[Tuple[ModelFunction, ModelFunction]]:
"""
Parse the line representing the ordering table
"""
line = next(infile).strip()
if line == '-1':
return None
table = line.split(" ")
assert len(table) == (size + 1)**2, f"Order table doesn't match expected size at line {infile.current_line}"
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'
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
mconjunction = ModelFunction(2, cmapping, "")
mdisjunction = ModelFunction(2, dmapping, "")
return mconjunction, mdisjunction
def parse_designated(infile: TextIO, size: int) -> Optional[Set[ModelValue]]:
"""
Parse the line representing which model values are designated.
"""
line = next(infile).strip()
if line == '-1':
return None
row = line.split(" ")
assert len(row) == size + 1, f"Designated table doesn't match expected size at line {infile.current_line}"
designated_values = set()
for i, j in zip(range(size + 1), row):
if j == '1':
x = mvalue_from_index(i)
designated_values.add(x)
return designated_values
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]
assert len(table) % (size + 1)**2 == 0, f"Implication table does not match expected size at line {infile.current_line}"
table_i = 0
mimplications: List[ModelFunction] = []
for _ in range(len(table) // (size + 1)**2):
mapping = {}
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
mimplication = ModelFunction(2, mapping, "")
mimplications.append(mimplication)
return mimplications
if __name__ == "__main__":
solutions: List[Model] = parse_matrices(SourceFile(sys.stdin))
print(f"Parsed {len(solutions)} matrices")
for i, (model, interpretation) in enumerate(solutions):
print(model)
print(has_vsp(model, interpretation))