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

#include <z3++.h>

+ Inheritance diagram for simplifier:

Public Member Functions

 simplifier (context &c, char const *name)
 
 simplifier (context &c, Z3_simplifier s)
 
 simplifier (simplifier const &s)
 
 ~simplifier () override
 
 operator Z3_simplifier () const
 
simplifieroperator= (simplifier const &s)
 
std::string help () const
 
param_descrs get_param_descrs ()
 
- Public Member Functions inherited from object
 object (context &c)
 
virtual ~object ()=default
 
contextctx () const
 
Z3_error_code check_error () const
 

Friends

simplifier operator& (simplifier const &t1, simplifier const &t2)
 
simplifier with (simplifier const &t, params const &p)
 

Additional Inherited Members

- Protected Attributes inherited from object
contextm_ctx
 

Detailed Description

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

Constructor & Destructor Documentation

◆ simplifier() [1/3]

simplifier ( context & c,
char const * name )
inline

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

3176:object(c) { Z3_simplifier r = Z3_mk_simplifier(c, name); check_error(); init(r); }
Z3_error_code check_error() const
Definition z3++.h:475
object(context &c)
Definition z3++.h:472
Z3_simplifier Z3_API Z3_mk_simplifier(Z3_context c, Z3_string name)
Return a simplifier associated with the given name. The complete list of simplifiers may be obtained ...

◆ simplifier() [2/3]

simplifier ( context & c,
Z3_simplifier s )
inline

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

3177:object(c) { init(s); }

◆ simplifier() [3/3]

simplifier ( simplifier const & s)
inline

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

3178:object(s) { init(s.m_simplifier); }

◆ ~simplifier()

~simplifier ( )
inlineoverride

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

3179{ Z3_simplifier_dec_ref(ctx(), m_simplifier); }
context & ctx() const
Definition z3++.h:474
void Z3_API Z3_simplifier_dec_ref(Z3_context c, Z3_simplifier g)
Decrement the reference counter of the given simplifier.

Member Function Documentation

◆ get_param_descrs()

param_descrs get_param_descrs ( )
inline

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

3191{ return param_descrs(ctx(), Z3_simplifier_get_param_descrs(ctx(), m_simplifier)); }
Z3_param_descrs Z3_API Z3_simplifier_get_param_descrs(Z3_context c, Z3_simplifier t)
Return the parameter description set for the given simplifier object.

◆ help()

std::string help ( ) const
inline

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

3188{ char const * r = Z3_simplifier_get_help(ctx(), m_simplifier); check_error(); return r; }
Z3_string Z3_API Z3_simplifier_get_help(Z3_context c, Z3_simplifier t)
Return a string containing a description of parameters accepted by the given simplifier.

◆ operator Z3_simplifier()

operator Z3_simplifier ( ) const
inline

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

3180{ return m_simplifier; }

◆ operator=()

simplifier & operator= ( simplifier const & s)
inline

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

3181 {
3182 Z3_simplifier_inc_ref(s.ctx(), s.m_simplifier);
3183 Z3_simplifier_dec_ref(ctx(), m_simplifier);
3184 object::operator=(s);
3185 m_simplifier = s.m_simplifier;
3186 return *this;
3187 }
void Z3_API Z3_simplifier_inc_ref(Z3_context c, Z3_simplifier t)
Increment the reference counter of the given simplifier.

Friends And Related Symbol Documentation

◆ operator&

simplifier operator& ( simplifier const & t1,
simplifier const & t2 )
friend

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

3197 {
3198 check_context(t1, t2);
3199 Z3_simplifier r = Z3_simplifier_and_then(t1.ctx(), t1, t2);
3200 t1.check_error();
3201 return simplifier(t1.ctx(), r);
3202 }
friend void check_context(object const &a, object const &b)
Definition z3++.h:478
simplifier(context &c, char const *name)
Definition z3++.h:3176
Z3_simplifier Z3_API Z3_simplifier_and_then(Z3_context c, Z3_simplifier t1, Z3_simplifier t2)
Return a simplifier that applies t1 to a given goal and t2 to every subgoal produced by t1.

◆ with

simplifier with ( simplifier const & t,
params const & p )
friend

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

3204 {
3205 Z3_simplifier r = Z3_simplifier_using_params(t.ctx(), t, p);
3206 t.check_error();
3207 return simplifier(t.ctx(), r);
3208 }
Z3_simplifier Z3_API Z3_simplifier_using_params(Z3_context c, Z3_simplifier t, Z3_params p)
Return a simplifier that applies t using the given set of parameters.