yices2_bindings 0.1 · OCaml Package

val anonymous_2 : [ `anonymous ] Ctypes.structure Ctypes.typ

val anonymous_3 : [ `anonymous_0 ] Ctypes.union Ctypes.typ

val anonymous_4 : [ `anonymous_1 ] Ctypes.structure Ctypes.typ

val _G_fpos_t_0 : [ `_G_fpos_t ] Ctypes.structure Ctypes.typ

val _G_fpos64_t_0 : [ `_G_fpos64_t ] Ctypes.structure Ctypes.typ

val _IO_marker_0 : [ `_IO_marker ] Ctypes.structure Ctypes.typ

val _IO_codecvt_0 : [ `_IO_codecvt ] Ctypes.structure Ctypes.typ

val _IO_wide_data_0 : [ `_IO_wide_data ] Ctypes.structure Ctypes.typ

val __IO_FILE_0 : [ `__IO_FILE ] Ctypes.structure Ctypes.typ

val context_s_0 : [ `context_s ] Ctypes.structure Ctypes.typ

val model_s_0 : [ `model_s ] Ctypes.structure Ctypes.typ

val ctx_config_s_0 : [ `ctx_config_s ] Ctypes.structure Ctypes.typ

val param_s_0 : [ `param_s ] Ctypes.structure Ctypes.typ

val term_vector_s_0 : [ `term_vector_s ] Ctypes.structure Ctypes.typ

val type_vector_s_0 : [ `type_vector_s ] Ctypes.structure Ctypes.typ

val yval_s_0 : [ `yval_s ] Ctypes.structure Ctypes.typ

val yval_vector_s_0 : [ `yval_vector_s ] Ctypes.structure Ctypes.typ

val error_report_s_0 : [ `error_report_s ] Ctypes.structure Ctypes.typ

val __u_char : Unsigned.uchar Ctypes.typ

val __u_short : Unsigned.ushort Ctypes.typ

val __u_int : Unsigned.uint Ctypes.typ

val __u_long : Unsigned.ulong Ctypes.typ

val __int8_t : int Ctypes.typ

val __uint8_t : Unsigned.uchar Ctypes.typ

val __int16_t : int Ctypes.typ

val __uint16_t : Unsigned.ushort Ctypes.typ

val __int32_t : Signed.sint Ctypes.typ

val __uint32_t : Unsigned.uint Ctypes.typ

val __int64_t : Signed.long Ctypes.typ

val __uint64_t : Unsigned.ulong Ctypes.typ

val __int_least8_t : int Ctypes.typ

val __uint_least8_t : Unsigned.uchar Ctypes.typ

val __int_least16_t : int Ctypes.typ

val __uint_least16_t : Unsigned.ushort Ctypes.typ

val __int_least32_t : Signed.sint Ctypes.typ

val __uint_least32_t : Unsigned.uint Ctypes.typ

val __int_least64_t : Signed.long Ctypes.typ

val __uint_least64_t : Unsigned.ulong Ctypes.typ

val __quad_t : Signed.long Ctypes.typ

val __u_quad_t : Unsigned.ulong Ctypes.typ

val __intmax_t : Signed.long Ctypes.typ

val __uintmax_t : Unsigned.ulong Ctypes.typ

val __dev_t : Unsigned.ulong Ctypes.typ

val __uid_t : Unsigned.uint Ctypes.typ

val __gid_t : Unsigned.uint Ctypes.typ

val __ino_t : Unsigned.ulong Ctypes.typ

val __ino64_t : Unsigned.ulong Ctypes.typ

val __mode_t : Unsigned.uint Ctypes.typ

val __nlink_t : Unsigned.ulong Ctypes.typ

val __off_t : Signed.long Ctypes.typ

val __off64_t : Signed.long Ctypes.typ

val __pid_t : Signed.sint Ctypes.typ

val anonymous : 
  < ctype : [ `anonymous ] Ctypes.structure Ctypes.typ
  ; members : 
    < __val : 
      (Signed.sint Ctypes_static.carray, [ `anonymous ] Ctypes.structure)
        Ctypes.field > >

val __fsid_t : [ `anonymous ] Ctypes.structure Ctypes.typ

val __clock_t : Signed.long Ctypes.typ

val __rlim_t : Unsigned.ulong Ctypes.typ

val __rlim64_t : Unsigned.ulong Ctypes.typ

val __id_t : Unsigned.uint Ctypes.typ

val __time_t : Signed.long Ctypes.typ

val __useconds_t : Unsigned.uint Ctypes.typ

val __suseconds_t : Signed.long Ctypes.typ

val __daddr_t : Signed.sint Ctypes.typ

val __key_t : Signed.sint Ctypes.typ

val __clockid_t : Signed.sint Ctypes.typ

val __timer_t : unit Ctypes_static.ptr Ctypes.typ

val __blksize_t : Signed.long Ctypes.typ

val __blkcnt_t : Signed.long Ctypes.typ

val __blkcnt64_t : Signed.long Ctypes.typ

val __fsblkcnt_t : Unsigned.ulong Ctypes.typ

val __fsblkcnt64_t : Unsigned.ulong Ctypes.typ

val __fsfilcnt_t : Unsigned.ulong Ctypes.typ

val __fsfilcnt64_t : Unsigned.ulong Ctypes.typ

val __fsword_t : Signed.long Ctypes.typ

val __ssize_t : Signed.long Ctypes.typ

val __syscall_slong_t : Signed.long Ctypes.typ

val __syscall_ulong_t : Unsigned.ulong Ctypes.typ

val __loff_t : Signed.long Ctypes.typ

val __caddr_t : char Ctypes_static.ptr Ctypes.typ

val __intptr_t : Signed.long Ctypes.typ

val __socklen_t : Unsigned.uint Ctypes.typ

val __sig_atomic_t : Signed.sint Ctypes.typ

val int8_t : int Ctypes.typ

val int16_t : int Ctypes.typ

val int32_t : Signed.sint Ctypes.typ

val int64_t : Signed.long Ctypes.typ

val uint8_t : Unsigned.uchar Ctypes.typ

val uint16_t : Unsigned.ushort Ctypes.typ

val uint32_t : Unsigned.uint Ctypes.typ

val uint64_t : Unsigned.ulong Ctypes.typ

val int_least8_t : int Ctypes.typ

val int_least16_t : int Ctypes.typ

val int_least32_t : Signed.sint Ctypes.typ

val int_least64_t : Signed.long Ctypes.typ

val uint_least8_t : Unsigned.uchar Ctypes.typ

val uint_least16_t : Unsigned.ushort Ctypes.typ

val uint_least32_t : Unsigned.uint Ctypes.typ

val uint_least64_t : Unsigned.ulong Ctypes.typ

val int_fast8_t : int Ctypes.typ

val int_fast16_t : Signed.long Ctypes.typ

val int_fast32_t : Signed.long Ctypes.typ

val int_fast64_t : Signed.long Ctypes.typ

val uint_fast8_t : Unsigned.uchar Ctypes.typ

val uint_fast16_t : Unsigned.ulong Ctypes.typ

val uint_fast32_t : Unsigned.ulong Ctypes.typ

val uint_fast64_t : Unsigned.ulong Ctypes.typ

val intptr_t : Signed.long Ctypes.typ

val uintptr_t : Unsigned.ulong Ctypes.typ

val intmax_t : Signed.long Ctypes.typ

val uintmax_t : Unsigned.ulong Ctypes.typ

val size_t : Unsigned.ulong Ctypes.typ

val anonymous_0 : 
  < ctype : [ `anonymous_0 ] Ctypes.union Ctypes.typ
  ; members : 
    < __wch : (Unsigned.uint, [ `anonymous_0 ] Ctypes.union) Ctypes.field
    ; __wchb : 
      (char Ctypes_static.carray, [ `anonymous_0 ] Ctypes.union) Ctypes.field > >

val anonymous_1 : 
  < ctype : [ `anonymous_1 ] Ctypes.structure Ctypes.typ
  ; members : 
    < __count : (Signed.sint, [ `anonymous_1 ] Ctypes.structure) Ctypes.field
    ; __value : 
      ([ `anonymous_0 ] Ctypes.union, [ `anonymous_1 ] Ctypes.structure)
        Ctypes.field > >

val __mbstate_t : [ `anonymous_1 ] Ctypes.structure Ctypes.typ

val _G_fpos_t : 
  < ctype : [ `_G_fpos_t ] Ctypes.structure Ctypes.typ
  ; members : 
    < __pos : (Signed.long, [ `_G_fpos_t ] Ctypes.structure) Ctypes.field
    ; __state : 
      ([ `anonymous_1 ] Ctypes.structure, [ `_G_fpos_t ] Ctypes.structure)
        Ctypes.field > >

val __fpos_t : [ `_G_fpos_t ] Ctypes.structure Ctypes.typ

val _G_fpos64_t : 
  < ctype : [ `_G_fpos64_t ] Ctypes.structure Ctypes.typ
  ; members : 
    < __pos : (Signed.long, [ `_G_fpos64_t ] Ctypes.structure) Ctypes.field
    ; __state : 
      ([ `anonymous_1 ] Ctypes.structure, [ `_G_fpos64_t ] Ctypes.structure)
        Ctypes.field > >

val __fpos64_t : [ `_G_fpos64_t ] Ctypes.structure Ctypes.typ

val ___FILE : [ `__IO_FILE ] Ctypes.structure Ctypes.typ

val _FILE : [ `__IO_FILE ] Ctypes.structure Ctypes.typ

val _IO_marker : 
  < ctype : [ `_IO_marker ] Ctypes.structure Ctypes.typ
  ; members : <  > >

val _IO_codecvt : 
  < ctype : [ `_IO_codecvt ] Ctypes.structure Ctypes.typ
  ; members : <  > >

val _IO_wide_data : 
  < ctype : [ `_IO_wide_data ] Ctypes.structure Ctypes.typ
  ; members : <  > >

val _IO_lock_t : unit Ctypes.typ

val __IO_FILE : 
  < ctype : [ `__IO_FILE ] Ctypes.structure Ctypes.typ
  ; members : 
    < _IO_backup_base : 
      (char Ctypes_static.ptr, [ `__IO_FILE ] Ctypes.structure) Ctypes.field
    ; _IO_buf_base : 
      (char Ctypes_static.ptr, [ `__IO_FILE ] Ctypes.structure) Ctypes.field
    ; _IO_buf_end : 
      (char Ctypes_static.ptr, [ `__IO_FILE ] Ctypes.structure) Ctypes.field
    ; _IO_read_base : 
      (char Ctypes_static.ptr, [ `__IO_FILE ] Ctypes.structure) Ctypes.field
    ; _IO_read_end : 
      (char Ctypes_static.ptr, [ `__IO_FILE ] Ctypes.structure) Ctypes.field
    ; _IO_read_ptr : 
      (char Ctypes_static.ptr, [ `__IO_FILE ] Ctypes.structure) Ctypes.field
    ; _IO_save_base : 
      (char Ctypes_static.ptr, [ `__IO_FILE ] Ctypes.structure) Ctypes.field
    ; _IO_save_end : 
      (char Ctypes_static.ptr, [ `__IO_FILE ] Ctypes.structure) Ctypes.field
    ; _IO_write_base : 
      (char Ctypes_static.ptr, [ `__IO_FILE ] Ctypes.structure) Ctypes.field
    ; _IO_write_end : 
      (char Ctypes_static.ptr, [ `__IO_FILE ] Ctypes.structure) Ctypes.field
    ; _IO_write_ptr : 
      (char Ctypes_static.ptr, [ `__IO_FILE ] Ctypes.structure) Ctypes.field
    ; __pad5 : (Unsigned.ulong, [ `__IO_FILE ] Ctypes.structure) Ctypes.field
    ; _chain : 
      ([ `__IO_FILE ] Ctypes.structure Ctypes_static.ptr,
        [ `__IO_FILE ] Ctypes.structure)
        Ctypes.field
    ; _codecvt : 
      ([ `_IO_codecvt ] Ctypes.structure Ctypes_static.ptr,
        [ `__IO_FILE ] Ctypes.structure)
        Ctypes.field
    ; _cur_column : 
      (Unsigned.ushort, [ `__IO_FILE ] Ctypes.structure) Ctypes.field
    ; _fileno : (Signed.sint, [ `__IO_FILE ] Ctypes.structure) Ctypes.field
    ; _flags : (Signed.sint, [ `__IO_FILE ] Ctypes.structure) Ctypes.field
    ; _flags2 : (Signed.sint, [ `__IO_FILE ] Ctypes.structure) Ctypes.field
    ; _freeres_buf : 
      (unit Ctypes_static.ptr, [ `__IO_FILE ] Ctypes.structure) Ctypes.field
    ; _freeres_list : 
      ([ `__IO_FILE ] Ctypes.structure Ctypes_static.ptr,
        [ `__IO_FILE ] Ctypes.structure)
        Ctypes.field
    ; _lock : 
      (unit Ctypes_static.ptr, [ `__IO_FILE ] Ctypes.structure) Ctypes.field
    ; _markers : 
      ([ `_IO_marker ] Ctypes.structure Ctypes_static.ptr,
        [ `__IO_FILE ] Ctypes.structure)
        Ctypes.field
    ; _mode : (Signed.sint, [ `__IO_FILE ] Ctypes.structure) Ctypes.field
    ; _offset : (Signed.long, [ `__IO_FILE ] Ctypes.structure) Ctypes.field
    ; _old_offset : (Signed.long, [ `__IO_FILE ] Ctypes.structure) Ctypes.field
    ; _shortbuf : 
      (char Ctypes_static.carray, [ `__IO_FILE ] Ctypes.structure) Ctypes.field
    ; _unused2 : 
      (char Ctypes_static.carray, [ `__IO_FILE ] Ctypes.structure) Ctypes.field
    ; _vtable_offset : (int, [ `__IO_FILE ] Ctypes.structure) Ctypes.field
    ; _wide_data : 
      ([ `_IO_wide_data ] Ctypes.structure Ctypes_static.ptr,
        [ `__IO_FILE ] Ctypes.structure)
        Ctypes.field > >

val off_t : Signed.long Ctypes.typ

val ssize_t : Signed.long Ctypes.typ

val fpos_t : [ `_G_fpos_t ] Ctypes.structure Ctypes.typ

val term_t : Signed.sint Ctypes.typ

val type_t : Signed.sint Ctypes.typ

val context_s : 
  < ctype : [ `context_s ] Ctypes.structure Ctypes.typ
  ; members : <  > >

val context_t : [ `context_s ] Ctypes.structure Ctypes.typ

val model_s : 
  < ctype : [ `model_s ] Ctypes.structure Ctypes.typ
  ; members : <  > >

val model_t : [ `model_s ] Ctypes.structure Ctypes.typ

val ctx_config_s : 
  < ctype : [ `ctx_config_s ] Ctypes.structure Ctypes.typ
  ; members : <  > >

val ctx_config_t : [ `ctx_config_s ] Ctypes.structure Ctypes.typ

val param_s : 
  < ctype : [ `param_s ] Ctypes.structure Ctypes.typ
  ; members : <  > >

val param_t : [ `param_s ] Ctypes.structure Ctypes.typ

val smt_status : 
  < ctype : Unsigned.uint Ctypes.typ
  ; of_int : 
    int64 ->
    [> `STATUS_ERROR
    | `STATUS_IDLE
    | `STATUS_INTERRUPTED
    | `STATUS_SAT
    | `STATUS_SEARCHING
    | `STATUS_UNKNOWN
    | `STATUS_UNSAT ]
  ; to_int : 
    [< `STATUS_ERROR
    | `STATUS_IDLE
    | `STATUS_INTERRUPTED
    | `STATUS_SAT
    | `STATUS_SEARCHING
    | `STATUS_UNKNOWN
    | `STATUS_UNSAT ] ->
    int64 >

val smt_status_t : Unsigned.uint Ctypes.typ

val term_vector_s : 
  < ctype : [ `term_vector_s ] Ctypes.structure Ctypes.typ
  ; members : 
    < capacity : 
      (Unsigned.uint, [ `term_vector_s ] Ctypes.structure) Ctypes.field
    ; data : 
      (Signed.sint Ctypes_static.ptr, [ `term_vector_s ] Ctypes.structure)
        Ctypes.field
    ; size : (Unsigned.uint, [ `term_vector_s ] Ctypes.structure) Ctypes.field > >

val term_vector_t : [ `term_vector_s ] Ctypes.structure Ctypes.typ

val type_vector_s : 
  < ctype : [ `type_vector_s ] Ctypes.structure Ctypes.typ
  ; members : 
    < capacity : 
      (Unsigned.uint, [ `type_vector_s ] Ctypes.structure) Ctypes.field
    ; data : 
      (Signed.sint Ctypes_static.ptr, [ `type_vector_s ] Ctypes.structure)
        Ctypes.field
    ; size : (Unsigned.uint, [ `type_vector_s ] Ctypes.structure) Ctypes.field > >

val type_vector_t : [ `type_vector_s ] Ctypes.structure Ctypes.typ

val term_constructor : 
  < ctype : Signed.sint Ctypes.typ
  ; of_int : 
    int64 ->
    [> `YICES_ABS
    | `YICES_APP_TERM
    | `YICES_ARITH_CONSTANT
    | `YICES_ARITH_GE_ATOM
    | `YICES_ARITH_ROOT_ATOM
    | `YICES_ARITH_SUM
    | `YICES_BIT_TERM
    | `YICES_BOOL_CONSTANT
    | `YICES_BV_ARRAY
    | `YICES_BV_ASHR
    | `YICES_BV_CONSTANT
    | `YICES_BV_DIV
    | `YICES_BV_GE_ATOM
    | `YICES_BV_LSHR
    | `YICES_BV_REM
    | `YICES_BV_SDIV
    | `YICES_BV_SGE_ATOM
    | `YICES_BV_SHL
    | `YICES_BV_SMOD
    | `YICES_BV_SREM
    | `YICES_BV_SUM
    | `YICES_CEIL
    | `YICES_CONSTRUCTOR_ERROR
    | `YICES_DISTINCT_TERM
    | `YICES_DIVIDES_ATOM
    | `YICES_EQ_TERM
    | `YICES_FLOOR
    | `YICES_FORALL_TERM
    | `YICES_IDIV
    | `YICES_IMOD
    | `YICES_IS_INT_ATOM
    | `YICES_ITE_TERM
    | `YICES_LAMBDA_TERM
    | `YICES_NOT_TERM
    | `YICES_OR_TERM
    | `YICES_POWER_PRODUCT
    | `YICES_RDIV
    | `YICES_SCALAR_CONSTANT
    | `YICES_SELECT_TERM
    | `YICES_TUPLE_TERM
    | `YICES_UNINTERPRETED_TERM
    | `YICES_UPDATE_TERM
    | `YICES_VARIABLE
    | `YICES_XOR_TERM ]
  ; to_int : 
    [< `YICES_ABS
    | `YICES_APP_TERM
    | `YICES_ARITH_CONSTANT
    | `YICES_ARITH_GE_ATOM
    | `YICES_ARITH_ROOT_ATOM
    | `YICES_ARITH_SUM
    | `YICES_BIT_TERM
    | `YICES_BOOL_CONSTANT
    | `YICES_BV_ARRAY
    | `YICES_BV_ASHR
    | `YICES_BV_CONSTANT
    | `YICES_BV_DIV
    | `YICES_BV_GE_ATOM
    | `YICES_BV_LSHR
    | `YICES_BV_REM
    | `YICES_BV_SDIV
    | `YICES_BV_SGE_ATOM
    | `YICES_BV_SHL
    | `YICES_BV_SMOD
    | `YICES_BV_SREM
    | `YICES_BV_SUM
    | `YICES_CEIL
    | `YICES_CONSTRUCTOR_ERROR
    | `YICES_DISTINCT_TERM
    | `YICES_DIVIDES_ATOM
    | `YICES_EQ_TERM
    | `YICES_FLOOR
    | `YICES_FORALL_TERM
    | `YICES_IDIV
    | `YICES_IMOD
    | `YICES_IS_INT_ATOM
    | `YICES_ITE_TERM
    | `YICES_LAMBDA_TERM
    | `YICES_NOT_TERM
    | `YICES_OR_TERM
    | `YICES_POWER_PRODUCT
    | `YICES_RDIV
    | `YICES_SCALAR_CONSTANT
    | `YICES_SELECT_TERM
    | `YICES_TUPLE_TERM
    | `YICES_UNINTERPRETED_TERM
    | `YICES_UPDATE_TERM
    | `YICES_VARIABLE
    | `YICES_XOR_TERM ] ->
    int64 >

val term_constructor_t : Signed.sint Ctypes.typ

val yval_tag : 
  < ctype : Unsigned.uint Ctypes.typ
  ; of_int : 
    int64 ->
    [> `YVAL_ALGEBRAIC
    | `YVAL_BOOL
    | `YVAL_BV
    | `YVAL_FUNCTION
    | `YVAL_MAPPING
    | `YVAL_RATIONAL
    | `YVAL_SCALAR
    | `YVAL_TUPLE
    | `YVAL_UNKNOWN ]
  ; to_int : 
    [< `YVAL_ALGEBRAIC
    | `YVAL_BOOL
    | `YVAL_BV
    | `YVAL_FUNCTION
    | `YVAL_MAPPING
    | `YVAL_RATIONAL
    | `YVAL_SCALAR
    | `YVAL_TUPLE
    | `YVAL_UNKNOWN ] ->
    int64 >

val yval_tag_t : Unsigned.uint Ctypes.typ

val yval_s : 
  < ctype : [ `yval_s ] Ctypes.structure Ctypes.typ
  ; members : 
    < node_id : (Signed.sint, [ `yval_s ] Ctypes.structure) Ctypes.field
    ; node_tag : (Unsigned.uint, [ `yval_s ] Ctypes.structure) Ctypes.field > >

val yval_t : [ `yval_s ] Ctypes.structure Ctypes.typ

val yval_vector_s : 
  < ctype : [ `yval_vector_s ] Ctypes.structure Ctypes.typ
  ; members : 
    < capacity : 
      (Unsigned.uint, [ `yval_vector_s ] Ctypes.structure) Ctypes.field
    ; data : 
      ([ `yval_s ] Ctypes.structure Ctypes_static.ptr,
        [ `yval_vector_s ] Ctypes.structure)
        Ctypes.field
    ; size : (Unsigned.uint, [ `yval_vector_s ] Ctypes.structure) Ctypes.field > >

val yval_vector_t : [ `yval_vector_s ] Ctypes.structure Ctypes.typ

val yices_gen_mode : 
  < ctype : Unsigned.uint Ctypes.typ
  ; of_int : 
    int64 ->
    [> `YICES_GEN_BY_PROJ | `YICES_GEN_BY_SUBST | `YICES_GEN_DEFAULT ]
  ; to_int : 
    [< `YICES_GEN_BY_PROJ | `YICES_GEN_BY_SUBST | `YICES_GEN_DEFAULT ] ->
    int64 >

val yices_gen_mode_t : Unsigned.uint Ctypes.typ

val error_code : 
  < ctype : Unsigned.uint Ctypes.typ
  ; of_int : 
    int64 ->
    [> `ARITHCONSTANT_REQUIRED
    | `ARITHTERM_REQUIRED
    | `ARITH_ERROR
    | `BAD_TERM_DECREF
    | `BAD_TYPE_DECREF
    | `BITVECTOR_REQUIRED
    | `BVARITH_ERROR
    | `BVTYPE_REQUIRED
    | `CTX_ARITH_NOT_SUPPORTED
    | `CTX_ARITH_SOLVER_EXCEPTION
    | `CTX_ARRAYS_NOT_SUPPORTED
    | `CTX_ARRAY_SOLVER_EXCEPTION
    | `CTX_BV_NOT_SUPPORTED
    | `CTX_BV_SOLVER_EXCEPTION
    | `CTX_DELEGATE_NOT_AVAILABLE
    | `CTX_FORMULA_NOT_IDL
    | `CTX_FORMULA_NOT_RDL
    | `CTX_FREE_VAR_IN_FORMULA
    | `CTX_INVALID_CONFIG
    | `CTX_INVALID_OPERATION
    | `CTX_INVALID_PARAMETER_VALUE
    | `CTX_LAMBDAS_NOT_SUPPORTED
    | `CTX_LOGIC_NOT_SUPPORTED
    | `CTX_NONLINEAR_ARITH_NOT_SUPPORTED
    | `CTX_OPERATION_NOT_SUPPORTED
    | `CTX_QUANTIFIERS_NOT_SUPPORTED
    | `CTX_SCALAR_NOT_SUPPORTED
    | `CTX_TOO_MANY_ARITH_ATOMS
    | `CTX_TOO_MANY_ARITH_VARS
    | `CTX_TOO_MANY_BV_ATOMS
    | `CTX_TOO_MANY_BV_VARS
    | `CTX_TUPLE_NOT_SUPPORTED
    | `CTX_UF_NOT_SUPPORTED
    | `CTX_UNKNOWN_DELEGATE
    | `CTX_UNKNOWN_LOGIC
    | `CTX_UNKNOWN_PARAMETER
    | `CTX_UTYPE_NOT_SUPPORTED
    | `DEGREE_OVERFLOW
    | `DIVISION_BY_ZERO
    | `DUPLICATE_NAME_IN_SCALAR
    | `DUPLICATE_TYPE_VAR
    | `DUPLICATE_VARIABLE
    | `DUPLICATE_VAR_NAME
    | `EMPTY_BITVECTOR
    | `EVAL_CONVERSION_FAILED
    | `EVAL_FAILED
    | `EVAL_FREEVAR_IN_TERM
    | `EVAL_LAMBDA
    | `EVAL_NOT_SUPPORTED
    | `EVAL_NO_IMPLICANT
    | `EVAL_OVERFLOW
    | `EVAL_QUANTIFIER
    | `EVAL_UNKNOWN_TERM
    | `FUNCTION_REQUIRED
    | `INCOMPATIBLE_BVSIZES
    | `INCOMPATIBLE_TYPES
    | `INTEGER_OVERFLOW
    | `INTEGER_REQUIRED
    | `INTERNAL_EXCEPTION
    | `INVALID_BITEXTRACT
    | `INVALID_BITSHIFT
    | `INVALID_BVBIN_FORMAT
    | `INVALID_BVCONSTANT
    | `INVALID_BVEXTRACT
    | `INVALID_BVHEX_FORMAT
    | `INVALID_CONSTANT_INDEX
    | `INVALID_FLOAT_FORMAT
    | `INVALID_MACRO
    | `INVALID_RATIONAL_FORMAT
    | `INVALID_TERM
    | `INVALID_TERM_OP
    | `INVALID_TOKEN
    | `INVALID_TUPLE_INDEX
    | `INVALID_TYPE
    | `INVALID_TYPE_OP
    | `INVALID_VAR_INDEX
    | `MAX_BVSIZE_EXCEEDED
    | `MCSAT_ERROR_UNSUPPORTED_THEORY
    | `MDL_CONSTANT_REQUIRED
    | `MDL_CONSTRUCTION_FAILED
    | `MDL_DUPLICATE_VAR
    | `MDL_FTYPE_NOT_ALLOWED
    | `MDL_GEN_FAILED
    | `MDL_GEN_NONLINEAR
    | `MDL_GEN_TYPE_NOT_SUPPORTED
    | `MDL_UNINT_REQUIRED
    | `NEGATIVE_BVSIZE
    | `NONNEG_INT_REQUIRED
    | `NON_CONSTANT_DIVISOR
    | `NO_ERROR
    | `OUTPUT_ERROR
    | `POS_INT_REQUIRED
    | `RATIONAL_REQUIRED
    | `REDEFINED_TERM_NAME
    | `REDEFINED_TYPE_NAME
    | `SCALAR_OR_UTYPE_REQUIRED
    | `SCALAR_TERM_REQUIRED
    | `SYMBOL_REQUIRED
    | `SYNTAX_ERROR
    | `TOO_MANY_ARGUMENTS
    | `TOO_MANY_MACRO_PARAMS
    | `TOO_MANY_VARS
    | `TUPLE_REQUIRED
    | `TYPE_MISMATCH
    | `TYPE_MISMATCH_IN_DEF
    | `TYPE_REQUIRED
    | `TYPE_VAR_REQUIRED
    | `UNDEFINED_TERM_NAME
    | `UNDEFINED_TYPE_NAME
    | `VARIABLE_REQUIRED
    | `WRONG_NUMBER_OF_ARGUMENTS
    | `YVAL_INVALID_OP
    | `YVAL_NOT_SUPPORTED
    | `YVAL_OVERFLOW ]
  ; to_int : 
    [< `ARITHCONSTANT_REQUIRED
    | `ARITHTERM_REQUIRED
    | `ARITH_ERROR
    | `BAD_TERM_DECREF
    | `BAD_TYPE_DECREF
    | `BITVECTOR_REQUIRED
    | `BVARITH_ERROR
    | `BVTYPE_REQUIRED
    | `CTX_ARITH_NOT_SUPPORTED
    | `CTX_ARITH_SOLVER_EXCEPTION
    | `CTX_ARRAYS_NOT_SUPPORTED
    | `CTX_ARRAY_SOLVER_EXCEPTION
    | `CTX_BV_NOT_SUPPORTED
    | `CTX_BV_SOLVER_EXCEPTION
    | `CTX_DELEGATE_NOT_AVAILABLE
    | `CTX_FORMULA_NOT_IDL
    | `CTX_FORMULA_NOT_RDL
    | `CTX_FREE_VAR_IN_FORMULA
    | `CTX_INVALID_CONFIG
    | `CTX_INVALID_OPERATION
    | `CTX_INVALID_PARAMETER_VALUE
    | `CTX_LAMBDAS_NOT_SUPPORTED
    | `CTX_LOGIC_NOT_SUPPORTED
    | `CTX_NONLINEAR_ARITH_NOT_SUPPORTED
    | `CTX_OPERATION_NOT_SUPPORTED
    | `CTX_QUANTIFIERS_NOT_SUPPORTED
    | `CTX_SCALAR_NOT_SUPPORTED
    | `CTX_TOO_MANY_ARITH_ATOMS
    | `CTX_TOO_MANY_ARITH_VARS
    | `CTX_TOO_MANY_BV_ATOMS
    | `CTX_TOO_MANY_BV_VARS
    | `CTX_TUPLE_NOT_SUPPORTED
    | `CTX_UF_NOT_SUPPORTED
    | `CTX_UNKNOWN_DELEGATE
    | `CTX_UNKNOWN_LOGIC
    | `CTX_UNKNOWN_PARAMETER
    | `CTX_UTYPE_NOT_SUPPORTED
    | `DEGREE_OVERFLOW
    | `DIVISION_BY_ZERO
    | `DUPLICATE_NAME_IN_SCALAR
    | `DUPLICATE_TYPE_VAR
    | `DUPLICATE_VARIABLE
    | `DUPLICATE_VAR_NAME
    | `EMPTY_BITVECTOR
    | `EVAL_CONVERSION_FAILED
    | `EVAL_FAILED
    | `EVAL_FREEVAR_IN_TERM
    | `EVAL_LAMBDA
    | `EVAL_NOT_SUPPORTED
    | `EVAL_NO_IMPLICANT
    | `EVAL_OVERFLOW
    | `EVAL_QUANTIFIER
    | `EVAL_UNKNOWN_TERM
    | `FUNCTION_REQUIRED
    | `INCOMPATIBLE_BVSIZES
    | `INCOMPATIBLE_TYPES
    | `INTEGER_OVERFLOW
    | `INTEGER_REQUIRED
    | `INTERNAL_EXCEPTION
    | `INVALID_BITEXTRACT
    | `INVALID_BITSHIFT
    | `INVALID_BVBIN_FORMAT
    | `INVALID_BVCONSTANT
    | `INVALID_BVEXTRACT
    | `INVALID_BVHEX_FORMAT
    | `INVALID_CONSTANT_INDEX
    | `INVALID_FLOAT_FORMAT
    | `INVALID_MACRO
    | `INVALID_RATIONAL_FORMAT
    | `INVALID_TERM
    | `INVALID_TERM_OP
    | `INVALID_TOKEN
    | `INVALID_TUPLE_INDEX
    | `INVALID_TYPE
    | `INVALID_TYPE_OP
    | `INVALID_VAR_INDEX
    | `MAX_BVSIZE_EXCEEDED
    | `MCSAT_ERROR_UNSUPPORTED_THEORY
    | `MDL_CONSTANT_REQUIRED
    | `MDL_CONSTRUCTION_FAILED
    | `MDL_DUPLICATE_VAR
    | `MDL_FTYPE_NOT_ALLOWED
    | `MDL_GEN_FAILED
    | `MDL_GEN_NONLINEAR
    | `MDL_GEN_TYPE_NOT_SUPPORTED
    | `MDL_UNINT_REQUIRED
    | `NEGATIVE_BVSIZE
    | `NONNEG_INT_REQUIRED
    | `NON_CONSTANT_DIVISOR
    | `NO_ERROR
    | `OUTPUT_ERROR
    | `POS_INT_REQUIRED
    | `RATIONAL_REQUIRED
    | `REDEFINED_TERM_NAME
    | `REDEFINED_TYPE_NAME
    | `SCALAR_OR_UTYPE_REQUIRED
    | `SCALAR_TERM_REQUIRED
    | `SYMBOL_REQUIRED
    | `SYNTAX_ERROR
    | `TOO_MANY_ARGUMENTS
    | `TOO_MANY_MACRO_PARAMS
    | `TOO_MANY_VARS
    | `TUPLE_REQUIRED
    | `TYPE_MISMATCH
    | `TYPE_MISMATCH_IN_DEF
    | `TYPE_REQUIRED
    | `TYPE_VAR_REQUIRED
    | `UNDEFINED_TERM_NAME
    | `UNDEFINED_TYPE_NAME
    | `VARIABLE_REQUIRED
    | `WRONG_NUMBER_OF_ARGUMENTS
    | `YVAL_INVALID_OP
    | `YVAL_NOT_SUPPORTED
    | `YVAL_OVERFLOW ] ->
    int64 >

val error_code_t : Unsigned.uint Ctypes.typ

val error_report_s : 
  < ctype : [ `error_report_s ] Ctypes.structure Ctypes.typ
  ; members : 
    < badval : (Signed.long, [ `error_report_s ] Ctypes.structure) Ctypes.field
    ; code : (Unsigned.uint, [ `error_report_s ] Ctypes.structure) Ctypes.field
    ; column : 
      (Unsigned.uint, [ `error_report_s ] Ctypes.structure) Ctypes.field
    ; line : (Unsigned.uint, [ `error_report_s ] Ctypes.structure) Ctypes.field
    ; term1 : (Signed.sint, [ `error_report_s ] Ctypes.structure) Ctypes.field
    ; term2 : (Signed.sint, [ `error_report_s ] Ctypes.structure) Ctypes.field
    ; type1 : (Signed.sint, [ `error_report_s ] Ctypes.structure) Ctypes.field
    ; type2 : (Signed.sint, [ `error_report_s ] Ctypes.structure) Ctypes.field > >

val error_report_t : [ `error_report_s ] Ctypes.structure Ctypes.typ

val yices_version : char Ctypes_static.ptr Ctypes.ptr

val yices_build_arch : char Ctypes_static.ptr Ctypes.ptr

val yices_build_mode : char Ctypes_static.ptr Ctypes.ptr

val yices_build_date : char Ctypes_static.ptr Ctypes.ptr

val yices_has_mcsat : unit -> Signed.sint

val yices_is_thread_safe : unit -> Signed.sint

val yices_init : unit -> unit

val yices_exit : unit -> unit

val yices_reset : unit -> unit

val yices_free_string : char Ctypes_static.ptr -> unit

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

val yices_error_code : unit -> Unsigned.uint

val yices_error_report : 
  unit ->
  [ `error_report_s ] Ctypes.structure Ctypes_static.ptr

val yices_clear_error : unit -> unit

val yices_print_error : 
  [ `__IO_FILE ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint

val yices_print_error_fd : Signed.sint -> Signed.sint

val yices_error_string : unit -> char Ctypes_static.ptr

val yices_init_term_vector : 
  [ `term_vector_s ] Ctypes.structure Ctypes_static.ptr ->
  unit

val yices_init_type_vector : 
  [ `type_vector_s ] Ctypes.structure Ctypes_static.ptr ->
  unit

val yices_delete_term_vector : 
  [ `term_vector_s ] Ctypes.structure Ctypes_static.ptr ->
  unit

val yices_delete_type_vector : 
  [ `type_vector_s ] Ctypes.structure Ctypes_static.ptr ->
  unit

val yices_reset_term_vector : 
  [ `term_vector_s ] Ctypes.structure Ctypes_static.ptr ->
  unit

val yices_reset_type_vector : 
  [ `type_vector_s ] Ctypes.structure Ctypes_static.ptr ->
  unit

val yices_bool_type : unit -> Signed.sint

val yices_int_type : unit -> Signed.sint

val yices_real_type : unit -> Signed.sint

val yices_bv_type : Unsigned.uint -> Signed.sint

val yices_new_scalar_type : Unsigned.uint -> Signed.sint

val yices_new_uninterpreted_type : unit -> Signed.sint

val yices_tuple_type : 
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_tuple_type1 : Signed.sint -> Signed.sint

val yices_tuple_type2 : Signed.sint -> Signed.sint -> Signed.sint

val yices_tuple_type3 : 
  Signed.sint ->
  Signed.sint ->
  Signed.sint ->
  Signed.sint

val yices_function_type : 
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint ->
  Signed.sint

val yices_function_type1 : Signed.sint -> Signed.sint -> Signed.sint

val yices_function_type2 : 
  Signed.sint ->
  Signed.sint ->
  Signed.sint ->
  Signed.sint

val yices_function_type3 : 
  Signed.sint ->
  Signed.sint ->
  Signed.sint ->
  Signed.sint ->
  Signed.sint

val yices_type_is_bool : Signed.sint -> Signed.sint

val yices_type_is_int : Signed.sint -> Signed.sint

val yices_type_is_real : Signed.sint -> Signed.sint

val yices_type_is_arithmetic : Signed.sint -> Signed.sint

val yices_type_is_bitvector : Signed.sint -> Signed.sint

val yices_type_is_tuple : Signed.sint -> Signed.sint

val yices_type_is_function : Signed.sint -> Signed.sint

val yices_type_is_scalar : Signed.sint -> Signed.sint

val yices_type_is_uninterpreted : Signed.sint -> Signed.sint

val yices_test_subtype : Signed.sint -> Signed.sint -> Signed.sint

val yices_compatible_types : Signed.sint -> Signed.sint -> Signed.sint

val yices_bvtype_size : Signed.sint -> Unsigned.uint

val yices_scalar_type_card : Signed.sint -> Unsigned.uint

val yices_type_num_children : Signed.sint -> Signed.sint

val yices_type_child : Signed.sint -> Signed.sint -> Signed.sint

val yices_type_children : 
  Signed.sint ->
  [ `type_vector_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint

val yices_true : unit -> Signed.sint

val yices_false : unit -> Signed.sint

val yices_constant : Signed.sint -> Signed.sint -> Signed.sint

val yices_new_uninterpreted_term : Signed.sint -> Signed.sint

val yices_new_variable : Signed.sint -> Signed.sint

val yices_application : 
  Signed.sint ->
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_application1 : Signed.sint -> Signed.sint -> Signed.sint

val yices_application2 : 
  Signed.sint ->
  Signed.sint ->
  Signed.sint ->
  Signed.sint

val yices_application3 : 
  Signed.sint ->
  Signed.sint ->
  Signed.sint ->
  Signed.sint ->
  Signed.sint

val yices_ite : Signed.sint -> Signed.sint -> Signed.sint -> Signed.sint

val yices_eq : Signed.sint -> Signed.sint -> Signed.sint

val yices_neq : Signed.sint -> Signed.sint -> Signed.sint

val yices_not : Signed.sint -> Signed.sint

val yices_or : Unsigned.uint -> Signed.sint Ctypes_static.ptr -> Signed.sint

val yices_and : Unsigned.uint -> Signed.sint Ctypes_static.ptr -> Signed.sint

val yices_xor : Unsigned.uint -> Signed.sint Ctypes_static.ptr -> Signed.sint

val yices_or2 : Signed.sint -> Signed.sint -> Signed.sint

val yices_and2 : Signed.sint -> Signed.sint -> Signed.sint

val yices_xor2 : Signed.sint -> Signed.sint -> Signed.sint

val yices_or3 : Signed.sint -> Signed.sint -> Signed.sint -> Signed.sint

val yices_and3 : Signed.sint -> Signed.sint -> Signed.sint -> Signed.sint

val yices_xor3 : Signed.sint -> Signed.sint -> Signed.sint -> Signed.sint

val yices_iff : Signed.sint -> Signed.sint -> Signed.sint

val yices_implies : Signed.sint -> Signed.sint -> Signed.sint

val yices_tuple : Unsigned.uint -> Signed.sint Ctypes_static.ptr -> Signed.sint

val yices_pair : Signed.sint -> Signed.sint -> Signed.sint

val yices_triple : Signed.sint -> Signed.sint -> Signed.sint -> Signed.sint

val yices_select : Unsigned.uint -> Signed.sint -> Signed.sint

val yices_tuple_update : 
  Signed.sint ->
  Unsigned.uint ->
  Signed.sint ->
  Signed.sint

val yices_update : 
  Signed.sint ->
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint ->
  Signed.sint

val yices_update1 : Signed.sint -> Signed.sint -> Signed.sint -> Signed.sint

val yices_update2 : 
  Signed.sint ->
  Signed.sint ->
  Signed.sint ->
  Signed.sint ->
  Signed.sint

val yices_update3 : 
  Signed.sint ->
  Signed.sint ->
  Signed.sint ->
  Signed.sint ->
  Signed.sint ->
  Signed.sint

val yices_distinct : 
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_forall : 
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint ->
  Signed.sint

val yices_exists : 
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint ->
  Signed.sint

val yices_lambda : 
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint ->
  Signed.sint

val yices_zero : unit -> Signed.sint

val yices_int32 : Signed.sint -> Signed.sint

val yices_int64 : Signed.long -> Signed.sint

val yices_rational32 : Signed.sint -> Unsigned.uint -> Signed.sint

val yices_rational64 : Signed.long -> Unsigned.ulong -> Signed.sint

val yices_mpz : Ctypes_zarith.MPZ.ptr -> Signed.sint

val yices_mpq : Ctypes_zarith.MPQ.ptr -> Signed.sint

val yices_parse_rational : char Ctypes_static.ptr -> Signed.sint

val yices_parse_float : char Ctypes_static.ptr -> Signed.sint

val yices_add : Signed.sint -> Signed.sint -> Signed.sint

val yices_sub : Signed.sint -> Signed.sint -> Signed.sint

val yices_neg : Signed.sint -> Signed.sint

val yices_mul : Signed.sint -> Signed.sint -> Signed.sint

val yices_square : Signed.sint -> Signed.sint

val yices_power : Signed.sint -> Unsigned.uint -> Signed.sint

val yices_sum : Unsigned.uint -> Signed.sint Ctypes_static.ptr -> Signed.sint

val yices_product : 
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_division : Signed.sint -> Signed.sint -> Signed.sint

val yices_idiv : Signed.sint -> Signed.sint -> Signed.sint

val yices_imod : Signed.sint -> Signed.sint -> Signed.sint

val yices_divides_atom : Signed.sint -> Signed.sint -> Signed.sint

val yices_is_int_atom : Signed.sint -> Signed.sint

val yices_abs : Signed.sint -> Signed.sint

val yices_floor : Signed.sint -> Signed.sint

val yices_ceil : Signed.sint -> Signed.sint

val yices_poly_int32 : 
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_poly_int64 : 
  Unsigned.uint ->
  Signed.long Ctypes_static.ptr ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_poly_rational32 : 
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Unsigned.uint Ctypes_static.ptr ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_poly_rational64 : 
  Unsigned.uint ->
  Signed.long Ctypes_static.ptr ->
  Unsigned.ulong Ctypes_static.ptr ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_poly_mpz : 
  Unsigned.uint ->
  Ctypes_zarith.MPZ.ptr ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_poly_mpq : 
  Unsigned.uint ->
  Ctypes_zarith.MPQ.ptr ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_arith_eq_atom : Signed.sint -> Signed.sint -> Signed.sint

val yices_arith_neq_atom : Signed.sint -> Signed.sint -> Signed.sint

val yices_arith_geq_atom : Signed.sint -> Signed.sint -> Signed.sint

val yices_arith_leq_atom : Signed.sint -> Signed.sint -> Signed.sint

val yices_arith_gt_atom : Signed.sint -> Signed.sint -> Signed.sint

val yices_arith_lt_atom : Signed.sint -> Signed.sint -> Signed.sint

val yices_arith_eq0_atom : Signed.sint -> Signed.sint

val yices_arith_neq0_atom : Signed.sint -> Signed.sint

val yices_arith_geq0_atom : Signed.sint -> Signed.sint

val yices_arith_leq0_atom : Signed.sint -> Signed.sint

val yices_arith_gt0_atom : Signed.sint -> Signed.sint

val yices_arith_lt0_atom : Signed.sint -> Signed.sint

val yices_bvconst_uint32 : Unsigned.uint -> Unsigned.uint -> Signed.sint

val yices_bvconst_uint64 : Unsigned.uint -> Unsigned.ulong -> Signed.sint

val yices_bvconst_int32 : Unsigned.uint -> Signed.sint -> Signed.sint

val yices_bvconst_int64 : Unsigned.uint -> Signed.long -> Signed.sint

val yices_bvconst_mpz : Unsigned.uint -> Ctypes_zarith.MPZ.ptr -> Signed.sint

val yices_bvconst_zero : Unsigned.uint -> Signed.sint

val yices_bvconst_one : Unsigned.uint -> Signed.sint

val yices_bvconst_minus_one : Unsigned.uint -> Signed.sint

val yices_bvconst_from_array : 
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_parse_bvbin : char Ctypes_static.ptr -> Signed.sint

val yices_parse_bvhex : char Ctypes_static.ptr -> Signed.sint

val yices_bvadd : Signed.sint -> Signed.sint -> Signed.sint

val yices_bvsub : Signed.sint -> Signed.sint -> Signed.sint

val yices_bvneg : Signed.sint -> Signed.sint

val yices_bvmul : Signed.sint -> Signed.sint -> Signed.sint

val yices_bvsquare : Signed.sint -> Signed.sint

val yices_bvpower : Signed.sint -> Unsigned.uint -> Signed.sint

val yices_bvdiv : Signed.sint -> Signed.sint -> Signed.sint

val yices_bvrem : Signed.sint -> Signed.sint -> Signed.sint

val yices_bvsdiv : Signed.sint -> Signed.sint -> Signed.sint

val yices_bvsrem : Signed.sint -> Signed.sint -> Signed.sint

val yices_bvsmod : Signed.sint -> Signed.sint -> Signed.sint

val yices_bvnot : Signed.sint -> Signed.sint

val yices_bvnand : Signed.sint -> Signed.sint -> Signed.sint

val yices_bvnor : Signed.sint -> Signed.sint -> Signed.sint

val yices_bvxnor : Signed.sint -> Signed.sint -> Signed.sint

val yices_bvshl : Signed.sint -> Signed.sint -> Signed.sint

val yices_bvlshr : Signed.sint -> Signed.sint -> Signed.sint

val yices_bvashr : Signed.sint -> Signed.sint -> Signed.sint

val yices_bvand : Unsigned.uint -> Signed.sint Ctypes_static.ptr -> Signed.sint

val yices_bvor : Unsigned.uint -> Signed.sint Ctypes_static.ptr -> Signed.sint

val yices_bvxor : Unsigned.uint -> Signed.sint Ctypes_static.ptr -> Signed.sint

val yices_bvand2 : Signed.sint -> Signed.sint -> Signed.sint

val yices_bvor2 : Signed.sint -> Signed.sint -> Signed.sint

val yices_bvxor2 : Signed.sint -> Signed.sint -> Signed.sint

val yices_bvand3 : Signed.sint -> Signed.sint -> Signed.sint -> Signed.sint

val yices_bvor3 : Signed.sint -> Signed.sint -> Signed.sint -> Signed.sint

val yices_bvxor3 : Signed.sint -> Signed.sint -> Signed.sint -> Signed.sint

val yices_bvsum : Unsigned.uint -> Signed.sint Ctypes_static.ptr -> Signed.sint

val yices_bvproduct : 
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_shift_left0 : Signed.sint -> Unsigned.uint -> Signed.sint

val yices_shift_left1 : Signed.sint -> Unsigned.uint -> Signed.sint

val yices_shift_right0 : Signed.sint -> Unsigned.uint -> Signed.sint

val yices_shift_right1 : Signed.sint -> Unsigned.uint -> Signed.sint

val yices_ashift_right : Signed.sint -> Unsigned.uint -> Signed.sint

val yices_rotate_left : Signed.sint -> Unsigned.uint -> Signed.sint

val yices_rotate_right : Signed.sint -> Unsigned.uint -> Signed.sint

val yices_bvextract : 
  Signed.sint ->
  Unsigned.uint ->
  Unsigned.uint ->
  Signed.sint

val yices_bvconcat2 : Signed.sint -> Signed.sint -> Signed.sint

val yices_bvconcat : 
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_bvrepeat : Signed.sint -> Unsigned.uint -> Signed.sint

val yices_sign_extend : Signed.sint -> Unsigned.uint -> Signed.sint

val yices_zero_extend : Signed.sint -> Unsigned.uint -> Signed.sint

val yices_redand : Signed.sint -> Signed.sint

val yices_redor : Signed.sint -> Signed.sint

val yices_redcomp : Signed.sint -> Signed.sint -> Signed.sint

val yices_bvarray : 
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_bitextract : Signed.sint -> Unsigned.uint -> Signed.sint

val yices_bveq_atom : Signed.sint -> Signed.sint -> Signed.sint

val yices_bvneq_atom : Signed.sint -> Signed.sint -> Signed.sint

val yices_bvge_atom : Signed.sint -> Signed.sint -> Signed.sint

val yices_bvgt_atom : Signed.sint -> Signed.sint -> Signed.sint

val yices_bvle_atom : Signed.sint -> Signed.sint -> Signed.sint

val yices_bvlt_atom : Signed.sint -> Signed.sint -> Signed.sint

val yices_bvsge_atom : Signed.sint -> Signed.sint -> Signed.sint

val yices_bvsgt_atom : Signed.sint -> Signed.sint -> Signed.sint

val yices_bvsle_atom : Signed.sint -> Signed.sint -> Signed.sint

val yices_bvslt_atom : Signed.sint -> Signed.sint -> Signed.sint

val yices_parse_type : char Ctypes_static.ptr -> Signed.sint

val yices_parse_term : char Ctypes_static.ptr -> Signed.sint

val yices_subst_term : 
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint ->
  Signed.sint

val yices_subst_term_array : 
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint Ctypes_static.ptr ->
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_set_type_name : Signed.sint -> char Ctypes_static.ptr -> Signed.sint

val yices_set_term_name : Signed.sint -> char Ctypes_static.ptr -> Signed.sint

val yices_remove_type_name : char Ctypes_static.ptr -> unit

val yices_remove_term_name : char Ctypes_static.ptr -> unit

val yices_get_type_by_name : char Ctypes_static.ptr -> Signed.sint

val yices_get_term_by_name : char Ctypes_static.ptr -> Signed.sint

val yices_clear_type_name : Signed.sint -> Signed.sint

val yices_clear_term_name : Signed.sint -> Signed.sint

val yices_get_type_name : Signed.sint -> char Ctypes_static.ptr

val yices_get_term_name : Signed.sint -> char Ctypes_static.ptr

val yices_type_of_term : Signed.sint -> Signed.sint

val yices_term_is_bool : Signed.sint -> Signed.sint

val yices_term_is_int : Signed.sint -> Signed.sint

val yices_term_is_real : Signed.sint -> Signed.sint

val yices_term_is_arithmetic : Signed.sint -> Signed.sint

val yices_term_is_bitvector : Signed.sint -> Signed.sint

val yices_term_is_tuple : Signed.sint -> Signed.sint

val yices_term_is_function : Signed.sint -> Signed.sint

val yices_term_is_scalar : Signed.sint -> Signed.sint

val yices_term_bitsize : Signed.sint -> Unsigned.uint

val yices_term_is_ground : Signed.sint -> Signed.sint

val yices_term_is_atomic : Signed.sint -> Signed.sint

val yices_term_is_composite : Signed.sint -> Signed.sint

val yices_term_is_projection : Signed.sint -> Signed.sint

val yices_term_is_sum : Signed.sint -> Signed.sint

val yices_term_is_bvsum : Signed.sint -> Signed.sint

val yices_term_is_product : Signed.sint -> Signed.sint

val yices_term_constructor : Signed.sint -> Signed.sint

val yices_term_num_children : Signed.sint -> Signed.sint

val yices_term_child : Signed.sint -> Signed.sint -> Signed.sint

val yices_term_children : 
  Signed.sint ->
  [ `term_vector_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint

val yices_proj_index : Signed.sint -> Signed.sint

val yices_proj_arg : Signed.sint -> Signed.sint

val yices_bool_const_value : 
  Signed.sint ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_bv_const_value : 
  Signed.sint ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_scalar_const_value : 
  Signed.sint ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_rational_const_value : 
  Signed.sint ->
  Ctypes_zarith.MPQ.ptr ->
  Signed.sint

val yices_sum_component : 
  Signed.sint ->
  Signed.sint ->
  Ctypes_zarith.MPQ.ptr ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_bvsum_component : 
  Signed.sint ->
  Signed.sint ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_product_component : 
  Signed.sint ->
  Signed.sint ->
  Signed.sint Ctypes_static.ptr ->
  Unsigned.uint Ctypes_static.ptr ->
  Signed.sint

val yices_num_terms : unit -> Unsigned.uint

val yices_num_types : unit -> Unsigned.uint

val yices_incref_term : Signed.sint -> Signed.sint

val yices_decref_term : Signed.sint -> Signed.sint

val yices_incref_type : Signed.sint -> Signed.sint

val yices_decref_type : Signed.sint -> Signed.sint

val yices_num_posref_terms : unit -> Unsigned.uint

val yices_num_posref_types : unit -> Unsigned.uint

val yices_garbage_collect : 
  Signed.sint Ctypes_static.ptr ->
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Unsigned.uint ->
  Signed.sint ->
  unit

val yices_new_config : 
  unit ->
  [ `ctx_config_s ] Ctypes.structure Ctypes_static.ptr

val yices_free_config : 
  [ `ctx_config_s ] Ctypes.structure Ctypes_static.ptr ->
  unit

val yices_set_config : 
  [ `ctx_config_s ] Ctypes.structure Ctypes_static.ptr ->
  char Ctypes_static.ptr ->
  char Ctypes_static.ptr ->
  Signed.sint

val yices_default_config_for_logic : 
  [ `ctx_config_s ] Ctypes.structure Ctypes_static.ptr ->
  char Ctypes_static.ptr ->
  Signed.sint

val yices_new_context : 
  [ `ctx_config_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `context_s ] Ctypes.structure Ctypes_static.ptr

val yices_free_context : 
  [ `context_s ] Ctypes.structure Ctypes_static.ptr ->
  unit

val yices_context_status : 
  [ `context_s ] Ctypes.structure Ctypes_static.ptr ->
  Unsigned.uint

val yices_reset_context : 
  [ `context_s ] Ctypes.structure Ctypes_static.ptr ->
  unit

val yices_push : 
  [ `context_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint

val yices_pop : 
  [ `context_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint

val yices_context_enable_option : 
  [ `context_s ] Ctypes.structure Ctypes_static.ptr ->
  char Ctypes_static.ptr ->
  Signed.sint

val yices_context_disable_option : 
  [ `context_s ] Ctypes.structure Ctypes_static.ptr ->
  char Ctypes_static.ptr ->
  Signed.sint

val yices_assert_formula : 
  [ `context_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint ->
  Signed.sint

val yices_assert_formulas : 
  [ `context_s ] Ctypes.structure Ctypes_static.ptr ->
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_check_context : 
  [ `context_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `param_s ] Ctypes.structure Ctypes_static.ptr ->
  Unsigned.uint

val yices_check_context_with_assumptions : 
  [ `context_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `param_s ] Ctypes.structure Ctypes_static.ptr ->
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Unsigned.uint

val yices_assert_blocking_clause : 
  [ `context_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint

val yices_stop_search : 
  [ `context_s ] Ctypes.structure Ctypes_static.ptr ->
  unit

val yices_new_param_record : 
  unit ->
  [ `param_s ] Ctypes.structure Ctypes_static.ptr

val yices_default_params_for_context : 
  [ `context_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `param_s ] Ctypes.structure Ctypes_static.ptr ->
  unit

val yices_set_param : 
  [ `param_s ] Ctypes.structure Ctypes_static.ptr ->
  char Ctypes_static.ptr ->
  char Ctypes_static.ptr ->
  Signed.sint

val yices_free_param_record : 
  [ `param_s ] Ctypes.structure Ctypes_static.ptr ->
  unit

val yices_get_unsat_core : 
  [ `context_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `term_vector_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint

val yices_get_model : 
  [ `context_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint ->
  [ `model_s ] Ctypes.structure Ctypes_static.ptr

val yices_free_model : [ `model_s ] Ctypes.structure Ctypes_static.ptr -> unit

val yices_model_from_map : 
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint Ctypes_static.ptr ->
  [ `model_s ] Ctypes.structure Ctypes_static.ptr

val yices_model_collect_defined_terms : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `term_vector_s ] Ctypes.structure Ctypes_static.ptr ->
  unit

val yices_check_formula : 
  Signed.sint ->
  char Ctypes_static.ptr ->
  [ `model_s ] Ctypes.structure Ctypes_static.ptr Ctypes_static.ptr ->
  char Ctypes_static.ptr ->
  Unsigned.uint

val yices_check_formulas : 
  Signed.sint Ctypes_static.ptr ->
  Unsigned.uint ->
  char Ctypes_static.ptr ->
  [ `model_s ] Ctypes.structure Ctypes_static.ptr Ctypes_static.ptr ->
  char Ctypes_static.ptr ->
  Unsigned.uint

val yices_has_delegate : char Ctypes_static.ptr -> Signed.sint

val yices_export_formula_to_dimacs : 
  Signed.sint ->
  char Ctypes_static.ptr ->
  Signed.sint ->
  Unsigned.uint Ctypes_static.ptr ->
  Signed.sint

val yices_export_formulas_to_dimacs : 
  Signed.sint Ctypes_static.ptr ->
  Unsigned.uint ->
  char Ctypes_static.ptr ->
  Signed.sint ->
  Unsigned.uint Ctypes_static.ptr ->
  Signed.sint

val yices_get_bool_value : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_get_int32_value : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_get_int64_value : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint ->
  Signed.long Ctypes_static.ptr ->
  Signed.sint

val yices_get_rational32_value : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint ->
  Signed.sint Ctypes_static.ptr ->
  Unsigned.uint Ctypes_static.ptr ->
  Signed.sint

val yices_get_rational64_value : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint ->
  Signed.long Ctypes_static.ptr ->
  Unsigned.ulong Ctypes_static.ptr ->
  Signed.sint

val yices_get_double_value : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint ->
  float Ctypes_static.ptr ->
  Signed.sint

val yices_get_mpz_value : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint ->
  Ctypes_zarith.MPZ.ptr ->
  Signed.sint

val yices_get_mpq_value : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint ->
  Ctypes_zarith.MPQ.ptr ->
  Signed.sint

val yices_get_bv_value : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_get_scalar_value : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_init_yval_vector : 
  [ `yval_vector_s ] Ctypes.structure Ctypes_static.ptr ->
  unit

val yices_delete_yval_vector : 
  [ `yval_vector_s ] Ctypes.structure Ctypes_static.ptr ->
  unit

val yices_reset_yval_vector : 
  [ `yval_vector_s ] Ctypes.structure Ctypes_static.ptr ->
  unit

val yices_get_value : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint ->
  [ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint

val yices_val_is_int32 : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint

val yices_val_is_int64 : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint

val yices_val_is_rational32 : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint

val yices_val_is_rational64 : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint

val yices_val_is_integer : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint

val yices_val_bitsize : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
  Unsigned.uint

val yices_val_tuple_arity : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
  Unsigned.uint

val yices_val_mapping_arity : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
  Unsigned.uint

val yices_val_function_arity : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
  Unsigned.uint

val yices_val_function_type : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint

val yices_val_get_bool : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_val_get_int32 : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_val_get_int64 : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.long Ctypes_static.ptr ->
  Signed.sint

val yices_val_get_rational32 : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint Ctypes_static.ptr ->
  Unsigned.uint Ctypes_static.ptr ->
  Signed.sint

val yices_val_get_rational64 : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.long Ctypes_static.ptr ->
  Unsigned.ulong Ctypes_static.ptr ->
  Signed.sint

val yices_val_get_double : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
  float Ctypes_static.ptr ->
  Signed.sint

val yices_val_get_mpz : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
  Ctypes_zarith.MPZ.ptr ->
  Signed.sint

val yices_val_get_mpq : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
  Ctypes_zarith.MPQ.ptr ->
  Signed.sint

val yices_val_get_bv : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_val_get_scalar : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_val_expand_tuple : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint

val yices_val_expand_function : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `yval_vector_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint

val yices_val_expand_mapping : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
  [ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint

val yices_formula_true_in_model : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint ->
  Signed.sint

val yices_formulas_true_in_model : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_get_value_as_term : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint ->
  Signed.sint

val yices_term_array_value : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_model_term_support : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint ->
  [ `term_vector_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint

val yices_model_term_array_support : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  [ `term_vector_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint

val yices_implicant_for_formula : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint ->
  [ `term_vector_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint

val yices_implicant_for_formulas : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  [ `term_vector_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint

val yices_generalize_model : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint ->
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Unsigned.uint ->
  [ `term_vector_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint

val yices_generalize_model_array : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Unsigned.uint ->
  [ `term_vector_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint

val yices_pp_type : 
  [ `__IO_FILE ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint ->
  Unsigned.uint ->
  Unsigned.uint ->
  Unsigned.uint ->
  Signed.sint

val yices_pp_term : 
  [ `__IO_FILE ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint ->
  Unsigned.uint ->
  Unsigned.uint ->
  Unsigned.uint ->
  Signed.sint

val yices_pp_term_array : 
  [ `__IO_FILE ] Ctypes.structure Ctypes_static.ptr ->
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Unsigned.uint ->
  Unsigned.uint ->
  Unsigned.uint ->
  Signed.sint ->
  Signed.sint

val yices_print_model : 
  [ `__IO_FILE ] Ctypes.structure Ctypes_static.ptr ->
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  unit

val yices_pp_model : 
  [ `__IO_FILE ] Ctypes.structure Ctypes_static.ptr ->
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  Unsigned.uint ->
  Unsigned.uint ->
  Unsigned.uint ->
  Signed.sint

val yices_print_term_values : 
  [ `__IO_FILE ] Ctypes.structure Ctypes_static.ptr ->
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_pp_term_values : 
  [ `__IO_FILE ] Ctypes.structure Ctypes_static.ptr ->
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Unsigned.uint ->
  Unsigned.uint ->
  Unsigned.uint ->
  Signed.sint

val yices_pp_type_fd : 
  Signed.sint ->
  Signed.sint ->
  Unsigned.uint ->
  Unsigned.uint ->
  Unsigned.uint ->
  Signed.sint

val yices_pp_term_fd : 
  Signed.sint ->
  Signed.sint ->
  Unsigned.uint ->
  Unsigned.uint ->
  Unsigned.uint ->
  Signed.sint

val yices_pp_term_array_fd : 
  Signed.sint ->
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Unsigned.uint ->
  Unsigned.uint ->
  Unsigned.uint ->
  Signed.sint ->
  Signed.sint

val yices_print_model_fd : 
  Signed.sint ->
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  Signed.sint

val yices_pp_model_fd : 
  Signed.sint ->
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  Unsigned.uint ->
  Unsigned.uint ->
  Unsigned.uint ->
  Signed.sint

val yices_print_term_values_fd : 
  Signed.sint ->
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Signed.sint

val yices_pp_term_values_fd : 
  Signed.sint ->
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  Unsigned.uint ->
  Signed.sint Ctypes_static.ptr ->
  Unsigned.uint ->
  Unsigned.uint ->
  Unsigned.uint ->
  Signed.sint

val yices_type_to_string : 
  Signed.sint ->
  Unsigned.uint ->
  Unsigned.uint ->
  Unsigned.uint ->
  char Ctypes_static.ptr

val yices_term_to_string : 
  Signed.sint ->
  Unsigned.uint ->
  Unsigned.uint ->
  Unsigned.uint ->
  char Ctypes_static.ptr

val yices_model_to_string : 
  [ `model_s ] Ctypes.structure Ctypes_static.ptr ->
  Unsigned.uint ->
  Unsigned.uint ->
  Unsigned.uint ->
  char Ctypes_static.ptr

package yices2_bindings