Enum IntegerExpression

Source

pub enum IntegerExpression<T: Atomic> {
    Atom(T),
    Const(u32),
    Param(Parameter),
    BinaryExpr(Box<IntegerExpression<T>>, IntegerOp, Box<IntegerExpression<T>>),
    Neg(Box<IntegerExpression<T>>),
}

Expand description

Integer expressions over objects of type T, parameters and integers

This enum represents integer expressions over objects of type T, parameters and integers.

§Example

use taco_threshold_automaton::expressions::*;

// x + 5
let _ = IntegerExpression::Atom(Variable::new("x"))
            + IntegerExpression::Const(5);

// -x
let _ = -IntegerExpression::Atom(Variable::new("x"));

Variants§

§

Atom(T)

Atomic of type T

§

Const(u32)

Integer constant

§

Param(Parameter)

Parameter

§

BinaryExpr(Box<IntegerExpression<T>>, IntegerOp, Box<IntegerExpression<T>>)

Integer expression combining two Integer expressions through an arithmetic operator

§

Neg(Box<IntegerExpression<T>>)

Negated expression

Implementations§

Source §

impl<T: Atomic> IntegerExpression<T>

Source

pub fn is_atomic(&self) -> bool

Check whether the constraint is a parameter or atomic

§Example

use taco_threshold_automaton::expressions::{IntegerExpression, Parameter, Variable};

let expr : IntegerExpression<Variable> = IntegerExpression::Param(Parameter::new("x"));
assert_eq!(expr.is_atomic(), true);

let expr : IntegerExpression<Variable> = IntegerExpression::Atom(Variable::new("x"));
assert_eq!(expr.is_atomic(), true);

let expr : IntegerExpression<Variable> = IntegerExpression::Const(1);
assert_eq!(expr.is_atomic(), false);

Source

pub fn contains_atom(&self) -> bool

Recursively check if the expression contains some atom

§Example

use taco_threshold_automaton::expressions::{IntegerExpression, Parameter, Variable};

let expr : IntegerExpression<Variable> = IntegerExpression::Atom(Variable::new("x"));
assert_eq!(expr.contains_atom(), true);

let expr : IntegerExpression<Variable> = IntegerExpression::Param(Parameter::new("x"));
assert_eq!(expr.contains_atom(), false);

let expr : IntegerExpression<Variable> = IntegerExpression::Param(Parameter::new("x"))
    + IntegerExpression::Atom(Variable::new("x"));
assert_eq!(expr.contains_atom(), true);

Source

pub fn contains_atom_a(&self, a: &T) -> bool

Recursively check if the expression references the atom a

§Example

use taco_threshold_automaton::expressions::{IntegerExpression, Parameter, Variable};

let expr : IntegerExpression<Variable> = IntegerExpression::Atom(Variable::new("x"));
assert_eq!(expr.contains_atom_a(&Variable::new("x")), true);
assert_eq!(expr.contains_atom_a(&Variable::new("y")), false);

let expr : IntegerExpression<Variable> = IntegerExpression::Param(Parameter::new("x"));
assert_eq!(expr.contains_atom_a(&Variable::new("x")), false);

let expr : IntegerExpression<Variable> = IntegerExpression::Param(Parameter::new("x"))
    + IntegerExpression::Atom(Variable::new("x"));
assert_eq!(expr.contains_atom_a(&Variable::new("x")), true);
assert_eq!(expr.contains_atom_a(&Variable::new("y")), false);

Source

pub fn try_to_evaluate_to_const(&self) -> Option<i64>

Try to evaluate the integer expression to a constant

This function succeeds if all sub-expressions are constants, otherwise it returns None.

Note: This function uses integer division (e.g. 5 / 2 = 2), be careful when using for simplification.

§Example

use crate::taco_threshold_automaton::expressions::*;

let expr = IntegerExpression::<Location>::Const(5)
    + IntegerExpression::Const(3);
assert_eq!(expr.try_to_evaluate_to_const(), Some(8));

let expr = IntegerExpression::<Location>::Param(Parameter::new("n"));
assert_eq!(expr.try_to_evaluate_to_const(), None);

let expr = IntegerExpression::<Location>::Const(5)
   / IntegerExpression::Const(2);
assert_eq!(expr.try_to_evaluate_to_const(), Some(2));

Source

pub fn try_to_evaluate_to_const_with_env( &self, env: &HashMap<T, u32>, param_env: &HashMap<Parameter, u32>, ) -> Result<i64, EvaluationError<T>>

Try to evaluate the integer expression in a given environment to a constant

This function succeeds if all sub-expressions are constants, parameters or atoms with a value specified in environment env or param_env.

If a parameter or atom is not found in the environment, an error is returned.

Note: This function uses integer division (e.g. 5 / 2 = 2), be careful when using for simplification.

§Example

use crate::taco_threshold_automaton::expressions::*;
use std::collections::HashMap;

let env = HashMap::from([(Location::new("loc"), 1)]);
let param_env = HashMap::from([(Parameter::new("n"), 1)]);

let expr = IntegerExpression::<Location>::Const(5)
   + IntegerExpression::Const(3);
assert_eq!(expr.try_to_evaluate_to_const_with_env(&env, &param_env), Ok(8));

let expr = IntegerExpression::<Location>::Const(5)
   - IntegerExpression::Atom(Location::new("loc"));
assert_eq!(expr.try_to_evaluate_to_const_with_env(&env, &param_env), Ok(4));

let expr = IntegerExpression::<Location>::Const(5)
   - IntegerExpression::Atom(Location::new("loc"))
   - IntegerExpression::Param(Parameter::new("n"));
assert_eq!(expr.try_to_evaluate_to_const_with_env(&env, &param_env), Ok(3));

Source

pub fn substitute_atom_with(&mut self, to_replace: &T, replace_with: &Self)

Substitute to_replace in this integer expression with integer expression replace_with

§Example

use crate::taco_threshold_automaton::expressions::*;

let mut expr = IntegerExpression::Const(5)
    + IntegerExpression::Atom(Location::new("l"));
expr.substitute_atom_with(&Location::new("l"), &IntegerExpression::Const(3));

let expected_expr = IntegerExpression::Const(5)
    + IntegerExpression::Const(3);
assert_eq!(expr, expected_expr);

Source

pub fn contains_parameter(&self) -> bool

Check whether the expressions contains a IntegerExpression::Param clause

This function checks whether an IntegerExpression contains a parameter.

Important: For expressions of type IntegerExpression<Parameter> one needs to additionally check whether the expression contains an atom using IntegerExpression::contains_atom.

§Example

use taco_threshold_automaton::expressions::{IntegerExpression, Parameter, Variable};

let expr : IntegerExpression<Variable> = IntegerExpression::Param(Parameter::new("x"));
assert_eq!(expr.contains_parameter(), true);

let expr : IntegerExpression<Variable> = IntegerExpression::Const(1);
assert_eq!(expr.contains_parameter(), false);

// careful when using with `IntegerExpression<Parameter>`
let expr : IntegerExpression<Parameter> = IntegerExpression::Atom(Parameter::new("x"));
assert_eq!(expr.contains_parameter(), false);

Source §

impl<T: Atomic> IntegerExpression<T>

Source

pub fn remove_unary_neg_and_sub(self) -> NonMinusIntegerExpr<T>

Remove unary negations and subtractions from the integer expression such that there are only negated constants.

§Implementation

The function recursively traverses the expression tree and pushes negations inwards until they are in front of constants, atoms, or parameters. In the latter two cases, it adds a -1 * in front of the atom or parameter.

§Example


// 1 - (n + -5)
let expr = IntegerExpression::BinaryExpr(
    Box::new(IntegerExpression::Const(1)),
    IntegerOp::Sub,
    Box::new(IntegerExpression::BinaryExpr(
        Box::new(IntegerExpression::Param(Parameter::new("n"))),
        IntegerOp::Add,
        Box::new(IntegerExpression::Neg(Box::new(IntegerExpression::Const(5)))),
    )),
);

// 1 + (-1 * n + 5)
let expected_expr : NonMinusIntegerExpr<Variable> = NonMinusIntegerExpr::BinaryExpr(
    Box::new(NonMinusIntegerExpr::Const(1)),
    NonMinusIntegerOp::Add,
    Box::new(NonMinusIntegerExpr::BinaryExpr(
        Box::new(
            NonMinusIntegerExpr::BinaryExpr(
                Box::new(NonMinusIntegerExpr::NegConst(1)),
                NonMinusIntegerOp::Mul,
                Box::new(NonMinusIntegerExpr::Param(Parameter::new("n"))),
           )
        ),
        NonMinusIntegerOp::Add,
        Box::new(NonMinusIntegerExpr::Const(5)),
    )),
);
     
let got_expr = expr.remove_unary_neg_and_sub();
assert_eq!(got_expr, expected_expr);

Source

fn negate_expression(self) -> NonMinusIntegerExpr<T>

Compute the negation of expression and removes any inner negations or subtractions

Helper function for remove_unary_neg_and_sub: This function pushes a found negation inwards until they are in front of constants, atoms, or parameters. In the latter two cases, it adds a -1 * in front of the atom or parameter.

Source

fn has_removable_negation_inside(&self, has_neg: bool) -> bool

Check whether further down the expression tree there is a negation that will be removed if we push the negation inwards.

Helper function for negate_expression. To check for a removable negation, for expression ex call with has_neg initially set to false, i.e. ex.has_removable_negation_inside(false).