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 |
![]() | |
object (context &c) | |
object (object const &s) | |
context & | ctx () 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 | |
![]() | |
context * | m_ctx |
|
inline |
|
inline |
Definition at line 1449 of file z3++.h.
Referenced by Tactic::__call__().
|
inline |
|
inline |
Definition at line 1448 of file z3++.h.
|
inline |
|
inline |
Definition at line 1459 of file z3++.h.
Definition at line 1465 of file z3++.h.