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

Public Member Functions

boolean isIntSymbol () throws Z3Exception
 
boolean isStringSymbol () throws Z3Exception
 
String toString ()
 
- Public Member Functions inherited from Z3Object
void dispose () throws Z3Exception
 
- Public Member Functions inherited from IDisposable
void dispose () throws Z3Exception
 

Protected Member Functions

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

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 
) throws Z3Exception
inlineprotected

Symbol constructor

Definition at line 75 of file Symbol.java.

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

Member Function Documentation

Z3_symbol_kind getKind ( ) throws Z3Exception
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 ( ) throws Z3Exception
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 ( ) throws Z3Exception
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