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

Detailed Description

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

Constructor & Destructor Documentation

tactic ( context &  c, char const *  name  )

inline

Definition at line 3260 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 3261 of file z3++.h.

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

tactic ( tactic const &  s )

inline

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

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

~tactic ( )

inlineoverride

Definition at line 3263 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 3273 of file z3++.h.

Referenced by tactic::operator()().

                                                 {
            check_context(*this, g);
            Z3_apply_result r = Z3_tactic_apply(ctx(), m_tactic, g);
            check_error();
            return apply_result(ctx(), r);
        }

param_descrs get_param_descrs ( )

inline

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

{ return param_descrs(ctx(), Z3_tactic_get_param_descrs(ctx(), m_tactic)); }

std::string help ( ) const

inline

Definition at line 3282 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 3272 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 3264 of file z3++.h.

{ return m_tactic; }

apply_result operator() ( goal const &  g ) const

inline

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

                                                      {
            return apply(g);
        }

tactic& operator= ( tactic const &  s )

inline

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

                                             {
            Z3_tactic_inc_ref(s.ctx(), s.m_tactic);
            Z3_tactic_dec_ref(ctx(), m_tactic);
            object::operator=(s);
            m_tactic = s.m_tactic;
            return *this;
        }

Friends And Related Function Documentation

tactic operator& ( tactic const &  t1, tactic const &  t2  )

friend

Definition at line 3293 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 3300 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 par_and_then ( tactic const &  t1, tactic const &  t2  )

friend

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

                                                                     {
        check_context(t1, t2);
        Z3_tactic r = Z3_tactic_par_and_then(t1.ctx(), t1, t2);
        t1.check_error();
        return tactic(t1.ctx(), r);
    }

tactic par_or ( unsigned  n, tactic const *  tactics  )

friend

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

                                                            {
        if (n == 0) {
            Z3_THROW(exception("a non-zero number of tactics need to be passed to par_or"));
        }
        array<Z3_tactic> buffer(n);
        for (unsigned i = 0; i < n; ++i) buffer[i] = tactics[i];
        return tactic(tactics[0u].ctx(), Z3_tactic_par_or(tactics[0u].ctx(), n, buffer.ptr()));
    }

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

friend

Definition at line 3307 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 3318 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 3313 of file z3++.h.

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