Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules 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
contextm_ctx
 

Detailed Description

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

Constructor & Destructor Documentation

func_interp ( context c,
Z3_func_interp  e 
)
inline

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

1139 :object(c) { init(e); }
object(context &c)
Definition: z3++.h:270
func_interp ( func_interp const &  s)
inline

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

1140 :object(s) { init(s.m_interp); }
object(context &c)
Definition: z3++.h:270
~func_interp ( )
inline

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

1141 { Z3_func_interp_dec_ref(ctx(), m_interp); }
context & ctx() const
Definition: z3++.h:272
void Z3_API Z3_func_interp_dec_ref(__in Z3_context c, __in Z3_func_interp f)
Decrement the reference counter of the given Z3_func_interp object.

Member Function Documentation

expr else_value ( ) const
inline

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

1150 { Z3_ast r = Z3_func_interp_get_else(ctx(), m_interp); check_error(); return expr(ctx(), r); }
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
Z3_ast Z3_API Z3_func_interp_get_else(__in Z3_context c, __in Z3_func_interp f)
Return the 'else' value of the given function interpretation.
func_entry entry ( unsigned  i) const
inline

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

1152 { Z3_func_entry e = Z3_func_interp_get_entry(ctx(), m_interp, i); check_error(); return func_entry(ctx(), e); }
Z3_func_entry Z3_API Z3_func_interp_get_entry(__in Z3_context c, __in Z3_func_interp f, unsigned i)
Return a "point" of the given function intepretation. It represents the value of f in a particular po...
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
unsigned num_entries ( ) const
inline

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

Referenced by FuncInterp::entry().

1151 { unsigned r = Z3_func_interp_get_num_entries(ctx(), m_interp); check_error(); return r; }
unsigned Z3_API Z3_func_interp_get_num_entries(__in Z3_context c, __in Z3_func_interp f)
Return the number of entries in the given function interpretation.
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
operator Z3_func_interp ( ) const
inline

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

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

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

1143  {
1144  Z3_func_interp_inc_ref(s.ctx(), s.m_interp);
1145  Z3_func_interp_dec_ref(ctx(), m_interp);
1146  m_ctx = s.m_ctx;
1147  m_interp = s.m_interp;
1148  return *this;
1149  }
context & ctx() const
Definition: z3++.h:272
void Z3_API Z3_func_interp_inc_ref(__in Z3_context c, __in Z3_func_interp f)
Increment the reference counter of the given Z3_func_interp object.
void Z3_API Z3_func_interp_dec_ref(__in Z3_context c, __in Z3_func_interp f)
Decrement the reference counter of the given Z3_func_interp object.
context * m_ctx
Definition: z3++.h:268