Z3
Loading...
Searching...
No Matches
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)
virtual ~object ()=default
contextctx () 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
contextm_ctx

Detailed Description

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

Constructor & Destructor Documentation

◆ symbol()

symbol ( context & c,
Z3_symbol s )
inline

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

483:object(c), m_sym(s) {}

Referenced by operator<<.

Member Function Documentation

◆ kind()

Z3_symbol_kind kind ( ) const
inline

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

485{ return Z3_get_symbol_kind(ctx(), m_sym); }
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 operator<<, str(), and to_int().

◆ operator Z3_symbol()

operator Z3_symbol ( ) const
inline

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

484{ return m_sym; }

◆ str()

std::string str ( ) const
inline

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

486{ assert(kind() == Z3_STRING_SYMBOL); return Z3_get_symbol_string(ctx(), m_sym); }
Z3_string Z3_API Z3_get_symbol_string(Z3_context c, Z3_symbol s)
Return the symbol name.
@ Z3_STRING_SYMBOL
Definition z3_api.h:74

Referenced by operator<<.

◆ to_int()

int to_int ( ) const
inline

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

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

Referenced by operator<<.

◆ operator<<

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

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

491 {
492 if (s.kind() == Z3_INT_SYMBOL)
493 out << "k!" << s.to_int();
494 else
495 out << s.str();
496 return out;
497 }