Z3
Z3_decl_kind.java
Go to the documentation of this file.
1 
5 package com.microsoft.z3.enumerations;
6 
7 import java.util.HashMap;
8 import java.util.Map;
9 
13 public enum Z3_decl_kind {
14  Z3_OP_TRUE (256),
15  Z3_OP_FALSE (257),
16  Z3_OP_EQ (258),
18  Z3_OP_ITE (260),
19  Z3_OP_AND (261),
20  Z3_OP_OR (262),
21  Z3_OP_IFF (263),
22  Z3_OP_XOR (264),
23  Z3_OP_NOT (265),
25  Z3_OP_OEQ (267),
26  Z3_OP_ANUM (512),
27  Z3_OP_AGNUM (513),
28  Z3_OP_LE (514),
29  Z3_OP_GE (515),
30  Z3_OP_LT (516),
31  Z3_OP_GT (517),
32  Z3_OP_ADD (518),
33  Z3_OP_SUB (519),
34  Z3_OP_UMINUS (520),
35  Z3_OP_MUL (521),
36  Z3_OP_DIV (522),
37  Z3_OP_IDIV (523),
38  Z3_OP_REM (524),
39  Z3_OP_MOD (525),
41  Z3_OP_TO_INT (527),
42  Z3_OP_IS_INT (528),
43  Z3_OP_POWER (529),
44  Z3_OP_STORE (768),
45  Z3_OP_SELECT (769),
58  Z3_OP_BNUM (1024),
59  Z3_OP_BIT1 (1025),
60  Z3_OP_BIT0 (1026),
61  Z3_OP_BNEG (1027),
62  Z3_OP_BADD (1028),
63  Z3_OP_BSUB (1029),
64  Z3_OP_BMUL (1030),
65  Z3_OP_BSDIV (1031),
66  Z3_OP_BUDIV (1032),
67  Z3_OP_BSREM (1033),
68  Z3_OP_BUREM (1034),
69  Z3_OP_BSMOD (1035),
70  Z3_OP_BSDIV0 (1036),
71  Z3_OP_BUDIV0 (1037),
72  Z3_OP_BSREM0 (1038),
73  Z3_OP_BUREM0 (1039),
74  Z3_OP_BSMOD0 (1040),
75  Z3_OP_ULEQ (1041),
76  Z3_OP_SLEQ (1042),
77  Z3_OP_UGEQ (1043),
78  Z3_OP_SGEQ (1044),
79  Z3_OP_ULT (1045),
80  Z3_OP_SLT (1046),
81  Z3_OP_UGT (1047),
82  Z3_OP_SGT (1048),
83  Z3_OP_BAND (1049),
84  Z3_OP_BOR (1050),
85  Z3_OP_BNOT (1051),
86  Z3_OP_BXOR (1052),
87  Z3_OP_BNAND (1053),
88  Z3_OP_BNOR (1054),
89  Z3_OP_BXNOR (1055),
90  Z3_OP_CONCAT (1056),
93  Z3_OP_EXTRACT (1059),
94  Z3_OP_REPEAT (1060),
95  Z3_OP_BREDOR (1061),
96  Z3_OP_BREDAND (1062),
97  Z3_OP_BCOMP (1063),
98  Z3_OP_BSHL (1064),
99  Z3_OP_BLSHR (1065),
100  Z3_OP_BASHR (1066),
106  Z3_OP_INT2BV (1072),
107  Z3_OP_BV2INT (1073),
108  Z3_OP_CARRY (1074),
109  Z3_OP_XOR3 (1075),
138  Z3_OP_PR_DER (1300),
174  Z3_OP_FD_LT (1550),
183  Z3_OP_SEQ_AT (1559),
203  Z3_OP_LABEL (1792),
207  Z3_OP_DT_IS (2050),
212  Z3_OP_PB_LE (2306),
213  Z3_OP_PB_GE (2307),
214  Z3_OP_PB_EQ (2308),
226  Z3_OP_FPA_NUM (45061),
229  Z3_OP_FPA_NAN (45064),
232  Z3_OP_FPA_ADD (45067),
233  Z3_OP_FPA_SUB (45068),
234  Z3_OP_FPA_NEG (45069),
235  Z3_OP_FPA_MUL (45070),
236  Z3_OP_FPA_DIV (45071),
237  Z3_OP_FPA_REM (45072),
238  Z3_OP_FPA_ABS (45073),
239  Z3_OP_FPA_MIN (45074),
240  Z3_OP_FPA_MAX (45075),
241  Z3_OP_FPA_FMA (45076),
242  Z3_OP_FPA_SQRT (45077),
244  Z3_OP_FPA_EQ (45079),
245  Z3_OP_FPA_LT (45080),
246  Z3_OP_FPA_GT (45081),
247  Z3_OP_FPA_LE (45082),
248  Z3_OP_FPA_GE (45083),
256  Z3_OP_FPA_FP (45091),
265  Z3_OP_INTERNAL (45100),
267 
268  private final int intValue;
269 
270  Z3_decl_kind(int v) {
271  this.intValue = v;
272  }
273 
274  // Cannot initialize map in constructor, so need to do it lazily.
275  // Easiest thread-safe way is the initialization-on-demand holder pattern.
276  private static class Z3_decl_kind_MappingHolder {
277  private static final Map<Integer, Z3_decl_kind> intMapping = new HashMap<>();
278  static {
279  for (Z3_decl_kind k : Z3_decl_kind.values())
280  intMapping.put(k.toInt(), k);
281  }
282  }
283 
284  public static final Z3_decl_kind fromInt(int v) {
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  }
289 
290  public final int toInt() { return this.intValue; }
291 }
292 
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR
Z3_OP_PR_TRANSITIVITY_STAR
Definition: Z3_decl_kind.java:126
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_SELECT
Z3_OP_RA_SELECT
Definition: Z3_decl_kind.java:171
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_POWER
Z3_OP_POWER
Definition: Z3_decl_kind.java:43
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_DT_CONSTRUCTOR
Z3_OP_DT_CONSTRUCTOR
Definition: Z3_decl_kind.java:205
com.microsoft.z3.enumerations.Z3_decl_kind.toInt
final int toInt()
Definition: Z3_decl_kind.java:290
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ARRAY_MAP
Z3_OP_ARRAY_MAP
Definition: Z3_decl_kind.java:47
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_BV2RM
Z3_OP_FPA_BV2RM
Definition: Z3_decl_kind.java:264
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_NOT
Z3_OP_NOT
Definition: Z3_decl_kind.java:23
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_PLUS_INF
Z3_OP_FPA_PLUS_INF
Definition: Z3_decl_kind.java:227
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SEQ_REPLACE
Z3_OP_SEQ_REPLACE
Definition: Z3_decl_kind.java:182
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_TO_REAL
Z3_OP_TO_REAL
Definition: Z3_decl_kind.java:40
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RE_COMPLEMENT
Z3_OP_RE_COMPLEMENT
Definition: Z3_decl_kind.java:202
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BNOT
Z3_OP_BNOT
Definition: Z3_decl_kind.java:85
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BREDAND
Z3_OP_BREDAND
Definition: Z3_decl_kind.java:96
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_PUSH_QUANT
Z3_OP_PR_PUSH_QUANT
Definition: Z3_decl_kind.java:136
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_IS_INF
Z3_OP_FPA_IS_INF
Definition: Z3_decl_kind.java:250
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_BIND
Z3_OP_PR_BIND
Definition: Z3_decl_kind.java:129
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SPECIAL_RELATION_PO
Z3_OP_SPECIAL_RELATION_PO
Definition: Z3_decl_kind.java:216
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_IMPLIES
Z3_OP_IMPLIES
Definition: Z3_decl_kind.java:24
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PB_LE
Z3_OP_PB_LE
Definition: Z3_decl_kind.java:212
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_DEF_AXIOM
Z3_OP_PR_DEF_AXIOM
Definition: Z3_decl_kind.java:146
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BNUM
Z3_OP_BNUM
Definition: Z3_decl_kind.java:58
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SET_SUBSET
Z3_OP_SET_SUBSET
Definition: Z3_decl_kind.java:53
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_IS_INT
Z3_OP_IS_INT
Definition: Z3_decl_kind.java:42
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_TRUE
Z3_OP_TRUE
Definition: Z3_decl_kind.java:14
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_IFF_OEQ
Z3_OP_PR_IFF_OEQ
Definition: Z3_decl_kind.java:153
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_TO_FP_UNSIGNED
Z3_OP_FPA_TO_FP_UNSIGNED
Definition: Z3_decl_kind.java:258
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_LE
Z3_OP_FPA_LE
Definition: Z3_decl_kind.java:247
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSMUL_NO_UDFL
Z3_OP_BSMUL_NO_UDFL
Definition: Z3_decl_kind.java:112
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SPECIAL_RELATION_PLO
Z3_OP_SPECIAL_RELATION_PLO
Definition: Z3_decl_kind.java:217
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SLEQ
Z3_OP_SLEQ
Definition: Z3_decl_kind.java:76
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SPECIAL_RELATION_LO
Z3_OP_SPECIAL_RELATION_LO
Definition: Z3_decl_kind.java:215
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SEQ_IN_RE
Z3_OP_SEQ_IN_RE
Definition: Z3_decl_kind.java:189
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_COMPLEMENT
Z3_OP_RA_COMPLEMENT
Definition: Z3_decl_kind.java:170
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSREM0
Z3_OP_BSREM0
Definition: Z3_decl_kind.java:72
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSMOD
Z3_OP_BSMOD
Definition: Z3_decl_kind.java:69
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_IFF_TRUE
Z3_OP_PR_IFF_TRUE
Definition: Z3_decl_kind.java:143
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RE_OPTION
Z3_OP_RE_OPTION
Definition: Z3_decl_kind.java:194
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ITE
Z3_OP_ITE
Definition: Z3_decl_kind.java:18
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BUDIV_I
Z3_OP_BUDIV_I
Definition: Z3_decl_kind.java:114
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_MUL
Z3_OP_FPA_MUL
Definition: Z3_decl_kind.java:235
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS
Z3_OP_PR_ELIM_UNUSED_VARS
Definition: Z3_decl_kind.java:137
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_DT_IS
Z3_OP_DT_IS
Definition: Z3_decl_kind.java:207
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RE_LOOP
Z3_OP_RE_LOOP
Definition: Z3_decl_kind.java:198
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT
Z3_OP_EXT_ROTATE_LEFT
Definition: Z3_decl_kind.java:103
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SEQ_UNIT
Z3_OP_SEQ_UNIT
Definition: Z3_decl_kind.java:175
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_MODUS_PONENS
Z3_OP_PR_MODUS_PONENS
Definition: Z3_decl_kind.java:122
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_NEG
Z3_OP_FPA_NEG
Definition: Z3_decl_kind.java:234
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO
Z3_OP_FPA_RM_TOWARD_ZERO
Definition: Z3_decl_kind.java:225
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RE_FULL_SET
Z3_OP_RE_FULL_SET
Definition: Z3_decl_kind.java:201
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_HYPOTHESIS
Z3_OP_PR_HYPOTHESIS
Definition: Z3_decl_kind.java:140
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BXNOR
Z3_OP_BXNOR
Definition: Z3_decl_kind.java:89
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_GT
Z3_OP_FPA_GT
Definition: Z3_decl_kind.java:246
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_TO_REAL
Z3_OP_FPA_TO_REAL
Definition: Z3_decl_kind.java:261
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PB_AT_MOST
Z3_OP_PB_AT_MOST
Definition: Z3_decl_kind.java:210
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_MAX
Z3_OP_FPA_MAX
Definition: Z3_decl_kind.java:240
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_RENAME
Z3_OP_RA_RENAME
Definition: Z3_decl_kind.java:169
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BXOR
Z3_OP_BXOR
Definition: Z3_decl_kind.java:86
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_LABEL
Z3_OP_LABEL
Definition: Z3_decl_kind.java:203
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_CONCAT
Z3_OP_CONCAT
Definition: Z3_decl_kind.java:90
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER
Z3_OP_RA_NEGATION_FILTER
Definition: Z3_decl_kind.java:168
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN
Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN
Definition: Z3_decl_kind.java:221
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_UNINTERPRETED
Z3_OP_UNINTERPRETED
Definition: Z3_decl_kind.java:266
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_INT2BV
Z3_OP_INT2BV
Definition: Z3_decl_kind.java:106
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_LT
Z3_OP_LT
Definition: Z3_decl_kind.java:30
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BIT2BOOL
Z3_OP_BIT2BOOL
Definition: Z3_decl_kind.java:105
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BUREM_I
Z3_OP_BUREM_I
Definition: Z3_decl_kind.java:116
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BIT0
Z3_OP_BIT0
Definition: Z3_decl_kind.java:60
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BV2INT
Z3_OP_BV2INT
Definition: Z3_decl_kind.java:107
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RE_UNION
Z3_OP_RE_UNION
Definition: Z3_decl_kind.java:196
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_CONST_ARRAY
Z3_OP_CONST_ARRAY
Definition: Z3_decl_kind.java:46
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PB_GE
Z3_OP_PB_GE
Definition: Z3_decl_kind.java:213
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SPECIAL_RELATION_TO
Z3_OP_SPECIAL_RELATION_TO
Definition: Z3_decl_kind.java:218
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_TRANSITIVITY
Z3_OP_PR_TRANSITIVITY
Definition: Z3_decl_kind.java:125
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_PLUS_ZERO
Z3_OP_FPA_PLUS_ZERO
Definition: Z3_decl_kind.java:230
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_STR_TO_INT
Z3_OP_STR_TO_INT
Definition: Z3_decl_kind.java:190
com.microsoft.z3.enumerations.Z3_decl_kind
Definition: Z3_decl_kind.java:13
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BNAND
Z3_OP_BNAND
Definition: Z3_decl_kind.java:87
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_FP
Z3_OP_FPA_FP
Definition: Z3_decl_kind.java:256
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY
Z3_OP_PR_COMMUTATIVITY
Definition: Z3_decl_kind.java:145
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RE_STAR
Z3_OP_RE_STAR
Definition: Z3_decl_kind.java:193
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_IS_SUBNORMAL
Z3_OP_FPA_IS_SUBNORMAL
Definition: Z3_decl_kind.java:253
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_LE
Z3_OP_LE
Definition: Z3_decl_kind.java:28
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_INT_TO_STR
Z3_OP_INT_TO_STR
Definition: Z3_decl_kind.java:191
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_ADD
Z3_OP_FPA_ADD
Definition: Z3_decl_kind.java:232
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_TRUE
Z3_OP_PR_TRUE
Definition: Z3_decl_kind.java:119
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ROTATE_RIGHT
Z3_OP_ROTATE_RIGHT
Definition: Z3_decl_kind.java:102
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SET_DIFFERENCE
Z3_OP_SET_DIFFERENCE
Definition: Z3_decl_kind.java:51
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_TO_UBV
Z3_OP_FPA_TO_UBV
Definition: Z3_decl_kind.java:259
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_JOIN
Z3_OP_RA_JOIN
Definition: Z3_decl_kind.java:163
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BUMUL_NO_OVFL
Z3_OP_BUMUL_NO_OVFL
Definition: Z3_decl_kind.java:111
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_QUANT_INST
Z3_OP_PR_QUANT_INST
Definition: Z3_decl_kind.java:139
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SEQ_EXTRACT
Z3_OP_SEQ_EXTRACT
Definition: Z3_decl_kind.java:181
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_OR
Z3_OP_OR
Definition: Z3_decl_kind.java:20
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BASHR
Z3_OP_BASHR
Definition: Z3_decl_kind.java:100
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_IS_ZERO
Z3_OP_FPA_IS_ZERO
Definition: Z3_decl_kind.java:251
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SEQ_LENGTH
Z3_OP_SEQ_LENGTH
Definition: Z3_decl_kind.java:185
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SPECIAL_RELATION_TC
Z3_OP_SPECIAL_RELATION_TC
Definition: Z3_decl_kind.java:219
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_REM
Z3_OP_REM
Definition: Z3_decl_kind.java:38
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BIT1
Z3_OP_BIT1
Definition: Z3_decl_kind.java:59
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_UGT
Z3_OP_UGT
Definition: Z3_decl_kind.java:81
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_SUB
Z3_OP_FPA_SUB
Definition: Z3_decl_kind.java:233
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_CARRY
Z3_OP_CARRY
Definition: Z3_decl_kind.java:108
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_MOD
Z3_OP_MOD
Definition: Z3_decl_kind.java:39
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_TH_LEMMA
Z3_OP_PR_TH_LEMMA
Definition: Z3_decl_kind.java:158
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_TO_IEEE_BV
Z3_OP_FPA_TO_IEEE_BV
Definition: Z3_decl_kind.java:262
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_REDUNDANT_DEL
Z3_OP_PR_REDUNDANT_DEL
Definition: Z3_decl_kind.java:149
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_PULL_QUANT
Z3_OP_PR_PULL_QUANT
Definition: Z3_decl_kind.java:135
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SEQ_AT
Z3_OP_SEQ_AT
Definition: Z3_decl_kind.java:183
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_REPEAT
Z3_OP_REPEAT
Definition: Z3_decl_kind.java:94
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_NNF_NEG
Z3_OP_PR_NNF_NEG
Definition: Z3_decl_kind.java:155
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_IDIV
Z3_OP_IDIV
Definition: Z3_decl_kind.java:37
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_MUL
Z3_OP_MUL
Definition: Z3_decl_kind.java:35
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_SYMMETRY
Z3_OP_PR_SYMMETRY
Definition: Z3_decl_kind.java:124
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_DEF_INTRO
Z3_OP_PR_DEF_INTRO
Definition: Z3_decl_kind.java:151
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SEQ_PREFIX
Z3_OP_SEQ_PREFIX
Definition: Z3_decl_kind.java:178
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_MINUS_INF
Z3_OP_FPA_MINUS_INF
Definition: Z3_decl_kind.java:228
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_GT
Z3_OP_GT
Definition: Z3_decl_kind.java:31
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_AGNUM
Z3_OP_AGNUM
Definition: Z3_decl_kind.java:27
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RE_RANGE
Z3_OP_RE_RANGE
Definition: Z3_decl_kind.java:197
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSDIV_I
Z3_OP_BSDIV_I
Definition: Z3_decl_kind.java:113
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_LT
Z3_OP_FPA_LT
Definition: Z3_decl_kind.java:245
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BNOR
Z3_OP_BNOR
Definition: Z3_decl_kind.java:88
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SET_UNION
Z3_OP_SET_UNION
Definition: Z3_decl_kind.java:49
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSREM
Z3_OP_BSREM
Definition: Z3_decl_kind.java:67
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RE_EMPTY_SET
Z3_OP_RE_EMPTY_SET
Definition: Z3_decl_kind.java:200
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ARRAY_EXT
Z3_OP_ARRAY_EXT
Definition: Z3_decl_kind.java:55
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BUREM
Z3_OP_BUREM
Definition: Z3_decl_kind.java:68
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_CLONE
Z3_OP_RA_CLONE
Definition: Z3_decl_kind.java:172
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_NNF_POS
Z3_OP_PR_NNF_POS
Definition: Z3_decl_kind.java:154
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSUB
Z3_OP_BSUB
Definition: Z3_decl_kind.java:63
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_INTERNAL
Z3_OP_INTERNAL
Definition: Z3_decl_kind.java:265
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_IS_EMPTY
Z3_OP_RA_IS_EMPTY
Definition: Z3_decl_kind.java:162
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_NUM
Z3_OP_FPA_NUM
Definition: Z3_decl_kind.java:226
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RE_CONCAT
Z3_OP_RE_CONCAT
Definition: Z3_decl_kind.java:195
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SET_COMPLEMENT
Z3_OP_SET_COMPLEMENT
Definition: Z3_decl_kind.java:52
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PB_EQ
Z3_OP_PB_EQ
Definition: Z3_decl_kind.java:214
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ADD
Z3_OP_ADD
Definition: Z3_decl_kind.java:32
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_DT_RECOGNISER
Z3_OP_DT_RECOGNISER
Definition: Z3_decl_kind.java:206
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ULT
Z3_OP_ULT
Definition: Z3_decl_kind.java:79
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_HYPER_RESOLVE
Z3_OP_PR_HYPER_RESOLVE
Definition: Z3_decl_kind.java:159
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSMOD_I
Z3_OP_BSMOD_I
Definition: Z3_decl_kind.java:117
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_ROUND_TO_INTEGRAL
Z3_OP_FPA_ROUND_TO_INTEGRAL
Definition: Z3_decl_kind.java:243
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_GE
Z3_OP_FPA_GE
Definition: Z3_decl_kind.java:248
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSMOD0
Z3_OP_BSMOD0
Definition: Z3_decl_kind.java:74
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ZERO_EXT
Z3_OP_ZERO_EXT
Definition: Z3_decl_kind.java:92
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_GOAL
Z3_OP_PR_GOAL
Definition: Z3_decl_kind.java:121
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SIGN_EXT
Z3_OP_SIGN_EXT
Definition: Z3_decl_kind.java:91
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BUDIV0
Z3_OP_BUDIV0
Definition: Z3_decl_kind.java:71
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BREDOR
Z3_OP_BREDOR
Definition: Z3_decl_kind.java:95
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BLSHR
Z3_OP_BLSHR
Definition: Z3_decl_kind.java:99
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_REWRITE
Z3_OP_PR_REWRITE
Definition: Z3_decl_kind.java:133
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_UNION
Z3_OP_RA_UNION
Definition: Z3_decl_kind.java:164
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_SQRT
Z3_OP_FPA_SQRT
Definition: Z3_decl_kind.java:242
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_EQ
Z3_OP_EQ
Definition: Z3_decl_kind.java:16
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_IS_NEGATIVE
Z3_OP_FPA_IS_NEGATIVE
Definition: Z3_decl_kind.java:254
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SET_HAS_SIZE
Z3_OP_SET_HAS_SIZE
Definition: Z3_decl_kind.java:56
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION
Z3_OP_PR_UNIT_RESOLUTION
Definition: Z3_decl_kind.java:142
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_WIDEN
Z3_OP_RA_WIDEN
Definition: Z3_decl_kind.java:165
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_MONOTONICITY
Z3_OP_PR_MONOTONICITY
Definition: Z3_decl_kind.java:127
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_MINUS_ZERO
Z3_OP_FPA_MINUS_ZERO
Definition: Z3_decl_kind.java:231
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY
Z3_OP_PR_DISTRIBUTIVITY
Definition: Z3_decl_kind.java:130
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SEQ_LAST_INDEX
Z3_OP_SEQ_LAST_INDEX
Definition: Z3_decl_kind.java:187
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RE_INTERSECT
Z3_OP_RE_INTERSECT
Definition: Z3_decl_kind.java:199
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSMUL_NO_OVFL
Z3_OP_BSMUL_NO_OVFL
Definition: Z3_decl_kind.java:110
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_decl_kind
Z3_decl_kind(int v)
Definition: Z3_decl_kind.java:270
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSHL
Z3_OP_BSHL
Definition: Z3_decl_kind.java:98
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_EXTRACT
Z3_OP_EXTRACT
Definition: Z3_decl_kind.java:93
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_XOR3
Z3_OP_XOR3
Definition: Z3_decl_kind.java:109
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_IFF_FALSE
Z3_OP_PR_IFF_FALSE
Definition: Z3_decl_kind.java:144
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_STORE
Z3_OP_RA_STORE
Definition: Z3_decl_kind.java:160
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BADD
Z3_OP_BADD
Definition: Z3_decl_kind.java:62
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_REFLEXIVITY
Z3_OP_PR_REFLEXIVITY
Definition: Z3_decl_kind.java:123
com.microsoft.z3.enumerations.Z3_decl_kind.fromInt
static final Z3_decl_kind fromInt(int v)
Definition: Z3_decl_kind.java:284
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RE_PLUS
Z3_OP_RE_PLUS
Definition: Z3_decl_kind.java:192
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_FILTER
Z3_OP_RA_FILTER
Definition: Z3_decl_kind.java:167
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_REWRITE_STAR
Z3_OP_PR_REWRITE_STAR
Definition: Z3_decl_kind.java:134
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BOR
Z3_OP_BOR
Definition: Z3_decl_kind.java:84
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ANUM
Z3_OP_ANUM
Definition: Z3_decl_kind.java:26
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ULEQ
Z3_OP_ULEQ
Definition: Z3_decl_kind.java:75
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_UGEQ
Z3_OP_UGEQ
Definition: Z3_decl_kind.java:77
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_ABS
Z3_OP_FPA_ABS
Definition: Z3_decl_kind.java:238
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_BVWRAP
Z3_OP_FPA_BVWRAP
Definition: Z3_decl_kind.java:263
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSREM_I
Z3_OP_BSREM_I
Definition: Z3_decl_kind.java:115
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_DIV
Z3_OP_DIV
Definition: Z3_decl_kind.java:36
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY
Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY
Definition: Z3_decl_kind.java:222
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SGT
Z3_OP_SGT
Definition: Z3_decl_kind.java:82
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_DT_UPDATE_FIELD
Z3_OP_DT_UPDATE_FIELD
Definition: Z3_decl_kind.java:209
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SLT
Z3_OP_SLT
Definition: Z3_decl_kind.java:80
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_AND_ELIM
Z3_OP_PR_AND_ELIM
Definition: Z3_decl_kind.java:131
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_UMINUS
Z3_OP_UMINUS
Definition: Z3_decl_kind.java:34
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_REM
Z3_OP_FPA_REM
Definition: Z3_decl_kind.java:237
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PB_AT_LEAST
Z3_OP_PB_AT_LEAST
Definition: Z3_decl_kind.java:211
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT
Z3_OP_EXT_ROTATE_RIGHT
Definition: Z3_decl_kind.java:104
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BUREM0
Z3_OP_BUREM0
Definition: Z3_decl_kind.java:73
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE
Z3_OP_FPA_RM_TOWARD_POSITIVE
Definition: Z3_decl_kind.java:223
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SEQ_NTH
Z3_OP_SEQ_NTH
Definition: Z3_decl_kind.java:184
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_NAN
Z3_OP_FPA_NAN
Definition: Z3_decl_kind.java:229
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_TO_FP
Z3_OP_FPA_TO_FP
Definition: Z3_decl_kind.java:257
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_IS_POSITIVE
Z3_OP_FPA_IS_POSITIVE
Definition: Z3_decl_kind.java:255
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSDIV0
Z3_OP_BSDIV0
Definition: Z3_decl_kind.java:70
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_TO_INT
Z3_OP_TO_INT
Definition: Z3_decl_kind.java:41
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_IS_NAN
Z3_OP_FPA_IS_NAN
Definition: Z3_decl_kind.java:249
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_ASSUMPTION_ADD
Z3_OP_PR_ASSUMPTION_ADD
Definition: Z3_decl_kind.java:147
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_LABEL_LIT
Z3_OP_LABEL_LIT
Definition: Z3_decl_kind.java:204
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BNEG
Z3_OP_BNEG
Definition: Z3_decl_kind.java:61
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SEQ_TO_RE
Z3_OP_SEQ_TO_RE
Definition: Z3_decl_kind.java:188
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_AS_ARRAY
Z3_OP_AS_ARRAY
Definition: Z3_decl_kind.java:54
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FD_CONSTANT
Z3_OP_FD_CONSTANT
Definition: Z3_decl_kind.java:173
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SEQ_CONTAINS
Z3_OP_SEQ_CONTAINS
Definition: Z3_decl_kind.java:180
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SEQ_CONCAT
Z3_OP_SEQ_CONCAT
Definition: Z3_decl_kind.java:177
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_OEQ
Z3_OP_OEQ
Definition: Z3_decl_kind.java:25
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_SKOLEMIZE
Z3_OP_PR_SKOLEMIZE
Definition: Z3_decl_kind.java:156
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SPECIAL_RELATION_TRC
Z3_OP_SPECIAL_RELATION_TRC
Definition: Z3_decl_kind.java:220
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE
Z3_OP_FPA_RM_TOWARD_NEGATIVE
Definition: Z3_decl_kind.java:224
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_FMA
Z3_OP_FPA_FMA
Definition: Z3_decl_kind.java:241
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SUB
Z3_OP_SUB
Definition: Z3_decl_kind.java:33
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BMUL
Z3_OP_BMUL
Definition: Z3_decl_kind.java:64
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ROTATE_LEFT
Z3_OP_ROTATE_LEFT
Definition: Z3_decl_kind.java:101
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SGEQ
Z3_OP_SGEQ
Definition: Z3_decl_kind.java:78
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_TO_SBV
Z3_OP_FPA_TO_SBV
Definition: Z3_decl_kind.java:260
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SELECT
Z3_OP_SELECT
Definition: Z3_decl_kind.java:45
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SET_INTERSECT
Z3_OP_SET_INTERSECT
Definition: Z3_decl_kind.java:50
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BAND
Z3_OP_BAND
Definition: Z3_decl_kind.java:83
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_DER
Z3_OP_PR_DER
Definition: Z3_decl_kind.java:138
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_EQ
Z3_OP_FPA_EQ
Definition: Z3_decl_kind.java:244
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_UNDEF
Z3_OP_PR_UNDEF
Definition: Z3_decl_kind.java:118
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_APPLY_DEF
Z3_OP_PR_APPLY_DEF
Definition: Z3_decl_kind.java:152
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_PROJECT
Z3_OP_RA_PROJECT
Definition: Z3_decl_kind.java:166
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BUDIV
Z3_OP_BUDIV
Definition: Z3_decl_kind.java:66
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_ARRAY_DEFAULT
Z3_OP_ARRAY_DEFAULT
Definition: Z3_decl_kind.java:48
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SEQ_EMPTY
Z3_OP_SEQ_EMPTY
Definition: Z3_decl_kind.java:176
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_RA_EMPTY
Z3_OP_RA_EMPTY
Definition: Z3_decl_kind.java:161
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_QUANT_INTRO
Z3_OP_PR_QUANT_INTRO
Definition: Z3_decl_kind.java:128
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BSDIV
Z3_OP_BSDIV
Definition: Z3_decl_kind.java:65
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FD_LT
Z3_OP_FD_LT
Definition: Z3_decl_kind.java:174
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_DISTINCT
Z3_OP_DISTINCT
Definition: Z3_decl_kind.java:17
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SEQ_SUFFIX
Z3_OP_SEQ_SUFFIX
Definition: Z3_decl_kind.java:179
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_LEMMA_ADD
Z3_OP_PR_LEMMA_ADD
Definition: Z3_decl_kind.java:148
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_CLAUSE_TRAIL
Z3_OP_PR_CLAUSE_TRAIL
Definition: Z3_decl_kind.java:150
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_DT_ACCESSOR
Z3_OP_DT_ACCESSOR
Definition: Z3_decl_kind.java:208
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_AND
Z3_OP_AND
Definition: Z3_decl_kind.java:19
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_STORE
Z3_OP_STORE
Definition: Z3_decl_kind.java:44
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SET_CARD
Z3_OP_SET_CARD
Definition: Z3_decl_kind.java:57
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ
Z3_OP_PR_MODUS_PONENS_OEQ
Definition: Z3_decl_kind.java:157
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM
Z3_OP_PR_NOT_OR_ELIM
Definition: Z3_decl_kind.java:132
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_IS_NORMAL
Z3_OP_FPA_IS_NORMAL
Definition: Z3_decl_kind.java:252
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_ASSERTED
Z3_OP_PR_ASSERTED
Definition: Z3_decl_kind.java:120
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_BCOMP
Z3_OP_BCOMP
Definition: Z3_decl_kind.java:97
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_PR_LEMMA
Z3_OP_PR_LEMMA
Definition: Z3_decl_kind.java:141
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_GE
Z3_OP_GE
Definition: Z3_decl_kind.java:29
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FALSE
Z3_OP_FALSE
Definition: Z3_decl_kind.java:15
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_DIV
Z3_OP_FPA_DIV
Definition: Z3_decl_kind.java:236
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_FPA_MIN
Z3_OP_FPA_MIN
Definition: Z3_decl_kind.java:239
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_SEQ_INDEX
Z3_OP_SEQ_INDEX
Definition: Z3_decl_kind.java:186
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_XOR
Z3_OP_XOR
Definition: Z3_decl_kind.java:22
com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_IFF
Z3_OP_IFF
Definition: Z3_decl_kind.java:21