yices2_bindings 0.2 · OCaml Package

val zero : unit -> Yices2_low.Types.term_t eh

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

val int32 : Signed.sint -> Yices2_low.Types.term_t eh

val int64 : Signed.long -> Yices2_low.Types.term_t eh

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

val rational32 : Signed.sint -> Unsigned.uint -> Yices2_low.Types.term_t eh

val rational64 : Signed.long -> Unsigned.ulong -> Yices2_low.Types.term_t eh

val mpz : Z.t -> Yices2_low.Types.term_t eh

val mpq : Q.t -> Yices2_low.Types.term_t eh

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

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

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

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

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

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

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

val power32 : 
  Yices2_low.Types.term_t ->
  Unsigned.uint ->
  Yices2_low.Types.term_t eh

val (++) : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t eh

val (--) : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t eh

val (!-) : Yices2_low.Types.term_t -> Yices2_low.Types.term_t eh

val (**) : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t eh

val (^^) : Yices2_low.Types.term_t -> int -> Yices2_low.Types.term_t eh

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

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

val (!+) : Yices2_low.Types.term_t list -> Yices2_low.Types.term_t eh

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

val (!*) : Yices2_low.Types.term_t list -> Yices2_low.Types.term_t eh

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

val (//) : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t eh

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

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

val (/.) : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t eh

val (%.) : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t eh

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

val (||.) : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t eh

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

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

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

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

val poly_int : 
  (int * Yices2_low.Types.term_t) list ->
  Yices2_low.Types.term_t eh

val poly_int32 : 
  (Signed.sint * Yices2_low.Types.term_t) list ->
  Yices2_low.Types.term_t eh

val poly_int64 : 
  (Signed.long * Yices2_low.Types.term_t) list ->
  Yices2_low.Types.term_t eh

val poly_rational : 
  (int * int * Yices2_low.Types.term_t) list ->
  Yices2_low.Types.term_t eh

val poly_rational32 : 
  (Signed.sint * Unsigned.uint * Yices2_low.Types.term_t) list ->
  Yices2_low.Types.term_t eh

val poly_rational64 : 
  (Signed.long * Unsigned.ulong * Yices2_low.Types.term_t) list ->
  Yices2_low.Types.term_t eh

val poly_mpz : 
  (Z.t * Yices2_low.Types.term_t) list ->
  Yices2_low.Types.term_t eh

val poly_mpq : 
  (Q.t * Yices2_low.Types.term_t) list ->
  Yices2_low.Types.term_t eh

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

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

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

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

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

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

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

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

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

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

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

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

package yices2_bindings