diff --git a/README.md b/README.md index 3dd895f..0c12b56 100644 --- a/README.md +++ b/README.md @@ -1,16 +1,12 @@ -# Matmod: Verify Relevance Properties for Matrix Models with Implicative Connectives +# Matmod: Matrix Model Generator for Implicative Connectives -Interested in seeing which satisfiable models from [arranstewart/magic](https://github.com/arranstewart/magic) have the variable sharing property? +This repository is mostly an experiment to help +me better understand matrix models. -(1) Generate satisfiable matrix models using `magic`. - - 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 +You're likely better off using [arranstewart/magic](https://github.com/arranstewart/magic). -(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. +We support output from magic using the ugly data format. ``` python3 parse_magic.py < UGLY_FILE_FROM_MAGIC ``` - -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. - diff --git a/parse_magic.py b/parse_magic.py index 7cc1fe0..5c7b746 100644 --- a/parse_magic.py +++ b/parse_magic.py @@ -80,8 +80,9 @@ def carrier_set_from_size(size: int): def parse_size(infile: TextIO) -> Optional[int]: """ Parse the line representing the matrix size. + NOTE: Elements are represented in hexidecimal. """ - size = int(next(infile)) + size = int(next(infile), 16) if size == -1: return None assert size > 0, "Unexpected size" @@ -109,16 +110,16 @@ def parse_negation(infile: TextIO, size: int) -> Optional[ModelFunction]: def mvalue_from_index(i: int): """ - Given an index, return the + Given an index, return the hexidecimal representation of the model value. """ - return ModelValue(f"a{i}") + return ModelValue(f"a{hex(i)[-1]}") def parse_mvalue(x: str) -> ModelValue: """ Parse an element and return the model value. """ - return mvalue_from_index(int(x)) + return mvalue_from_index(int(x, 16)) def determine_cresult(size: int, ordering: Dict[ModelValue, ModelValue], a: ModelValue, b: ModelValue) -> ModelValue: """