Crate isla_cat[][src]

This crate implements a library for compiling cat files as used by herdtools7 into SMTLIB defintions that can be used by an SMT solver such as z3.

There are some restrictions on the cat files we can support - roughly speaking, we support the subset of cat that defines relations and sets over events which is easily translated into first-order SMT definitions.

Modules

cat

Provides the top-level interface for interacting with cats. 🐱

smt

This module implements the compilation from the high-order relation-algebra style expressions used by cat into first-order SMT definitions, where relations are represented as functions from Event × Event → Bool and sets are Event → Bool functions.