Z3
Public Member Functions | Friends
simplifier Class Reference
+ 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 ...

Referenced by Simplifier::__deepcopy__(), Simplifier::__del__(), Simplifier::add(), Simplifier::help(), Simplifier::param_descrs(), and Simplifier::using_params().

◆ simplifier() [2/3]

simplifier ( context c,
Z3_simplifier  s 
)
inline

◆ simplifier() [3/3]

simplifier ( simplifier const &  s)
inline

◆ ~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 Function 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.