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 int_to_bv : int -> t -> t
val ubv_to_int : t -> t
val sbv_to_int : 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
val bvuaddo : t -> t -> t
val bvsaddo : t -> t -> t
val bvnego : t -> t
val bvusubo : t -> t -> t
val bvssubo : t -> t -> t
val bvumulo : t -> t -> t
val bvsmulo : t -> t -> t
val bvsdivo : t -> t -> t