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

#include <z3++.h>

+ Inheritance diagram for tactic:

Public Member Functions

 tactic (context &c, char const *name)
 
 tactic (context &c, Z3_tactic s)
 
 tactic (tactic const &s)
 
 ~tactic () override
 
 operator Z3_tactic () const
 
tacticoperator= (tactic const &s)
 
solver mk_solver () const
 
apply_result apply (goal const &g) const
 
apply_result operator() (goal const &g) const
 
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

tactic operator& (tactic const &t1, tactic const &t2)
 
tactic operator| (tactic const &t1, tactic const &t2)
 
tactic repeat (tactic const &t, unsigned max=UINT_MAX)
 
tactic with (tactic const &t, params const &p)
 
tactic try_for (tactic const &t, unsigned ms)
 
tactic par_or (unsigned n, tactic const *tactics)
 
tactic par_and_then (tactic const &t1, tactic const &t2)
 

Additional Inherited Members

- Protected Attributes inherited from object
contextm_ctx
 

Detailed Description

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

Constructor & Destructor Documentation

◆ tactic() [1/3]

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

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

3090:object(c) { Z3_tactic r = Z3_mk_tactic(c, name); check_error(); init(r); }
Z3_error_code check_error() const
Definition z3++.h:475
object(context &c)
Definition z3++.h:472
Z3_tactic Z3_API Z3_mk_tactic(Z3_context c, Z3_string name)
Return a tactic associated with the given name. The complete list of tactics may be obtained using th...

◆ tactic() [2/3]

tactic ( context & c,
Z3_tactic s )
inline

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

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

◆ tactic() [3/3]

tactic ( tactic const & s)
inline

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

3092:object(s) { init(s.m_tactic); }

◆ ~tactic()

~tactic ( )
inlineoverride

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

3093{ Z3_tactic_dec_ref(ctx(), m_tactic); }
context & ctx() const
Definition z3++.h:474
void Z3_API Z3_tactic_dec_ref(Z3_context c, Z3_tactic g)
Decrement the reference counter of the given tactic.

Member Function Documentation

◆ apply()

apply_result apply ( goal const & g) const
inline

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

3103 {
3104 check_context(*this, g);
3105 Z3_apply_result r = Z3_tactic_apply(ctx(), m_tactic, g);
3106 check_error();
3107 return apply_result(ctx(), r);
3108 }
friend void check_context(object const &a, object const &b)
Definition z3++.h:478
Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g)
Apply tactic t to the goal g.

Referenced by tactic::operator()().

◆ get_param_descrs()

param_descrs get_param_descrs ( )
inline

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

3120{ return param_descrs(ctx(), Z3_tactic_get_param_descrs(ctx(), m_tactic)); }
Z3_param_descrs Z3_API Z3_tactic_get_param_descrs(Z3_context c, Z3_tactic t)
Return the parameter description set for the given tactic object.

◆ help()

std::string help ( ) const
inline

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

3112{ char const * r = Z3_tactic_get_help(ctx(), m_tactic); check_error(); return r; }
Z3_string Z3_API Z3_tactic_get_help(Z3_context c, Z3_tactic t)
Return a string containing a description of parameters accepted by the given tactic.

◆ mk_solver()

solver mk_solver ( ) const
inline

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

3102{ Z3_solver r = Z3_mk_solver_from_tactic(ctx(), m_tactic); check_error(); return solver(ctx(), r); }
Z3_solver Z3_API Z3_mk_solver_from_tactic(Z3_context c, Z3_tactic t)
Create a new solver that is implemented using the given tactic. The solver supports the commands Z3_s...

◆ operator Z3_tactic()

operator Z3_tactic ( ) const
inline

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

3094{ return m_tactic; }

◆ operator()()

apply_result operator() ( goal const & g) const
inline

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

3109 {
3110 return apply(g);
3111 }
apply_result apply(goal const &g) const
Definition z3++.h:3103

◆ operator=()

tactic & operator= ( tactic const & s)
inline

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

3095 {
3096 Z3_tactic_inc_ref(s.ctx(), s.m_tactic);
3097 Z3_tactic_dec_ref(ctx(), m_tactic);
3098 object::operator=(s);
3099 m_tactic = s.m_tactic;
3100 return *this;
3101 }
void Z3_API Z3_tactic_inc_ref(Z3_context c, Z3_tactic t)
Increment the reference counter of the given tactic.

Friends And Related Symbol Documentation

◆ operator&

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

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

3123 {
3124 check_context(t1, t2);
3125 Z3_tactic r = Z3_tactic_and_then(t1.ctx(), t1, t2);
3126 t1.check_error();
3127 return tactic(t1.ctx(), r);
3128 }
tactic(context &c, char const *name)
Definition z3++.h:3090
Z3_tactic Z3_API Z3_tactic_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal and t2 to every subgoal produced by t1.

◆ operator|

tactic operator| ( tactic const & t1,
tactic const & t2 )
friend

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

3130 {
3131 check_context(t1, t2);
3132 Z3_tactic r = Z3_tactic_or_else(t1.ctx(), t1, t2);
3133 t1.check_error();
3134 return tactic(t1.ctx(), r);
3135 }
Z3_tactic Z3_API Z3_tactic_or_else(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that first applies t1 to a given goal, if it fails then returns the result of t2 appl...

◆ par_and_then

tactic par_and_then ( tactic const & t1,
tactic const & t2 )
friend

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

3162 {
3163 check_context(t1, t2);
3164 Z3_tactic r = Z3_tactic_par_and_then(t1.ctx(), t1, t2);
3165 t1.check_error();
3166 return tactic(t1.ctx(), r);
3167 }
Z3_tactic Z3_API Z3_tactic_par_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1....

◆ par_or

tactic par_or ( unsigned n,
tactic const * tactics )
friend

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

3153 {
3154 if (n == 0) {
3155 Z3_THROW(exception("a non-zero number of tactics need to be passed to par_or"));
3156 }
3157 array<Z3_tactic> buffer(n);
3158 for (unsigned i = 0; i < n; ++i) buffer[i] = tactics[i];
3159 return tactic(tactics[0u].ctx(), Z3_tactic_par_or(tactics[0u].ctx(), n, buffer.ptr()));
3160 }
Z3_tactic Z3_API Z3_tactic_par_or(Z3_context c, unsigned num, Z3_tactic const ts[])
Return a tactic that applies the given tactics in parallel.
#define Z3_THROW(x)
Definition z3++.h:103

◆ repeat

tactic repeat ( tactic const & t,
unsigned max = UINT_MAX )
friend

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

3137 {
3138 Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
3139 t.check_error();
3140 return tactic(t.ctx(), r);
3141 }
Z3_tactic Z3_API Z3_tactic_repeat(Z3_context c, Z3_tactic t, unsigned max)
Return a tactic that keeps applying t until the goal is not modified anymore or the maximum number of...
expr max(expr const &a, expr const &b)
Definition z3++.h:1967

◆ try_for

tactic try_for ( tactic const & t,
unsigned ms )
friend

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

3148 {
3149 Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
3150 t.check_error();
3151 return tactic(t.ctx(), r);
3152 }
Z3_tactic Z3_API Z3_tactic_try_for(Z3_context c, Z3_tactic t, unsigned ms)
Return a tactic that applies t to a given goal for ms milliseconds. If t does not terminate in ms mil...

◆ with

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

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

3143 {
3144 Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
3145 t.check_error();
3146 return tactic(t.ctx(), r);
3147 }
Z3_tactic Z3_API Z3_tactic_using_params(Z3_context c, Z3_tactic t, Z3_params p)
Return a tactic that applies t using the given set of parameters.