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
{
32
public
int
getInt
()
33
{
34
if
(!
isIntSymbol
())
35
throw
new
Z3Exception
(
"Int requested from non-Int symbol"
);
36
return
Native
.
getSymbolInt
(getContext().nCtx(), getNativeObject());
37
}
38
39
IntSymbol
(
Context
ctx,
long
obj)
40
{
41
super(ctx, obj);
42
}
43
44
IntSymbol
(
Context
ctx,
int
i)
45
{
46
super(ctx,
Native
.
mkIntSymbol
(ctx.nCtx(), i));
47
}
48
49
void
checkNativeObject(
long
obj)
50
{
51
if
(
Native
.
getSymbolKind
(getContext().nCtx(), obj) !=
Z3_symbol_kind
.
Z3_INT_SYMBOL
52
.toInt())
53
throw
new
Z3Exception
(
"Symbol is not of integer kind"
);
54
super.checkNativeObject(obj);
55
}
56
}
com.microsoft.z3.enumerations.Z3_symbol_kind.Z3_INT_SYMBOL
Z3_INT_SYMBOL
Definition:
Z3_symbol_kind.java:11
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:32
com.microsoft.z3.enumerations.Z3_symbol_kind
Definition:
Z3_symbol_kind.java:10
com.microsoft.z3.Native.getSymbolInt
static int getSymbolInt(long a0, long a1)
Definition:
Native.java:2036
com.microsoft.z3.IntSymbol
Definition:
IntSymbol.java:25
com.microsoft.z3.Symbol.isIntSymbol
boolean isIntSymbol()
Definition:
Symbol.java:39
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.Native.mkIntSymbol
static long mkIntSymbol(long a0, int a1)
Definition:
Native.java:861
com.microsoft.z3.enumerations
Definition:
Z3_ast_kind.java:5
Generated on Tue Jul 19 2016 21:26:48 for Z3 by
1.8.11