Z3 |

Public Member Functions | Static Public Member Functions
param_descrs Class Reference

`#include <z3++.h>`

Inheritance diagram for param_descrs:

## Public Member Functions
| param_descrs (context &c, Z3_param_descrs d)
| param_descrs (param_descrs const &o)
param_descrs & | operator= (param_descrs const &o)
| ~param_descrs ()
unsigned | size ()
symbol | name (unsigned i)
Z3_param_kind | kind (symbol const &s)
std::string | documentation (symbol const &s)
std::string | to_string () const
Public Member Functions inherited from object
| object (context &c)
context & | ctx () const
Z3_error_code | check_error () const

## Static Public Member Functions
static param_descrs | simplify_param_descrs (context &c)

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

## Detailed Description

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

## Constructor & Destructor Documentation

## ◆ param_descrs() [1/2]

param_descrs | ( | context & | c,
|  | Z3_param_descrs | d
| ) |  |
| inline

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

451: object(c), m_descrs(d) { Z3_param_descrs_inc_ref(c, d); }
z3::object::object
object(context &c)
Definition: z3++.h:421
Z3_param_descrs_inc_ref
void Z3_API Z3_param_descrs_inc_ref(Z3_context c, Z3_param_descrs p)
Increment the reference counter of the given parameter description set.

Referenced by param_descrs::simplify_param_descrs().

## ◆ param_descrs() [2/2]

param_descrs | ( | param_descrs const & | o | ) |
| inline

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

452: object(o.ctx()), m_descrs(o.m_descrs) { Z3_param_descrs_inc_ref(ctx(), m_descrs); }
z3::object::ctx
context & ctx() const
Definition: z3++.h:422

## ◆ ~param_descrs()

~param_descrs | ( |  | ) |
| inline

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

460{ Z3_param_descrs_dec_ref(ctx(), m_descrs); }
Z3_param_descrs_dec_ref
void Z3_API Z3_param_descrs_dec_ref(Z3_context c, Z3_param_descrs p)
Decrement the reference counter of the given parameter description set.

## Member Function Documentation

## ◆ documentation()

std::string documentation | ( | symbol const & | s | ) |
| inline

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

466{ char const* r = Z3_param_descrs_get_documentation(ctx(), m_descrs, s); check_error(); return r; }
z3::object::check_error
Z3_error_code check_error() const
Definition: z3++.h:423
Z3_param_descrs_get_documentation
Z3_string Z3_API Z3_param_descrs_get_documentation(Z3_context c, Z3_param_descrs p, Z3_symbol s)
Retrieve documentation string corresponding to parameter name s.

## ◆ kind()

Z3_param_kind kind | ( | symbol const & | s | ) |
| inline

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

465{ return Z3_param_descrs_get_kind(ctx(), m_descrs, s); }
Z3_param_descrs_get_kind
Z3_param_kind Z3_API Z3_param_descrs_get_kind(Z3_context c, Z3_param_descrs p, Z3_symbol n)
Return the kind associated with the given parameter name n.

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

## ◆ name()

symbol name | ( | unsigned | i | ) |
| inline

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

464{ return symbol(ctx(), Z3_param_descrs_get_name(ctx(), m_descrs, i)); }
Z3_param_descrs_get_name
Z3_symbol Z3_API Z3_param_descrs_get_name(Z3_context c, Z3_param_descrs p, unsigned i)
Return the name of the parameter at given index i.

Referenced by Datatype::__deepcopy__(), and Datatype::__repr__().

## ◆ operator=()

param_descrs & operator= | ( | param_descrs const & | o | ) |
| inline

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

453 {
454 Z3_param_descrs_inc_ref(o.ctx(), o.m_descrs);
455 Z3_param_descrs_dec_ref(ctx(), m_descrs);
456 m_descrs = o.m_descrs;
457 object::operator=(o);
458 return *this;
459 }

## ◆ simplify_param_descrs()

static param_descrs simplify_param_descrs | ( | context & | c | ) |
| inline static

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

461{ return param_descrs(c, Z3_simplify_get_param_descrs(c)); }
z3::param_descrs::param_descrs
param_descrs(context &c, Z3_param_descrs d)
Definition: z3++.h:451
Z3_simplify_get_param_descrs
Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(Z3_context c)
Return the parameter description set for the simplify procedure.

## ◆ size()

unsigned size | ( |  | ) |
| inline

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

463{ return Z3_param_descrs_size(ctx(), m_descrs); }
Z3_param_descrs_size
unsigned Z3_API Z3_param_descrs_size(Z3_context c, Z3_param_descrs p)
Return the number of parameters in the given parameter description set.

Referenced by ParamDescrsRef::__len__(), Goal::__len__(), BitVecNumRef::as_signed_long(), and BitVecSortRef::subsort().

## ◆ to_string()

std::string to_string | ( |  | ) | const
| inline

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

467{ return Z3_param_descrs_to_string(ctx(), m_descrs); }
Z3_param_descrs_to_string
Z3_string Z3_API Z3_param_descrs_to_string(Z3_context c, Z3_param_descrs p)
Convert a parameter description set into a string. This function is mainly used for printing the cont...

Referenced by z3::operator<<().