Struct Tactic 

pub struct Tactic { /* 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 Tactic

pub fn list_all() -> Vec<Result<String, Utf8Error>>

Iterate through the valid tactic names.

Example

let tactics: Vec<_> = Tactic::list_all().into_iter().filter_map(|r| r.ok()).collect();
assert!(tactics.contains(&"ufbv".to_string()));

pub fn new(name: &str) -> Tactic

Create a tactic by name.

Example

let tactic = Tactic::new("nlsat");

See also

• Tactic::list_all()

pub fn create_skip() -> Tactic

Return a tactic that just return the given goal.

pub fn create_fail() -> Tactic

Return a tactic that always fails.

pub fn repeat(t: &Tactic, max: u32) -> Tactic

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

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) -> Tactic

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) -> 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.

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

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) -> Tactic

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(p: &Probe, t1: &Tactic, t2: &Tactic) -> 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.

pub fn fail_if(p: &Probe) -> Tactic

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

pub fn apply( &self, goal: &Goal, params: Option<&Params>, ) -> Result<ApplyResult, 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

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

Example

let tactic = Tactic::new("qfnra");
let solver = tactic.solver();

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

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

Trait Implementations

impl Debug for Tactic

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

Formats the value using the given formatter.

impl Display for Tactic

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

Formats the value using the given formatter.

impl Drop for Tactic

fn drop(&mut self)

Executes the destructor for this type.