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 }
com.microsoft.z3.Symbol.isStringSymbol
boolean isStringSymbol()
Definition: Symbol.java:46
com.microsoft.z3.enumerations
Definition: Z3_ast_kind.java:5
com.microsoft.z3.enumerations.Z3_symbol_kind.fromInt
static final Z3_symbol_kind fromInt(int v)
Definition: Z3_symbol_kind.java:33
com.microsoft
com.microsoft.z3.Symbol.getKind
Z3_symbol_kind getKind()
Definition: Symbol.java:29
com.microsoft.z3.Symbol.toString
String toString()
Definition: Symbol.java:64
com.microsoft.z3.Symbol.equals
boolean equals(Object o)
Definition: Symbol.java:52
com.microsoft.z3.Symbol
Definition: Symbol.java:25
Z3_INT_SYMBOL
@ Z3_INT_SYMBOL
Definition: z3_api.h:115
com.microsoft.z3.StringSymbol
Definition: StringSymbol.java:25
com.microsoft.z3.IntSymbol
Definition: IntSymbol.java:25
com.microsoft.z3.Native
Definition: Native.java:4
com.microsoft.z3
Definition: AlgebraicNum.java:18
com.microsoft.z3.enumerations.Z3_symbol_kind.Z3_INT_SYMBOL
Z3_INT_SYMBOL
Definition: Z3_symbol_kind.java:14
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:113
com.microsoft.z3.enumerations.Z3_symbol_kind
Definition: Z3_symbol_kind.java:13
com.microsoft.z3.Native.getSymbolKind
static int getSymbolKind(long a0, long a1)
Definition: Native.java:2632
com
com.microsoft.z3.enumerations.Z3_symbol_kind.Z3_STRING_SYMBOL
Z3_STRING_SYMBOL
Definition: Z3_symbol_kind.java:15
com.microsoft.z3.Context
Definition: Context.java:35
com.microsoft.z3.Symbol.Symbol
Symbol(Context ctx, long obj)
Definition: Symbol.java:77
com.microsoft.z3.Z3Object
Definition: Z3Object.java:24
com.microsoft.z3.Symbol.isIntSymbol
boolean isIntSymbol()
Definition: Symbol.java:38
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10111
Z3_STRING_SYMBOL
@ Z3_STRING_SYMBOL
Definition: z3_api.h:116