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 ()
 
 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)
 
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 3129 of file z3++.h.

Constructor & Destructor Documentation

simplifier ( context c,
char const *  name 
)
inline

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

3136 :object(c) { Z3_simplifier r = Z3_mk_simplifier(c, name); check_error(); init(r); }
Z3_error_code check_error() const
Definition: z3++.h:474
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 ( context c,
Z3_simplifier  s 
)
inline

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

3137 :object(c) { init(s); }
object(context &c)
Definition: z3++.h:472
simplifier ( simplifier const &  s)
inline

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

3138 :object(s) { init(s.m_simplifier); }
object(context &c)
Definition: z3++.h:472
~simplifier ( )
inline

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

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

Member Function Documentation

param_descrs get_param_descrs ( )
inline

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

3151 { 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.
context & ctx() const
Definition: z3++.h:473
std::string help ( ) const
inline

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

3148 { 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.
Z3_error_code check_error() const
Definition: z3++.h:474
context & ctx() const
Definition: z3++.h:473
operator Z3_simplifier ( ) const
inline

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

3140 { return m_simplifier; }
simplifier& operator= ( simplifier const &  s)
inline

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

3141  {
3142  Z3_simplifier_inc_ref(s.ctx(), s.m_simplifier);
3143  Z3_simplifier_dec_ref(ctx(), m_simplifier);
3144  object::operator=(s);
3145  m_simplifier = s.m_simplifier;
3146  return *this;
3147  }
void Z3_API Z3_simplifier_dec_ref(Z3_context c, Z3_simplifier g)
Decrement the reference counter of the given simplifier.
context & ctx() const
Definition: z3++.h:473
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

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

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

3157  {
3158  check_context(t1, t2);
3159  Z3_simplifier r = Z3_simplifier_and_then(t1.ctx(), t1, t2);
3160  t1.check_error();
3161  return simplifier(t1.ctx(), r);
3162  }
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...
friend void check_context(object const &a, object const &b)
Definition: z3++.h:477
simplifier(context &c, char const *name)
Definition: z3++.h:3136
simplifier with ( simplifier const &  t,
params const &  p 
)
friend

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

3164  {
3165  Z3_simplifier r = Z3_simplifier_using_params(t.ctx(), t, p);
3166  t.check_error();
3167  return simplifier(t.ctx(), r);
3168  }
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.
simplifier(context &c, char const *name)
Definition: z3++.h:3136