Struct Assumptions 

pub struct Assumptions { /* private fields */ }

A set of per-variable sign assumptions used to license otherwise-unsound rewrites.

Implementations

impl Assumptions

pub fn new() -> Self

pub fn assume(self, var: &str, sign: Sign) -> Self

Assert a sign for var. Builder-style (chainable).

pub fn is_nonnegative(&self, e: &Expr) -> bool

Provable expr ≥ 0 under these assumptions (a sufficient test — None-of-proof means “unknown”, never “negative”).

pub fn is_positive(&self, e: &Expr) -> bool

Provable expr > 0 under these assumptions.

pub fn is_nonpositive(&self, e: &Expr) -> bool

Provable expr ≤ 0.

pub fn is_negative(&self, e: &Expr) -> bool

Provable expr < 0.

pub fn is_nonzero(&self, e: &Expr) -> bool

Provable expr ≠ 0.

Trait Implementations

impl Clone for Assumptions

fn clone(&self) -> Assumptions

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Assumptions

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

Formats the value using the given formatter.

impl Default for Assumptions

fn default() -> Assumptions

Returns the “default value” for a type.