sig
  type lbool = L_TRUE | L_UNDEF | L_FALSE
  val int_of_lbool : Z3enums.lbool -> int
  val lbool_of_int : int -> Z3enums.lbool
  type symbol_kind = INT_SYMBOL | STRING_SYMBOL
  val int_of_symbol_kind : Z3enums.symbol_kind -> int
  val symbol_kind_of_int : int -> Z3enums.symbol_kind
  type parameter_kind =
      PARAMETER_FUNC_DECL
    | PARAMETER_DOUBLE
    | PARAMETER_SYMBOL
    | PARAMETER_INT
    | PARAMETER_AST
    | PARAMETER_SORT
    | PARAMETER_RATIONAL
  val int_of_parameter_kind : Z3enums.parameter_kind -> int
  val parameter_kind_of_int : int -> Z3enums.parameter_kind
  type sort_kind =
      BV_SORT
    | FINITE_DOMAIN_SORT
    | ARRAY_SORT
    | UNKNOWN_SORT
    | RELATION_SORT
    | REAL_SORT
    | INT_SORT
    | FLOATING_POINT_SORT
    | ROUNDING_MODE_SORT
    | UNINTERPRETED_SORT
    | BOOL_SORT
    | DATATYPE_SORT
  val int_of_sort_kind : Z3enums.sort_kind -> int
  val sort_kind_of_int : int -> Z3enums.sort_kind
  type ast_kind =
      VAR_AST
    | SORT_AST
    | QUANTIFIER_AST
    | UNKNOWN_AST
    | FUNC_DECL_AST
    | NUMERAL_AST
    | APP_AST
  val int_of_ast_kind : Z3enums.ast_kind -> int
  val ast_kind_of_int : int -> Z3enums.ast_kind
  type decl_kind =
      OP_LABEL
    | OP_PR_REWRITE
    | OP_UNINTERPRETED
    | OP_SUB
    | OP_ZERO_EXT
    | OP_ADD
    | OP_FPA_ABS
    | OP_IS_INT
    | OP_BREDOR
    | OP_FPA_IS_INF
    | OP_BNOT
    | OP_BNOR
    | OP_PR_CNF_STAR
    | OP_FPA_TO_UBV
    | OP_RA_JOIN
    | OP_FPA_RM_NEAREST_TIES_TO_AWAY
    | OP_LE
    | OP_SET_UNION
    | OP_PR_UNDEF
    | OP_BREDAND
    | OP_LT
    | OP_RA_UNION
    | OP_FPA_IS_SUBNORMAL
    | OP_BADD
    | OP_BUREM0
    | OP_OEQ
    | OP_PR_MODUS_PONENS
    | OP_RA_CLONE
    | OP_REPEAT
    | OP_RA_NEGATION_FILTER
    | OP_FPA_NAN
    | OP_BSMOD0
    | OP_FPA_GT
    | OP_BLSHR
    | OP_BASHR
    | OP_PR_UNIT_RESOLUTION
    | OP_ROTATE_RIGHT
    | OP_ARRAY_DEFAULT
    | OP_PR_PULL_QUANT
    | OP_PR_APPLY_DEF
    | OP_PR_REWRITE_STAR
    | OP_IDIV
    | OP_PR_GOAL
    | OP_FPA_RM_TOWARD_POSITIVE
    | OP_PR_IFF_TRUE
    | OP_FPA_LT
    | OP_FPA_IS_NORMAL
    | OP_LABEL_LIT
    | OP_FPA_TO_IEEE_BV
    | OP_FPA_LE
    | OP_BOR
    | OP_PR_SYMMETRY
    | OP_TRUE
    | OP_SET_COMPLEMENT
    | OP_CONCAT
    | OP_PR_NOT_OR_ELIM
    | OP_IFF
    | OP_BSHL
    | OP_PR_TRANSITIVITY
    | OP_FPA_ROUND_TO_INTEGRAL
    | OP_SGT
    | OP_RA_WIDEN
    | OP_PR_DEF_INTRO
    | OP_NOT
    | OP_PR_QUANT_INTRO
    | OP_FPA_PLUS_ZERO
    | OP_UGT
    | OP_FPA_NEG
    | OP_DT_RECOGNISER
    | OP_SET_INTERSECT
    | OP_BSREM
    | OP_RA_STORE
    | OP_SLT
    | OP_ROTATE_LEFT
    | OP_PR_NNF_NEG
    | OP_FPA_EQ
    | OP_PR_REFLEXIVITY
    | OP_ULEQ
    | OP_BIT1
    | OP_BIT0
    | OP_FPA_MIN
    | OP_PB_AT_MOST
    | OP_EQ
    | OP_FPA_SUB
    | OP_BMUL
    | OP_ARRAY_MAP
    | OP_STORE
    | OP_PR_HYPOTHESIS
    | OP_RA_RENAME
    | OP_AND
    | OP_TO_REAL
    | OP_DT_UPDATE_FIELD
    | OP_PR_NNF_POS
    | OP_PR_AND_ELIM
    | OP_FPA_TO_SBV
    | OP_MOD
    | OP_BUDIV0
    | OP_FPA_MAX
    | OP_PR_TRUE
    | OP_BNAND
    | OP_PR_ELIM_UNUSED_VARS
    | OP_RA_FILTER
    | OP_FPA_ADD
    | OP_FD_LT
    | OP_RA_EMPTY
    | OP_DIV
    | OP_ANUM
    | OP_MUL
    | OP_UGEQ
    | OP_BSREM0
    | OP_PR_TH_LEMMA
    | OP_FPA_MINUS_INF
    | OP_BXOR
    | OP_DISTINCT
    | OP_PR_IFF_FALSE
    | OP_BV2INT
    | OP_EXT_ROTATE_LEFT
    | OP_PR_PULL_QUANT_STAR
    | OP_BSUB
    | OP_PR_ASSERTED
    | OP_BXNOR
    | OP_FPA_IS_ZERO
    | OP_EXTRACT
    | OP_PR_DER
    | OP_DT_CONSTRUCTOR
    | OP_GT
    | OP_BUREM
    | OP_IMPLIES
    | OP_SLEQ
    | OP_GE
    | OP_PB_GE
    | OP_BAND
    | OP_ITE
    | OP_AS_ARRAY
    | OP_FPA_IS_POSITIVE
    | OP_RA_SELECT
    | OP_CONST_ARRAY
    | OP_FPA_TO_REAL
    | OP_BSDIV
    | OP_FPA_IS_NEGATIVE
    | OP_OR
    | OP_FPA_FP
    | OP_PR_HYPER_RESOLVE
    | OP_AGNUM
    | OP_FPA_IS_NAN
    | OP_PR_PUSH_QUANT
    | OP_FPA_FMA
    | OP_BSMOD
    | OP_PR_IFF_OEQ
    | OP_INTERP
    | OP_PR_LEMMA
    | OP_FPA_TO_FP_UNSIGNED
    | OP_SET_SUBSET
    | OP_FPA_SQRT
    | OP_PB_LE
    | OP_FPA_GE
    | OP_FPA_DIV
    | OP_FPA_RM_TOWARD_ZERO
    | OP_SELECT
    | OP_RA_PROJECT
    | OP_BNEG
    | OP_UMINUS
    | OP_REM
    | OP_FPA_RM_NEAREST_TIES_TO_EVEN
    | OP_TO_INT
    | OP_PR_QUANT_INST
    | OP_SGEQ
    | OP_POWER
    | OP_XOR3
    | OP_RA_IS_EMPTY
    | OP_CARRY
    | OP_DT_ACCESSOR
    | OP_PR_TRANSITIVITY_STAR
    | OP_PR_NNF_STAR
    | OP_PR_COMMUTATIVITY
    | OP_ULT
    | OP_FPA_MUL
    | OP_BSDIV0
    | OP_SET_DIFFERENCE
    | OP_INT2BV
    | OP_FPA_NUM
    | OP_FPA_MINUS_ZERO
    | OP_FPA_REM
    | OP_XOR
    | OP_FPA_TO_FP
    | OP_PR_MODUS_PONENS_OEQ
    | OP_FPA_RM_TOWARD_NEGATIVE
    | OP_BNUM
    | OP_BUDIV
    | OP_PR_MONOTONICITY
    | OP_PR_DEF_AXIOM
    | OP_FALSE
    | OP_EXT_ROTATE_RIGHT
    | OP_PR_DISTRIBUTIVITY
    | OP_SIGN_EXT
    | OP_FPA_PLUS_INF
    | OP_PR_SKOLEMIZE
    | OP_BCOMP
    | OP_RA_COMPLEMENT
  val int_of_decl_kind : Z3enums.decl_kind -> int
  val decl_kind_of_int : int -> Z3enums.decl_kind
  type param_kind =
      PK_BOOL
    | PK_SYMBOL
    | PK_OTHER
    | PK_INVALID
    | PK_UINT
    | PK_STRING
    | PK_DOUBLE
  val int_of_param_kind : Z3enums.param_kind -> int
  val param_kind_of_int : int -> Z3enums.param_kind
  type ast_print_mode =
      PRINT_SMTLIB2_COMPLIANT
    | PRINT_SMTLIB_COMPLIANT
    | PRINT_SMTLIB_FULL
    | PRINT_LOW_LEVEL
  val int_of_ast_print_mode : Z3enums.ast_print_mode -> int
  val ast_print_mode_of_int : int -> Z3enums.ast_print_mode
  type error_code =
      INVALID_PATTERN
    | MEMOUT_FAIL
    | NO_PARSER
    | OK
    | INVALID_ARG
    | EXCEPTION
    | IOB
    | INTERNAL_FATAL
    | INVALID_USAGE
    | FILE_ACCESS_ERROR
    | SORT_ERROR
    | PARSER_ERROR
    | DEC_REF_ERROR
  val int_of_error_code : Z3enums.error_code -> int
  val error_code_of_int : int -> Z3enums.error_code
  type goal_prec = GOAL_UNDER | GOAL_PRECISE | GOAL_UNDER_OVER | GOAL_OVER
  val int_of_goal_prec : Z3enums.goal_prec -> int
  val goal_prec_of_int : int -> Z3enums.goal_prec
end