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 () override
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)
virtual	~object ()=default
context &	ctx () const
Z3_error_code	check_error () const

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

Additional Inherited Members
Protected Attributes inherited from object
context *	m_ctx

Detailed Description

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

Constructor & Destructor Documentation

param_descrs() [1/2]

param_descrs ( context & c, Z3_param_descrs d )

inline

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

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

Referenced by global_param_descrs(), operator=(), param_descrs(), and simplify_param_descrs().

param_descrs() [2/2]

param_descrs ( param_descrs const & o )

inline

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

: object(o.ctx()), m_descrs(o.m_descrs) { Z3_param_descrs_inc_ref(ctx(), m_descrs); }

~param_descrs()

~param_descrs ( )

inlineoverride

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

{ Z3_param_descrs_dec_ref(ctx(), m_descrs); }

Member Function Documentation

documentation()

std::string documentation ( symbol const & s )

inline

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

{ char const* r = Z3_param_descrs_get_documentation(ctx(), m_descrs, s); check_error(); return r; }

global_param_descrs()

param_descrs global_param_descrs ( context & c )

inlinestatic

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

{ return param_descrs(c, Z3_get_global_param_descrs(c)); }

kind()

Z3_param_kind kind ( symbol const & s )

inline

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

{ return Z3_param_descrs_get_kind(ctx(), m_descrs, s); }

name()

symbol name ( unsigned i )

inline

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

{ return symbol(ctx(), Z3_param_descrs_get_name(ctx(), m_descrs, i)); }

operator=()

param_descrs & operator= ( param_descrs const & o )

inline

Definition at line 591 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;
            object::operator=(o);
            return *this;
        }

simplify_param_descrs()

param_descrs simplify_param_descrs ( context & c )

inlinestatic

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

{ return param_descrs(c, Z3_simplify_get_param_descrs(c)); }

size()

unsigned size ( )

inline

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

{ return Z3_param_descrs_size(ctx(), m_descrs); }

to_string()

std::string to_string ( ) const

inline

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

{ return Z3_param_descrs_to_string(ctx(), m_descrs); }

Referenced by z3::operator<<().