Z3
Data Structures | 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_TRUE =(256)
 
 Z3_OP_FALSE =(257)
 
 Z3_OP_EQ =(258)
 
 Z3_OP_DISTINCT =(259)
 
 Z3_OP_ITE =(260)
 
 Z3_OP_AND =(261)
 
 Z3_OP_OR =(262)
 
 Z3_OP_IFF =(263)
 
 Z3_OP_XOR =(264)
 
 Z3_OP_NOT =(265)
 
 Z3_OP_IMPLIES =(266)
 
 Z3_OP_OEQ =(267)
 
 Z3_OP_ANUM =(512)
 
 Z3_OP_AGNUM =(513)
 
 Z3_OP_LE =(514)
 
 Z3_OP_GE =(515)
 
 Z3_OP_LT =(516)
 
 Z3_OP_GT =(517)
 
 Z3_OP_ADD =(518)
 
 Z3_OP_SUB =(519)
 
 Z3_OP_UMINUS =(520)
 
 Z3_OP_MUL =(521)
 
 Z3_OP_DIV =(522)
 
 Z3_OP_IDIV =(523)
 
 Z3_OP_REM =(524)
 
 Z3_OP_MOD =(525)
 
 Z3_OP_TO_REAL =(526)
 
 Z3_OP_TO_INT =(527)
 
 Z3_OP_IS_INT =(528)
 
 Z3_OP_POWER =(529)
 
 Z3_OP_STORE =(768)
 
 Z3_OP_SELECT =(769)
 
 Z3_OP_CONST_ARRAY =(770)
 
 Z3_OP_ARRAY_MAP =(771)
 
 Z3_OP_ARRAY_DEFAULT =(772)
 
 Z3_OP_SET_UNION =(773)
 
 Z3_OP_SET_INTERSECT =(774)
 
 Z3_OP_SET_DIFFERENCE =(775)
 
 Z3_OP_SET_COMPLEMENT =(776)
 
 Z3_OP_SET_SUBSET =(777)
 
 Z3_OP_AS_ARRAY =(778)
 
 Z3_OP_ARRAY_EXT =(779)
 
 Z3_OP_SET_HAS_SIZE =(780)
 
 Z3_OP_SET_CARD =(781)
 
 Z3_OP_BNUM =(1024)
 
 Z3_OP_BIT1 =(1025)
 
 Z3_OP_BIT0 =(1026)
 
 Z3_OP_BNEG =(1027)
 
 Z3_OP_BADD =(1028)
 
 Z3_OP_BSUB =(1029)
 
 Z3_OP_BMUL =(1030)
 
 Z3_OP_BSDIV =(1031)
 
 Z3_OP_BUDIV =(1032)
 
 Z3_OP_BSREM =(1033)
 
 Z3_OP_BUREM =(1034)
 
 Z3_OP_BSMOD =(1035)
 
 Z3_OP_BSDIV0 =(1036)
 
 Z3_OP_BUDIV0 =(1037)
 
 Z3_OP_BSREM0 =(1038)
 
 Z3_OP_BUREM0 =(1039)
 
 Z3_OP_BSMOD0 =(1040)
 
 Z3_OP_ULEQ =(1041)
 
 Z3_OP_SLEQ =(1042)
 
 Z3_OP_UGEQ =(1043)
 
 Z3_OP_SGEQ =(1044)
 
 Z3_OP_ULT =(1045)
 
 Z3_OP_SLT =(1046)
 
 Z3_OP_UGT =(1047)
 
 Z3_OP_SGT =(1048)
 
 Z3_OP_BAND =(1049)
 
 Z3_OP_BOR =(1050)
 
 Z3_OP_BNOT =(1051)
 
 Z3_OP_BXOR =(1052)
 
 Z3_OP_BNAND =(1053)
 
 Z3_OP_BNOR =(1054)
 
 Z3_OP_BXNOR =(1055)
 
 Z3_OP_CONCAT =(1056)
 
 Z3_OP_SIGN_EXT =(1057)
 
 Z3_OP_ZERO_EXT =(1058)
 
 Z3_OP_EXTRACT =(1059)
 
 Z3_OP_REPEAT =(1060)
 
 Z3_OP_BREDOR =(1061)
 
 Z3_OP_BREDAND =(1062)
 
 Z3_OP_BCOMP =(1063)
 
 Z3_OP_BSHL =(1064)
 
 Z3_OP_BLSHR =(1065)
 
 Z3_OP_BASHR =(1066)
 
 Z3_OP_ROTATE_LEFT =(1067)
 
 Z3_OP_ROTATE_RIGHT =(1068)
 
 Z3_OP_EXT_ROTATE_LEFT =(1069)
 
 Z3_OP_EXT_ROTATE_RIGHT =(1070)
 
 Z3_OP_BIT2BOOL =(1071)
 
 Z3_OP_INT2BV =(1072)
 
 Z3_OP_BV2INT =(1073)
 
 Z3_OP_CARRY =(1074)
 
 Z3_OP_XOR3 =(1075)
 
 Z3_OP_BSMUL_NO_OVFL =(1076)
 
 Z3_OP_BUMUL_NO_OVFL =(1077)
 
 Z3_OP_BSMUL_NO_UDFL =(1078)
 
 Z3_OP_BSDIV_I =(1079)
 
 Z3_OP_BUDIV_I =(1080)
 
 Z3_OP_BSREM_I =(1081)
 
 Z3_OP_BUREM_I =(1082)
 
 Z3_OP_BSMOD_I =(1083)
 
 Z3_OP_PR_UNDEF =(1280)
 
 Z3_OP_PR_TRUE =(1281)
 
 Z3_OP_PR_ASSERTED =(1282)
 
 Z3_OP_PR_GOAL =(1283)
 
 Z3_OP_PR_MODUS_PONENS =(1284)
 
 Z3_OP_PR_REFLEXIVITY =(1285)
 
 Z3_OP_PR_SYMMETRY =(1286)
 
 Z3_OP_PR_TRANSITIVITY =(1287)
 
 Z3_OP_PR_TRANSITIVITY_STAR =(1288)
 
 Z3_OP_PR_MONOTONICITY =(1289)
 
 Z3_OP_PR_QUANT_INTRO =(1290)
 
 Z3_OP_PR_BIND =(1291)
 
 Z3_OP_PR_DISTRIBUTIVITY =(1292)
 
 Z3_OP_PR_AND_ELIM =(1293)
 
 Z3_OP_PR_NOT_OR_ELIM =(1294)
 
 Z3_OP_PR_REWRITE =(1295)
 
 Z3_OP_PR_REWRITE_STAR =(1296)
 
 Z3_OP_PR_PULL_QUANT =(1297)
 
 Z3_OP_PR_PUSH_QUANT =(1298)
 
 Z3_OP_PR_ELIM_UNUSED_VARS =(1299)
 
 Z3_OP_PR_DER =(1300)
 
 Z3_OP_PR_QUANT_INST =(1301)
 
 Z3_OP_PR_HYPOTHESIS =(1302)
 
 Z3_OP_PR_LEMMA =(1303)
 
 Z3_OP_PR_UNIT_RESOLUTION =(1304)
 
 Z3_OP_PR_IFF_TRUE =(1305)
 
 Z3_OP_PR_IFF_FALSE =(1306)
 
 Z3_OP_PR_COMMUTATIVITY =(1307)
 
 Z3_OP_PR_DEF_AXIOM =(1308)
 
 Z3_OP_PR_ASSUMPTION_ADD =(1309)
 
 Z3_OP_PR_LEMMA_ADD =(1310)
 
 Z3_OP_PR_REDUNDANT_DEL =(1311)
 
 Z3_OP_PR_CLAUSE_TRAIL =(1312)
 
 Z3_OP_PR_DEF_INTRO =(1313)
 
 Z3_OP_PR_APPLY_DEF =(1314)
 
 Z3_OP_PR_IFF_OEQ =(1315)
 
 Z3_OP_PR_NNF_POS =(1316)
 
 Z3_OP_PR_NNF_NEG =(1317)
 
 Z3_OP_PR_SKOLEMIZE =(1318)
 
 Z3_OP_PR_MODUS_PONENS_OEQ =(1319)
 
 Z3_OP_PR_TH_LEMMA =(1320)
 
 Z3_OP_PR_HYPER_RESOLVE =(1321)
 
 Z3_OP_RA_STORE =(1536)
 
 Z3_OP_RA_EMPTY =(1537)
 
 Z3_OP_RA_IS_EMPTY =(1538)
 
 Z3_OP_RA_JOIN =(1539)
 
 Z3_OP_RA_UNION =(1540)
 
 Z3_OP_RA_WIDEN =(1541)
 
 Z3_OP_RA_PROJECT =(1542)
 
 Z3_OP_RA_FILTER =(1543)
 
 Z3_OP_RA_NEGATION_FILTER =(1544)
 
 Z3_OP_RA_RENAME =(1545)
 
 Z3_OP_RA_COMPLEMENT =(1546)
 
 Z3_OP_RA_SELECT =(1547)
 
 Z3_OP_RA_CLONE =(1548)
 
 Z3_OP_FD_CONSTANT =(1549)
 
 Z3_OP_FD_LT =(1550)
 
 Z3_OP_SEQ_UNIT =(1551)
 
 Z3_OP_SEQ_EMPTY =(1552)
 
 Z3_OP_SEQ_CONCAT =(1553)
 
 Z3_OP_SEQ_PREFIX =(1554)
 
 Z3_OP_SEQ_SUFFIX =(1555)
 
 Z3_OP_SEQ_CONTAINS =(1556)
 
 Z3_OP_SEQ_EXTRACT =(1557)
 
 Z3_OP_SEQ_REPLACE =(1558)
 
 Z3_OP_SEQ_AT =(1559)
 
 Z3_OP_SEQ_NTH =(1560)
 
 Z3_OP_SEQ_LENGTH =(1561)
 
 Z3_OP_SEQ_INDEX =(1562)
 
 Z3_OP_SEQ_LAST_INDEX =(1563)
 
 Z3_OP_SEQ_TO_RE =(1564)
 
 Z3_OP_SEQ_IN_RE =(1565)
 
 Z3_OP_STR_TO_INT =(1566)
 
 Z3_OP_INT_TO_STR =(1567)
 
 Z3_OP_RE_PLUS =(1568)
 
 Z3_OP_RE_STAR =(1569)
 
 Z3_OP_RE_OPTION =(1570)
 
 Z3_OP_RE_CONCAT =(1571)
 
 Z3_OP_RE_UNION =(1572)
 
 Z3_OP_RE_RANGE =(1573)
 
 Z3_OP_RE_LOOP =(1574)
 
 Z3_OP_RE_INTERSECT =(1575)
 
 Z3_OP_RE_EMPTY_SET =(1576)
 
 Z3_OP_RE_FULL_SET =(1577)
 
 Z3_OP_RE_COMPLEMENT =(1578)
 
 Z3_OP_LABEL =(1792)
 
 Z3_OP_LABEL_LIT =(1793)
 
 Z3_OP_DT_CONSTRUCTOR =(2048)
 
 Z3_OP_DT_RECOGNISER =(2049)
 
 Z3_OP_DT_IS =(2050)
 
 Z3_OP_DT_ACCESSOR =(2051)
 
 Z3_OP_DT_UPDATE_FIELD =(2052)
 
 Z3_OP_PB_AT_MOST =(2304)
 
 Z3_OP_PB_AT_LEAST =(2305)
 
 Z3_OP_PB_LE =(2306)
 
 Z3_OP_PB_GE =(2307)
 
 Z3_OP_PB_EQ =(2308)
 
 Z3_OP_SPECIAL_RELATION_LO =(40960)
 
 Z3_OP_SPECIAL_RELATION_PO =(40961)
 
 Z3_OP_SPECIAL_RELATION_PLO =(40962)
 
 Z3_OP_SPECIAL_RELATION_TO =(40963)
 
 Z3_OP_SPECIAL_RELATION_TC =(40964)
 
 Z3_OP_SPECIAL_RELATION_TRC =(40965)
 
 Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN =(45056)
 
 Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY =(45057)
 
 Z3_OP_FPA_RM_TOWARD_POSITIVE =(45058)
 
 Z3_OP_FPA_RM_TOWARD_NEGATIVE =(45059)
 
 Z3_OP_FPA_RM_TOWARD_ZERO =(45060)
 
 Z3_OP_FPA_NUM =(45061)
 
 Z3_OP_FPA_PLUS_INF =(45062)
 
 Z3_OP_FPA_MINUS_INF =(45063)
 
 Z3_OP_FPA_NAN =(45064)
 
 Z3_OP_FPA_PLUS_ZERO =(45065)
 
 Z3_OP_FPA_MINUS_ZERO =(45066)
 
 Z3_OP_FPA_ADD =(45067)
 
 Z3_OP_FPA_SUB =(45068)
 
 Z3_OP_FPA_NEG =(45069)
 
 Z3_OP_FPA_MUL =(45070)
 
 Z3_OP_FPA_DIV =(45071)
 
 Z3_OP_FPA_REM =(45072)
 
 Z3_OP_FPA_ABS =(45073)
 
 Z3_OP_FPA_MIN =(45074)
 
 Z3_OP_FPA_MAX =(45075)
 
 Z3_OP_FPA_FMA =(45076)
 
 Z3_OP_FPA_SQRT =(45077)
 
 Z3_OP_FPA_ROUND_TO_INTEGRAL =(45078)
 
 Z3_OP_FPA_EQ =(45079)
 
 Z3_OP_FPA_LT =(45080)
 
 Z3_OP_FPA_GT =(45081)
 
 Z3_OP_FPA_LE =(45082)
 
 Z3_OP_FPA_GE =(45083)
 
 Z3_OP_FPA_IS_NAN =(45084)
 
 Z3_OP_FPA_IS_INF =(45085)
 
 Z3_OP_FPA_IS_ZERO =(45086)
 
 Z3_OP_FPA_IS_NORMAL =(45087)
 
 Z3_OP_FPA_IS_SUBNORMAL =(45088)
 
 Z3_OP_FPA_IS_NEGATIVE =(45089)
 
 Z3_OP_FPA_IS_POSITIVE =(45090)
 
 Z3_OP_FPA_FP =(45091)
 
 Z3_OP_FPA_TO_FP =(45092)
 
 Z3_OP_FPA_TO_FP_UNSIGNED =(45093)
 
 Z3_OP_FPA_TO_UBV =(45094)
 
 Z3_OP_FPA_TO_SBV =(45095)
 
 Z3_OP_FPA_TO_REAL =(45096)
 
 Z3_OP_FPA_TO_IEEE_BV =(45097)
 
 Z3_OP_FPA_BVWRAP =(45098)
 
 Z3_OP_FPA_BV2RM =(45099)
 
 Z3_OP_INTERNAL =(45100)
 
 Z3_OP_UNINTERPRETED =(45101)
 

Detailed Description

Z3_decl_kind

Definition at line 13 of file Z3_decl_kind.java.

Constructor & Destructor Documentation

◆ Z3_decl_kind()

Z3_decl_kind ( int  v)
inline

Definition at line 270 of file Z3_decl_kind.java.

270  {
271  this.intValue = v;
272  }

Member Function Documentation

◆ fromInt()

static final Z3_decl_kind fromInt ( int  v)
inlinestatic

Definition at line 284 of file Z3_decl_kind.java.

284  {
285  Z3_decl_kind k = Z3_decl_kind_MappingHolder.intMapping.get(v);
286  if (k != null) return k;
287  throw new IllegalArgumentException("Illegal value " + v + " for Z3_decl_kind");
288  }

Referenced by FuncDecl.getDeclKind().

◆ toInt()

final int toInt ( )
inline

Definition at line 290 of file Z3_decl_kind.java.

290 { return this.intValue; }

Field Documentation

◆ Z3_OP_ADD

Z3_OP_ADD =(518)

Definition at line 32 of file Z3_decl_kind.java.

Referenced by Expr.isAdd().

◆ Z3_OP_AGNUM

Z3_OP_AGNUM =(513)

Definition at line 27 of file Z3_decl_kind.java.

◆ Z3_OP_AND

Z3_OP_AND =(261)

Definition at line 19 of file Z3_decl_kind.java.

Referenced by Expr.isAnd().

◆ Z3_OP_ANUM

Z3_OP_ANUM =(512)

Definition at line 26 of file Z3_decl_kind.java.

Referenced by Expr.isArithmeticNumeral().

◆ Z3_OP_ARRAY_DEFAULT

Z3_OP_ARRAY_DEFAULT =(772)

Definition at line 48 of file Z3_decl_kind.java.

Referenced by Expr.isDefaultArray().

◆ Z3_OP_ARRAY_EXT

Z3_OP_ARRAY_EXT =(779)

Definition at line 55 of file Z3_decl_kind.java.

◆ Z3_OP_ARRAY_MAP

Z3_OP_ARRAY_MAP =(771)

Definition at line 47 of file Z3_decl_kind.java.

Referenced by Expr.isArrayMap().

◆ Z3_OP_AS_ARRAY

Z3_OP_AS_ARRAY =(778)

Definition at line 54 of file Z3_decl_kind.java.

Referenced by Expr.isAsArray().

◆ Z3_OP_BADD

Z3_OP_BADD =(1028)

Definition at line 62 of file Z3_decl_kind.java.

Referenced by Expr.isBVAdd().

◆ Z3_OP_BAND

Z3_OP_BAND =(1049)

Definition at line 83 of file Z3_decl_kind.java.

Referenced by Expr.isBVAND().

◆ Z3_OP_BASHR

Z3_OP_BASHR =(1066)

Definition at line 100 of file Z3_decl_kind.java.

Referenced by Expr.isBVShiftRightArithmetic().

◆ Z3_OP_BCOMP

Z3_OP_BCOMP =(1063)

Definition at line 97 of file Z3_decl_kind.java.

Referenced by Expr.isBVComp().

◆ Z3_OP_BIT0

Z3_OP_BIT0 =(1026)

Definition at line 60 of file Z3_decl_kind.java.

Referenced by Expr.isBVBitZero().

◆ Z3_OP_BIT1

Z3_OP_BIT1 =(1025)

Definition at line 59 of file Z3_decl_kind.java.

Referenced by Expr.isBVBitOne().

◆ Z3_OP_BIT2BOOL

Z3_OP_BIT2BOOL =(1071)

Definition at line 105 of file Z3_decl_kind.java.

◆ Z3_OP_BLSHR

Z3_OP_BLSHR =(1065)

Definition at line 99 of file Z3_decl_kind.java.

Referenced by Expr.isBVShiftRightLogical().

◆ Z3_OP_BMUL

Z3_OP_BMUL =(1030)

Definition at line 64 of file Z3_decl_kind.java.

Referenced by Expr.isBVMul().

◆ Z3_OP_BNAND

Z3_OP_BNAND =(1053)

Definition at line 87 of file Z3_decl_kind.java.

Referenced by Expr.isBVNAND().

◆ Z3_OP_BNEG

Z3_OP_BNEG =(1027)

Definition at line 61 of file Z3_decl_kind.java.

Referenced by Expr.isBVUMinus().

◆ Z3_OP_BNOR

Z3_OP_BNOR =(1054)

Definition at line 88 of file Z3_decl_kind.java.

Referenced by Expr.isBVNOR().

◆ Z3_OP_BNOT

Z3_OP_BNOT =(1051)

Definition at line 85 of file Z3_decl_kind.java.

Referenced by Expr.isBVNOT().

◆ Z3_OP_BNUM

Z3_OP_BNUM =(1024)

Definition at line 58 of file Z3_decl_kind.java.

Referenced by Expr.isBVNumeral().

◆ Z3_OP_BOR

Z3_OP_BOR =(1050)

Definition at line 84 of file Z3_decl_kind.java.

Referenced by Expr.isBVOR().

◆ Z3_OP_BREDAND

Z3_OP_BREDAND =(1062)

Definition at line 96 of file Z3_decl_kind.java.

Referenced by Expr.isBVReduceAND().

◆ Z3_OP_BREDOR

Z3_OP_BREDOR =(1061)

Definition at line 95 of file Z3_decl_kind.java.

Referenced by Expr.isBVReduceOR().

◆ Z3_OP_BSDIV

Z3_OP_BSDIV =(1031)

Definition at line 65 of file Z3_decl_kind.java.

Referenced by Expr.isBVSDiv().

◆ Z3_OP_BSDIV0

Z3_OP_BSDIV0 =(1036)

Definition at line 70 of file Z3_decl_kind.java.

◆ Z3_OP_BSDIV_I

Z3_OP_BSDIV_I =(1079)

Definition at line 113 of file Z3_decl_kind.java.

◆ Z3_OP_BSHL

Z3_OP_BSHL =(1064)

Definition at line 98 of file Z3_decl_kind.java.

Referenced by Expr.isBVShiftLeft().

◆ Z3_OP_BSMOD

Z3_OP_BSMOD =(1035)

Definition at line 69 of file Z3_decl_kind.java.

Referenced by Expr.isBVSMod().

◆ Z3_OP_BSMOD0

Z3_OP_BSMOD0 =(1040)

Definition at line 74 of file Z3_decl_kind.java.

◆ Z3_OP_BSMOD_I

Z3_OP_BSMOD_I =(1083)

Definition at line 117 of file Z3_decl_kind.java.

◆ Z3_OP_BSMUL_NO_OVFL

Z3_OP_BSMUL_NO_OVFL =(1076)

Definition at line 110 of file Z3_decl_kind.java.

◆ Z3_OP_BSMUL_NO_UDFL

Z3_OP_BSMUL_NO_UDFL =(1078)

Definition at line 112 of file Z3_decl_kind.java.

◆ Z3_OP_BSREM

Z3_OP_BSREM =(1033)

Definition at line 67 of file Z3_decl_kind.java.

Referenced by Expr.isBVSRem().

◆ Z3_OP_BSREM0

Z3_OP_BSREM0 =(1038)

Definition at line 72 of file Z3_decl_kind.java.

◆ Z3_OP_BSREM_I

Z3_OP_BSREM_I =(1081)

Definition at line 115 of file Z3_decl_kind.java.

◆ Z3_OP_BSUB

Z3_OP_BSUB =(1029)

Definition at line 63 of file Z3_decl_kind.java.

Referenced by Expr.isBVSub().

◆ Z3_OP_BUDIV

Z3_OP_BUDIV =(1032)

Definition at line 66 of file Z3_decl_kind.java.

Referenced by Expr.isBVUDiv().

◆ Z3_OP_BUDIV0

Z3_OP_BUDIV0 =(1037)

Definition at line 71 of file Z3_decl_kind.java.

◆ Z3_OP_BUDIV_I

Z3_OP_BUDIV_I =(1080)

Definition at line 114 of file Z3_decl_kind.java.

◆ Z3_OP_BUMUL_NO_OVFL

Z3_OP_BUMUL_NO_OVFL =(1077)

Definition at line 111 of file Z3_decl_kind.java.

◆ Z3_OP_BUREM

Z3_OP_BUREM =(1034)

Definition at line 68 of file Z3_decl_kind.java.

Referenced by Expr.isBVURem().

◆ Z3_OP_BUREM0

Z3_OP_BUREM0 =(1039)

Definition at line 73 of file Z3_decl_kind.java.

◆ Z3_OP_BUREM_I

Z3_OP_BUREM_I =(1082)

Definition at line 116 of file Z3_decl_kind.java.

◆ Z3_OP_BV2INT

Z3_OP_BV2INT =(1073)

Definition at line 107 of file Z3_decl_kind.java.

Referenced by Expr.isBVToInt().

◆ Z3_OP_BXNOR

Z3_OP_BXNOR =(1055)

Definition at line 89 of file Z3_decl_kind.java.

Referenced by Expr.isBVXNOR().

◆ Z3_OP_BXOR

Z3_OP_BXOR =(1052)

Definition at line 86 of file Z3_decl_kind.java.

Referenced by Expr.isBVXOR().

◆ Z3_OP_CARRY

Z3_OP_CARRY =(1074)

Definition at line 108 of file Z3_decl_kind.java.

Referenced by Expr.isBVCarry().

◆ Z3_OP_CONCAT

Z3_OP_CONCAT =(1056)

Definition at line 90 of file Z3_decl_kind.java.

Referenced by Expr.isBVConcat().

◆ Z3_OP_CONST_ARRAY

Z3_OP_CONST_ARRAY =(770)

Definition at line 46 of file Z3_decl_kind.java.

Referenced by Expr.isConstantArray().

◆ Z3_OP_DISTINCT

Z3_OP_DISTINCT =(259)

Definition at line 17 of file Z3_decl_kind.java.

Referenced by Expr.isDistinct().

◆ Z3_OP_DIV

Z3_OP_DIV =(522)

Definition at line 36 of file Z3_decl_kind.java.

Referenced by Expr.isDiv().

◆ Z3_OP_DT_ACCESSOR

Z3_OP_DT_ACCESSOR =(2051)

Definition at line 208 of file Z3_decl_kind.java.

◆ Z3_OP_DT_CONSTRUCTOR

Z3_OP_DT_CONSTRUCTOR =(2048)

Definition at line 205 of file Z3_decl_kind.java.

◆ Z3_OP_DT_IS

Z3_OP_DT_IS =(2050)

Definition at line 207 of file Z3_decl_kind.java.

◆ Z3_OP_DT_RECOGNISER

Z3_OP_DT_RECOGNISER =(2049)

Definition at line 206 of file Z3_decl_kind.java.

◆ Z3_OP_DT_UPDATE_FIELD

Z3_OP_DT_UPDATE_FIELD =(2052)

Definition at line 209 of file Z3_decl_kind.java.

◆ Z3_OP_EQ

Z3_OP_EQ =(258)

Definition at line 16 of file Z3_decl_kind.java.

Referenced by Expr.isEq().

◆ Z3_OP_EXT_ROTATE_LEFT

Z3_OP_EXT_ROTATE_LEFT =(1069)

Definition at line 103 of file Z3_decl_kind.java.

Referenced by Expr.isBVRotateLeftExtended().

◆ Z3_OP_EXT_ROTATE_RIGHT

Z3_OP_EXT_ROTATE_RIGHT =(1070)

Definition at line 104 of file Z3_decl_kind.java.

Referenced by Expr.isBVRotateRightExtended().

◆ Z3_OP_EXTRACT

Z3_OP_EXTRACT =(1059)

Definition at line 93 of file Z3_decl_kind.java.

Referenced by Expr.isBVExtract().

◆ Z3_OP_FALSE

Z3_OP_FALSE =(257)

Definition at line 15 of file Z3_decl_kind.java.

Referenced by Expr.isFalse().

◆ Z3_OP_FD_CONSTANT

Z3_OP_FD_CONSTANT =(1549)

Definition at line 173 of file Z3_decl_kind.java.

◆ Z3_OP_FD_LT

Z3_OP_FD_LT =(1550)

Definition at line 174 of file Z3_decl_kind.java.

Referenced by Expr.isFiniteDomainLT().

◆ Z3_OP_FPA_ABS

Z3_OP_FPA_ABS =(45073)

Definition at line 238 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_ADD

Z3_OP_FPA_ADD =(45067)

Definition at line 232 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_BV2RM

Z3_OP_FPA_BV2RM =(45099)

Definition at line 264 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_BVWRAP

Z3_OP_FPA_BVWRAP =(45098)

Definition at line 263 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_DIV

Z3_OP_FPA_DIV =(45071)

Definition at line 236 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_EQ

Z3_OP_FPA_EQ =(45079)

Definition at line 244 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_FMA

Z3_OP_FPA_FMA =(45076)

Definition at line 241 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_FP

Z3_OP_FPA_FP =(45091)

Definition at line 256 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_GE

Z3_OP_FPA_GE =(45083)

Definition at line 248 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_GT

Z3_OP_FPA_GT =(45081)

Definition at line 246 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_IS_INF

Z3_OP_FPA_IS_INF =(45085)

Definition at line 250 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_IS_NAN

Z3_OP_FPA_IS_NAN =(45084)

Definition at line 249 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_IS_NEGATIVE

Z3_OP_FPA_IS_NEGATIVE =(45089)

Definition at line 254 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_IS_NORMAL

Z3_OP_FPA_IS_NORMAL =(45087)

Definition at line 252 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_IS_POSITIVE

Z3_OP_FPA_IS_POSITIVE =(45090)

Definition at line 255 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_IS_SUBNORMAL

Z3_OP_FPA_IS_SUBNORMAL =(45088)

Definition at line 253 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_IS_ZERO

Z3_OP_FPA_IS_ZERO =(45086)

Definition at line 251 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_LE

Z3_OP_FPA_LE =(45082)

Definition at line 247 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_LT

Z3_OP_FPA_LT =(45080)

Definition at line 245 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_MAX

Z3_OP_FPA_MAX =(45075)

Definition at line 240 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_MIN

Z3_OP_FPA_MIN =(45074)

Definition at line 239 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_MINUS_INF

Z3_OP_FPA_MINUS_INF =(45063)

Definition at line 228 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_MINUS_ZERO

Z3_OP_FPA_MINUS_ZERO =(45066)

Definition at line 231 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_MUL

Z3_OP_FPA_MUL =(45070)

Definition at line 235 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_NAN

Z3_OP_FPA_NAN =(45064)

Definition at line 229 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_NEG

Z3_OP_FPA_NEG =(45069)

Definition at line 234 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_NUM

Z3_OP_FPA_NUM =(45061)

Definition at line 226 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_PLUS_INF

Z3_OP_FPA_PLUS_INF =(45062)

Definition at line 227 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_PLUS_ZERO

Z3_OP_FPA_PLUS_ZERO =(45065)

Definition at line 230 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_REM

Z3_OP_FPA_REM =(45072)

Definition at line 237 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY

Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY =(45057)

Definition at line 222 of file Z3_decl_kind.java.

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

◆ Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN

Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN =(45056)

Definition at line 221 of file Z3_decl_kind.java.

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

◆ Z3_OP_FPA_RM_TOWARD_NEGATIVE

Z3_OP_FPA_RM_TOWARD_NEGATIVE =(45059)

Definition at line 224 of file Z3_decl_kind.java.

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

◆ Z3_OP_FPA_RM_TOWARD_POSITIVE

Z3_OP_FPA_RM_TOWARD_POSITIVE =(45058)

Definition at line 223 of file Z3_decl_kind.java.

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

◆ Z3_OP_FPA_RM_TOWARD_ZERO

Z3_OP_FPA_RM_TOWARD_ZERO =(45060)

Definition at line 225 of file Z3_decl_kind.java.

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

◆ Z3_OP_FPA_ROUND_TO_INTEGRAL

Z3_OP_FPA_ROUND_TO_INTEGRAL =(45078)

Definition at line 243 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_SQRT

Z3_OP_FPA_SQRT =(45077)

Definition at line 242 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_SUB

Z3_OP_FPA_SUB =(45068)

Definition at line 233 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_TO_FP

Z3_OP_FPA_TO_FP =(45092)

Definition at line 257 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_TO_FP_UNSIGNED

Z3_OP_FPA_TO_FP_UNSIGNED =(45093)

Definition at line 258 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_TO_IEEE_BV

Z3_OP_FPA_TO_IEEE_BV =(45097)

Definition at line 262 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_TO_REAL

Z3_OP_FPA_TO_REAL =(45096)

Definition at line 261 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_TO_SBV

Z3_OP_FPA_TO_SBV =(45095)

Definition at line 260 of file Z3_decl_kind.java.

◆ Z3_OP_FPA_TO_UBV

Z3_OP_FPA_TO_UBV =(45094)

Definition at line 259 of file Z3_decl_kind.java.

◆ Z3_OP_GE

Z3_OP_GE =(515)

Definition at line 29 of file Z3_decl_kind.java.

Referenced by Expr.isGE().

◆ Z3_OP_GT

Z3_OP_GT =(517)

Definition at line 31 of file Z3_decl_kind.java.

Referenced by Expr.isGT().

◆ Z3_OP_IDIV

Z3_OP_IDIV =(523)

Definition at line 37 of file Z3_decl_kind.java.

Referenced by Expr.isIDiv().

◆ Z3_OP_IFF

Z3_OP_IFF =(263)

Definition at line 21 of file Z3_decl_kind.java.

Referenced by Expr.isIff().

◆ Z3_OP_IMPLIES

Z3_OP_IMPLIES =(266)

Definition at line 24 of file Z3_decl_kind.java.

Referenced by Expr.isImplies().

◆ Z3_OP_INT2BV

Z3_OP_INT2BV =(1072)

Definition at line 106 of file Z3_decl_kind.java.

Referenced by Expr.isIntToBV().

◆ Z3_OP_INT_TO_STR

Z3_OP_INT_TO_STR =(1567)

Definition at line 191 of file Z3_decl_kind.java.

◆ Z3_OP_INTERNAL

Z3_OP_INTERNAL =(45100)

Definition at line 265 of file Z3_decl_kind.java.

◆ Z3_OP_IS_INT

Z3_OP_IS_INT =(528)

Definition at line 42 of file Z3_decl_kind.java.

Referenced by Expr.isRealIsInt().

◆ Z3_OP_ITE

Z3_OP_ITE =(260)

Definition at line 18 of file Z3_decl_kind.java.

Referenced by Expr.isITE().

◆ Z3_OP_LABEL

Z3_OP_LABEL =(1792)

Definition at line 203 of file Z3_decl_kind.java.

Referenced by Expr.isLabel().

◆ Z3_OP_LABEL_LIT

Z3_OP_LABEL_LIT =(1793)

Definition at line 204 of file Z3_decl_kind.java.

Referenced by Expr.isLabelLit().

◆ Z3_OP_LE

Z3_OP_LE =(514)

Definition at line 28 of file Z3_decl_kind.java.

Referenced by Expr.isLE().

◆ Z3_OP_LT

Z3_OP_LT =(516)

Definition at line 30 of file Z3_decl_kind.java.

Referenced by Expr.isLT().

◆ Z3_OP_MOD

Z3_OP_MOD =(525)

Definition at line 39 of file Z3_decl_kind.java.

Referenced by Expr.isModulus().

◆ Z3_OP_MUL

Z3_OP_MUL =(521)

Definition at line 35 of file Z3_decl_kind.java.

Referenced by Expr.isMul().

◆ Z3_OP_NOT

Z3_OP_NOT =(265)

Definition at line 23 of file Z3_decl_kind.java.

Referenced by Expr.isNot().

◆ Z3_OP_OEQ

Z3_OP_OEQ =(267)

Definition at line 25 of file Z3_decl_kind.java.

Referenced by Expr.isOEQ().

◆ Z3_OP_OR

Z3_OP_OR =(262)

Definition at line 20 of file Z3_decl_kind.java.

Referenced by Expr.isOr().

◆ Z3_OP_PB_AT_LEAST

Z3_OP_PB_AT_LEAST =(2305)

Definition at line 211 of file Z3_decl_kind.java.

◆ Z3_OP_PB_AT_MOST

Z3_OP_PB_AT_MOST =(2304)

Definition at line 210 of file Z3_decl_kind.java.

◆ Z3_OP_PB_EQ

Z3_OP_PB_EQ =(2308)

Definition at line 214 of file Z3_decl_kind.java.

◆ Z3_OP_PB_GE

Z3_OP_PB_GE =(2307)

Definition at line 213 of file Z3_decl_kind.java.

◆ Z3_OP_PB_LE

Z3_OP_PB_LE =(2306)

Definition at line 212 of file Z3_decl_kind.java.

◆ Z3_OP_POWER

Z3_OP_POWER =(529)

Definition at line 43 of file Z3_decl_kind.java.

◆ Z3_OP_PR_AND_ELIM

Z3_OP_PR_AND_ELIM =(1293)

Definition at line 131 of file Z3_decl_kind.java.

Referenced by Expr.isProofAndElimination().

◆ Z3_OP_PR_APPLY_DEF

Z3_OP_PR_APPLY_DEF =(1314)

Definition at line 152 of file Z3_decl_kind.java.

Referenced by Expr.isProofApplyDef().

◆ Z3_OP_PR_ASSERTED

Z3_OP_PR_ASSERTED =(1282)

Definition at line 120 of file Z3_decl_kind.java.

Referenced by Expr.isProofAsserted().

◆ Z3_OP_PR_ASSUMPTION_ADD

Z3_OP_PR_ASSUMPTION_ADD =(1309)

Definition at line 147 of file Z3_decl_kind.java.

◆ Z3_OP_PR_BIND

Z3_OP_PR_BIND =(1291)

Definition at line 129 of file Z3_decl_kind.java.

◆ Z3_OP_PR_CLAUSE_TRAIL

Z3_OP_PR_CLAUSE_TRAIL =(1312)

Definition at line 150 of file Z3_decl_kind.java.

◆ Z3_OP_PR_COMMUTATIVITY

Z3_OP_PR_COMMUTATIVITY =(1307)

Definition at line 145 of file Z3_decl_kind.java.

Referenced by Expr.isProofCommutativity().

◆ Z3_OP_PR_DEF_AXIOM

Z3_OP_PR_DEF_AXIOM =(1308)

Definition at line 146 of file Z3_decl_kind.java.

Referenced by Expr.isProofDefAxiom().

◆ Z3_OP_PR_DEF_INTRO

Z3_OP_PR_DEF_INTRO =(1313)

Definition at line 151 of file Z3_decl_kind.java.

Referenced by Expr.isProofDefIntro().

◆ Z3_OP_PR_DER

Z3_OP_PR_DER =(1300)

Definition at line 138 of file Z3_decl_kind.java.

Referenced by Expr.isProofDER().

◆ Z3_OP_PR_DISTRIBUTIVITY

Z3_OP_PR_DISTRIBUTIVITY =(1292)

Definition at line 130 of file Z3_decl_kind.java.

Referenced by Expr.isProofDistributivity().

◆ Z3_OP_PR_ELIM_UNUSED_VARS

Z3_OP_PR_ELIM_UNUSED_VARS =(1299)

Definition at line 137 of file Z3_decl_kind.java.

Referenced by Expr.isProofElimUnusedVars().

◆ Z3_OP_PR_GOAL

Z3_OP_PR_GOAL =(1283)

Definition at line 121 of file Z3_decl_kind.java.

Referenced by Expr.isProofGoal().

◆ Z3_OP_PR_HYPER_RESOLVE

Z3_OP_PR_HYPER_RESOLVE =(1321)

Definition at line 159 of file Z3_decl_kind.java.

◆ Z3_OP_PR_HYPOTHESIS

Z3_OP_PR_HYPOTHESIS =(1302)

Definition at line 140 of file Z3_decl_kind.java.

Referenced by Expr.isProofHypothesis().

◆ Z3_OP_PR_IFF_FALSE

Z3_OP_PR_IFF_FALSE =(1306)

Definition at line 144 of file Z3_decl_kind.java.

Referenced by Expr.isProofIFFFalse().

◆ Z3_OP_PR_IFF_OEQ

Z3_OP_PR_IFF_OEQ =(1315)

Definition at line 153 of file Z3_decl_kind.java.

Referenced by Expr.isProofIFFOEQ().

◆ Z3_OP_PR_IFF_TRUE

Z3_OP_PR_IFF_TRUE =(1305)

Definition at line 143 of file Z3_decl_kind.java.

Referenced by Expr.isProofIFFTrue().

◆ Z3_OP_PR_LEMMA

Z3_OP_PR_LEMMA =(1303)

Definition at line 141 of file Z3_decl_kind.java.

Referenced by Expr.isProofLemma().

◆ Z3_OP_PR_LEMMA_ADD

Z3_OP_PR_LEMMA_ADD =(1310)

Definition at line 148 of file Z3_decl_kind.java.

◆ Z3_OP_PR_MODUS_PONENS

Z3_OP_PR_MODUS_PONENS =(1284)

Definition at line 122 of file Z3_decl_kind.java.

Referenced by Expr.isProofModusPonens().

◆ Z3_OP_PR_MODUS_PONENS_OEQ

Z3_OP_PR_MODUS_PONENS_OEQ =(1319)

Definition at line 157 of file Z3_decl_kind.java.

Referenced by Expr.isProofModusPonensOEQ().

◆ Z3_OP_PR_MONOTONICITY

Z3_OP_PR_MONOTONICITY =(1289)

Definition at line 127 of file Z3_decl_kind.java.

Referenced by Expr.isProofMonotonicity().

◆ Z3_OP_PR_NNF_NEG

Z3_OP_PR_NNF_NEG =(1317)

Definition at line 155 of file Z3_decl_kind.java.

Referenced by Expr.isProofNNFNeg().

◆ Z3_OP_PR_NNF_POS

Z3_OP_PR_NNF_POS =(1316)

Definition at line 154 of file Z3_decl_kind.java.

Referenced by Expr.isProofNNFPos().

◆ Z3_OP_PR_NOT_OR_ELIM

Z3_OP_PR_NOT_OR_ELIM =(1294)

Definition at line 132 of file Z3_decl_kind.java.

Referenced by Expr.isProofOrElimination().

◆ Z3_OP_PR_PULL_QUANT

Z3_OP_PR_PULL_QUANT =(1297)

Definition at line 135 of file Z3_decl_kind.java.

Referenced by Expr.isProofPullQuant().

◆ Z3_OP_PR_PUSH_QUANT

Z3_OP_PR_PUSH_QUANT =(1298)

Definition at line 136 of file Z3_decl_kind.java.

Referenced by Expr.isProofPushQuant().

◆ Z3_OP_PR_QUANT_INST

Z3_OP_PR_QUANT_INST =(1301)

Definition at line 139 of file Z3_decl_kind.java.

Referenced by Expr.isProofQuantInst().

◆ Z3_OP_PR_QUANT_INTRO

Z3_OP_PR_QUANT_INTRO =(1290)

Definition at line 128 of file Z3_decl_kind.java.

Referenced by Expr.isProofQuantIntro().

◆ Z3_OP_PR_REDUNDANT_DEL

Z3_OP_PR_REDUNDANT_DEL =(1311)

Definition at line 149 of file Z3_decl_kind.java.

◆ Z3_OP_PR_REFLEXIVITY

Z3_OP_PR_REFLEXIVITY =(1285)

Definition at line 123 of file Z3_decl_kind.java.

Referenced by Expr.isProofReflexivity().

◆ Z3_OP_PR_REWRITE

Z3_OP_PR_REWRITE =(1295)

Definition at line 133 of file Z3_decl_kind.java.

Referenced by Expr.isProofRewrite().

◆ Z3_OP_PR_REWRITE_STAR

Z3_OP_PR_REWRITE_STAR =(1296)

Definition at line 134 of file Z3_decl_kind.java.

Referenced by Expr.isProofRewriteStar().

◆ Z3_OP_PR_SKOLEMIZE

Z3_OP_PR_SKOLEMIZE =(1318)

Definition at line 156 of file Z3_decl_kind.java.

Referenced by Expr.isProofSkolemize().

◆ Z3_OP_PR_SYMMETRY

Z3_OP_PR_SYMMETRY =(1286)

Definition at line 124 of file Z3_decl_kind.java.

Referenced by Expr.isProofSymmetry().

◆ Z3_OP_PR_TH_LEMMA

Z3_OP_PR_TH_LEMMA =(1320)

Definition at line 158 of file Z3_decl_kind.java.

Referenced by Expr.isProofTheoryLemma().

◆ Z3_OP_PR_TRANSITIVITY

Z3_OP_PR_TRANSITIVITY =(1287)

Definition at line 125 of file Z3_decl_kind.java.

Referenced by Expr.isProofTransitivity().

◆ Z3_OP_PR_TRANSITIVITY_STAR

Z3_OP_PR_TRANSITIVITY_STAR =(1288)

Definition at line 126 of file Z3_decl_kind.java.

Referenced by Expr.isProofTransitivityStar().

◆ Z3_OP_PR_TRUE

Z3_OP_PR_TRUE =(1281)

Definition at line 119 of file Z3_decl_kind.java.

Referenced by Expr.isProofTrue().

◆ Z3_OP_PR_UNDEF

Z3_OP_PR_UNDEF =(1280)

Definition at line 118 of file Z3_decl_kind.java.

◆ Z3_OP_PR_UNIT_RESOLUTION

Z3_OP_PR_UNIT_RESOLUTION =(1304)

Definition at line 142 of file Z3_decl_kind.java.

Referenced by Expr.isProofUnitResolution().

◆ Z3_OP_RA_CLONE

Z3_OP_RA_CLONE =(1548)

Definition at line 172 of file Z3_decl_kind.java.

Referenced by Expr.isRelationClone().

◆ Z3_OP_RA_COMPLEMENT

Z3_OP_RA_COMPLEMENT =(1546)

Definition at line 170 of file Z3_decl_kind.java.

Referenced by Expr.isRelationComplement().

◆ Z3_OP_RA_EMPTY

Z3_OP_RA_EMPTY =(1537)

Definition at line 161 of file Z3_decl_kind.java.

Referenced by Expr.isEmptyRelation().

◆ Z3_OP_RA_FILTER

Z3_OP_RA_FILTER =(1543)

Definition at line 167 of file Z3_decl_kind.java.

Referenced by Expr.isRelationFilter().

◆ Z3_OP_RA_IS_EMPTY

Z3_OP_RA_IS_EMPTY =(1538)

Definition at line 162 of file Z3_decl_kind.java.

Referenced by Expr.isIsEmptyRelation().

◆ Z3_OP_RA_JOIN

Z3_OP_RA_JOIN =(1539)

Definition at line 163 of file Z3_decl_kind.java.

Referenced by Expr.isRelationalJoin().

◆ Z3_OP_RA_NEGATION_FILTER

Z3_OP_RA_NEGATION_FILTER =(1544)

Definition at line 168 of file Z3_decl_kind.java.

Referenced by Expr.isRelationNegationFilter().

◆ Z3_OP_RA_PROJECT

Z3_OP_RA_PROJECT =(1542)

Definition at line 166 of file Z3_decl_kind.java.

Referenced by Expr.isRelationProject().

◆ Z3_OP_RA_RENAME

Z3_OP_RA_RENAME =(1545)

Definition at line 169 of file Z3_decl_kind.java.

Referenced by Expr.isRelationRename().

◆ Z3_OP_RA_SELECT

Z3_OP_RA_SELECT =(1547)

Definition at line 171 of file Z3_decl_kind.java.

Referenced by Expr.isRelationSelect().

◆ Z3_OP_RA_STORE

Z3_OP_RA_STORE =(1536)

Definition at line 160 of file Z3_decl_kind.java.

Referenced by Expr.isRelationStore().

◆ Z3_OP_RA_UNION

Z3_OP_RA_UNION =(1540)

Definition at line 164 of file Z3_decl_kind.java.

Referenced by Expr.isRelationUnion().

◆ Z3_OP_RA_WIDEN

Z3_OP_RA_WIDEN =(1541)

Definition at line 165 of file Z3_decl_kind.java.

Referenced by Expr.isRelationWiden().

◆ Z3_OP_RE_COMPLEMENT

Z3_OP_RE_COMPLEMENT =(1578)

Definition at line 202 of file Z3_decl_kind.java.

◆ Z3_OP_RE_CONCAT

Z3_OP_RE_CONCAT =(1571)

Definition at line 195 of file Z3_decl_kind.java.

◆ Z3_OP_RE_EMPTY_SET

Z3_OP_RE_EMPTY_SET =(1576)

Definition at line 200 of file Z3_decl_kind.java.

◆ Z3_OP_RE_FULL_SET

Z3_OP_RE_FULL_SET =(1577)

Definition at line 201 of file Z3_decl_kind.java.

◆ Z3_OP_RE_INTERSECT

Z3_OP_RE_INTERSECT =(1575)

Definition at line 199 of file Z3_decl_kind.java.

◆ Z3_OP_RE_LOOP

Z3_OP_RE_LOOP =(1574)

Definition at line 198 of file Z3_decl_kind.java.

◆ Z3_OP_RE_OPTION

Z3_OP_RE_OPTION =(1570)

Definition at line 194 of file Z3_decl_kind.java.

◆ Z3_OP_RE_PLUS

Z3_OP_RE_PLUS =(1568)

Definition at line 192 of file Z3_decl_kind.java.

◆ Z3_OP_RE_RANGE

Z3_OP_RE_RANGE =(1573)

Definition at line 197 of file Z3_decl_kind.java.

◆ Z3_OP_RE_STAR

Z3_OP_RE_STAR =(1569)

Definition at line 193 of file Z3_decl_kind.java.

◆ Z3_OP_RE_UNION

Z3_OP_RE_UNION =(1572)

Definition at line 196 of file Z3_decl_kind.java.

◆ Z3_OP_REM

Z3_OP_REM =(524)

Definition at line 38 of file Z3_decl_kind.java.

Referenced by Expr.isRemainder().

◆ Z3_OP_REPEAT

Z3_OP_REPEAT =(1060)

Definition at line 94 of file Z3_decl_kind.java.

Referenced by Expr.isBVRepeat().

◆ Z3_OP_ROTATE_LEFT

Z3_OP_ROTATE_LEFT =(1067)

Definition at line 101 of file Z3_decl_kind.java.

Referenced by Expr.isBVRotateLeft().

◆ Z3_OP_ROTATE_RIGHT

Z3_OP_ROTATE_RIGHT =(1068)

Definition at line 102 of file Z3_decl_kind.java.

Referenced by Expr.isBVRotateRight().

◆ Z3_OP_SELECT

Z3_OP_SELECT =(769)

Definition at line 45 of file Z3_decl_kind.java.

Referenced by Expr.isSelect().

◆ Z3_OP_SEQ_AT

Z3_OP_SEQ_AT =(1559)

Definition at line 183 of file Z3_decl_kind.java.

◆ Z3_OP_SEQ_CONCAT

Z3_OP_SEQ_CONCAT =(1553)

Definition at line 177 of file Z3_decl_kind.java.

Referenced by Expr.isConcat().

◆ Z3_OP_SEQ_CONTAINS

Z3_OP_SEQ_CONTAINS =(1556)

Definition at line 180 of file Z3_decl_kind.java.

◆ Z3_OP_SEQ_EMPTY

Z3_OP_SEQ_EMPTY =(1552)

Definition at line 176 of file Z3_decl_kind.java.

◆ Z3_OP_SEQ_EXTRACT

Z3_OP_SEQ_EXTRACT =(1557)

Definition at line 181 of file Z3_decl_kind.java.

◆ Z3_OP_SEQ_IN_RE

Z3_OP_SEQ_IN_RE =(1565)

Definition at line 189 of file Z3_decl_kind.java.

◆ Z3_OP_SEQ_INDEX

Z3_OP_SEQ_INDEX =(1562)

Definition at line 186 of file Z3_decl_kind.java.

◆ Z3_OP_SEQ_LAST_INDEX

Z3_OP_SEQ_LAST_INDEX =(1563)

Definition at line 187 of file Z3_decl_kind.java.

◆ Z3_OP_SEQ_LENGTH

Z3_OP_SEQ_LENGTH =(1561)

Definition at line 185 of file Z3_decl_kind.java.

◆ Z3_OP_SEQ_NTH

Z3_OP_SEQ_NTH =(1560)

Definition at line 184 of file Z3_decl_kind.java.

◆ Z3_OP_SEQ_PREFIX

Z3_OP_SEQ_PREFIX =(1554)

Definition at line 178 of file Z3_decl_kind.java.

◆ Z3_OP_SEQ_REPLACE

Z3_OP_SEQ_REPLACE =(1558)

Definition at line 182 of file Z3_decl_kind.java.

◆ Z3_OP_SEQ_SUFFIX

Z3_OP_SEQ_SUFFIX =(1555)

Definition at line 179 of file Z3_decl_kind.java.

◆ Z3_OP_SEQ_TO_RE

Z3_OP_SEQ_TO_RE =(1564)

Definition at line 188 of file Z3_decl_kind.java.

◆ Z3_OP_SEQ_UNIT

Z3_OP_SEQ_UNIT =(1551)

Definition at line 175 of file Z3_decl_kind.java.

◆ Z3_OP_SET_CARD

Z3_OP_SET_CARD =(781)

Definition at line 57 of file Z3_decl_kind.java.

◆ Z3_OP_SET_COMPLEMENT

Z3_OP_SET_COMPLEMENT =(776)

Definition at line 52 of file Z3_decl_kind.java.

Referenced by Expr.isSetComplement().

◆ Z3_OP_SET_DIFFERENCE

Z3_OP_SET_DIFFERENCE =(775)

Definition at line 51 of file Z3_decl_kind.java.

Referenced by Expr.isSetDifference().

◆ Z3_OP_SET_HAS_SIZE

Z3_OP_SET_HAS_SIZE =(780)

Definition at line 56 of file Z3_decl_kind.java.

◆ Z3_OP_SET_INTERSECT

Z3_OP_SET_INTERSECT =(774)

Definition at line 50 of file Z3_decl_kind.java.

Referenced by Expr.isSetIntersect().

◆ Z3_OP_SET_SUBSET

Z3_OP_SET_SUBSET =(777)

Definition at line 53 of file Z3_decl_kind.java.

Referenced by Expr.isSetSubset().

◆ Z3_OP_SET_UNION

Z3_OP_SET_UNION =(773)

Definition at line 49 of file Z3_decl_kind.java.

Referenced by Expr.isSetUnion().

◆ Z3_OP_SGEQ

Z3_OP_SGEQ =(1044)

Definition at line 78 of file Z3_decl_kind.java.

Referenced by Expr.isBVSGE().

◆ Z3_OP_SGT

Z3_OP_SGT =(1048)

Definition at line 82 of file Z3_decl_kind.java.

Referenced by Expr.isBVSGT().

◆ Z3_OP_SIGN_EXT

Z3_OP_SIGN_EXT =(1057)

Definition at line 91 of file Z3_decl_kind.java.

Referenced by Expr.isBVSignExtension().

◆ Z3_OP_SLEQ

Z3_OP_SLEQ =(1042)

Definition at line 76 of file Z3_decl_kind.java.

Referenced by Expr.isBVSLE().

◆ Z3_OP_SLT

Z3_OP_SLT =(1046)

Definition at line 80 of file Z3_decl_kind.java.

Referenced by Expr.isBVSLT().

◆ Z3_OP_SPECIAL_RELATION_LO

Z3_OP_SPECIAL_RELATION_LO =(40960)

Definition at line 215 of file Z3_decl_kind.java.

◆ Z3_OP_SPECIAL_RELATION_PLO

Z3_OP_SPECIAL_RELATION_PLO =(40962)

Definition at line 217 of file Z3_decl_kind.java.

◆ Z3_OP_SPECIAL_RELATION_PO

Z3_OP_SPECIAL_RELATION_PO =(40961)

Definition at line 216 of file Z3_decl_kind.java.

◆ Z3_OP_SPECIAL_RELATION_TC

Z3_OP_SPECIAL_RELATION_TC =(40964)

Definition at line 219 of file Z3_decl_kind.java.

◆ Z3_OP_SPECIAL_RELATION_TO

Z3_OP_SPECIAL_RELATION_TO =(40963)

Definition at line 218 of file Z3_decl_kind.java.

◆ Z3_OP_SPECIAL_RELATION_TRC

Z3_OP_SPECIAL_RELATION_TRC =(40965)

Definition at line 220 of file Z3_decl_kind.java.

◆ Z3_OP_STORE

Z3_OP_STORE =(768)

Definition at line 44 of file Z3_decl_kind.java.

Referenced by Expr.isStore().

◆ Z3_OP_STR_TO_INT

Z3_OP_STR_TO_INT =(1566)

Definition at line 190 of file Z3_decl_kind.java.

◆ Z3_OP_SUB

Z3_OP_SUB =(519)

Definition at line 33 of file Z3_decl_kind.java.

Referenced by Expr.isSub().

◆ Z3_OP_TO_INT

Z3_OP_TO_INT =(527)

Definition at line 41 of file Z3_decl_kind.java.

Referenced by Expr.isRealToInt().

◆ Z3_OP_TO_REAL

Z3_OP_TO_REAL =(526)

Definition at line 40 of file Z3_decl_kind.java.

Referenced by Expr.isIntToReal().

◆ Z3_OP_TRUE

Z3_OP_TRUE =(256)

Definition at line 14 of file Z3_decl_kind.java.

Referenced by Expr.isTrue().

◆ Z3_OP_UGEQ

Z3_OP_UGEQ =(1043)

Definition at line 77 of file Z3_decl_kind.java.

Referenced by Expr.isBVUGE().

◆ Z3_OP_UGT

Z3_OP_UGT =(1047)

Definition at line 81 of file Z3_decl_kind.java.

Referenced by Expr.isBVUGT().

◆ Z3_OP_ULEQ

Z3_OP_ULEQ =(1041)

Definition at line 75 of file Z3_decl_kind.java.

Referenced by Expr.isBVULE().

◆ Z3_OP_ULT

Z3_OP_ULT =(1045)

Definition at line 79 of file Z3_decl_kind.java.

Referenced by Expr.isBVULT().

◆ Z3_OP_UMINUS

Z3_OP_UMINUS =(520)

Definition at line 34 of file Z3_decl_kind.java.

Referenced by Expr.isUMinus().

◆ Z3_OP_UNINTERPRETED

Z3_OP_UNINTERPRETED =(45101)

Definition at line 266 of file Z3_decl_kind.java.

◆ Z3_OP_XOR

Z3_OP_XOR =(264)

Definition at line 22 of file Z3_decl_kind.java.

Referenced by Expr.isXor().

◆ Z3_OP_XOR3

Z3_OP_XOR3 =(1075)

Definition at line 109 of file Z3_decl_kind.java.

Referenced by Expr.isBVXOR3().

◆ Z3_OP_ZERO_EXT

Z3_OP_ZERO_EXT =(1058)

Definition at line 92 of file Z3_decl_kind.java.

Referenced by Expr.isBVZeroExtension().

Z3_decl_kind
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:1007