yices2_bindings 0.1 · OCaml Package

type t = Yices2_low.Types.term_t

val equal : t -> t -> Ppx_deriving_runtime.bool

val compare : t -> t -> Ppx_deriving_runtime.int

val hash : t -> int

val true0 : unit -> Yices2_low.Types.term_t EH.t

val false0 : unit -> Yices2_low.Types.term_t EH.t

val constant : 
  Yices2_low.Types.type_t ->
  id:int ->
  Yices2_low.Types.term_t EH.t

val new_uninterpreted : 
  ?name:string ->
  Yices2_low.Types.type_t ->
  Yices2_low.Types.term_t EH.t

val new_variable : Yices2_low.Types.type_t -> Yices2_low.Types.term_t EH.t

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

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

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

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

val (===) : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

val (=/=) : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

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

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

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

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

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

val (!|) : Yices2_low.Types.term_t list -> Yices2_low.Types.term_t EH.t

val (!&) : Yices2_low.Types.term_t list -> Yices2_low.Types.term_t EH.t

val (!^) : Yices2_low.Types.term_t list -> Yices2_low.Types.term_t EH.t

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

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

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

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

val (&&&) : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

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

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

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

val (<=>) : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

val (==>) : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

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

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

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

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

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

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

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

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

module Arith : sig ... end

module BV : sig ... end

val subst_term : 
  (Yices2_low.Types.term_t * Yices2_low.Types.term_t) list ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

val subst_terms : 
  (Yices2_low.Types.term_t * Yices2_low.Types.term_t) list ->
  Yices2_low.Types.term_t list ->
  Yices2_low.Types.term_t list EH.t

val type_of_term : Yices2_low.Types.term_t -> Yices2_low.Types.type_t EH.t

val is_bool : Yices2_low.Types.term_t -> bool EH.t

val is_int : Yices2_low.Types.term_t -> bool EH.t

val is_real : Yices2_low.Types.term_t -> bool EH.t

val is_arithmetic : Yices2_low.Types.term_t -> bool EH.t

val is_bitvector : Yices2_low.Types.term_t -> bool EH.t

val is_tuple : Yices2_low.Types.term_t -> bool EH.t

val is_function : Yices2_low.Types.term_t -> bool EH.t

val is_scalar : Yices2_low.Types.term_t -> bool EH.t

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

val is_ground : Yices2_low.Types.term_t -> bool EH.t

val is_atomic : Yices2_low.Types.term_t -> bool EH.t

val is_composite : Yices2_low.Types.term_t -> bool EH.t

val is_projection : Yices2_low.Types.term_t -> bool EH.t

val is_sum : Yices2_low.Types.term_t -> bool EH.t

val is_bvsum : Yices2_low.Types.term_t -> bool EH.t

val is_product : Yices2_low.Types.term_t -> bool EH.t

val reveal : Yices2_low.Types.term_t -> Yices2_high_types.Types.yterm EH.t

val build : 
  'a Yices2_high_types.Types.termstruct ->
  Yices2_low.Types.term_t EH.t

val map : 
  (Yices2_low.Types.term_t -> Yices2_low.Types.term_t EH.t) ->
  'a Yices2_high_types.Types.termstruct ->
  'a Yices2_high_types.Types.termstruct EH.t

val constructor : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_constructor EH.t

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

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

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

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

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

val bool_const_value : Yices2_low.Types.term_t -> bool EH.t

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

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

val rational_const_value : Yices2_low.Types.term_t -> Q.t EH.t

val sum_component : 
  Yices2_low.Types.term_t ->
  int ->
  (Q.t * Yices2_low.Types.term_t option) EH.t

val bvsum_component : 
  Yices2_low.Types.term_t ->
  int ->
  (bool list * Yices2_low.Types.term_t option) EH.t

val product_component : 
  Yices2_low.Types.term_t ->
  int ->
  (Yices2_low.Types.term_t * Unsigned.uint) EH.t

module Names : sig ... end

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

package yices2_bindings