#include <z3++.h>
Definition at line 3083 of file z3++.h.
◆ tactic() [1/3]
Definition at line 3090 of file z3++.h.
3090:object(c) { Z3_tactic r =
Z3_mk_tactic(c, name); check_error(); init(r); }
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...
Referenced by operator&, operator=(), operator|, par_and_then, par_or, repeat, tactic(), try_for, and with.
◆ tactic() [2/3]
Definition at line 3091 of file z3++.h.
3091:object(c) { init(s); }
◆ tactic() [3/3]
Definition at line 3092 of file z3++.h.
3092:object(s) { init(s.m_tactic); }
◆ ~tactic()
Definition at line 3093 of file z3++.h.
void Z3_API Z3_tactic_dec_ref(Z3_context c, Z3_tactic g)
Decrement the reference counter of the given tactic.
◆ apply()
Definition at line 3103 of file z3++.h.
3103 {
3106 check_error();
3107 return apply_result(ctx(), r);
3108 }
Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g)
Apply tactic t to the goal g.
void check_context(object const &a, object const &b)
Referenced by operator()().
◆ get_param_descrs()
Definition at line 3120 of file z3++.h.
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.
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()
Definition at line 3102 of file z3++.h.
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 |
◆ operator()()
Definition at line 3109 of file z3++.h.
3109 {
3110 return apply(g);
3111 }
◆ operator=()
Definition at line 3095 of file z3++.h.
3095 {
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.
◆ operator&
Definition at line 3123 of file z3++.h.
3123 {
3126 t1.check_error();
3127 return tactic(t1.ctx(), r);
3128 }
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|
Definition at line 3130 of file z3++.h.
3130 {
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
Definition at line 3162 of file z3++.h.
3162 {
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
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.
◆ repeat
Definition at line 3137 of file z3++.h.
3137 {
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...
◆ try_for
Definition at line 3148 of file z3++.h.
3148 {
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
Definition at line 3143 of file z3++.h.
3143 {
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.