yices2_bindings 0.2 · OCaml Package

val bvconst_int : width:int -> int -> Yices2_low.Types.term_t EH.t

val bvconst_uint32 : width:int -> Unsigned.uint -> Yices2_low.Types.term_t EH.t

val bvconst_uint64 : 
  width:int ->
  Unsigned.ulong ->
  Yices2_low.Types.term_t EH.t

val bvconst_int32 : width:int -> Signed.sint -> Yices2_low.Types.term_t EH.t

val bvconst_int64 : width:int -> Signed.long -> Yices2_low.Types.term_t EH.t

val bvconst_mpz : width:int -> Z.t -> Yices2_low.Types.term_t EH.t

val bvconst_zero : width:int -> Yices2_low.Types.term_t EH.t

val bvconst_one : width:int -> Yices2_low.Types.term_t EH.t

val bvconst_minus_one : width:int -> Yices2_low.Types.term_t EH.t

val bvconst_from_list : bool list -> Yices2_low.Types.term_t EH.t

val parse_bvbin : string -> Yices2_low.Types.term_t EH.t

val parse_bvhex : string -> Yices2_low.Types.term_t EH.t

val bvadd : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

val bvsub : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

val bvneg : Yices2_low.Types.term_t -> Yices2_low.Types.term_t EH.t

val bvmul : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

val bvsquare : Yices2_low.Types.term_t -> Yices2_low.Types.term_t EH.t

val bvpower : Yices2_low.Types.term_t -> int -> Yices2_low.Types.term_t EH.t

val bvdiv : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

val bvrem : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

val bvsdiv : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

val bvsrem : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

val bvsmod : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

val bvnot : Yices2_low.Types.term_t -> Yices2_low.Types.term_t EH.t

val bvnand : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

val bvnor : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

val bvxnor : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

val bvshl : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

val bvlshr : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

val bvashr : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

val bvand : Yices2_low.Types.term_t list -> Yices2_low.Types.term_t EH.t

val bvor : Yices2_low.Types.term_t list -> Yices2_low.Types.term_t EH.t

val bvxor : Yices2_low.Types.term_t list -> Yices2_low.Types.term_t EH.t

val bvsum : Yices2_low.Types.term_t list -> Yices2_low.Types.term_t EH.t

val bvproduct : Yices2_low.Types.term_t list -> Yices2_low.Types.term_t EH.t

val shift_left0 : 
  Yices2_low.Types.term_t ->
  int ->
  Yices2_low.Types.term_t EH.t

val shift_left1 : 
  Yices2_low.Types.term_t ->
  int ->
  Yices2_low.Types.term_t EH.t

val shift_right0 : 
  Yices2_low.Types.term_t ->
  int ->
  Yices2_low.Types.term_t EH.t

val shift_right1 : 
  Yices2_low.Types.term_t ->
  int ->
  Yices2_low.Types.term_t EH.t

val ashift_right : 
  Yices2_low.Types.term_t ->
  int ->
  Yices2_low.Types.term_t EH.t

val rotate_left : 
  Yices2_low.Types.term_t ->
  int ->
  Yices2_low.Types.term_t EH.t

val rotate_right : 
  Yices2_low.Types.term_t ->
  int ->
  Yices2_low.Types.term_t EH.t

val bvextract : 
  Yices2_low.Types.term_t ->
  int ->
  int ->
  Yices2_low.Types.term_t EH.t

val bvconcat2 : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

val bvconcat : Yices2_low.Types.term_t list -> Yices2_low.Types.term_t EH.t

val bvrepeat : Yices2_low.Types.term_t -> int -> Yices2_low.Types.term_t EH.t

val sign_extend : 
  Yices2_low.Types.term_t ->
  int ->
  Yices2_low.Types.term_t EH.t

val zero_extend : 
  Yices2_low.Types.term_t ->
  int ->
  Yices2_low.Types.term_t EH.t

val redand : Yices2_low.Types.term_t -> Yices2_low.Types.term_t EH.t

val redor : Yices2_low.Types.term_t -> Yices2_low.Types.term_t EH.t

val redcomp : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

val bvarray : Yices2_low.Types.term_t list -> Yices2_low.Types.term_t EH.t

val bitextract : Yices2_low.Types.term_t -> int -> Yices2_low.Types.term_t EH.t

val bveq : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

val bvneq : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

val bvge : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

val bvgt : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

val bvle : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

val bvlt : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

val bvsge : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

val bvsgt : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

val bvsle : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

val bvslt : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

package yices2_bindings