Z3
Public Member Functions | Static Public Member Functions | Data Fields
Z3_decl_kind Enum Reference

Public Member Functions

 Z3_decl_kind (int v)
 
final int toInt ()
 

Static Public Member Functions

static final Z3_decl_kind fromInt (int v)
 

Data Fields

 Z3_OP_LABEL =(1792)
 
 Z3_OP_PR_REWRITE =(1294)
 
 Z3_OP_UNINTERPRETED =(2349)
 
 Z3_OP_SUB =(519)
 
 Z3_OP_ZERO_EXT =(1058)
 
 Z3_OP_ADD =(518)
 
 Z3_OP_FPA_ABS =(2324)
 
 Z3_OP_IS_INT =(528)
 
 Z3_OP_BREDOR =(1061)
 
 Z3_OP_FPA_IS_INF =(2336)
 
 Z3_OP_BNOT =(1051)
 
 Z3_OP_BNOR =(1054)
 
 Z3_OP_PR_CNF_STAR =(1315)
 
 Z3_OP_FPA_TO_UBV =(2345)
 
 Z3_OP_RA_JOIN =(1539)
 
 Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY =(2308)
 
 Z3_OP_LE =(514)
 
 Z3_OP_SET_UNION =(773)
 
 Z3_OP_PR_UNDEF =(1280)
 
 Z3_OP_BREDAND =(1062)
 
 Z3_OP_LT =(516)
 
 Z3_OP_RA_UNION =(1540)
 
 Z3_OP_FPA_IS_SUBNORMAL =(2339)
 
 Z3_OP_BADD =(1028)
 
 Z3_OP_BUREM0 =(1039)
 
 Z3_OP_OEQ =(267)
 
 Z3_OP_PR_MODUS_PONENS =(1284)
 
 Z3_OP_RA_CLONE =(1548)
 
 Z3_OP_REPEAT =(1060)
 
 Z3_OP_RA_NEGATION_FILTER =(1544)
 
 Z3_OP_FPA_NAN =(2315)
 
 Z3_OP_BSMOD0 =(1040)
 
 Z3_OP_FPA_GT =(2332)
 
 Z3_OP_BLSHR =(1065)
 
 Z3_OP_BASHR =(1066)
 
 Z3_OP_PR_UNIT_RESOLUTION =(1304)
 
 Z3_OP_ROTATE_RIGHT =(1068)
 
 Z3_OP_ARRAY_DEFAULT =(772)
 
 Z3_OP_PR_PULL_QUANT =(1296)
 
 Z3_OP_PR_APPLY_DEF =(1310)
 
 Z3_OP_PR_REWRITE_STAR =(1295)
 
 Z3_OP_IDIV =(523)
 
 Z3_OP_PR_GOAL =(1283)
 
 Z3_OP_FPA_RM_TOWARD_POSITIVE =(2309)
 
 Z3_OP_PR_IFF_TRUE =(1305)
 
 Z3_OP_FPA_LT =(2331)
 
 Z3_OP_FPA_IS_NORMAL =(2338)
 
 Z3_OP_LABEL_LIT =(1793)
 
 Z3_OP_FPA_TO_IEEE_BV =(2348)
 
 Z3_OP_FPA_LE =(2333)
 
 Z3_OP_BOR =(1050)
 
 Z3_OP_PR_SYMMETRY =(1286)
 
 Z3_OP_TRUE =(256)
 
 Z3_OP_SET_COMPLEMENT =(776)
 
 Z3_OP_CONCAT =(1056)
 
 Z3_OP_PR_NOT_OR_ELIM =(1293)
 
 Z3_OP_IFF =(263)
 
 Z3_OP_BSHL =(1064)
 
 Z3_OP_PR_TRANSITIVITY =(1287)
 
 Z3_OP_FPA_ROUND_TO_INTEGRAL =(2329)
 
 Z3_OP_SGT =(1048)
 
 Z3_OP_RA_WIDEN =(1541)
 
 Z3_OP_PR_DEF_INTRO =(1309)
 
 Z3_OP_NOT =(265)
 
 Z3_OP_PR_QUANT_INTRO =(1290)
 
 Z3_OP_FPA_PLUS_ZERO =(2316)
 
 Z3_OP_UGT =(1047)
 
 Z3_OP_FPA_NEG =(2320)
 
 Z3_OP_DT_RECOGNISER =(2049)
 
 Z3_OP_SET_INTERSECT =(774)
 
 Z3_OP_BSREM =(1033)
 
 Z3_OP_RA_STORE =(1536)
 
 Z3_OP_SLT =(1046)
 
 Z3_OP_ROTATE_LEFT =(1067)
 
 Z3_OP_PR_NNF_NEG =(1313)
 
 Z3_OP_FPA_EQ =(2330)
 
 Z3_OP_PR_REFLEXIVITY =(1285)
 
 Z3_OP_ULEQ =(1041)
 
 Z3_OP_BIT1 =(1025)
 
 Z3_OP_BIT0 =(1026)
 
 Z3_OP_FPA_MIN =(2325)
 
 Z3_OP_PB_AT_MOST =(2304)
 
 Z3_OP_EQ =(258)
 
 Z3_OP_FPA_SUB =(2319)
 
 Z3_OP_BMUL =(1030)
 
 Z3_OP_ARRAY_MAP =(771)
 
 Z3_OP_STORE =(768)
 
 Z3_OP_PR_HYPOTHESIS =(1302)
 
 Z3_OP_RA_RENAME =(1545)
 
 Z3_OP_AND =(261)
 
 Z3_OP_TO_REAL =(526)
 
 Z3_OP_DT_UPDATE_FIELD =(2051)
 
 Z3_OP_PR_NNF_POS =(1312)
 
 Z3_OP_PR_AND_ELIM =(1292)
 
 Z3_OP_FPA_TO_SBV =(2346)
 
 Z3_OP_MOD =(525)
 
 Z3_OP_BUDIV0 =(1037)
 
 Z3_OP_FPA_MAX =(2326)
 
 Z3_OP_PR_TRUE =(1281)
 
 Z3_OP_BNAND =(1053)
 
 Z3_OP_PR_ELIM_UNUSED_VARS =(1299)
 
 Z3_OP_RA_FILTER =(1543)
 
 Z3_OP_FPA_ADD =(2318)
 
 Z3_OP_FD_LT =(1549)
 
 Z3_OP_RA_EMPTY =(1537)
 
 Z3_OP_DIV =(522)
 
 Z3_OP_ANUM =(512)
 
 Z3_OP_MUL =(521)
 
 Z3_OP_UGEQ =(1043)
 
 Z3_OP_BSREM0 =(1038)
 
 Z3_OP_PR_TH_LEMMA =(1318)
 
 Z3_OP_FPA_MINUS_INF =(2314)
 
 Z3_OP_BXOR =(1052)
 
 Z3_OP_DISTINCT =(259)
 
 Z3_OP_PR_IFF_FALSE =(1306)
 
 Z3_OP_BV2INT =(1072)
 
 Z3_OP_EXT_ROTATE_LEFT =(1069)
 
 Z3_OP_PR_PULL_QUANT_STAR =(1297)
 
 Z3_OP_BSUB =(1029)
 
 Z3_OP_PR_ASSERTED =(1282)
 
 Z3_OP_BXNOR =(1055)
 
 Z3_OP_FPA_IS_ZERO =(2337)
 
 Z3_OP_EXTRACT =(1059)
 
 Z3_OP_PR_DER =(1300)
 
 Z3_OP_DT_CONSTRUCTOR =(2048)
 
 Z3_OP_GT =(517)
 
 Z3_OP_BUREM =(1034)
 
 Z3_OP_IMPLIES =(266)
 
 Z3_OP_SLEQ =(1042)
 
 Z3_OP_GE =(515)
 
 Z3_OP_PB_GE =(2306)
 
 Z3_OP_BAND =(1049)
 
 Z3_OP_ITE =(260)
 
 Z3_OP_AS_ARRAY =(778)
 
 Z3_OP_FPA_IS_POSITIVE =(2341)
 
 Z3_OP_RA_SELECT =(1547)
 
 Z3_OP_CONST_ARRAY =(770)
 
 Z3_OP_FPA_TO_REAL =(2347)
 
 Z3_OP_BSDIV =(1031)
 
 Z3_OP_FPA_IS_NEGATIVE =(2340)
 
 Z3_OP_OR =(262)
 
 Z3_OP_FPA_FP =(2342)
 
 Z3_OP_PR_HYPER_RESOLVE =(1319)
 
 Z3_OP_AGNUM =(513)
 
 Z3_OP_FPA_IS_NAN =(2335)
 
 Z3_OP_PR_PUSH_QUANT =(1298)
 
 Z3_OP_FPA_FMA =(2327)
 
 Z3_OP_BSMOD =(1035)
 
 Z3_OP_PR_IFF_OEQ =(1311)
 
 Z3_OP_INTERP =(268)
 
 Z3_OP_PR_LEMMA =(1303)
 
 Z3_OP_FPA_TO_FP_UNSIGNED =(2344)
 
 Z3_OP_SET_SUBSET =(777)
 
 Z3_OP_FPA_SQRT =(2328)
 
 Z3_OP_PB_LE =(2305)
 
 Z3_OP_FPA_GE =(2334)
 
 Z3_OP_FPA_DIV =(2322)
 
 Z3_OP_FPA_RM_TOWARD_ZERO =(2311)
 
 Z3_OP_SELECT =(769)
 
 Z3_OP_RA_PROJECT =(1542)
 
 Z3_OP_BNEG =(1027)
 
 Z3_OP_UMINUS =(520)
 
 Z3_OP_REM =(524)
 
 Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN =(2307)
 
 Z3_OP_TO_INT =(527)
 
 Z3_OP_PR_QUANT_INST =(1301)
 
 Z3_OP_SGEQ =(1044)
 
 Z3_OP_POWER =(529)
 
 Z3_OP_XOR3 =(1074)
 
 Z3_OP_RA_IS_EMPTY =(1538)
 
 Z3_OP_CARRY =(1073)
 
 Z3_OP_DT_ACCESSOR =(2050)
 
 Z3_OP_PR_TRANSITIVITY_STAR =(1288)
 
 Z3_OP_PR_NNF_STAR =(1314)
 
 Z3_OP_PR_COMMUTATIVITY =(1307)
 
 Z3_OP_ULT =(1045)
 
 Z3_OP_FPA_MUL =(2321)
 
 Z3_OP_BSDIV0 =(1036)
 
 Z3_OP_SET_DIFFERENCE =(775)
 
 Z3_OP_INT2BV =(1071)
 
 Z3_OP_FPA_NUM =(2312)
 
 Z3_OP_FPA_MINUS_ZERO =(2317)
 
 Z3_OP_FPA_REM =(2323)
 
 Z3_OP_XOR =(264)
 
 Z3_OP_FPA_TO_FP =(2343)
 
 Z3_OP_PR_MODUS_PONENS_OEQ =(1317)
 
 Z3_OP_FPA_RM_TOWARD_NEGATIVE =(2310)
 
 Z3_OP_BNUM =(1024)
 
 Z3_OP_BUDIV =(1032)
 
 Z3_OP_PR_MONOTONICITY =(1289)
 
 Z3_OP_PR_DEF_AXIOM =(1308)
 
 Z3_OP_FALSE =(257)
 
 Z3_OP_EXT_ROTATE_RIGHT =(1070)
 
 Z3_OP_PR_DISTRIBUTIVITY =(1291)
 
 Z3_OP_SIGN_EXT =(1057)
 
 Z3_OP_FPA_PLUS_INF =(2313)
 
 Z3_OP_PR_SKOLEMIZE =(1316)
 
 Z3_OP_BCOMP =(1063)
 
 Z3_OP_RA_COMPLEMENT =(1546)
 

Detailed Description

Z3_decl_kind

Definition at line 10 of file Z3_decl_kind.java.

Constructor & Destructor Documentation

Z3_decl_kind ( int  v)
inline

Definition at line 213 of file Z3_decl_kind.java.

213  {
214  this.intValue = v;
215  }

Member Function Documentation

static final Z3_decl_kind fromInt ( int  v)
inlinestatic

Definition at line 217 of file Z3_decl_kind.java.

Referenced by FuncDecl.getDeclKind().

217  {
218  for (Z3_decl_kind k: values())
219  if (k.intValue == v) return k;
220  return values()[0];
221  }
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:988
final int toInt ( )
inline

Definition at line 223 of file Z3_decl_kind.java.

223 { return this.intValue; }

Field Documentation

Z3_OP_ADD =(518)

Definition at line 16 of file Z3_decl_kind.java.

Referenced by Expr.isAdd().

Z3_OP_AGNUM =(513)

Definition at line 154 of file Z3_decl_kind.java.

Z3_OP_AND =(261)

Definition at line 100 of file Z3_decl_kind.java.

Referenced by Expr.isAnd().

Z3_OP_ANUM =(512)

Definition at line 117 of file Z3_decl_kind.java.

Referenced by Expr.isArithmeticNumeral().

Z3_OP_ARRAY_DEFAULT =(772)

Definition at line 48 of file Z3_decl_kind.java.

Referenced by Expr.isDefaultArray().

Z3_OP_ARRAY_MAP =(771)

Definition at line 96 of file Z3_decl_kind.java.

Referenced by Expr.isArrayMap().

Z3_OP_AS_ARRAY =(778)

Definition at line 144 of file Z3_decl_kind.java.

Referenced by Expr.isAsArray().

Z3_OP_BADD =(1028)

Definition at line 34 of file Z3_decl_kind.java.

Referenced by Expr.isBVAdd().

Z3_OP_BAND =(1049)

Definition at line 142 of file Z3_decl_kind.java.

Referenced by Expr.isBVAND().

Z3_OP_BASHR =(1066)

Definition at line 45 of file Z3_decl_kind.java.

Referenced by Expr.isBVShiftRightArithmetic().

Z3_OP_BCOMP =(1063)

Definition at line 208 of file Z3_decl_kind.java.

Referenced by Expr.isBVComp().

Z3_OP_BIT0 =(1026)

Definition at line 90 of file Z3_decl_kind.java.

Referenced by Expr.isBVBitZero().

Z3_OP_BIT1 =(1025)

Definition at line 89 of file Z3_decl_kind.java.

Referenced by Expr.isBVBitOne().

Z3_OP_BLSHR =(1065)

Definition at line 44 of file Z3_decl_kind.java.

Referenced by Expr.isBVShiftRightLogical().

Z3_OP_BMUL =(1030)

Definition at line 95 of file Z3_decl_kind.java.

Referenced by Expr.isBVMul().

Z3_OP_BNAND =(1053)

Definition at line 110 of file Z3_decl_kind.java.

Referenced by Expr.isBVNAND().

Z3_OP_BNEG =(1027)

Definition at line 171 of file Z3_decl_kind.java.

Referenced by Expr.isBVUMinus().

Z3_OP_BNOR =(1054)

Definition at line 22 of file Z3_decl_kind.java.

Referenced by Expr.isBVNOR().

Z3_OP_BNOT =(1051)

Definition at line 21 of file Z3_decl_kind.java.

Referenced by Expr.isBVNOT().

Z3_OP_BNUM =(1024)

Definition at line 198 of file Z3_decl_kind.java.

Referenced by Expr.isBVNumeral().

Z3_OP_BOR =(1050)

Definition at line 61 of file Z3_decl_kind.java.

Referenced by Expr.isBVOR().

Z3_OP_BREDAND =(1062)

Definition at line 30 of file Z3_decl_kind.java.

Referenced by Expr.isBVReduceAND().

Z3_OP_BREDOR =(1061)

Definition at line 19 of file Z3_decl_kind.java.

Referenced by Expr.isBVReduceOR().

Z3_OP_BSDIV =(1031)

Definition at line 149 of file Z3_decl_kind.java.

Referenced by Expr.isBVSDiv().

Z3_OP_BSDIV0 =(1036)

Definition at line 188 of file Z3_decl_kind.java.

Referenced by Expr.isBVSMod().

Z3_OP_BSHL =(1064)

Definition at line 68 of file Z3_decl_kind.java.

Referenced by Expr.isBVShiftLeft().

Z3_OP_BSMOD =(1035)

Definition at line 158 of file Z3_decl_kind.java.

Referenced by Expr.isBVSMod().

Z3_OP_BSMOD0 =(1040)

Definition at line 42 of file Z3_decl_kind.java.

Referenced by Expr.isBVSMod().

Z3_OP_BSREM =(1033)

Definition at line 81 of file Z3_decl_kind.java.

Referenced by Expr.isBVSRem().

Z3_OP_BSREM0 =(1038)

Definition at line 120 of file Z3_decl_kind.java.

Referenced by Expr.isBVSMod().

Z3_OP_BSUB =(1029)

Definition at line 129 of file Z3_decl_kind.java.

Referenced by Expr.isBVSub().

Z3_OP_BUDIV =(1032)

Definition at line 199 of file Z3_decl_kind.java.

Referenced by Expr.isBVUDiv().

Z3_OP_BUDIV0 =(1037)

Definition at line 107 of file Z3_decl_kind.java.

Referenced by Expr.isBVSMod().

Z3_OP_BUREM =(1034)

Definition at line 137 of file Z3_decl_kind.java.

Referenced by Expr.isBVURem().

Z3_OP_BUREM0 =(1039)

Definition at line 35 of file Z3_decl_kind.java.

Referenced by Expr.isBVSMod().

Z3_OP_BV2INT =(1072)

Definition at line 126 of file Z3_decl_kind.java.

Referenced by Expr.isBVToInt().

Z3_OP_BXNOR =(1055)

Definition at line 131 of file Z3_decl_kind.java.

Referenced by Expr.isBVXNOR().

Z3_OP_BXOR =(1052)

Definition at line 123 of file Z3_decl_kind.java.

Referenced by Expr.isBVXOR().

Z3_OP_CARRY =(1073)

Definition at line 181 of file Z3_decl_kind.java.

Referenced by Expr.isBVCarry().

Z3_OP_CONCAT =(1056)

Definition at line 65 of file Z3_decl_kind.java.

Referenced by Expr.isBVConcat().

Z3_OP_CONST_ARRAY =(770)

Definition at line 147 of file Z3_decl_kind.java.

Referenced by Expr.isConstantArray().

Z3_OP_DISTINCT =(259)

Definition at line 124 of file Z3_decl_kind.java.

Referenced by Expr.isDistinct().

Z3_OP_DIV =(522)

Definition at line 116 of file Z3_decl_kind.java.

Referenced by Expr.isDiv().

Z3_OP_DT_ACCESSOR =(2050)

Definition at line 182 of file Z3_decl_kind.java.

Z3_OP_DT_CONSTRUCTOR =(2048)

Definition at line 135 of file Z3_decl_kind.java.

Z3_OP_DT_RECOGNISER =(2049)

Definition at line 79 of file Z3_decl_kind.java.

Z3_OP_DT_UPDATE_FIELD =(2051)

Definition at line 102 of file Z3_decl_kind.java.

Z3_OP_EQ =(258)

Definition at line 93 of file Z3_decl_kind.java.

Referenced by Expr.isEq().

Z3_OP_EXT_ROTATE_LEFT =(1069)

Definition at line 127 of file Z3_decl_kind.java.

Referenced by Expr.isBVRotateLeftExtended().

Z3_OP_EXT_ROTATE_RIGHT =(1070)

Definition at line 203 of file Z3_decl_kind.java.

Referenced by Expr.isBVRotateRightExtended().

Z3_OP_EXTRACT =(1059)

Definition at line 133 of file Z3_decl_kind.java.

Referenced by Expr.isBVExtract().

Z3_OP_FALSE =(257)

Definition at line 202 of file Z3_decl_kind.java.

Referenced by Expr.isFalse().

Z3_OP_FD_LT =(1549)

Definition at line 114 of file Z3_decl_kind.java.

Referenced by Expr.isFiniteDomainLT().

Z3_OP_FPA_ABS =(2324)

Definition at line 17 of file Z3_decl_kind.java.

Z3_OP_FPA_ADD =(2318)

Definition at line 113 of file Z3_decl_kind.java.

Z3_OP_FPA_DIV =(2322)

Definition at line 167 of file Z3_decl_kind.java.

Z3_OP_FPA_EQ =(2330)

Definition at line 86 of file Z3_decl_kind.java.

Z3_OP_FPA_FMA =(2327)

Definition at line 157 of file Z3_decl_kind.java.

Z3_OP_FPA_FP =(2342)

Definition at line 152 of file Z3_decl_kind.java.

Z3_OP_FPA_GE =(2334)

Definition at line 166 of file Z3_decl_kind.java.

Z3_OP_FPA_GT =(2332)

Definition at line 43 of file Z3_decl_kind.java.

Z3_OP_FPA_IS_INF =(2336)

Definition at line 20 of file Z3_decl_kind.java.

Z3_OP_FPA_IS_NAN =(2335)

Definition at line 155 of file Z3_decl_kind.java.

Z3_OP_FPA_IS_NEGATIVE =(2340)

Definition at line 150 of file Z3_decl_kind.java.

Z3_OP_FPA_IS_NORMAL =(2338)

Definition at line 57 of file Z3_decl_kind.java.

Z3_OP_FPA_IS_POSITIVE =(2341)

Definition at line 145 of file Z3_decl_kind.java.

Z3_OP_FPA_IS_SUBNORMAL =(2339)

Definition at line 33 of file Z3_decl_kind.java.

Z3_OP_FPA_IS_ZERO =(2337)

Definition at line 132 of file Z3_decl_kind.java.

Z3_OP_FPA_LE =(2333)

Definition at line 60 of file Z3_decl_kind.java.

Z3_OP_FPA_LT =(2331)

Definition at line 56 of file Z3_decl_kind.java.

Z3_OP_FPA_MAX =(2326)

Definition at line 108 of file Z3_decl_kind.java.

Z3_OP_FPA_MIN =(2325)

Definition at line 91 of file Z3_decl_kind.java.

Z3_OP_FPA_MINUS_INF =(2314)

Definition at line 122 of file Z3_decl_kind.java.

Z3_OP_FPA_MINUS_ZERO =(2317)

Definition at line 192 of file Z3_decl_kind.java.

Z3_OP_FPA_MUL =(2321)

Definition at line 187 of file Z3_decl_kind.java.

Z3_OP_FPA_NAN =(2315)

Definition at line 41 of file Z3_decl_kind.java.

Z3_OP_FPA_NEG =(2320)

Definition at line 78 of file Z3_decl_kind.java.

Z3_OP_FPA_NUM =(2312)

Definition at line 191 of file Z3_decl_kind.java.

Z3_OP_FPA_PLUS_INF =(2313)

Definition at line 206 of file Z3_decl_kind.java.

Z3_OP_FPA_PLUS_ZERO =(2316)

Definition at line 76 of file Z3_decl_kind.java.

Z3_OP_FPA_REM =(2323)

Definition at line 193 of file Z3_decl_kind.java.

Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY =(2308)

Definition at line 26 of file Z3_decl_kind.java.

Referenced by FPRMNum.isRNA(), and FPRMNum.isRoundNearestTiesToAway().

Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN =(2307)

Definition at line 174 of file Z3_decl_kind.java.

Referenced by FPRMNum.isRNE(), and FPRMNum.isRoundNearestTiesToEven().

Z3_OP_FPA_RM_TOWARD_NEGATIVE =(2310)

Definition at line 197 of file Z3_decl_kind.java.

Referenced by FPRMNum.isRoundTowardNegative(), and FPRMNum.isRTN().

Z3_OP_FPA_RM_TOWARD_POSITIVE =(2309)

Definition at line 54 of file Z3_decl_kind.java.

Referenced by FPRMNum.isRoundTowardPositive(), and FPRMNum.isRTP().

Z3_OP_FPA_RM_TOWARD_ZERO =(2311)

Definition at line 168 of file Z3_decl_kind.java.

Referenced by FPRMNum.isRoundTowardZero(), and FPRMNum.isRTZ().

Z3_OP_FPA_ROUND_TO_INTEGRAL =(2329)

Definition at line 70 of file Z3_decl_kind.java.

Z3_OP_FPA_SQRT =(2328)

Definition at line 164 of file Z3_decl_kind.java.

Z3_OP_FPA_SUB =(2319)

Definition at line 94 of file Z3_decl_kind.java.

Z3_OP_FPA_TO_FP =(2343)

Definition at line 195 of file Z3_decl_kind.java.

Z3_OP_FPA_TO_FP_UNSIGNED =(2344)

Definition at line 162 of file Z3_decl_kind.java.

Z3_OP_FPA_TO_IEEE_BV =(2348)

Definition at line 59 of file Z3_decl_kind.java.

Z3_OP_FPA_TO_REAL =(2347)

Definition at line 148 of file Z3_decl_kind.java.

Z3_OP_FPA_TO_SBV =(2346)

Definition at line 105 of file Z3_decl_kind.java.

Z3_OP_FPA_TO_UBV =(2345)

Definition at line 24 of file Z3_decl_kind.java.

Z3_OP_GE =(515)

Definition at line 140 of file Z3_decl_kind.java.

Referenced by Expr.isGE().

Z3_OP_GT =(517)

Definition at line 136 of file Z3_decl_kind.java.

Referenced by Expr.isGT().

Z3_OP_IDIV =(523)

Definition at line 52 of file Z3_decl_kind.java.

Referenced by Expr.isIDiv().

Z3_OP_IFF =(263)

Definition at line 67 of file Z3_decl_kind.java.

Referenced by Expr.isIff().

Z3_OP_IMPLIES =(266)

Definition at line 138 of file Z3_decl_kind.java.

Referenced by Expr.isImplies().

Z3_OP_INT2BV =(1071)

Definition at line 190 of file Z3_decl_kind.java.

Referenced by Expr.isIntToBV().

Z3_OP_INTERP =(268)

Definition at line 160 of file Z3_decl_kind.java.

Z3_OP_IS_INT =(528)

Definition at line 18 of file Z3_decl_kind.java.

Referenced by Expr.isRealIsInt().

Z3_OP_ITE =(260)

Definition at line 143 of file Z3_decl_kind.java.

Referenced by Expr.isITE().

Z3_OP_LABEL =(1792)

Definition at line 11 of file Z3_decl_kind.java.

Referenced by Expr.isLabel().

Z3_OP_LABEL_LIT =(1793)

Definition at line 58 of file Z3_decl_kind.java.

Referenced by Expr.isLabelLit().

Z3_OP_LE =(514)

Definition at line 27 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 106 of file Z3_decl_kind.java.

Referenced by Expr.isModulus().

Z3_OP_MUL =(521)

Definition at line 118 of file Z3_decl_kind.java.

Referenced by Expr.isMul().

Z3_OP_NOT =(265)

Definition at line 74 of file Z3_decl_kind.java.

Referenced by Expr.isNot().

Z3_OP_OEQ =(267)

Definition at line 36 of file Z3_decl_kind.java.

Referenced by Expr.isOEQ().

Z3_OP_OR =(262)

Definition at line 151 of file Z3_decl_kind.java.

Referenced by Expr.isOr().

Z3_OP_PB_AT_MOST =(2304)

Definition at line 92 of file Z3_decl_kind.java.

Z3_OP_PB_GE =(2306)

Definition at line 141 of file Z3_decl_kind.java.

Z3_OP_PB_LE =(2305)

Definition at line 165 of file Z3_decl_kind.java.

Z3_OP_POWER =(529)

Definition at line 178 of file Z3_decl_kind.java.

Z3_OP_PR_AND_ELIM =(1292)

Definition at line 104 of file Z3_decl_kind.java.

Referenced by Expr.isProofAndElimination().

Z3_OP_PR_APPLY_DEF =(1310)

Definition at line 50 of file Z3_decl_kind.java.

Referenced by Expr.isProofApplyDef().

Z3_OP_PR_ASSERTED =(1282)

Definition at line 130 of file Z3_decl_kind.java.

Referenced by Expr.isProofAsserted().

Z3_OP_PR_CNF_STAR =(1315)

Definition at line 23 of file Z3_decl_kind.java.

Referenced by Expr.isProofCNFStar().

Z3_OP_PR_COMMUTATIVITY =(1307)

Definition at line 185 of file Z3_decl_kind.java.

Referenced by Expr.isProofCommutativity().

Z3_OP_PR_DEF_AXIOM =(1308)

Definition at line 201 of file Z3_decl_kind.java.

Referenced by Expr.isProofDefAxiom().

Z3_OP_PR_DEF_INTRO =(1309)

Definition at line 73 of file Z3_decl_kind.java.

Referenced by Expr.isProofDefIntro().

Z3_OP_PR_DER =(1300)

Definition at line 134 of file Z3_decl_kind.java.

Referenced by Expr.isProofDER().

Z3_OP_PR_DISTRIBUTIVITY =(1291)

Definition at line 204 of file Z3_decl_kind.java.

Referenced by Expr.isProofDistributivity().

Z3_OP_PR_ELIM_UNUSED_VARS =(1299)

Definition at line 111 of file Z3_decl_kind.java.

Referenced by Expr.isProofElimUnusedVars().

Z3_OP_PR_GOAL =(1283)

Definition at line 53 of file Z3_decl_kind.java.

Referenced by Expr.isProofGoal().

Z3_OP_PR_HYPER_RESOLVE =(1319)

Definition at line 153 of file Z3_decl_kind.java.

Z3_OP_PR_HYPOTHESIS =(1302)

Definition at line 98 of file Z3_decl_kind.java.

Referenced by Expr.isProofHypothesis().

Z3_OP_PR_IFF_FALSE =(1306)

Definition at line 125 of file Z3_decl_kind.java.

Referenced by Expr.isProofIFFFalse().

Z3_OP_PR_IFF_OEQ =(1311)

Definition at line 159 of file Z3_decl_kind.java.

Referenced by Expr.isProofIFFOEQ().

Z3_OP_PR_IFF_TRUE =(1305)

Definition at line 55 of file Z3_decl_kind.java.

Referenced by Expr.isProofIFFTrue().

Z3_OP_PR_LEMMA =(1303)

Definition at line 161 of file Z3_decl_kind.java.

Referenced by Expr.isProofLemma().

Z3_OP_PR_MODUS_PONENS =(1284)

Definition at line 37 of file Z3_decl_kind.java.

Referenced by Expr.isProofModusPonens().

Z3_OP_PR_MODUS_PONENS_OEQ =(1317)

Definition at line 196 of file Z3_decl_kind.java.

Referenced by Expr.isProofModusPonensOEQ().

Z3_OP_PR_MONOTONICITY =(1289)

Definition at line 200 of file Z3_decl_kind.java.

Referenced by Expr.isProofMonotonicity().

Z3_OP_PR_NNF_NEG =(1313)

Definition at line 85 of file Z3_decl_kind.java.

Referenced by Expr.isProofNNFNeg().

Z3_OP_PR_NNF_POS =(1312)

Definition at line 103 of file Z3_decl_kind.java.

Referenced by Expr.isProofNNFPos().

Z3_OP_PR_NNF_STAR =(1314)

Definition at line 184 of file Z3_decl_kind.java.

Referenced by Expr.isProofNNFStar().

Z3_OP_PR_NOT_OR_ELIM =(1293)

Definition at line 66 of file Z3_decl_kind.java.

Referenced by Expr.isProofOrElimination().

Z3_OP_PR_PULL_QUANT =(1296)

Definition at line 49 of file Z3_decl_kind.java.

Referenced by Expr.isProofPullQuant().

Z3_OP_PR_PULL_QUANT_STAR =(1297)

Definition at line 128 of file Z3_decl_kind.java.

Referenced by Expr.isProofPullQuantStar().

Z3_OP_PR_PUSH_QUANT =(1298)

Definition at line 156 of file Z3_decl_kind.java.

Referenced by Expr.isProofPushQuant().

Z3_OP_PR_QUANT_INST =(1301)

Definition at line 176 of file Z3_decl_kind.java.

Referenced by Expr.isProofQuantInst().

Z3_OP_PR_QUANT_INTRO =(1290)

Definition at line 75 of file Z3_decl_kind.java.

Referenced by Expr.isProofQuantIntro().

Z3_OP_PR_REFLEXIVITY =(1285)

Definition at line 87 of file Z3_decl_kind.java.

Referenced by Expr.isProofReflexivity().

Z3_OP_PR_REWRITE =(1294)

Definition at line 12 of file Z3_decl_kind.java.

Referenced by Expr.isProofRewrite().

Z3_OP_PR_REWRITE_STAR =(1295)

Definition at line 51 of file Z3_decl_kind.java.

Referenced by Expr.isProofRewriteStar().

Z3_OP_PR_SKOLEMIZE =(1316)

Definition at line 207 of file Z3_decl_kind.java.

Referenced by Expr.isProofSkolemize().

Z3_OP_PR_SYMMETRY =(1286)

Definition at line 62 of file Z3_decl_kind.java.

Referenced by Expr.isProofSymmetry().

Z3_OP_PR_TH_LEMMA =(1318)

Definition at line 121 of file Z3_decl_kind.java.

Referenced by Expr.isProofTheoryLemma().

Z3_OP_PR_TRANSITIVITY =(1287)

Definition at line 69 of file Z3_decl_kind.java.

Referenced by Expr.isProofTransitivity().

Z3_OP_PR_TRANSITIVITY_STAR =(1288)

Definition at line 183 of file Z3_decl_kind.java.

Referenced by Expr.isProofTransitivityStar().

Z3_OP_PR_TRUE =(1281)

Definition at line 109 of file Z3_decl_kind.java.

Referenced by Expr.isProofTrue().

Z3_OP_PR_UNDEF =(1280)

Definition at line 29 of file Z3_decl_kind.java.

Z3_OP_PR_UNIT_RESOLUTION =(1304)

Definition at line 46 of file Z3_decl_kind.java.

Referenced by Expr.isProofUnitResolution().

Z3_OP_RA_CLONE =(1548)

Definition at line 38 of file Z3_decl_kind.java.

Referenced by Expr.isRelationClone().

Z3_OP_RA_COMPLEMENT =(1546)

Definition at line 209 of file Z3_decl_kind.java.

Referenced by Expr.isRelationComplement().

Z3_OP_RA_EMPTY =(1537)

Definition at line 115 of file Z3_decl_kind.java.

Referenced by Expr.isEmptyRelation().

Z3_OP_RA_FILTER =(1543)

Definition at line 112 of file Z3_decl_kind.java.

Referenced by Expr.isRelationFilter().

Z3_OP_RA_IS_EMPTY =(1538)

Definition at line 180 of file Z3_decl_kind.java.

Referenced by Expr.isIsEmptyRelation().

Z3_OP_RA_JOIN =(1539)

Definition at line 25 of file Z3_decl_kind.java.

Referenced by Expr.isRelationalJoin().

Z3_OP_RA_NEGATION_FILTER =(1544)

Definition at line 40 of file Z3_decl_kind.java.

Referenced by Expr.isRelationNegationFilter().

Z3_OP_RA_PROJECT =(1542)

Definition at line 170 of file Z3_decl_kind.java.

Referenced by Expr.isRelationProject().

Z3_OP_RA_RENAME =(1545)

Definition at line 99 of file Z3_decl_kind.java.

Referenced by Expr.isRelationRename().

Z3_OP_RA_SELECT =(1547)

Definition at line 146 of file Z3_decl_kind.java.

Referenced by Expr.isRelationSelect().

Z3_OP_RA_STORE =(1536)

Definition at line 82 of file Z3_decl_kind.java.

Referenced by Expr.isRelationStore().

Z3_OP_RA_UNION =(1540)

Definition at line 32 of file Z3_decl_kind.java.

Referenced by Expr.isRelationUnion().

Z3_OP_RA_WIDEN =(1541)

Definition at line 72 of file Z3_decl_kind.java.

Referenced by Expr.isRelationWiden().

Z3_OP_REM =(524)

Definition at line 173 of file Z3_decl_kind.java.

Referenced by Expr.isRemainder().

Z3_OP_REPEAT =(1060)

Definition at line 39 of file Z3_decl_kind.java.

Referenced by Expr.isBVRepeat().

Z3_OP_ROTATE_LEFT =(1067)

Definition at line 84 of file Z3_decl_kind.java.

Referenced by Expr.isBVRotateLeft().

Z3_OP_ROTATE_RIGHT =(1068)

Definition at line 47 of file Z3_decl_kind.java.

Referenced by Expr.isBVRotateRight().

Z3_OP_SELECT =(769)

Definition at line 169 of file Z3_decl_kind.java.

Referenced by Expr.isSelect().

Z3_OP_SET_COMPLEMENT =(776)

Definition at line 64 of file Z3_decl_kind.java.

Referenced by Expr.isSetComplement().

Z3_OP_SET_DIFFERENCE =(775)

Definition at line 189 of file Z3_decl_kind.java.

Referenced by Expr.isSetDifference().

Z3_OP_SET_INTERSECT =(774)

Definition at line 80 of file Z3_decl_kind.java.

Referenced by Expr.isSetIntersect().

Z3_OP_SET_SUBSET =(777)

Definition at line 163 of file Z3_decl_kind.java.

Referenced by Expr.isSetSubset().

Z3_OP_SET_UNION =(773)

Definition at line 28 of file Z3_decl_kind.java.

Referenced by Expr.isSetUnion().

Z3_OP_SGEQ =(1044)

Definition at line 177 of file Z3_decl_kind.java.

Referenced by Expr.isBVSGE().

Z3_OP_SGT =(1048)

Definition at line 71 of file Z3_decl_kind.java.

Referenced by Expr.isBVSGT().

Z3_OP_SIGN_EXT =(1057)

Definition at line 205 of file Z3_decl_kind.java.

Referenced by Expr.isBVSignExtension().

Z3_OP_SLEQ =(1042)

Definition at line 139 of file Z3_decl_kind.java.

Referenced by Expr.isBVSLE().

Z3_OP_SLT =(1046)

Definition at line 83 of file Z3_decl_kind.java.

Referenced by Expr.isBVSLT().

Z3_OP_STORE =(768)

Definition at line 97 of file Z3_decl_kind.java.

Referenced by Expr.isStore().

Z3_OP_SUB =(519)

Definition at line 14 of file Z3_decl_kind.java.

Referenced by Expr.isSub().

Z3_OP_TO_INT =(527)

Definition at line 175 of file Z3_decl_kind.java.

Referenced by Expr.isRealToInt().

Z3_OP_TO_REAL =(526)

Definition at line 101 of file Z3_decl_kind.java.

Referenced by Expr.isIntToReal().

Z3_OP_TRUE =(256)

Definition at line 63 of file Z3_decl_kind.java.

Referenced by Expr.isTrue().

Z3_OP_UGEQ =(1043)

Definition at line 119 of file Z3_decl_kind.java.

Referenced by Expr.isBVUGE().

Z3_OP_UGT =(1047)

Definition at line 77 of file Z3_decl_kind.java.

Referenced by Expr.isBVUGT().

Z3_OP_ULEQ =(1041)

Definition at line 88 of file Z3_decl_kind.java.

Referenced by Expr.isBVULE().

Z3_OP_ULT =(1045)

Definition at line 186 of file Z3_decl_kind.java.

Referenced by Expr.isBVULT().

Z3_OP_UMINUS =(520)

Definition at line 172 of file Z3_decl_kind.java.

Referenced by Expr.isUMinus().

Z3_OP_UNINTERPRETED =(2349)

Definition at line 13 of file Z3_decl_kind.java.

Z3_OP_XOR =(264)

Definition at line 194 of file Z3_decl_kind.java.

Referenced by Expr.isXor().

Z3_OP_XOR3 =(1074)

Definition at line 179 of file Z3_decl_kind.java.

Referenced by Expr.isBVXOR3().

Z3_OP_ZERO_EXT =(1058)

Definition at line 15 of file Z3_decl_kind.java.

Referenced by Expr.isBVZeroExtension().