Bitvoector extraction. TODO: document meaning of the itnegers indexes.
Constants, i.e non predefined symbols. This includes both constants defined by theories, defined locally in a problem, and also quantified variables.
Pattern matching. The first term is the term to match, and each tuple in the list is a match case, which is a pair of a pattern and a match branch.
Create a record expression, with a list of equalities of the form "label = expr".
Record update, of the form "s with
label = expr, ...".
Create a projection for the given field of an adt constructor.
Create a trigger for the given term/variable being inside of a given interval, which is given as a lower bound, and an upper bound. Each bound contains an expression for the bound value, as well as a boolean indicating whether the bound is strict or not.
Annotate a term (generally a quantified formula), with a list of triggers.
Annotate a term (genrally a quantified formula) with a list of filters.