Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules Pages
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
 
- Public Member Functions inherited from object
 object (context &c)
 
 object (object const &s)
 
contextctx () const
 
void 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 278 of file z3++.h.

Constructor & Destructor Documentation

symbol ( context c,
Z3_symbol  s 
)
inline

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

281 :object(c), m_sym(s) {}
object(context &c)
Definition: z3++.h:270
symbol ( symbol const &  s)
inline

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

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

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().

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

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

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

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

283 { m_ctx = s.m_ctx; m_sym = s.m_sym; return *this; }
context * m_ctx
Definition: z3++.h:268
std::string str ( ) const
inline

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

286 { assert(kind() == Z3_STRING_SYMBOL); return Z3_get_symbol_string(ctx(), m_sym); }
context & ctx() const
Definition: z3++.h:272
Z3_symbol_kind kind() const
Definition: z3++.h:285
Z3_string Z3_API Z3_get_symbol_string(__in Z3_context c, __in Z3_symbol s)
Return the symbol name.
int to_int ( ) const
inline

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

287 { assert(kind() == Z3_INT_SYMBOL); return Z3_get_symbol_int(ctx(), m_sym); }
context & ctx() const
Definition: z3++.h:272
int Z3_API Z3_get_symbol_int(__in Z3_context c, __in Z3_symbol s)
Return the symbol int value.
Z3_symbol_kind kind() const
Definition: z3++.h:285

Friends And Related Function Documentation

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

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

288  {
289  if (s.kind() == Z3_INT_SYMBOL)
290  out << "k!" << s.to_int();
291  else
292  out << s.str().c_str();
293  return out;
294  }