Z3
src
api
java
Symbol.java
Go to the documentation of this file.
1
18
package
com.microsoft.z3;
19
20
import
com
.
microsoft
.
z3
.
enumerations
.
Z3_symbol_kind
;
21
25
public
class
Symbol
extends
Z3Object
26
{
30
protected
Z3_symbol_kind
getKind
()
31
{
32
return
Z3_symbol_kind
.
fromInt
(
Native
.
getSymbolKind
(getContext().nCtx(),
33
getNativeObject()));
34
}
35
39
public
boolean
isIntSymbol
()
40
{
41
return
getKind
() ==
Z3_symbol_kind
.
Z3_INT_SYMBOL
;
42
}
43
47
public
boolean
isStringSymbol
()
48
{
49
return
getKind
() ==
Z3_symbol_kind
.
Z3_STRING_SYMBOL
;
50
}
51
52
public
boolean
equals
(Object o)
53
{
54
Symbol
casted = null;
55
try
{
56
casted =
Symbol
.class.cast(o);
57
}
58
catch
(ClassCastException e) {
59
return
false
;
60
}
61
62
return
this.getNativeObject() == casted.getNativeObject();
63
}
64
68
public
String
toString
()
69
{
70
try
71
{
72
if
(
isIntSymbol
())
73
return
Integer.toString(((
IntSymbol
)
this
).getInt());
74
else
if
(
isStringSymbol
())
75
return
((
StringSymbol
)
this
).getString();
76
else
77
return
new
String(
78
"Z3Exception: Unknown symbol kind encountered."
);
79
}
catch
(
Z3Exception
ex)
80
{
81
return
new
String(
"Z3Exception: "
+ ex.getMessage());
82
}
83
}
84
88
protected
Symbol
(
Context
ctx,
long
obj)
89
{
90
super(ctx, obj);
91
}
92
93
static
Symbol
create(
Context
ctx,
long
obj)
94
{
95
switch
(
Z3_symbol_kind
.
fromInt
(
Native
.
getSymbolKind
(ctx.nCtx(), obj)))
96
{
97
case
Z3_INT_SYMBOL
:
98
return
new
IntSymbol
(ctx, obj);
99
case
Z3_STRING_SYMBOL
:
100
return
new
StringSymbol
(ctx, obj);
101
default
:
102
throw
new
Z3Exception
(
"Unknown symbol kind encountered"
);
103
}
104
}
105
}
com.microsoft.z3.enumerations.Z3_symbol_kind.Z3_INT_SYMBOL
Z3_INT_SYMBOL
Definition:
Z3_symbol_kind.java:11
com.microsoft.z3.StringSymbol
Definition:
StringSymbol.java:25
com.microsoft.z3.Symbol.Symbol
Symbol(Context ctx, long obj)
Definition:
Symbol.java:88
com.microsoft
com
com.microsoft.z3.Symbol
Definition:
Symbol.java:25
com.microsoft.z3.enumerations.Z3_symbol_kind.Z3_STRING_SYMBOL
Z3_STRING_SYMBOL
Definition:
Z3_symbol_kind.java:12
com.microsoft.z3.Context
Definition:
Context.java:27
com.microsoft.z3.enumerations.Z3_symbol_kind.fromInt
static final Z3_symbol_kind fromInt(int v)
Definition:
Z3_symbol_kind.java:20
com.microsoft.z3.Native
Definition:
Native.java:4
com.microsoft.z3
Definition:
AlgebraicNum.java:18
com.microsoft.z3.Symbol.equals
boolean equals(Object o)
Definition:
Symbol.java:52
com.microsoft.z3.Symbol.getKind
Z3_symbol_kind getKind()
Definition:
Symbol.java:30
com.microsoft.z3.enumerations.Z3_symbol_kind
Definition:
Z3_symbol_kind.java:10
com.microsoft.z3.IntSymbol
Definition:
IntSymbol.java:25
com.microsoft.z3.Symbol.isStringSymbol
boolean isStringSymbol()
Definition:
Symbol.java:47
com.microsoft.z3.Symbol.isIntSymbol
boolean isIntSymbol()
Definition:
Symbol.java:39
com.microsoft.z3.Z3Object
Definition:
Z3Object.java:24
com.microsoft.z3.Native.getSymbolKind
static int getSymbolKind(long a0, long a1)
Definition:
Native.java:2027
com.microsoft.z3.Z3Exception
Definition:
Z3Exception.java:25
com.microsoft.z3.enumerations
Definition:
Z3_ast_kind.java:5
Z3_STRING_SYMBOL
Definition:
z3_api.h:161
com.microsoft.z3.Symbol.toString
String toString()
Definition:
Symbol.java:68
Z3_INT_SYMBOL
Definition:
z3_api.h:160
Generated on Tue Jul 19 2016 21:26:49 for Z3 by
1.8.11