Definition at line 3083 of file z3++.h.
◆ tactic() [1/3] ◆ tactic() [2/3] ◆ tactic() [3/3] ◆ ~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.
3107 returnapply_result(
ctx(), r);
friend void check_context(object const &a, object const &b)
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::__call__(), and tactic::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 inlineDefinition 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 inlineDefinition at line 3094 of file z3++.h.
3094{
returnm_tactic; }
◆ operator()()Definition at line 3109 of file z3++.h.
apply_result apply(goal const &g) const
◆ operator=()Definition at line 3095 of file z3++.h.
3098object::operator=(s);
3099m_tactic = s.m_tactic;
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.
3127 return tactic(t1.ctx(), r);
tactic(context &c, char const *name)
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.
3134 return tactic(t1.ctx(), r);
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_thenDefinition at line 3162 of file z3++.h.
3166 return tactic(t1.ctx(), r);
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_orDefinition at line 3153 of file z3++.h.
3155 Z3_THROW(exception(
"a non-zero number of tactics need to be passed to par_or"));
3157array<Z3_tactic> buffer(n);
3158 for(
unsignedi = 0; i < n; ++i) buffer[i] =
tactics[i];
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.
◆ repeatDefinition at line 3137 of file z3++.h.
3140 return tactic(t.ctx(), r);
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)
◆ try_forDefinition at line 3148 of file z3++.h.
3151 return tactic(t.ctx(), r);
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...
◆ withDefinition at line 3143 of file z3++.h.
3146 return tactic(t.ctx(), r);
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.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4