Z3
Public Member Functions | Protected Member Functions
Symbol Class Reference
+ Inheritance diagram for Symbol:

Public Member Functions

boolean isIntSymbol ()
 
boolean isStringSymbol ()
 
boolean equals (Object o)
 
String toString ()
 
- Public Member Functions inherited from Z3Object
void dispose ()
 
- Public Member Functions inherited from IDisposable
void dispose ()
 

Protected Member Functions

Z3_symbol_kind getKind ()
 
 Symbol (Context ctx, long obj)
 
- Protected Member Functions inherited from Z3Object
void finalize ()
 

Detailed Description

Symbols are used to name several term and type constructors.

Definition at line 25 of file Symbol.java.

Constructor & Destructor Documentation

Symbol ( Context  ctx,
long  obj 
)
inlineprotected

Symbol constructor

Definition at line 88 of file Symbol.java.

89  {
90  super(ctx, obj);
91  }

Member Function Documentation

boolean equals ( Object  o)
inline

Definition at line 52 of file Symbol.java.

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  }
Symbol(Context ctx, long obj)
Definition: Symbol.java:88
Z3_symbol_kind getKind ( )
inlineprotected

The kind of the symbol (int or string)

Definition at line 30 of file Symbol.java.

Referenced by Symbol.isIntSymbol(), and Symbol.isStringSymbol().

31  {
32  return Z3_symbol_kind.fromInt(Native.getSymbolKind(getContext().nCtx(),
33  getNativeObject()));
34  }
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:158
boolean isIntSymbol ( )
inline

Indicates whether the symbol is of Int kind

Definition at line 39 of file Symbol.java.

Referenced by IntSymbol.getInt(), and Symbol.toString().

40  {
42  }
Z3_symbol_kind getKind()
Definition: Symbol.java:30
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:158
boolean isStringSymbol ( )
inline

Indicates whether the symbol is of string kind.

Definition at line 47 of file Symbol.java.

Referenced by Symbol.toString().

48  {
50  }
Z3_symbol_kind getKind()
Definition: Symbol.java:30
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:158
String toString ( )
inline

A string representation of the symbol.

Definition at line 68 of file Symbol.java.

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  }
boolean isStringSymbol()
Definition: Symbol.java:47
boolean isIntSymbol()
Definition: Symbol.java:39