Z3
Symbol.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
21 
25 public class Symbol extends Z3Object {
29  protected Z3_symbol_kind getKind()
30  {
31  return Z3_symbol_kind.fromInt(Native.getSymbolKind(getContext().nCtx(),
32  getNativeObject()));
33  }
34 
38  public boolean isIntSymbol()
39  {
41  }
42 
46  public boolean isStringSymbol()
47  {
49  }
50 
51  @Override
52  public boolean equals(Object o)
53  {
54  if (o == this) return true;
55  if (!(o instanceof Symbol)) return false;
56  Symbol other = (Symbol) o;
57  return this.getNativeObject() == other.getNativeObject();
58  }
59 
63  @Override
64  public String toString() {
65  if (isIntSymbol()) {
66  return Integer.toString(((IntSymbol) this).getInt());
67  } else if (isStringSymbol()) {
68  return ((StringSymbol) this).getString();
69  } else {
70  return "Z3Exception: Unknown symbol kind encountered.";
71  }
72  }
73 
77  protected Symbol(Context ctx, long obj)
78  {
79  super(ctx, obj);
80  }
81 
82  @Override
83  void incRef() {
84  // Symbol does not require tracking.
85  }
86 
87  @Override
88  void addToReferenceQueue() {
89 
90  // Symbol does not require tracking.
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:77
static final Z3_symbol_kind fromInt(int v)
boolean equals(Object o)
Definition: Symbol.java:52
Z3_symbol_kind getKind()
Definition: Symbol.java:29
boolean isStringSymbol()
Definition: Symbol.java:46
boolean isIntSymbol()
Definition: Symbol.java:38
static int getSymbolKind(long a0, long a1)
Definition: Native.java:2285
def String(name, ctx=None)
Definition: z3py.py:9443