Z3
src
api
java
IntSymbol.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
IntSymbol
extends
Symbol
26
{
31
public
int
getInt
() throws
Z3Exception
32
{
33
if
(!
isIntSymbol
())
34
throw
new
Z3Exception(
"Int requested from non-Int symbol"
);
35
return
Native
.
getSymbolInt
(getContext().nCtx(), getNativeObject());
36
}
37
38
IntSymbol
(
Context
ctx,
long
obj)
throws
Z3Exception
39
{
40
super(ctx, obj);
41
}
42
43
IntSymbol(Context ctx,
int
i)
throws
Z3Exception
44
{
45
super(ctx, Native.mkIntSymbol(ctx.nCtx(), i));
46
}
47
48
void
checkNativeObject(
long
obj)
throws
Z3Exception
49
{
50
if
(Native.getSymbolKind(getContext().nCtx(), obj) !=
Z3_symbol_kind
.Z3_INT_SYMBOL
51
.toInt())
52
throw
new
Z3Exception(
"Symbol is not of integer kind"
);
53
super.checkNativeObject(obj);
54
}
55
}
com.microsoft
com
com.microsoft.z3.Symbol
Definition:
Symbol.java:25
com.microsoft.z3.Context
Definition:
Context.java:27
com.microsoft.z3.Native
Definition:
Native.java:4
com.microsoft.z3
Definition:
AlgebraicNum.java:18
com.microsoft.z3.IntSymbol.getInt
int getInt()
Definition:
IntSymbol.java:31
com.microsoft.z3.enumerations.Z3_symbol_kind
Definition:
Z3_symbol_kind.java:10
Z3_symbol_kind
Z3_symbol_kind
The different kinds of symbol. In Z3, a symbol can be represented using integers and strings (See Z3_...
Definition:
z3_api.h:150
com.microsoft.z3.Native.getSymbolInt
static int getSymbolInt(long a0, long a1)
Definition:
Native.java:1940
com.microsoft.z3.IntSymbol
Definition:
IntSymbol.java:25
com.microsoft.z3.Symbol.isIntSymbol
boolean isIntSymbol()
Definition:
Symbol.java:39
com.microsoft.z3.Z3Exception
Definition:
Z3Exception.java:25
com.microsoft.z3.enumerations
Definition:
Z3_ast_kind.java:5
Generated on Sat Apr 25 2015 18:37:50 for Z3 by
1.8.9.1