Module BaseLogic.Bitvector

include module type of struct include Equality end
val mk_eq : Self.t Stdlib.List.t -> t
val mk_distinct : t Stdlib.List.t -> t
val mk_eq2 : Self.t -> Self.t -> t
val mk_distinct2 : t -> t -> t
include module type of struct include DefaultVars end
val mk_var : string -> Variable.Sort.t -> t
val mk_fresh_var : string -> Variable.Sort.t -> t
val mk_sort : int -> Sort.t
val mk_const : Bitvector.t -> t
val mk_const_of_int : int -> int -> t
val mk_const_of_string : string -> t
val get_width : t -> int
val mk_zero : int -> t
val mk_one : int -> t
val mk_full_zeros : int -> t
val mk_full_ones : int -> t
val mk_bit_check : t -> t -> t
val mk_not : t -> t
val mk_plus : Stdlib.Int.t -> Self.t Stdlib.List.t -> Self.t
val mk_mult : Stdlib.Int.t -> Self.t Stdlib.List.t -> Self.t
val mk_neg : t -> t
val mk_minus : Self.t -> t -> Self.t
val mk_and : Stdlib.Int.t -> Self.t Stdlib.List.t -> Self.t
val mk_or : Stdlib.Int.t -> Self.t Stdlib.List.t -> Self.t
val mk_xor : Stdlib.Int.t -> t Stdlib.List.t -> t
val mk_implies : t -> t -> t
val mk_shift_left : t -> t -> t
val mk_shift_right : t -> t -> t
val mk_lesser : t -> t -> t
val mk_lesser_eq : t -> t -> t

Casts

val mk_extraction : left:Stdlib.Int.t -> right:Stdlib.Int.t -> t -> t
val mk_zero_extension : Stdlib.Int.t -> t -> t
val mk_sign_extension : Stdlib.Int.t -> t -> t