Module SMT.Bitvector

include SMT_sig.EQUALITY with type t := t
val mk_eq : t list -> t
val mk_distinct : t list -> t
val mk_sort : int -> Sort.t
val mk_var : string -> Sort.t -> t
val mk_fresh_var : string -> Sort.t -> t
val mk_const : Bitvector.t -> t
val mk_const_of_int : int -> int -> t
val mk_const_of_string : string -> t
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_plus : int -> t list -> t
val mk_not : t -> t
val mk_and : int -> t list -> t
val mk_or : int -> t list -> t
val mk_xor : int -> t list -> t
val mk_implies : t -> t -> t
val mk_neg : t -> t

Two's complement, i.e. unary minus.

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
val get_width : t -> int

Printing

val to_bit_string : t -> string