#include <z3++.h>
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 () |
![]() | |
object (context &c) | |
object (object const &s) | |
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 | |
![]() | |
context * | m_ctx |
Definition at line 2599 of file z3++.h.
Referenced by Tactic::__deepcopy__(), Tactic::__del__(), Tactic::apply(), Tactic::help(), Tactic::param_descrs(), and Tactic::solver().
Definition at line 2600 of file z3++.h.
Referenced by Tactic::__deepcopy__(), Tactic::__del__(), Tactic::apply(), Tactic::help(), Tactic::param_descrs(), and Tactic::solver().
Definition at line 2601 of file z3++.h.
Referenced by Tactic::__deepcopy__(), Tactic::__del__(), Tactic::apply(), Tactic::help(), Tactic::param_descrs(), and Tactic::solver().
|
inline |
|
inline |
Definition at line 2612 of file z3++.h.
Referenced by Tactic::__call__(), and tactic::operator()().
|
inline |
|
inline |
|
inline |
Definition at line 2611 of file z3++.h.
|
inline |
|
inline |
Definition at line 2604 of file z3++.h.
Definition at line 2632 of file z3++.h.
Definition at line 2639 of file z3++.h.
Definition at line 2671 of file z3++.h.
Definition at line 2657 of file z3++.h.
Definition at line 2652 of file z3++.h.