val pp_alpha_term : 'a Fmt.t -> 'a alpha_term Fmt.tThe 'a signed type represents possibly negated values of type 'a. It is used for bvnot at the leaves (Other and Ext below).
type 'a simple_term = 'a simple_term_aux alpha_termtype 'a abstract = 'a simple_term listextract size i j x extracts i..j from a composition of size size.
An element of size sz at the head of the composition contains the bits size - 1 .. size - sz inclusive.
zero_extract sz bv adds sz zeros to the front (high bits) of bv.
int2bv_const n z evaluates z as a constant n-bits bitvector.
If z is out of the 0 .. 2^n range, only the first n bits of z in binary representation are considered, i.e. int2bv_const n z is always equal to int2bv_const n (erem z (1 lsl n)).
module type ALIEN = sig ... end