Z3 |

Public Member Functions | Friends
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 ()
| operator Z3_tactic () const
tactic & | operator= (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)
context & | ctx () 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)
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
context * | m_ctx

## Detailed Description

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

## Constructor & Destructor Documentation

## ◆ tactic() [1/3]

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

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

2858:object(c) { Z3_tactic r = Z3_mk_tactic(c, name); check_error(); init(r); }
z3::object::check_error
Z3_error_code check_error() const
Definition: z3++.h:423
z3::object::object
object(context &c)
Definition: z3++.h:421
Z3_mk_tactic
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 Tactic::__deepcopy__(), Tactic::__del__(), Tactic::apply(), Tactic::help(), Tactic::param_descrs(), and Tactic::solver().

## ◆ tactic() [2/3]

tactic | ( | context & | c,
|  | Z3_tactic | s
| ) |  |
| inline

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

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

Referenced by Tactic::__deepcopy__(), Tactic::__del__(), Tactic::apply(), Tactic::help(), Tactic::param_descrs(), and Tactic::solver().

## ◆ tactic() [3/3]

tactic | ( | tactic const & | s | ) |
| inline

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

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

Referenced by Tactic::__deepcopy__(), Tactic::__del__(), Tactic::apply(), Tactic::help(), Tactic::param_descrs(), and Tactic::solver().

## ◆ ~tactic()

~tactic | ( |  | ) |
| inline

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

2861{ Z3_tactic_dec_ref(ctx(), m_tactic); }
z3::object::ctx
context & ctx() const
Definition: z3++.h:422
Z3_tactic_dec_ref
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 2871 of file z3++.h.

2871 {
2872 check_context(*this, g);
2873 Z3_apply_result r = Z3_tactic_apply(ctx(), m_tactic, g);
2874 check_error();
2875 return apply_result(ctx(), r);
2876 }
z3::object::check_context
friend void check_context(object const &a, object const &b)
Definition: z3++.h:426
Z3_tactic_apply
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()

param_descrs get_param_descrs | ( |  | ) |
| inline

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

2888{ return param_descrs(ctx(), Z3_tactic_get_param_descrs(ctx(), m_tactic)); }
Z3_tactic_get_param_descrs
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 2880 of file z3++.h.

2880{ char const * r = Z3_tactic_get_help(ctx(), m_tactic); check_error(); return r; }
Z3_tactic_get_help
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 2870 of file z3++.h.

2870{ Z3_solver r = Z3_mk_solver_from_tactic(ctx(), m_tactic); check_error(); return solver(ctx(), r); }
Z3_mk_solver_from_tactic
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 2862 of file z3++.h.

2862{ return m_tactic; }

## ◆ operator()()

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

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

2877 {
2878 return apply(g);
2879 }
z3::tactic::apply
apply_result apply(goal const &g) const
Definition: z3++.h:2871

## ◆ operator=()

tactic & operator= | ( | tactic const & | s | ) |
| inline

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

2863 {
2864 Z3_tactic_inc_ref(s.ctx(), s.m_tactic);
2865 Z3_tactic_dec_ref(ctx(), m_tactic);
2866 object::operator=(s);
2867 m_tactic = s.m_tactic;
2868 return *this;
2869 }
Z3_tactic_inc_ref
void Z3_API Z3_tactic_inc_ref(Z3_context c, Z3_tactic t)
Increment the reference counter of the given tactic.

## Friends And Related Function Documentation

## ◆ operator&

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

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

2891 {
2892 check_context(t1, t2);
2893 Z3_tactic r = Z3_tactic_and_then(t1.ctx(), t1, t2);
2894 t1.check_error();
2895 return tactic(t1.ctx(), r);
2896 }
z3::tactic::tactic
tactic(context &c, char const *name)
Definition: z3++.h:2858
Z3_tactic_and_then
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 2898 of file z3++.h.

2898 {
2899 check_context(t1, t2);
2900 Z3_tactic r = Z3_tactic_or_else(t1.ctx(), t1, t2);
2901 t1.check_error();
2902 return tactic(t1.ctx(), r);
2903 }
Z3_tactic_or_else
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 2930 of file z3++.h.

2930 {
2931 check_context(t1, t2);
2932 Z3_tactic r = Z3_tactic_par_and_then(t1.ctx(), t1, t2);
2933 t1.check_error();
2934 return tactic(t1.ctx(), r);
2935 }
Z3_tactic_par_and_then
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 2921 of file z3++.h.

2921 {
2922 if (n == 0) {
2923 Z3_THROW(exception("a non-zero number of tactics need to be passed to par_or"));
2924 }
2925 array<Z3_tactic> buffer(n);
2926 for (unsigned i = 0; i < n; ++i) buffer[i] = tactics[i];
2927 return tactic(tactics[0].ctx(), Z3_tactic_par_or(tactics[0].ctx(), n, buffer.ptr()));
2928 }
z3py.tactics
def tactics(ctx=None)
Definition: z3py.py:8323
Z3_THROW
#define Z3_THROW(x)
Definition: z3++.h:100
Z3_tactic_par_or
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

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

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

2905 {
2906 Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
2907 t.check_error();
2908 return tactic(t.ctx(), r);
2909 }
z3::max
expr max(expr const &a, expr const &b)
Definition: z3++.h:1836
Z3_tactic_repeat
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

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

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

2916 {
2917 Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
2918 t.check_error();
2919 return tactic(t.ctx(), r);
2920 }
Z3_tactic_try_for
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 2911 of file z3++.h.

2911 {
2912 Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
2913 t.check_error();
2914 return tactic(t.ctx(), r);
2915 }
Z3_tactic_using_params
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.