brozek/vspursuer
1
0
Fork 0
mirror of https://github.com/Brandon-Rozek/matmod.git synced 2025-06-19 11:35:54 +00:00
Code Issues Projects Releases Packages Wiki Activity

Merge 312e1aeda5 into 84e4d3d1e1

Browse source
This commit is contained in:
Brandon Rozek 2024-10-24 21:22:50 -04:00 • committed by GitHub
commit b5ce1d4064
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 16 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
parse_magic.py
View file

@ -28,9 +28,10 @@ class SourceFile:
return contents return contents
class UglyHeader: class UglyHeader:
def __init__(self, negation: bool, necessitation: bool): def __init__(self, negation: bool, necessitation: bool, custom_model_functions: List[Tuple[int, str]]):
self.negation = negation self.negation = negation
self.necessitation = necessitation self.necessitation = necessitation
self.custom_model_functions = custom_model_functions
class ModelBuilder: class ModelBuilder:
def __init__(self): def __init__(self):
@ -199,15 +200,21 @@ def process_model(mp: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
def parse_header(infile: SourceFile) -> UglyHeader: def parse_header(infile: SourceFile) -> UglyHeader:
""" """
Parse the header line from the ugly data format. Parse the header line from the ugly data format.
NOTE: Currently Incomplete.
""" """
header_line = next(infile).strip() header_line = next(infile).strip()
header_tokens = header_line.split(" ") header_tokens = header_line.split(" ")
assert header_tokens[0] in ["0", "1"] assert header_tokens[0] in ["0", "1"]
assert header_tokens[6] in ["0", "1"] assert header_tokens[6] in ["0", "1"]
assert len(header_tokens) >= 7
negation_defined = bool(int(header_tokens[0])) negation_defined = bool(int(header_tokens[0]))
necessitation_defined = bool(int(header_tokens[6])) necessitation_defined = bool(int(header_tokens[6]))
return UglyHeader(negation_defined, necessitation_defined) num_custom_connectives = int(header_tokens[7])
custom_model_functions: List[Tuple[int, str]] = []
for i in range(num_custom_connectives):
arity = int(header_tokens[7 + (2 * i) + 1])
symbol = header_tokens[7 + (2 * i) + 2]
custom_model_functions.append((arity, symbol))
return UglyHeader(negation_defined, necessitation_defined, custom_model_functions)
def carrier_set_from_size(size: int): def carrier_set_from_size(size: int):
""" """
@ -222,10 +229,13 @@ def parse_size(infile: SourceFile, first_run: bool) -> Optional[int]:
""" """
Parse the line representing the matrix size. Parse the line representing the matrix size.
""" """
size = int(next(infile)) size = int(next(infile))
# HACK: The first size line may be -1 due to a bug. Skip it # HACK: When necessitation and custom connectives are enabled
if size == -1 and first_run: # MaGIC may produce -1s at the beginning of the file
size = int(next(infile)) if first_run:
while size == -1:
size = int(next(infile))
if size == -1: if size == -1:
return None return None