param_descrs Class Reference

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)
static param_descrs	global_param_descrs (context &c)

Additional Inherited Members
Protected Attributes inherited from object
context *	m_ctx

Detailed Description

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

Constructor & Destructor Documentation

param_descrs() [1/2]

param_descrs ( context &  c, Z3_param_descrs  d  )

inline

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

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

Referenced by param_descrs::global_param_descrs(), and param_descrs::simplify_param_descrs().

param_descrs() [2/2]

param_descrs ( param_descrs const &  o )

inline

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

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

~param_descrs()

~param_descrs ( )

inline

Definition at line 501 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 508 of file z3++.h.

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

global_param_descrs()

static param_descrs global_param_descrs ( context &  c )

inlinestatic

Definition at line 503 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 507 of file z3++.h.

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

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

name()

symbol name ( unsigned  i )

inline

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

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

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

operator=()

param_descrs& operator= ( param_descrs const &  o )

inline

Definition at line 494 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()

static param_descrs simplify_param_descrs ( context &  c )

inlinestatic

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

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

size()

unsigned size ( )

inline

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

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

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

to_string()

std::string to_string ( ) const

inline

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

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

Referenced by z3::operator<<().