Struct z3::Tactic

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

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

Z3 provides a variety of tactics, which can be queried via Tactic::list_all(). Individual tactics can be created via Tactic::new().

Various combinators are available to combine tactics:

• Tactic::repeat()
• Tactic::try_for()
• Tactic::and_then()
• Tactic::or_else()
• Tactic::probe_or_else()
• Tactic::when()
• Tactic::cond()

Finally, a solver utilizing a tactic can be created via Tactic::solver().

Implementations

impl<'ctx> Tactic<'ctx>

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

Iterate through the valid tactic names.

Example

use z3::{Config, Context, Tactic};

let cfg = Config::new();
let ctx = Context::new(&cfg);
let tactics: Vec<_> = Tactic::list_all(&ctx).filter_map(|r| r.ok()).collect();
assert!(tactics.contains(&"ufbv"));

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

Create a tactic by name.

Example

use z3::{Config, Context, Tactic};

let cfg = Config::new();
let ctx = Context::new(&cfg);
let tactic = Tactic::new(&ctx, "nlsat");

See also

• Tactic::list_all()

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 try_for(&self, timeout: Duration) -> Tactic<'ctx>

Return a tactic that applies the current tactic to a given goal, failing if it doesn’t terminate within the period specified by timeout.

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>> ) -> Result<ApplyResult<'ctx>, String>

Attempts to apply the tactic to goal. If the tactic succeeds, returns Ok(_) with a ApplyResult. If the tactic fails, returns Err(_) with an error message describing why.

pub fn solver(&self) -> Solver<'ctx>

Create a new solver that is implemented using the given tactic.

Example

use z3::{ast, Config, Context, SatResult, Tactic};

let cfg = Config::new();
let ctx = Context::new(&cfg);
let tactic = Tactic::new(&ctx, "qfnra");
let solver = tactic.solver();

let x = ast::Int::new_const(&ctx, "x");
let y = ast::Int::new_const(&ctx, "y");

solver.assert(&x.gt(&y));
assert_eq!(solver.check(), SatResult::Sat);

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.