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 ()

## Protected Member Functions
Z3_symbol_kind | getKind ()
| Symbol (Context ctx, long obj)

## Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[] | arrayToNative (Z3Object[] a)
static int | arrayLength (Z3Object[] a)

## Detailed Description

Symbols are used to name several term and type constructors.

Definition at line 25 of file Symbol.java.

## Constructor & Destructor Documentation

## ◆ Symbol()

Symbol | ( | Context | ctx,
|  | long | obj
| ) |  |
| inline protected

Symbol constructor

Definition at line 77 of file Symbol.java.

78 {
79 super(ctx, obj);
80 }

Referenced by Symbol.equals().

## Member Function Documentation

## ◆ equals()

boolean equals | ( | Object | o | ) |
| inline

Definition at line 52 of file Symbol.java.

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 }
com.microsoft.z3.Symbol.Symbol
Symbol(Context ctx, long obj)
Definition: Symbol.java:77

## ◆ getKind()

Z3_symbol_kind getKind | ( |  | ) |
| inline protected

The kind of the symbol (int or string)

Definition at line 29 of file Symbol.java.

30 {
31 return Z3_symbol_kind.fromInt(Native.getSymbolKind(getContext().nCtx(),
32 getNativeObject()));
33 }
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:116

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

## ◆ isIntSymbol()

boolean isIntSymbol | ( |  | ) |
| inline

Indicates whether the symbol is of Int kind

Definition at line 38 of file Symbol.java.

39 {
40 return getKind() == Z3_symbol_kind.Z3_INT_SYMBOL;
41 }
com.microsoft.z3.Symbol.getKind
Z3_symbol_kind getKind()
Definition: Symbol.java:29

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

## ◆ isStringSymbol()

boolean isStringSymbol | ( |  | ) |
| inline

Indicates whether the symbol is of string kind.

Definition at line 46 of file Symbol.java.

47 {
48 return getKind() == Z3_symbol_kind.Z3_STRING_SYMBOL;
49 }

Referenced by Symbol.toString().

## ◆ toString()

String toString | ( |  | ) |
| inline

A string representation of the symbol.

Definition at line 64 of file Symbol.java.

64 {
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 }
com.microsoft.z3.Symbol.isStringSymbol
boolean isStringSymbol()
Definition: Symbol.java:46
com.microsoft.z3.Symbol.isIntSymbol
boolean isIntSymbol()
Definition: Symbol.java:38