diff --git a/parse_magic.py b/parse_magic.py index f77295a..4254d5f 100644 --- a/parse_magic.py +++ b/parse_magic.py @@ -28,9 +28,10 @@ class SourceFile: return contents 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.necessitation = necessitation + self.custom_model_functions = custom_model_functions class ModelBuilder: def __init__(self): @@ -199,15 +200,21 @@ def process_model(mp: ModelBuilder, solutions: List[Tuple[Model, Dict]]): 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"] + assert len(header_tokens) >= 7 negation_defined = bool(int(header_tokens[0])) 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): """ @@ -222,10 +229,13 @@ def parse_size(infile: SourceFile, first_run: bool) -> Optional[int]: """ Parse the line representing the matrix size. """ + size = int(next(infile)) - # HACK: The first size line may be -1 due to a bug. Skip it - if size == -1 and first_run: - size = int(next(infile)) + # HACK: When necessitation and custom connectives are enabled + # MaGIC may produce -1s at the beginning of the file + if first_run: + while size == -1: + size = int(next(infile)) if size == -1: return None