Z3
Loading...
Searching...
No Matches
params Class Reference

#include <z3++.h>

Inheritance diagram for params:

Public Member Functions

 params (context &c)
 params (params const &s)
 ~params () override
 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)
void set (char const *k, char const *s)
Public Member Functions inherited from object
 object (context &c)
virtual ~object ()=default
contextctx () const
Z3_error_code 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 542 of file z3++.h.

Constructor & Destructor Documentation

◆ params() [1/2]

params ( context & c)
inline

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

545: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...
void Z3_API Z3_params_inc_ref(Z3_context c, Z3_params p)
Increment the reference counter of the given parameter set.

Referenced by operator<<, operator=(), and params().

◆ params() [2/2]

params ( params const & s)
inline

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

546:object(s), m_params(s.m_params) { Z3_params_inc_ref(ctx(), m_params); }

◆ ~params()

~params ( )
inlineoverride

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

547{ Z3_params_dec_ref(ctx(), m_params); }
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 548 of file z3++.h.

548{ return m_params; }

◆ operator=()

params & operator= ( params const & s)
inline

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

549 {
550 Z3_params_inc_ref(s.ctx(), s.m_params);
551 Z3_params_dec_ref(ctx(), m_params);
552 object::operator=(s);
553 m_params = s.m_params;
554 return *this;
555 }

◆ set() [1/5]

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

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

556{ Z3_params_set_bool(ctx(), m_params, ctx().str_symbol(k), b); }
void Z3_API Z3_params_set_bool(Z3_context c, Z3_params p, Z3_symbol k, bool v)
Add a Boolean parameter k with value v to the parameter set p.

Referenced by solver::set(), solver::set(), solver::set(), solver::set(), and solver::set().

◆ set() [2/5]

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

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

560{ Z3_params_set_symbol(ctx(), m_params, ctx().str_symbol(k), ctx().str_symbol(s)); }
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.

◆ set() [3/5]

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

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

558{ Z3_params_set_double(ctx(), m_params, ctx().str_symbol(k), n); }
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/5]

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

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

559{ Z3_params_set_symbol(ctx(), m_params, ctx().str_symbol(k), s); }

◆ set() [5/5]

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

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

557{ 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.

◆ operator<<

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

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

564 {
565 out << Z3_params_to_string(p.ctx(), p); return out;
566 }
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...