Z3
IntSymbol.java
Go to the documentation of this file.
1
18package com.microsoft.z3;
19
20import com.microsoft.z3.enumerations.Z3_symbol_kind;
21
25public 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 @Override
50 void checkNativeObject(long obj)
51 {
52 if (Native.getSymbolKind(getContext().nCtx(), obj) != Z3_symbol_kind.Z3_INT_SYMBOL
53 .toInt())
54 throw new Z3Exception("Symbol is not of integer kind");
55 super.checkNativeObject(obj);
56 }
57}
boolean isIntSymbol()
Definition: Symbol.java:38
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:116