package yices2_bindings

  1. Overview
  2. Docs
module FILE : sig ... end
type context_t = [ `context_s ] Ctypes.structure
type model_t = [ `model_s ] Ctypes.structure
type ctx_config_t = [ `ctx_config_s ] Ctypes.structure
type param_t = [ `param_s ] Ctypes.structure
type term_vector_t = [ `term_vector_s ] Ctypes.structure
type type_vector_t = [ `type_vector_s ] Ctypes.structure
type yval_t = [ `yval_s ] Ctypes.structure
type yval_vector_t = [ `yval_vector_s ] Ctypes.structure
type error_report_t = [ `error_report_s ] Ctypes.structure
type smt_status = [
  1. | `STATUS_ERROR
  2. | `STATUS_IDLE
  3. | `STATUS_INTERRUPTED
  4. | `STATUS_SAT
  5. | `STATUS_SEARCHING
  6. | `STATUS_UNKNOWN
  7. | `STATUS_UNSAT
]
val equal_smt_status : smt_status -> smt_status -> Ppx_deriving_runtime.bool
val show_smt_status : smt_status -> Ppx_deriving_runtime.string
type term_constructor = [
  1. | `YICES_ABS
  2. | `YICES_APP_TERM
  3. | `YICES_ARITH_CONSTANT
  4. | `YICES_ARITH_GE_ATOM
  5. | `YICES_ARITH_ROOT_ATOM
  6. | `YICES_ARITH_SUM
  7. | `YICES_BIT_TERM
  8. | `YICES_BOOL_CONSTANT
  9. | `YICES_BV_ARRAY
  10. | `YICES_BV_ASHR
  11. | `YICES_BV_CONSTANT
  12. | `YICES_BV_DIV
  13. | `YICES_BV_GE_ATOM
  14. | `YICES_BV_LSHR
  15. | `YICES_BV_REM
  16. | `YICES_BV_SDIV
  17. | `YICES_BV_SGE_ATOM
  18. | `YICES_BV_SHL
  19. | `YICES_BV_SMOD
  20. | `YICES_BV_SREM
  21. | `YICES_BV_SUM
  22. | `YICES_CEIL
  23. | `YICES_CONSTRUCTOR_ERROR
  24. | `YICES_DISTINCT_TERM
  25. | `YICES_DIVIDES_ATOM
  26. | `YICES_EQ_TERM
  27. | `YICES_FLOOR
  28. | `YICES_FORALL_TERM
  29. | `YICES_IDIV
  30. | `YICES_IMOD
  31. | `YICES_IS_INT_ATOM
  32. | `YICES_ITE_TERM
  33. | `YICES_LAMBDA_TERM
  34. | `YICES_NOT_TERM
  35. | `YICES_OR_TERM
  36. | `YICES_POWER_PRODUCT
  37. | `YICES_RDIV
  38. | `YICES_SCALAR_CONSTANT
  39. | `YICES_SELECT_TERM
  40. | `YICES_TUPLE_TERM
  41. | `YICES_UNINTERPRETED_TERM
  42. | `YICES_UPDATE_TERM
  43. | `YICES_VARIABLE
  44. | `YICES_XOR_TERM
]
val show_term_constructor : term_constructor -> Ppx_deriving_runtime.string
type yval_tag = [
  1. | `YVAL_ALGEBRAIC
  2. | `YVAL_BOOL
  3. | `YVAL_BV
  4. | `YVAL_FUNCTION
  5. | `YVAL_MAPPING
  6. | `YVAL_RATIONAL
  7. | `YVAL_SCALAR
  8. | `YVAL_TUPLE
  9. | `YVAL_UNKNOWN
]
val equal_yval_tag : yval_tag -> yval_tag -> Ppx_deriving_runtime.bool
val show_yval_tag : yval_tag -> Ppx_deriving_runtime.string
type yices_gen_mode = [
  1. | `YICES_GEN_BY_PROJ
  2. | `YICES_GEN_BY_SUBST
  3. | `YICES_GEN_DEFAULT
]
val show_yices_gen_mode : yices_gen_mode -> Ppx_deriving_runtime.string
type error_code = [
  1. | `ARITHCONSTANT_REQUIRED
  2. | `ARITHTERM_REQUIRED
  3. | `ARITH_ERROR
  4. | `BAD_TERM_DECREF
  5. | `BAD_TYPE_DECREF
  6. | `BITVECTOR_REQUIRED
  7. | `BVARITH_ERROR
  8. | `BVTYPE_REQUIRED
  9. | `CTX_ARITH_NOT_SUPPORTED
  10. | `CTX_ARITH_SOLVER_EXCEPTION
  11. | `CTX_ARRAYS_NOT_SUPPORTED
  12. | `CTX_ARRAY_SOLVER_EXCEPTION
  13. | `CTX_BV_NOT_SUPPORTED
  14. | `CTX_BV_SOLVER_EXCEPTION
  15. | `CTX_DELEGATE_NOT_AVAILABLE
  16. | `CTX_FORMULA_NOT_IDL
  17. | `CTX_FORMULA_NOT_RDL
  18. | `CTX_FREE_VAR_IN_FORMULA
  19. | `CTX_INVALID_CONFIG
  20. | `CTX_INVALID_OPERATION
  21. | `CTX_INVALID_PARAMETER_VALUE
  22. | `CTX_LAMBDAS_NOT_SUPPORTED
  23. | `CTX_LOGIC_NOT_SUPPORTED
  24. | `CTX_NONLINEAR_ARITH_NOT_SUPPORTED
  25. | `CTX_OPERATION_NOT_SUPPORTED
  26. | `CTX_QUANTIFIERS_NOT_SUPPORTED
  27. | `CTX_SCALAR_NOT_SUPPORTED
  28. | `CTX_TOO_MANY_ARITH_ATOMS
  29. | `CTX_TOO_MANY_ARITH_VARS
  30. | `CTX_TOO_MANY_BV_ATOMS
  31. | `CTX_TOO_MANY_BV_VARS
  32. | `CTX_TUPLE_NOT_SUPPORTED
  33. | `CTX_UF_NOT_SUPPORTED
  34. | `CTX_UNKNOWN_DELEGATE
  35. | `CTX_UNKNOWN_LOGIC
  36. | `CTX_UNKNOWN_PARAMETER
  37. | `CTX_UTYPE_NOT_SUPPORTED
  38. | `DEGREE_OVERFLOW
  39. | `DIVISION_BY_ZERO
  40. | `DUPLICATE_NAME_IN_SCALAR
  41. | `DUPLICATE_TYPE_VAR
  42. | `DUPLICATE_VARIABLE
  43. | `DUPLICATE_VAR_NAME
  44. | `EMPTY_BITVECTOR
  45. | `EVAL_CONVERSION_FAILED
  46. | `EVAL_FAILED
  47. | `EVAL_FREEVAR_IN_TERM
  48. | `EVAL_LAMBDA
  49. | `EVAL_NOT_SUPPORTED
  50. | `EVAL_NO_IMPLICANT
  51. | `EVAL_OVERFLOW
  52. | `EVAL_QUANTIFIER
  53. | `EVAL_UNKNOWN_TERM
  54. | `FUNCTION_REQUIRED
  55. | `INCOMPATIBLE_BVSIZES
  56. | `INCOMPATIBLE_TYPES
  57. | `INTEGER_OVERFLOW
  58. | `INTEGER_REQUIRED
  59. | `INTERNAL_EXCEPTION
  60. | `INVALID_BITEXTRACT
  61. | `INVALID_BITSHIFT
  62. | `INVALID_BVBIN_FORMAT
  63. | `INVALID_BVCONSTANT
  64. | `INVALID_BVEXTRACT
  65. | `INVALID_BVHEX_FORMAT
  66. | `INVALID_CONSTANT_INDEX
  67. | `INVALID_FLOAT_FORMAT
  68. | `INVALID_MACRO
  69. | `INVALID_RATIONAL_FORMAT
  70. | `INVALID_TERM
  71. | `INVALID_TERM_OP
  72. | `INVALID_TOKEN
  73. | `INVALID_TUPLE_INDEX
  74. | `INVALID_TYPE
  75. | `INVALID_TYPE_OP
  76. | `INVALID_VAR_INDEX
  77. | `MAX_BVSIZE_EXCEEDED
  78. | `MCSAT_ERROR_UNSUPPORTED_THEORY
  79. | `MDL_CONSTANT_REQUIRED
  80. | `MDL_CONSTRUCTION_FAILED
  81. | `MDL_DUPLICATE_VAR
  82. | `MDL_FTYPE_NOT_ALLOWED
  83. | `MDL_GEN_FAILED
  84. | `MDL_GEN_NONLINEAR
  85. | `MDL_GEN_TYPE_NOT_SUPPORTED
  86. | `MDL_UNINT_REQUIRED
  87. | `NEGATIVE_BVSIZE
  88. | `NONNEG_INT_REQUIRED
  89. | `NON_CONSTANT_DIVISOR
  90. | `NO_ERROR
  91. | `OUTPUT_ERROR
  92. | `POS_INT_REQUIRED
  93. | `RATIONAL_REQUIRED
  94. | `REDEFINED_TERM_NAME
  95. | `REDEFINED_TYPE_NAME
  96. | `SCALAR_OR_UTYPE_REQUIRED
  97. | `SCALAR_TERM_REQUIRED
  98. | `SYMBOL_REQUIRED
  99. | `SYNTAX_ERROR
  100. | `TOO_MANY_ARGUMENTS
  101. | `TOO_MANY_MACRO_PARAMS
  102. | `TOO_MANY_VARS
  103. | `TUPLE_REQUIRED
  104. | `TYPE_MISMATCH
  105. | `TYPE_MISMATCH_IN_DEF
  106. | `TYPE_REQUIRED
  107. | `TYPE_VAR_REQUIRED
  108. | `UNDEFINED_TERM_NAME
  109. | `UNDEFINED_TYPE_NAME
  110. | `VARIABLE_REQUIRED
  111. | `WRONG_NUMBER_OF_ARGUMENTS
  112. | `YVAL_INVALID_OP
  113. | `YVAL_NOT_SUPPORTED
  114. | `YVAL_OVERFLOW
]
val equal_error_code : error_code -> error_code -> Ppx_deriving_runtime.bool
val show_error_code : error_code -> Ppx_deriving_runtime.string
type (!'a, !'b) converter = ('a, 'b) Yices2_low_types.BaseTypes.converter = {
  1. read : 'a -> 'b;
  2. write : 'b -> 'a;
}
type _ sintbase
type _ uintbase
val hash_sint : 'a sintbase -> int
val hash_uint : 'a uintbase -> int
type uint_t = [ `uint_t ] uintbase
val equal_uint_t : uint_t -> uint_t -> Ppx_deriving_runtime.bool
val compare_uint_t : uint_t -> uint_t -> Ppx_deriving_runtime.int
type sint_t = [ `sint_t ] sintbase
val equal_sint_t : sint_t -> sint_t -> Ppx_deriving_runtime.bool
val compare_sint_t : sint_t -> sint_t -> Ppx_deriving_runtime.int
type unit_t = [ `unit_t ] sintbase
val equal_unit_t : unit_t -> unit_t -> Ppx_deriving_runtime.bool
val compare_unit_t : unit_t -> unit_t -> Ppx_deriving_runtime.int
type bool_t = [ `bool_t ] sintbase
val equal_bool_t : bool_t -> bool_t -> Ppx_deriving_runtime.bool
val compare_bool_t : bool_t -> bool_t -> Ppx_deriving_runtime.int
type term_t = [ `term_t ] sintbase
val equal_term_t : term_t -> term_t -> Ppx_deriving_runtime.bool
val compare_term_t : term_t -> term_t -> Ppx_deriving_runtime.int
type type_t = [ `type_t ] sintbase
val equal_type_t : type_t -> type_t -> Ppx_deriving_runtime.bool
val compare_type_t : type_t -> type_t -> Ppx_deriving_runtime.int
type smt_status_t
val equal_smt_status_t : smt_status_t -> smt_status_t -> Ppx_deriving_runtime.bool
val compare_smt_status_t : smt_status_t -> smt_status_t -> Ppx_deriving_runtime.int
type term_constructor_t = [ `term_constructor_t ] sintbase
val compare_term_constructor_t : term_constructor_t -> term_constructor_t -> Ppx_deriving_runtime.int
type yval_tag_t
val equal_yval_tag_t : yval_tag_t -> yval_tag_t -> Ppx_deriving_runtime.bool
val compare_yval_tag_t : yval_tag_t -> yval_tag_t -> Ppx_deriving_runtime.int
type yices_gen_mode_t
val compare_yices_gen_mode_t : yices_gen_mode_t -> yices_gen_mode_t -> Ppx_deriving_runtime.int
type error_code_t
val equal_error_code_t : error_code_t -> error_code_t -> Ppx_deriving_runtime.bool
val compare_error_code_t : error_code_t -> error_code_t -> Ppx_deriving_runtime.int