Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules Pages
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
 
- Public Member Functions inherited from object
 object (context &c)
 
 object (object const &s)
 
contextctx () const
 
void 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)
 

Additional Inherited Members

- Protected Attributes inherited from object
contextm_ctx
 

Detailed Description

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

Constructor & Destructor Documentation

tactic ( context c,
char const *  name 
)
inline

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

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

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

1401 :object(c) { init(s); }
object(context &c)
Definition: z3++.h:270
tactic ( tactic const &  s)
inline

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

1402 :object(s) { init(s.m_tactic); }
object(context &c)
Definition: z3++.h:270
~tactic ( )
inline

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

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

Member Function Documentation

apply_result apply ( goal const &  g) const
inline

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

Referenced by Tactic::__call__(), and tactic::operator()().

1413  {
1414  check_context(*this, g);
1415  Z3_apply_result r = Z3_tactic_apply(ctx(), m_tactic, g);
1416  check_error();
1417  return apply_result(ctx(), r);
1418  }
Z3_apply_result Z3_API Z3_tactic_apply(__in Z3_context c, __in Z3_tactic t, __in Z3_goal g)
Apply tactic t to the goal g.
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
std::string help ( ) const
inline

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

1422 { char const * r = Z3_tactic_get_help(ctx(), m_tactic); check_error(); return r; }
Z3_string Z3_API Z3_tactic_get_help(__in Z3_context c, __in Z3_tactic t)
Return a string containing a description of parameters accepted by the given tactic.
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
solver mk_solver ( ) const
inline

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

1412 { Z3_solver r = Z3_mk_solver_from_tactic(ctx(), m_tactic); check_error(); return solver(ctx(), r); }
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
Z3_solver Z3_API Z3_mk_solver_from_tactic(__in Z3_context c, __in Z3_tactic t)
Create a new solver that is implemented using the given tactic. The solver supports the commands Z3_s...
operator Z3_tactic ( ) const
inline

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

1404 { return m_tactic; }
apply_result operator() ( goal const &  g) const
inline

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

1419  {
1420  return apply(g);
1421  }
apply_result apply(goal const &g) const
Definition: z3++.h:1413
tactic& operator= ( tactic const &  s)
inline

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

1405  {
1406  Z3_tactic_inc_ref(s.ctx(), s.m_tactic);
1407  Z3_tactic_dec_ref(ctx(), m_tactic);
1408  m_ctx = s.m_ctx;
1409  m_tactic = s.m_tactic;
1410  return *this;
1411  }
context & ctx() const
Definition: z3++.h:272
void Z3_API Z3_tactic_dec_ref(__in Z3_context c, __in Z3_tactic g)
Decrement the reference counter of the given tactic.
context * m_ctx
Definition: z3++.h:268
void Z3_API Z3_tactic_inc_ref(__in Z3_context c, __in Z3_tactic t)
Increment the reference counter of the given tactic.

Friends And Related Function Documentation

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

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

1423  {
1424  check_context(t1, t2);
1425  Z3_tactic r = Z3_tactic_and_then(t1.ctx(), t1, t2);
1426  t1.check_error();
1427  return tactic(t1.ctx(), r);
1428  }
Z3_tactic Z3_API Z3_tactic_and_then(__in Z3_context c, __in Z3_tactic t1, __in Z3_tactic t2)
Return a tactic that applies t1 to a given goal and t2 to every subgoal produced by t1...
tactic(context &c, char const *name)
Definition: z3++.h:1400
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
tactic operator| ( tactic const &  t1,
tactic const &  t2 
)
friend

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

1429  {
1430  check_context(t1, t2);
1431  Z3_tactic r = Z3_tactic_or_else(t1.ctx(), t1, t2);
1432  t1.check_error();
1433  return tactic(t1.ctx(), r);
1434  }
tactic(context &c, char const *name)
Definition: z3++.h:1400
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
Z3_tactic Z3_API Z3_tactic_or_else(__in Z3_context c, __in Z3_tactic t1, __in Z3_tactic t2)
Return a tactic that first applies t1 to a given goal, if it fails then returns the result of t2 appl...
tactic repeat ( tactic const &  t,
unsigned  max = UINT_MAX 
)
friend

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

1440  {
1441  Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
1442  t.check_error();
1443  return tactic(t.ctx(), r);
1444  }
Z3_tactic Z3_API Z3_tactic_repeat(__in Z3_context c, __in Z3_tactic t, unsigned max)
Return a tactic that keeps applying t until the goal is not modified anymore or the maximum number of...
tactic(context &c, char const *name)
Definition: z3++.h:1400
tactic try_for ( tactic const &  t,
unsigned  ms 
)
friend

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

1451  {
1452  Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
1453  t.check_error();
1454  return tactic(t.ctx(), r);
1455  }
Z3_tactic Z3_API Z3_tactic_try_for(__in Z3_context c, __in Z3_tactic t, __in unsigned ms)
Return a tactic that applies t to a given goal for ms milliseconds. If t does not terminate in ms mil...
tactic(context &c, char const *name)
Definition: z3++.h:1400
tactic with ( tactic const &  t,
params const &  p 
)
friend

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

1446  {
1447  Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
1448  t.check_error();
1449  return tactic(t.ctx(), r);
1450  }
Z3_tactic Z3_API Z3_tactic_using_params(__in Z3_context c, __in Z3_tactic t, __in Z3_params p)
Return a tactic that applies t using the given set of parameters.
tactic(context &c, char const *name)
Definition: z3++.h:1400