package yices2

  1. Overview
  2. Docs

Module Yices2.Error

type code =
  1. | NO_ERROR
  2. | INVALID_TYPE
  3. | INVALID_TERM
  4. | INVALID_CONSTANT_INDEX
  5. | INVALID_VAR_INDEX
  6. | INVALID_TUPLE_INDEX
  7. | INVALID_RATIONAL_FORMAT
  8. | INVALID_FLOAT_FORMAT
  9. | INVALID_BVBIN_FORMAT
  10. | INVALID_BVHEX_FORMAT
  11. | INVALID_BITSHIFT
  12. | INVALID_BVEXTRACT
  13. | INVALID_BITEXTRACT
  14. | TOO_MANY_ARGUMENTS
  15. | TOO_MANY_VARS
  16. | MAX_BVSIZE_EXCEEDED
  17. | DEGREE_OVERFLOW
  18. | DIVISION_BY_ZERO
  19. | POS_INT_REQUIRED
  20. | NONNEG_INT_REQUIRED
  21. | SCALAR_OR_UTYPE_REQUIRED
  22. | FUNCTION_REQUIRED
  23. | TUPLE_REQUIRED
  24. | VARIABLE_REQUIRED
  25. | ARITHTERM_REQUIRED
  26. | BITVECTOR_REQUIRED
  27. | SCALAR_TERM_REQUIRED
  28. | WRONG_NUMBER_OF_ARGUMENTS
  29. | TYPE_MISMATCH
  30. | INCOMPATIBLE_TYPES
  31. | DUPLICATE_VARIABLE
  32. | INCOMPATIBLE_BVSIZES
  33. | EMPTY_BITVECTOR
  34. | ARITHCONSTANT_REQUIRED
  35. | INVALID_MACRO
  36. | TOO_MANY_MACRO_PARAMS
  37. | TYPE_VAR_REQUIRED
  38. | DUPLICATE_TYPE_VAR
  39. | BVTYPE_REQUIRED
  40. | BAD_TERM_DECREF
  41. | BAD_TYPE_DECREF
  42. | INVALID_TOKEN
  43. | SYNTAX_ERROR
  44. | UNDEFINED_TYPE_NAME
  45. | UNDEFINED_TERM_NAME
  46. | REDEFINED_TYPE_NAME
  47. | REDEFINED_TERM_NAME
  48. | DUPLICATE_NAME_IN_SCALAR
  49. | DUPLICATE_VAR_NAME
  50. | INTEGER_OVERFLOW
  51. | INTEGER_REQUIRED
  52. | RATIONAL_REQUIRED
  53. | SYMBOL_REQUIRED
  54. | TYPE_REQUIRED
  55. | NON_CONSTANT_DIVISOR
  56. | NEGATIVE_BVSIZE
  57. | INVALID_BVCONSTANT
  58. | TYPE_MISMATCH_IN_DEF
  59. | ARITH_ERROR
  60. | BVARITH_ERROR
  61. | CTX_FREE_VAR_IN_FORMULA
  62. | CTX_LOGIC_NOT_SUPPORTED
  63. | CTX_UF_NOT_SUPPORTED
  64. | CTX_ARITH_NOT_SUPPORTED
  65. | CTX_BV_NOT_SUPPORTED
  66. | CTX_ARRAYS_NOT_SUPPORTED
  67. | CTX_QUANTIFIERS_NOT_SUPPORTED
  68. | CTX_LAMBDAS_NOT_SUPPORTED
  69. | CTX_NONLINEAR_ARITH_NOT_SUPPORTED
  70. | CTX_FORMULA_NOT_IDL
  71. | CTX_FORMULA_NOT_RDL
  72. | CTX_TOO_MANY_ARITH_VARS
  73. | CTX_TOO_MANY_ARITH_ATOMS
  74. | CTX_TOO_MANY_BV_VARS
  75. | CTX_TOO_MANY_BV_ATOMS
  76. | CTX_ARITH_SOLVER_EXCEPTION
  77. | CTX_BV_SOLVER_EXCEPTION
  78. | CTX_ARRAY_SOLVER_EXCEPTION
  79. | CTX_INVALID_OPERATION
  80. | CTX_OPERATION_NOT_SUPPORTED
  81. | CTX_INVALID_CONFIG
  82. | CTX_UNKNOWN_PARAMETER
  83. | CTX_INVALID_PARAMETER_VALUE
  84. | CTX_UNKNOWN_LOGIC
  85. | EVAL_UNKNOWN_TERM
  86. | EVAL_FREEVAR_IN_TERM
  87. | EVAL_QUANTIFIER
  88. | EVAL_LAMBDA
  89. | EVAL_OVERFLOW
  90. | EVAL_FAILED
  91. | EVAL_CONVERSION_FAILED
  92. | EVAL_NO_IMPLICANT
  93. | MDL_UNINT_REQUIRED
  94. | MDL_CONSTANT_REQUIRED
  95. | MDL_DUPLICATE_VAR
  96. | MDL_FTYPE_NOT_ALLOWED
  97. | MDL_CONSTRUCTION_FAILED
  98. | YVAL_INVALID_OP
  99. | YVAL_OVERFLOW
  100. | OUTPUT_ERROR
  101. | INTERNAL_EXCEPTION
type report = {
  1. name : string;
  2. line : int;
  3. column : int;
  4. term1 : term option;
  5. type1 : typ option;
  6. term2 : term option;
  7. type2 : typ option;
  8. badval : int64;
}