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 |
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) |
Definition at line 1400 of file z3++.h.
:object(c) { Z3_tactic r = Z3_mk_tactic(c, name); check_error(); init(r); }
~tactic | ( | ) | [inline] |
Definition at line 1403 of file z3++.h.
{ Z3_tactic_dec_ref(ctx(), m_tactic); }
apply_result apply | ( | goal const & | g | ) | const [inline] |
Definition at line 1413 of file z3++.h.
Referenced by Tactic::__call__(), and tactic::operator()().
{ check_context(*this, g); Z3_apply_result r = Z3_tactic_apply(ctx(), m_tactic, g); check_error(); return apply_result(ctx(), r); }
std::string help | ( | ) | const [inline] |
Definition at line 1422 of file z3++.h.
{ char const * r = Z3_tactic_get_help(ctx(), m_tactic); check_error(); return r; }
Definition at line 1412 of file z3++.h.
{ Z3_solver r = Z3_mk_solver_from_tactic(ctx(), m_tactic); check_error(); return solver(ctx(), r); }
apply_result operator() | ( | goal const & | g | ) | const [inline] |
Definition at line 1405 of file z3++.h.
{ Z3_tactic_inc_ref(s.ctx(), s.m_tactic); Z3_tactic_dec_ref(ctx(), m_tactic); m_ctx = s.m_ctx; m_tactic = s.m_tactic; return *this; }
Definition at line 1423 of file z3++.h.
{ check_context(t1, t2); Z3_tactic r = Z3_tactic_and_then(t1.ctx(), t1, t2); t1.check_error(); return tactic(t1.ctx(), r); }
Definition at line 1429 of file z3++.h.
{ check_context(t1, t2); Z3_tactic r = Z3_tactic_or_else(t1.ctx(), t1, t2); t1.check_error(); return tactic(t1.ctx(), r); }
Definition at line 1440 of file z3++.h.
{ Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max); t.check_error(); return tactic(t.ctx(), r); }
Definition at line 1451 of file z3++.h.
{ Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms); t.check_error(); return tactic(t.ctx(), r); }