All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
Public Member Functions
func_interp Class Reference
+ Inheritance diagram for func_interp:

Public Member Functions

 func_interp (context &c, Z3_func_interp e)
 func_interp (func_interp const &s)
 ~func_interp ()
 operator Z3_func_interp () const
func_interpoperator= (func_interp const &s)
expr else_value () const
unsigned num_entries () const
func_entry entry (unsigned i) const
- Public Member Functions inherited from object
 object (context &c)
 object (object const &s)
contextctx () const
void check_error () const

Additional Inherited Members

- Protected Attributes inherited from object

Detailed Description

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

Constructor & Destructor Documentation

func_interp ( context c,
Z3_func_interp  e 

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

:object(c) { init(e); }
func_interp ( func_interp const &  s)

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

:object(s) { init(s.m_interp); }
~func_interp ( )

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

{ Z3_func_interp_dec_ref(ctx(), m_interp); }

Member Function Documentation

expr else_value ( ) const

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

{ Z3_ast r = Z3_func_interp_get_else(ctx(), m_interp); check_error(); return expr(ctx(), r); }
func_entry entry ( unsigned  i) const

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

{ Z3_func_entry e = Z3_func_interp_get_entry(ctx(), m_interp, i); check_error(); return func_entry(ctx(), e); }
unsigned num_entries ( ) const

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

Referenced by FuncInterp::entry().

{ unsigned r = Z3_func_interp_get_num_entries(ctx(), m_interp); check_error(); return r; }
operator Z3_func_interp ( ) const

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

{ return m_interp; }
func_interp& operator= ( func_interp const &  s)

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

Z3_func_interp_inc_ref(s.ctx(), s.m_interp);
m_ctx = s.m_ctx;
m_interp = s.m_interp;
return *this;