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
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)

---

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.

:object(c) { Z3_tactic r = Z3_mk_tactic(c, name); check_error(); init(r); }

tactic	(	context &	c,
		Z3_tactic	s
	)		[inline]

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

:object(c) { init(s); }

tactic

(

tactic const &

s

)

[inline]

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

:object(s) { init(s.m_tactic); }

~tactic

(

)

[inline]

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

{ Z3_tactic_dec_ref(ctx(), m_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()().

                                                 { 
            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; }

solver mk_solver

(

)

const [inline]

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);  }

operator Z3_tactic

(

)

const [inline]

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

{ return m_tactic; }

apply_result operator()

(

goal const &

g

)

const [inline]

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

                                                      {
            return apply(g);
        }

tactic& operator=

(

tactic const &

s

)

[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; 
        }

---

Friends And Related Function Documentation

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

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);
        }

tactic operator|	(	tactic const &	t1,
		tactic const &	t2
	)		[friend]

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);
        }

tactic repeat	(	tactic const &	t,
		unsigned	max = UINT_MAX
	)		[friend]

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);
    }

tactic try_for	(	tactic const &	t,
		unsigned	ms
	)		[friend]

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);
    }

tactic with	(	tactic const &	t,
		params const &	p
	)		[friend]

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

                                                           {
        Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
        t.check_error();
        return tactic(t.ctx(), r);
    }