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

Public Member Functions

boolean isIntSymbol ()
 
boolean isStringSymbol ()
 
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 75 of file Symbol.java.

76  {
77  super(ctx, obj);
78  }

Member Function Documentation

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:150
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:150
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:150
String toString ( )
inline

A string representation of the symbol.

Definition at line 55 of file Symbol.java.

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