Module `Bitvector`

Bit-vectors

author: Arjun Viswanathan

exception ComparingUnequalBVs
exception NonStandardBVSize

type t: Constant bitvector

val length_of_bitvector : t -> int: Return the length of a bitvector as a numeral

val repeat_bit : bool -> int -> t: Return bitvector resulting from repeating input bit b, (input) n times

val bvextract : int -> int -> t -> t: Return bits m down to n from the input bitvector

val bvsignext : int -> t -> t: Return input bitvector sign-extended to m bits

val bvconcat : t -> t -> t: Return input bitvectors concatenated together

val num_to_ubv8 : Numeral.t -> t: Return size 8 unsigned bitvector converted from a numeral

val num_to_ubv16 : Numeral.t -> t: Return size 16 unsigned bitvector converted from a numeral

val num_to_ubv32 : Numeral.t -> t: Return size 32 unsigned bitvector converted from a numeral

val num_to_ubv64 : Numeral.t -> t: Return size 64 unsigned bitvector converted from a numeral

val ubv_to_num : t -> Numeral.t: Return numeral converted from an unsigned bitvector

val ubv8_to_num : t -> Numeral.t: Return numeral converted from a size 8 unsigned bitvector

val ubv16_to_num : t -> Numeral.t: Return numeral converted from a size 16 unsigned bitvector

val ubv32_to_num : t -> Numeral.t: Return numeral converted from a size 32 unsigned bitvector

val ubv64_to_num : t -> Numeral.t: Return numeral converted from a size 64 unsigned bitvector

val num_to_bv8 : Numeral.t -> t: Return size 8 signed bitvector converted from a numeral

val num_to_bv16 : Numeral.t -> t: Return size 16 signed bitvector converted from a numeral

val num_to_bv32 : Numeral.t -> t: Return size 32 signed bitvector converted from a numeral

val num_to_bv64 : Numeral.t -> t: Return size 64 signed bitvector converted from a numeral

val bv_to_num : t -> Numeral.t: Return numeral converted from a signed bitvector

val bv8_to_num : t -> Numeral.t: Return numeral converted from a size 8 signed bitvector

val bv16_to_num : t -> Numeral.t: Return numeral converted from a size 16 signed bitvector

val bv32_to_num : t -> Numeral.t: Return numeral converted from a size 32 signed bitvector

val bv64_to_num : t -> Numeral.t: Return numeral converted from a size 64 signed bitvector

val sbv_add : t -> t -> t: Function that adds two signed bitvectors

val ubv_add : t -> t -> t: Function that adds two unsigned bitvectors

val sbv_mult : t -> t -> t: Function that multiplies two signed bitvectors

val ubv_mult : t -> t -> t: Function that multiplies two unsigned bitvectors

val sbv_div : t -> t -> t: Function that divides two signed bitvectors

val ubv_div : t -> t -> t: Function that divides two unsigned bitvectors

val sbv_rem : t -> t -> t: Function that finds remainder of two signed bitvectors

val ubv_rem : t -> t -> t: Function that finds remainder of two unsigned bitvectors

val sbv_sub : t -> t -> t: Function for signed bitvector subtraction

val sbv_neg : t -> t: Funciton for signed bitvector negation

val bv_and : t -> t -> t: Function that computes bitwise conjunction

val bv_or : t -> t -> t: Funciton that computes bitwise disjunction

val bv_not : t -> t: Function that computes bitwise negation

val equal : t -> t -> bool: Equality

val ult : t -> t -> bool: Unsigned lesser than

val ugt : t -> t -> bool: Unsigned greater than

val ulte : t -> t -> bool: Unsigned lesser than or equal to

val ugte : t -> t -> bool: Unsigned greater than or equal to

val lt : t -> t -> bool: Signed lesser than

val gt : t -> t -> bool: Signed greater than

val lte : t -> t -> bool: Signed lesser than or equal to

val gte : t -> t -> bool: Signed greater than or equal to

val bv_lsh : t -> t -> t: Shift bitvector left by n times, where n is specified as an unsigned BV

val bv_rsh : t -> t -> t: Shift bitvector right by n times, where n is specified as an unsigned BV

val bv_arsh : t -> t -> t: Arithmetic right shift of bitvector by n times, where n is specified as an unsigned BV

val pp_smtlib_print_bitvector_b : Stdlib.Format.formatter -> t -> unit: Pretty-print a constant bitvector in SMTLIB binary format

val pp_smtlib_print_bitvector_d : Stdlib.Format.formatter -> Numeral.t -> Numeral.t -> unit
val pp_yices_print_bitvector_b : Stdlib.Format.formatter -> t -> unit: Pretty-print a constant bitvector in Yices' binary format

val pp_yices_print_bitvector_d : Stdlib.Format.formatter -> Numeral.t -> Numeral.t -> unit: Pretty-print a constant bitvector in Yices' binary format given the decimal value and size

val pp_print_unsigned_machine_integer : Stdlib.Format.formatter -> t -> unit: Pretty-print a constant unsigned bitvector as a Lustre machine integer

val pp_print_signed_machine_integer : Stdlib.Format.formatter -> t -> unit: Pretty-print a constant signed bitvector as a Lustre machine integer

val pp_print_bitvector_x : Stdlib.Format.formatter -> t -> unit: Pretty-print a constant bitvector in hexadeciaml format

val bitvector_of_string : string -> t: Convert a string to a bitvector Binary and hexadecimal notation is accepted as #b01+ and #x0-9a-fA-F+ as in the SMTLIB standard

val bitvector_of_hstring : HString.t -> t: Convert a hashconsed string to a bitvector, store all converted values in a cache

val bool_of_hstring : HString.t -> bool: Convert a hashconsed string to a Boolean value

val (=) : t -> t -> bool: Equality

val (<) : t -> t -> bool: Signed lesser than

val (>) : t -> t -> bool: Signed greater than

val (<=) : t -> t -> bool: Signed lesser than or equal to

val (>=) : t -> t -> bool: Signed greater than or equal to

val first_bit : t -> bool: Return the first bit of input bitvector b