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.
Juxtaposition of terms, used to annotate terms with their type.
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, ...".
Record access for the field given by the identifier.
Create a projection for the given field of an adt constructor.
Create a term to "check" a formula. TODO: ask @iguernlala about this.
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.