Struct Lin 

pub struct Lin<Id>(/* private fields */);

Represents a type-level positive, linear expression ex: 2a + 3b + 4c + 5 The invariant is that multipliers are non-zero

Implementations

impl<T: Ord> Lin<T>

pub fn new(terms: Ctx<T, u8>, v: u8) -> Self

pub fn lit(a: u8) -> Self

Create a linear constant

pub fn var(v: T) -> Self

Create a linear variable

pub fn term(v: T, a: u8) -> Self

Create a linear variable with multiplier

pub fn leq(&self, other: &Self) -> bool

Define a partial order for linear, positive expressions true: 2a + b <= 3a + b + c {} <= a false: 4a <= 3a + b + c b <= c

Trait Implementations

impl<T: Ord + Clone> Add for &Lin<T>

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

Add two linear terms

type Output = Lin<T>

The resulting type after applying the + operator.

impl<T: Ord + Clone> Add for Lin<T>

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

Add two linear terms

type Output = Lin<T>

The resulting type after applying the + operator.

impl<T: Ord> AddAssign for Lin<T>

fn add_assign(&mut self, other: Self)

Add two linear terms

impl<Id: Clone> Clone for Lin<Id>

fn clone(&self) -> Lin<Id>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<Id: Debug> Debug for Lin<Id>

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

Formats the value using the given formatter.

impl<T: Ord> Default for Lin<T>

Identity element of addition is 0

fn default() -> Self

Returns the “default value” for a type.

impl<'a, T> Display for Lin<T>

where T: Pretty<'a, BoxAllocator, ()> + Clone + Ord,

Display instance calls the pretty printer

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

Formats the value using the given formatter.

impl<Id: Hash> Hash for Lin<Id>

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl<T: Ord + Clone> Normalizable for Lin<T>

Remove all zero elements (0*a + c = c)

fn normalize(&mut self)

fn is_normal(&self) -> bool

where Self: Clone + Eq,

Check if it is in normal form by syntactic equality

fn eqn(&self, other: &Self) -> bool

where Self: Eq + Clone,

Equality modulo normalization

impl<Id: Ord> Ord for Lin<Id>

fn cmp(&self, other: &Lin<Id>) -> Ordering

This method returns an Ordering between self and other.

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

where Self: Sized,

Compares and returns the maximum of two values.

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

where Self: Sized,

Compares and returns the minimum of two values.

fn clamp(self, min: Self, max: Self) -> Self

where Self: Sized,

Restrict a value to a certain interval.

impl<Id: PartialEq> PartialEq for Lin<Id>

fn eq(&self, other: &Lin<Id>) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl<Id: PartialOrd> PartialOrd for Lin<Id>

fn partial_cmp(&self, other: &Lin<Id>) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

fn lt(&self, other: &Rhs) -> bool

Tests less than (for self and other) and is used by the < operator.

fn le(&self, other: &Rhs) -> bool

Tests less than or equal to (for self and other) and is used by the <= operator.

fn gt(&self, other: &Rhs) -> bool

Tests greater than (for self and other) and is used by the > operator.

fn ge(&self, other: &Rhs) -> bool

Tests greater than or equal to (for self and other) and is used by the >= operator.

impl<'a, D, A, T> Pretty<'a, D, A> for Lin<T>

where D: DocAllocator<'a, A>, D::Doc: Clone, A: 'a + Clone, T: Pretty<'a, D, A> + Clone + Ord,

fn pretty(self, allocator: &'a D) -> DocBuilder<'a, D, A>

Converts self into a document

impl<T: Ord + Display + Clone> Specializable<T, u8> for Lin<T>

Specialize a linear term by substituting a variable

fn specialize(&mut self, id: &T, val: u8)

fn free_vars(&self) -> Set<&T>

fn is_closed(&self) -> bool

where T: Ord,

fn specialize_all(&mut self, ctx: Ctx<T, V>)

where T: Ord + Clone, V: Clone, Self: Sized,

impl<T: Ord + Clone> Sub for &Lin<T>

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

Subtract two linear terms (with remainder)

type Output = (Lin<T>, Lin<T>)

The resulting type after applying the - operator.

impl<T: Ord + Clone> Sub for Lin<T>

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

Subtract two linear terms (with remainder)

type Output = (Lin<T>, Lin<T>)

The resulting type after applying the - operator.

impl<Id: Eq> Eq for Lin<Id>

impl<Id> StructuralPartialEq for Lin<Id>