yices2_bindings 0.1 · OCaml Package

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

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

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

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

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

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

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

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

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

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

val parse_bvbin : string -> Yices2_low.Types.term_t

val parse_bvhex : string -> Yices2_low.Types.term_t

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

package yices2_bindings