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)

	object (object const &s)

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

Constructor & Destructor Documentation

◆ param_descrs() [1/2]

param_descrs	(	context &	c,
		Z3_param_descrs	d
	)

inline

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

449 : object(c), m_descrs(d) { Z3_param_descrs_inc_ref(c, d); }

z3::object::object

object(context &c)

Definition: z3++.h:416

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

450 : 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:418

◆ ~param_descrs()

~param_descrs ( )

inline

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

458 { 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 464 of file z3++.h.

464 { 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:419

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

463 { 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 462 of file z3++.h.

462 { 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 451 of file z3++.h.

                                                        {
             Z3_param_descrs_inc_ref(o.ctx(), o.m_descrs);
             Z3_param_descrs_dec_ref(ctx(), m_descrs);
             m_descrs = o.m_descrs;
             m_ctx = o.m_ctx;
             return *this;
         }