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
{
29
protected
Z3_symbol_kind
getKind
()
30
{
31
return
Z3_symbol_kind
.
fromInt
(
Native
.
getSymbolKind
(getContext().nCtx(),
32
getNativeObject()));
33
}
34
38
public
boolean
isIntSymbol
()
39
{
40
return
getKind
() ==
Z3_symbol_kind
.
Z3_INT_SYMBOL
;
41
}
42
46
public
boolean
isStringSymbol
()
47
{
48
return
getKind
() ==
Z3_symbol_kind
.
Z3_STRING_SYMBOL
;
49
}
50
51
@Override
52
public
boolean
equals
(Object o)
53
{
54
if
(o ==
this
)
return
true
;
55
if
(!(o instanceof
Symbol
))
return
false
;
56
Symbol other = (
Symbol
) o;
57
return
this.getNativeObject() == other.getNativeObject();
58
}
59
63
@Override
64
public
String
toString
() {
65
if
(
isIntSymbol
()) {
66
return
Integer.toString(((
IntSymbol
)
this
).getInt());
67
}
else
if
(
isStringSymbol
()) {
68
return
((
StringSymbol
)
this
).getString();
69
}
else
{
70
return
"Z3Exception: Unknown symbol kind encountered."
;
71
}
72
}
73
77
protected
Symbol
(
Context
ctx,
long
obj)
78
{
79
super(ctx, obj);
80
}
81
82
@Override
83
void
incRef() {
84
// Symbol does not require tracking.
85
}
86
87
@Override
88
void
addToReferenceQueue() {
89
90
// Symbol does not require tracking.
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:14
com.microsoft.z3.StringSymbol
Definition:
StringSymbol.java:25
com.microsoft.z3.Symbol.Symbol
Symbol(Context ctx, long obj)
Definition:
Symbol.java:77
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:15
com.microsoft.z3.Context
Definition:
Context.java:29
com.microsoft.z3.enumerations.Z3_symbol_kind.fromInt
static final Z3_symbol_kind fromInt(int v)
Definition:
Z3_symbol_kind.java:33
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:29
com.microsoft.z3.enumerations.Z3_symbol_kind
Definition:
Z3_symbol_kind.java:13
com.microsoft.z3.IntSymbol
Definition:
IntSymbol.java:25
com.microsoft.z3.Symbol.isStringSymbol
boolean isStringSymbol()
Definition:
Symbol.java:46
com.microsoft.z3.Symbol.isIntSymbol
boolean isIntSymbol()
Definition:
Symbol.java:38
com.microsoft.z3.Z3Object
Definition:
Z3Object.java:24
com.microsoft.z3.Native.getSymbolKind
static int getSymbolKind(long a0, long a1)
Definition:
Native.java:2285
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:122
com.microsoft.z3.Symbol.toString
String toString()
Definition:
Symbol.java:64
Z3_INT_SYMBOL
Definition:
z3_api.h:121
z3py.String
def String(name, ctx=None)
Definition:
z3py.py:9443
Generated on Sat Nov 12 2016 23:18:41 for Z3 by
1.8.12