diff --git a/examples/R3-PN b/examples/R3-PN new file mode 100644 index 0000000..d6ceb3a --- /dev/null +++ b/examples/R3-PN @@ -0,0 +1,27 @@ + 1 1 1 1 1 1 1 0 + -1 + 1 + 1 0 + 1 1 0 1 + 0 1 + 1 1 0 1 0 1 + 1 1 + -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 0 1 1 + 1 1 1 + 0 1 2 + 0 2 2 + 2 2 2 + -1 + -1 + -1 + -1 + -1 diff --git a/examples/README.md b/examples/README.md index 7d82e22..9668226 100644 --- a/examples/README.md +++ b/examples/README.md @@ -9,3 +9,13 @@ 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. + +## R3-PN + +Extends R to have necessitation with the following additional axioms: + +1) p / !p +2) !(p -> q) -> (!p -> !q) +3) (!p & !q) -> !(p & q) + +Output contains all satisfiable models up to size 3. diff --git a/logic.py b/logic.py index 39eb95d..f81059d 100644 --- a/logic.py +++ b/logic.py @@ -66,6 +66,7 @@ Negation = Operation("¬", 1) Conjunction = Operation("∧", 2) Disjunction = Operation("∨", 2) Implication = Operation("→", 2) +Necessitation = Operation("!", 1) class Inequation: def __init__(self, antecedant : Term, consequent: Term): diff --git a/parse_magic.py b/parse_magic.py index 07c4643..bbd0f49 100644 --- a/parse_magic.py +++ b/parse_magic.py @@ -12,6 +12,7 @@ from logic import ( Implication, Conjunction, Negation, + Necessitation, Disjunction ) from vsp import has_vsp @@ -44,6 +45,8 @@ class ModelBuilder: self.designated_values: Set[ModelValue] = set() self.num_implication: int = 0 self.mimplication: Optional[ModelFunction] = None + self.num_necessitation: int = 0 + self.mnecessitation: Optional[ModelFunction] = None def parse_matrices(infile: SourceFile) -> List[Tuple[Model, Dict]]: solutions = [] # Reset @@ -54,10 +57,22 @@ def parse_matrices(infile: SourceFile) -> List[Tuple[Model, Dict]]: def process_sizes(infile: SourceFile, header: UglyHeader, current_model_parts: ModelBuilder, solutions: List[Tuple[Model, Dict]]): """Stage 1""" + + # NOTE: In R3-PN the first size line is -1? + if header.necessitation: + next(infile) + while True: - size = parse_size(infile) + print("Processing next size") + try: + size = parse_size(infile) + except StopIteration: + # For some reason, when necessitation is enabled this doesn't + # have a -1 on the last line + break if size is None: break + carrier_set = carrier_set_from_size(size) current_model_parts.size = size current_model_parts.carrier_set = carrier_set @@ -67,6 +82,7 @@ def process_negations(infile: SourceFile, header: UglyHeader, current_model_part """Stage 2 (Optional)""" num_negation = 0 while True: + print("Processing next negation") mnegation = None if header.negation: mnegation = parse_single_negation(infile, current_model_parts.size) @@ -86,6 +102,7 @@ def process_orders(infile: SourceFile, header: UglyHeader, current_model_parts: """Stage 3""" num_order = 0 while True: + print("Processing next order") result = parse_single_order(infile, current_model_parts.size) if result is None: break @@ -100,6 +117,7 @@ def process_designateds(infile: SourceFile, header: UglyHeader, current_model_pa """Stage 4""" num_designated = 0 while True: + print("Processing next designated") designated_values = parse_single_designated(infile, current_model_parts.size) if designated_values is None: break @@ -111,10 +129,45 @@ def process_designateds(infile: SourceFile, header: UglyHeader, current_model_pa 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 + if header.necessitation: + num_implication = 0 + while True: + print("Processing next implication") + instr = next(infile).strip() + mimplication, reststr = parse_single_implication(instr, infile.current_line, current_model_parts.size) + if mimplication is None: + break + num_implication += 1 + current_model_parts.num_implication = num_implication + current_model_parts.mimplication = mimplication + process_necessitations(infile, reststr, header, current_model_parts, solutions) + else: + 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_necessitations(infile: SourceFile, instr: str, header: UglyHeader, current_model_parts: ModelBuilder, solutions: List[Tuple[Model, Dict]]): + + # NOTE: For some reason, one necessitation table will be on the same line as the implication table + mnecessitation = parse_single_necessitation_from_str(instr, infile.current_line, current_model_parts.size) + assert mnecessitation is not None, f"Expected Necessitation Table at line {infile.current_line}" + num_necessitation = 1 + + current_model_parts.num_necessitation = num_necessitation + current_model_parts.mnecessitation = mnecessitation + process_model(current_model_parts, solutions) + + while True: + print("Processing next necessitation") + mnecessitation = parse_single_necessitation(infile, current_model_parts.size) + if mnecessitation is None: + break + num_necessitation += 1 + + current_model_parts.num_necessitation = num_necessitation + current_model_parts.mnecessitation = mnecessitation process_model(current_model_parts, solutions) def process_model(mp: ModelBuilder, solutions: List[Tuple[Model, Dict]]): @@ -123,7 +176,7 @@ def process_model(mp: ModelBuilder, solutions: List[Tuple[Model, Dict]]): 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_name = f"{mp.size}{'.' + str(mp.num_negation) if mp.num_negation != 0 else ''}.{mp.num_order}.{mp.num_designated}.{mp.num_implication}{'.' + str(mp.num_necessitation) if mp.num_necessitation != 0 else ''}" model = Model(mp.carrier_set, logical_operations, mp.designated_values, name=model_name) interpretation = { Implication: mp.mimplication @@ -137,6 +190,9 @@ def process_model(mp: ModelBuilder, solutions: List[Tuple[Model, Dict]]): if mp.mdisjunction is not None: logical_operations.add(mp.mdisjunction) interpretation[Disjunction] = mp.mdisjunction + if mp.mnecessitation is not None: + logical_operations.add(mp.mnecessitation) + interpretation[Necessitation] = mp.mnecessitation solutions.append((model, interpretation)) print(f"Parsed Matrix {model.name}") @@ -254,7 +310,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_single_order(infile: SourceFile, size: int) -> Optional[Tuple[ModelFunction, ModelFunction]]: """ Parse the line representing the ordering table """ @@ -305,7 +361,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_single_designated(infile: SourceFile, size: int) -> Optional[Set[ModelValue]]: """ Parse the line representing which model values are designated. """ @@ -326,7 +382,36 @@ 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_single_implication(instr: str, line: int, size: int) -> Tuple[ModelFunction, str]: + """ + Take the current string, parse an implication table from it, + and return along with it the remainder of the string + """ + if instr == "-1": + return None, "" + + table = instr.split(" ") + + assert len(table) >= (size + 1)**2, f"Implication table does not match expected size at line {line}" + + mapping = {} + 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) + + r = parse_mvalue(table[table_i]) + table_i += 1 + + mapping[(x, y)] = r + + mimplication = ModelFunction(2, mapping, "→") + reststr = " ".join(table[(size + 1)**2:]) + return mimplication, reststr + + +def parse_implications(infile: SourceFile, size: int) -> List[ModelFunction]: """ Parse the line representing the list of implication tables. @@ -359,6 +444,28 @@ def parse_implications(infile: TextIO, size: int) -> List[ModelFunction]: return mimplications +def parse_single_necessitation_from_str(instr: str, line: int, size: int) -> Optional[ModelFunction]: + """ + Parse the line representing the necessitation table. + """ + if instr == "-1": + return None + + row = instr.split(" ") + assert len(row) == size + 1, f"Necessitation table doesn't match size at line {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 parse_single_necessitation(infile: SourceFile, size: int) -> Optional[ModelFunction]: + line = next(infile).strip() + return parse_single_necessitation_from_str(line, infile.current_line, size) + if __name__ == "__main__": parser = argparse.ArgumentParser(description="VSP Checker")