yices2_bindings 0.2 · OCaml Package

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

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

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

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

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

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

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

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

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

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

val parse_bvbin : string -> Yices2_low.Types.term_t eh

val parse_bvhex : string -> Yices2_low.Types.term_t eh

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

package yices2_bindings