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