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

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  }

◆ getKind()

Z3_symbol_kind getKind ( )
inlineprotected

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  }

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  }

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.getKind
Z3_symbol_kind getKind()
Definition: Symbol.java:29
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:115
com.microsoft.z3.Symbol.Symbol
Symbol(Context ctx, long obj)
Definition: Symbol.java:77
com.microsoft.z3.Symbol.isIntSymbol
boolean isIntSymbol()
Definition: Symbol.java:38