Z3
src
api
java
enumerations
Z3_goal_prec.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_goal_prec
{
14
Z3_GOAL_PRECISE
(0),
15
Z3_GOAL_UNDER
(1),
16
Z3_GOAL_OVER
(2),
17
Z3_GOAL_UNDER_OVER
(3);
18
19
private
final
int
intValue;
20
21
Z3_goal_prec
(
int
v) {
22
this.intValue = v;
23
}
24
25
// Cannot initialize map in constructor, so need to do it lazily.
26
// Easiest thread-safe way is the initialization-on-demand holder pattern.
27
private
static
class
Z3_goal_prec_MappingHolder {
28
private
static
final
Map<Integer, Z3_goal_prec> intMapping =
new
HashMap<>();
29
static
{
30
for
(
Z3_goal_prec
k :
Z3_goal_prec
.values())
31
intMapping.put(k.toInt(), k);
32
}
33
}
34
35
public
static
final
Z3_goal_prec
fromInt
(
int
v) {
36
Z3_goal_prec
k = Z3_goal_prec_MappingHolder.intMapping.get(v);
37
if
(k != null)
return
k;
38
throw
new
IllegalArgumentException(
"Illegal value "
+ v +
" for Z3_goal_prec"
);
39
}
40
41
public
final
int
toInt
() {
return
this.intValue; }
42
}
43
com.microsoft.z3.enumerations.Z3_goal_prec.Z3_GOAL_UNDER_OVER
Z3_GOAL_UNDER_OVER
Definition:
Z3_goal_prec.java:17
com.microsoft.z3.enumerations.Z3_goal_prec.toInt
final int toInt()
Definition:
Z3_goal_prec.java:41
com.microsoft.z3.enumerations.Z3_goal_prec
Definition:
Z3_goal_prec.java:13
com.microsoft.z3.enumerations.Z3_goal_prec.Z3_GOAL_PRECISE
Z3_GOAL_PRECISE
Definition:
Z3_goal_prec.java:14
com.microsoft.z3.enumerations.Z3_goal_prec.fromInt
static final Z3_goal_prec fromInt(int v)
Definition:
Z3_goal_prec.java:35
com.microsoft.z3.enumerations.Z3_goal_prec.Z3_goal_prec
Z3_goal_prec(int v)
Definition:
Z3_goal_prec.java:21
com.microsoft.z3.enumerations.Z3_goal_prec.Z3_GOAL_OVER
Z3_GOAL_OVER
Definition:
Z3_goal_prec.java:16
com.microsoft.z3.enumerations.Z3_goal_prec.Z3_GOAL_UNDER
Z3_GOAL_UNDER
Definition:
Z3_goal_prec.java:15
Generated on Sat Nov 12 2016 22:01:04 for Z3 by
1.8.12