Struct Measure 

pub struct Measure<'a> {
    pub ctx: &'a LayoutContext,
    /* private fields */
}

A real-number measurement of a property of an object.

Fields

ctx: &'a LayoutContext

Implementations

impl<'a> Measure<'a>

pub fn zero(ctx: &'a LayoutContext) -> Self

pub fn new_const( ctx: &'a LayoutContext, value: f64, ) -> Result<Self, MeasureError>

pub fn new_unbound(ctx: &'a LayoutContext) -> Self

pub fn is_unbound(&self) -> bool

pub fn build_z3<'ctx>( self, build_ctx: &mut Z3BuildContext<'ctx>, ) -> Result<Real<'ctx>>

pub fn prop_eq(self, that: Self) -> Prop<'a>

pub fn prop_lt(self, that: Self) -> Prop<'a>

pub fn prop_le(self, that: Self) -> Prop<'a>

pub fn prop_gt(self, that: Self) -> Prop<'a>

pub fn prop_ge(self, that: Self) -> Prop<'a>

pub fn min(self, that: Self) -> Measure<'a>

pub fn max(self, that: Self) -> Measure<'a>

Trait Implementations

impl<'a> Add<f64> for Measure<'a>

type Output = Measure<'a>

The resulting type after applying the + operator.

fn add(self, other: f64) -> Self

Performs the + operation.

impl<'a> Add for Measure<'a>

type Output = Measure<'a>

The resulting type after applying the + operator.

fn add(self, other: Self) -> Self

Performs the + operation.

impl<'a> Clone for Measure<'a>

fn clone(&self) -> Measure<'a>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<'a> Debug for Measure<'a>

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

Formats the value using the given formatter.

impl<'a> Display for Measure<'a>

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

Formats the value using the given formatter.

impl<'a> Div<f64> for Measure<'a>

type Output = Measure<'a>

The resulting type after applying the / operator.

fn div(self, other: f64) -> Self

Performs the / operation.

impl<'a> Div for Measure<'a>

type Output = Measure<'a>

The resulting type after applying the / operator.

fn div(self, other: Self) -> Self

Performs the / operation.

impl<'a> Mul<f64> for Measure<'a>

type Output = Measure<'a>

The resulting type after applying the * operator.

fn mul(self, other: f64) -> Self

Performs the * operation.

impl<'a> Mul for Measure<'a>

type Output = Measure<'a>

The resulting type after applying the * operator.

fn mul(self, other: Self) -> Self

Performs the * operation.

impl<'a> Sub<f64> for Measure<'a>

type Output = Measure<'a>

The resulting type after applying the - operator.

fn sub(self, other: f64) -> Self

Performs the - operation.

impl<'a> Sub for Measure<'a>

type Output = Measure<'a>

The resulting type after applying the - operator.

fn sub(self, other: Self) -> Self

Performs the - operation.

impl<'a> Copy for Measure<'a>