Z3
src
api
java
StringSymbol.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
StringSymbol
extends
Symbol
26
{
32
public
String
getString
()
33
{
34
return
Native
.
getSymbolString
(getContext().nCtx(), getNativeObject());
35
}
36
37
StringSymbol
(
Context
ctx,
long
obj)
38
{
39
super(ctx, obj);
40
}
41
42
StringSymbol
(
Context
ctx, String s)
43
{
44
super(ctx,
Native
.
mkStringSymbol
(ctx.nCtx(), s));
45
}
46
47
void
checkNativeObject(
long
obj)
48
{
49
if
(
Native
.
getSymbolKind
(getContext().nCtx(), obj) !=
Z3_symbol_kind
.
Z3_STRING_SYMBOL
50
.toInt())
51
throw
new
Z3Exception
(
"Symbol is not of String kind"
);
52
53
super.checkNativeObject(obj);
54
}
55
}
com.microsoft.z3.StringSymbol
Definition:
StringSymbol.java:25
com.microsoft.z3.Native.getSymbolString
static String getSymbolString(long a0, long a1)
Definition:
Native.java:2045
com.microsoft
com
com.microsoft.z3.StringSymbol.getString
String getString()
Definition:
StringSymbol.java:32
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.Native.mkStringSymbol
static long mkStringSymbol(long a0, String a1)
Definition:
Native.java:870
com.microsoft.z3.Native
Definition:
Native.java:4
com.microsoft.z3
Definition:
AlgebraicNum.java:18
com.microsoft.z3.enumerations.Z3_symbol_kind
Definition:
Z3_symbol_kind.java:10
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
Generated on Tue Jul 19 2016 21:26:49 for Z3 by
1.8.11