menu
z3 package
documentation
z3_ffi.dart
Z3_decl_kind
OP_XOR3 constant
OP_XOR3 constant
dark_mode
light_mode
OP_XOR3
constant
int
const
OP_XOR3
Implementation
static
const
int
OP_XOR3 =
1075
;
z3 package
documentation
z3_ffi
Z3_decl_kind
OP_XOR3 constant
Z3_decl_kind class
Constructors
Z3_decl_kind
Properties
hashCode
runtimeType
Methods
noSuchMethod
toString
Operators
operator ==
Constants
OP_ADD
OP_AGNUM
OP_AND
OP_ANUM
OP_ARRAY_DEFAULT
OP_ARRAY_EXT
OP_ARRAY_MAP
OP_AS_ARRAY
OP_BADD
OP_BAND
OP_BASHR
OP_BCOMP
OP_BIT0
OP_BIT1
OP_BIT2BOOL
OP_BLSHR
OP_BMUL
OP_BNAND
OP_BNEG
OP_BNOR
OP_BNOT
OP_BNUM
OP_BOR
OP_BREDAND
OP_BREDOR
OP_BSDIV
OP_BSDIV0
OP_BSDIV_I
OP_BSHL
OP_BSMOD
OP_BSMOD0
OP_BSMOD_I
OP_BSMUL_NO_OVFL
OP_BSMUL_NO_UDFL
OP_BSREM
OP_BSREM0
OP_BSREM_I
OP_BSUB
OP_BUDIV
OP_BUDIV0
OP_BUDIV_I
OP_BUMUL_NO_OVFL
OP_BUREM
OP_BUREM0
OP_BUREM_I
OP_BV2INT
OP_BXNOR
OP_BXOR
OP_CARRY
OP_CHAR_CONST
OP_CHAR_FROM_BV
OP_CHAR_IS_DIGIT
OP_CHAR_LE
OP_CHAR_TO_BV
OP_CHAR_TO_INT
OP_CONCAT
OP_CONST_ARRAY
OP_DISTINCT
OP_DIV
OP_DT_ACCESSOR
OP_DT_CONSTRUCTOR
OP_DT_IS
OP_DT_RECOGNISER
OP_DT_UPDATE_FIELD
OP_EQ
OP_EXT_ROTATE_LEFT
OP_EXT_ROTATE_RIGHT
OP_EXTRACT
OP_FALSE
OP_FD_CONSTANT
OP_FD_LT
OP_FPA_ABS
OP_FPA_ADD
OP_FPA_BV2RM
OP_FPA_BVWRAP
OP_FPA_DIV
OP_FPA_EQ
OP_FPA_FMA
OP_FPA_FP
OP_FPA_GE
OP_FPA_GT
OP_FPA_IS_INF
OP_FPA_IS_NAN
OP_FPA_IS_NEGATIVE
OP_FPA_IS_NORMAL
OP_FPA_IS_POSITIVE
OP_FPA_IS_SUBNORMAL
OP_FPA_IS_ZERO
OP_FPA_LE
OP_FPA_LT
OP_FPA_MAX
OP_FPA_MIN
OP_FPA_MINUS_INF
OP_FPA_MINUS_ZERO
OP_FPA_MUL
OP_FPA_NAN
OP_FPA_NEG
OP_FPA_NUM
OP_FPA_PLUS_INF
OP_FPA_PLUS_ZERO
OP_FPA_REM
OP_FPA_RM_NEAREST_TIES_TO_AWAY
OP_FPA_RM_NEAREST_TIES_TO_EVEN
OP_FPA_RM_TOWARD_NEGATIVE
OP_FPA_RM_TOWARD_POSITIVE
OP_FPA_RM_TOWARD_ZERO
OP_FPA_ROUND_TO_INTEGRAL
OP_FPA_SQRT
OP_FPA_SUB
OP_FPA_TO_FP
OP_FPA_TO_FP_UNSIGNED
OP_FPA_TO_IEEE_BV
OP_FPA_TO_REAL
OP_FPA_TO_SBV
OP_FPA_TO_UBV
OP_GE
OP_GT
OP_IDIV
OP_IFF
OP_IMPLIES
OP_INT2BV
OP_INT_TO_STR
OP_INTERNAL
OP_IS_INT
OP_ITE
OP_LABEL
OP_LABEL_LIT
OP_LE
OP_LT
OP_MOD
OP_MUL
OP_NOT
OP_OEQ
OP_OR
OP_PB_AT_LEAST
OP_PB_AT_MOST
OP_PB_EQ
OP_PB_GE
OP_PB_LE
OP_POWER
OP_PR_AND_ELIM
OP_PR_APPLY_DEF
OP_PR_ASSERTED
OP_PR_ASSUMPTION_ADD
OP_PR_BIND
OP_PR_CLAUSE_TRAIL
OP_PR_COMMUTATIVITY
OP_PR_DEF_AXIOM
OP_PR_DEF_INTRO
OP_PR_DER
OP_PR_DISTRIBUTIVITY
OP_PR_ELIM_UNUSED_VARS
OP_PR_GOAL
OP_PR_HYPER_RESOLVE
OP_PR_HYPOTHESIS
OP_PR_IFF_FALSE
OP_PR_IFF_OEQ
OP_PR_IFF_TRUE
OP_PR_LEMMA
OP_PR_LEMMA_ADD
OP_PR_MODUS_PONENS
OP_PR_MODUS_PONENS_OEQ
OP_PR_MONOTONICITY
OP_PR_NNF_NEG
OP_PR_NNF_POS
OP_PR_NOT_OR_ELIM
OP_PR_PULL_QUANT
OP_PR_PUSH_QUANT
OP_PR_QUANT_INST
OP_PR_QUANT_INTRO
OP_PR_REDUNDANT_DEL
OP_PR_REFLEXIVITY
OP_PR_REWRITE
OP_PR_REWRITE_STAR
OP_PR_SKOLEMIZE
OP_PR_SYMMETRY
OP_PR_TH_LEMMA
OP_PR_TRANSITIVITY
OP_PR_TRANSITIVITY_STAR
OP_PR_TRUE
OP_PR_UNDEF
OP_PR_UNIT_RESOLUTION
OP_RA_CLONE
OP_RA_COMPLEMENT
OP_RA_EMPTY
OP_RA_FILTER
OP_RA_IS_EMPTY
OP_RA_JOIN
OP_RA_NEGATION_FILTER
OP_RA_PROJECT
OP_RA_RENAME
OP_RA_SELECT
OP_RA_STORE
OP_RA_UNION
OP_RA_WIDEN
OP_RE_COMPLEMENT
OP_RE_CONCAT
OP_RE_DERIVATIVE
OP_RE_DIFF
OP_RE_EMPTY_SET
OP_RE_FULL_CHAR_SET
OP_RE_FULL_SET
OP_RE_INTERSECT
OP_RE_LOOP
OP_RE_OF_PRED
OP_RE_OPTION
OP_RE_PLUS
OP_RE_POWER
OP_RE_RANGE
OP_RE_REVERSE
OP_RE_STAR
OP_RE_UNION
OP_RECURSIVE
OP_REM
OP_REPEAT
OP_ROTATE_LEFT
OP_ROTATE_RIGHT
OP_SBV_TO_STR
OP_SELECT
OP_SEQ_AT
OP_SEQ_CONCAT
OP_SEQ_CONTAINS
OP_SEQ_EMPTY
OP_SEQ_EXTRACT
OP_SEQ_IN_RE
OP_SEQ_INDEX
OP_SEQ_LAST_INDEX
OP_SEQ_LENGTH
OP_SEQ_NTH
OP_SEQ_PREFIX
OP_SEQ_REPLACE
OP_SEQ_REPLACE_ALL
OP_SEQ_REPLACE_RE
OP_SEQ_REPLACE_RE_ALL
OP_SEQ_SUFFIX
OP_SEQ_TO_RE
OP_SEQ_UNIT
OP_SET_CARD
OP_SET_COMPLEMENT
OP_SET_DIFFERENCE
OP_SET_HAS_SIZE
OP_SET_INTERSECT
OP_SET_SUBSET
OP_SET_UNION
OP_SGEQ
OP_SGT
OP_SIGN_EXT
OP_SLEQ
OP_SLT
OP_SPECIAL_RELATION_LO
OP_SPECIAL_RELATION_PLO
OP_SPECIAL_RELATION_PO
OP_SPECIAL_RELATION_TC
OP_SPECIAL_RELATION_TO
OP_SPECIAL_RELATION_TRC
OP_STORE
OP_STR_FROM_CODE
OP_STR_TO_CODE
OP_STR_TO_INT
OP_STRING_LE
OP_STRING_LT
OP_SUB
OP_TO_INT
OP_TO_REAL
OP_TRUE
OP_UBV_TO_STR
OP_UGEQ
OP_UGT
OP_ULEQ
OP_ULT
OP_UMINUS
OP_UNINTERPRETED
OP_XOR
OP_XOR3
OP_ZERO_EXT