Public Member Functions | |
tactic (context &c, char const *name) | |
tactic (context &c, Z3_tactic s) | |
tactic (tactic const &s) | |
~tactic () override | |
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) | |
virtual | ~object ()=default |
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 |
Definition at line 3090 of file z3++.h.
Referenced by Tactic::__deepcopy__(), Tactic::__del__(), Tactic::apply(), Tactic::help(), Tactic::param_descrs(), and Tactic::solver().
Definition at line 3091 of file z3++.h.
Referenced by Tactic::__deepcopy__(), Tactic::__del__(), Tactic::apply(), Tactic::help(), Tactic::param_descrs(), and Tactic::solver().
Definition at line 3092 of file z3++.h.
Referenced by Tactic::__deepcopy__(), Tactic::__del__(), Tactic::apply(), Tactic::help(), Tactic::param_descrs(), and Tactic::solver().
|
inlineoverride |
|
inline |
Definition at line 3103 of file z3++.h.
Referenced by Tactic::__call__(), and tactic::operator()().
|
inline |
|
inline |
|
inline |
Definition at line 3102 of file z3++.h.
|
inline |
|
inline |