taco_threshold_automaton::lia_threshold_automaton::integer_thresholds

Struct WeightedSum

pub struct WeightedSum<T>where
    T: Atomic,{
    weight_map: BTreeMap<T, Fraction>,
}

Expand description

Weighted sum of Atomic values

A weighted sum is an expression of the form c_1 * v_1 + ... + c_n * v_n where v_1, ..., v_n are atomic values and c_1, ..., c_n are real valued coefficients to these variables.

Fields§

§weight_map: BTreeMap<T, Fraction>

Map of atomic values and their weights

Implementations§

Source §

impl<T: Atomic> WeightedSum<T>

Source

pub fn is_zero(&self) -> bool

Check if the weighted sum is empty / equal to 0

Source

pub fn is_integer_form(&self) -> bool

Check whether all coefficients are already integers

This checks whether all coefficients in the weighted sum are integers, i.e., they can be converted to integer values without a loss in precision.

§Example

use taco_threshold_automaton::{
    expressions::{Variable, fraction::Fraction},
    lia_threshold_automaton::integer_thresholds::WeightedSum
};

let ws : WeightedSum<Variable> = WeightedSum::new([
    (Variable::new("var2"), 1),
]);
assert!(ws.is_integer_form());

let ws : WeightedSum<Variable> = WeightedSum::new([
    (Variable::new("var2"), Fraction::new(1, 2, false)),
]);
assert!(!ws.is_integer_form());

Source

pub fn new<F, I, V>(weight_map: I) -> Self
where F: Into<Fraction>, V: Into<T>, I: IntoIterator<Item = (V, F)>,

Create a new WeightedSum

Creates a new WeightedSum, filtering all components with a factor of 0

Source

pub fn new_empty() -> Self

Create a new empty WeightedSum

Source

pub fn get_factor(&self, v: &T) -> Option<&Fraction>

Get the factor for v if it exists

§Example

use taco_threshold_automaton::{
    expressions::{Variable, fraction::Fraction},
    lia_threshold_automaton::integer_thresholds::WeightedSum
};

let ws : WeightedSum<Variable> = WeightedSum::new([
    (Variable::new("var1"), 1),
]);
assert_eq!(ws.get_factor(&Variable::new("var1")), Some(&Fraction::from(1)));

Source

pub fn get_lcm_of_denominators(&self) -> u32

Get the least common multiple across all denominators of the coefficients

The least common multiple is computed across all denominators of the coefficients in the WeightedSum.

This can be useful for scaling such that all coefficients are integers.

§Example

use taco_threshold_automaton::{
    expressions::{Variable, fraction::Fraction},
    lia_threshold_automaton::integer_thresholds::WeightedSum
};

let ws : WeightedSum<Variable> = WeightedSum::new([
    (Variable::new("var1"), 1),
]);
assert_eq!(ws.get_lcm_of_denominators(), 1);

let ws : WeightedSum<Variable> = WeightedSum::new([
    (Variable::new("var1"), Fraction::from(1)),
    (Variable::new("var2"), Fraction::new(1, 2, false)),
]);
assert_eq!(ws.get_lcm_of_denominators(), 2);

Source

pub fn scale(&mut self, factor: Fraction)

Scale the weighted sum by a factor

§Example

use taco_threshold_automaton::{
    expressions::Variable,
    lia_threshold_automaton::integer_thresholds::WeightedSum
};

let mut ws : WeightedSum<Variable> = WeightedSum::new([
    (Variable::new("var2"), 1),
    (Variable::new("var2"), 3),
]);
let scaled_ws = WeightedSum::new([
    (Variable::new("var2"), 3),
    (Variable::new("var2"), 9),
]);

ws.scale(3.into());

assert_eq!(ws, scaled_ws);

Source

pub fn contains(&self, t: &T) -> bool

Check whether t is part of the WeightedSum (and the factor is not 0)

§Example

use taco_threshold_automaton::{
    expressions::Variable,
    lia_threshold_automaton::integer_thresholds::WeightedSum
};

let ws = WeightedSum::new([
    (Variable::new("var"), 1),
    (Variable::new("zvar"), 0),
]);

assert!(ws.contains(&Variable::new("var")));
assert!(!ws.contains(&Variable::new("unknown")));
assert!(!ws.contains(&Variable::new("zvar")));

Source

fn get_integer_expression<S>(&self) -> IntegerExpression<S>
where T: Into<IntegerExpression<S>>, S: Atomic,

Encode the weighted sum into an IntegerExpression

This method will return the WeightedSum encoded as an IntegerExpression. In case the weighted sum contains a fraction that is not in an integer form this function will encode the fraction without panicking or returning an error

Source