Added ability to parse necessitation

This commit is contained in:
Brandon Rozek 2024-10-04 15:51:05 -04:00
parent b4b5a7d4e6
commit 46e570103f
4 changed files with 154 additions and 9 deletions

27
examples/R3-PN Normal file
View file

@ -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

View file

@ -9,3 +9,13 @@ Contains all models of R up to size 6.
## R4-MN ## R4-MN
Contains all models of a fragment of R without negation up to size 4. 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.

View file

@ -66,6 +66,7 @@ Negation = Operation("¬", 1)
Conjunction = Operation("", 2) Conjunction = Operation("", 2)
Disjunction = Operation("", 2) Disjunction = Operation("", 2)
Implication = Operation("", 2) Implication = Operation("", 2)
Necessitation = Operation("!", 1)
class Inequation: class Inequation:
def __init__(self, antecedant : Term, consequent: Term): def __init__(self, antecedant : Term, consequent: Term):

View file

@ -12,6 +12,7 @@ from logic import (
Implication, Implication,
Conjunction, Conjunction,
Negation, Negation,
Necessitation,
Disjunction Disjunction
) )
from vsp import has_vsp from vsp import has_vsp
@ -44,6 +45,8 @@ class ModelBuilder:
self.designated_values: Set[ModelValue] = set() self.designated_values: Set[ModelValue] = set()
self.num_implication: int = 0 self.num_implication: int = 0
self.mimplication: Optional[ModelFunction] = None self.mimplication: Optional[ModelFunction] = None
self.num_necessitation: int = 0
self.mnecessitation: Optional[ModelFunction] = None
def parse_matrices(infile: SourceFile) -> List[Tuple[Model, Dict]]: def parse_matrices(infile: SourceFile) -> List[Tuple[Model, Dict]]:
solutions = [] # Reset 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]]): def process_sizes(infile: SourceFile, header: UglyHeader, current_model_parts: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
"""Stage 1""" """Stage 1"""
# NOTE: In R3-PN the first size line is -1?
if header.necessitation:
next(infile)
while True: while True:
print("Processing next size")
try:
size = parse_size(infile) 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: if size is None:
break break
carrier_set = carrier_set_from_size(size) carrier_set = carrier_set_from_size(size)
current_model_parts.size = size current_model_parts.size = size
current_model_parts.carrier_set = carrier_set current_model_parts.carrier_set = carrier_set
@ -67,6 +82,7 @@ def process_negations(infile: SourceFile, header: UglyHeader, current_model_part
"""Stage 2 (Optional)""" """Stage 2 (Optional)"""
num_negation = 0 num_negation = 0
while True: while True:
print("Processing next negation")
mnegation = None mnegation = None
if header.negation: if header.negation:
mnegation = parse_single_negation(infile, current_model_parts.size) 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""" """Stage 3"""
num_order = 0 num_order = 0
while True: while True:
print("Processing next order")
result = parse_single_order(infile, current_model_parts.size) result = parse_single_order(infile, current_model_parts.size)
if result is None: if result is None:
break break
@ -100,6 +117,7 @@ def process_designateds(infile: SourceFile, header: UglyHeader, current_model_pa
"""Stage 4""" """Stage 4"""
num_designated = 0 num_designated = 0
while True: while True:
print("Processing next designated")
designated_values = parse_single_designated(infile, current_model_parts.size) designated_values = parse_single_designated(infile, current_model_parts.size)
if designated_values is None: if designated_values is None:
break break
@ -111,19 +129,54 @@ def process_designateds(infile: SourceFile, header: UglyHeader, current_model_pa
def process_implications( def process_implications(
infile: SourceFile, header: UglyHeader, current_model_parts: ModelBuilder, solutions: List[Tuple[Model, Dict]]): infile: SourceFile, header: UglyHeader, current_model_parts: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
"""Stage 5""" """Stage 5"""
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) results = parse_implications(infile, current_model_parts.size)
for num_implication, mimplication in enumerate(results, 1): for num_implication, mimplication in enumerate(results, 1):
current_model_parts.num_implication = num_implication current_model_parts.num_implication = num_implication
current_model_parts.mimplication = mimplication current_model_parts.mimplication = mimplication
process_model(current_model_parts, solutions) 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]]): def process_model(mp: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
"""Create Model""" """Create Model"""
assert mp.mimplication is not None assert mp.mimplication is not None
assert len(mp.carrier_set) > 0 assert len(mp.carrier_set) > 0
logical_operations = { mp.mimplication } 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) model = Model(mp.carrier_set, logical_operations, mp.designated_values, name=model_name)
interpretation = { interpretation = {
Implication: mp.mimplication Implication: mp.mimplication
@ -137,6 +190,9 @@ def process_model(mp: ModelBuilder, solutions: List[Tuple[Model, Dict]]):
if mp.mdisjunction is not None: if mp.mdisjunction is not None:
logical_operations.add(mp.mdisjunction) logical_operations.add(mp.mdisjunction)
interpretation[Disjunction] = 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)) solutions.append((model, interpretation))
print(f"Parsed Matrix {model.name}") print(f"Parsed Matrix {model.name}")
@ -254,7 +310,7 @@ def determine_dresult(size: int, ordering: Dict[ModelValue, ModelValue], a: Mode
if not invalid: if not invalid:
return c 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 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 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. 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 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 Parse the line representing the list of implication
tables. tables.
@ -359,6 +444,28 @@ def parse_implications(infile: TextIO, size: int) -> List[ModelFunction]:
return mimplications 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__": if __name__ == "__main__":
parser = argparse.ArgumentParser(description="VSP Checker") parser = argparse.ArgumentParser(description="VSP Checker")