Public Member Functions | |
symbol (context &c, Z3_symbol s) | |
symbol (symbol const &s) | |
symbol & | operator= (symbol const &s) |
operator Z3_symbol () const | |
Z3_symbol_kind | kind () const |
std::string | str () const |
int | to_int () const |
Friends | |
std::ostream & | operator<< (std::ostream &out, symbol const &s) |
Z3_symbol_kind kind | ( | ) | const [inline] |
Definition at line 285 of file z3++.h.
Referenced by symbol::str(), and symbol::to_int().
{ return Z3_get_symbol_kind(ctx(), m_sym); }
std::string str | ( | ) | const [inline] |
Definition at line 286 of file z3++.h.
{ assert(kind() == Z3_STRING_SYMBOL); return Z3_get_symbol_string(ctx(), m_sym); }
int to_int | ( | ) | const [inline] |
Definition at line 287 of file z3++.h.
{ assert(kind() == Z3_INT_SYMBOL); return Z3_get_symbol_int(ctx(), m_sym); }
std::ostream& operator<< | ( | std::ostream & | out, |
symbol const & | s | ||
) | [friend] |
Definition at line 288 of file z3++.h.
{ if (s.kind() == Z3_INT_SYMBOL) out << "k!" << s.to_int(); else out << s.str().c_str(); return out; }