Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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),
56  Z3_OP_BNUM (1024),
57  Z3_OP_BIT1 (1025),
58  Z3_OP_BIT0 (1026),
59  Z3_OP_BNEG (1027),
60  Z3_OP_BADD (1028),
61  Z3_OP_BSUB (1029),
62  Z3_OP_BMUL (1030),
63  Z3_OP_BSDIV (1031),
64  Z3_OP_BUDIV (1032),
65  Z3_OP_BSREM (1033),
66  Z3_OP_BUREM (1034),
67  Z3_OP_BSMOD (1035),
68  Z3_OP_BSDIV0 (1036),
69  Z3_OP_BUDIV0 (1037),
70  Z3_OP_BSREM0 (1038),
71  Z3_OP_BUREM0 (1039),
72  Z3_OP_BSMOD0 (1040),
73  Z3_OP_ULEQ (1041),
74  Z3_OP_SLEQ (1042),
75  Z3_OP_UGEQ (1043),
76  Z3_OP_SGEQ (1044),
77  Z3_OP_ULT (1045),
78  Z3_OP_SLT (1046),
79  Z3_OP_UGT (1047),
80  Z3_OP_SGT (1048),
81  Z3_OP_BAND (1049),
82  Z3_OP_BOR (1050),
83  Z3_OP_BNOT (1051),
84  Z3_OP_BXOR (1052),
85  Z3_OP_BNAND (1053),
86  Z3_OP_BNOR (1054),
87  Z3_OP_BXNOR (1055),
88  Z3_OP_CONCAT (1056),
91  Z3_OP_EXTRACT (1059),
92  Z3_OP_REPEAT (1060),
93  Z3_OP_BREDOR (1061),
94  Z3_OP_BREDAND (1062),
95  Z3_OP_BCOMP (1063),
96  Z3_OP_BSHL (1064),
97  Z3_OP_BLSHR (1065),
98  Z3_OP_BASHR (1066),
104  Z3_OP_INT2BV (1072),
105  Z3_OP_BV2INT (1073),
106  Z3_OP_CARRY (1074),
107  Z3_OP_XOR3 (1075),
136  Z3_OP_PR_DER (1300),
172  Z3_OP_FD_LT (1550),
181  Z3_OP_SEQ_AT (1559),
201  Z3_OP_LABEL (1792),
205  Z3_OP_DT_IS (2050),
210  Z3_OP_PB_LE (2306),
211  Z3_OP_PB_GE (2307),
212  Z3_OP_PB_EQ (2308),
224  Z3_OP_FPA_NUM (45061),
227  Z3_OP_FPA_NAN (45064),
230  Z3_OP_FPA_ADD (45067),
231  Z3_OP_FPA_SUB (45068),
232  Z3_OP_FPA_NEG (45069),
233  Z3_OP_FPA_MUL (45070),
234  Z3_OP_FPA_DIV (45071),
235  Z3_OP_FPA_REM (45072),
236  Z3_OP_FPA_ABS (45073),
237  Z3_OP_FPA_MIN (45074),
238  Z3_OP_FPA_MAX (45075),
239  Z3_OP_FPA_FMA (45076),
240  Z3_OP_FPA_SQRT (45077),
242  Z3_OP_FPA_EQ (45079),
243  Z3_OP_FPA_LT (45080),
244  Z3_OP_FPA_GT (45081),
245  Z3_OP_FPA_LE (45082),
246  Z3_OP_FPA_GE (45083),
254  Z3_OP_FPA_FP (45091),
263  Z3_OP_INTERNAL (45100),
265 
266  private final int intValue;
267 
268  Z3_decl_kind(int v) {
269  this.intValue = v;
270  }
271 
272  // Cannot initialize map in constructor, so need to do it lazily.
273  // Easiest thread-safe way is the initialization-on-demand holder pattern.
274  private static class Z3_decl_kind_MappingHolder {
275  private static final Map<Integer, Z3_decl_kind> intMapping = new HashMap<>();
276  static {
277  for (Z3_decl_kind k : Z3_decl_kind.values())
278  intMapping.put(k.toInt(), k);
279  }
280  }
281 
282  public static final Z3_decl_kind fromInt(int v) {
283  Z3_decl_kind k = Z3_decl_kind_MappingHolder.intMapping.get(v);
284  if (k != null) return k;
285  throw new IllegalArgumentException("Illegal value " + v + " for Z3_decl_kind");
286  }
287 
288  public final int toInt() { return this.intValue; }
289 }
290 
static final Z3_decl_kind fromInt(int v)