Enum NonMinusIntegerExpr 

pub enum NonMinusIntegerExpr<T: Atomic> {
    Atom(T),
    Const(u32),
    NegConst(u32),
    Param(Parameter),
    BinaryExpr(Box<NonMinusIntegerExpr<T>>, NonMinusIntegerOp, Box<NonMinusIntegerExpr<T>>),
}

Integer expression that does not contain a minus operator, i.e., no negations or subtractions, only negated constants are allowed.

Variants

Atom(T)

Atomic of type T

Const(u32)

Integer constant

NegConst(u32)

Negated integer constant

Param(Parameter)

Parameter

BinaryExpr(Box<NonMinusIntegerExpr<T>>, NonMinusIntegerOp, Box<NonMinusIntegerExpr<T>>)

Integer expression combining two Integer expressions through an arithmetic operator

Implementations

impl<T> NonMinusIntegerExpr<T>

where T: Atomic,

pub fn remove_div(self) -> Result<NoDivIntegerExpr<T>, ConstraintRewriteError>

Remove all division operators from the expression

This function recursively evaluates the expression and tries to simplify it by removing all division operators. If the formula is not linear arithmetic, an error is returned. This is the case if a parameter or atom appears in the denominator of a division.

Note that we do not implement full symbolic math, therefore it could be the case that the expression is linear arithmetic but requires simplification (e.g. that violating atom also appears in the denominator and could be removed by a simplification step).

pub fn try_to_fraction(&self) -> Option<Fraction>

Attempt to parse the expression into a fraction by recursively evaluating the expression

This function returns None if the expression contains any atoms or parameters. Otherwise, it returns a fraction equivalent to the original expression

Trait Implementations

impl<T: Clone + Atomic> Clone for NonMinusIntegerExpr<T>

fn clone(&self) -> NonMinusIntegerExpr<T>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<T: Debug + Atomic> Debug for NonMinusIntegerExpr<T>

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

Formats the value using the given formatter.

impl<T: Atomic> Display for NonMinusIntegerExpr<T>

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

Formats the value using the given formatter.

impl<T: Atomic> From<IntegerExpression<T>> for NonMinusIntegerExpr<T>

fn from(val: IntegerExpression<T>) -> Self

Converts to this type from the input type.

impl<T: Atomic> From<NonMinusIntegerExpr<T>> for IntegerExpression<T>

fn from(val: NonMinusIntegerExpr<T>) -> Self

Converts to this type from the input type.

impl<T: PartialEq + Atomic> PartialEq for NonMinusIntegerExpr<T>

fn eq(&self, other: &NonMinusIntegerExpr<T>) -> 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<T: Atomic> TryFrom<NonMinusIntegerExpr<T>> for NoDivIntegerExpr<T>

type Error = ConstraintRewriteError

The type returned in the event of a conversion error.

fn try_from(value: NonMinusIntegerExpr<T>) -> Result<Self, Self::Error>

Performs the conversion.

impl<T: Atomic> StructuralPartialEq for NonMinusIntegerExpr<T>