Z3
Public Member Functions | Friends
symbol Class Reference
+ 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)
 
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 457 of file z3++.h.

Constructor & Destructor Documentation

◆ symbol()

symbol ( context c,
Z3_symbol  s 
)
inline

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

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

Member Function Documentation

◆ kind()

Z3_symbol_kind kind ( ) const
inline

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

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

Referenced by z3::operator<<(), symbol::str(), and symbol::to_int().

◆ operator Z3_symbol()

operator Z3_symbol ( ) const
inline

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

461 { return m_sym; }

◆ str()

std::string str ( ) const
inline

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

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

Referenced by z3::operator<<().

◆ to_int()

int to_int ( ) const
inline

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

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

Referenced by z3::operator<<().

Friends And Related Function Documentation

◆ operator<<

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

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

468  {
469  if (s.kind() == Z3_INT_SYMBOL)
470  out << "k!" << s.to_int();
471  else
472  out << s.str();
473  return out;
474  }
z3::object::object
object(context &c)
Definition: z3++.h:450
z3::symbol::kind
Z3_symbol_kind kind() const
Definition: z3++.h:462
Z3_get_symbol_string
Z3_string Z3_API Z3_get_symbol_string(Z3_context c, Z3_symbol s)
Return the symbol name.
Z3_STRING_SYMBOL
@ Z3_STRING_SYMBOL
Definition: z3_api.h:76
Z3_get_symbol_int
int Z3_API Z3_get_symbol_int(Z3_context c, Z3_symbol s)
Return the symbol int value.
z3::object::ctx
context & ctx() const
Definition: z3++.h:451
Z3_get_symbol_kind
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...
Z3_INT_SYMBOL
@ Z3_INT_SYMBOL
Definition: z3_api.h:75