Enum BooleanExpression

Source

pub enum BooleanExpression<T: Atomic> {
    ComparisonExpression(Box<IntegerExpression<T>>, ComparisonOp, Box<IntegerExpression<T>>),
    BinaryExpression(Box<BooleanExpression<T>>, BooleanConnective, Box<BooleanExpression<T>>),
    Not(Box<BooleanExpression<T>>),
    True,
    False,
}

Expand description

Boolean constraint over type T

This enum represents a boolean expression over integer expressions and can be used to for example guards in rules of a threshold automaton.

§Example

use taco_threshold_automaton::expressions::*;

// y > 0
let _ = BooleanExpression::ComparisonExpression(
    Box::new(IntegerExpression::Atom(Variable::new("y"))),
    ComparisonOp::Gt,
    Box::new(IntegerExpression::Const(0))
);

// x > 0 && y < 10
let _ = BooleanExpression::ComparisonExpression(
          Box::new(IntegerExpression::Atom(Variable::new("x"))),
          ComparisonOp::Gt,
          Box::new(IntegerExpression::Const(0)),
   ) & BooleanExpression::ComparisonExpression(
          Box::new(IntegerExpression::Atom(Variable::new("y"))),
          ComparisonOp::Lt,
          Box::new(IntegerExpression::Const(10)),
    );

Variants§

§

ComparisonExpression(Box<IntegerExpression<T>>, ComparisonOp, Box<IntegerExpression<T>>)

Comparison between two integer expressions

§

BinaryExpression(Box<BooleanExpression<T>>, BooleanConnective, Box<BooleanExpression<T>>)

Boolean expressions combined through boolean connective

§

Not(Box<BooleanExpression<T>>)

Negation of boolean expression

§

True

true

§

False

false

Implementations§

Source §

impl<T: Atomic> BooleanExpression<T>

Source

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

Check whether the constraint is satisfied in the given environment

This function evaluates the boolean expression in the given environment and returns whether the expression is satisfied.

§Example

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

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

let expr: BooleanExpression<Location> = BooleanExpression::ComparisonExpression(
    Box::new(IntegerExpression::Const(5)),
    ComparisonOp::Eq,
    Box::new(IntegerExpression::Const(5)),
);
assert_eq!(expr.check_satisfied(&env, &param_env), Ok(true));

let expr = BooleanExpression::ComparisonExpression(
    Box::new(IntegerExpression::Atom(Location::new("loc"))),
    ComparisonOp::Eq,
    Box::new(IntegerExpression::Const(1)),
);
assert_eq!(expr.check_satisfied(&env, &param_env), Ok(true));

let expr = BooleanExpression::ComparisonExpression(
    Box::new(IntegerExpression::Atom(Location::new("loc"))),
    ComparisonOp::Gt,
    Box::new(IntegerExpression::Const(1)),
);
assert_eq!(expr.check_satisfied(&env, &param_env), Ok(false));

let expr = BooleanExpression::ComparisonExpression(
    Box::new(IntegerExpression::Atom(Location::new("otherloc"))),
    ComparisonOp::Gt,
    Box::new(IntegerExpression::Const(1)),
);
assert_eq!(expr.check_satisfied(&env, &param_env), Err(EvaluationError::AtomicNotFound(Location::new("otherloc"))));

Source

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

Recursively check whether the expression contains the atom a

§Example

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

let expr = BooleanExpression::ComparisonExpression(
    Box::new(IntegerExpression::Atom(Location::new("loc"))),
    ComparisonOp::Eq,
    Box::new(IntegerExpression::Const(1)),
);
assert_eq!(expr.contains_atom_a(&Location::new("loc")), true);
assert_eq!(expr.contains_atom_a(&Location::new("otherloc")), false);

Source

pub fn substitute_atom_with( &mut self, to_replace: &T, replace_with: &IntegerExpression<T>, )

Substitute to_replace in this integer expression with integer expression replace_with

§Example

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

let mut expr = BooleanExpression::ComparisonExpression(
    Box::new(IntegerExpression::Const(1)),
    ComparisonOp::Eq,
    Box::new(IntegerExpression::Atom(Location::new("l"))),
);
expr.substitute_atom_with(&Location::new("l"),  &IntegerExpression::Const(3));

let expected_expr = BooleanExpression::ComparisonExpression(
    Box::new(IntegerExpression::Const(1)),
    ComparisonOp::Eq,
    Box::new(IntegerExpression::Const(3)),
);
assert_eq!(expr, expected_expr);

Source

pub fn try_check_expr_constraints_to_zero(&self, atom: &T) -> bool

Check whether this expression is a constraint forces the atom to be equal to 0

Note: This function is not complete ! It only checks for simple syntactic cases, as otherwise an SMT solver would be required.

The function covers the following cases:

atom == 0
atom < 1
atom <= 0

(and these cases appearing in a conjunction, or if they appear in both sides of a disjunction)

§Example

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

let atom = Location::new("loc");
let expr = BooleanExpression::ComparisonExpression(
   Box::new(IntegerExpression::Atom(atom.clone())),
  ComparisonOp::Eq,
  Box::new(IntegerExpression::Const(0)),
);
assert_eq!(expr.try_check_expr_constraints_to_zero(&atom), true);


let expr = BooleanExpression::ComparisonExpression(
  Box::new(IntegerExpression::Atom(atom.clone())),
  ComparisonOp::Geq,
  Box::new(IntegerExpression::Const(0)),
);
assert_eq!(expr.try_check_expr_constraints_to_zero(&atom), false);

let expr = BooleanExpression::ComparisonExpression(
   Box::new(IntegerExpression::Atom(Location::new("otherloc"))),
   ComparisonOp::Eq,
   Box::new(IntegerExpression::Const(0)),
);
assert_eq!(expr.try_check_expr_constraints_to_zero(&atom), false);

let expr = !BooleanExpression::ComparisonExpression(
  Box::new(IntegerExpression::Atom(atom.clone())),
  ComparisonOp::Gt,
  Box::new(IntegerExpression::Const(1)),
);
assert_eq!(expr.try_check_expr_constraints_to_zero(&atom), false);

Source §

impl<T: Atomic> BooleanExpression<T>

Source

pub fn remove_boolean_negations(&self) -> NonNegatedBooleanExpression<T>

Remove boolean negations from an expression, transforming the expression into a NonNegatedBooleanExpression.

This function removes a boolean negation by pushing it inwards and transforming the expression accordingly.

§Example

// !(x > 0)
let expr = BooleanExpression::Not(Box::new(BooleanExpression::ComparisonExpression(
   Box::new(IntegerExpression::Atom(Variable::new("x"))),
   ComparisonOp::Gt,
   Box::new(IntegerExpression::Const(0)),
)));

// !(x > 0) -> x <= 0
let transformed_expr = expr.remove_boolean_negations();

assert_eq!(
   transformed_expr,
   NonNegatedBooleanExpression::ComparisonExpression(
        Box::new(IntegerExpression::Atom(Variable::new("x"))),
        ComparisonOp::Leq,
        Box::new(IntegerExpression::Const(0)),
   ),
);

§Implementation

The goal of this function is to remove all boolean negations from an expression. This is done by recursively traversing the expression, if a negation i.e. Not is encountered, the negation is pushed inwards using the helper function negate_expression.

The helper function then: - replaces a BooleanExpression::True constant with a BooleanExpression::False and vice versa - calls BooleanExpression::remove_boolean_negations again if another BooleanExpression::Not is encountered (double negation) - inverts the comparison operator if a comparison expression is encountered - inverts the boolean connective if a binary expression is encountered and continues recursively on the left and right side of the binary expression

Source