Struct z3::Probe

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

Function/predicate used to inspect a goal and collect information that may be used to decide which solver and/or preprocessing step will be used.

Z3 provides a variety of probes, which can be queried via Probe::list_all().

Implementations

impl<'ctx> Probe<'ctx>

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

Iterate through the valid probe names.

Example

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

let cfg = Config::new();
let ctx = Context::new(&cfg);
let probes: Vec<_> = Probe::list_all(&ctx).filter_map(|r| r.ok()).collect();
assert!(probes.contains(&"is-quasi-pb"));

pub fn describe(ctx: &'ctx Context, name: &str) -> Result<&'ctx str, Utf8Error>

Return a string containing a description of the probe with the given name.

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

Return a probe associated with the given name.

Example

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

let cfg = Config::new();
let ctx = Context::new(&cfg);
let probe = Probe::new(&ctx, "is-qfbv");

pub fn apply(&self, goal: &'ctx Goal<'_>) -> f64

Execute the probe over the goal.

The probe always produce a double value. “Boolean” probes return 0.0 for false, and a value different from 0.0 for true.

pub fn constant(ctx: &'ctx Context, val: f64) -> Probe<'ctx>

Return a probe that always evaluates to val.

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

let cfg = Config::new();
let ctx = Context::new(&cfg);
let probe = Probe::constant(&ctx, 1.0);

pub fn lt(&self, p: Probe<'_>) -> Probe<'ctx>

Return a probe that evaluates to “true” when the value returned by self is less than the value returned by p.

NOTE: For probes, “true” is any value different from 0.0.

pub fn gt(&self, p: &Probe<'_>) -> Probe<'ctx>

Return a probe that evaluates to “true” when the value returned by self is greater than the value returned by p.

pub fn le(&self, p: &Probe<'_>) -> Probe<'ctx>

Return a probe that evaluates to “true” when the value returned by self is less than or equal to the value returned by p.

pub fn ge(&self, p: &Probe<'_>) -> Probe<'ctx>

Return a probe that evaluates to “true” when the value returned by self is greater than or equal to the value returned by p.

pub fn eq(&self, p: &Probe<'_>) -> Probe<'ctx>

Return a probe that evaluates to “true” when the value returned by self is equal to the value returned by p.

pub fn and(&self, p: &Probe<'_>) -> Probe<'ctx>

Return a probe that evaluates to “true” when self and p evaluates to true.

pub fn or(&self, p: &Probe<'_>) -> Probe<'ctx>

Return a probe that evaluates to “true” when p1 or p2 evaluates to true.

pub fn not(&self) -> Probe<'ctx>

Return a probe that evaluates to “true” when p does not evaluate to true.

pub fn ne(&self, p: &Probe<'_>) -> Probe<'ctx>

Return a probe that evaluates to “true” when the value returned by self is not equal to the value returned by p.

Trait Implementations

impl<'ctx> Clone for Probe<'ctx>

fn clone(&self) -> Self

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<'ctx> Debug for Probe<'ctx>

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

Formats the value using the given formatter.

impl<'ctx> Display for Probe<'ctx>

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

Formats the value using the given formatter.

impl<'ctx> Drop for Probe<'ctx>

fn drop(&mut self)

Executes the destructor for this type.