Package com.microsoft.z3.enumerations

Enum Z3_decl_kind

java.lang.Object
java.lang.Enum<Z3_decl_kind>
com.microsoft.z3.enumerations.Z3_decl_kind
All Implemented Interfaces:
Serializable, Comparable<Z3_decl_kind>, java.lang.constant.Constable
public enum Z3_decl_kind extends Enum<Z3_decl_kind>
Z3_decl_kind

  • Enum Constant Details

    • Z3_OP_TRUE

      public static final Z3_decl_kind Z3_OP_TRUE

    • Z3_OP_FALSE

      public static final Z3_decl_kind Z3_OP_FALSE

    • Z3_OP_EQ

      public static final Z3_decl_kind Z3_OP_EQ

    • Z3_OP_DISTINCT

      public static final Z3_decl_kind Z3_OP_DISTINCT

    • Z3_OP_ITE

      public static final Z3_decl_kind Z3_OP_ITE

    • Z3_OP_AND

      public static final Z3_decl_kind Z3_OP_AND

    • Z3_OP_OR

      public static final Z3_decl_kind Z3_OP_OR

    • Z3_OP_IFF

      public static final Z3_decl_kind Z3_OP_IFF

    • Z3_OP_XOR

      public static final Z3_decl_kind Z3_OP_XOR

    • Z3_OP_NOT

      public static final Z3_decl_kind Z3_OP_NOT

    • Z3_OP_IMPLIES

      public static final Z3_decl_kind Z3_OP_IMPLIES

    • Z3_OP_OEQ

      public static final Z3_decl_kind Z3_OP_OEQ

    • Z3_OP_ANUM

      public static final Z3_decl_kind Z3_OP_ANUM

    • Z3_OP_AGNUM

      public static final Z3_decl_kind Z3_OP_AGNUM

    • Z3_OP_LE

      public static final Z3_decl_kind Z3_OP_LE

    • Z3_OP_GE

      public static final Z3_decl_kind Z3_OP_GE

    • Z3_OP_LT

      public static final Z3_decl_kind Z3_OP_LT

    • Z3_OP_GT

      public static final Z3_decl_kind Z3_OP_GT

    • Z3_OP_ADD

      public static final Z3_decl_kind Z3_OP_ADD

    • Z3_OP_SUB

      public static final Z3_decl_kind Z3_OP_SUB

    • Z3_OP_UMINUS

      public static final Z3_decl_kind Z3_OP_UMINUS

    • Z3_OP_MUL

      public static final Z3_decl_kind Z3_OP_MUL

    • Z3_OP_DIV

      public static final Z3_decl_kind Z3_OP_DIV

    • Z3_OP_IDIV

      public static final Z3_decl_kind Z3_OP_IDIV

    • Z3_OP_REM

      public static final Z3_decl_kind Z3_OP_REM

    • Z3_OP_MOD

      public static final Z3_decl_kind Z3_OP_MOD

    • Z3_OP_TO_REAL

      public static final Z3_decl_kind Z3_OP_TO_REAL

    • Z3_OP_TO_INT

      public static final Z3_decl_kind Z3_OP_TO_INT

    • Z3_OP_IS_INT

      public static final Z3_decl_kind Z3_OP_IS_INT

    • Z3_OP_POWER

      public static final Z3_decl_kind Z3_OP_POWER

    • Z3_OP_STORE

      public static final Z3_decl_kind Z3_OP_STORE

    • Z3_OP_SELECT

      public static final Z3_decl_kind Z3_OP_SELECT

    • Z3_OP_CONST_ARRAY

      public static final Z3_decl_kind Z3_OP_CONST_ARRAY

    • Z3_OP_ARRAY_MAP

      public static final Z3_decl_kind Z3_OP_ARRAY_MAP

    • Z3_OP_ARRAY_DEFAULT

      public static final Z3_decl_kind Z3_OP_ARRAY_DEFAULT

    • Z3_OP_SET_UNION

      public static final Z3_decl_kind Z3_OP_SET_UNION

    • Z3_OP_SET_INTERSECT

      public static final Z3_decl_kind Z3_OP_SET_INTERSECT

    • Z3_OP_SET_DIFFERENCE

      public static final Z3_decl_kind Z3_OP_SET_DIFFERENCE

    • Z3_OP_SET_COMPLEMENT

      public static final Z3_decl_kind Z3_OP_SET_COMPLEMENT

    • Z3_OP_SET_SUBSET

      public static final Z3_decl_kind Z3_OP_SET_SUBSET

    • Z3_OP_AS_ARRAY

      public static final Z3_decl_kind Z3_OP_AS_ARRAY

    • Z3_OP_ARRAY_EXT

      public static final Z3_decl_kind Z3_OP_ARRAY_EXT

    • Z3_OP_SET_HAS_SIZE

      public static final Z3_decl_kind Z3_OP_SET_HAS_SIZE

    • Z3_OP_SET_CARD

      public static final Z3_decl_kind Z3_OP_SET_CARD

    • Z3_OP_BNUM

      public static final Z3_decl_kind Z3_OP_BNUM

    • Z3_OP_BIT1

      public static final Z3_decl_kind Z3_OP_BIT1

    • Z3_OP_BIT0

      public static final Z3_decl_kind Z3_OP_BIT0

    • Z3_OP_BNEG

      public static final Z3_decl_kind Z3_OP_BNEG

    • Z3_OP_BADD

      public static final Z3_decl_kind Z3_OP_BADD

    • Z3_OP_BSUB

      public static final Z3_decl_kind Z3_OP_BSUB

    • Z3_OP_BMUL

      public static final Z3_decl_kind Z3_OP_BMUL

    • Z3_OP_BSDIV

      public static final Z3_decl_kind Z3_OP_BSDIV

    • Z3_OP_BUDIV

      public static final Z3_decl_kind Z3_OP_BUDIV

    • Z3_OP_BSREM

      public static final Z3_decl_kind Z3_OP_BSREM

    • Z3_OP_BUREM

      public static final Z3_decl_kind Z3_OP_BUREM

    • Z3_OP_BSMOD

      public static final Z3_decl_kind Z3_OP_BSMOD

    • Z3_OP_BSDIV0

      public static final Z3_decl_kind Z3_OP_BSDIV0

    • Z3_OP_BUDIV0

      public static final Z3_decl_kind Z3_OP_BUDIV0

    • Z3_OP_BSREM0

      public static final Z3_decl_kind Z3_OP_BSREM0

    • Z3_OP_BUREM0

      public static final Z3_decl_kind Z3_OP_BUREM0

    • Z3_OP_BSMOD0

      public static final Z3_decl_kind Z3_OP_BSMOD0

    • Z3_OP_ULEQ

      public static final Z3_decl_kind Z3_OP_ULEQ

    • Z3_OP_SLEQ

      public static final Z3_decl_kind Z3_OP_SLEQ

    • Z3_OP_UGEQ

      public static final Z3_decl_kind Z3_OP_UGEQ

    • Z3_OP_SGEQ

      public static final Z3_decl_kind Z3_OP_SGEQ

    • Z3_OP_ULT

      public static final Z3_decl_kind Z3_OP_ULT

    • Z3_OP_SLT

      public static final Z3_decl_kind Z3_OP_SLT

    • Z3_OP_UGT

      public static final Z3_decl_kind Z3_OP_UGT

    • Z3_OP_SGT

      public static final Z3_decl_kind Z3_OP_SGT

    • Z3_OP_BAND

      public static final Z3_decl_kind Z3_OP_BAND

    • Z3_OP_BOR

      public static final Z3_decl_kind Z3_OP_BOR

    • Z3_OP_BNOT

      public static final Z3_decl_kind Z3_OP_BNOT

    • Z3_OP_BXOR

      public static final Z3_decl_kind Z3_OP_BXOR

    • Z3_OP_BNAND

      public static final Z3_decl_kind Z3_OP_BNAND

    • Z3_OP_BNOR

      public static final Z3_decl_kind Z3_OP_BNOR

    • Z3_OP_BXNOR

      public static final Z3_decl_kind Z3_OP_BXNOR

    • Z3_OP_CONCAT

      public static final Z3_decl_kind Z3_OP_CONCAT

    • Z3_OP_SIGN_EXT

      public static final Z3_decl_kind Z3_OP_SIGN_EXT

    • Z3_OP_ZERO_EXT

      public static final Z3_decl_kind Z3_OP_ZERO_EXT

    • Z3_OP_EXTRACT

      public static final Z3_decl_kind Z3_OP_EXTRACT

    • Z3_OP_REPEAT

      public static final Z3_decl_kind Z3_OP_REPEAT

    • Z3_OP_BREDOR

      public static final Z3_decl_kind Z3_OP_BREDOR

    • Z3_OP_BREDAND

      public static final Z3_decl_kind Z3_OP_BREDAND

    • Z3_OP_BCOMP

      public static final Z3_decl_kind Z3_OP_BCOMP

    • Z3_OP_BSHL

      public static final Z3_decl_kind Z3_OP_BSHL

    • Z3_OP_BLSHR

      public static final Z3_decl_kind Z3_OP_BLSHR

    • Z3_OP_BASHR

      public static final Z3_decl_kind Z3_OP_BASHR

    • Z3_OP_ROTATE_LEFT

      public static final Z3_decl_kind Z3_OP_ROTATE_LEFT

    • Z3_OP_ROTATE_RIGHT

      public static final Z3_decl_kind Z3_OP_ROTATE_RIGHT

    • Z3_OP_EXT_ROTATE_LEFT

      public static final Z3_decl_kind Z3_OP_EXT_ROTATE_LEFT

    • Z3_OP_EXT_ROTATE_RIGHT

      public static final Z3_decl_kind Z3_OP_EXT_ROTATE_RIGHT

    • Z3_OP_BIT2BOOL

      public static final Z3_decl_kind Z3_OP_BIT2BOOL

    • Z3_OP_INT2BV

      public static final Z3_decl_kind Z3_OP_INT2BV

    • Z3_OP_BV2INT

      public static final Z3_decl_kind Z3_OP_BV2INT

    • Z3_OP_CARRY

      public static final Z3_decl_kind Z3_OP_CARRY

    • Z3_OP_XOR3

      public static final Z3_decl_kind Z3_OP_XOR3

    • Z3_OP_BSMUL_NO_OVFL

      public static final Z3_decl_kind Z3_OP_BSMUL_NO_OVFL

    • Z3_OP_BUMUL_NO_OVFL

      public static final Z3_decl_kind Z3_OP_BUMUL_NO_OVFL

    • Z3_OP_BSMUL_NO_UDFL

      public static final Z3_decl_kind Z3_OP_BSMUL_NO_UDFL

    • Z3_OP_BSDIV_I

      public static final Z3_decl_kind Z3_OP_BSDIV_I

    • Z3_OP_BUDIV_I

      public static final Z3_decl_kind Z3_OP_BUDIV_I

    • Z3_OP_BSREM_I

      public static final Z3_decl_kind Z3_OP_BSREM_I

    • Z3_OP_BUREM_I

      public static final Z3_decl_kind Z3_OP_BUREM_I

    • Z3_OP_BSMOD_I

      public static final Z3_decl_kind Z3_OP_BSMOD_I

    • Z3_OP_PR_UNDEF

      public static final Z3_decl_kind Z3_OP_PR_UNDEF

    • Z3_OP_PR_TRUE

      public static final Z3_decl_kind Z3_OP_PR_TRUE

    • Z3_OP_PR_ASSERTED

      public static final Z3_decl_kind Z3_OP_PR_ASSERTED

    • Z3_OP_PR_GOAL

      public static final Z3_decl_kind Z3_OP_PR_GOAL

    • Z3_OP_PR_MODUS_PONENS

      public static final Z3_decl_kind Z3_OP_PR_MODUS_PONENS

    • Z3_OP_PR_REFLEXIVITY

      public static final Z3_decl_kind Z3_OP_PR_REFLEXIVITY

    • Z3_OP_PR_SYMMETRY

      public static final Z3_decl_kind Z3_OP_PR_SYMMETRY

    • Z3_OP_PR_TRANSITIVITY

      public static final Z3_decl_kind Z3_OP_PR_TRANSITIVITY

    • Z3_OP_PR_TRANSITIVITY_STAR

      public static final Z3_decl_kind Z3_OP_PR_TRANSITIVITY_STAR

    • Z3_OP_PR_MONOTONICITY

      public static final Z3_decl_kind Z3_OP_PR_MONOTONICITY

    • Z3_OP_PR_QUANT_INTRO

      public static final Z3_decl_kind Z3_OP_PR_QUANT_INTRO

    • Z3_OP_PR_BIND

      public static final Z3_decl_kind Z3_OP_PR_BIND

    • Z3_OP_PR_DISTRIBUTIVITY

      public static final Z3_decl_kind Z3_OP_PR_DISTRIBUTIVITY

    • Z3_OP_PR_AND_ELIM

      public static final Z3_decl_kind Z3_OP_PR_AND_ELIM

    • Z3_OP_PR_NOT_OR_ELIM

      public static final Z3_decl_kind Z3_OP_PR_NOT_OR_ELIM

    • Z3_OP_PR_REWRITE

      public static final Z3_decl_kind Z3_OP_PR_REWRITE

    • Z3_OP_PR_REWRITE_STAR

      public static final Z3_decl_kind Z3_OP_PR_REWRITE_STAR

    • Z3_OP_PR_PULL_QUANT

      public static final Z3_decl_kind Z3_OP_PR_PULL_QUANT

    • Z3_OP_PR_PUSH_QUANT

      public static final Z3_decl_kind Z3_OP_PR_PUSH_QUANT

    • Z3_OP_PR_ELIM_UNUSED_VARS

      public static final Z3_decl_kind Z3_OP_PR_ELIM_UNUSED_VARS

    • Z3_OP_PR_DER

      public static final Z3_decl_kind Z3_OP_PR_DER

    • Z3_OP_PR_QUANT_INST

      public static final Z3_decl_kind Z3_OP_PR_QUANT_INST

    • Z3_OP_PR_HYPOTHESIS

      public static final Z3_decl_kind Z3_OP_PR_HYPOTHESIS

    • Z3_OP_PR_LEMMA

      public static final Z3_decl_kind Z3_OP_PR_LEMMA

    • Z3_OP_PR_UNIT_RESOLUTION

      public static final Z3_decl_kind Z3_OP_PR_UNIT_RESOLUTION

    • Z3_OP_PR_IFF_TRUE

      public static final Z3_decl_kind Z3_OP_PR_IFF_TRUE

    • Z3_OP_PR_IFF_FALSE

      public static final Z3_decl_kind Z3_OP_PR_IFF_FALSE

    • Z3_OP_PR_COMMUTATIVITY

      public static final Z3_decl_kind Z3_OP_PR_COMMUTATIVITY

    • Z3_OP_PR_DEF_AXIOM

      public static final Z3_decl_kind Z3_OP_PR_DEF_AXIOM

    • Z3_OP_PR_ASSUMPTION_ADD

      public static final Z3_decl_kind Z3_OP_PR_ASSUMPTION_ADD

    • Z3_OP_PR_LEMMA_ADD

      public static final Z3_decl_kind Z3_OP_PR_LEMMA_ADD

    • Z3_OP_PR_REDUNDANT_DEL

      public static final Z3_decl_kind Z3_OP_PR_REDUNDANT_DEL

    • Z3_OP_PR_CLAUSE_TRAIL

      public static final Z3_decl_kind Z3_OP_PR_CLAUSE_TRAIL

    • Z3_OP_PR_DEF_INTRO

      public static final Z3_decl_kind Z3_OP_PR_DEF_INTRO

    • Z3_OP_PR_APPLY_DEF

      public static final Z3_decl_kind Z3_OP_PR_APPLY_DEF

    • Z3_OP_PR_IFF_OEQ

      public static final Z3_decl_kind Z3_OP_PR_IFF_OEQ

    • Z3_OP_PR_NNF_POS

      public static final Z3_decl_kind Z3_OP_PR_NNF_POS

    • Z3_OP_PR_NNF_NEG

      public static final Z3_decl_kind Z3_OP_PR_NNF_NEG

    • Z3_OP_PR_SKOLEMIZE

      public static final Z3_decl_kind Z3_OP_PR_SKOLEMIZE

    • Z3_OP_PR_MODUS_PONENS_OEQ

      public static final Z3_decl_kind Z3_OP_PR_MODUS_PONENS_OEQ

    • Z3_OP_PR_TH_LEMMA

      public static final Z3_decl_kind Z3_OP_PR_TH_LEMMA

    • Z3_OP_PR_HYPER_RESOLVE

      public static final Z3_decl_kind Z3_OP_PR_HYPER_RESOLVE

    • Z3_OP_RA_STORE

      public static final Z3_decl_kind Z3_OP_RA_STORE

    • Z3_OP_RA_EMPTY

      public static final Z3_decl_kind Z3_OP_RA_EMPTY

    • Z3_OP_RA_IS_EMPTY

      public static final Z3_decl_kind Z3_OP_RA_IS_EMPTY

    • Z3_OP_RA_JOIN

      public static final Z3_decl_kind Z3_OP_RA_JOIN

    • Z3_OP_RA_UNION

      public static final Z3_decl_kind Z3_OP_RA_UNION

    • Z3_OP_RA_WIDEN

      public static final Z3_decl_kind Z3_OP_RA_WIDEN

    • Z3_OP_RA_PROJECT

      public static final Z3_decl_kind Z3_OP_RA_PROJECT

    • Z3_OP_RA_FILTER

      public static final Z3_decl_kind Z3_OP_RA_FILTER

    • Z3_OP_RA_NEGATION_FILTER

      public static final Z3_decl_kind Z3_OP_RA_NEGATION_FILTER

    • Z3_OP_RA_RENAME

      public static final Z3_decl_kind Z3_OP_RA_RENAME

    • Z3_OP_RA_COMPLEMENT

      public static final Z3_decl_kind Z3_OP_RA_COMPLEMENT

    • Z3_OP_RA_SELECT

      public static final Z3_decl_kind Z3_OP_RA_SELECT

    • Z3_OP_RA_CLONE

      public static final Z3_decl_kind Z3_OP_RA_CLONE

    • Z3_OP_FD_CONSTANT

      public static final Z3_decl_kind Z3_OP_FD_CONSTANT

    • Z3_OP_FD_LT

      public static final Z3_decl_kind Z3_OP_FD_LT

    • Z3_OP_SEQ_UNIT

      public static final Z3_decl_kind Z3_OP_SEQ_UNIT

    • Z3_OP_SEQ_EMPTY

      public static final Z3_decl_kind Z3_OP_SEQ_EMPTY

    • Z3_OP_SEQ_CONCAT

      public static final Z3_decl_kind Z3_OP_SEQ_CONCAT

    • Z3_OP_SEQ_PREFIX

      public static final Z3_decl_kind Z3_OP_SEQ_PREFIX

    • Z3_OP_SEQ_SUFFIX

      public static final Z3_decl_kind Z3_OP_SEQ_SUFFIX

    • Z3_OP_SEQ_CONTAINS

      public static final Z3_decl_kind Z3_OP_SEQ_CONTAINS

    • Z3_OP_SEQ_EXTRACT

      public static final Z3_decl_kind Z3_OP_SEQ_EXTRACT

    • Z3_OP_SEQ_REPLACE

      public static final Z3_decl_kind Z3_OP_SEQ_REPLACE

    • Z3_OP_SEQ_REPLACE_RE

      public static final Z3_decl_kind Z3_OP_SEQ_REPLACE_RE

    • Z3_OP_SEQ_REPLACE_RE_ALL

      public static final Z3_decl_kind Z3_OP_SEQ_REPLACE_RE_ALL

    • Z3_OP_SEQ_REPLACE_ALL

      public static final Z3_decl_kind Z3_OP_SEQ_REPLACE_ALL

    • Z3_OP_SEQ_AT

      public static final Z3_decl_kind Z3_OP_SEQ_AT

    • Z3_OP_SEQ_NTH

      public static final Z3_decl_kind Z3_OP_SEQ_NTH

    • Z3_OP_SEQ_LENGTH

      public static final Z3_decl_kind Z3_OP_SEQ_LENGTH

    • Z3_OP_SEQ_INDEX

      public static final Z3_decl_kind Z3_OP_SEQ_INDEX

    • Z3_OP_SEQ_LAST_INDEX

      public static final Z3_decl_kind Z3_OP_SEQ_LAST_INDEX

    • Z3_OP_SEQ_TO_RE

      public static final Z3_decl_kind Z3_OP_SEQ_TO_RE

    • Z3_OP_SEQ_IN_RE

      public static final Z3_decl_kind Z3_OP_SEQ_IN_RE

    • Z3_OP_STR_TO_INT

      public static final Z3_decl_kind Z3_OP_STR_TO_INT

    • Z3_OP_INT_TO_STR

      public static final Z3_decl_kind Z3_OP_INT_TO_STR

    • Z3_OP_UBV_TO_STR

      public static final Z3_decl_kind Z3_OP_UBV_TO_STR

    • Z3_OP_SBV_TO_STR

      public static final Z3_decl_kind Z3_OP_SBV_TO_STR

    • Z3_OP_STR_TO_CODE

      public static final Z3_decl_kind Z3_OP_STR_TO_CODE

    • Z3_OP_STR_FROM_CODE

      public static final Z3_decl_kind Z3_OP_STR_FROM_CODE

    • Z3_OP_STRING_LT

      public static final Z3_decl_kind Z3_OP_STRING_LT

    • Z3_OP_STRING_LE

      public static final Z3_decl_kind Z3_OP_STRING_LE

    • Z3_OP_RE_PLUS

      public static final Z3_decl_kind Z3_OP_RE_PLUS

    • Z3_OP_RE_STAR

      public static final Z3_decl_kind Z3_OP_RE_STAR

    • Z3_OP_RE_OPTION

      public static final Z3_decl_kind Z3_OP_RE_OPTION

    • Z3_OP_RE_CONCAT

      public static final Z3_decl_kind Z3_OP_RE_CONCAT

    • Z3_OP_RE_UNION

      public static final Z3_decl_kind Z3_OP_RE_UNION

    • Z3_OP_RE_RANGE

      public static final Z3_decl_kind Z3_OP_RE_RANGE

    • Z3_OP_RE_DIFF

      public static final Z3_decl_kind Z3_OP_RE_DIFF

    • Z3_OP_RE_INTERSECT

      public static final Z3_decl_kind Z3_OP_RE_INTERSECT

    • Z3_OP_RE_LOOP

      public static final Z3_decl_kind Z3_OP_RE_LOOP

    • Z3_OP_RE_POWER

      public static final Z3_decl_kind Z3_OP_RE_POWER

    • Z3_OP_RE_COMPLEMENT

      public static final Z3_decl_kind Z3_OP_RE_COMPLEMENT

    • Z3_OP_RE_EMPTY_SET

      public static final Z3_decl_kind Z3_OP_RE_EMPTY_SET

    • Z3_OP_RE_FULL_SET

      public static final Z3_decl_kind Z3_OP_RE_FULL_SET

    • Z3_OP_RE_FULL_CHAR_SET

      public static final Z3_decl_kind Z3_OP_RE_FULL_CHAR_SET

    • Z3_OP_RE_OF_PRED

      public static final Z3_decl_kind Z3_OP_RE_OF_PRED

    • Z3_OP_RE_REVERSE

      public static final Z3_decl_kind Z3_OP_RE_REVERSE

    • Z3_OP_RE_DERIVATIVE

      public static final Z3_decl_kind Z3_OP_RE_DERIVATIVE

    • Z3_OP_CHAR_CONST

      public static final Z3_decl_kind Z3_OP_CHAR_CONST

    • Z3_OP_CHAR_LE

      public static final Z3_decl_kind Z3_OP_CHAR_LE

    • Z3_OP_CHAR_TO_INT

      public static final Z3_decl_kind Z3_OP_CHAR_TO_INT

    • Z3_OP_CHAR_TO_BV

      public static final Z3_decl_kind Z3_OP_CHAR_TO_BV

    • Z3_OP_CHAR_FROM_BV

      public static final Z3_decl_kind Z3_OP_CHAR_FROM_BV

    • Z3_OP_CHAR_IS_DIGIT

      public static final Z3_decl_kind Z3_OP_CHAR_IS_DIGIT

    • Z3_OP_LABEL

      public static final Z3_decl_kind Z3_OP_LABEL

    • Z3_OP_LABEL_LIT

      public static final Z3_decl_kind Z3_OP_LABEL_LIT

    • Z3_OP_DT_CONSTRUCTOR

      public static final Z3_decl_kind Z3_OP_DT_CONSTRUCTOR

    • Z3_OP_DT_RECOGNISER

      public static final Z3_decl_kind Z3_OP_DT_RECOGNISER

    • Z3_OP_DT_IS

      public static final Z3_decl_kind Z3_OP_DT_IS

    • Z3_OP_DT_ACCESSOR

      public static final Z3_decl_kind Z3_OP_DT_ACCESSOR

    • Z3_OP_DT_UPDATE_FIELD

      public static final Z3_decl_kind Z3_OP_DT_UPDATE_FIELD

    • Z3_OP_PB_AT_MOST

      public static final Z3_decl_kind Z3_OP_PB_AT_MOST

    • Z3_OP_PB_AT_LEAST

      public static final Z3_decl_kind Z3_OP_PB_AT_LEAST

    • Z3_OP_PB_LE

      public static final Z3_decl_kind Z3_OP_PB_LE

    • Z3_OP_PB_GE

      public static final Z3_decl_kind Z3_OP_PB_GE

    • Z3_OP_PB_EQ

      public static final Z3_decl_kind Z3_OP_PB_EQ

    • Z3_OP_SPECIAL_RELATION_LO

      public static final Z3_decl_kind Z3_OP_SPECIAL_RELATION_LO

    • Z3_OP_SPECIAL_RELATION_PO

      public static final Z3_decl_kind Z3_OP_SPECIAL_RELATION_PO

    • Z3_OP_SPECIAL_RELATION_PLO

      public static final Z3_decl_kind Z3_OP_SPECIAL_RELATION_PLO

    • Z3_OP_SPECIAL_RELATION_TO

      public static final Z3_decl_kind Z3_OP_SPECIAL_RELATION_TO

    • Z3_OP_SPECIAL_RELATION_TC

      public static final Z3_decl_kind Z3_OP_SPECIAL_RELATION_TC

    • Z3_OP_SPECIAL_RELATION_TRC

      public static final Z3_decl_kind Z3_OP_SPECIAL_RELATION_TRC

    • Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN

      public static final Z3_decl_kind Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN

    • Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY

      public static final Z3_decl_kind Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY

    • Z3_OP_FPA_RM_TOWARD_POSITIVE

      public static final Z3_decl_kind Z3_OP_FPA_RM_TOWARD_POSITIVE

    • Z3_OP_FPA_RM_TOWARD_NEGATIVE

      public static final Z3_decl_kind Z3_OP_FPA_RM_TOWARD_NEGATIVE

    • Z3_OP_FPA_RM_TOWARD_ZERO

      public static final Z3_decl_kind Z3_OP_FPA_RM_TOWARD_ZERO

    • Z3_OP_FPA_NUM

      public static final Z3_decl_kind Z3_OP_FPA_NUM

    • Z3_OP_FPA_PLUS_INF

      public static final Z3_decl_kind Z3_OP_FPA_PLUS_INF

    • Z3_OP_FPA_MINUS_INF

      public static final Z3_decl_kind Z3_OP_FPA_MINUS_INF

    • Z3_OP_FPA_NAN

      public static final Z3_decl_kind Z3_OP_FPA_NAN

    • Z3_OP_FPA_PLUS_ZERO

      public static final Z3_decl_kind Z3_OP_FPA_PLUS_ZERO

    • Z3_OP_FPA_MINUS_ZERO

      public static final Z3_decl_kind Z3_OP_FPA_MINUS_ZERO

    • Z3_OP_FPA_ADD

      public static final Z3_decl_kind Z3_OP_FPA_ADD

    • Z3_OP_FPA_SUB

      public static final Z3_decl_kind Z3_OP_FPA_SUB

    • Z3_OP_FPA_NEG

      public static final Z3_decl_kind Z3_OP_FPA_NEG

    • Z3_OP_FPA_MUL

      public static final Z3_decl_kind Z3_OP_FPA_MUL

    • Z3_OP_FPA_DIV

      public static final Z3_decl_kind Z3_OP_FPA_DIV

    • Z3_OP_FPA_REM

      public static final Z3_decl_kind Z3_OP_FPA_REM

    • Z3_OP_FPA_ABS

      public static final Z3_decl_kind Z3_OP_FPA_ABS

    • Z3_OP_FPA_MIN

      public static final Z3_decl_kind Z3_OP_FPA_MIN

    • Z3_OP_FPA_MAX

      public static final Z3_decl_kind Z3_OP_FPA_MAX

    • Z3_OP_FPA_FMA

      public static final Z3_decl_kind Z3_OP_FPA_FMA

    • Z3_OP_FPA_SQRT

      public static final Z3_decl_kind Z3_OP_FPA_SQRT

    • Z3_OP_FPA_ROUND_TO_INTEGRAL

      public static final Z3_decl_kind Z3_OP_FPA_ROUND_TO_INTEGRAL

    • Z3_OP_FPA_EQ

      public static final Z3_decl_kind Z3_OP_FPA_EQ

    • Z3_OP_FPA_LT

      public static final Z3_decl_kind Z3_OP_FPA_LT

    • Z3_OP_FPA_GT

      public static final Z3_decl_kind Z3_OP_FPA_GT

    • Z3_OP_FPA_LE

      public static final Z3_decl_kind Z3_OP_FPA_LE

    • Z3_OP_FPA_GE

      public static final Z3_decl_kind Z3_OP_FPA_GE

    • Z3_OP_FPA_IS_NAN

      public static final Z3_decl_kind Z3_OP_FPA_IS_NAN

    • Z3_OP_FPA_IS_INF

      public static final Z3_decl_kind Z3_OP_FPA_IS_INF

    • Z3_OP_FPA_IS_ZERO

      public static final Z3_decl_kind Z3_OP_FPA_IS_ZERO

    • Z3_OP_FPA_IS_NORMAL

      public static final Z3_decl_kind Z3_OP_FPA_IS_NORMAL

    • Z3_OP_FPA_IS_SUBNORMAL

      public static final Z3_decl_kind Z3_OP_FPA_IS_SUBNORMAL

    • Z3_OP_FPA_IS_NEGATIVE

      public static final Z3_decl_kind Z3_OP_FPA_IS_NEGATIVE

    • Z3_OP_FPA_IS_POSITIVE

      public static final Z3_decl_kind Z3_OP_FPA_IS_POSITIVE

    • Z3_OP_FPA_FP

      public static final Z3_decl_kind Z3_OP_FPA_FP

    • Z3_OP_FPA_TO_FP

      public static final Z3_decl_kind Z3_OP_FPA_TO_FP

    • Z3_OP_FPA_TO_FP_UNSIGNED

      public static final Z3_decl_kind Z3_OP_FPA_TO_FP_UNSIGNED

    • Z3_OP_FPA_TO_UBV

      public static final Z3_decl_kind Z3_OP_FPA_TO_UBV

    • Z3_OP_FPA_TO_SBV

      public static final Z3_decl_kind Z3_OP_FPA_TO_SBV

    • Z3_OP_FPA_TO_REAL

      public static final Z3_decl_kind Z3_OP_FPA_TO_REAL

    • Z3_OP_FPA_TO_IEEE_BV

      public static final Z3_decl_kind Z3_OP_FPA_TO_IEEE_BV

    • Z3_OP_FPA_BVWRAP

      public static final Z3_decl_kind Z3_OP_FPA_BVWRAP

    • Z3_OP_FPA_BV2RM

      public static final Z3_decl_kind Z3_OP_FPA_BV2RM

    • Z3_OP_INTERNAL

      public static final Z3_decl_kind Z3_OP_INTERNAL

    • Z3_OP_UNINTERPRETED

      public static final Z3_decl_kind Z3_OP_UNINTERPRETED

  • Method Details

    • values

      public static Z3_decl_kind[] values()
      Returns an array containing the constants of this enum type, in the order they are declared.
      Returns:
      an array containing the constants of this enum type, in the order they are declared

    • valueOf

      public static Z3_decl_kind valueOf(String name)
      Returns the enum constant of this type with the specified name. The string must match exactly an identifier used to declare an enum constant in this type. (Extraneous whitespace characters are not permitted.)
      Parameters:
      name - the name of the enum constant to be returned.
      Returns:
      the enum constant with the specified name
      Throws:
      IllegalArgumentException - if this enum type has no constant with the specified name
      NullPointerException - if the argument is null

    • fromInt

      public static final Z3_decl_kind fromInt(int v)

    • toInt

      public final int toInt()