Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Friends
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
tacticoperator= (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);
    }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines