class for auxiliary parameters associated with func_decl The class is initialized with a func_decl or application expression and an index The accessor get_expr, get_sort, ... is available depending on the value of kind(). The caller is responsible to check that the kind of the parameter aligns with the call (get_expr etc). More...
Public Member Functions | |
parameter (func_decl const &d, unsigned idx) | |
parameter (expr const &e, unsigned idx) | |
Z3_parameter_kind | kind () const |
expr | get_expr () const |
sort | get_sort () const |
func_decl | get_decl () const |
symbol | get_symbol () const |
std::string | get_rational () const |
double | get_double () const |
int | get_int () const |
class for auxiliary parameters associated with func_decl The class is initialized with a func_decl or application expression and an index The accessor get_expr, get_sort, ... is available depending on the value of kind(). The caller is responsible to check that the kind of the parameter aligns with the call (get_expr etc).
Parameters are available on some declarations to contain additional information that is not passed as arguments when a function is applied to arguments. For example, bit-vector extraction has two integer parameters. Array map has a function parameter.
|
inline |
Definition at line 2753 of file z3++.h.
|
inline |
|
inline |
Definition at line 2751 of file z3++.h.
|
inline |
|
inline |
Definition at line 2755 of file z3++.h.
|
inline |
Definition at line 2752 of file z3++.h.
Referenced by ModelRef::sorts().
|
inline |
Definition at line 2754 of file z3++.h.
|
inline |
Definition at line 2750 of file z3++.h.
Referenced by ArithSortRef::is_int(), and ArithSortRef::is_real().