Z3 |

Public Member Functions | Friends
symbol Class Reference

`#include <z3++.h>`

Inheritance diagram for symbol:

## Public Member Functions
| symbol (context &c, Z3_symbol s)
| operator Z3_symbol () const
Z3_symbol_kind | kind () const
std::string | str () const
int | to_int () const
Public Member Functions inherited from object
| object (context &c)
context & | ctx () const
Z3_error_code | check_error () const

## Friends
std::ostream & | operator<< (std::ostream &out, symbol const &s)

## Additional Inherited Members
Protected Attributes inherited from object
context * | m_ctx

## Detailed Description

Definition at line 428 of file z3++.h.

## Constructor & Destructor Documentation

## ◆ symbol()

symbol | ( | context & | c,
|  | Z3_symbol | s
| ) |  |
| inline

Definition at line 431 of file z3++.h.

431:object(c), m_sym(s) {}
z3::object::object
object(context &c)
Definition: z3++.h:421

## Member Function Documentation

## ◆ kind()

Z3_symbol_kind kind | ( |  | ) | const
| inline

Definition at line 433 of file z3++.h.

433{ return Z3_get_symbol_kind(ctx(), m_sym); }
z3::object::ctx
context & ctx() const
Definition: z3++.h:422
Z3_get_symbol_kind
Z3_symbol_kind Z3_API Z3_get_symbol_kind(Z3_context c, Z3_symbol s)
Return Z3_INT_SYMBOL if the symbol was constructed using Z3_mk_int_symbol, and Z3_STRING_SYMBOL if th...

Referenced by ArithSortRef::is_int(), ArithSortRef::is_real(), symbol::str(), and symbol::to_int().

## ◆ operator Z3_symbol()

operator Z3_symbol | ( |  | ) | const
| inline

Definition at line 432 of file z3++.h.

432{ return m_sym; }

## ◆ str()

std::string str | ( |  | ) | const
| inline

Definition at line 434 of file z3++.h.

434{ assert(kind() == Z3_STRING_SYMBOL); return Z3_get_symbol_string(ctx(), m_sym); }
z3::symbol::kind
Z3_symbol_kind kind() const
Definition: z3++.h:433
Z3_get_symbol_string
Z3_string Z3_API Z3_get_symbol_string(Z3_context c, Z3_symbol s)
Return the symbol name.
Z3_STRING_SYMBOL
@ Z3_STRING_SYMBOL
Definition: z3_api.h:118

## ◆ to_int()

int to_int | ( |  | ) | const
| inline

Definition at line 435 of file z3++.h.

435{ assert(kind() == Z3_INT_SYMBOL); return Z3_get_symbol_int(ctx(), m_sym); }
Z3_get_symbol_int
int Z3_API Z3_get_symbol_int(Z3_context c, Z3_symbol s)
Return the symbol int value.
Z3_INT_SYMBOL
@ Z3_INT_SYMBOL
Definition: z3_api.h:117

## Friends And Related Function Documentation

## ◆ operator<<

std::ostream & operator<< | ( | std::ostream & | out,
|  | symbol const & | s
| ) |  |
| friend

Definition at line 439 of file z3++.h.

439 {
440 if (s.kind() == Z3_INT_SYMBOL)
441 out << "k!" << s.to_int();
442 else
443 out << s.str();
444 return out;
445 }