Z3 |

Public Member Functions
func_interp Class Reference

`#include <z3++.h>`

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_interp & | operator= (func_interp const &s)
expr | else_value () const
unsigned | num_entries () const
func_entry | entry (unsigned i) const
void | add_entry (expr_vector const &args, expr &value)
void | set_else (expr &value)
Public Member Functions inherited from object
| object (context &c)
context & | ctx () const
Z3_error_code | check_error () const

## Additional Inherited Members
Protected Attributes inherited from object
context * | m_ctx

## Detailed Description

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

## Constructor & Destructor Documentation

## ◆ func_interp() [1/2]

func_interp | ( | context & | c,
|  | Z3_func_interp | e
| ) |  |
| inline

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

2408:object(c) { init(e); }
z3::object::object
object(context &c)
Definition: z3++.h:421

## ◆ func_interp() [2/2]

func_interp | ( | func_interp const & | s | ) |
| inline

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

2409:object(s) { init(s.m_interp); }

## ◆ ~func_interp()

~func_interp | ( |  | ) |
| inline

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

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

## Member Function Documentation

## ◆ add_entry()

void add_entry | ( | expr_vector const & | args,
|  | expr & | value
| ) |  |
| inline

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

2422 {
2423 Z3_func_interp_add_entry(ctx(), m_interp, args, value);
2424 check_error();
2425 }
z3::object::check_error
Z3_error_code check_error() const
Definition: z3++.h:423
Z3_func_interp_add_entry
void Z3_API Z3_func_interp_add_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value)
add a function entry to a function interpretation.

## ◆ else_value()

expr else_value | ( |  | ) | const
| inline

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

2419{ Z3_ast r = Z3_func_interp_get_else(ctx(), m_interp); check_error(); return expr(ctx(), r); }
Z3_func_interp_get_else
Z3_ast Z3_API Z3_func_interp_get_else(Z3_context c, Z3_func_interp f)
Return the 'else' value of the given function interpretation.

Referenced by FuncInterp::as_list().

## ◆ entry()

func_entry entry | ( | unsigned | i | ) | const
| inline

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

2421{ Z3_func_entry e = Z3_func_interp_get_entry(ctx(), m_interp, i); check_error(); return func_entry(ctx(), e); }
Z3_func_interp_get_entry
Z3_func_entry Z3_API Z3_func_interp_get_entry(Z3_context c, Z3_func_interp f, unsigned i)
Return a "point" of the given function interpretation. It represents the value of f in a particular p...

Referenced by FuncEntry::__deepcopy__(), FuncEntry::__del__(), FuncEntry::arg_value(), FuncInterp::as_list(), FuncEntry::num_args(), and FuncEntry::value().

## ◆ num_entries()

unsigned num_entries | ( |  | ) | const
| inline

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

2420{ unsigned r = Z3_func_interp_get_num_entries(ctx(), m_interp); check_error(); return r; }
Z3_func_interp_get_num_entries
unsigned Z3_API Z3_func_interp_get_num_entries(Z3_context c, Z3_func_interp f)
Return the number of entries in the given function interpretation.

Referenced by FuncInterp::as_list(), and FuncInterp::entry().

## ◆ operator Z3_func_interp()

operator Z3_func_interp | ( |  | ) | const
| inline

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

2411{ return m_interp; }

## ◆ operator=()

func_interp & operator= | ( | func_interp const & | s | ) |
| inline

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

2412 {
2413 Z3_func_interp_inc_ref(s.ctx(), s.m_interp);
2414 Z3_func_interp_dec_ref(ctx(), m_interp);
2415 object::operator=(s);
2416 m_interp = s.m_interp;
2417 return *this;
2418 }
Z3_func_interp_inc_ref
void Z3_API Z3_func_interp_inc_ref(Z3_context c, Z3_func_interp f)
Increment the reference counter of the given Z3_func_interp object.

## ◆ set_else()

void set_else | ( | expr & | value | ) |
| inline

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

2426 {
2427 Z3_func_interp_set_else(ctx(), m_interp, value);
2428 check_error();
2429 }
Z3_func_interp_set_else
void Z3_API Z3_func_interp_set_else(Z3_context c, Z3_func_interp f, Z3_ast else_value)
Return the 'else' value of the given function interpretation.