Module Expr.BV

Constructors from the smtlib theory of fixed-size bit-vectors and the QF_BV logic.

https://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml https://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV

val of_Z : size:int -> Z.t -> t
val int2bv : int -> t -> t
val bv2nat : t -> t
val bvzero : int -> t
val bvones : int -> t
val concat : t -> t -> t
val extract : int -> int -> t -> t
val repeat : int -> t -> t
val zero_extend : int -> t -> t
val sign_extend : int -> t -> t
val rotate_left : int -> t -> t
val rotate_right : int -> t -> t
val bvnot : t -> t
val bvand : t -> t -> t
val bvor : t -> t -> t
val bvnand : t -> t -> t
val bvnor : t -> t -> t
val bvxor : t -> t -> t
val bvxnor : t -> t -> t
val bvcomp : t -> t -> t
val bvneg : t -> t
val bvadd : t -> t -> t
val bvsub : t -> t -> t
val bvmul : t -> t -> t
val bvudiv : t -> t -> t
val bvurem : t -> t -> t
val bvsdiv : t -> t -> t
val bvsrem : t -> t -> t
val bvsmod : t -> t -> t
val bvult : t -> t -> t
val bvule : t -> t -> t
val bvugt : t -> t -> t
val bvuge : t -> t -> t
val bvslt : t -> t -> t
val bvsle : t -> t -> t
val bvsgt : t -> t -> t
val bvsge : t -> t -> t
val bvshl : t -> t -> t
val bvlshr : t -> t -> t
val bvashr : t -> t -> t