Struct z3::Tactic [−][src]
pub struct Tactic<'ctx> { /* fields omitted */ }
Expand description
Basic building block for creating custom solvers for specific problem domains.
Implementations
Return a tactic that just return the given goal.
Return a tactic that always fails.
Return a tactic that keeps applying t
until the goal is not modified anymore or the maximum
number of iterations max
is reached.
Return a tactic that applies the current tactic to a given goal and
the then_tactic
to every subgoal produced by the original tactic.
Return a tactic that current tactic to a given goal,
if it fails then returns the result of else_tactic
applied to the given goal.
Return a tactic that applies self to a given goal if the probe p
evaluates to true,
and t
if p
evaluates to false.
Return a tactic that applies itself to a given goal if the probe p
evaluates to true.
If p
evaluates to false, then the new tactic behaves like the skip tactic.
Return a tactic that applies t1
to a given goal if the probe p
evaluates to true,
and t2
if p
evaluates to false.
Return a tactic that fails if the probe p
evaluates to false.
Trait Implementations
Auto Trait Implementations
impl<'ctx> RefUnwindSafe for Tactic<'ctx>
impl<'ctx> UnwindSafe for Tactic<'ctx>