Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
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
 
- Public Member Functions inherited from object
 object (context &c)
 
 object (object const &s)
 
contextctx () const
 
void 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)
 

Additional Inherited Members

- Protected Attributes inherited from object
contextm_ctx
 

Detailed Description

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

Constructor & Destructor Documentation

tactic ( context c,
char const *  name 
)
inline

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

:object(c) { init(s); }
tactic ( tactic const &  s)
inline

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

:object(s) { init(s.m_tactic); }
~tactic ( )
inline

Definition at line 1287 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 1297 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);
return apply_result(ctx(), r);
}
std::string help ( ) const
inline

Definition at line 1306 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 1296 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 1288 of file z3++.h.

{ return m_tactic; }
apply_result operator() ( goal const &  g) const
inline

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

{
return apply(g);
}
tactic& operator= ( tactic const &  s)
inline

Definition at line 1289 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 1307 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 1313 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 1319 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 1329 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 1324 of file z3++.h.

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