Struct Probe 

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

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

Iterate through the valid probe names.

Example

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

pub fn describe(name: &str) -> Result<String, Utf8Error>

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

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

Return a probe associated with the given name.

Example

let probe = Probe::new("is-qfbv");

pub fn apply(&self, goal: &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(val: f64) -> Probe

Return a probe that always evaluates to val.

let probe = Probe::constant(1.0);

pub fn lt(&self, p: &Probe) -> Probe

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

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

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

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

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

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

pub fn or(&self, p: &Probe) -> Probe

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

pub fn not(&self) -> Probe

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

pub fn ne(&self, p: &Probe) -> Probe

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 Clone for Probe

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Probe

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

Formats the value using the given formatter.

impl Display for Probe

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

Formats the value using the given formatter.

impl Drop for Probe

fn drop(&mut self)

Executes the destructor for this type.