yices2_bindings 0.2 · 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

val false0 : unit -> Yices2_low.Types.term_t

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

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

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

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

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

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

val neq : 
  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 not1 : Yices2_low.Types.term_t -> Yices2_low.Types.term_t

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

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

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

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

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

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

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

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

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

val xor2 : 
  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 (***) : 
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t

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

val implies : 
  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 tuple : Yices2_low.Types.term_t list -> Yices2_low.Types.term_t

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

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

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

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

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

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

val lambda : 
  Yices2_low.Types.term_t list ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_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

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

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

val is_bool : Yices2_low.Types.term_t -> bool

val is_int : Yices2_low.Types.term_t -> bool

val is_real : Yices2_low.Types.term_t -> bool

val is_arithmetic : Yices2_low.Types.term_t -> bool

val is_bitvector : Yices2_low.Types.term_t -> bool

val is_tuple : Yices2_low.Types.term_t -> bool

val is_function : Yices2_low.Types.term_t -> bool

val is_scalar : Yices2_low.Types.term_t -> bool

val bitsize : Yices2_low.Types.term_t -> int

val is_ground : Yices2_low.Types.term_t -> bool

val is_atomic : Yices2_low.Types.term_t -> bool

val is_composite : Yices2_low.Types.term_t -> bool

val is_projection : Yices2_low.Types.term_t -> bool

val is_sum : Yices2_low.Types.term_t -> bool

val is_bvsum : Yices2_low.Types.term_t -> bool

val is_product : Yices2_low.Types.term_t -> bool

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

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

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

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

val num_children : Yices2_low.Types.term_t -> int

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

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

val proj_index : Yices2_low.Types.term_t -> int

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

val bool_const_value : Yices2_low.Types.term_t -> bool

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

val scalar_const_value : Yices2_low.Types.term_t -> int

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

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

val bvsum_component : 
  Yices2_low.Types.term_t ->
  int ->
  bool list * Yices2_low.Types.term_t option

val product_component : 
  Yices2_low.Types.term_t ->
  int ->
  Yices2_low.Types.term_t * Unsigned.uint

module Names : sig ... end

val parse : string -> Yices2_low.Types.term_t

val pph : int -> t Containers.Format.printer

val pp : t Containers.Format.printer

val to_sexp : t -> Sexplib.Type.t

package yices2_bindings