module TMP : sig ... endval anonymous_2 : [ `anonymous ] Ctypes.structure Ctypes.typval anonymous_3 : [ `anonymous_0 ] Ctypes.union Ctypes.typval anonymous_4 : [ `anonymous_1 ] Ctypes.structure Ctypes.typval _G_fpos_t_0 : [ `_G_fpos_t ] Ctypes.structure Ctypes.typval _G_fpos64_t_0 : [ `_G_fpos64_t ] Ctypes.structure Ctypes.typval _IO_marker_0 : [ `_IO_marker ] Ctypes.structure Ctypes.typval _IO_codecvt_0 : [ `_IO_codecvt ] Ctypes.structure Ctypes.typval _IO_wide_data_0 : [ `_IO_wide_data ] Ctypes.structure Ctypes.typval __IO_FILE_0 : [ `__IO_FILE ] Ctypes.structure Ctypes.typval context_s_0 : [ `context_s ] Ctypes.structure Ctypes.typval model_s_0 : [ `model_s ] Ctypes.structure Ctypes.typval ctx_config_s_0 : [ `ctx_config_s ] Ctypes.structure Ctypes.typval param_s_0 : [ `param_s ] Ctypes.structure Ctypes.typval term_vector_s_0 : [ `term_vector_s ] Ctypes.structure Ctypes.typval type_vector_s_0 : [ `type_vector_s ] Ctypes.structure Ctypes.typval yval_s_0 : [ `yval_s ] Ctypes.structure Ctypes.typval yval_vector_s_0 : [ `yval_vector_s ] Ctypes.structure Ctypes.typval error_report_s_0 : [ `error_report_s ] Ctypes.structure Ctypes.typval __u_char : Unsigned.uchar Ctypes.typval __u_short : Unsigned.ushort Ctypes.typval __u_int : Unsigned.uint Ctypes.typval __u_long : Unsigned.ulong Ctypes.typval __int8_t : int Ctypes.typval __uint8_t : Unsigned.uchar Ctypes.typval __int16_t : int Ctypes.typval __uint16_t : Unsigned.ushort Ctypes.typval __int32_t : Signed.sint Ctypes.typval __uint32_t : Unsigned.uint Ctypes.typval __int64_t : Signed.long Ctypes.typval __uint64_t : Unsigned.ulong Ctypes.typval __int_least8_t : int Ctypes.typval __uint_least8_t : Unsigned.uchar Ctypes.typval __int_least16_t : int Ctypes.typval __uint_least16_t : Unsigned.ushort Ctypes.typval __int_least32_t : Signed.sint Ctypes.typval __uint_least32_t : Unsigned.uint Ctypes.typval __int_least64_t : Signed.long Ctypes.typval __uint_least64_t : Unsigned.ulong Ctypes.typval __quad_t : Signed.long Ctypes.typval __u_quad_t : Unsigned.ulong Ctypes.typval __intmax_t : Signed.long Ctypes.typval __uintmax_t : Unsigned.ulong Ctypes.typval __dev_t : Unsigned.ulong Ctypes.typval __uid_t : Unsigned.uint Ctypes.typval __gid_t : Unsigned.uint Ctypes.typval __ino_t : Unsigned.ulong Ctypes.typval __ino64_t : Unsigned.ulong Ctypes.typval __mode_t : Unsigned.uint Ctypes.typval __nlink_t : Unsigned.ulong Ctypes.typval __off_t : Signed.long Ctypes.typval __off64_t : Signed.long Ctypes.typval __pid_t : Signed.sint Ctypes.typval 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.typval __clock_t : Signed.long Ctypes.typval __rlim_t : Unsigned.ulong Ctypes.typval __rlim64_t : Unsigned.ulong Ctypes.typval __id_t : Unsigned.uint Ctypes.typval __time_t : Signed.long Ctypes.typval __useconds_t : Unsigned.uint Ctypes.typval __suseconds_t : Signed.long Ctypes.typval __daddr_t : Signed.sint Ctypes.typval __key_t : Signed.sint Ctypes.typval __clockid_t : Signed.sint Ctypes.typval __timer_t : unit Ctypes_static.ptr Ctypes.typval __blksize_t : Signed.long Ctypes.typval __blkcnt_t : Signed.long Ctypes.typval __blkcnt64_t : Signed.long Ctypes.typval __fsblkcnt_t : Unsigned.ulong Ctypes.typval __fsblkcnt64_t : Unsigned.ulong Ctypes.typval __fsfilcnt_t : Unsigned.ulong Ctypes.typval __fsfilcnt64_t : Unsigned.ulong Ctypes.typval __fsword_t : Signed.long Ctypes.typval __ssize_t : Signed.long Ctypes.typval __syscall_slong_t : Signed.long Ctypes.typval __syscall_ulong_t : Unsigned.ulong Ctypes.typval __loff_t : Signed.long Ctypes.typval __caddr_t : char Ctypes_static.ptr Ctypes.typval __intptr_t : Signed.long Ctypes.typval __socklen_t : Unsigned.uint Ctypes.typval __sig_atomic_t : Signed.sint Ctypes.typval int8_t : int Ctypes.typval int16_t : int Ctypes.typval int32_t : Signed.sint Ctypes.typval int64_t : Signed.long Ctypes.typval uint8_t : Unsigned.uchar Ctypes.typval uint16_t : Unsigned.ushort Ctypes.typval uint32_t : Unsigned.uint Ctypes.typval uint64_t : Unsigned.ulong Ctypes.typval int_least8_t : int Ctypes.typval int_least16_t : int Ctypes.typval int_least32_t : Signed.sint Ctypes.typval int_least64_t : Signed.long Ctypes.typval uint_least8_t : Unsigned.uchar Ctypes.typval uint_least16_t : Unsigned.ushort Ctypes.typval uint_least32_t : Unsigned.uint Ctypes.typval uint_least64_t : Unsigned.ulong Ctypes.typval int_fast8_t : int Ctypes.typval int_fast16_t : Signed.long Ctypes.typval int_fast32_t : Signed.long Ctypes.typval int_fast64_t : Signed.long Ctypes.typval uint_fast8_t : Unsigned.uchar Ctypes.typval uint_fast16_t : Unsigned.ulong Ctypes.typval uint_fast32_t : Unsigned.ulong Ctypes.typval uint_fast64_t : Unsigned.ulong Ctypes.typval intptr_t : Signed.long Ctypes.typval uintptr_t : Unsigned.ulong Ctypes.typval intmax_t : Signed.long Ctypes.typval uintmax_t : Unsigned.ulong Ctypes.typval size_t : Unsigned.ulong Ctypes.typval 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.typval _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.typval _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.typval ___FILE : [ `__IO_FILE ] Ctypes.structure Ctypes.typval _FILE : [ `__IO_FILE ] Ctypes.structure Ctypes.typval _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.typval __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.typval ssize_t : Signed.long Ctypes.typval fpos_t : [ `_G_fpos_t ] Ctypes.structure Ctypes.typval term_t : Signed.sint Ctypes.typval type_t : Signed.sint Ctypes.typval context_s :
< ctype : [ `context_s ] Ctypes.structure Ctypes.typ
; members : < > >val context_t : [ `context_s ] Ctypes.structure Ctypes.typval model_s :
< ctype : [ `model_s ] Ctypes.structure Ctypes.typ
; members : < > >val model_t : [ `model_s ] Ctypes.structure Ctypes.typval ctx_config_s :
< ctype : [ `ctx_config_s ] Ctypes.structure Ctypes.typ
; members : < > >val ctx_config_t : [ `ctx_config_s ] Ctypes.structure Ctypes.typval param_s :
< ctype : [ `param_s ] Ctypes.structure Ctypes.typ
; members : < > >val param_t : [ `param_s ] Ctypes.structure Ctypes.typval 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.typval 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.typval 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.typval 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.typval 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.typval 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.typval 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.typval 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.typval 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.typval 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.typval yices_version : char Ctypes_static.ptr Ctypes.ptrval yices_build_arch : char Ctypes_static.ptr Ctypes.ptrval yices_build_mode : char Ctypes_static.ptr Ctypes.ptrval yices_build_date : char Ctypes_static.ptr Ctypes.ptrval yices_has_mcsat : unit -> Signed.sintval yices_is_thread_safe : unit -> Signed.sintval yices_free_string : char Ctypes_static.ptr -> unitval yices_set_out_of_mem_callback :
(unit -> unit) Ctypes_static.static_funptr ->
unitval yices_error_code : unit -> Unsigned.uintval yices_error_report :
unit ->
[ `error_report_s ] Ctypes.structure Ctypes_static.ptrval yices_print_error :
[ `__IO_FILE ] Ctypes.structure Ctypes_static.ptr ->
Signed.sintval yices_print_error_fd : Signed.sint -> Signed.sintval yices_error_string : unit -> char Ctypes_static.ptrval yices_init_term_vector :
[ `term_vector_s ] Ctypes.structure Ctypes_static.ptr ->
unitval yices_init_type_vector :
[ `type_vector_s ] Ctypes.structure Ctypes_static.ptr ->
unitval yices_delete_term_vector :
[ `term_vector_s ] Ctypes.structure Ctypes_static.ptr ->
unitval yices_delete_type_vector :
[ `type_vector_s ] Ctypes.structure Ctypes_static.ptr ->
unitval yices_reset_term_vector :
[ `term_vector_s ] Ctypes.structure Ctypes_static.ptr ->
unitval yices_reset_type_vector :
[ `type_vector_s ] Ctypes.structure Ctypes_static.ptr ->
unitval yices_bool_type : unit -> Signed.sintval yices_int_type : unit -> Signed.sintval yices_real_type : unit -> Signed.sintval yices_bv_type : Unsigned.uint -> Signed.sintval yices_new_scalar_type : Unsigned.uint -> Signed.sintval yices_new_uninterpreted_type : unit -> Signed.sintval yices_tuple_type :
Unsigned.uint ->
Signed.sint Ctypes_static.ptr ->
Signed.sintval yices_tuple_type1 : Signed.sint -> Signed.sintval yices_tuple_type2 : Signed.sint -> Signed.sint -> Signed.sintval yices_tuple_type3 :
Signed.sint ->
Signed.sint ->
Signed.sint ->
Signed.sintval yices_function_type :
Unsigned.uint ->
Signed.sint Ctypes_static.ptr ->
Signed.sint ->
Signed.sintval yices_function_type1 : Signed.sint -> Signed.sint -> Signed.sintval yices_function_type2 :
Signed.sint ->
Signed.sint ->
Signed.sint ->
Signed.sintval yices_function_type3 :
Signed.sint ->
Signed.sint ->
Signed.sint ->
Signed.sint ->
Signed.sintval yices_type_is_bool : Signed.sint -> Signed.sintval yices_type_is_int : Signed.sint -> Signed.sintval yices_type_is_real : Signed.sint -> Signed.sintval yices_type_is_arithmetic : Signed.sint -> Signed.sintval yices_type_is_bitvector : Signed.sint -> Signed.sintval yices_type_is_tuple : Signed.sint -> Signed.sintval yices_type_is_function : Signed.sint -> Signed.sintval yices_type_is_scalar : Signed.sint -> Signed.sintval yices_type_is_uninterpreted : Signed.sint -> Signed.sintval yices_test_subtype : Signed.sint -> Signed.sint -> Signed.sintval yices_compatible_types : Signed.sint -> Signed.sint -> Signed.sintval yices_bvtype_size : Signed.sint -> Unsigned.uintval yices_scalar_type_card : Signed.sint -> Unsigned.uintval yices_type_num_children : Signed.sint -> Signed.sintval yices_type_child : Signed.sint -> Signed.sint -> Signed.sintval yices_type_children :
Signed.sint ->
[ `type_vector_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sintval yices_true : unit -> Signed.sintval yices_false : unit -> Signed.sintval yices_constant : Signed.sint -> Signed.sint -> Signed.sintval yices_new_uninterpreted_term : Signed.sint -> Signed.sintval yices_new_variable : Signed.sint -> Signed.sintval yices_application :
Signed.sint ->
Unsigned.uint ->
Signed.sint Ctypes_static.ptr ->
Signed.sintval yices_application1 : Signed.sint -> Signed.sint -> Signed.sintval yices_application2 :
Signed.sint ->
Signed.sint ->
Signed.sint ->
Signed.sintval yices_application3 :
Signed.sint ->
Signed.sint ->
Signed.sint ->
Signed.sint ->
Signed.sintval yices_ite : Signed.sint -> Signed.sint -> Signed.sint -> Signed.sintval yices_eq : Signed.sint -> Signed.sint -> Signed.sintval yices_neq : Signed.sint -> Signed.sint -> Signed.sintval yices_not : Signed.sint -> Signed.sintval yices_or : Unsigned.uint -> Signed.sint Ctypes_static.ptr -> Signed.sintval yices_and : Unsigned.uint -> Signed.sint Ctypes_static.ptr -> Signed.sintval yices_xor : Unsigned.uint -> Signed.sint Ctypes_static.ptr -> Signed.sintval yices_or2 : Signed.sint -> Signed.sint -> Signed.sintval yices_and2 : Signed.sint -> Signed.sint -> Signed.sintval yices_xor2 : Signed.sint -> Signed.sint -> Signed.sintval yices_or3 : Signed.sint -> Signed.sint -> Signed.sint -> Signed.sintval yices_and3 : Signed.sint -> Signed.sint -> Signed.sint -> Signed.sintval yices_xor3 : Signed.sint -> Signed.sint -> Signed.sint -> Signed.sintval yices_iff : Signed.sint -> Signed.sint -> Signed.sintval yices_implies : Signed.sint -> Signed.sint -> Signed.sintval yices_tuple : Unsigned.uint -> Signed.sint Ctypes_static.ptr -> Signed.sintval yices_pair : Signed.sint -> Signed.sint -> Signed.sintval yices_triple : Signed.sint -> Signed.sint -> Signed.sint -> Signed.sintval yices_select : Unsigned.uint -> Signed.sint -> Signed.sintval yices_tuple_update :
Signed.sint ->
Unsigned.uint ->
Signed.sint ->
Signed.sintval yices_update :
Signed.sint ->
Unsigned.uint ->
Signed.sint Ctypes_static.ptr ->
Signed.sint ->
Signed.sintval yices_update1 : Signed.sint -> Signed.sint -> Signed.sint -> Signed.sintval yices_update2 :
Signed.sint ->
Signed.sint ->
Signed.sint ->
Signed.sint ->
Signed.sintval yices_update3 :
Signed.sint ->
Signed.sint ->
Signed.sint ->
Signed.sint ->
Signed.sint ->
Signed.sintval yices_distinct :
Unsigned.uint ->
Signed.sint Ctypes_static.ptr ->
Signed.sintval yices_forall :
Unsigned.uint ->
Signed.sint Ctypes_static.ptr ->
Signed.sint ->
Signed.sintval yices_exists :
Unsigned.uint ->
Signed.sint Ctypes_static.ptr ->
Signed.sint ->
Signed.sintval yices_lambda :
Unsigned.uint ->
Signed.sint Ctypes_static.ptr ->
Signed.sint ->
Signed.sintval yices_zero : unit -> Signed.sintval yices_int32 : Signed.sint -> Signed.sintval yices_int64 : Signed.long -> Signed.sintval yices_rational32 : Signed.sint -> Unsigned.uint -> Signed.sintval yices_rational64 : Signed.long -> Unsigned.ulong -> Signed.sintval yices_mpz : Ctypes_zarith.MPZ.ptr -> Signed.sintval yices_mpq : Ctypes_zarith.MPQ.ptr -> Signed.sintval yices_parse_rational : char Ctypes_static.ptr -> Signed.sintval yices_parse_float : char Ctypes_static.ptr -> Signed.sintval yices_add : Signed.sint -> Signed.sint -> Signed.sintval yices_sub : Signed.sint -> Signed.sint -> Signed.sintval yices_neg : Signed.sint -> Signed.sintval yices_mul : Signed.sint -> Signed.sint -> Signed.sintval yices_square : Signed.sint -> Signed.sintval yices_power : Signed.sint -> Unsigned.uint -> Signed.sintval yices_sum : Unsigned.uint -> Signed.sint Ctypes_static.ptr -> Signed.sintval yices_product :
Unsigned.uint ->
Signed.sint Ctypes_static.ptr ->
Signed.sintval yices_division : Signed.sint -> Signed.sint -> Signed.sintval yices_idiv : Signed.sint -> Signed.sint -> Signed.sintval yices_imod : Signed.sint -> Signed.sint -> Signed.sintval yices_divides_atom : Signed.sint -> Signed.sint -> Signed.sintval yices_is_int_atom : Signed.sint -> Signed.sintval yices_abs : Signed.sint -> Signed.sintval yices_floor : Signed.sint -> Signed.sintval yices_ceil : Signed.sint -> Signed.sintval yices_poly_int32 :
Unsigned.uint ->
Signed.sint Ctypes_static.ptr ->
Signed.sint Ctypes_static.ptr ->
Signed.sintval yices_poly_int64 :
Unsigned.uint ->
Signed.long Ctypes_static.ptr ->
Signed.sint Ctypes_static.ptr ->
Signed.sintval yices_poly_rational32 :
Unsigned.uint ->
Signed.sint Ctypes_static.ptr ->
Unsigned.uint Ctypes_static.ptr ->
Signed.sint Ctypes_static.ptr ->
Signed.sintval yices_poly_rational64 :
Unsigned.uint ->
Signed.long Ctypes_static.ptr ->
Unsigned.ulong Ctypes_static.ptr ->
Signed.sint Ctypes_static.ptr ->
Signed.sintval yices_poly_mpz :
Unsigned.uint ->
Ctypes_zarith.MPZ.ptr ->
Signed.sint Ctypes_static.ptr ->
Signed.sintval yices_poly_mpq :
Unsigned.uint ->
Ctypes_zarith.MPQ.ptr ->
Signed.sint Ctypes_static.ptr ->
Signed.sintval yices_arith_eq_atom : Signed.sint -> Signed.sint -> Signed.sintval yices_arith_neq_atom : Signed.sint -> Signed.sint -> Signed.sintval yices_arith_geq_atom : Signed.sint -> Signed.sint -> Signed.sintval yices_arith_leq_atom : Signed.sint -> Signed.sint -> Signed.sintval yices_arith_gt_atom : Signed.sint -> Signed.sint -> Signed.sintval yices_arith_lt_atom : Signed.sint -> Signed.sint -> Signed.sintval yices_arith_eq0_atom : Signed.sint -> Signed.sintval yices_arith_neq0_atom : Signed.sint -> Signed.sintval yices_arith_geq0_atom : Signed.sint -> Signed.sintval yices_arith_leq0_atom : Signed.sint -> Signed.sintval yices_arith_gt0_atom : Signed.sint -> Signed.sintval yices_arith_lt0_atom : Signed.sint -> Signed.sintval yices_bvconst_uint32 : Unsigned.uint -> Unsigned.uint -> Signed.sintval yices_bvconst_uint64 : Unsigned.uint -> Unsigned.ulong -> Signed.sintval yices_bvconst_int32 : Unsigned.uint -> Signed.sint -> Signed.sintval yices_bvconst_int64 : Unsigned.uint -> Signed.long -> Signed.sintval yices_bvconst_mpz : Unsigned.uint -> Ctypes_zarith.MPZ.ptr -> Signed.sintval yices_bvconst_zero : Unsigned.uint -> Signed.sintval yices_bvconst_one : Unsigned.uint -> Signed.sintval yices_bvconst_minus_one : Unsigned.uint -> Signed.sintval yices_bvconst_from_array :
Unsigned.uint ->
Signed.sint Ctypes_static.ptr ->
Signed.sintval yices_parse_bvbin : char Ctypes_static.ptr -> Signed.sintval yices_parse_bvhex : char Ctypes_static.ptr -> Signed.sintval yices_bvadd : Signed.sint -> Signed.sint -> Signed.sintval yices_bvsub : Signed.sint -> Signed.sint -> Signed.sintval yices_bvneg : Signed.sint -> Signed.sintval yices_bvmul : Signed.sint -> Signed.sint -> Signed.sintval yices_bvsquare : Signed.sint -> Signed.sintval yices_bvpower : Signed.sint -> Unsigned.uint -> Signed.sintval yices_bvdiv : Signed.sint -> Signed.sint -> Signed.sintval yices_bvrem : Signed.sint -> Signed.sint -> Signed.sintval yices_bvsdiv : Signed.sint -> Signed.sint -> Signed.sintval yices_bvsrem : Signed.sint -> Signed.sint -> Signed.sintval yices_bvsmod : Signed.sint -> Signed.sint -> Signed.sintval yices_bvnot : Signed.sint -> Signed.sintval yices_bvnand : Signed.sint -> Signed.sint -> Signed.sintval yices_bvnor : Signed.sint -> Signed.sint -> Signed.sintval yices_bvxnor : Signed.sint -> Signed.sint -> Signed.sintval yices_bvshl : Signed.sint -> Signed.sint -> Signed.sintval yices_bvlshr : Signed.sint -> Signed.sint -> Signed.sintval yices_bvashr : Signed.sint -> Signed.sint -> Signed.sintval yices_bvand : Unsigned.uint -> Signed.sint Ctypes_static.ptr -> Signed.sintval yices_bvor : Unsigned.uint -> Signed.sint Ctypes_static.ptr -> Signed.sintval yices_bvxor : Unsigned.uint -> Signed.sint Ctypes_static.ptr -> Signed.sintval yices_bvand2 : Signed.sint -> Signed.sint -> Signed.sintval yices_bvor2 : Signed.sint -> Signed.sint -> Signed.sintval yices_bvxor2 : Signed.sint -> Signed.sint -> Signed.sintval yices_bvand3 : Signed.sint -> Signed.sint -> Signed.sint -> Signed.sintval yices_bvor3 : Signed.sint -> Signed.sint -> Signed.sint -> Signed.sintval yices_bvxor3 : Signed.sint -> Signed.sint -> Signed.sint -> Signed.sintval yices_bvsum : Unsigned.uint -> Signed.sint Ctypes_static.ptr -> Signed.sintval yices_bvproduct :
Unsigned.uint ->
Signed.sint Ctypes_static.ptr ->
Signed.sintval yices_shift_left0 : Signed.sint -> Unsigned.uint -> Signed.sintval yices_shift_left1 : Signed.sint -> Unsigned.uint -> Signed.sintval yices_shift_right0 : Signed.sint -> Unsigned.uint -> Signed.sintval yices_shift_right1 : Signed.sint -> Unsigned.uint -> Signed.sintval yices_ashift_right : Signed.sint -> Unsigned.uint -> Signed.sintval yices_rotate_left : Signed.sint -> Unsigned.uint -> Signed.sintval yices_rotate_right : Signed.sint -> Unsigned.uint -> Signed.sintval yices_bvextract :
Signed.sint ->
Unsigned.uint ->
Unsigned.uint ->
Signed.sintval yices_bvconcat2 : Signed.sint -> Signed.sint -> Signed.sintval yices_bvconcat :
Unsigned.uint ->
Signed.sint Ctypes_static.ptr ->
Signed.sintval yices_bvrepeat : Signed.sint -> Unsigned.uint -> Signed.sintval yices_sign_extend : Signed.sint -> Unsigned.uint -> Signed.sintval yices_zero_extend : Signed.sint -> Unsigned.uint -> Signed.sintval yices_redand : Signed.sint -> Signed.sintval yices_redor : Signed.sint -> Signed.sintval yices_redcomp : Signed.sint -> Signed.sint -> Signed.sintval yices_bvarray :
Unsigned.uint ->
Signed.sint Ctypes_static.ptr ->
Signed.sintval yices_bitextract : Signed.sint -> Unsigned.uint -> Signed.sintval yices_bveq_atom : Signed.sint -> Signed.sint -> Signed.sintval yices_bvneq_atom : Signed.sint -> Signed.sint -> Signed.sintval yices_bvge_atom : Signed.sint -> Signed.sint -> Signed.sintval yices_bvgt_atom : Signed.sint -> Signed.sint -> Signed.sintval yices_bvle_atom : Signed.sint -> Signed.sint -> Signed.sintval yices_bvlt_atom : Signed.sint -> Signed.sint -> Signed.sintval yices_bvsge_atom : Signed.sint -> Signed.sint -> Signed.sintval yices_bvsgt_atom : Signed.sint -> Signed.sint -> Signed.sintval yices_bvsle_atom : Signed.sint -> Signed.sint -> Signed.sintval yices_bvslt_atom : Signed.sint -> Signed.sint -> Signed.sintval yices_parse_type : char Ctypes_static.ptr -> Signed.sintval yices_parse_term : char Ctypes_static.ptr -> Signed.sintval yices_subst_term :
Unsigned.uint ->
Signed.sint Ctypes_static.ptr ->
Signed.sint Ctypes_static.ptr ->
Signed.sint ->
Signed.sintval yices_subst_term_array :
Unsigned.uint ->
Signed.sint Ctypes_static.ptr ->
Signed.sint Ctypes_static.ptr ->
Unsigned.uint ->
Signed.sint Ctypes_static.ptr ->
Signed.sintval yices_set_type_name : Signed.sint -> char Ctypes_static.ptr -> Signed.sintval yices_set_term_name : Signed.sint -> char Ctypes_static.ptr -> Signed.sintval yices_remove_type_name : char Ctypes_static.ptr -> unitval yices_remove_term_name : char Ctypes_static.ptr -> unitval yices_get_type_by_name : char Ctypes_static.ptr -> Signed.sintval yices_get_term_by_name : char Ctypes_static.ptr -> Signed.sintval yices_clear_type_name : Signed.sint -> Signed.sintval yices_clear_term_name : Signed.sint -> Signed.sintval yices_get_type_name : Signed.sint -> char Ctypes_static.ptrval yices_get_term_name : Signed.sint -> char Ctypes_static.ptrval yices_type_of_term : Signed.sint -> Signed.sintval yices_term_is_bool : Signed.sint -> Signed.sintval yices_term_is_int : Signed.sint -> Signed.sintval yices_term_is_real : Signed.sint -> Signed.sintval yices_term_is_arithmetic : Signed.sint -> Signed.sintval yices_term_is_bitvector : Signed.sint -> Signed.sintval yices_term_is_tuple : Signed.sint -> Signed.sintval yices_term_is_function : Signed.sint -> Signed.sintval yices_term_is_scalar : Signed.sint -> Signed.sintval yices_term_bitsize : Signed.sint -> Unsigned.uintval yices_term_is_ground : Signed.sint -> Signed.sintval yices_term_is_atomic : Signed.sint -> Signed.sintval yices_term_is_composite : Signed.sint -> Signed.sintval yices_term_is_projection : Signed.sint -> Signed.sintval yices_term_is_sum : Signed.sint -> Signed.sintval yices_term_is_bvsum : Signed.sint -> Signed.sintval yices_term_is_product : Signed.sint -> Signed.sintval yices_term_constructor : Signed.sint -> Signed.sintval yices_term_num_children : Signed.sint -> Signed.sintval yices_term_child : Signed.sint -> Signed.sint -> Signed.sintval yices_term_children :
Signed.sint ->
[ `term_vector_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sintval yices_proj_index : Signed.sint -> Signed.sintval yices_proj_arg : Signed.sint -> Signed.sintval yices_bool_const_value :
Signed.sint ->
Signed.sint Ctypes_static.ptr ->
Signed.sintval yices_bv_const_value :
Signed.sint ->
Signed.sint Ctypes_static.ptr ->
Signed.sintval yices_scalar_const_value :
Signed.sint ->
Signed.sint Ctypes_static.ptr ->
Signed.sintval yices_rational_const_value :
Signed.sint ->
Ctypes_zarith.MPQ.ptr ->
Signed.sintval yices_sum_component :
Signed.sint ->
Signed.sint ->
Ctypes_zarith.MPQ.ptr ->
Signed.sint Ctypes_static.ptr ->
Signed.sintval yices_bvsum_component :
Signed.sint ->
Signed.sint ->
Signed.sint Ctypes_static.ptr ->
Signed.sint Ctypes_static.ptr ->
Signed.sintval yices_product_component :
Signed.sint ->
Signed.sint ->
Signed.sint Ctypes_static.ptr ->
Unsigned.uint Ctypes_static.ptr ->
Signed.sintval yices_num_terms : unit -> Unsigned.uintval yices_num_types : unit -> Unsigned.uintval yices_incref_term : Signed.sint -> Signed.sintval yices_decref_term : Signed.sint -> Signed.sintval yices_incref_type : Signed.sint -> Signed.sintval yices_decref_type : Signed.sint -> Signed.sintval yices_num_posref_terms : unit -> Unsigned.uintval yices_num_posref_types : unit -> Unsigned.uintval yices_garbage_collect :
Signed.sint Ctypes_static.ptr ->
Unsigned.uint ->
Signed.sint Ctypes_static.ptr ->
Unsigned.uint ->
Signed.sint ->
unitval yices_new_config :
unit ->
[ `ctx_config_s ] Ctypes.structure Ctypes_static.ptrval yices_free_config :
[ `ctx_config_s ] Ctypes.structure Ctypes_static.ptr ->
unitval yices_set_config :
[ `ctx_config_s ] Ctypes.structure Ctypes_static.ptr ->
char Ctypes_static.ptr ->
char Ctypes_static.ptr ->
Signed.sintval yices_default_config_for_logic :
[ `ctx_config_s ] Ctypes.structure Ctypes_static.ptr ->
char Ctypes_static.ptr ->
Signed.sintval yices_new_context :
[ `ctx_config_s ] Ctypes.structure Ctypes_static.ptr ->
[ `context_s ] Ctypes.structure Ctypes_static.ptrval yices_free_context :
[ `context_s ] Ctypes.structure Ctypes_static.ptr ->
unitval yices_context_status :
[ `context_s ] Ctypes.structure Ctypes_static.ptr ->
Unsigned.uintval yices_reset_context :
[ `context_s ] Ctypes.structure Ctypes_static.ptr ->
unitval yices_push :
[ `context_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sintval yices_pop :
[ `context_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sintval yices_context_enable_option :
[ `context_s ] Ctypes.structure Ctypes_static.ptr ->
char Ctypes_static.ptr ->
Signed.sintval yices_context_disable_option :
[ `context_s ] Ctypes.structure Ctypes_static.ptr ->
char Ctypes_static.ptr ->
Signed.sintval yices_assert_formula :
[ `context_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sint ->
Signed.sintval yices_assert_formulas :
[ `context_s ] Ctypes.structure Ctypes_static.ptr ->
Unsigned.uint ->
Signed.sint Ctypes_static.ptr ->
Signed.sintval yices_check_context :
[ `context_s ] Ctypes.structure Ctypes_static.ptr ->
[ `param_s ] Ctypes.structure Ctypes_static.ptr ->
Unsigned.uintval 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.uintval yices_assert_blocking_clause :
[ `context_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sintval yices_stop_search :
[ `context_s ] Ctypes.structure Ctypes_static.ptr ->
unitval yices_new_param_record :
unit ->
[ `param_s ] Ctypes.structure Ctypes_static.ptrval yices_default_params_for_context :
[ `context_s ] Ctypes.structure Ctypes_static.ptr ->
[ `param_s ] Ctypes.structure Ctypes_static.ptr ->
unitval yices_set_param :
[ `param_s ] Ctypes.structure Ctypes_static.ptr ->
char Ctypes_static.ptr ->
char Ctypes_static.ptr ->
Signed.sintval yices_free_param_record :
[ `param_s ] Ctypes.structure Ctypes_static.ptr ->
unitval yices_get_unsat_core :
[ `context_s ] Ctypes.structure Ctypes_static.ptr ->
[ `term_vector_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sintval yices_get_model :
[ `context_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sint ->
[ `model_s ] Ctypes.structure Ctypes_static.ptrval yices_free_model : [ `model_s ] Ctypes.structure Ctypes_static.ptr -> unitval yices_model_from_map :
Unsigned.uint ->
Signed.sint Ctypes_static.ptr ->
Signed.sint Ctypes_static.ptr ->
[ `model_s ] Ctypes.structure Ctypes_static.ptrval yices_model_collect_defined_terms :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
[ `term_vector_s ] Ctypes.structure Ctypes_static.ptr ->
unitval yices_check_formula :
Signed.sint ->
char Ctypes_static.ptr ->
[ `model_s ] Ctypes.structure Ctypes_static.ptr Ctypes_static.ptr ->
char Ctypes_static.ptr ->
Unsigned.uintval 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.uintval yices_has_delegate : char Ctypes_static.ptr -> Signed.sintval yices_export_formula_to_dimacs :
Signed.sint ->
char Ctypes_static.ptr ->
Signed.sint ->
Unsigned.uint Ctypes_static.ptr ->
Signed.sintval yices_export_formulas_to_dimacs :
Signed.sint Ctypes_static.ptr ->
Unsigned.uint ->
char Ctypes_static.ptr ->
Signed.sint ->
Unsigned.uint Ctypes_static.ptr ->
Signed.sintval yices_get_bool_value :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sint ->
Signed.sint Ctypes_static.ptr ->
Signed.sintval yices_get_int32_value :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sint ->
Signed.sint Ctypes_static.ptr ->
Signed.sintval yices_get_int64_value :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sint ->
Signed.long Ctypes_static.ptr ->
Signed.sintval yices_get_rational32_value :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sint ->
Signed.sint Ctypes_static.ptr ->
Unsigned.uint Ctypes_static.ptr ->
Signed.sintval yices_get_rational64_value :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sint ->
Signed.long Ctypes_static.ptr ->
Unsigned.ulong Ctypes_static.ptr ->
Signed.sintval yices_get_double_value :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sint ->
float Ctypes_static.ptr ->
Signed.sintval yices_get_mpz_value :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sint ->
Ctypes_zarith.MPZ.ptr ->
Signed.sintval yices_get_mpq_value :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sint ->
Ctypes_zarith.MPQ.ptr ->
Signed.sintval yices_get_bv_value :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sint ->
Signed.sint Ctypes_static.ptr ->
Signed.sintval yices_get_scalar_value :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sint ->
Signed.sint Ctypes_static.ptr ->
Signed.sintval yices_init_yval_vector :
[ `yval_vector_s ] Ctypes.structure Ctypes_static.ptr ->
unitval yices_delete_yval_vector :
[ `yval_vector_s ] Ctypes.structure Ctypes_static.ptr ->
unitval yices_reset_yval_vector :
[ `yval_vector_s ] Ctypes.structure Ctypes_static.ptr ->
unitval yices_get_value :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sint ->
[ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sintval yices_val_is_int32 :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
[ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sintval yices_val_is_int64 :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
[ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sintval yices_val_is_rational32 :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
[ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sintval yices_val_is_rational64 :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
[ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sintval yices_val_is_integer :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
[ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sintval yices_val_bitsize :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
[ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
Unsigned.uintval yices_val_tuple_arity :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
[ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
Unsigned.uintval yices_val_mapping_arity :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
[ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
Unsigned.uintval yices_val_function_arity :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
[ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
Unsigned.uintval yices_val_function_type :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
[ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sintval yices_val_get_bool :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
[ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sint Ctypes_static.ptr ->
Signed.sintval yices_val_get_int32 :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
[ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sint Ctypes_static.ptr ->
Signed.sintval yices_val_get_int64 :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
[ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.long Ctypes_static.ptr ->
Signed.sintval 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.sintval 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.sintval yices_val_get_double :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
[ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
float Ctypes_static.ptr ->
Signed.sintval yices_val_get_mpz :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
[ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
Ctypes_zarith.MPZ.ptr ->
Signed.sintval yices_val_get_mpq :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
[ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
Ctypes_zarith.MPQ.ptr ->
Signed.sintval yices_val_get_bv :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
[ `yval_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sint Ctypes_static.ptr ->
Signed.sintval 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.sintval 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.sintval 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.sintval 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.sintval yices_formula_true_in_model :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sint ->
Signed.sintval yices_formulas_true_in_model :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
Unsigned.uint ->
Signed.sint Ctypes_static.ptr ->
Signed.sintval yices_get_value_as_term :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sint ->
Signed.sintval yices_term_array_value :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
Unsigned.uint ->
Signed.sint Ctypes_static.ptr ->
Signed.sint Ctypes_static.ptr ->
Signed.sintval yices_model_term_support :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sint ->
[ `term_vector_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sintval 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.sintval yices_implicant_for_formula :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sint ->
[ `term_vector_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sintval 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.sintval 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.sintval 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.sintval yices_pp_type :
[ `__IO_FILE ] Ctypes.structure Ctypes_static.ptr ->
Signed.sint ->
Unsigned.uint ->
Unsigned.uint ->
Unsigned.uint ->
Signed.sintval yices_pp_term :
[ `__IO_FILE ] Ctypes.structure Ctypes_static.ptr ->
Signed.sint ->
Unsigned.uint ->
Unsigned.uint ->
Unsigned.uint ->
Signed.sintval 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.sintval yices_print_model :
[ `__IO_FILE ] Ctypes.structure Ctypes_static.ptr ->
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
unitval yices_pp_model :
[ `__IO_FILE ] Ctypes.structure Ctypes_static.ptr ->
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
Unsigned.uint ->
Unsigned.uint ->
Unsigned.uint ->
Signed.sintval 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.sintval 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.sintval yices_pp_type_fd :
Signed.sint ->
Signed.sint ->
Unsigned.uint ->
Unsigned.uint ->
Unsigned.uint ->
Signed.sintval yices_pp_term_fd :
Signed.sint ->
Signed.sint ->
Unsigned.uint ->
Unsigned.uint ->
Unsigned.uint ->
Signed.sintval yices_pp_term_array_fd :
Signed.sint ->
Unsigned.uint ->
Signed.sint Ctypes_static.ptr ->
Unsigned.uint ->
Unsigned.uint ->
Unsigned.uint ->
Signed.sint ->
Signed.sintval yices_print_model_fd :
Signed.sint ->
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
Signed.sintval yices_pp_model_fd :
Signed.sint ->
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
Unsigned.uint ->
Unsigned.uint ->
Unsigned.uint ->
Signed.sintval yices_print_term_values_fd :
Signed.sint ->
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
Unsigned.uint ->
Signed.sint Ctypes_static.ptr ->
Signed.sintval 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.sintval yices_type_to_string :
Signed.sint ->
Unsigned.uint ->
Unsigned.uint ->
Unsigned.uint ->
char Ctypes_static.ptrval yices_term_to_string :
Signed.sint ->
Unsigned.uint ->
Unsigned.uint ->
Unsigned.uint ->
char Ctypes_static.ptrval yices_model_to_string :
[ `model_s ] Ctypes.structure Ctypes_static.ptr ->
Unsigned.uint ->
Unsigned.uint ->
Unsigned.uint ->
char Ctypes_static.ptr