Struct z3::Tactic

pub struct Tactic<'ctx> { /* fields omitted */ }

Basic building block for creating custom solvers for specific problem domains.

Implementations

impl<'ctx> Tactic<'ctx>

pub fn list_all(
    ctx: &'ctx Context
) -> impl Iterator<Item = Result<&'ctx str, Utf8Error>>

pub fn new(ctx: &'ctx Context, name: &str) -> Tactic<'ctx>

pub fn create_skip(ctx: &'ctx Context) -> Tactic<'ctx>

Return a tactic that just return the given goal.

pub fn create_fail(ctx: &'ctx Context) -> Tactic<'ctx>

Return a tactic that always fails.

pub fn repeat(ctx: &'ctx Context, t: &Tactic<'ctx>, max: u32) -> Tactic<'ctx>

Return a tactic that keeps applying t until the goal is not modified anymore or the maximum number of iterations max is reached.

pub fn and_then(&self, then_tactic: &Tactic<'ctx>) -> Tactic<'ctx>

Return a tactic that applies the current tactic to a given goal and the then_tactic to every subgoal produced by the original tactic.

pub fn or_else(&self, else_tactic: &Tactic<'ctx>) -> Tactic<'ctx>

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.

pub fn probe_or_else(&self, p: &Probe<'ctx>, t: &Tactic<'ctx>) -> Tactic<'ctx>

Return a tactic that applies self to a given goal if the probe p evaluates to true, and t if p evaluates to false.

pub fn when(&self, p: &Probe<'ctx>) -> Tactic<'ctx>

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.

pub fn cond(
    ctx: &'ctx Context,
    p: &Probe<'ctx>,
    t1: &Tactic<'ctx>,
    t2: &Tactic<'ctx>
) -> Tactic<'ctx>

Return a tactic that applies t1 to a given goal if the probe p evaluates to true, and t2 if p evaluates to false.

pub fn fail_if(ctx: &'ctx Context, p: &Probe<'ctx>) -> Tactic<'ctx>

Return a tactic that fails if the probe p evaluates to false.

pub fn apply(
    &self,
    goal: &Goal<'ctx>,
    params: Option<&Params<'ctx>>
) -> ApplyResult<'ctx>

Trait Implementations

impl<'ctx> Debug for Tactic<'ctx>

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl<'ctx> Display for Tactic<'ctx>

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl<'ctx> Drop for Tactic<'ctx>

fn drop(&mut self)

Executes the destructor for this type.