Z3
Public Member Functions
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...

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 2733 of file z3++.h.

Constructor & Destructor Documentation

◆ parameter() [1/2]

parameter ( func_decl const &  d,
unsigned  idx 
)
inline

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

2740  : m_decl(d), m_index(idx) {
2741  if (ctx().enable_exceptions() && idx >= d.num_parameters())
2742  Z3_THROW(exception("parameter index is out of bounds"));
2743  m_kind = Z3_get_decl_parameter_kind(ctx(), d, idx);
2744  }
Z3_parameter_kind Z3_API Z3_get_decl_parameter_kind(Z3_context c, Z3_func_decl d, unsigned idx)
Return the parameter type associated with a declaration.
#define Z3_THROW(x)
Definition: z3++.h:103

◆ parameter() [2/2]

parameter ( expr const &  e,
unsigned  idx 
)
inline

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

2745  : m_decl(e.decl()), m_index(idx) {
2746  if (ctx().enable_exceptions() && idx >= m_decl.num_parameters())
2747  Z3_THROW(exception("parameter index is out of bounds"));
2748  m_kind = Z3_get_decl_parameter_kind(ctx(), m_decl, idx);
2749  }
unsigned num_parameters() const
Definition: z3++.h:776

Member Function Documentation

◆ get_decl()

func_decl get_decl ( ) const
inline

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

2753 { Z3_func_decl f = Z3_get_decl_func_decl_parameter(ctx(), m_decl, m_index); check_error(); return func_decl(ctx(), f); }
Z3_func_decl Z3_API Z3_get_decl_func_decl_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the expression value associated with an expression parameter.
System.IntPtr Z3_func_decl

◆ get_double()

double get_double ( ) const
inline

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

2756 { double d = Z3_get_decl_double_parameter(ctx(), m_decl, m_index); check_error(); return d; }
double Z3_API Z3_get_decl_double_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the double value associated with an double parameter.

◆ get_expr()

expr get_expr ( ) const
inline

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

2751 { Z3_ast a = Z3_get_decl_ast_parameter(ctx(), m_decl, m_index); check_error(); return expr(ctx(), a); }
Z3_ast Z3_API Z3_get_decl_ast_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the expression value associated with an expression parameter.
System.IntPtr Z3_ast

◆ get_int()

int get_int ( ) const
inline

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

2757 { int i = Z3_get_decl_int_parameter(ctx(), m_decl, m_index); check_error(); return i; }
int Z3_API Z3_get_decl_int_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the integer value associated with an integer parameter.

◆ get_rational()

std::string get_rational ( ) const
inline

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

2755 { Z3_string s = Z3_get_decl_rational_parameter(ctx(), m_decl, m_index); check_error(); return s; }
const char * Z3_string
Z3 string type. It is just an alias for const char *.
Definition: z3_api.h:53
Z3_string Z3_API Z3_get_decl_rational_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the rational value, as a string, associated with a rational parameter.

◆ get_sort()

sort get_sort ( ) const
inline

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

2752 { Z3_sort s = Z3_get_decl_sort_parameter(ctx(), m_decl, m_index); check_error(); return sort(ctx(), s); }
Z3_sort Z3_API Z3_get_decl_sort_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the sort value associated with a sort parameter.
System.IntPtr Z3_sort

Referenced by ModelRef::sorts().

◆ get_symbol()

symbol get_symbol ( ) const
inline

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

2754 { Z3_symbol s = Z3_get_decl_symbol_parameter(ctx(), m_decl, m_index); check_error(); return symbol(ctx(), s); }
Z3_symbol Z3_API Z3_get_decl_symbol_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the double value associated with an double parameter.
System.IntPtr Z3_symbol

◆ kind()

Z3_parameter_kind kind ( ) const
inline

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

2750 { return m_kind; }

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