parameter Class Reference

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...

#include <z3++.h>

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

Detailed Description

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.

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

Constructor & Destructor Documentation

parameter() [1/2]

parameter ( func_decl const &  d, unsigned  idx  )

inline

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

                                                    : m_decl(d), m_index(idx) { 
            if (ctx().enable_exceptions() && idx >= d.num_parameters())
                Z3_THROW(exception("parameter index is out of bounds"));
            m_kind = Z3_get_decl_parameter_kind(ctx(), d, idx); 
        }

parameter() [2/2]

parameter ( expr const &  e, unsigned  idx  )

inline

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

                                               : m_decl(e.decl()), m_index(idx) {
            if (ctx().enable_exceptions() && idx >= m_decl.num_parameters())
                Z3_THROW(exception("parameter index is out of bounds"));
            m_kind = Z3_get_decl_parameter_kind(ctx(), m_decl, idx);
        }

Member Function Documentation

get_decl()

func_decl get_decl ( ) const

inline

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

{ Z3_func_decl f = Z3_get_decl_func_decl_parameter(ctx(), m_decl, m_index); check_error(); return func_decl(ctx(), f); }

get_double()

double get_double ( ) const

inline

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

{ double d = Z3_get_decl_double_parameter(ctx(), m_decl, m_index); check_error(); return d; }

get_expr()

expr get_expr ( ) const

inline

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

{ Z3_ast a = Z3_get_decl_ast_parameter(ctx(), m_decl, m_index); check_error(); return expr(ctx(), a); }

get_int()

int get_int ( ) const

inline

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

{ int i = Z3_get_decl_int_parameter(ctx(), m_decl, m_index); check_error(); return i; }

get_rational()

std::string get_rational ( ) const

inline

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

{ Z3_string s = Z3_get_decl_rational_parameter(ctx(), m_decl, m_index); check_error(); return s; }

get_sort()

sort get_sort ( ) const

inline

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

{ Z3_sort s = Z3_get_decl_sort_parameter(ctx(), m_decl, m_index); check_error(); return sort(ctx(), s); }

Referenced by ModelRef::sorts().

get_symbol()

symbol get_symbol ( ) const

inline

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

{ Z3_symbol s = Z3_get_decl_symbol_parameter(ctx(), m_decl, m_index); check_error(); return symbol(ctx(), s); }

kind()

Z3_parameter_kind kind ( ) const

inline

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

{ return m_kind; }

Referenced by ArithSortRef::is_int(), and ArithSortRef::is_real().