yices2_bindings 0.1 · OCaml Package

val zero : unit -> Yices2_low.Types.term_t

val int : int -> Yices2_low.Types.term_t

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

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

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

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

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

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

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

val parse_rational : string -> Yices2_low.Types.term_t

val parse_float : string -> Yices2_low.Types.term_t

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

package yices2_bindings