mirror of
https://github.com/Brandon-Rozek/matmod.git
synced 2024-11-20 21:56:29 -05:00
Updated interface
This commit is contained in:
parent
8628107704
commit
f057ba64fc
3 changed files with 39 additions and 26 deletions
|
@ -2,15 +2,15 @@
|
||||||
|
|
||||||
Interested in seeing which satisfiable models from [arranstewart/magic](https://github.com/arranstewart/magic) have the variable sharing property?
|
Interested in seeing which satisfiable models from [arranstewart/magic](https://github.com/arranstewart/magic) have the variable sharing property?
|
||||||
|
|
||||||
(1) Generate satisfiable matrix models using `magic`.
|
(1) Generate satisfiable matrix models using `MaGIC`.
|
||||||
- Use the `ugly` data format as the output
|
- Use the `ugly` data format as the output
|
||||||
- Keep in mind not all logic features in magic are supported, check out the [GitHub issue tracker](https://github.com/Brandon-Rozek/matmod/issues) to see upcoming features or make your own requests
|
|
||||||
|
|
||||||
(2) Run our tool! It will first attempt to parse all the matrices in the output file and then check for the variable sharing property one-by-one.
|
(2) Run our tool! It will first attempt to parse all the matrices in the output file and then check for the variable sharing property one-by-one.
|
||||||
|
|
||||||
```
|
```
|
||||||
python3 parse_magic.py < examples/R6
|
./vspursuer.py -i examples/R6
|
||||||
```
|
```
|
||||||
|
|
||||||
If you face any troubles, feel free to reach out. This tool also has capabilities to generate satisfiable models given a specification (see: R.py), however, it is much slower than magic so you're better off using that.
|
If you face any troubles, feel free to reach out. This tool also is able to generate satisfiable models given a specification (see: R.py). This is, however, much slower than MaGIC so you're better off using that.
|
||||||
|
|
||||||
|
Check out the [GitHub issue tracker](https://github.com/Brandon-Rozek/matmod/issues) to see upcoming features or make your own requests.
|
||||||
|
|
|
@ -3,9 +3,7 @@ Parses the Magic Ugly Data File Format
|
||||||
|
|
||||||
Assumes the base logic is R with no extra connectives
|
Assumes the base logic is R with no extra connectives
|
||||||
"""
|
"""
|
||||||
import argparse
|
|
||||||
import re
|
import re
|
||||||
import sys
|
|
||||||
from typing import TextIO, List, Optional, Tuple, Set, Dict
|
from typing import TextIO, List, Optional, Tuple, Set, Dict
|
||||||
|
|
||||||
from model import Model, ModelValue, ModelFunction
|
from model import Model, ModelValue, ModelFunction
|
||||||
|
@ -17,7 +15,6 @@ from logic import (
|
||||||
Disjunction,
|
Disjunction,
|
||||||
Operation
|
Operation
|
||||||
)
|
)
|
||||||
from vsp import has_vsp
|
|
||||||
|
|
||||||
class SourceFile:
|
class SourceFile:
|
||||||
def __init__(self, fileobj: TextIO):
|
def __init__(self, fileobj: TextIO):
|
||||||
|
@ -594,22 +591,3 @@ def parse_single_dyadic_connective(infile: SourceFile, symbol: str, size: int) -
|
||||||
mapping[(x, y)] = r
|
mapping[(x, y)] = r
|
||||||
|
|
||||||
return ModelFunction(2, mapping, symbol)
|
return ModelFunction(2, mapping, symbol)
|
||||||
|
|
||||||
|
|
||||||
if __name__ == "__main__":
|
|
||||||
parser = argparse.ArgumentParser(description="VSP Checker")
|
|
||||||
parser.add_argument("--verbose", action='store_true', help="Print out all parsed matrices")
|
|
||||||
args = vars(parser.parse_args())
|
|
||||||
solutions = parse_matrices(SourceFile(sys.stdin))
|
|
||||||
print(f"Parsed {len(solutions)} matrices")
|
|
||||||
num_has_vsp = 0
|
|
||||||
for i, (model, interpretation) in enumerate(solutions):
|
|
||||||
vsp_result = has_vsp(model, interpretation)
|
|
||||||
print(vsp_result)
|
|
||||||
|
|
||||||
if args['verbose'] or vsp_result.has_vsp:
|
|
||||||
print(model)
|
|
||||||
|
|
||||||
if vsp_result.has_vsp:
|
|
||||||
num_has_vsp += 1
|
|
||||||
print(f"Tested {len(solutions)} models, {num_has_vsp} of which satisfy VSP")
|
|
||||||
|
|
35
vspursuer.py
Executable file
35
vspursuer.py
Executable file
|
@ -0,0 +1,35 @@
|
||||||
|
#!/usr/bin/env python3
|
||||||
|
import argparse
|
||||||
|
from parse_magic import (
|
||||||
|
SourceFile,
|
||||||
|
parse_matrices
|
||||||
|
)
|
||||||
|
from vsp import has_vsp
|
||||||
|
|
||||||
|
if __name__ == "__main__":
|
||||||
|
parser = argparse.ArgumentParser(description="VSP Checker")
|
||||||
|
parser.add_argument("--verbose", action='store_true', help="Print out all parsed matrices")
|
||||||
|
parser.add_argument("-i", type=str, help="Path to MaGIC ugly data file")
|
||||||
|
args = vars(parser.parse_args())
|
||||||
|
|
||||||
|
data_file_path = args.get("i")
|
||||||
|
if data_file_path is None:
|
||||||
|
data_file_path = input("Path to MaGIC Ugly Data File: ")
|
||||||
|
|
||||||
|
solutions = []
|
||||||
|
with open(data_file_path, "r") as data_file:
|
||||||
|
solutions = parse_matrices(SourceFile(data_file))
|
||||||
|
print(f"Parsed {len(solutions)} matrices")
|
||||||
|
|
||||||
|
num_has_vsp = 0
|
||||||
|
for i, (model, interpretation) in enumerate(solutions):
|
||||||
|
vsp_result = has_vsp(model, interpretation)
|
||||||
|
print(vsp_result)
|
||||||
|
|
||||||
|
if args['verbose'] or vsp_result.has_vsp:
|
||||||
|
print(model)
|
||||||
|
|
||||||
|
if vsp_result.has_vsp:
|
||||||
|
num_has_vsp += 1
|
||||||
|
|
||||||
|
print(f"Tested {len(solutions)} models, {num_has_vsp} of which satisfy VSP")
|
Loading…
Reference in a new issue