Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Friends
symbol Class Reference
+ Inheritance diagram for symbol:

Public Member Functions

 symbol (context &c, Z3_symbol s)
 symbol (symbol const &s)
symboloperator= (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)

Detailed Description

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


Constructor & Destructor Documentation

symbol ( context c,
Z3_symbol  s 
) [inline]

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

:object(c), m_sym(s) {}
symbol ( symbol const &  s) [inline]

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

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

Member Function Documentation

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); }
operator Z3_symbol ( ) const [inline]

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

{ return m_sym; }
symbol& operator= ( symbol const &  s) [inline]

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

{ m_ctx = s.m_ctx; m_sym = s.m_sym; return *this; }
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); }

Friends And Related Function Documentation

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;
        }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines