Public Member Functions | Friends
tactic Class Reference
+ 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
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)
 object (object const &s)
contextctx () const
Z3_error_code check_error () const


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

Detailed Description

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

Constructor & Destructor Documentation

◆ tactic() [1/3]

tactic ( context c,
char const *  name 

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

2668 :object(c) { Z3_tactic r = Z3_mk_tactic(c, name); check_error(); init(r); }

◆ tactic() [2/3]

tactic ( context c,
Z3_tactic  s 

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

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

◆ tactic() [3/3]

tactic ( tactic const &  s)

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

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

◆ ~tactic()

~tactic ( )

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

2671 { Z3_tactic_dec_ref(ctx(), m_tactic); }

Member Function Documentation

◆ apply()

apply_result apply ( goal const &  g) const

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

2681  {
2682  check_context(*this, g);
2683  Z3_apply_result r = Z3_tactic_apply(ctx(), m_tactic, g);
2684  check_error();
2685  return apply_result(ctx(), r);
2686  }

Referenced by tactic::operator()().

◆ get_param_descrs()

param_descrs get_param_descrs ( )

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

2698 { return param_descrs(ctx(), Z3_tactic_get_param_descrs(ctx(), m_tactic)); }

◆ help()

std::string help ( ) const

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

2690 { char const * r = Z3_tactic_get_help(ctx(), m_tactic); check_error(); return r; }

◆ mk_solver()

solver mk_solver ( ) const

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

2680 { Z3_solver r = Z3_mk_solver_from_tactic(ctx(), m_tactic); check_error(); return solver(ctx(), r); }

◆ operator Z3_tactic()

operator Z3_tactic ( ) const

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

2672 { return m_tactic; }

◆ operator()()

apply_result operator() ( goal const &  g) const

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

2687  {
2688  return apply(g);
2689  }

◆ operator=()

tactic& operator= ( tactic const &  s)

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

2673  {
2674  Z3_tactic_inc_ref(s.ctx(), s.m_tactic);
2675  Z3_tactic_dec_ref(ctx(), m_tactic);
2676  m_ctx = s.m_ctx;
2677  m_tactic = s.m_tactic;
2678  return *this;
2679  }

Friends And Related Function Documentation

◆ operator&

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

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

2701  {
2702  check_context(t1, t2);
2703  Z3_tactic r = Z3_tactic_and_then(t1.ctx(), t1, t2);
2704  t1.check_error();
2705  return tactic(t1.ctx(), r);
2706  }

◆ operator|

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

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

2708  {
2709  check_context(t1, t2);
2710  Z3_tactic r = Z3_tactic_or_else(t1.ctx(), t1, t2);
2711  t1.check_error();
2712  return tactic(t1.ctx(), r);
2713  }

◆ par_and_then

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

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

2740  {
2741  check_context(t1, t2);
2742  Z3_tactic r = Z3_tactic_par_and_then(t1.ctx(), t1, t2);
2743  t1.check_error();
2744  return tactic(t1.ctx(), r);
2745  }

◆ par_or

tactic par_or ( unsigned  n,
tactic const *  tactics 

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

2731  {
2732  if (n == 0) {
2733  Z3_THROW(exception("a non-zero number of tactics need to be passed to par_or"));
2734  }
2735  array<Z3_tactic> buffer(n);
2736  for (unsigned i = 0; i < n; ++i) buffer[i] = tactics[i];
2737  return tactic(tactics[0].ctx(), Z3_tactic_par_or(tactics[0].ctx(), n, buffer.ptr()));
2738  }

◆ repeat

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

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

2715  {
2716  Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
2717  t.check_error();
2718  return tactic(t.ctx(), r);
2719  }

◆ try_for

tactic try_for ( tactic const &  t,
unsigned  ms 

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

2726  {
2727  Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
2728  t.check_error();
2729  return tactic(t.ctx(), r);
2730  }

◆ with

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

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

2721  {
2722  Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
2723  t.check_error();
2724  return tactic(t.ctx(), r);
2725  }
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...
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....
void Z3_API Z3_tactic_inc_ref(Z3_context c, Z3_tactic t)
Increment the reference counter of the given tactic.
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...
#define Z3_THROW(x)
Definition: z3++.h:99
def tactics(ctx=None)
Definition: z3py.py:7929
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...
apply_result apply(goal const &g) const
Definition: z3++.h:2681
void Z3_API Z3_tactic_dec_ref(Z3_context c, Z3_tactic g)
Decrement the reference counter of the given tactic.
object(context &c)
Definition: z3++.h:416
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.
context * m_ctx
Definition: z3++.h:414
Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g)
Apply tactic t to the goal g.
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...
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.
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.
expr max(expr const &a, expr const &b)
Definition: z3++.h:1724
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.
friend void check_context(object const &a, object const &b)
Definition: z3++.h:422
tactic(context &c, char const *name)
Definition: z3++.h:2668
Z3_error_code check_error() const
Definition: z3++.h:419
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.
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...
context & ctx() const
Definition: z3++.h:418