# 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
```