Z3
IntSymbol.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
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 }
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
static int getSymbolInt(long a0, long a1)
Definition: Native.java:1940
boolean isIntSymbol()
Definition: Symbol.java:39