Struct z3::Probe

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

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.

Implementations

impl<'ctx> Probe<'ctx>

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

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

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

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

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

Return a probe that always evaluates to val.

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.