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 
52  public boolean equals(Object o)
53  {
54  Symbol casted = null;
55  try {
56  casted = Symbol.class.cast(o);
57  }
58  catch (ClassCastException e) {
59  return false;
60  }
61 
62  return this.getNativeObject() == casted.getNativeObject();
63  }
64 
68  public String toString()
69  {
70  try
71  {
72  if (isIntSymbol())
73  return Integer.toString(((IntSymbol) this).getInt());
74  else if (isStringSymbol())
75  return ((StringSymbol) this).getString();
76  else
77  return new String(
78  "Z3Exception: Unknown symbol kind encountered.");
79  } catch (Z3Exception ex)
80  {
81  return new String("Z3Exception: " + ex.getMessage());
82  }
83  }
84 
88  protected Symbol(Context ctx, long obj)
89  {
90  super(ctx, obj);
91  }
92 
93  static Symbol create(Context ctx, long obj)
94  {
95  switch (Z3_symbol_kind.fromInt(Native.getSymbolKind(ctx.nCtx(), obj)))
96  {
97  case Z3_INT_SYMBOL:
98  return new IntSymbol(ctx, obj);
99  case Z3_STRING_SYMBOL:
100  return new StringSymbol(ctx, obj);
101  default:
102  throw new Z3Exception("Unknown symbol kind encountered");
103  }
104  }
105 }
Symbol(Context ctx, long obj)
Definition: Symbol.java:88
static final Z3_symbol_kind fromInt(int v)
boolean equals(Object o)
Definition: Symbol.java:52
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:2027