Bitvector (kind2dev@731decdf5fb1.Bitvector)

exception ComparingUnequalBVs

exception NonStandardBVSize

type t

Constant bitvector

val length_of_bitvector : t -> int

Return the length of a bitvector as a numeral

val zero : int -> t

Bit-vector representing decimal 0

val one : int -> t

Bit-vector representing decimal 1

val f : int -> t

Bit-vector representing hexadecimal F - all bit's are 1

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 bvzeroext : int -> t -> t

Extend input bitvector by concatenating m zero bits

val bvconcat : t -> t -> t

Return input bitvectors concatenated together

Numeral to Unsigned Bitvector

author Arjun Viswanathan

val num_to_ubv : Numeral.t -> Numeral.t -> t

num_to_ubv s n returns size s unsigned bitvector converted from numeral n

Usigned Bitvector to Numeral

author Arjun Viswanathan

val ubv_to_num : t -> Numeral.t

Return numeral converted from an unsigned bitvector

Numeral to Signed Bitvector

author Arjun Viswanathan

val num_to_bv : Numeral.t -> Numeral.t -> t

Return signed bitvector converted from a numeral

Signed Bitvector to Numeral

author Arjun Viswanathan

val bv_to_num : t -> Numeral.t

Return numeral converted from a signed bitvector

Arithmetic Operations

author Arjun Viswanathan

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

Logical Operations

author Arjun Viswanathan

val bv_and : t -> t -> t

Function that computes bitwise conjunction

val bv_or : t -> t -> t

Function that computes bitwise disjunction

val bv_xor : t -> t -> t

Function that computes bitwise exclusive disjunction

val bv_not : t -> t

Function that computes bitwise negation

Comparison Operators

author Arjun Viswanathan

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

Shift Operators

author Arjun Viswanathan

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

Pretty Printing

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 -> t -> unit

Pretty-print a bitvector in SMTLIB extended decimal format

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

Conversions

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

Infix Comparison Operators

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

Unused Functions

val first_bit : t -> bool

Return the first bit of input bitvector b