Z3
Public Member Functions | Friends
params Class Reference
+ Inheritance diagram for params:

Public Member Functions

 params (context &c)
 
 params (params const &s)
 
 ~params ()
 
 operator Z3_params () const
 
paramsoperator= (params const &s)
 
void set (char const *k, bool b)
 
void set (char const *k, unsigned n)
 
void set (char const *k, double n)
 
void set (char const *k, symbol const &s)
 
- Public Member Functions inherited from object
 object (context &c)
 
 object (object const &s)
 
contextctx () const
 
void check_error () const
 

Friends

std::ostream & operator<< (std::ostream &out, params const &p)
 

Additional Inherited Members

- Protected Attributes inherited from object
contextm_ctx
 

Detailed Description

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

Constructor & Destructor Documentation

§ params() [1/2]

params ( context c)
inline

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

387 :object(c) { m_params = Z3_mk_params(c); Z3_params_inc_ref(ctx(), m_params); }
Z3_params Z3_API Z3_mk_params(Z3_context c)
Create a Z3 (empty) parameter set. Starting at Z3 4.0, parameter sets are used to configure many comp...
context & ctx() const
Definition: z3++.h:332
object(context &c)
Definition: z3++.h:330
void Z3_API Z3_params_inc_ref(Z3_context c, Z3_params p)
Increment the reference counter of the given parameter set.

§ params() [2/2]

params ( params const &  s)
inline

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

388 :object(s), m_params(s.m_params) { Z3_params_inc_ref(ctx(), m_params); }
context & ctx() const
Definition: z3++.h:332
object(context &c)
Definition: z3++.h:330
void Z3_API Z3_params_inc_ref(Z3_context c, Z3_params p)
Increment the reference counter of the given parameter set.

§ ~params()

~params ( )
inline

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

389 { Z3_params_dec_ref(ctx(), m_params); }
context & ctx() const
Definition: z3++.h:332
void Z3_API Z3_params_dec_ref(Z3_context c, Z3_params p)
Decrement the reference counter of the given parameter set.

Member Function Documentation

§ operator Z3_params()

operator Z3_params ( ) const
inline

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

390 { return m_params; }

§ operator=()

params& operator= ( params const &  s)
inline

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

391  {
392  Z3_params_inc_ref(s.ctx(), s.m_params);
393  Z3_params_dec_ref(ctx(), m_params);
394  m_ctx = s.m_ctx;
395  m_params = s.m_params;
396  return *this;
397  }
context & ctx() const
Definition: z3++.h:332
void Z3_API Z3_params_dec_ref(Z3_context c, Z3_params p)
Decrement the reference counter of the given parameter set.
void Z3_API Z3_params_inc_ref(Z3_context c, Z3_params p)
Increment the reference counter of the given parameter set.
context * m_ctx
Definition: z3++.h:328

§ set() [1/4]

void set ( char const *  k,
bool  b 
)
inline

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

398 { Z3_params_set_bool(ctx(), m_params, ctx().str_symbol(k), b); }
context & ctx() const
Definition: z3++.h:332
void Z3_API Z3_params_set_bool(Z3_context c, Z3_params p, Z3_symbol k, Z3_bool v)
Add a Boolean parameter k with value v to the parameter set p.

§ set() [2/4]

void set ( char const *  k,
unsigned  n 
)
inline

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

399 { Z3_params_set_uint(ctx(), m_params, ctx().str_symbol(k), n); }
void Z3_API Z3_params_set_uint(Z3_context c, Z3_params p, Z3_symbol k, unsigned v)
Add a unsigned parameter k with value v to the parameter set p.
context & ctx() const
Definition: z3++.h:332

§ set() [3/4]

void set ( char const *  k,
double  n 
)
inline

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

400 { Z3_params_set_double(ctx(), m_params, ctx().str_symbol(k), n); }
context & ctx() const
Definition: z3++.h:332
void Z3_API Z3_params_set_double(Z3_context c, Z3_params p, Z3_symbol k, double v)
Add a double parameter k with value v to the parameter set p.

§ set() [4/4]

void set ( char const *  k,
symbol const &  s 
)
inline

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

401 { Z3_params_set_symbol(ctx(), m_params, ctx().str_symbol(k), s); }
context & ctx() const
Definition: z3++.h:332
void Z3_API Z3_params_set_symbol(Z3_context c, Z3_params p, Z3_symbol k, Z3_symbol v)
Add a symbol parameter k with value v to the parameter set p.

Friends And Related Function Documentation

§ operator<<

std::ostream& operator<< ( std::ostream &  out,
params const &  p 
)
friend

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

405  {
406  out << Z3_params_to_string(p.ctx(), p); return out;
407  }
Z3_string Z3_API Z3_params_to_string(Z3_context c, Z3_params p)
Convert a parameter set into a string. This function is mainly used for printing the contents of a pa...