Z3
Public Member Functions | Static Public Member Functions
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_descrsoperator= (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)
 
contextctx () 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
contextm_ctx
 

Detailed Description

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

Constructor & Destructor Documentation

param_descrs ( context c,
Z3_param_descrs  d 
)
inline

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

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

502 : object(c), m_descrs(d) { Z3_param_descrs_inc_ref(c, d); }
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.
object(context &c)
Definition: z3++.h:472
param_descrs ( param_descrs const &  o)
inline

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

503 : object(o.ctx()), m_descrs(o.m_descrs) { Z3_param_descrs_inc_ref(ctx(), m_descrs); }
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.
context & ctx() const
Definition: z3++.h:473
object(context &c)
Definition: z3++.h:472
~param_descrs ( )
inline

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

511 { Z3_param_descrs_dec_ref(ctx(), m_descrs); }
context & ctx() const
Definition: z3++.h:473
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

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

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

518 { char const* r = Z3_param_descrs_get_documentation(ctx(), m_descrs, s); check_error(); return r; }
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.
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
static param_descrs global_param_descrs ( context c)
inlinestatic

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

513 { return param_descrs(c, Z3_get_global_param_descrs(c)); }
param_descrs(context &c, Z3_param_descrs d)
Definition: z3++.h:502
Z3_param_descrs Z3_API Z3_get_global_param_descrs(Z3_context c)
Retrieve description of global parameters.
Z3_param_kind kind ( symbol const &  s)
inline

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

517 { return Z3_param_descrs_get_kind(ctx(), m_descrs, s); }
context & ctx() const
Definition: z3++.h:473
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.
symbol name ( unsigned  i)
inline

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

516 { return symbol(ctx(), Z3_param_descrs_get_name(ctx(), m_descrs, i)); }
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.
context & ctx() const
Definition: z3++.h:473
param_descrs& operator= ( param_descrs const &  o)
inline

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

504  {
505  Z3_param_descrs_inc_ref(o.ctx(), o.m_descrs);
506  Z3_param_descrs_dec_ref(ctx(), m_descrs);
507  m_descrs = o.m_descrs;
508  object::operator=(o);
509  return *this;
510  }
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.
context & ctx() const
Definition: z3++.h:473
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.
static param_descrs simplify_param_descrs ( context c)
inlinestatic

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

Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(Z3_context c)
Return the parameter description set for the simplify procedure.
param_descrs(context &c, Z3_param_descrs d)
Definition: z3++.h:502
unsigned size ( )
inline

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

515 { return Z3_param_descrs_size(ctx(), m_descrs); }
context & ctx() const
Definition: z3++.h:473
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.
std::string to_string ( ) const
inline

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

Referenced by z3::operator<<().

519 { return Z3_param_descrs_to_string(ctx(), m_descrs); }
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...
context & ctx() const
Definition: z3++.h:473