klee
Public Member Functions | Protected Attributes | Private Member Functions | List of all members
klee::Z3NodeHandle< T > Class Template Reference

#include <Z3Builder.h>

Public Member Functions

 Z3NodeHandle ()
 
 Z3NodeHandle (const T _node, const ::Z3_context _context)
 
 ~Z3NodeHandle ()
 
 Z3NodeHandle (const Z3NodeHandle &b)
 
Z3NodeHandle & operator= (const Z3NodeHandle &b)
 
void dump ()
 
 operator T () const
 
void dump () __attribute__((used))
 
void dump () __attribute__((used))
 

Protected Attributes

T node
 
::Z3_context context
 

Private Member Functions

inline ::Z3_ast as_ast ()
 
Z3_ast as_ast ()
 
Z3_ast as_ast ()
 

Detailed Description

template<typename T>
class klee::Z3NodeHandle< T >

Definition at line 22 of file Z3Builder.h.

Constructor & Destructor Documentation

◆ Z3NodeHandle() [1/3]

template<typename T >
klee::Z3NodeHandle< T >::Z3NodeHandle ( )
inline

Definition at line 36 of file Z3Builder.h.

◆ Z3NodeHandle() [2/3]

template<typename T >
klee::Z3NodeHandle< T >::Z3NodeHandle ( const T  _node,
const ::Z3_context  _context 
)
inline

Definition at line 37 of file Z3Builder.h.

References klee::Z3NodeHandle< T >::as_ast(), klee::Z3NodeHandle< T >::context, and klee::Z3NodeHandle< T >::node.

Here is the call graph for this function:

◆ ~Z3NodeHandle()

template<typename T >
klee::Z3NodeHandle< T >::~Z3NodeHandle ( )
inline

Definition at line 43 of file Z3Builder.h.

References klee::Z3NodeHandle< T >::as_ast(), klee::Z3NodeHandle< T >::context, and klee::Z3NodeHandle< T >::node.

Here is the call graph for this function:

◆ Z3NodeHandle() [3/3]

template<typename T >
klee::Z3NodeHandle< T >::Z3NodeHandle ( const Z3NodeHandle< T > &  b)
inline

Definition at line 48 of file Z3Builder.h.

References klee::Z3NodeHandle< T >::as_ast(), klee::Z3NodeHandle< T >::context, and klee::Z3NodeHandle< T >::node.

Here is the call graph for this function:

Member Function Documentation

◆ as_ast() [1/3]

template<typename T >
inline ::Z3_ast klee::Z3NodeHandle< T >::as_ast ( )
private

Referenced by klee::Z3NodeHandle< T >::operator=(), klee::Z3NodeHandle< T >::Z3NodeHandle(), and klee::Z3NodeHandle< T >::~Z3NodeHandle().

Here is the caller graph for this function:

◆ as_ast() [2/3]

Z3_ast klee::Z3NodeHandle< Z3_sort >::as_ast ( )
inlineprivate

Definition at line 81 of file Z3Builder.h.

◆ as_ast() [3/3]

Z3_ast klee::Z3NodeHandle< Z3_ast >::as_ast ( )
inlineprivate

Definition at line 90 of file Z3Builder.h.

◆ dump() [1/3]

template<typename T >
void klee::Z3NodeHandle< T >::dump ( )

◆ dump() [2/3]

void klee::Z3NodeHandle< Z3_sort >::dump ( )

◆ dump() [3/3]

void klee::Z3NodeHandle< Z3_ast >::dump ( )

◆ operator T()

template<typename T >
klee::Z3NodeHandle< T >::operator T ( ) const
inline

Definition at line 77 of file Z3Builder.h.

References klee::Z3NodeHandle< T >::node.

◆ operator=()

template<typename T >
Z3NodeHandle & klee::Z3NodeHandle< T >::operator= ( const Z3NodeHandle< T > &  b)
inline

Definition at line 53 of file Z3Builder.h.

References klee::Z3NodeHandle< T >::as_ast(), klee::Z3NodeHandle< T >::context, and klee::Z3NodeHandle< T >::node.

Here is the call graph for this function:

Member Data Documentation

◆ context

template<typename T >
::Z3_context klee::Z3NodeHandle< T >::context
protected

Definition at line 29 of file Z3Builder.h.

Referenced by klee::Z3NodeHandle< T >::operator=(), klee::Z3NodeHandle< T >::Z3NodeHandle(), and klee::Z3NodeHandle< T >::~Z3NodeHandle().

◆ node

template<typename T >
T klee::Z3NodeHandle< T >::node
protected

Definition at line 28 of file Z3Builder.h.

Referenced by klee::Z3NodeHandle< T >::operator T(), klee::Z3NodeHandle< T >::operator=(), klee::Z3NodeHandle< T >::Z3NodeHandle(), and klee::Z3NodeHandle< T >::~Z3NodeHandle().

The documentation for this class was generated from the following file: