yices2_bindings 0.1 · OCaml Package

module Types : sig ... end

val uint_t : Types.uint_t Ctypes.typ

val sint_t : Types.sint_t Ctypes.typ

val unit_t : Types.unit_t Ctypes.typ

val bool_t : Types.bool_t Ctypes.typ

val term_t : Types.term_t Ctypes.typ

val type_t : Types.type_t Ctypes.typ

val null_term : Types.term_t

val null_type : Types.type_t

val smt_status_t : Types.smt_status_t Ctypes.typ

val term_constructor_t : Types.term_constructor_t Ctypes.typ

val yices_gen_mode_t : Types.yices_gen_mode_t Ctypes.typ

val error_code_t : Types.error_code_t Ctypes.typ

module Conv : sig ... end

val context_t : Types.context_t Ctypes.typ

val model_t : Types.model_t Ctypes.typ

val ctx_config_t : Types.ctx_config_t Ctypes.typ

val param_t : Types.param_t Ctypes.typ

val term_vector_s : 
  < ctype : Types.term_vector_t Ctypes.typ
  ; members : 
    < capacity : (Unsigned.uint, Types.term_vector_t) Ctypes.field
    ; data : (Types.term_t Ctypes.ptr, Types.term_vector_t) Ctypes.field
    ; size : (Unsigned.uint, Types.term_vector_t) Ctypes.field > >

val term_vector_t : Types.term_vector_t Ctypes.typ

val type_vector_s : 
  < ctype : Types.type_vector_t Ctypes.typ
  ; members : 
    < capacity : (Unsigned.uint, Types.type_vector_t) Ctypes.field
    ; data : (Types.type_t Ctypes.ptr, Types.type_vector_t) Ctypes.field
    ; size : (Unsigned.uint, Types.type_vector_t) Ctypes.field > >

val type_vector_t : Types.type_vector_t Ctypes.typ

val yval_tag_t : Types.yval_tag_t Ctypes.typ

val yval_s : 
  < ctype : Types.yval_t Ctypes.typ
  ; members : 
    < node_id : (Signed.sint, Types.yval_t) Ctypes.field
    ; node_tag : (Types.yval_tag_t, Types.yval_t) Ctypes.field > >

val yval_t : Types.yval_t Ctypes.typ

val yval_vector_s : 
  < ctype : Types.yval_vector_t Ctypes.typ
  ; members : 
    < capacity : (Unsigned.uint, Types.yval_vector_t) Ctypes.field
    ; data : (Types.yval_t Ctypes.ptr, Types.yval_vector_t) Ctypes.field
    ; size : (Unsigned.uint, Types.yval_vector_t) Ctypes.field > >

val yval_vector_t : Types.yval_vector_t Ctypes.typ

val error_report_s : 
  < ctype : Types.error_report_t Ctypes.typ
  ; members : 
    < badval : (Signed.long, Types.error_report_t) Ctypes.field
    ; code : (Types.error_code_t, Types.error_report_t) Ctypes.field
    ; column : (Unsigned.uint, Types.error_report_t) Ctypes.field
    ; line : (Unsigned.uint, Types.error_report_t) Ctypes.field
    ; term1 : (Types.term_t, Types.error_report_t) Ctypes.field
    ; term2 : (Types.term_t, Types.error_report_t) Ctypes.field
    ; type1 : (Types.type_t, Types.error_report_t) Ctypes.field
    ; type2 : (Types.type_t, Types.error_report_t) Ctypes.field > >

val error_report_t : Types.error_report_t Ctypes.typ

type 'a checkable

val sintcheck : 'a Types.sintbase checkable -> bool

val uintcheck : 'a Types.uintbase checkable -> bool

val ptrcheck : 'a Ctypes.ptr checkable -> bool

val yices_version : char Ctypes.ptr Ctypes.ptr checkable

val yices_build_arch : char Ctypes.ptr Ctypes.ptr checkable

val yices_build_mode : char Ctypes.ptr Ctypes.ptr checkable

val yices_build_date : char Ctypes.ptr Ctypes.ptr checkable

val yices_has_mcsat : unit -> Types.bool_t checkable

val yices_is_thread_safe : unit -> Types.bool_t checkable

val yices_init : unit -> unit

val yices_exit : unit -> unit

val yices_reset : unit -> unit

val yices_free_string : char Ctypes.ptr -> unit

val yices_set_out_of_mem_callback : (unit -> unit) Ctypes.static_funptr -> unit

val yices_error_code : unit -> Types.error_code_t

val yices_error_report : unit -> Types.error_report_t Ctypes.ptr

val yices_clear_error : unit -> unit

val yices_print_error : Types.FILE.t Ctypes.ptr -> Types.unit_t checkable

val yices_print_error_fd : Signed.sint -> Types.unit_t checkable

val yices_error_string : unit -> char Ctypes.ptr checkable

val yices_init_term_vector : Types.term_vector_t Ctypes.ptr -> unit

val yices_init_type_vector : Types.type_vector_t Ctypes.ptr -> unit

val yices_delete_term_vector : Types.term_vector_t Ctypes.ptr -> unit

val yices_delete_type_vector : Types.type_vector_t Ctypes.ptr -> unit

val yices_reset_term_vector : Types.term_vector_t Ctypes.ptr -> unit

val yices_reset_type_vector : Types.type_vector_t Ctypes.ptr -> unit

val yices_bool_type : unit -> Types.type_t checkable

val yices_int_type : unit -> Types.type_t checkable

val yices_real_type : unit -> Types.type_t checkable

val yices_bv_type : Unsigned.uint -> Types.type_t checkable

val yices_new_scalar_type : Unsigned.uint -> Types.type_t checkable

val yices_new_uninterpreted_type : unit -> Types.type_t checkable

val yices_tuple_type : 
  Unsigned.uint ->
  Types.type_t Ctypes.ptr ->
  Types.type_t checkable

val yices_tuple_type1 : Types.type_t -> Types.type_t checkable

val yices_tuple_type2 : Types.type_t -> Types.type_t -> Types.type_t checkable

val yices_tuple_type3 : 
  Types.type_t ->
  Types.type_t ->
  Types.type_t ->
  Types.type_t checkable

val yices_function_type : 
  Unsigned.uint ->
  Types.type_t Ctypes.ptr ->
  Types.type_t ->
  Types.type_t checkable

val yices_function_type1 : 
  Types.type_t ->
  Types.type_t ->
  Types.type_t checkable

val yices_function_type2 : 
  Types.type_t ->
  Types.type_t ->
  Types.type_t ->
  Types.type_t checkable

val yices_function_type3 : 
  Types.type_t ->
  Types.type_t ->
  Types.type_t ->
  Types.type_t ->
  Types.type_t checkable

val yices_type_is_bool : Types.type_t -> Types.bool_t checkable

val yices_type_is_int : Types.type_t -> Types.bool_t checkable

val yices_type_is_real : Types.type_t -> Types.bool_t checkable

val yices_type_is_arithmetic : Types.type_t -> Types.bool_t checkable

val yices_type_is_bitvector : Types.type_t -> Types.bool_t checkable

val yices_type_is_tuple : Types.type_t -> Types.bool_t checkable

val yices_type_is_function : Types.type_t -> Types.bool_t checkable

val yices_type_is_scalar : Types.type_t -> Types.bool_t checkable

val yices_type_is_uninterpreted : Types.type_t -> Types.bool_t checkable

val yices_test_subtype : Types.type_t -> Types.type_t -> Types.bool_t checkable

val yices_compatible_types : 
  Types.type_t ->
  Types.type_t ->
  Types.bool_t checkable

val yices_bvtype_size : Types.type_t -> Types.uint_t checkable

val yices_scalar_type_card : Types.type_t -> Types.uint_t checkable

val yices_type_num_children : Types.type_t -> Types.sint_t checkable

val yices_type_child : Types.type_t -> Signed.sint -> Types.type_t checkable

val yices_type_children : 
  Types.type_t ->
  Types.type_vector_t Ctypes.ptr ->
  Types.unit_t checkable

val yices_true : unit -> Types.term_t checkable

val yices_false : unit -> Types.term_t checkable

val yices_constant : Types.type_t -> Signed.sint -> Types.term_t checkable

val yices_new_uninterpreted_term : Types.type_t -> Types.term_t checkable

val yices_new_variable : Types.type_t -> Types.term_t checkable

val yices_application : 
  Types.term_t ->
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.term_t checkable

val yices_application1 : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_application2 : 
  Types.term_t ->
  Types.term_t ->
  Types.term_t ->
  Types.term_t checkable

val yices_application3 : 
  Types.term_t ->
  Types.term_t ->
  Types.term_t ->
  Types.term_t ->
  Types.term_t checkable

val yices_ite : 
  Types.term_t ->
  Types.term_t ->
  Types.term_t ->
  Types.term_t checkable

val yices_eq : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_neq : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_not : Types.term_t -> Types.term_t checkable

val yices_or : 
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.term_t checkable

val yices_and : 
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.term_t checkable

val yices_xor : 
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.term_t checkable

val yices_or2 : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_and2 : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_xor2 : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_or3 : 
  Types.term_t ->
  Types.term_t ->
  Types.term_t ->
  Types.term_t checkable

val yices_and3 : 
  Types.term_t ->
  Types.term_t ->
  Types.term_t ->
  Types.term_t checkable

val yices_xor3 : 
  Types.term_t ->
  Types.term_t ->
  Types.term_t ->
  Types.term_t checkable

val yices_iff : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_implies : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_tuple : 
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.term_t checkable

val yices_pair : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_triple : 
  Types.term_t ->
  Types.term_t ->
  Types.term_t ->
  Types.term_t checkable

val yices_select : Unsigned.uint -> Types.term_t -> Types.term_t checkable

val yices_tuple_update : 
  Types.term_t ->
  Unsigned.uint ->
  Types.term_t ->
  Types.term_t checkable

val yices_update : 
  Types.term_t ->
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.term_t ->
  Types.term_t checkable

val yices_update1 : 
  Types.term_t ->
  Types.term_t ->
  Types.term_t ->
  Types.term_t checkable

val yices_update2 : 
  Types.term_t ->
  Types.term_t ->
  Types.term_t ->
  Types.term_t ->
  Types.term_t checkable

val yices_update3 : 
  Types.term_t ->
  Types.term_t ->
  Types.term_t ->
  Types.term_t ->
  Types.term_t ->
  Types.term_t checkable

val yices_distinct : 
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.term_t checkable

val yices_forall : 
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.term_t ->
  Types.term_t checkable

val yices_exists : 
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.term_t ->
  Types.term_t checkable

val yices_lambda : 
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.term_t ->
  Types.term_t checkable

val yices_zero : unit -> Types.term_t checkable

val yices_int32 : Signed.sint -> Types.term_t checkable

val yices_int64 : Signed.long -> Types.term_t checkable

val yices_rational32 : Signed.sint -> Unsigned.uint -> Types.term_t checkable

val yices_rational64 : Signed.long -> Unsigned.ulong -> Types.term_t checkable

val yices_mpz : 
  Ctypes_zarith.MPZ.t Ctypes.abstract Ctypes.ptr ->
  Types.term_t checkable

val yices_mpq : 
  Ctypes_zarith.MPQ.t Ctypes.abstract Ctypes.ptr ->
  Types.term_t checkable

val yices_parse_rational : char Ctypes.ptr -> Types.term_t checkable

val yices_parse_float : char Ctypes.ptr -> Types.term_t checkable

val yices_add : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_sub : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_neg : Types.term_t -> Types.term_t checkable

val yices_mul : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_square : Types.term_t -> Types.term_t checkable

val yices_power : Types.term_t -> Unsigned.uint -> Types.term_t checkable

val yices_sum : 
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.term_t checkable

val yices_product : 
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.term_t checkable

val yices_division : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_idiv : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_imod : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_divides_atom : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_is_int_atom : Types.term_t -> Types.term_t checkable

val yices_abs : Types.term_t -> Types.term_t checkable

val yices_floor : Types.term_t -> Types.term_t checkable

val yices_ceil : Types.term_t -> Types.term_t checkable

val yices_poly_int32 : 
  Unsigned.uint ->
  Signed.sint Ctypes.ptr ->
  Types.term_t Ctypes.ptr ->
  Types.term_t checkable

val yices_poly_int64 : 
  Unsigned.uint ->
  Signed.long Ctypes.ptr ->
  Types.term_t Ctypes.ptr ->
  Types.term_t checkable

val yices_poly_rational32 : 
  Unsigned.uint ->
  Signed.sint Ctypes.ptr ->
  Unsigned.uint Ctypes.ptr ->
  Types.term_t Ctypes.ptr ->
  Types.term_t checkable

val yices_poly_rational64 : 
  Unsigned.uint ->
  Signed.long Ctypes.ptr ->
  Unsigned.ulong Ctypes.ptr ->
  Types.term_t Ctypes.ptr ->
  Types.term_t checkable

val yices_poly_mpz : 
  Unsigned.uint ->
  Ctypes_zarith.MPZ.t Ctypes.abstract Ctypes.ptr ->
  Types.term_t Ctypes.ptr ->
  Types.term_t checkable

val yices_poly_mpq : 
  Unsigned.uint ->
  Ctypes_zarith.MPQ.t Ctypes.abstract Ctypes.ptr ->
  Types.term_t Ctypes.ptr ->
  Types.term_t checkable

val yices_arith_eq_atom : 
  Types.term_t ->
  Types.term_t ->
  Types.term_t checkable

val yices_arith_neq_atom : 
  Types.term_t ->
  Types.term_t ->
  Types.term_t checkable

val yices_arith_geq_atom : 
  Types.term_t ->
  Types.term_t ->
  Types.term_t checkable

val yices_arith_leq_atom : 
  Types.term_t ->
  Types.term_t ->
  Types.term_t checkable

val yices_arith_gt_atom : 
  Types.term_t ->
  Types.term_t ->
  Types.term_t checkable

val yices_arith_lt_atom : 
  Types.term_t ->
  Types.term_t ->
  Types.term_t checkable

val yices_arith_eq0_atom : Types.term_t -> Types.term_t checkable

val yices_arith_neq0_atom : Types.term_t -> Types.term_t checkable

val yices_arith_geq0_atom : Types.term_t -> Types.term_t checkable

val yices_arith_leq0_atom : Types.term_t -> Types.term_t checkable

val yices_arith_gt0_atom : Types.term_t -> Types.term_t checkable

val yices_arith_lt0_atom : Types.term_t -> Types.term_t checkable

val yices_bvconst_uint32 : 
  Unsigned.uint ->
  Unsigned.uint ->
  Types.term_t checkable

val yices_bvconst_uint64 : 
  Unsigned.uint ->
  Unsigned.ulong ->
  Types.term_t checkable

val yices_bvconst_int32 : 
  Unsigned.uint ->
  Signed.sint ->
  Types.term_t checkable

val yices_bvconst_int64 : 
  Unsigned.uint ->
  Signed.long ->
  Types.term_t checkable

val yices_bvconst_mpz : 
  Unsigned.uint ->
  Ctypes_zarith.MPZ.t Ctypes.abstract Ctypes.ptr ->
  Types.term_t checkable

val yices_bvconst_zero : Unsigned.uint -> Types.term_t checkable

val yices_bvconst_one : Unsigned.uint -> Types.term_t checkable

val yices_bvconst_minus_one : Unsigned.uint -> Types.term_t checkable

val yices_bvconst_from_array : 
  Unsigned.uint ->
  Signed.sint Ctypes.ptr ->
  Types.term_t checkable

val yices_parse_bvbin : char Ctypes.ptr -> Types.term_t checkable

val yices_parse_bvhex : char Ctypes.ptr -> Types.term_t checkable

val yices_bvadd : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_bvsub : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_bvneg : Types.term_t -> Types.term_t checkable

val yices_bvmul : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_bvsquare : Types.term_t -> Types.term_t checkable

val yices_bvpower : Types.term_t -> Unsigned.uint -> Types.term_t checkable

val yices_bvdiv : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_bvrem : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_bvsdiv : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_bvsrem : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_bvsmod : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_bvnot : Types.term_t -> Types.term_t checkable

val yices_bvnand : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_bvnor : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_bvxnor : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_bvshl : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_bvlshr : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_bvashr : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_bvand : 
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.term_t checkable

val yices_bvor : 
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.term_t checkable

val yices_bvxor : 
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.term_t checkable

val yices_bvand2 : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_bvor2 : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_bvxor2 : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_bvand3 : 
  Types.term_t ->
  Types.term_t ->
  Types.term_t ->
  Types.term_t checkable

val yices_bvor3 : 
  Types.term_t ->
  Types.term_t ->
  Types.term_t ->
  Types.term_t checkable

val yices_bvxor3 : 
  Types.term_t ->
  Types.term_t ->
  Types.term_t ->
  Types.term_t checkable

val yices_bvsum : 
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.term_t checkable

val yices_bvproduct : 
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.term_t checkable

val yices_shift_left0 : Types.term_t -> Unsigned.uint -> Types.term_t checkable

val yices_shift_left1 : Types.term_t -> Unsigned.uint -> Types.term_t checkable

val yices_shift_right0 : 
  Types.term_t ->
  Unsigned.uint ->
  Types.term_t checkable

val yices_shift_right1 : 
  Types.term_t ->
  Unsigned.uint ->
  Types.term_t checkable

val yices_ashift_right : 
  Types.term_t ->
  Unsigned.uint ->
  Types.term_t checkable

val yices_rotate_left : Types.term_t -> Unsigned.uint -> Types.term_t checkable

val yices_rotate_right : 
  Types.term_t ->
  Unsigned.uint ->
  Types.term_t checkable

val yices_bvextract : 
  Types.term_t ->
  Unsigned.uint ->
  Unsigned.uint ->
  Types.term_t checkable

val yices_bvconcat2 : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_bvconcat : 
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.term_t checkable

val yices_bvrepeat : Types.term_t -> Unsigned.uint -> Types.term_t checkable

val yices_sign_extend : Types.term_t -> Unsigned.uint -> Types.term_t checkable

val yices_zero_extend : Types.term_t -> Unsigned.uint -> Types.term_t checkable

val yices_redand : Types.term_t -> Types.term_t checkable

val yices_redor : Types.term_t -> Types.term_t checkable

val yices_redcomp : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_bvarray : 
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.term_t checkable

val yices_bitextract : Types.term_t -> Unsigned.uint -> Types.term_t checkable

val yices_bveq_atom : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_bvneq_atom : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_bvge_atom : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_bvgt_atom : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_bvle_atom : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_bvlt_atom : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_bvsge_atom : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_bvsgt_atom : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_bvsle_atom : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_bvslt_atom : Types.term_t -> Types.term_t -> Types.term_t checkable

val yices_parse_type : char Ctypes.ptr -> Types.type_t checkable

val yices_parse_term : char Ctypes.ptr -> Types.term_t checkable

val yices_subst_term : 
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.term_t Ctypes.ptr ->
  Types.term_t ->
  Types.term_t checkable

val yices_subst_term_array : 
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.term_t Ctypes.ptr ->
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.unit_t checkable

val yices_set_type_name : 
  Types.type_t ->
  char Ctypes.ptr ->
  Types.unit_t checkable

val yices_set_term_name : 
  Types.term_t ->
  char Ctypes.ptr ->
  Types.unit_t checkable

val yices_remove_type_name : char Ctypes.ptr -> unit

val yices_remove_term_name : char Ctypes.ptr -> unit

val yices_get_type_by_name : char Ctypes.ptr -> Types.type_t checkable

val yices_get_term_by_name : char Ctypes.ptr -> Types.term_t checkable

val yices_clear_type_name : Types.type_t -> Types.unit_t checkable

val yices_clear_term_name : Types.term_t -> Types.unit_t checkable

val yices_get_type_name : Types.type_t -> char Ctypes.ptr checkable

val yices_get_term_name : Types.term_t -> char Ctypes.ptr checkable

val yices_type_of_term : Types.term_t -> Types.type_t checkable

val yices_term_is_bool : Types.term_t -> Types.bool_t checkable

val yices_term_is_int : Types.term_t -> Types.bool_t checkable

val yices_term_is_real : Types.term_t -> Types.bool_t checkable

val yices_term_is_arithmetic : Types.term_t -> Types.bool_t checkable

val yices_term_is_bitvector : Types.term_t -> Types.bool_t checkable

val yices_term_is_tuple : Types.term_t -> Types.bool_t checkable

val yices_term_is_function : Types.term_t -> Types.bool_t checkable

val yices_term_is_scalar : Types.term_t -> Types.bool_t checkable

val yices_term_bitsize : Types.term_t -> Types.uint_t checkable

val yices_term_is_ground : Types.term_t -> Types.bool_t checkable

val yices_term_is_atomic : Types.term_t -> Types.bool_t checkable

val yices_term_is_composite : Types.term_t -> Types.bool_t checkable

val yices_term_is_projection : Types.term_t -> Types.bool_t checkable

val yices_term_is_sum : Types.term_t -> Types.bool_t checkable

val yices_term_is_bvsum : Types.term_t -> Types.bool_t checkable

val yices_term_is_product : Types.term_t -> Types.bool_t checkable

val yices_term_constructor : Types.term_t -> Types.term_constructor_t checkable

val yices_term_num_children : Types.term_t -> Types.sint_t checkable

val yices_term_child : Types.term_t -> Signed.sint -> Types.term_t checkable

val yices_term_children : 
  Types.term_t ->
  Types.term_vector_t Ctypes.ptr ->
  Types.unit_t checkable

val yices_proj_index : Types.term_t -> Types.sint_t checkable

val yices_proj_arg : Types.term_t -> Types.term_t checkable

val yices_bool_const_value : 
  Types.term_t ->
  Types.bool_t Ctypes.ptr ->
  Types.unit_t checkable

val yices_bv_const_value : 
  Types.term_t ->
  Signed.sint Ctypes.ptr ->
  Types.unit_t checkable

val yices_scalar_const_value : 
  Types.term_t ->
  Signed.sint Ctypes.ptr ->
  Types.unit_t checkable

val yices_rational_const_value : 
  Types.term_t ->
  Ctypes_zarith.MPQ.t Ctypes.abstract Ctypes.ptr ->
  Types.unit_t checkable

val yices_sum_component : 
  Types.term_t ->
  Signed.sint ->
  Ctypes_zarith.MPQ.t Ctypes.abstract Ctypes.ptr ->
  Types.term_t Ctypes.ptr ->
  Types.unit_t checkable

val yices_bvsum_component : 
  Types.term_t ->
  Signed.sint ->
  Signed.sint Ctypes.ptr ->
  Types.term_t Ctypes.ptr ->
  Types.unit_t checkable

val yices_product_component : 
  Types.term_t ->
  Signed.sint ->
  Types.term_t Ctypes.ptr ->
  Unsigned.uint Ctypes.ptr ->
  Types.unit_t checkable

val yices_num_terms : unit -> Unsigned.uint

val yices_num_types : unit -> Unsigned.uint

val yices_incref_term : Types.term_t -> Types.unit_t checkable

val yices_decref_term : Types.term_t -> Types.unit_t checkable

val yices_incref_type : Types.type_t -> Types.unit_t checkable

val yices_decref_type : Types.type_t -> Types.unit_t checkable

val yices_num_posref_terms : unit -> Unsigned.uint

val yices_num_posref_types : unit -> Unsigned.uint

val yices_garbage_collect : 
  Types.term_t Ctypes.ptr ->
  Unsigned.uint ->
  Types.type_t Ctypes.ptr ->
  Unsigned.uint ->
  Signed.sint ->
  unit

val yices_new_config : unit -> Types.ctx_config_t Ctypes.ptr checkable

val yices_free_config : Types.ctx_config_t Ctypes.ptr -> unit

val yices_set_config : 
  Types.ctx_config_t Ctypes.ptr ->
  char Ctypes.ptr ->
  char Ctypes.ptr ->
  Types.unit_t checkable

val yices_default_config_for_logic : 
  Types.ctx_config_t Ctypes.ptr ->
  char Ctypes.ptr ->
  Types.unit_t checkable

val yices_new_context : 
  Types.ctx_config_t Ctypes.ptr ->
  Types.context_t Ctypes.ptr checkable

val yices_free_context : Types.context_t Ctypes.ptr -> unit

val yices_context_status : Types.context_t Ctypes.ptr -> Types.smt_status_t

val yices_reset_context : Types.context_t Ctypes.ptr -> unit

val yices_push : Types.context_t Ctypes.ptr -> Types.unit_t checkable

val yices_pop : Types.context_t Ctypes.ptr -> Types.unit_t checkable

val yices_context_enable_option : 
  Types.context_t Ctypes.ptr ->
  char Ctypes.ptr ->
  Types.unit_t checkable

val yices_context_disable_option : 
  Types.context_t Ctypes.ptr ->
  char Ctypes.ptr ->
  Types.unit_t checkable

val yices_assert_formula : 
  Types.context_t Ctypes.ptr ->
  Types.term_t ->
  Types.unit_t checkable

val yices_assert_formulas : 
  Types.context_t Ctypes.ptr ->
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.unit_t checkable

val yices_check_context : 
  Types.context_t Ctypes.ptr ->
  Types.param_t Ctypes.ptr ->
  Types.smt_status_t

val yices_check_context_with_assumptions : 
  Types.context_t Ctypes.ptr ->
  Types.param_t Ctypes.ptr ->
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.smt_status_t

val yices_assert_blocking_clause : 
  Types.context_t Ctypes.ptr ->
  Types.unit_t checkable

val yices_stop_search : Types.context_t Ctypes.ptr -> unit

val yices_new_param_record : unit -> Types.param_t Ctypes.ptr checkable

val yices_default_params_for_context : 
  Types.context_t Ctypes.ptr ->
  Types.param_t Ctypes.ptr ->
  unit

val yices_set_param : 
  Types.param_t Ctypes.ptr ->
  char Ctypes.ptr ->
  char Ctypes.ptr ->
  Types.unit_t checkable

val yices_free_param_record : Types.param_t Ctypes.ptr -> unit

val yices_get_unsat_core : 
  Types.context_t Ctypes.ptr ->
  Types.term_vector_t Ctypes.ptr ->
  Types.unit_t checkable

val yices_get_model : 
  Types.context_t Ctypes.ptr ->
  Types.bool_t ->
  Types.model_t Ctypes.ptr checkable

val yices_free_model : Types.model_t Ctypes.ptr -> unit

val yices_model_from_map : 
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.term_t Ctypes.ptr ->
  Types.model_t Ctypes.ptr checkable

val yices_model_collect_defined_terms : 
  Types.model_t Ctypes.ptr ->
  Types.term_vector_t Ctypes.ptr ->
  unit

val yices_check_formula : 
  Types.term_t ->
  char Ctypes.ptr ->
  Types.model_t Ctypes.ptr Ctypes.ptr ->
  char Ctypes.ptr ->
  Types.smt_status_t

val yices_check_formulas : 
  Types.term_t Ctypes.ptr ->
  Unsigned.uint ->
  char Ctypes.ptr ->
  Types.model_t Ctypes.ptr Ctypes.ptr ->
  char Ctypes.ptr ->
  Types.smt_status_t

val yices_has_delegate : char Ctypes.ptr -> Types.bool_t checkable

val yices_export_formula_to_dimacs : 
  Types.term_t ->
  char Ctypes.ptr ->
  Types.bool_t ->
  Types.smt_status_t Ctypes.ptr ->
  Types.bool_t checkable

val yices_export_formulas_to_dimacs : 
  Types.term_t Ctypes.ptr ->
  Unsigned.uint ->
  char Ctypes.ptr ->
  Types.bool_t ->
  Types.smt_status_t Ctypes.ptr ->
  Types.bool_t checkable

val yices_get_bool_value : 
  Types.model_t Ctypes.ptr ->
  Types.term_t ->
  Types.bool_t Ctypes.ptr ->
  Types.unit_t checkable

val yices_get_int32_value : 
  Types.model_t Ctypes.ptr ->
  Types.term_t ->
  Signed.sint Ctypes.ptr ->
  Types.unit_t checkable

val yices_get_int64_value : 
  Types.model_t Ctypes.ptr ->
  Types.term_t ->
  Signed.long Ctypes.ptr ->
  Types.unit_t checkable

val yices_get_rational32_value : 
  Types.model_t Ctypes.ptr ->
  Types.term_t ->
  Signed.sint Ctypes.ptr ->
  Unsigned.uint Ctypes.ptr ->
  Types.unit_t checkable

val yices_get_rational64_value : 
  Types.model_t Ctypes.ptr ->
  Types.term_t ->
  Signed.long Ctypes.ptr ->
  Unsigned.ulong Ctypes.ptr ->
  Types.unit_t checkable

val yices_get_double_value : 
  Types.model_t Ctypes.ptr ->
  Types.term_t ->
  float Ctypes.ptr ->
  Types.unit_t checkable

val yices_get_mpz_value : 
  Types.model_t Ctypes.ptr ->
  Types.term_t ->
  Ctypes_zarith.MPZ.t Ctypes.abstract Ctypes.ptr ->
  Types.unit_t checkable

val yices_get_mpq_value : 
  Types.model_t Ctypes.ptr ->
  Types.term_t ->
  Ctypes_zarith.MPQ.t Ctypes.abstract Ctypes.ptr ->
  Types.unit_t checkable

val yices_get_bv_value : 
  Types.model_t Ctypes.ptr ->
  Types.term_t ->
  Signed.sint Ctypes.ptr ->
  Types.unit_t checkable

val yices_get_scalar_value : 
  Types.model_t Ctypes.ptr ->
  Types.term_t ->
  Signed.sint Ctypes.ptr ->
  Types.unit_t checkable

val yices_init_yval_vector : Types.yval_vector_t Ctypes.ptr -> unit

val yices_delete_yval_vector : Types.yval_vector_t Ctypes.ptr -> unit

val yices_reset_yval_vector : Types.yval_vector_t Ctypes.ptr -> unit

val yices_get_value : 
  Types.model_t Ctypes.ptr ->
  Types.term_t ->
  Types.yval_t Ctypes.ptr ->
  Types.unit_t checkable

val yices_val_is_int32 : 
  Types.model_t Ctypes.ptr ->
  Types.yval_t Ctypes.ptr ->
  Types.bool_t checkable

val yices_val_is_int64 : 
  Types.model_t Ctypes.ptr ->
  Types.yval_t Ctypes.ptr ->
  Types.bool_t checkable

val yices_val_is_rational32 : 
  Types.model_t Ctypes.ptr ->
  Types.yval_t Ctypes.ptr ->
  Types.bool_t checkable

val yices_val_is_rational64 : 
  Types.model_t Ctypes.ptr ->
  Types.yval_t Ctypes.ptr ->
  Types.bool_t checkable

val yices_val_is_integer : 
  Types.model_t Ctypes.ptr ->
  Types.yval_t Ctypes.ptr ->
  Types.bool_t checkable

val yices_val_bitsize : 
  Types.model_t Ctypes.ptr ->
  Types.yval_t Ctypes.ptr ->
  Types.uint_t checkable

val yices_val_tuple_arity : 
  Types.model_t Ctypes.ptr ->
  Types.yval_t Ctypes.ptr ->
  Types.uint_t checkable

val yices_val_mapping_arity : 
  Types.model_t Ctypes.ptr ->
  Types.yval_t Ctypes.ptr ->
  Types.uint_t checkable

val yices_val_function_arity : 
  Types.model_t Ctypes.ptr ->
  Types.yval_t Ctypes.ptr ->
  Types.uint_t checkable

val yices_val_function_type : 
  Types.model_t Ctypes.ptr ->
  Types.yval_t Ctypes.ptr ->
  Types.type_t checkable

val yices_val_get_bool : 
  Types.model_t Ctypes.ptr ->
  Types.yval_t Ctypes.ptr ->
  Types.bool_t Ctypes.ptr ->
  Types.unit_t checkable

val yices_val_get_int32 : 
  Types.model_t Ctypes.ptr ->
  Types.yval_t Ctypes.ptr ->
  Signed.sint Ctypes.ptr ->
  Types.unit_t checkable

val yices_val_get_int64 : 
  Types.model_t Ctypes.ptr ->
  Types.yval_t Ctypes.ptr ->
  Signed.long Ctypes.ptr ->
  Types.unit_t checkable

val yices_val_get_rational32 : 
  Types.model_t Ctypes.ptr ->
  Types.yval_t Ctypes.ptr ->
  Signed.sint Ctypes.ptr ->
  Unsigned.uint Ctypes.ptr ->
  Types.unit_t checkable

val yices_val_get_rational64 : 
  Types.model_t Ctypes.ptr ->
  Types.yval_t Ctypes.ptr ->
  Signed.long Ctypes.ptr ->
  Unsigned.ulong Ctypes.ptr ->
  Types.unit_t checkable

val yices_val_get_double : 
  Types.model_t Ctypes.ptr ->
  Types.yval_t Ctypes.ptr ->
  float Ctypes.ptr ->
  Types.unit_t checkable

val yices_val_get_mpz : 
  Types.model_t Ctypes.ptr ->
  Types.yval_t Ctypes.ptr ->
  Ctypes_zarith.MPZ.t Ctypes.abstract Ctypes.ptr ->
  Types.unit_t checkable

val yices_val_get_mpq : 
  Types.model_t Ctypes.ptr ->
  Types.yval_t Ctypes.ptr ->
  Ctypes_zarith.MPQ.t Ctypes.abstract Ctypes.ptr ->
  Types.unit_t checkable

val yices_val_get_bv : 
  Types.model_t Ctypes.ptr ->
  Types.yval_t Ctypes.ptr ->
  Signed.sint Ctypes.ptr ->
  Types.unit_t checkable

val yices_val_get_scalar : 
  Types.model_t Ctypes.ptr ->
  Types.yval_t Ctypes.ptr ->
  Signed.sint Ctypes.ptr ->
  Types.type_t Ctypes.ptr ->
  Types.unit_t checkable

val yices_val_expand_tuple : 
  Types.model_t Ctypes.ptr ->
  Types.yval_t Ctypes.ptr ->
  Types.yval_t Ctypes.ptr ->
  Types.unit_t checkable

val yices_val_expand_function : 
  Types.model_t Ctypes.ptr ->
  Types.yval_t Ctypes.ptr ->
  Types.yval_t Ctypes.ptr ->
  Types.yval_vector_t Ctypes.ptr ->
  Types.unit_t checkable

val yices_val_expand_mapping : 
  Types.model_t Ctypes.ptr ->
  Types.yval_t Ctypes.ptr ->
  Types.yval_t Ctypes.ptr ->
  Types.yval_t Ctypes.ptr ->
  Types.unit_t checkable

val yices_formula_true_in_model : 
  Types.model_t Ctypes.ptr ->
  Types.term_t ->
  Types.bool_t checkable

val yices_formulas_true_in_model : 
  Types.model_t Ctypes.ptr ->
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.bool_t checkable

val yices_get_value_as_term : 
  Types.model_t Ctypes.ptr ->
  Types.term_t ->
  Types.term_t checkable

val yices_term_array_value : 
  Types.model_t Ctypes.ptr ->
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.term_t Ctypes.ptr ->
  Types.unit_t checkable

val yices_model_term_support : 
  Types.model_t Ctypes.ptr ->
  Types.term_t ->
  Types.term_vector_t Ctypes.ptr ->
  Types.unit_t checkable

val yices_model_term_array_support : 
  Types.model_t Ctypes.ptr ->
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.term_vector_t Ctypes.ptr ->
  Types.unit_t checkable

val yices_implicant_for_formula : 
  Types.model_t Ctypes.ptr ->
  Types.term_t ->
  Types.term_vector_t Ctypes.ptr ->
  Types.unit_t checkable

val yices_implicant_for_formulas : 
  Types.model_t Ctypes.ptr ->
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.term_vector_t Ctypes.ptr ->
  Types.unit_t checkable

val yices_generalize_model : 
  Types.model_t Ctypes.ptr ->
  Types.term_t ->
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.yices_gen_mode_t ->
  Types.term_vector_t Ctypes.ptr ->
  Types.unit_t checkable

val yices_generalize_model_array : 
  Types.model_t Ctypes.ptr ->
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.yices_gen_mode_t ->
  Types.term_vector_t Ctypes.ptr ->
  Types.unit_t checkable

val yices_pp_type : 
  Types.FILE.t Ctypes.ptr ->
  Types.type_t ->
  Unsigned.uint ->
  Unsigned.uint ->
  Unsigned.uint ->
  Types.unit_t checkable

val yices_pp_term : 
  Types.FILE.t Ctypes.ptr ->
  Types.term_t ->
  Unsigned.uint ->
  Unsigned.uint ->
  Unsigned.uint ->
  Types.unit_t checkable

val yices_pp_term_array : 
  Types.FILE.t Ctypes.ptr ->
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Unsigned.uint ->
  Unsigned.uint ->
  Unsigned.uint ->
  Types.bool_t ->
  Types.unit_t checkable

val yices_print_model : 
  Types.FILE.t Ctypes.ptr ->
  Types.model_t Ctypes.ptr ->
  unit

val yices_pp_model : 
  Types.FILE.t Ctypes.ptr ->
  Types.model_t Ctypes.ptr ->
  Unsigned.uint ->
  Unsigned.uint ->
  Unsigned.uint ->
  Types.unit_t checkable

val yices_print_term_values : 
  Types.FILE.t Ctypes.ptr ->
  Types.model_t Ctypes.ptr ->
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.unit_t checkable

val yices_pp_term_values : 
  Types.FILE.t Ctypes.ptr ->
  Types.model_t Ctypes.ptr ->
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Unsigned.uint ->
  Unsigned.uint ->
  Unsigned.uint ->
  Types.unit_t checkable

val yices_pp_type_fd : 
  Signed.sint ->
  Types.type_t ->
  Unsigned.uint ->
  Unsigned.uint ->
  Unsigned.uint ->
  Types.unit_t checkable

val yices_pp_term_fd : 
  Signed.sint ->
  Types.term_t ->
  Unsigned.uint ->
  Unsigned.uint ->
  Unsigned.uint ->
  Types.unit_t checkable

val yices_pp_term_array_fd : 
  Signed.sint ->
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Unsigned.uint ->
  Unsigned.uint ->
  Unsigned.uint ->
  Types.bool_t ->
  Types.unit_t checkable

val yices_print_model_fd : 
  Signed.sint ->
  Types.model_t Ctypes.ptr ->
  Types.unit_t checkable

val yices_pp_model_fd : 
  Signed.sint ->
  Types.model_t Ctypes.ptr ->
  Unsigned.uint ->
  Unsigned.uint ->
  Unsigned.uint ->
  Types.unit_t checkable

val yices_print_term_values_fd : 
  Signed.sint ->
  Types.model_t Ctypes.ptr ->
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Types.unit_t checkable

val yices_pp_term_values_fd : 
  Signed.sint ->
  Types.model_t Ctypes.ptr ->
  Unsigned.uint ->
  Types.term_t Ctypes.ptr ->
  Unsigned.uint ->
  Unsigned.uint ->
  Unsigned.uint ->
  Types.unit_t checkable

val yices_type_to_string : 
  Types.type_t ->
  Unsigned.uint ->
  Unsigned.uint ->
  Unsigned.uint ->
  char Ctypes.ptr checkable

val yices_term_to_string : 
  Types.term_t ->
  Unsigned.uint ->
  Unsigned.uint ->
  Unsigned.uint ->
  char Ctypes.ptr checkable

val yices_model_to_string : 
  Types.model_t Ctypes.ptr ->
  Unsigned.uint ->
  Unsigned.uint ->
  Unsigned.uint ->
  char Ctypes.ptr checkable

package yices2_bindings