Z3
 
Loading...
Searching...
No Matches
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 () override
 
 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
 
void add_entry (expr_vector const &args, expr &value)
 
void set_else (expr &value)
 
- Public Member Functions inherited from object
 object (context &c)
 
virtual ~object ()=default
 
contextctx () const
 
Z3_error_code check_error () const
 

Additional Inherited Members

- Protected Attributes inherited from object
contextm_ctx
 

Detailed Description

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

Constructor & Destructor Documentation

◆ func_interp() [1/2]

func_interp ( context & c,
Z3_func_interp e )
inline

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

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

◆ func_interp() [2/2]

func_interp ( func_interp const & s)
inline

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

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

◆ ~func_interp()

~func_interp ( )
inlineoverride

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

2582{ Z3_func_interp_dec_ref(ctx(), m_interp); }
context & ctx() const
Definition z3++.h:474
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 2594 of file z3++.h.

2594 {
2595 Z3_func_interp_add_entry(ctx(), m_interp, args, value);
2596 check_error();
2597 }
Z3_error_code check_error() const
Definition z3++.h:475
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 2591 of file z3++.h.

2591{ Z3_ast r = Z3_func_interp_get_else(ctx(), m_interp); check_error(); return expr(ctx(), r); }
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 2593 of file z3++.h.

2593{ 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(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 2592 of file z3++.h.

2592{ unsigned r = Z3_func_interp_get_num_entries(ctx(), m_interp); check_error(); return r; }
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 2583 of file z3++.h.

2583{ return m_interp; }

◆ operator=()

func_interp & operator= ( func_interp const & s)
inline

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

2584 {
2585 Z3_func_interp_inc_ref(s.ctx(), s.m_interp);
2586 Z3_func_interp_dec_ref(ctx(), m_interp);
2587 object::operator=(s);
2588 m_interp = s.m_interp;
2589 return *this;
2590 }
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 2598 of file z3++.h.

2598 {
2599 Z3_func_interp_set_else(ctx(), m_interp, value);
2600 check_error();
2601 }
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.