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.
| Sexp | The SMTLIB2 format uses Lisp-style S-expressions. Here we
represent only the subset of S-expressions required to represent
the relational expressions used by the cat language.
|
| compile_cat | Compile all the definitions in a cat model.
|
| compile_rel | compile_rel(R, ev1, ev2) compiles the given expression in a
Bool-typed S-expression representing (ev1,ev2)∈R. Returns
None if the expression R does not denote a valid relation.
|
| compile_set | compile_set(S, ev) compiles the given expression into a
Bool-kinded S-expression representing ev∈S. Returns None if
the expression S does not denote a valid set.
|
| compile_toplevel | compile_toplevel compiles a toplevel expression into either a
set or relation depending on its type. The event names are
implicitly ev1 and ev2 for relations and ev1 for sets, which
is why it is only valid at the toplevel.
|
| EventId | Event ids are u32 variables denoted in the generated SMTLIB as
evX where X is a number greater than 0. The arguments to
toplevel relations and sets are always ev1 and ev2.
|