tactic Class Reference

#include <z3++.h>

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=UINT_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 3439 of file z3++.h.

Constructor & Destructor Documentation

tactic() [1/3]

tactic ( context & c, char const * name )

inline

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

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

Referenced by z3::cond(), z3::fail_if(), operator&, operator=(), operator|, par_and_then, par_or, repeat, tactic(), try_for, z3::when(), and with.

tactic() [2/3]

tactic ( context & c, Z3_tactic s )

inline

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

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

tactic() [3/3]

tactic ( tactic const & s )

inline

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

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

~tactic()

~tactic ( )

inlineoverride

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

{ Z3_tactic_dec_ref(ctx(), m_tactic); }

Member Function Documentation

apply()

apply_result apply ( goal const & g ) const

inline

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

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

Referenced by operator()().

get_param_descrs()

param_descrs get_param_descrs ( )

inline

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

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

help()

std::string help ( ) const

inline

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

{ char const * r = Z3_tactic_get_help(ctx(), m_tactic); check_error();  return r; }

mk_solver()

solver mk_solver ( ) const

inline

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

{ Z3_solver r = Z3_mk_solver_from_tactic(ctx(), m_tactic); check_error(); return solver(ctx(), r);  }

operator Z3_tactic()

operator Z3_tactic ( ) const

inline

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

{ return m_tactic; }

operator()()

apply_result operator() ( goal const & g ) const

inline

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

                                                      {
            return apply(g);
        }

operator=()

tactic & operator= ( tactic const & s )

inline

Definition at line 3451 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 Symbol Documentation

operator&

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

friend

Definition at line 3479 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);
    }

Referenced by operator&.

operator|

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

friend

Definition at line 3486 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);
    }

Referenced by operator|.

par_and_then

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

friend

Definition at line 3518 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);
    }

Referenced by par_and_then.

par_or

tactic par_or ( unsigned n, tactic const * tactics )

friend

Definition at line 3509 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()));
    }

Referenced by par_or.

repeat

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

friend

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

                                                                {
        Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
        t.check_error();
        return tactic(t.ctx(), r);
    }

Referenced by repeat.

try_for

tactic try_for ( tactic const & t, unsigned ms )

friend

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

                                                         {
        Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
        t.check_error();
        return tactic(t.ctx(), r);
    }

Referenced by try_for.

with

tactic with ( tactic const & t, params const & p )

friend

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

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

Referenced by with.