Z3
Symbol.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
21 
25 public class Symbol extends Z3Object
26 {
30  protected Z3_symbol_kind getKind()
31  {
32  return Z3_symbol_kind.fromInt(Native.getSymbolKind(getContext().nCtx(),
33  getNativeObject()));
34  }
35 
39  public boolean isIntSymbol()
40  {
42  }
43 
47  public boolean isStringSymbol()
48  {
50  }
51 
55  public String toString()
56  {
57  try
58  {
59  if (isIntSymbol())
60  return Integer.toString(((IntSymbol) this).getInt());
61  else if (isStringSymbol())
62  return ((StringSymbol) this).getString();
63  else
64  return new String(
65  "Z3Exception: Unknown symbol kind encountered.");
66  } catch (Z3Exception ex)
67  {
68  return new String("Z3Exception: " + ex.getMessage());
69  }
70  }
71 
75  protected Symbol(Context ctx, long obj)
76  {
77  super(ctx, obj);
78  }
79 
80  static Symbol create(Context ctx, long obj)
81  {
82  switch (Z3_symbol_kind.fromInt(Native.getSymbolKind(ctx.nCtx(), obj)))
83  {
84  case Z3_INT_SYMBOL:
85  return new IntSymbol(ctx, obj);
86  case Z3_STRING_SYMBOL:
87  return new StringSymbol(ctx, obj);
88  default:
89  throw new Z3Exception("Unknown symbol kind encountered");
90  }
91  }
92 }
Symbol(Context ctx, long obj)
Definition: Symbol.java:75
static final Z3_symbol_kind fromInt(int v)
Z3_symbol_kind getKind()
Definition: Symbol.java:30
boolean isStringSymbol()
Definition: Symbol.java:47
boolean isIntSymbol()
Definition: Symbol.java:39
static int getSymbolKind(long a0, long a1)
Definition: Native.java:2000