Module Z3enums

type lbool =
  1. | L_FALSE
  2. | L_UNDEF
  3. | L_TRUE
val int_of_lbool : lbool -> int
val lbool_of_int : int -> lbool
type symbol_kind =
  1. | INT_SYMBOL
  2. | STRING_SYMBOL
val int_of_symbol_kind : symbol_kind -> int
val symbol_kind_of_int : int -> symbol_kind
type parameter_kind =
  1. | PARAMETER_INT
  2. | PARAMETER_DOUBLE
  3. | PARAMETER_RATIONAL
  4. | PARAMETER_SYMBOL
  5. | PARAMETER_SORT
  6. | PARAMETER_AST
  7. | PARAMETER_FUNC_DECL
  8. | PARAMETER_INTERNAL
  9. | PARAMETER_ZSTRING
val int_of_parameter_kind : parameter_kind -> int
val parameter_kind_of_int : int -> parameter_kind
type sort_kind =
  1. | UNINTERPRETED_SORT
  2. | BOOL_SORT
  3. | INT_SORT
  4. | REAL_SORT
  5. | BV_SORT
  6. | ARRAY_SORT
  7. | DATATYPE_SORT
  8. | RELATION_SORT
  9. | FINITE_DOMAIN_SORT
  10. | FLOATING_POINT_SORT
  11. | ROUNDING_MODE_SORT
  12. | SEQ_SORT
  13. | RE_SORT
  14. | CHAR_SORT
  15. | TYPE_VAR
  16. | UNKNOWN_SORT
val int_of_sort_kind : sort_kind -> int
val sort_kind_of_int : int -> sort_kind
type ast_kind =
  1. | NUMERAL_AST
  2. | APP_AST
  3. | VAR_AST
  4. | QUANTIFIER_AST
  5. | SORT_AST
  6. | FUNC_DECL_AST
  7. | UNKNOWN_AST
val int_of_ast_kind : ast_kind -> int
val ast_kind_of_int : int -> ast_kind
type decl_kind =
  1. | OP_TRUE
  2. | OP_FALSE
  3. | OP_EQ
  4. | OP_DISTINCT
  5. | OP_ITE
  6. | OP_AND
  7. | OP_OR
  8. | OP_IFF
  9. | OP_XOR
  10. | OP_NOT
  11. | OP_IMPLIES
  12. | OP_OEQ
  13. | OP_ANUM
  14. | OP_AGNUM
  15. | OP_LE
  16. | OP_GE
  17. | OP_LT
  18. | OP_GT
  19. | OP_ADD
  20. | OP_SUB
  21. | OP_UMINUS
  22. | OP_MUL
  23. | OP_DIV
  24. | OP_IDIV
  25. | OP_REM
  26. | OP_MOD
  27. | OP_TO_REAL
  28. | OP_TO_INT
  29. | OP_IS_INT
  30. | OP_POWER
  31. | OP_ABS
  32. | OP_STORE
  33. | OP_SELECT
  34. | OP_CONST_ARRAY
  35. | OP_ARRAY_MAP
  36. | OP_ARRAY_DEFAULT
  37. | OP_SET_UNION
  38. | OP_SET_INTERSECT
  39. | OP_SET_DIFFERENCE
  40. | OP_SET_COMPLEMENT
  41. | OP_SET_SUBSET
  42. | OP_AS_ARRAY
  43. | OP_ARRAY_EXT
  44. | OP_BNUM
  45. | OP_BIT1
  46. | OP_BIT0
  47. | OP_BNEG
  48. | OP_BADD
  49. | OP_BSUB
  50. | OP_BMUL
  51. | OP_BSDIV
  52. | OP_BUDIV
  53. | OP_BSREM
  54. | OP_BUREM
  55. | OP_BSMOD
  56. | OP_BSDIV0
  57. | OP_BUDIV0
  58. | OP_BSREM0
  59. | OP_BUREM0
  60. | OP_BSMOD0
  61. | OP_ULEQ
  62. | OP_SLEQ
  63. | OP_UGEQ
  64. | OP_SGEQ
  65. | OP_ULT
  66. | OP_SLT
  67. | OP_UGT
  68. | OP_SGT
  69. | OP_BAND
  70. | OP_BOR
  71. | OP_BNOT
  72. | OP_BXOR
  73. | OP_BNAND
  74. | OP_BNOR
  75. | OP_BXNOR
  76. | OP_CONCAT
  77. | OP_SIGN_EXT
  78. | OP_ZERO_EXT
  79. | OP_EXTRACT
  80. | OP_REPEAT
  81. | OP_BREDOR
  82. | OP_BREDAND
  83. | OP_BCOMP
  84. | OP_BSHL
  85. | OP_BLSHR
  86. | OP_BASHR
  87. | OP_ROTATE_LEFT
  88. | OP_ROTATE_RIGHT
  89. | OP_EXT_ROTATE_LEFT
  90. | OP_EXT_ROTATE_RIGHT
  91. | OP_BIT2BOOL
  92. | OP_INT2BV
  93. | OP_BV2INT
  94. | OP_SBV2INT
  95. | OP_CARRY
  96. | OP_XOR3
  97. | OP_BSMUL_NO_OVFL
  98. | OP_BUMUL_NO_OVFL
  99. | OP_BSMUL_NO_UDFL
  100. | OP_BSDIV_I
  101. | OP_BUDIV_I
  102. | OP_BSREM_I
  103. | OP_BUREM_I
  104. | OP_BSMOD_I
  105. | OP_PR_UNDEF
  106. | OP_PR_TRUE
  107. | OP_PR_ASSERTED
  108. | OP_PR_GOAL
  109. | OP_PR_MODUS_PONENS
  110. | OP_PR_REFLEXIVITY
  111. | OP_PR_SYMMETRY
  112. | OP_PR_TRANSITIVITY
  113. | OP_PR_TRANSITIVITY_STAR
  114. | OP_PR_MONOTONICITY
  115. | OP_PR_QUANT_INTRO
  116. | OP_PR_BIND
  117. | OP_PR_DISTRIBUTIVITY
  118. | OP_PR_AND_ELIM
  119. | OP_PR_NOT_OR_ELIM
  120. | OP_PR_REWRITE
  121. | OP_PR_REWRITE_STAR
  122. | OP_PR_PULL_QUANT
  123. | OP_PR_PUSH_QUANT
  124. | OP_PR_ELIM_UNUSED_VARS
  125. | OP_PR_DER
  126. | OP_PR_QUANT_INST
  127. | OP_PR_HYPOTHESIS
  128. | OP_PR_LEMMA
  129. | OP_PR_UNIT_RESOLUTION
  130. | OP_PR_IFF_TRUE
  131. | OP_PR_IFF_FALSE
  132. | OP_PR_COMMUTATIVITY
  133. | OP_PR_DEF_AXIOM
  134. | OP_PR_ASSUMPTION_ADD
  135. | OP_PR_LEMMA_ADD
  136. | OP_PR_REDUNDANT_DEL
  137. | OP_PR_CLAUSE_TRAIL
  138. | OP_PR_DEF_INTRO
  139. | OP_PR_APPLY_DEF
  140. | OP_PR_IFF_OEQ
  141. | OP_PR_NNF_POS
  142. | OP_PR_NNF_NEG
  143. | OP_PR_SKOLEMIZE
  144. | OP_PR_MODUS_PONENS_OEQ
  145. | OP_PR_TH_LEMMA
  146. | OP_PR_HYPER_RESOLVE
  147. | OP_RA_STORE
  148. | OP_RA_EMPTY
  149. | OP_RA_IS_EMPTY
  150. | OP_RA_JOIN
  151. | OP_RA_UNION
  152. | OP_RA_WIDEN
  153. | OP_RA_PROJECT
  154. | OP_RA_FILTER
  155. | OP_RA_NEGATION_FILTER
  156. | OP_RA_RENAME
  157. | OP_RA_COMPLEMENT
  158. | OP_RA_SELECT
  159. | OP_RA_CLONE
  160. | OP_FD_CONSTANT
  161. | OP_FD_LT
  162. | OP_SEQ_UNIT
  163. | OP_SEQ_EMPTY
  164. | OP_SEQ_CONCAT
  165. | OP_SEQ_PREFIX
  166. | OP_SEQ_SUFFIX
  167. | OP_SEQ_CONTAINS
  168. | OP_SEQ_EXTRACT
  169. | OP_SEQ_REPLACE
  170. | OP_SEQ_REPLACE_RE
  171. | OP_SEQ_REPLACE_RE_ALL
  172. | OP_SEQ_REPLACE_ALL
  173. | OP_SEQ_AT
  174. | OP_SEQ_NTH
  175. | OP_SEQ_LENGTH
  176. | OP_SEQ_INDEX
  177. | OP_SEQ_LAST_INDEX
  178. | OP_SEQ_TO_RE
  179. | OP_SEQ_IN_RE
  180. | OP_SEQ_MAP
  181. | OP_SEQ_MAPI
  182. | OP_SEQ_FOLDL
  183. | OP_SEQ_FOLDLI
  184. | OP_STR_TO_INT
  185. | OP_INT_TO_STR
  186. | OP_UBV_TO_STR
  187. | OP_SBV_TO_STR
  188. | OP_STR_TO_CODE
  189. | OP_STR_FROM_CODE
  190. | OP_STRING_LT
  191. | OP_STRING_LE
  192. | OP_RE_PLUS
  193. | OP_RE_STAR
  194. | OP_RE_OPTION
  195. | OP_RE_CONCAT
  196. | OP_RE_UNION
  197. | OP_RE_RANGE
  198. | OP_RE_DIFF
  199. | OP_RE_INTERSECT
  200. | OP_RE_LOOP
  201. | OP_RE_POWER
  202. | OP_RE_COMPLEMENT
  203. | OP_RE_EMPTY_SET
  204. | OP_RE_FULL_SET
  205. | OP_RE_FULL_CHAR_SET
  206. | OP_RE_OF_PRED
  207. | OP_RE_REVERSE
  208. | OP_RE_DERIVATIVE
  209. | OP_CHAR_CONST
  210. | OP_CHAR_LE
  211. | OP_CHAR_TO_INT
  212. | OP_CHAR_TO_BV
  213. | OP_CHAR_FROM_BV
  214. | OP_CHAR_IS_DIGIT
  215. | OP_LABEL
  216. | OP_LABEL_LIT
  217. | OP_DT_CONSTRUCTOR
  218. | OP_DT_RECOGNISER
  219. | OP_DT_IS
  220. | OP_DT_ACCESSOR
  221. | OP_DT_UPDATE_FIELD
  222. | OP_PB_AT_MOST
  223. | OP_PB_AT_LEAST
  224. | OP_PB_LE
  225. | OP_PB_GE
  226. | OP_PB_EQ
  227. | OP_SPECIAL_RELATION_LO
  228. | OP_SPECIAL_RELATION_PO
  229. | OP_SPECIAL_RELATION_PLO
  230. | OP_SPECIAL_RELATION_TO
  231. | OP_SPECIAL_RELATION_TC
  232. | OP_SPECIAL_RELATION_TRC
  233. | OP_FPA_RM_NEAREST_TIES_TO_EVEN
  234. | OP_FPA_RM_NEAREST_TIES_TO_AWAY
  235. | OP_FPA_RM_TOWARD_POSITIVE
  236. | OP_FPA_RM_TOWARD_NEGATIVE
  237. | OP_FPA_RM_TOWARD_ZERO
  238. | OP_FPA_NUM
  239. | OP_FPA_PLUS_INF
  240. | OP_FPA_MINUS_INF
  241. | OP_FPA_NAN
  242. | OP_FPA_PLUS_ZERO
  243. | OP_FPA_MINUS_ZERO
  244. | OP_FPA_ADD
  245. | OP_FPA_SUB
  246. | OP_FPA_NEG
  247. | OP_FPA_MUL
  248. | OP_FPA_DIV
  249. | OP_FPA_REM
  250. | OP_FPA_ABS
  251. | OP_FPA_MIN
  252. | OP_FPA_MAX
  253. | OP_FPA_FMA
  254. | OP_FPA_SQRT
  255. | OP_FPA_ROUND_TO_INTEGRAL
  256. | OP_FPA_EQ
  257. | OP_FPA_LT
  258. | OP_FPA_GT
  259. | OP_FPA_LE
  260. | OP_FPA_GE
  261. | OP_FPA_IS_NAN
  262. | OP_FPA_IS_INF
  263. | OP_FPA_IS_ZERO
  264. | OP_FPA_IS_NORMAL
  265. | OP_FPA_IS_SUBNORMAL
  266. | OP_FPA_IS_NEGATIVE
  267. | OP_FPA_IS_POSITIVE
  268. | OP_FPA_FP
  269. | OP_FPA_TO_FP
  270. | OP_FPA_TO_FP_UNSIGNED
  271. | OP_FPA_TO_UBV
  272. | OP_FPA_TO_SBV
  273. | OP_FPA_TO_REAL
  274. | OP_FPA_TO_IEEE_BV
  275. | OP_FPA_BVWRAP
  276. | OP_FPA_BV2RM
  277. | OP_INTERNAL
  278. | OP_RECURSIVE
  279. | OP_UNINTERPRETED
val int_of_decl_kind : decl_kind -> int
val decl_kind_of_int : int -> decl_kind
type param_kind =
  1. | PK_UINT
  2. | PK_BOOL
  3. | PK_DOUBLE
  4. | PK_SYMBOL
  5. | PK_STRING
  6. | PK_OTHER
  7. | PK_INVALID
val int_of_param_kind : param_kind -> int
val param_kind_of_int : int -> param_kind
type ast_print_mode =
  1. | PRINT_SMTLIB_FULL
  2. | PRINT_LOW_LEVEL
  3. | PRINT_SMTLIB2_COMPLIANT
val int_of_ast_print_mode : ast_print_mode -> int
val ast_print_mode_of_int : int -> ast_print_mode
type error_code =
  1. | OK
  2. | SORT_ERROR
  3. | IOB
  4. | INVALID_ARG
  5. | PARSER_ERROR
  6. | NO_PARSER
  7. | INVALID_PATTERN
  8. | MEMOUT_FAIL
  9. | FILE_ACCESS_ERROR
  10. | INTERNAL_FATAL
  11. | INVALID_USAGE
  12. | DEC_REF_ERROR
  13. | EXCEPTION
val int_of_error_code : error_code -> int
val error_code_of_int : int -> error_code
type goal_prec =
  1. | GOAL_PRECISE
  2. | GOAL_UNDER
  3. | GOAL_OVER
  4. | GOAL_UNDER_OVER
val int_of_goal_prec : goal_prec -> int
val goal_prec_of_int : int -> goal_prec