Trait IntoNoDivBooleanExpr 

pub trait IntoNoDivBooleanExpr<T>
where
    T: Atomic,
{
    // Required methods
    fn get_scaled_integer_expression(
        &self,
        scaling_factor: u32,
    ) -> IntegerExpression<T>;
    fn get_lcm_of_denominators(&self) -> u32;

    // Provided method
    fn encode_comparison_to_boolean_expression<Q>(
        &self,
        comparison_op: ComparisonOp,
        other: &Q,
    ) -> BooleanExpression<T>
       where Q: IntoNoDivBooleanExpr<T> { ... }
}

Trait for objects that can be encoded into boolean expressions that do not contain any integer divisions or real numbers.

When using this trait all expressions will be scaled such that there are no longer real coefficients appearing in the expression, but the set of satisfying (integer) solutions will stay the same.

This is done by computing the least common multiple (LCM) of all denominators of rational coefficients and then scaling both sides of a ComparisonExpr to obtain an equivalent expression only containing integers.

Note that using this trait might result in a lot of LCM computations.

Required Methods

fn get_scaled_integer_expression( &self, scaling_factor: u32, ) -> IntegerExpression<T>

Encode the object into an IntegerExpression without divisions appearing

Important: The scaling factor must be a multiple of the least common multiple (LCM) of the expression. That is the relation scaling_factor % self.get_lcm_of_denominators() == 0 must hold.

This function converts the object into an integer expression without any divisions or real numbers. To eliminate rational coefficients, the expression is therefore scaled by the given factor.

fn get_lcm_of_denominators(&self) -> u32

Get the lcm across all denominators in the object

This is useful to determine the (least) scaling factor needed to scale this expressions such that it does not contain any real numbers.

Provided Methods

fn encode_comparison_to_boolean_expression<Q>( &self, comparison_op: ComparisonOp, other: &Q, ) -> BooleanExpression<T>

where Q: IntoNoDivBooleanExpr<T>,

Encode the comparison of two expressions into a boolean expression with a that does not contain any real numbers.

This functions scales the given thresholds such that in both thresholds all factors are integers. The scaling is done by computing the least common multiple (LCM) of the denominators.

Resulting comparison: self <OP> other

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors

impl<T> IntoNoDivBooleanExpr<T> for Location

where T: Atomic, IntegerExpression<T>: From<Self> + From<u32>,

impl<T> IntoNoDivBooleanExpr<T> for Parameter

where Self: Into<IntegerExpression<T>>, T: Atomic,

impl<T> IntoNoDivBooleanExpr<T> for Variable

where T: Atomic, IntegerExpression<T>: From<Self> + From<u32>,

impl<T> IntoNoDivBooleanExpr<T> for Threshold

where WeightedSum<Parameter>: IntoNoDivBooleanExpr<T>, T: Atomic,

impl<T, S> IntoNoDivBooleanExpr<S> for WeightedSum<T>

where T: Atomic + IntoNoDivBooleanExpr<S>, S: Atomic, IntegerExpression<S>: From<T>,