mirror of
https://github.com/Brandon-Rozek/matmod.git
synced 2024-11-22 22:06:29 -05:00
Handle fragments without negation
This commit is contained in:
parent
d86601c575
commit
d513656422
1 changed files with 94 additions and 51 deletions
|
@ -26,57 +26,90 @@ class SourceFile:
|
||||||
self.current_line += 1
|
self.current_line += 1
|
||||||
return contents
|
return contents
|
||||||
|
|
||||||
|
class UglyHeader:
|
||||||
|
def __init__(self, negation: bool, necessitation: bool):
|
||||||
|
self.negation = negation
|
||||||
|
self.necessitation = necessitation
|
||||||
|
|
||||||
def parse_matrices(infile: SourceFile) -> List[Tuple[Model, Dict]]:
|
# NOTE: Global variable used to keep track of solution models
|
||||||
next(infile) # Skip header line
|
|
||||||
|
|
||||||
solutions: List[Tuple[Model, Dict]] = []
|
solutions: List[Tuple[Model, Dict]] = []
|
||||||
|
|
||||||
|
def parse_matrices(infile: SourceFile) -> List[Tuple[Model, Dict]]:
|
||||||
|
global solutions
|
||||||
|
solutions = [] # Reset
|
||||||
|
header = parse_header(infile)
|
||||||
|
process_sizes(infile, header)
|
||||||
|
|
||||||
|
def process_sizes(infile: SourceFile, header: UglyHeader):
|
||||||
|
"""Stage 1"""
|
||||||
while True:
|
while True:
|
||||||
size = parse_size(infile)
|
size = parse_size(infile)
|
||||||
if size is None:
|
if size is None:
|
||||||
break
|
break
|
||||||
|
|
||||||
carrier_set = carrier_set_from_size(size)
|
carrier_set = carrier_set_from_size(size)
|
||||||
|
process_negations(infile, header, size, carrier_set)
|
||||||
|
|
||||||
|
def process_negations(infile: SourceFile, header: UglyHeader, size: int, carrier_set: Set[ModelValue]):
|
||||||
|
"""Stage 2 (Optional)"""
|
||||||
num_negation = 0
|
num_negation = 0
|
||||||
while True:
|
while True:
|
||||||
mnegation = parse_negation(infile, size)
|
mnegation = None
|
||||||
|
if header.negation:
|
||||||
|
mnegation = parse_single_negation(infile, size)
|
||||||
if mnegation is None:
|
if mnegation is None:
|
||||||
break
|
break
|
||||||
num_negation += 1
|
num_negation += 1
|
||||||
|
|
||||||
|
process_orders(infile, header, size, carrier_set, num_negation, mnegation)
|
||||||
|
|
||||||
|
if not header.negation:
|
||||||
|
break
|
||||||
|
|
||||||
|
def process_orders(infile: SourceFile, header: UglyHeader, size: int, carrier_set: Set[ModelValue], num_negation: int, mnegation: Optional[ModelFunction]):
|
||||||
|
"""Stage 3"""
|
||||||
num_order = 0
|
num_order = 0
|
||||||
while True:
|
while True:
|
||||||
result = parse_order(infile, size)
|
result = parse_single_order(infile, size)
|
||||||
if result is None:
|
if result is None:
|
||||||
break
|
break
|
||||||
mconjunction, mdisjunction = result
|
mconjunction, mdisjunction = result
|
||||||
num_order += 1
|
num_order += 1
|
||||||
|
process_designateds(infile, header, size, carrier_set, num_negation, mnegation, num_order, mconjunction, mdisjunction)
|
||||||
|
|
||||||
|
def process_designateds(infile: SourceFile, header: UglyHeader, size: int, carrier_set: Set[ModelValue], num_negation: int, mnegation: Optional[ModelFunction], num_order: int, mconjunction: Optional[ModelFunction], mdisjunction: Optional[ModelFunction]):
|
||||||
|
"""Stage 4"""
|
||||||
num_designated = 0
|
num_designated = 0
|
||||||
while True:
|
while True:
|
||||||
designated_values = parse_designated(infile, size)
|
designated_values = parse_single_designated(infile, size)
|
||||||
if designated_values is None:
|
if designated_values is None:
|
||||||
break
|
break
|
||||||
num_designated += 1
|
num_designated += 1
|
||||||
|
process_implications(infile, header, size, carrier_set, num_negation, mnegation, num_order, mconjunction, mdisjunction, num_designated, designated_values)
|
||||||
|
|
||||||
results = parse_implication(infile, size)
|
def process_implications(
|
||||||
if result is None:
|
infile: SourceFile, header: UglyHeader, size: int, carrier_set: Set[ModelValue], num_negation: int, mnegation: Optional[ModelFunction],
|
||||||
break
|
num_order: int, mconjunction: Optional[ModelFunction], mdisjunction: Optional[ModelFunction], num_designated: int, designated_values: Set[ModelValue]):
|
||||||
|
"""Stage 5"""
|
||||||
|
results = parse_implications(infile, size)
|
||||||
|
for num_implication, mimplication in enumerate(results, 1):
|
||||||
|
process_model(size, carrier_set, num_negation, mnegation, num_order, mconjunction, mdisjunction, num_designated, designated_values, num_implication, mimplication)
|
||||||
|
|
||||||
num_implication = 0
|
def process_model(
|
||||||
for mimplication in results:
|
size: int, carrier_set: Set[ModelValue], num_negation: int, mnegation: Optional[ModelFunction],
|
||||||
logical_operations = {
|
num_order: int, mconjunction: Optional[ModelFunction], mdisjunction: Optional[ModelFunction], num_designated: int,
|
||||||
mnegation, mimplication
|
designated_values: Set[ModelValue], num_implication: int, mimplication: ModelFunction):
|
||||||
}
|
"""Create Model"""
|
||||||
num_implication += 1
|
global solutions
|
||||||
model_name = f"{size}.{num_negation}.{num_order}.{num_designated}.{num_implication}"
|
|
||||||
|
logical_operations = { mimplication }
|
||||||
|
model_name = f"{size}{"." + str(num_negation) if num_negation != 0 else ""}.{num_order}.{num_designated}.{num_implication}"
|
||||||
model = Model(carrier_set, logical_operations, designated_values, name=model_name)
|
model = Model(carrier_set, logical_operations, designated_values, name=model_name)
|
||||||
interpretation = {
|
interpretation = {
|
||||||
Negation: mnegation,
|
|
||||||
Implication: mimplication
|
Implication: mimplication
|
||||||
}
|
}
|
||||||
|
if mnegation is not None:
|
||||||
|
logical_operations.add(mnegation)
|
||||||
|
interpretation[Negation] = mnegation
|
||||||
if mconjunction is not None:
|
if mconjunction is not None:
|
||||||
logical_operations.add(mconjunction)
|
logical_operations.add(mconjunction)
|
||||||
interpretation[Conjunction] = mconjunction
|
interpretation[Conjunction] = mconjunction
|
||||||
|
@ -87,7 +120,19 @@ def parse_matrices(infile: SourceFile) -> List[Tuple[Model, Dict]]:
|
||||||
solutions.append((model, interpretation))
|
solutions.append((model, interpretation))
|
||||||
print(f"Parsed Matrix {model.name}")
|
print(f"Parsed Matrix {model.name}")
|
||||||
|
|
||||||
return solutions
|
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(" ")
|
||||||
|
print(header_tokens)
|
||||||
|
assert header_tokens[0] in ["0", "1"]
|
||||||
|
assert header_tokens[6] in ["0", "1"]
|
||||||
|
negation_defined = bool(int(header_tokens[0]))
|
||||||
|
necessitation_defined = bool(int(header_tokens[6]))
|
||||||
|
return UglyHeader(negation_defined, necessitation_defined)
|
||||||
|
|
||||||
def carrier_set_from_size(size: int):
|
def carrier_set_from_size(size: int):
|
||||||
"""
|
"""
|
||||||
|
@ -108,7 +153,7 @@ def parse_size(infile: SourceFile) -> Optional[int]:
|
||||||
assert size > 0, f"Unexpected size at line {infile.current_line}"
|
assert size > 0, f"Unexpected size at line {infile.current_line}"
|
||||||
return size
|
return size
|
||||||
|
|
||||||
def parse_negation(infile: SourceFile, size: int) -> Optional[ModelFunction]:
|
def parse_single_negation(infile: SourceFile, size: int) -> Optional[ModelFunction]:
|
||||||
"""
|
"""
|
||||||
Parse the line representing the negation table.
|
Parse the line representing the negation table.
|
||||||
"""
|
"""
|
||||||
|
@ -189,7 +234,7 @@ def determine_dresult(size: int, ordering: Dict[ModelValue, ModelValue], a: Mode
|
||||||
if not invalid:
|
if not invalid:
|
||||||
return c
|
return c
|
||||||
|
|
||||||
def parse_order(infile: TextIO, size: int) -> Optional[Tuple[ModelFunction, ModelFunction]]:
|
def parse_single_order(infile: TextIO, size: int) -> Optional[Tuple[ModelFunction, ModelFunction]]:
|
||||||
"""
|
"""
|
||||||
Parse the line representing the ordering table
|
Parse the line representing the ordering table
|
||||||
"""
|
"""
|
||||||
|
@ -240,7 +285,7 @@ def parse_order(infile: TextIO, size: int) -> Optional[Tuple[ModelFunction, Mode
|
||||||
|
|
||||||
return mconjunction, mdisjunction
|
return mconjunction, mdisjunction
|
||||||
|
|
||||||
def parse_designated(infile: TextIO, size: int) -> Optional[Set[ModelValue]]:
|
def parse_single_designated(infile: TextIO, size: int) -> Optional[Set[ModelValue]]:
|
||||||
"""
|
"""
|
||||||
Parse the line representing which model values are designated.
|
Parse the line representing which model values are designated.
|
||||||
"""
|
"""
|
||||||
|
@ -261,14 +306,12 @@ def parse_designated(infile: TextIO, size: int) -> Optional[Set[ModelValue]]:
|
||||||
return designated_values
|
return designated_values
|
||||||
|
|
||||||
|
|
||||||
def parse_implication(infile: TextIO, size: int) -> Optional[List[ModelFunction]]:
|
def parse_implications(infile: TextIO, size: int) -> List[ModelFunction]:
|
||||||
"""
|
"""
|
||||||
Parse the line representing the list of implication
|
Parse the line representing the list of implication
|
||||||
tables.
|
tables.
|
||||||
"""
|
"""
|
||||||
line = next(infile).strip()
|
line = next(infile).strip()
|
||||||
if line == '-1':
|
|
||||||
return None
|
|
||||||
|
|
||||||
# Split and remove the last '-1' character
|
# Split and remove the last '-1' character
|
||||||
table = line.split(" ")[:-1]
|
table = line.split(" ")[:-1]
|
||||||
|
@ -301,7 +344,7 @@ if __name__ == "__main__":
|
||||||
parser = argparse.ArgumentParser(description="VSP Checker")
|
parser = argparse.ArgumentParser(description="VSP Checker")
|
||||||
parser.add_argument("--verbose", action='store_true', help="Print out all parsed matrices")
|
parser.add_argument("--verbose", action='store_true', help="Print out all parsed matrices")
|
||||||
args = vars(parser.parse_args())
|
args = vars(parser.parse_args())
|
||||||
solutions: List[Model] = parse_matrices(SourceFile(sys.stdin))
|
parse_matrices(SourceFile(sys.stdin))
|
||||||
print(f"Parsed {len(solutions)} matrices")
|
print(f"Parsed {len(solutions)} matrices")
|
||||||
for i, (model, interpretation) in enumerate(solutions):
|
for i, (model, interpretation) in enumerate(solutions):
|
||||||
vsp_result = has_vsp(model, interpretation)
|
vsp_result = has_vsp(model, interpretation)
|
||||||
|
|
Loading…
Reference in a new issue