package yices2

  1. Overview
  2. Docs

Module Term.Bitvector

Bit-vectors

val of_int : int -> int -> term
val of_int32 : int -> int32 -> term
val of_int64 : int -> int64 -> term
val of_nativeint : int -> nativeint -> term
val of_bools : bool array -> term
val of_terms : term array -> term
val of_bin : string -> term
val of_hex : string -> term
val of_z : int -> Z.t -> term
val zero : int -> term
val one : int -> term
val minus_one : int -> term
val add : term -> term -> term
val sub : term -> term -> term
val neg : term -> term
val mul : term -> term -> term
val square : term -> term
val power : term -> int -> term
val power_int64 : term -> int64 -> term
val div : term -> term -> term
val rem : term -> term -> term
val sdiv : term -> term -> term
val srem : term -> term -> term
val smod : term -> term -> term
val not : term -> term
val and_ : term -> term -> term
val or_ : term -> term -> term
val xor : term -> term -> term
val nand : term -> term -> term
val nor : term -> term -> term
val xnor : term -> term -> term
val shl : term -> term -> term
val lshr : term -> term -> term
val ashr : term -> term -> term
val shift_left0 : term -> int -> term
val shift_left1 : term -> int -> term
val shift_right0 : term -> int -> term
val shift_right1 : term -> int -> term
val ashift_right : term -> int -> term
val rotate_left : term -> int -> term
val rotate_right : term -> int -> term
val extract : term -> int -> int -> term
val concat : term -> term -> term
val repeat : term -> int -> term
val sign_extend : term -> int -> term
val zero_extend : term -> int -> term
val redand : term -> term
val redor : term -> term
val redcomp : term -> term -> term
val bitextract : term -> int -> term
val eq : term -> term -> term
val neq : term -> term -> term
val ge : term -> term -> term
val gt : term -> term -> term
val le : term -> term -> term
val lt : term -> term -> term
val sge : term -> term -> term
val sgt : term -> term -> term
val sle : term -> term -> term
val slt : term -> term -> term