symbol Class Reference

Inheritance diagram for symbol:

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
Public Member Functions inherited from object
	object (context &c)
	object (object const &s)
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 424 of file z3++.h.

Constructor & Destructor Documentation

symbol() [1/2]

symbol ( context &  c, Z3_symbol  s  )

inline

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

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

symbol() [2/2]

symbol ( symbol const &  s )

inline

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

:object(s), m_sym(s.m_sym) {}

Member Function Documentation

kind()

Z3_symbol_kind kind ( ) const

inline

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

Referenced by z3::operator<<().

{ return Z3_get_symbol_kind(ctx(), m_sym); }

operator Z3_symbol()

operator Z3_symbol ( ) const

inline

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

{ return m_sym; }

operator=()

symbol& operator= ( symbol const &  s )

inline

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

{ m_ctx = s.m_ctx; m_sym = s.m_sym; return *this; }

str()

std::string str ( ) const

inline

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

Referenced by z3::operator<<().

{ assert(kind() == Z3_STRING_SYMBOL); return Z3_get_symbol_string(ctx(), m_sym); }

to_int()

int to_int ( ) const

inline

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

Referenced by z3::operator<<().

{ assert(kind() == Z3_INT_SYMBOL); return Z3_get_symbol_int(ctx(), m_sym); }

Friends And Related Function Documentation

operator<<

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

friend

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

                                                                       {
        if (s.kind() == Z3_INT_SYMBOL)
            out << "k!" << s.to_int();
        else
            out << s.str();
        return out;
    }