Z3 |

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 @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}
com.microsoft.z3.Context
Definition: Context.java:36
com.microsoft.z3.IntSymbol
Definition: IntSymbol.java:26
com.microsoft.z3.IntSymbol.getInt
int getInt()
Definition: IntSymbol.java:32
com.microsoft.z3.Symbol
Definition: Symbol.java:25
com.microsoft.z3.Symbol.isIntSymbol
boolean isIntSymbol()
Definition: Symbol.java:38
com.microsoft.z3.Z3Exception
Definition: Z3Exception.java:26
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:116