Public Member Functions | |
Z3_decl_kind (int v) | |
final int | toInt () |
Static Public Member Functions | |
static final Z3_decl_kind | fromInt (int v) |
Definition at line 13 of file Z3_decl_kind.java.
|
inline |
Definition at line 248 of file Z3_decl_kind.java.
|
inlinestatic |
|
inline |
Definition at line 268 of file Z3_decl_kind.java.
Z3_OP_ADD =(518) |
Definition at line 33 of file Z3_decl_kind.java.
Referenced by Expr.isAdd().
Z3_OP_AGNUM =(513) |
Definition at line 28 of file Z3_decl_kind.java.
Z3_OP_AND =(261) |
Definition at line 19 of file Z3_decl_kind.java.
Referenced by Expr.isAnd().
Z3_OP_ANUM =(512) |
Definition at line 27 of file Z3_decl_kind.java.
Referenced by Expr.isArithmeticNumeral().
Z3_OP_ARRAY_DEFAULT =(772) |
Definition at line 49 of file Z3_decl_kind.java.
Referenced by Expr.isDefaultArray().
Z3_OP_ARRAY_EXT =(779) |
Definition at line 56 of file Z3_decl_kind.java.
Z3_OP_ARRAY_MAP =(771) |
Definition at line 48 of file Z3_decl_kind.java.
Referenced by Expr.isArrayMap().
Z3_OP_AS_ARRAY =(778) |
Definition at line 55 of file Z3_decl_kind.java.
Referenced by Expr.isAsArray().
Z3_OP_BADD =(1028) |
Definition at line 61 of file Z3_decl_kind.java.
Referenced by Expr.isBVAdd().
Z3_OP_BAND =(1049) |
Definition at line 82 of file Z3_decl_kind.java.
Referenced by Expr.isBVAND().
Z3_OP_BASHR =(1066) |
Definition at line 99 of file Z3_decl_kind.java.
Referenced by Expr.isBVShiftRightArithmetic().
Z3_OP_BCOMP =(1063) |
Definition at line 96 of file Z3_decl_kind.java.
Referenced by Expr.isBVComp().
Z3_OP_BIT0 =(1026) |
Definition at line 59 of file Z3_decl_kind.java.
Referenced by Expr.isBVBitZero().
Z3_OP_BIT1 =(1025) |
Definition at line 58 of file Z3_decl_kind.java.
Referenced by Expr.isBVBitOne().
Z3_OP_BLSHR =(1065) |
Definition at line 98 of file Z3_decl_kind.java.
Referenced by Expr.isBVShiftRightLogical().
Z3_OP_BMUL =(1030) |
Definition at line 63 of file Z3_decl_kind.java.
Referenced by Expr.isBVMul().
Z3_OP_BNAND =(1053) |
Definition at line 86 of file Z3_decl_kind.java.
Referenced by Expr.isBVNAND().
Z3_OP_BNEG =(1027) |
Definition at line 60 of file Z3_decl_kind.java.
Referenced by Expr.isBVUMinus().
Z3_OP_BNOR =(1054) |
Definition at line 87 of file Z3_decl_kind.java.
Referenced by Expr.isBVNOR().
Z3_OP_BNOT =(1051) |
Definition at line 84 of file Z3_decl_kind.java.
Referenced by Expr.isBVNOT().
Z3_OP_BNUM =(1024) |
Definition at line 57 of file Z3_decl_kind.java.
Referenced by Expr.isBVNumeral().
Z3_OP_BOR =(1050) |
Definition at line 83 of file Z3_decl_kind.java.
Referenced by Expr.isBVOR().
Z3_OP_BREDAND =(1062) |
Definition at line 95 of file Z3_decl_kind.java.
Referenced by Expr.isBVReduceAND().
Z3_OP_BREDOR =(1061) |
Definition at line 94 of file Z3_decl_kind.java.
Referenced by Expr.isBVReduceOR().
Z3_OP_BSDIV =(1031) |
Definition at line 64 of file Z3_decl_kind.java.
Referenced by Expr.isBVSDiv().
Z3_OP_BSDIV0 =(1036) |
Definition at line 69 of file Z3_decl_kind.java.
Referenced by Expr.isBVSMod().
Z3_OP_BSDIV_I =(1078) |
Definition at line 111 of file Z3_decl_kind.java.
Z3_OP_BSHL =(1064) |
Definition at line 97 of file Z3_decl_kind.java.
Referenced by Expr.isBVShiftLeft().
Z3_OP_BSMOD =(1035) |
Definition at line 68 of file Z3_decl_kind.java.
Referenced by Expr.isBVSMod().
Z3_OP_BSMOD0 =(1040) |
Definition at line 73 of file Z3_decl_kind.java.
Referenced by Expr.isBVSMod().
Z3_OP_BSMOD_I =(1082) |
Definition at line 115 of file Z3_decl_kind.java.
Z3_OP_BSMUL_NO_OVFL =(1075) |
Definition at line 108 of file Z3_decl_kind.java.
Z3_OP_BSMUL_NO_UDFL =(1077) |
Definition at line 110 of file Z3_decl_kind.java.
Z3_OP_BSREM =(1033) |
Definition at line 66 of file Z3_decl_kind.java.
Referenced by Expr.isBVSRem().
Z3_OP_BSREM0 =(1038) |
Definition at line 71 of file Z3_decl_kind.java.
Referenced by Expr.isBVSMod().
Z3_OP_BSREM_I =(1080) |
Definition at line 113 of file Z3_decl_kind.java.
Z3_OP_BSUB =(1029) |
Definition at line 62 of file Z3_decl_kind.java.
Referenced by Expr.isBVSub().
Z3_OP_BUDIV =(1032) |
Definition at line 65 of file Z3_decl_kind.java.
Referenced by Expr.isBVUDiv().
Z3_OP_BUDIV0 =(1037) |
Definition at line 70 of file Z3_decl_kind.java.
Referenced by Expr.isBVSMod().
Z3_OP_BUDIV_I =(1079) |
Definition at line 112 of file Z3_decl_kind.java.
Z3_OP_BUMUL_NO_OVFL =(1076) |
Definition at line 109 of file Z3_decl_kind.java.
Z3_OP_BUREM =(1034) |
Definition at line 67 of file Z3_decl_kind.java.
Referenced by Expr.isBVURem().
Z3_OP_BUREM0 =(1039) |
Definition at line 72 of file Z3_decl_kind.java.
Referenced by Expr.isBVSMod().
Z3_OP_BUREM_I =(1081) |
Definition at line 114 of file Z3_decl_kind.java.
Z3_OP_BV2INT =(1072) |
Definition at line 105 of file Z3_decl_kind.java.
Referenced by Expr.isBVToInt().
Z3_OP_BXNOR =(1055) |
Definition at line 88 of file Z3_decl_kind.java.
Referenced by Expr.isBVXNOR().
Z3_OP_BXOR =(1052) |
Definition at line 85 of file Z3_decl_kind.java.
Referenced by Expr.isBVXOR().
Z3_OP_CARRY =(1073) |
Definition at line 106 of file Z3_decl_kind.java.
Referenced by Expr.isBVCarry().
Z3_OP_CONCAT =(1056) |
Definition at line 89 of file Z3_decl_kind.java.
Referenced by Expr.isBVConcat().
Z3_OP_CONST_ARRAY =(770) |
Definition at line 47 of file Z3_decl_kind.java.
Referenced by Expr.isConstantArray().
Z3_OP_DISTINCT =(259) |
Definition at line 17 of file Z3_decl_kind.java.
Referenced by Expr.isDistinct().
Z3_OP_DIV =(522) |
Definition at line 37 of file Z3_decl_kind.java.
Referenced by Expr.isDiv().
Z3_OP_DT_ACCESSOR =(2050) |
Definition at line 193 of file Z3_decl_kind.java.
Z3_OP_DT_CONSTRUCTOR =(2048) |
Definition at line 191 of file Z3_decl_kind.java.
Z3_OP_DT_RECOGNISER =(2049) |
Definition at line 192 of file Z3_decl_kind.java.
Z3_OP_DT_UPDATE_FIELD =(2051) |
Definition at line 194 of file Z3_decl_kind.java.
Z3_OP_EQ =(258) |
Definition at line 16 of file Z3_decl_kind.java.
Referenced by Expr.isEq().
Z3_OP_EXT_ROTATE_LEFT =(1069) |
Definition at line 102 of file Z3_decl_kind.java.
Referenced by Expr.isBVRotateLeftExtended().
Z3_OP_EXT_ROTATE_RIGHT =(1070) |
Definition at line 103 of file Z3_decl_kind.java.
Referenced by Expr.isBVRotateRightExtended().
Z3_OP_EXTRACT =(1059) |
Definition at line 92 of file Z3_decl_kind.java.
Referenced by Expr.isBVExtract().
Z3_OP_FALSE =(257) |
Definition at line 15 of file Z3_decl_kind.java.
Referenced by Expr.isFalse().
Z3_OP_FD_CONSTANT =(1549) |
Definition at line 169 of file Z3_decl_kind.java.
Z3_OP_FD_LT =(1550) |
Definition at line 170 of file Z3_decl_kind.java.
Referenced by Expr.isFiniteDomainLT().
Z3_OP_FPA_ABS =(2325) |
Definition at line 216 of file Z3_decl_kind.java.
Z3_OP_FPA_ADD =(2319) |
Definition at line 210 of file Z3_decl_kind.java.
Z3_OP_FPA_DIV =(2323) |
Definition at line 214 of file Z3_decl_kind.java.
Z3_OP_FPA_EQ =(2331) |
Definition at line 222 of file Z3_decl_kind.java.
Z3_OP_FPA_FMA =(2328) |
Definition at line 219 of file Z3_decl_kind.java.
Z3_OP_FPA_FP =(2343) |
Definition at line 234 of file Z3_decl_kind.java.
Z3_OP_FPA_GE =(2335) |
Definition at line 226 of file Z3_decl_kind.java.
Z3_OP_FPA_GT =(2333) |
Definition at line 224 of file Z3_decl_kind.java.
Z3_OP_FPA_IS_INF =(2337) |
Definition at line 228 of file Z3_decl_kind.java.
Z3_OP_FPA_IS_NAN =(2336) |
Definition at line 227 of file Z3_decl_kind.java.
Z3_OP_FPA_IS_NEGATIVE =(2341) |
Definition at line 232 of file Z3_decl_kind.java.
Z3_OP_FPA_IS_NORMAL =(2339) |
Definition at line 230 of file Z3_decl_kind.java.
Z3_OP_FPA_IS_POSITIVE =(2342) |
Definition at line 233 of file Z3_decl_kind.java.
Z3_OP_FPA_IS_SUBNORMAL =(2340) |
Definition at line 231 of file Z3_decl_kind.java.
Z3_OP_FPA_IS_ZERO =(2338) |
Definition at line 229 of file Z3_decl_kind.java.
Z3_OP_FPA_LE =(2334) |
Definition at line 225 of file Z3_decl_kind.java.
Z3_OP_FPA_LT =(2332) |
Definition at line 223 of file Z3_decl_kind.java.
Z3_OP_FPA_MAX =(2327) |
Definition at line 218 of file Z3_decl_kind.java.
Z3_OP_FPA_MAX_I =(2351) |
Definition at line 242 of file Z3_decl_kind.java.
Z3_OP_FPA_MIN =(2326) |
Definition at line 217 of file Z3_decl_kind.java.
Z3_OP_FPA_MIN_I =(2350) |
Definition at line 241 of file Z3_decl_kind.java.
Z3_OP_FPA_MINUS_INF =(2315) |
Definition at line 206 of file Z3_decl_kind.java.
Z3_OP_FPA_MINUS_ZERO =(2318) |
Definition at line 209 of file Z3_decl_kind.java.
Z3_OP_FPA_MUL =(2322) |
Definition at line 213 of file Z3_decl_kind.java.
Z3_OP_FPA_NAN =(2316) |
Definition at line 207 of file Z3_decl_kind.java.
Z3_OP_FPA_NEG =(2321) |
Definition at line 212 of file Z3_decl_kind.java.
Z3_OP_FPA_NUM =(2313) |
Definition at line 204 of file Z3_decl_kind.java.
Z3_OP_FPA_PLUS_INF =(2314) |
Definition at line 205 of file Z3_decl_kind.java.
Z3_OP_FPA_PLUS_ZERO =(2317) |
Definition at line 208 of file Z3_decl_kind.java.
Z3_OP_FPA_REM =(2324) |
Definition at line 215 of file Z3_decl_kind.java.
Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY =(2309) |
Definition at line 200 of file Z3_decl_kind.java.
Referenced by FPRMNum.isRNA(), and FPRMNum.isRoundNearestTiesToAway().
Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN =(2308) |
Definition at line 199 of file Z3_decl_kind.java.
Referenced by FPRMNum.isRNE(), and FPRMNum.isRoundNearestTiesToEven().
Z3_OP_FPA_RM_TOWARD_NEGATIVE =(2311) |
Definition at line 202 of file Z3_decl_kind.java.
Referenced by FPRMNum.isRoundTowardNegative(), and FPRMNum.isRTN().
Z3_OP_FPA_RM_TOWARD_POSITIVE =(2310) |
Definition at line 201 of file Z3_decl_kind.java.
Referenced by FPRMNum.isRoundTowardPositive(), and FPRMNum.isRTP().
Z3_OP_FPA_RM_TOWARD_ZERO =(2312) |
Definition at line 203 of file Z3_decl_kind.java.
Referenced by FPRMNum.isRoundTowardZero(), and FPRMNum.isRTZ().
Z3_OP_FPA_ROUND_TO_INTEGRAL =(2330) |
Definition at line 221 of file Z3_decl_kind.java.
Z3_OP_FPA_SQRT =(2329) |
Definition at line 220 of file Z3_decl_kind.java.
Z3_OP_FPA_SUB =(2320) |
Definition at line 211 of file Z3_decl_kind.java.
Z3_OP_FPA_TO_FP =(2344) |
Definition at line 235 of file Z3_decl_kind.java.
Z3_OP_FPA_TO_FP_UNSIGNED =(2345) |
Definition at line 236 of file Z3_decl_kind.java.
Z3_OP_FPA_TO_IEEE_BV =(2349) |
Definition at line 240 of file Z3_decl_kind.java.
Z3_OP_FPA_TO_REAL =(2348) |
Definition at line 239 of file Z3_decl_kind.java.
Z3_OP_FPA_TO_SBV =(2347) |
Definition at line 238 of file Z3_decl_kind.java.
Z3_OP_FPA_TO_UBV =(2346) |
Definition at line 237 of file Z3_decl_kind.java.
Z3_OP_GE =(515) |
Definition at line 30 of file Z3_decl_kind.java.
Referenced by Expr.isGE().
Z3_OP_GT =(517) |
Definition at line 32 of file Z3_decl_kind.java.
Referenced by Expr.isGT().
Z3_OP_IDIV =(523) |
Definition at line 38 of file Z3_decl_kind.java.
Referenced by Expr.isIDiv().
Z3_OP_IFF =(263) |
Definition at line 21 of file Z3_decl_kind.java.
Referenced by Expr.isIff().
Z3_OP_IMPLIES =(266) |
Definition at line 24 of file Z3_decl_kind.java.
Referenced by Expr.isImplies().
Z3_OP_INT2BV =(1071) |
Definition at line 104 of file Z3_decl_kind.java.
Referenced by Expr.isIntToBV().
Z3_OP_INTERNAL =(2352) |
Definition at line 243 of file Z3_decl_kind.java.
Z3_OP_INTERP =(268) |
Definition at line 26 of file Z3_decl_kind.java.
Z3_OP_IS_INT =(528) |
Definition at line 43 of file Z3_decl_kind.java.
Referenced by Expr.isRealIsInt().
Z3_OP_ITE =(260) |
Definition at line 18 of file Z3_decl_kind.java.
Referenced by Expr.isITE().
Z3_OP_LABEL =(1792) |
Definition at line 189 of file Z3_decl_kind.java.
Referenced by Expr.isLabel().
Z3_OP_LABEL_LIT =(1793) |
Definition at line 190 of file Z3_decl_kind.java.
Referenced by Expr.isLabelLit().
Z3_OP_LE =(514) |
Definition at line 29 of file Z3_decl_kind.java.
Referenced by Expr.isLE().
Z3_OP_LT =(516) |
Definition at line 31 of file Z3_decl_kind.java.
Referenced by Expr.isLT().
Z3_OP_MOD =(525) |
Definition at line 40 of file Z3_decl_kind.java.
Referenced by Expr.isModulus().
Z3_OP_MUL =(521) |
Definition at line 36 of file Z3_decl_kind.java.
Referenced by Expr.isMul().
Z3_OP_NOT =(265) |
Definition at line 23 of file Z3_decl_kind.java.
Referenced by Expr.isNot().
Z3_OP_OEQ =(267) |
Definition at line 25 of file Z3_decl_kind.java.
Referenced by Expr.isOEQ().
Z3_OP_OR =(262) |
Definition at line 20 of file Z3_decl_kind.java.
Referenced by Expr.isOr().
Z3_OP_PB_AT_MOST =(2304) |
Definition at line 195 of file Z3_decl_kind.java.
Z3_OP_PB_EQ =(2307) |
Definition at line 198 of file Z3_decl_kind.java.
Z3_OP_PB_GE =(2306) |
Definition at line 197 of file Z3_decl_kind.java.
Z3_OP_PB_LE =(2305) |
Definition at line 196 of file Z3_decl_kind.java.
Z3_OP_POWER =(529) |
Definition at line 44 of file Z3_decl_kind.java.
Z3_OP_PR_AND_ELIM =(1292) |
Definition at line 128 of file Z3_decl_kind.java.
Referenced by Expr.isProofAndElimination().
Z3_OP_PR_APPLY_DEF =(1310) |
Definition at line 146 of file Z3_decl_kind.java.
Referenced by Expr.isProofApplyDef().
Z3_OP_PR_ASSERTED =(1282) |
Definition at line 118 of file Z3_decl_kind.java.
Referenced by Expr.isProofAsserted().
Z3_OP_PR_CNF_STAR =(1315) |
Definition at line 151 of file Z3_decl_kind.java.
Referenced by Expr.isProofCNFStar().
Z3_OP_PR_COMMUTATIVITY =(1307) |
Definition at line 143 of file Z3_decl_kind.java.
Referenced by Expr.isProofCommutativity().
Z3_OP_PR_DEF_AXIOM =(1308) |
Definition at line 144 of file Z3_decl_kind.java.
Referenced by Expr.isProofDefAxiom().
Z3_OP_PR_DEF_INTRO =(1309) |
Definition at line 145 of file Z3_decl_kind.java.
Referenced by Expr.isProofDefIntro().
Z3_OP_PR_DER =(1300) |
Definition at line 136 of file Z3_decl_kind.java.
Referenced by Expr.isProofDER().
Z3_OP_PR_DISTRIBUTIVITY =(1291) |
Definition at line 127 of file Z3_decl_kind.java.
Referenced by Expr.isProofDistributivity().
Z3_OP_PR_ELIM_UNUSED_VARS =(1299) |
Definition at line 135 of file Z3_decl_kind.java.
Referenced by Expr.isProofElimUnusedVars().
Z3_OP_PR_GOAL =(1283) |
Definition at line 119 of file Z3_decl_kind.java.
Referenced by Expr.isProofGoal().
Z3_OP_PR_HYPER_RESOLVE =(1319) |
Definition at line 155 of file Z3_decl_kind.java.
Z3_OP_PR_HYPOTHESIS =(1302) |
Definition at line 138 of file Z3_decl_kind.java.
Referenced by Expr.isProofHypothesis().
Z3_OP_PR_IFF_FALSE =(1306) |
Definition at line 142 of file Z3_decl_kind.java.
Referenced by Expr.isProofIFFFalse().
Z3_OP_PR_IFF_OEQ =(1311) |
Definition at line 147 of file Z3_decl_kind.java.
Referenced by Expr.isProofIFFOEQ().
Z3_OP_PR_IFF_TRUE =(1305) |
Definition at line 141 of file Z3_decl_kind.java.
Referenced by Expr.isProofIFFTrue().
Z3_OP_PR_LEMMA =(1303) |
Definition at line 139 of file Z3_decl_kind.java.
Referenced by Expr.isProofLemma().
Z3_OP_PR_MODUS_PONENS =(1284) |
Definition at line 120 of file Z3_decl_kind.java.
Referenced by Expr.isProofModusPonens().
Z3_OP_PR_MODUS_PONENS_OEQ =(1317) |
Definition at line 153 of file Z3_decl_kind.java.
Referenced by Expr.isProofModusPonensOEQ().
Z3_OP_PR_MONOTONICITY =(1289) |
Definition at line 125 of file Z3_decl_kind.java.
Referenced by Expr.isProofMonotonicity().
Z3_OP_PR_NNF_NEG =(1313) |
Definition at line 149 of file Z3_decl_kind.java.
Referenced by Expr.isProofNNFNeg().
Z3_OP_PR_NNF_POS =(1312) |
Definition at line 148 of file Z3_decl_kind.java.
Referenced by Expr.isProofNNFPos().
Z3_OP_PR_NNF_STAR =(1314) |
Definition at line 150 of file Z3_decl_kind.java.
Referenced by Expr.isProofNNFStar().
Z3_OP_PR_NOT_OR_ELIM =(1293) |
Definition at line 129 of file Z3_decl_kind.java.
Referenced by Expr.isProofOrElimination().
Z3_OP_PR_PULL_QUANT =(1296) |
Definition at line 132 of file Z3_decl_kind.java.
Referenced by Expr.isProofPullQuant().
Z3_OP_PR_PULL_QUANT_STAR =(1297) |
Definition at line 133 of file Z3_decl_kind.java.
Referenced by Expr.isProofPullQuantStar().
Z3_OP_PR_PUSH_QUANT =(1298) |
Definition at line 134 of file Z3_decl_kind.java.
Referenced by Expr.isProofPushQuant().
Z3_OP_PR_QUANT_INST =(1301) |
Definition at line 137 of file Z3_decl_kind.java.
Referenced by Expr.isProofQuantInst().
Z3_OP_PR_QUANT_INTRO =(1290) |
Definition at line 126 of file Z3_decl_kind.java.
Referenced by Expr.isProofQuantIntro().
Z3_OP_PR_REFLEXIVITY =(1285) |
Definition at line 121 of file Z3_decl_kind.java.
Referenced by Expr.isProofReflexivity().
Z3_OP_PR_REWRITE =(1294) |
Definition at line 130 of file Z3_decl_kind.java.
Referenced by Expr.isProofRewrite().
Z3_OP_PR_REWRITE_STAR =(1295) |
Definition at line 131 of file Z3_decl_kind.java.
Referenced by Expr.isProofRewriteStar().
Z3_OP_PR_SKOLEMIZE =(1316) |
Definition at line 152 of file Z3_decl_kind.java.
Referenced by Expr.isProofSkolemize().
Z3_OP_PR_SYMMETRY =(1286) |
Definition at line 122 of file Z3_decl_kind.java.
Referenced by Expr.isProofSymmetry().
Z3_OP_PR_TH_LEMMA =(1318) |
Definition at line 154 of file Z3_decl_kind.java.
Referenced by Expr.isProofTheoryLemma().
Z3_OP_PR_TRANSITIVITY =(1287) |
Definition at line 123 of file Z3_decl_kind.java.
Referenced by Expr.isProofTransitivity().
Z3_OP_PR_TRANSITIVITY_STAR =(1288) |
Definition at line 124 of file Z3_decl_kind.java.
Referenced by Expr.isProofTransitivityStar().
Z3_OP_PR_TRUE =(1281) |
Definition at line 117 of file Z3_decl_kind.java.
Referenced by Expr.isProofTrue().
Z3_OP_PR_UNDEF =(1280) |
Definition at line 116 of file Z3_decl_kind.java.
Z3_OP_PR_UNIT_RESOLUTION =(1304) |
Definition at line 140 of file Z3_decl_kind.java.
Referenced by Expr.isProofUnitResolution().
Z3_OP_RA_CLONE =(1548) |
Definition at line 168 of file Z3_decl_kind.java.
Referenced by Expr.isRelationClone().
Z3_OP_RA_COMPLEMENT =(1546) |
Definition at line 166 of file Z3_decl_kind.java.
Referenced by Expr.isRelationComplement().
Z3_OP_RA_EMPTY =(1537) |
Definition at line 157 of file Z3_decl_kind.java.
Referenced by Expr.isEmptyRelation().
Z3_OP_RA_FILTER =(1543) |
Definition at line 163 of file Z3_decl_kind.java.
Referenced by Expr.isRelationFilter().
Z3_OP_RA_IS_EMPTY =(1538) |
Definition at line 158 of file Z3_decl_kind.java.
Referenced by Expr.isIsEmptyRelation().
Z3_OP_RA_JOIN =(1539) |
Definition at line 159 of file Z3_decl_kind.java.
Referenced by Expr.isRelationalJoin().
Z3_OP_RA_NEGATION_FILTER =(1544) |
Definition at line 164 of file Z3_decl_kind.java.
Referenced by Expr.isRelationNegationFilter().
Z3_OP_RA_PROJECT =(1542) |
Definition at line 162 of file Z3_decl_kind.java.
Referenced by Expr.isRelationProject().
Z3_OP_RA_RENAME =(1545) |
Definition at line 165 of file Z3_decl_kind.java.
Referenced by Expr.isRelationRename().
Z3_OP_RA_SELECT =(1547) |
Definition at line 167 of file Z3_decl_kind.java.
Referenced by Expr.isRelationSelect().
Z3_OP_RA_STORE =(1536) |
Definition at line 156 of file Z3_decl_kind.java.
Referenced by Expr.isRelationStore().
Z3_OP_RA_UNION =(1540) |
Definition at line 160 of file Z3_decl_kind.java.
Referenced by Expr.isRelationUnion().
Z3_OP_RA_WIDEN =(1541) |
Definition at line 161 of file Z3_decl_kind.java.
Referenced by Expr.isRelationWiden().
Z3_OP_RE_CONCAT =(1567) |
Definition at line 187 of file Z3_decl_kind.java.
Z3_OP_RE_OPTION =(1566) |
Definition at line 186 of file Z3_decl_kind.java.
Z3_OP_RE_PLUS =(1564) |
Definition at line 184 of file Z3_decl_kind.java.
Z3_OP_RE_STAR =(1565) |
Definition at line 185 of file Z3_decl_kind.java.
Z3_OP_RE_UNION =(1568) |
Definition at line 188 of file Z3_decl_kind.java.
Z3_OP_REM =(524) |
Definition at line 39 of file Z3_decl_kind.java.
Referenced by Expr.isRemainder().
Z3_OP_REPEAT =(1060) |
Definition at line 93 of file Z3_decl_kind.java.
Referenced by Expr.isBVRepeat().
Z3_OP_ROTATE_LEFT =(1067) |
Definition at line 100 of file Z3_decl_kind.java.
Referenced by Expr.isBVRotateLeft().
Z3_OP_ROTATE_RIGHT =(1068) |
Definition at line 101 of file Z3_decl_kind.java.
Referenced by Expr.isBVRotateRight().
Z3_OP_SELECT =(769) |
Definition at line 46 of file Z3_decl_kind.java.
Referenced by Expr.isSelect().
Z3_OP_SEQ_AT =(1559) |
Definition at line 179 of file Z3_decl_kind.java.
Z3_OP_SEQ_CONCAT =(1553) |
Definition at line 173 of file Z3_decl_kind.java.
Z3_OP_SEQ_CONTAINS =(1556) |
Definition at line 176 of file Z3_decl_kind.java.
Z3_OP_SEQ_EMPTY =(1552) |
Definition at line 172 of file Z3_decl_kind.java.
Z3_OP_SEQ_EXTRACT =(1557) |
Definition at line 177 of file Z3_decl_kind.java.
Z3_OP_SEQ_IN_RE =(1563) |
Definition at line 183 of file Z3_decl_kind.java.
Z3_OP_SEQ_INDEX =(1561) |
Definition at line 181 of file Z3_decl_kind.java.
Z3_OP_SEQ_LENGTH =(1560) |
Definition at line 180 of file Z3_decl_kind.java.
Z3_OP_SEQ_PREFIX =(1554) |
Definition at line 174 of file Z3_decl_kind.java.
Z3_OP_SEQ_REPLACE =(1558) |
Definition at line 178 of file Z3_decl_kind.java.
Z3_OP_SEQ_SUFFIX =(1555) |
Definition at line 175 of file Z3_decl_kind.java.
Z3_OP_SEQ_TO_RE =(1562) |
Definition at line 182 of file Z3_decl_kind.java.
Z3_OP_SEQ_UNIT =(1551) |
Definition at line 171 of file Z3_decl_kind.java.
Z3_OP_SET_COMPLEMENT =(776) |
Definition at line 53 of file Z3_decl_kind.java.
Referenced by Expr.isSetComplement().
Z3_OP_SET_DIFFERENCE =(775) |
Definition at line 52 of file Z3_decl_kind.java.
Referenced by Expr.isSetDifference().
Z3_OP_SET_INTERSECT =(774) |
Definition at line 51 of file Z3_decl_kind.java.
Referenced by Expr.isSetIntersect().
Z3_OP_SET_SUBSET =(777) |
Definition at line 54 of file Z3_decl_kind.java.
Referenced by Expr.isSetSubset().
Z3_OP_SET_UNION =(773) |
Definition at line 50 of file Z3_decl_kind.java.
Referenced by Expr.isSetUnion().
Z3_OP_SGEQ =(1044) |
Definition at line 77 of file Z3_decl_kind.java.
Referenced by Expr.isBVSGE().
Z3_OP_SGT =(1048) |
Definition at line 81 of file Z3_decl_kind.java.
Referenced by Expr.isBVSGT().
Z3_OP_SIGN_EXT =(1057) |
Definition at line 90 of file Z3_decl_kind.java.
Referenced by Expr.isBVSignExtension().
Z3_OP_SLEQ =(1042) |
Definition at line 75 of file Z3_decl_kind.java.
Referenced by Expr.isBVSLE().
Z3_OP_SLT =(1046) |
Definition at line 79 of file Z3_decl_kind.java.
Referenced by Expr.isBVSLT().
Z3_OP_STORE =(768) |
Definition at line 45 of file Z3_decl_kind.java.
Referenced by Expr.isStore().
Z3_OP_SUB =(519) |
Definition at line 34 of file Z3_decl_kind.java.
Referenced by Expr.isSub().
Z3_OP_TO_INT =(527) |
Definition at line 42 of file Z3_decl_kind.java.
Referenced by Expr.isRealToInt().
Z3_OP_TO_REAL =(526) |
Definition at line 41 of file Z3_decl_kind.java.
Referenced by Expr.isIntToReal().
Z3_OP_TRUE =(256) |
Definition at line 14 of file Z3_decl_kind.java.
Referenced by Expr.isTrue().
Z3_OP_UGEQ =(1043) |
Definition at line 76 of file Z3_decl_kind.java.
Referenced by Expr.isBVUGE().
Z3_OP_UGT =(1047) |
Definition at line 80 of file Z3_decl_kind.java.
Referenced by Expr.isBVUGT().
Z3_OP_ULEQ =(1041) |
Definition at line 74 of file Z3_decl_kind.java.
Referenced by Expr.isBVULE().
Z3_OP_ULT =(1045) |
Definition at line 78 of file Z3_decl_kind.java.
Referenced by Expr.isBVULT().
Z3_OP_UMINUS =(520) |
Definition at line 35 of file Z3_decl_kind.java.
Referenced by Expr.isUMinus().
Z3_OP_UNINTERPRETED =(2353) |
Definition at line 244 of file Z3_decl_kind.java.
Z3_OP_XOR =(264) |
Definition at line 22 of file Z3_decl_kind.java.
Referenced by Expr.isXor().
Z3_OP_XOR3 =(1074) |
Definition at line 107 of file Z3_decl_kind.java.
Referenced by Expr.isBVXOR3().
Z3_OP_ZERO_EXT =(1058) |
Definition at line 91 of file Z3_decl_kind.java.
Referenced by Expr.isBVZeroExtension().