# isla-cat 🱠isla-cat is a Rust library for converting the cat files used by [herd](https://github.com/herd/herdtools7) to describe hardware relaxed memory models into a form suitable for use with SMT solvers such as Z3 and CVC4. It also contains a small binary `cat2smt` which translates such cat files on the command line. Documentation for the cat language can be found [here](http://diy.inria.fr/doc/herd.html). # Licensing The `.cat` files in the catlib subdirectory are licensed under the CeCILL-B license [from herd](https://github.com/herd/herdtools7/blob/master/LICENSE.txt). The `.cat` files in the tests directory are likewise licensed under the CeCILL-B license, except `aarch64.cat` which is under a 3-clause BSD license from ARM Ltd. # Limitations cat has some features which are not easy (or even possible at all) to translate into SMT. Roughly-speaking, this supports the fragment of cat that defines sets and relations over events. More formally the fragment of cat we support is defined by the grammar: ``` expr ::= 0 | id | expr? | expr^-1 | ~expr | [expr] | expr | expr | expr ; expr | expr \ expr | expr & expr | expr * expr | expr expr | let id = expr in expr | ( expr ) binding ::= id = expr closure_binding ::= id = expr^+ | id = expr^* id ::= [a-zA-Z_][0-9a-z_.-]* def ::= let binding { and binding } | let closure_binding | let funbinding | include string | show expr as id | show id {, id } | unshow id {, id } | [ flag ] check expr [ as id ] funbinding ::= id ( id ) = expr check ::= checkname | ~checkname checkname ::= acyclic | irreflexive | empty ```