taco_threshold_automaton/expressions/
properties.rs

1//! This module implements functionality for expressions, such as evaluations
2//! under environments, and interfaces for expressions
3
4use core::fmt;
5use std::{collections::HashMap, error, ops};
6
7use crate::expressions::{And, IntegerExpression, Location, Or, Variable};
8
9use super::{Atomic, ComparisonOp, Parameter};
10use super::{BooleanConnective, BooleanExpression, IntegerOp};
11
12impl<T: Atomic> IntegerExpression<T> {
13    /// Check whether the constraint is a parameter or atomic
14    ///
15    /// # Example
16    ///
17    /// ```
18    /// use taco_threshold_automaton::expressions::{IntegerExpression, Parameter, Variable};
19    ///
20    /// let expr : IntegerExpression<Variable> = IntegerExpression::Param(Parameter::new("x"));
21    /// assert_eq!(expr.is_atomic(), true);
22    ///
23    /// let expr : IntegerExpression<Variable> = IntegerExpression::Atom(Variable::new("x"));
24    /// assert_eq!(expr.is_atomic(), true);
25    ///
26    /// let expr : IntegerExpression<Variable> = IntegerExpression::Const(1);
27    /// assert_eq!(expr.is_atomic(), false);
28    /// ```
29    pub fn is_atomic(&self) -> bool {
30        match self {
31            IntegerExpression::Param(_) => true,
32            IntegerExpression::Atom(_) => true,
33            IntegerExpression::Const(_) => false,
34            IntegerExpression::BinaryExpr(_, _, _) => false,
35            IntegerExpression::Neg(_) => false,
36        }
37    }
38
39    /// Recursively check if the expression contains some atom
40    ///
41    /// # Example
42    ///
43    /// ```
44    /// use taco_threshold_automaton::expressions::{IntegerExpression, Parameter, Variable};
45    ///
46    /// let expr : IntegerExpression<Variable> = IntegerExpression::Atom(Variable::new("x"));
47    /// assert_eq!(expr.contains_atom(), true);
48    ///
49    /// let expr : IntegerExpression<Variable> = IntegerExpression::Param(Parameter::new("x"));
50    /// assert_eq!(expr.contains_atom(), false);
51    ///
52    /// let expr : IntegerExpression<Variable> = IntegerExpression::Param(Parameter::new("x"))
53    ///     + IntegerExpression::Atom(Variable::new("x"));
54    /// assert_eq!(expr.contains_atom(), true);
55    /// ```
56    pub fn contains_atom(&self) -> bool {
57        match self {
58            IntegerExpression::Atom(_) => true,
59            IntegerExpression::Const(_) => false,
60            IntegerExpression::Param(_) => false,
61            IntegerExpression::Neg(ex) => ex.contains_atom(),
62            IntegerExpression::BinaryExpr(lhs, _, rhs) => {
63                lhs.contains_atom() || rhs.contains_atom()
64            }
65        }
66    }
67
68    /// Recursively check if the expression references the atom `a`
69    ///
70    /// # Example
71    ///
72    /// ```
73    /// use taco_threshold_automaton::expressions::{IntegerExpression, Parameter, Variable};
74    ///
75    /// let expr : IntegerExpression<Variable> = IntegerExpression::Atom(Variable::new("x"));
76    /// assert_eq!(expr.contains_atom_a(&Variable::new("x")), true);
77    /// assert_eq!(expr.contains_atom_a(&Variable::new("y")), false);
78    ///
79    /// let expr : IntegerExpression<Variable> = IntegerExpression::Param(Parameter::new("x"));
80    /// assert_eq!(expr.contains_atom_a(&Variable::new("x")), false);
81    ///
82    /// let expr : IntegerExpression<Variable> = IntegerExpression::Param(Parameter::new("x"))
83    ///     + IntegerExpression::Atom(Variable::new("x"));
84    /// assert_eq!(expr.contains_atom_a(&Variable::new("x")), true);
85    /// assert_eq!(expr.contains_atom_a(&Variable::new("y")), false);
86    /// ```
87    pub fn contains_atom_a(&self, a: &T) -> bool {
88        match self {
89            IntegerExpression::Atom(at) => at == a,
90            IntegerExpression::Const(_) => false,
91            IntegerExpression::Param(_) => false,
92            IntegerExpression::Neg(ex) => ex.contains_atom_a(a),
93            IntegerExpression::BinaryExpr(lhs, _, rhs) => {
94                lhs.contains_atom_a(a) || rhs.contains_atom_a(a)
95            }
96        }
97    }
98
99    /// Try to evaluate the integer expression to a constant
100    ///
101    /// This function succeeds if all sub-expressions are constants, otherwise
102    /// it returns None.
103    ///
104    /// > **Note:** This function uses integer division (e.g. 5 / 2 = 2), be
105    /// > careful when using for simplification.
106    ///
107    /// # Example
108    ///
109    /// ```
110    /// use crate::taco_threshold_automaton::expressions::*;
111    ///
112    /// let expr = IntegerExpression::<Location>::Const(5)
113    ///     + IntegerExpression::Const(3);
114    /// assert_eq!(expr.try_to_evaluate_to_const(), Some(8));
115    ///
116    /// let expr = IntegerExpression::<Location>::Param(Parameter::new("n"));
117    /// assert_eq!(expr.try_to_evaluate_to_const(), None);
118    ///
119    /// let expr = IntegerExpression::<Location>::Const(5)
120    ///    / IntegerExpression::Const(2);
121    /// assert_eq!(expr.try_to_evaluate_to_const(), Some(2));
122    /// ```
123    pub fn try_to_evaluate_to_const(&self) -> Option<i64> {
124        self.try_to_evaluate_to_const_with_env(
125            &HashMap::<T, u32>::new(),
126            &HashMap::<Parameter, u32>::new(),
127        )
128        .ok()
129    }
130
131    /// Try to evaluate the integer expression in a given environment to a
132    /// constant
133    ///
134    /// This function succeeds if all sub-expressions are constants, parameters
135    /// or atoms with a value specified in environment `env` or `param_env`.
136    ///
137    /// If a parameter or atom is not found in the environment, an error is
138    /// returned.
139    ///
140    /// > **Note:** This function uses integer division (e.g. 5 / 2 = 2), be
141    /// > careful when using for simplification.
142    ///
143    /// # Example
144    ///
145    /// ```
146    /// use crate::taco_threshold_automaton::expressions::*;
147    /// use std::collections::HashMap;
148    ///
149    /// let env = HashMap::from([(Location::new("loc"), 1)]);
150    /// let param_env = HashMap::from([(Parameter::new("n"), 1)]);
151    ///
152    /// let expr = IntegerExpression::<Location>::Const(5)
153    ///    + IntegerExpression::Const(3);
154    /// assert_eq!(expr.try_to_evaluate_to_const_with_env(&env, &param_env), Ok(8));
155    ///
156    /// let expr = IntegerExpression::<Location>::Const(5)
157    ///    - IntegerExpression::Atom(Location::new("loc"));
158    /// assert_eq!(expr.try_to_evaluate_to_const_with_env(&env, &param_env), Ok(4));
159    ///
160    /// let expr = IntegerExpression::<Location>::Const(5)
161    ///    - IntegerExpression::Atom(Location::new("loc"))
162    ///    - IntegerExpression::Param(Parameter::new("n"));
163    /// assert_eq!(expr.try_to_evaluate_to_const_with_env(&env, &param_env), Ok(3));
164    /// ```
165    pub fn try_to_evaluate_to_const_with_env(
166        &self,
167        env: &HashMap<T, u32>,
168        param_env: &HashMap<Parameter, u32>,
169    ) -> Result<i64, EvaluationError<T>> {
170        match self {
171            IntegerExpression::Const(c) => Ok(*c as i64),
172            IntegerExpression::Param(p) => {
173                if param_env.contains_key(p) {
174                    Ok(*param_env.get(p).unwrap() as i64)
175                } else {
176                    Err(EvaluationError::ParameterNotFound(p.clone()))
177                }
178            }
179            IntegerExpression::Atom(a) => {
180                if env.contains_key(a) {
181                    Ok(*env.get(a).unwrap() as i64)
182                } else {
183                    Err(EvaluationError::AtomicNotFound(a.clone()))
184                }
185            }
186            IntegerExpression::BinaryExpr(lhs, op, rhs) => {
187                let lhs = lhs.try_to_evaluate_to_const_with_env(env, param_env)?;
188                let rhs = rhs.try_to_evaluate_to_const_with_env(env, param_env)?;
189                match op {
190                    IntegerOp::Add => Ok(lhs + rhs),
191                    IntegerOp::Sub => Ok(lhs - rhs),
192                    IntegerOp::Mul => Ok(lhs * rhs),
193                    IntegerOp::Div => Ok(lhs / rhs),
194                }
195            }
196            IntegerExpression::Neg(ex) => ex
197                .try_to_evaluate_to_const_with_env(env, param_env)
198                .map(|c| -c),
199        }
200    }
201
202    /// Substitute `to_replace` in this integer expression with integer
203    /// expression `replace_with`
204    ///
205    /// # Example
206    ///
207    /// ```
208    /// use crate::taco_threshold_automaton::expressions::*;
209    ///
210    /// let mut expr = IntegerExpression::Const(5)
211    ///     + IntegerExpression::Atom(Location::new("l"));
212    /// expr.substitute_atom_with(&Location::new("l"), &IntegerExpression::Const(3));
213    ///
214    /// let expected_expr = IntegerExpression::Const(5)
215    ///     + IntegerExpression::Const(3);
216    /// assert_eq!(expr, expected_expr);
217    /// ```
218    pub fn substitute_atom_with(&mut self, to_replace: &T, replace_with: &Self) {
219        match self {
220            IntegerExpression::Atom(a) => {
221                if *a == *to_replace {
222                    *self = replace_with.clone();
223                }
224            }
225
226            IntegerExpression::BinaryExpr(lhs, _, rhs) => {
227                lhs.substitute_atom_with(to_replace, replace_with);
228                rhs.substitute_atom_with(to_replace, replace_with);
229            }
230            IntegerExpression::Neg(e) => e.substitute_atom_with(to_replace, replace_with),
231
232            IntegerExpression::Const(_) | IntegerExpression::Param(_) => (),
233        }
234    }
235
236    /// Check whether the expressions contains a [`IntegerExpression::Param`]
237    /// clause
238    ///
239    /// This function checks whether an [`IntegerExpression`] contains a
240    /// parameter.
241    ///
242    /// **Important**: For expressions of type [`IntegerExpression<Parameter>`]
243    /// one needs to additionally check whether the expression contains an atom
244    /// using [`IntegerExpression::contains_atom`].
245    ///
246    /// # Example
247    ///
248    /// ```
249    /// use taco_threshold_automaton::expressions::{IntegerExpression, Parameter, Variable};
250    ///
251    /// let expr : IntegerExpression<Variable> = IntegerExpression::Param(Parameter::new("x"));
252    /// assert_eq!(expr.contains_parameter(), true);
253    ///
254    /// let expr : IntegerExpression<Variable> = IntegerExpression::Const(1);
255    /// assert_eq!(expr.contains_parameter(), false);
256    ///
257    /// // careful when using with `IntegerExpression<Parameter>`
258    /// let expr : IntegerExpression<Parameter> = IntegerExpression::Atom(Parameter::new("x"));
259    /// assert_eq!(expr.contains_parameter(), false);
260    /// ```
261    pub fn contains_parameter(&self) -> bool {
262        match self {
263            IntegerExpression::Atom(_) | IntegerExpression::Const(_) => false,
264            IntegerExpression::Param(_) => true,
265            IntegerExpression::BinaryExpr(lhs, _op, rhs) => {
266                lhs.contains_parameter() || rhs.contains_parameter()
267            }
268            IntegerExpression::Neg(expr) => expr.contains_parameter(),
269        }
270    }
271}
272
273impl From<IntegerExpression<Parameter>> for IntegerExpression<Location> {
274    fn from(value: IntegerExpression<Parameter>) -> Self {
275        match value {
276            IntegerExpression::Param(p) | IntegerExpression::Atom(p) => IntegerExpression::Param(p),
277            IntegerExpression::Const(c) => IntegerExpression::Const(c),
278            IntegerExpression::BinaryExpr(lhs, op, rhs) => {
279                let lhs = Box::new((*lhs).into());
280                let rhs = Box::new((*rhs).into());
281
282                IntegerExpression::BinaryExpr(lhs, op, rhs)
283            }
284            IntegerExpression::Neg(integer_expression) => {
285                IntegerExpression::Neg(Box::new((*integer_expression).into()))
286            }
287        }
288    }
289}
290
291impl From<IntegerExpression<Parameter>> for IntegerExpression<Variable> {
292    fn from(value: IntegerExpression<Parameter>) -> Self {
293        match value {
294            IntegerExpression::Param(p) | IntegerExpression::Atom(p) => IntegerExpression::Param(p),
295            IntegerExpression::Const(c) => IntegerExpression::Const(c),
296            IntegerExpression::BinaryExpr(lhs, op, rhs) => {
297                let lhs = Box::new((*lhs).into());
298                let rhs = Box::new((*rhs).into());
299
300                IntegerExpression::BinaryExpr(lhs, op, rhs)
301            }
302            IntegerExpression::Neg(integer_expression) => {
303                IntegerExpression::Neg(Box::new((*integer_expression).into()))
304            }
305        }
306    }
307}
308
309/// Evaluation error of an expression
310///
311/// Error that can occur during the evaluation of an expression in an
312/// environment.
313#[derive(Debug, Clone, PartialEq)]
314pub enum EvaluationError<T: fmt::Display + PartialEq + fmt::Debug> {
315    /// Atomic was not found in the environment
316    AtomicNotFound(T),
317    /// Parameter was not found in the environment
318    ParameterNotFound(Parameter),
319}
320
321impl<T: fmt::Display + PartialEq + fmt::Debug> error::Error for EvaluationError<T> {}
322
323impl<T: fmt::Display + PartialEq + fmt::Debug> fmt::Display for EvaluationError<T> {
324    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
325        match self {
326            EvaluationError::AtomicNotFound(t) => {
327                write!(f, "Atomic {t} not found in environment")
328            }
329            EvaluationError::ParameterNotFound(p) => {
330                write!(f, "Parameter {p} not found in environment")
331            }
332        }
333    }
334}
335
336impl<T: Atomic> BooleanExpression<T> {
337    /// Check whether the constraint is satisfied in the given environment
338    ///
339    /// This function evaluates the boolean expression in the given environment
340    /// and returns whether the expression is satisfied.
341    ///
342    /// # Example
343    ///
344    /// ```
345    /// use crate::taco_threshold_automaton::expressions::*;
346    /// use std::collections::HashMap;
347    /// use taco_threshold_automaton::expressions::properties::EvaluationError;
348    ///
349    /// let env = HashMap::from([(Location::new("loc"), 1)]);
350    /// let param_env = HashMap::from([(Parameter::new("n"), 1)]);
351    ///
352    /// let expr: BooleanExpression<Location> = BooleanExpression::ComparisonExpression(
353    ///     Box::new(IntegerExpression::Const(5)),
354    ///     ComparisonOp::Eq,
355    ///     Box::new(IntegerExpression::Const(5)),
356    /// );
357    /// assert_eq!(expr.check_satisfied(&env, &param_env), Ok(true));
358    ///
359    /// let expr = BooleanExpression::ComparisonExpression(
360    ///     Box::new(IntegerExpression::Atom(Location::new("loc"))),
361    ///     ComparisonOp::Eq,
362    ///     Box::new(IntegerExpression::Const(1)),
363    /// );
364    /// assert_eq!(expr.check_satisfied(&env, &param_env), Ok(true));
365    ///
366    /// let expr = BooleanExpression::ComparisonExpression(
367    ///     Box::new(IntegerExpression::Atom(Location::new("loc"))),
368    ///     ComparisonOp::Gt,
369    ///     Box::new(IntegerExpression::Const(1)),
370    /// );
371    /// assert_eq!(expr.check_satisfied(&env, &param_env), Ok(false));
372    ///
373    /// let expr = BooleanExpression::ComparisonExpression(
374    ///     Box::new(IntegerExpression::Atom(Location::new("otherloc"))),
375    ///     ComparisonOp::Gt,
376    ///     Box::new(IntegerExpression::Const(1)),
377    /// );
378    /// assert_eq!(expr.check_satisfied(&env, &param_env), Err(EvaluationError::AtomicNotFound(Location::new("otherloc"))));
379    /// ```
380    pub fn check_satisfied(
381        &self,
382        env: &HashMap<T, u32>,
383        param_env: &HashMap<Parameter, u32>,
384    ) -> Result<bool, EvaluationError<T>> {
385        match self {
386            BooleanExpression::ComparisonExpression(rhs, op, lhs) => {
387                let rhs = rhs
388                    .as_ref()
389                    .try_to_evaluate_to_const_with_env(env, param_env)?;
390                let lhs = lhs
391                    .as_ref()
392                    .try_to_evaluate_to_const_with_env(env, param_env)?;
393                match op {
394                    ComparisonOp::Eq => Ok(rhs == lhs),
395                    ComparisonOp::Neq => Ok(rhs != lhs),
396                    ComparisonOp::Lt => Ok(rhs < lhs),
397                    ComparisonOp::Leq => Ok(rhs <= lhs),
398                    ComparisonOp::Gt => Ok(rhs > lhs),
399                    ComparisonOp::Geq => Ok(rhs >= lhs),
400                }
401            }
402            BooleanExpression::BinaryExpression(rhs, op, lhs) => {
403                let rhs = rhs.check_satisfied(env, param_env)?;
404                let lhs = lhs.check_satisfied(env, param_env)?;
405                match op {
406                    BooleanConnective::And => Ok(rhs && lhs),
407                    BooleanConnective::Or => Ok(rhs || lhs),
408                }
409            }
410            BooleanExpression::Not(expr) => Ok(!expr.check_satisfied(env, param_env)?),
411            BooleanExpression::True => Ok(true),
412            BooleanExpression::False => Ok(false),
413        }
414    }
415
416    /// Recursively check whether the expression contains the atom `a`
417    ///
418    /// # Example
419    ///
420    /// ```
421    /// use crate::taco_threshold_automaton::expressions::*;
422    ///
423    /// let expr = BooleanExpression::ComparisonExpression(
424    ///     Box::new(IntegerExpression::Atom(Location::new("loc"))),
425    ///     ComparisonOp::Eq,
426    ///     Box::new(IntegerExpression::Const(1)),
427    /// );
428    /// assert_eq!(expr.contains_atom_a(&Location::new("loc")), true);
429    /// assert_eq!(expr.contains_atom_a(&Location::new("otherloc")), false);
430    /// ```
431    pub fn contains_atom_a(&self, a: &T) -> bool {
432        match self {
433            BooleanExpression::ComparisonExpression(lhs, _, rhs) => {
434                lhs.contains_atom_a(a) || rhs.contains_atom_a(a)
435            }
436            BooleanExpression::BinaryExpression(lhs, _, rhs) => {
437                lhs.contains_atom_a(a) || rhs.contains_atom_a(a)
438            }
439            BooleanExpression::Not(expr) => expr.contains_atom_a(a),
440            BooleanExpression::True => false,
441            BooleanExpression::False => false,
442        }
443    }
444
445    /// Substitute `to_replace` in this integer expression with integer
446    /// expression `replace_with`
447    ///
448    /// # Example
449    ///
450    /// ```
451    /// use crate::taco_threshold_automaton::expressions::*;
452    ///
453    /// let mut expr = BooleanExpression::ComparisonExpression(
454    ///     Box::new(IntegerExpression::Const(1)),
455    ///     ComparisonOp::Eq,
456    ///     Box::new(IntegerExpression::Atom(Location::new("l"))),
457    /// );
458    /// expr.substitute_atom_with(&Location::new("l"),  &IntegerExpression::Const(3));
459    ///
460    /// let expected_expr = BooleanExpression::ComparisonExpression(
461    ///     Box::new(IntegerExpression::Const(1)),
462    ///     ComparisonOp::Eq,
463    ///     Box::new(IntegerExpression::Const(3)),
464    /// );
465    /// assert_eq!(expr, expected_expr);
466    /// ```
467    pub fn substitute_atom_with(&mut self, to_replace: &T, replace_with: &IntegerExpression<T>) {
468        match self {
469            BooleanExpression::ComparisonExpression(lhs, _, rhs) => {
470                lhs.substitute_atom_with(to_replace, replace_with);
471                rhs.substitute_atom_with(to_replace, replace_with);
472            }
473            BooleanExpression::BinaryExpression(lhs, _, rhs) => {
474                lhs.substitute_atom_with(to_replace, replace_with);
475                rhs.substitute_atom_with(to_replace, replace_with);
476            }
477            BooleanExpression::Not(expr) => expr.substitute_atom_with(to_replace, replace_with),
478            BooleanExpression::True | BooleanExpression::False => (),
479        }
480    }
481
482    /// Check whether this expression is a constraint forces the atom to be
483    /// equal to 0
484    ///
485    /// **Note:** This function is not complete ! It only checks for simple
486    /// syntactic cases, as otherwise an SMT solver would be required.
487    ///
488    /// The function covers the following cases:
489    ///  - `atom == 0`
490    ///  - `atom < 1`
491    ///  - `atom <= 0`
492    ///
493    /// (and these cases appearing in a conjunction, or if they appear in both
494    /// sides of a disjunction)
495    ///
496    /// # Example
497    ///
498    /// ```
499    /// use crate::taco_threshold_automaton::expressions::*;
500    ///
501    /// let atom = Location::new("loc");
502    /// let expr = BooleanExpression::ComparisonExpression(
503    ///    Box::new(IntegerExpression::Atom(atom.clone())),
504    ///   ComparisonOp::Eq,
505    ///   Box::new(IntegerExpression::Const(0)),
506    /// );
507    /// assert_eq!(expr.try_check_expr_constraints_to_zero(&atom), true);
508    ///
509    ///
510    /// let expr = BooleanExpression::ComparisonExpression(
511    ///   Box::new(IntegerExpression::Atom(atom.clone())),
512    ///   ComparisonOp::Geq,
513    ///   Box::new(IntegerExpression::Const(0)),
514    /// );
515    /// assert_eq!(expr.try_check_expr_constraints_to_zero(&atom), false);
516    ///
517    /// let expr = BooleanExpression::ComparisonExpression(
518    ///    Box::new(IntegerExpression::Atom(Location::new("otherloc"))),
519    ///    ComparisonOp::Eq,
520    ///    Box::new(IntegerExpression::Const(0)),
521    /// );
522    /// assert_eq!(expr.try_check_expr_constraints_to_zero(&atom), false);
523    ///
524    /// let expr = !BooleanExpression::ComparisonExpression(
525    ///   Box::new(IntegerExpression::Atom(atom.clone())),
526    ///   ComparisonOp::Gt,
527    ///   Box::new(IntegerExpression::Const(1)),
528    /// );
529    /// assert_eq!(expr.try_check_expr_constraints_to_zero(&atom), false);
530    /// ```
531    pub fn try_check_expr_constraints_to_zero(&self, atom: &T) -> bool {
532        match self {
533            BooleanExpression::ComparisonExpression(lhs, op, rhs) => {
534                let mut atom_expr = lhs;
535                let mut const_expr = rhs;
536                let mut op = *op;
537
538                if matches!(rhs.as_ref(), IntegerExpression::Atom(_)) {
539                    atom_expr = rhs;
540                    const_expr = lhs;
541                    op = op.get_swap_side();
542                }
543
544                if let (IntegerExpression::Atom(a), Some(c)) =
545                    (atom_expr.as_ref(), const_expr.try_to_evaluate_to_const())
546                    && a == atom
547                {
548                    return match op {
549                        ComparisonOp::Eq | ComparisonOp::Leq => c == 0,
550                        ComparisonOp::Lt => c == 1,
551                        _ => false,
552                    };
553                }
554
555                false
556            }
557            BooleanExpression::BinaryExpression(rhs, BooleanConnective::And, lhs) => {
558                lhs.try_check_expr_constraints_to_zero(atom)
559                    || rhs.try_check_expr_constraints_to_zero(atom)
560            }
561            BooleanExpression::BinaryExpression(rhs, BooleanConnective::Or, lhs) => {
562                lhs.try_check_expr_constraints_to_zero(atom)
563                    && rhs.try_check_expr_constraints_to_zero(atom)
564            }
565            BooleanExpression::Not(_) | BooleanExpression::True | BooleanExpression::False => false,
566        }
567    }
568}
569
570impl<T> From<Parameter> for IntegerExpression<T>
571where
572    T: Atomic,
573{
574    fn from(value: Parameter) -> Self {
575        IntegerExpression::Param(value)
576    }
577}
578
579impl From<Variable> for IntegerExpression<Variable> {
580    fn from(value: Variable) -> Self {
581        IntegerExpression::Atom(value)
582    }
583}
584
585impl From<Location> for IntegerExpression<Location> {
586    fn from(value: Location) -> Self {
587        IntegerExpression::Atom(value)
588    }
589}
590
591impl<S> From<u32> for IntegerExpression<S>
592where
593    S: Atomic,
594{
595    fn from(value: u32) -> Self {
596        IntegerExpression::Const(value)
597    }
598}
599
600impl From<BooleanExpression<Parameter>> for BooleanExpression<Location> {
601    fn from(value: BooleanExpression<Parameter>) -> Self {
602        match value {
603            BooleanExpression::ComparisonExpression(lhs, op, rhs) => {
604                let lhs = Box::new((*lhs).into());
605                let rhs = Box::new((*rhs).into());
606                BooleanExpression::ComparisonExpression(lhs, op, rhs)
607            }
608            BooleanExpression::BinaryExpression(lhs, conn, rhs) => {
609                let lhs = Box::new((*lhs).into());
610                let rhs = Box::new((*rhs).into());
611                BooleanExpression::BinaryExpression(lhs, conn, rhs)
612            }
613            BooleanExpression::Not(expr) => BooleanExpression::Not(Box::new((*expr).into())),
614            BooleanExpression::True => BooleanExpression::True,
615            BooleanExpression::False => BooleanExpression::False,
616        }
617    }
618}
619
620impl From<BooleanExpression<Parameter>> for BooleanExpression<Variable> {
621    fn from(value: BooleanExpression<Parameter>) -> Self {
622        match value {
623            BooleanExpression::ComparisonExpression(lhs, op, rhs) => {
624                let lhs = Box::new((*lhs).into());
625                let rhs = Box::new((*rhs).into());
626                BooleanExpression::ComparisonExpression(lhs, op, rhs)
627            }
628            BooleanExpression::BinaryExpression(lhs, conn, rhs) => {
629                let lhs = Box::new((*lhs).into());
630                let rhs = Box::new((*rhs).into());
631                BooleanExpression::BinaryExpression(lhs, conn, rhs)
632            }
633            BooleanExpression::Not(expr) => BooleanExpression::Not(Box::new((*expr).into())),
634            BooleanExpression::True => BooleanExpression::True,
635            BooleanExpression::False => BooleanExpression::False,
636        }
637    }
638}
639
640// Overload operators for easier construction of expressions
641
642impl<T> ops::Add for IntegerExpression<T>
643where
644    T: Atomic,
645{
646    type Output = IntegerExpression<T>;
647
648    fn add(self, other: IntegerExpression<T>) -> IntegerExpression<T> {
649        IntegerExpression::BinaryExpr(Box::new(self), IntegerOp::Add, Box::new(other))
650    }
651}
652
653impl<T> ops::Sub for IntegerExpression<T>
654where
655    T: Atomic,
656{
657    type Output = IntegerExpression<T>;
658
659    fn sub(self, other: IntegerExpression<T>) -> IntegerExpression<T> {
660        IntegerExpression::BinaryExpr(Box::new(self), IntegerOp::Sub, Box::new(other))
661    }
662}
663
664impl<T> ops::Mul for IntegerExpression<T>
665where
666    T: Atomic,
667{
668    type Output = IntegerExpression<T>;
669
670    fn mul(self, other: IntegerExpression<T>) -> IntegerExpression<T> {
671        IntegerExpression::BinaryExpr(Box::new(self), IntegerOp::Mul, Box::new(other))
672    }
673}
674
675impl<T> ops::Div for IntegerExpression<T>
676where
677    T: Atomic,
678{
679    type Output = IntegerExpression<T>;
680
681    fn div(self, other: IntegerExpression<T>) -> IntegerExpression<T> {
682        IntegerExpression::BinaryExpr(Box::new(self), IntegerOp::Div, Box::new(other))
683    }
684}
685
686impl<T> ops::Neg for IntegerExpression<T>
687where
688    T: Atomic,
689{
690    type Output = IntegerExpression<T>;
691
692    fn neg(self) -> IntegerExpression<T> {
693        IntegerExpression::Neg(Box::new(self))
694    }
695}
696
697impl<T> ops::Not for BooleanExpression<T>
698where
699    T: Atomic,
700{
701    type Output = BooleanExpression<T>;
702
703    fn not(self) -> BooleanExpression<T> {
704        BooleanExpression::Not(Box::new(self))
705    }
706}
707
708impl<T: Atomic> And for BooleanExpression<T> {
709    fn and(self, other: Self) -> Self {
710        BooleanExpression::BinaryExpression(
711            Box::new(self),
712            super::BooleanConnective::And,
713            Box::new(other),
714        )
715    }
716}
717impl<T> ops::BitAnd for BooleanExpression<T>
718where
719    T: Atomic,
720{
721    type Output = BooleanExpression<T>;
722
723    // Overload the `&` operator to represent the logical AND operation
724    fn bitand(self, other: BooleanExpression<T>) -> BooleanExpression<T> {
725        self.and(other)
726    }
727}
728
729impl<T: Atomic> Or for BooleanExpression<T> {
730    fn or(self, other: Self) -> Self {
731        BooleanExpression::BinaryExpression(
732            Box::new(self),
733            super::BooleanConnective::Or,
734            Box::new(other),
735        )
736    }
737}
738
739impl<T> ops::BitOr for BooleanExpression<T>
740where
741    T: Atomic,
742{
743    type Output = BooleanExpression<T>;
744
745    // Overload the `|` operator to represent the logical OR operation
746    fn bitor(self, other: BooleanExpression<T>) -> BooleanExpression<T> {
747        self.or(other)
748    }
749}
750
751impl ComparisonOp {
752    /// Invert the operation
753    ///
754    /// This function can for example be useful when negating a comparison
755    /// expression
756    ///
757    /// # Example
758    ///
759    /// ```
760    /// use taco_threshold_automaton::expressions::ComparisonOp;
761    ///
762    /// assert_eq!(ComparisonOp::Eq.invert(), ComparisonOp::Neq);
763    /// assert_eq!(ComparisonOp::Lt.invert(), ComparisonOp::Geq);
764    /// ```
765    pub fn invert(self) -> Self {
766        match self {
767            ComparisonOp::Eq => ComparisonOp::Neq,
768            ComparisonOp::Neq => ComparisonOp::Eq,
769            ComparisonOp::Lt => ComparisonOp::Geq,
770            ComparisonOp::Leq => ComparisonOp::Gt,
771            ComparisonOp::Gt => ComparisonOp::Leq,
772            ComparisonOp::Geq => ComparisonOp::Lt,
773        }
774    }
775
776    /// Swap the side of the comparison operator
777    ///
778    /// This is for example required when multiplying with negative constants
779    ///
780    /// # Example
781    ///
782    /// ```
783    /// use taco_threshold_automaton::expressions::ComparisonOp;
784    ///
785    /// assert_eq!(ComparisonOp::Eq.get_swap_side(), ComparisonOp::Eq);
786    /// assert_eq!(ComparisonOp::Lt.get_swap_side(), ComparisonOp::Gt);
787    /// ```
788    pub fn get_swap_side(self) -> Self {
789        match self {
790            ComparisonOp::Gt => ComparisonOp::Lt,
791            ComparisonOp::Geq => ComparisonOp::Leq,
792            ComparisonOp::Eq => ComparisonOp::Eq,
793            ComparisonOp::Neq => ComparisonOp::Neq,
794            ComparisonOp::Leq => ComparisonOp::Geq,
795            ComparisonOp::Lt => ComparisonOp::Gt,
796        }
797    }
798}
799
800impl BooleanConnective {
801    /// Get the dual operator of the connective
802    ///
803    /// # Example
804    ///
805    /// ```
806    /// use taco_threshold_automaton::expressions::*;
807    ///
808    /// assert_eq!(BooleanConnective::And.invert(), BooleanConnective::Or);
809    /// assert_eq!(BooleanConnective::Or.invert(), BooleanConnective::And);
810    /// ```
811    pub fn invert(self) -> Self {
812        match self {
813            BooleanConnective::And => BooleanConnective::Or,
814            BooleanConnective::Or => BooleanConnective::And,
815        }
816    }
817}
818
819#[cfg(test)]
820mod tests {
821    use std::collections::HashMap;
822
823    use crate::expressions::{
824        BooleanConnective, BooleanExpression, ComparisonOp, IntegerExpression, IntegerOp, Location,
825        Parameter, Variable, properties::EvaluationError,
826    };
827
828    #[test]
829    fn test_is_atomic() {
830        let expr: IntegerExpression<Variable> = IntegerExpression::Param(Parameter::new("x"));
831        assert!(expr.is_atomic());
832
833        let expr: IntegerExpression<Variable> = IntegerExpression::Atom(Variable::new("x"));
834        assert!(expr.is_atomic());
835
836        let expr: IntegerExpression<Variable> = IntegerExpression::Const(1);
837        assert!(!expr.is_atomic());
838
839        let expr: IntegerExpression<Variable> = IntegerExpression::BinaryExpr(
840            Box::new(IntegerExpression::Const(1)),
841            IntegerOp::Add,
842            Box::new(IntegerExpression::Const(1)),
843        );
844        assert!(!expr.is_atomic());
845
846        let expr: IntegerExpression<Variable> =
847            IntegerExpression::Neg(Box::new(IntegerExpression::Const(1)));
848        assert!(!expr.is_atomic());
849    }
850
851    #[test]
852    fn test_is_param_to_var() {
853        let expr: IntegerExpression<Parameter> = IntegerExpression::Atom(Parameter::new("x"));
854        let expected_expr: IntegerExpression<Variable> =
855            IntegerExpression::Param(Parameter::new("x"));
856        assert_eq!(
857            Into::<IntegerExpression<Variable>>::into(expr),
858            expected_expr
859        );
860
861        let expr: IntegerExpression<Parameter> = IntegerExpression::Param(Parameter::new("x"));
862        let expected_expr: IntegerExpression<Variable> =
863            IntegerExpression::Param(Parameter::new("x"));
864        assert_eq!(
865            Into::<IntegerExpression<Variable>>::into(expr),
866            expected_expr
867        );
868
869        let expr: IntegerExpression<Parameter> =
870            IntegerExpression::Neg(Box::new(IntegerExpression::Atom(Parameter::new("x"))));
871        let expected_expr: IntegerExpression<Variable> =
872            IntegerExpression::Neg(Box::new(IntegerExpression::Param(Parameter::new("x"))));
873        assert_eq!(
874            Into::<IntegerExpression<Variable>>::into(expr),
875            expected_expr
876        );
877
878        let expr: IntegerExpression<Parameter> = IntegerExpression::BinaryExpr(
879            Box::new(IntegerExpression::Atom(Parameter::new("x"))),
880            IntegerOp::Add,
881            Box::new(IntegerExpression::Const(1)),
882        );
883        let expected_expr: IntegerExpression<Variable> = IntegerExpression::BinaryExpr(
884            Box::new(IntegerExpression::Param(Parameter::new("x"))),
885            IntegerOp::Add,
886            Box::new(IntegerExpression::Const(1)),
887        );
888        assert_eq!(
889            Into::<IntegerExpression<Variable>>::into(expr),
890            expected_expr
891        );
892    }
893
894    #[test]
895    fn test_is_param_to_loc() {
896        let expr: IntegerExpression<Parameter> = IntegerExpression::Atom(Parameter::new("x"));
897        let expected_expr: IntegerExpression<Location> =
898            IntegerExpression::Param(Parameter::new("x"));
899        assert_eq!(
900            Into::<IntegerExpression<Location>>::into(expr),
901            expected_expr
902        );
903
904        let expr: IntegerExpression<Parameter> = IntegerExpression::Param(Parameter::new("x"));
905        let expected_expr: IntegerExpression<Location> =
906            IntegerExpression::Param(Parameter::new("x"));
907        assert_eq!(
908            Into::<IntegerExpression<Location>>::into(expr),
909            expected_expr
910        );
911
912        let expr: IntegerExpression<Parameter> =
913            IntegerExpression::Neg(Box::new(IntegerExpression::Atom(Parameter::new("x"))));
914        let expected_expr: IntegerExpression<Location> =
915            IntegerExpression::Neg(Box::new(IntegerExpression::Param(Parameter::new("x"))));
916        assert_eq!(
917            Into::<IntegerExpression<Location>>::into(expr),
918            expected_expr
919        );
920
921        let expr: IntegerExpression<Parameter> = IntegerExpression::BinaryExpr(
922            Box::new(IntegerExpression::Atom(Parameter::new("x"))),
923            IntegerOp::Add,
924            Box::new(IntegerExpression::Const(1)),
925        );
926        let expected_expr: IntegerExpression<Location> = IntegerExpression::BinaryExpr(
927            Box::new(IntegerExpression::Param(Parameter::new("x"))),
928            IntegerOp::Add,
929            Box::new(IntegerExpression::Const(1)),
930        );
931        assert_eq!(
932            Into::<IntegerExpression<Location>>::into(expr),
933            expected_expr
934        );
935    }
936
937    #[test]
938    fn test_integer_expression_addition() {
939        let expr1: IntegerExpression<Variable> = IntegerExpression::Const(1);
940        let expr2: IntegerExpression<Variable> = IntegerExpression::Const(2);
941        let result = expr1 + expr2;
942        assert_eq!(
943            result,
944            IntegerExpression::BinaryExpr(
945                Box::new(IntegerExpression::Const(1)),
946                IntegerOp::Add,
947                Box::new(IntegerExpression::Const(2)),
948            )
949        );
950    }
951
952    #[test]
953    fn test_integer_expression_subtraction() {
954        let expr1: IntegerExpression<Variable> = IntegerExpression::Const(3);
955        let expr2: IntegerExpression<Variable> = IntegerExpression::Const(2);
956        let result = expr1 - expr2;
957        assert_eq!(
958            result,
959            IntegerExpression::BinaryExpr(
960                Box::new(IntegerExpression::Const(3)),
961                IntegerOp::Sub,
962                Box::new(IntegerExpression::Const(2)),
963            )
964        );
965    }
966
967    #[test]
968    fn test_integer_expression_multiplication() {
969        let expr1: IntegerExpression<Variable> = IntegerExpression::Const(4);
970        let expr2: IntegerExpression<Variable> = IntegerExpression::Const(5);
971        let result = expr1 * expr2;
972        assert_eq!(
973            result,
974            IntegerExpression::BinaryExpr(
975                Box::new(IntegerExpression::Const(4)),
976                IntegerOp::Mul,
977                Box::new(IntegerExpression::Const(5)),
978            )
979        );
980    }
981
982    #[test]
983    fn test_integer_expression_division() {
984        let expr1: IntegerExpression<Variable> = IntegerExpression::Const(10);
985        let expr2: IntegerExpression<Variable> = IntegerExpression::Const(2);
986        let result = expr1 / expr2;
987        assert_eq!(
988            result,
989            IntegerExpression::BinaryExpr(
990                Box::new(IntegerExpression::Const(10)),
991                IntegerOp::Div,
992                Box::new(IntegerExpression::Const(2)),
993            )
994        );
995    }
996
997    #[test]
998    fn test_integer_expression_negation() {
999        let expr: IntegerExpression<Variable> = IntegerExpression::Const(5);
1000        let result = -expr;
1001        assert_eq!(
1002            result,
1003            IntegerExpression::Neg(Box::new(IntegerExpression::Const(5)))
1004        );
1005    }
1006
1007    #[test]
1008    fn test_boolean_expression_negation() {
1009        let expr: BooleanExpression<Variable> = BooleanExpression::True;
1010        let result = !expr;
1011        assert_eq!(
1012            result,
1013            BooleanExpression::Not(Box::new(BooleanExpression::True))
1014        );
1015    }
1016
1017    #[test]
1018    fn test_boolean_expression_and() {
1019        let expr1: BooleanExpression<Variable> = BooleanExpression::True;
1020        let expr2: BooleanExpression<Variable> = BooleanExpression::True;
1021        let result = expr1 & expr2;
1022        assert_eq!(
1023            result,
1024            BooleanExpression::BinaryExpression(
1025                Box::new(BooleanExpression::True),
1026                BooleanConnective::And,
1027                Box::new(BooleanExpression::True),
1028            )
1029        );
1030    }
1031
1032    #[test]
1033    fn test_boolean_expression_or() {
1034        let expr1: BooleanExpression<Variable> = BooleanExpression::True;
1035        let expr2: BooleanExpression<Variable> = BooleanExpression::True;
1036        let result = expr1 | expr2;
1037        assert_eq!(
1038            result,
1039            BooleanExpression::BinaryExpression(
1040                Box::new(BooleanExpression::True),
1041                BooleanConnective::Or,
1042                Box::new(BooleanExpression::True),
1043            )
1044        );
1045    }
1046
1047    #[test]
1048    fn test_boolean_expr_param_to_loc() {
1049        let expr: BooleanExpression<Parameter> = BooleanExpression::True;
1050        let expected_expr: BooleanExpression<Location> = BooleanExpression::True;
1051        assert_eq!(
1052            Into::<BooleanExpression<Location>>::into(expr),
1053            expected_expr
1054        );
1055
1056        let expr: BooleanExpression<Parameter> = BooleanExpression::False;
1057        let expected_expr: BooleanExpression<Location> = BooleanExpression::False;
1058        assert_eq!(
1059            Into::<BooleanExpression<Location>>::into(expr),
1060            expected_expr
1061        );
1062
1063        let expr: BooleanExpression<Parameter> =
1064            BooleanExpression::Not(Box::new(BooleanExpression::True));
1065        let expected_expr: BooleanExpression<Location> =
1066            BooleanExpression::Not(Box::new(BooleanExpression::True));
1067        assert_eq!(
1068            Into::<BooleanExpression<Location>>::into(expr),
1069            expected_expr
1070        );
1071
1072        let expr: BooleanExpression<Parameter> = BooleanExpression::BinaryExpression(
1073            Box::new(BooleanExpression::True),
1074            BooleanConnective::And,
1075            Box::new(BooleanExpression::False),
1076        );
1077        let expected_expr: BooleanExpression<Location> = BooleanExpression::BinaryExpression(
1078            Box::new(BooleanExpression::True),
1079            BooleanConnective::And,
1080            Box::new(BooleanExpression::False),
1081        );
1082        assert_eq!(
1083            Into::<BooleanExpression<Location>>::into(expr),
1084            expected_expr
1085        );
1086
1087        let expr: BooleanExpression<Parameter> = BooleanExpression::ComparisonExpression(
1088            Box::new(IntegerExpression::Const(42)),
1089            ComparisonOp::Leq,
1090            Box::new(IntegerExpression::Atom(Parameter::new("n"))),
1091        );
1092        let expected_expr: BooleanExpression<Location> = BooleanExpression::ComparisonExpression(
1093            Box::new(IntegerExpression::Const(42)),
1094            ComparisonOp::Leq,
1095            Box::new(IntegerExpression::Param(Parameter::new("n"))),
1096        );
1097        assert_eq!(
1098            Into::<BooleanExpression<Location>>::into(expr),
1099            expected_expr
1100        );
1101    }
1102
1103    #[test]
1104    fn test_boolean_expr_param_to_var() {
1105        let expr: BooleanExpression<Parameter> = BooleanExpression::True;
1106        let expected_expr: BooleanExpression<Variable> = BooleanExpression::True;
1107        assert_eq!(
1108            Into::<BooleanExpression<Variable>>::into(expr),
1109            expected_expr
1110        );
1111
1112        let expr: BooleanExpression<Parameter> = BooleanExpression::False;
1113        let expected_expr: BooleanExpression<Variable> = BooleanExpression::False;
1114        assert_eq!(
1115            Into::<BooleanExpression<Variable>>::into(expr),
1116            expected_expr
1117        );
1118
1119        let expr: BooleanExpression<Parameter> =
1120            BooleanExpression::Not(Box::new(BooleanExpression::True));
1121        let expected_expr: BooleanExpression<Variable> =
1122            BooleanExpression::Not(Box::new(BooleanExpression::True));
1123        assert_eq!(
1124            Into::<BooleanExpression<Variable>>::into(expr),
1125            expected_expr
1126        );
1127
1128        let expr: BooleanExpression<Parameter> = BooleanExpression::BinaryExpression(
1129            Box::new(BooleanExpression::True),
1130            BooleanConnective::And,
1131            Box::new(BooleanExpression::False),
1132        );
1133        let expected_expr: BooleanExpression<Variable> = BooleanExpression::BinaryExpression(
1134            Box::new(BooleanExpression::True),
1135            BooleanConnective::And,
1136            Box::new(BooleanExpression::False),
1137        );
1138        assert_eq!(
1139            Into::<BooleanExpression<Variable>>::into(expr),
1140            expected_expr
1141        );
1142
1143        let expr: BooleanExpression<Parameter> = BooleanExpression::ComparisonExpression(
1144            Box::new(IntegerExpression::Const(42)),
1145            ComparisonOp::Leq,
1146            Box::new(IntegerExpression::Atom(Parameter::new("n"))),
1147        );
1148        let expected_expr: BooleanExpression<Variable> = BooleanExpression::ComparisonExpression(
1149            Box::new(IntegerExpression::Const(42)),
1150            ComparisonOp::Leq,
1151            Box::new(IntegerExpression::Param(Parameter::new("n"))),
1152        );
1153        assert_eq!(
1154            Into::<BooleanExpression<Variable>>::into(expr),
1155            expected_expr
1156        );
1157    }
1158
1159    #[test]
1160    fn test_integer_expression_contains_atom() {
1161        let expr1: IntegerExpression<Variable> = IntegerExpression::Atom(Variable::new("x"));
1162        assert!(expr1.contains_atom());
1163
1164        let expr2: IntegerExpression<Variable> = IntegerExpression::Const(1);
1165        assert!(!expr2.contains_atom());
1166
1167        let expr3: IntegerExpression<Variable> = IntegerExpression::Param(Parameter::new("y"));
1168        assert!(!expr3.contains_atom());
1169
1170        let expr4: IntegerExpression<Variable> =
1171            IntegerExpression::Neg(Box::new(IntegerExpression::Atom(Variable::new("z"))));
1172        assert!(expr4.contains_atom());
1173
1174        let expr5: IntegerExpression<Variable> = IntegerExpression::BinaryExpr(
1175            Box::new(IntegerExpression::Atom(Variable::new("a"))),
1176            IntegerOp::Add,
1177            Box::new(IntegerExpression::Const(1)),
1178        );
1179        assert!(expr5.contains_atom());
1180    }
1181
1182    #[test]
1183    fn test_swap_side_comp_op() {
1184        assert_eq!(ComparisonOp::Eq.get_swap_side(), ComparisonOp::Eq);
1185        assert_eq!(ComparisonOp::Neq.get_swap_side(), ComparisonOp::Neq);
1186        assert_eq!(ComparisonOp::Lt.get_swap_side(), ComparisonOp::Gt);
1187        assert_eq!(ComparisonOp::Leq.get_swap_side(), ComparisonOp::Geq);
1188        assert_eq!(ComparisonOp::Gt.get_swap_side(), ComparisonOp::Lt);
1189        assert_eq!(ComparisonOp::Geq.get_swap_side(), ComparisonOp::Leq);
1190    }
1191
1192    #[test]
1193    fn test_invert_comp_op() {
1194        assert_eq!(ComparisonOp::Eq.invert(), ComparisonOp::Neq);
1195        assert_eq!(ComparisonOp::Neq.invert(), ComparisonOp::Eq);
1196        assert_eq!(ComparisonOp::Lt.invert(), ComparisonOp::Geq);
1197        assert_eq!(ComparisonOp::Leq.invert(), ComparisonOp::Gt);
1198        assert_eq!(ComparisonOp::Gt.invert(), ComparisonOp::Leq);
1199        assert_eq!(ComparisonOp::Geq.invert(), ComparisonOp::Lt);
1200    }
1201
1202    #[test]
1203    fn test_invert_boolean_connective() {
1204        assert_eq!(BooleanConnective::And.invert(), BooleanConnective::Or);
1205        assert_eq!(BooleanConnective::Or.invert(), BooleanConnective::And);
1206    }
1207
1208    #[test]
1209    fn test_try_to_evaluate_to_const() {
1210        let expr = IntegerExpression::<Location>::Const(5) + IntegerExpression::Const(3);
1211        assert_eq!(expr.try_to_evaluate_to_const(), Some(8));
1212
1213        let expr = IntegerExpression::<Location>::Const(5) - IntegerExpression::Const(3);
1214        assert_eq!(expr.try_to_evaluate_to_const(), Some(2));
1215
1216        let expr = IntegerExpression::<Location>::Const(10) / IntegerExpression::Const(5);
1217        assert_eq!(expr.try_to_evaluate_to_const(), Some(2));
1218
1219        let expr = -IntegerExpression::Const(42) / IntegerExpression::<Location>::Const(2);
1220        assert_eq!(expr.try_to_evaluate_to_const(), Some(-21));
1221
1222        let expr = -IntegerExpression::<Location>::Const(42) * IntegerExpression::Const(2);
1223        assert_eq!(expr.try_to_evaluate_to_const(), Some(-84));
1224
1225        let expr = IntegerExpression::<Location>::Param(Parameter::new("n"));
1226        assert_eq!(expr.try_to_evaluate_to_const(), None);
1227
1228        let expr = -IntegerExpression::Const(42) / IntegerExpression::Atom(Location::new("loc"));
1229        assert_eq!(expr.try_to_evaluate_to_const(), None);
1230    }
1231
1232    #[test]
1233    fn test_try_to_evaluate_to_const_with_env() {
1234        let env = HashMap::from([(Location::new("loc"), 1)]);
1235        let param_env = HashMap::from([(Parameter::new("n"), 1)]);
1236
1237        let expr = IntegerExpression::<Location>::Const(5) + IntegerExpression::Const(3);
1238        assert_eq!(
1239            expr.try_to_evaluate_to_const_with_env(&env, &param_env),
1240            Ok(8)
1241        );
1242
1243        let expr = IntegerExpression::<Location>::Const(5) - IntegerExpression::Const(3);
1244        assert_eq!(
1245            expr.try_to_evaluate_to_const_with_env(&env, &param_env),
1246            Ok(2)
1247        );
1248
1249        let expr = IntegerExpression::<Location>::Const(10) / IntegerExpression::Const(5);
1250        assert_eq!(
1251            expr.try_to_evaluate_to_const_with_env(&env, &param_env),
1252            Ok(2)
1253        );
1254
1255        let expr = -IntegerExpression::Const(42) / IntegerExpression::<Location>::Const(2);
1256        assert_eq!(
1257            expr.try_to_evaluate_to_const_with_env(&env, &param_env),
1258            Ok(-21)
1259        );
1260
1261        let expr = -IntegerExpression::<Location>::Const(42) * IntegerExpression::Const(2);
1262        assert_eq!(
1263            expr.try_to_evaluate_to_const_with_env(&env, &param_env),
1264            Ok(-84)
1265        );
1266
1267        let expr = IntegerExpression::Atom(Location::new("loc"));
1268        assert_eq!(
1269            expr.try_to_evaluate_to_const_with_env(&env, &param_env),
1270            Ok(1)
1271        );
1272
1273        let expr = -IntegerExpression::Const(42) / IntegerExpression::Atom(Location::new("loc"));
1274        assert_eq!(
1275            expr.try_to_evaluate_to_const_with_env(&env, &param_env),
1276            Ok(-42)
1277        );
1278
1279        let expr = IntegerExpression::<Location>::Param(Parameter::new("n"));
1280        assert_eq!(
1281            expr.try_to_evaluate_to_const_with_env(&HashMap::new(), &param_env),
1282            Ok(1)
1283        );
1284
1285        let expr = IntegerExpression::<Location>::Param(Parameter::new("n"));
1286        assert_eq!(
1287            expr.try_to_evaluate_to_const_with_env(&env, &HashMap::new()),
1288            Err(EvaluationError::ParameterNotFound(Parameter::new("n")))
1289        );
1290
1291        let expr = IntegerExpression::Atom(Location::new("loc"));
1292        assert_eq!(
1293            expr.try_to_evaluate_to_const_with_env(&HashMap::new(), &param_env),
1294            Err(EvaluationError::AtomicNotFound(Location::new("loc")))
1295        );
1296    }
1297
1298    #[test]
1299    fn test_boolean_expr_check_satisfied() {
1300        let env = HashMap::from([(Location::new("loc"), 1)]);
1301        let param_env = HashMap::from([(Parameter::new("n"), 1)]);
1302
1303        let expr = BooleanExpression::ComparisonExpression(
1304            Box::new(IntegerExpression::Const(5)),
1305            ComparisonOp::Eq,
1306            Box::new(IntegerExpression::Const(5)),
1307        );
1308        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(true));
1309
1310        let expr = BooleanExpression::ComparisonExpression(
1311            Box::new(IntegerExpression::Const(5)),
1312            ComparisonOp::Eq,
1313            Box::new(IntegerExpression::Const(3)),
1314        );
1315        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(false));
1316
1317        let expr = BooleanExpression::ComparisonExpression(
1318            Box::new(IntegerExpression::Const(5)),
1319            ComparisonOp::Lt,
1320            Box::new(IntegerExpression::Const(3)),
1321        );
1322        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(false));
1323
1324        let expr = BooleanExpression::ComparisonExpression(
1325            Box::new(IntegerExpression::Const(5)),
1326            ComparisonOp::Lt,
1327            Box::new(IntegerExpression::Const(10)),
1328        );
1329        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(true));
1330
1331        let expr = BooleanExpression::ComparisonExpression(
1332            Box::new(IntegerExpression::Const(5)),
1333            ComparisonOp::Leq,
1334            Box::new(IntegerExpression::Const(5)),
1335        );
1336        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(true));
1337
1338        let expr = BooleanExpression::ComparisonExpression(
1339            Box::new(IntegerExpression::Const(5)),
1340            ComparisonOp::Leq,
1341            Box::new(IntegerExpression::Const(3)),
1342        );
1343        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(false));
1344
1345        let expr = BooleanExpression::ComparisonExpression(
1346            Box::new(IntegerExpression::Const(5)),
1347            ComparisonOp::Gt,
1348            Box::new(IntegerExpression::Const(3)),
1349        );
1350        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(true));
1351
1352        let expr = BooleanExpression::ComparisonExpression(
1353            Box::new(IntegerExpression::Const(5)),
1354            ComparisonOp::Gt,
1355            Box::new(IntegerExpression::Const(10)),
1356        );
1357        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(false));
1358
1359        let expr = BooleanExpression::ComparisonExpression(
1360            Box::new(IntegerExpression::Const(5)),
1361            ComparisonOp::Neq,
1362            Box::new(IntegerExpression::Const(5)),
1363        );
1364        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(false));
1365
1366        let expr = BooleanExpression::ComparisonExpression(
1367            Box::new(IntegerExpression::Const(5)),
1368            ComparisonOp::Neq,
1369            Box::new(IntegerExpression::Const(3)),
1370        );
1371        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(true));
1372
1373        let expr = BooleanExpression::ComparisonExpression(
1374            Box::new(IntegerExpression::Const(5)),
1375            ComparisonOp::Geq,
1376            Box::new(IntegerExpression::Const(3)),
1377        );
1378        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(true));
1379
1380        let expr = BooleanExpression::ComparisonExpression(
1381            Box::new(IntegerExpression::Const(5)),
1382            ComparisonOp::Geq,
1383            Box::new(IntegerExpression::Const(10)),
1384        );
1385        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(false));
1386
1387        let expr = BooleanExpression::BinaryExpression(
1388            Box::new(BooleanExpression::True),
1389            BooleanConnective::And,
1390            Box::new(BooleanExpression::True),
1391        );
1392        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(true));
1393
1394        let expr = BooleanExpression::BinaryExpression(
1395            Box::new(BooleanExpression::True),
1396            BooleanConnective::Or,
1397            Box::new(BooleanExpression::False),
1398        );
1399        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(true));
1400
1401        let expr = !BooleanExpression::False;
1402        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(true));
1403
1404        let expr = BooleanExpression::False;
1405        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(false));
1406    }
1407
1408    #[test]
1409    fn test_display_evaluation_error() {
1410        let error = EvaluationError::AtomicNotFound(Location::new("loc"));
1411        assert!(
1412            error
1413                .to_string()
1414                .contains(&Location::new("loc").to_string())
1415        );
1416
1417        let error: EvaluationError<Location> =
1418            EvaluationError::ParameterNotFound(Parameter::new("n"));
1419        assert!(error.to_string().contains("n"));
1420    }
1421
1422    #[test]
1423    fn test_contains_atom_a_integer_expr() {
1424        let atom = Variable::new("x");
1425
1426        let expr1: IntegerExpression<Variable> = IntegerExpression::Atom(atom.clone());
1427        assert!(expr1.contains_atom_a(&atom));
1428
1429        let expr2: IntegerExpression<Variable> = IntegerExpression::Const(1);
1430        assert!(!expr2.contains_atom_a(&atom));
1431
1432        let expr3: IntegerExpression<Variable> = IntegerExpression::Param(Parameter::new("y"));
1433        assert!(!expr3.contains_atom_a(&atom));
1434
1435        let expr4: IntegerExpression<Variable> =
1436            IntegerExpression::Neg(Box::new(IntegerExpression::Atom(atom.clone())));
1437        assert!(expr4.contains_atom_a(&atom));
1438
1439        let expr5: IntegerExpression<Variable> = IntegerExpression::BinaryExpr(
1440            Box::new(IntegerExpression::Atom(atom.clone())),
1441            IntegerOp::Add,
1442            Box::new(IntegerExpression::Const(1)),
1443        );
1444        assert!(expr5.contains_atom_a(&atom));
1445
1446        let expr6: IntegerExpression<Variable> = IntegerExpression::BinaryExpr(
1447            Box::new(IntegerExpression::Const(1)),
1448            IntegerOp::Add,
1449            Box::new(IntegerExpression::Const(2)),
1450        );
1451        assert!(!expr6.contains_atom_a(&atom));
1452    }
1453
1454    #[test]
1455    fn test_contains_atom_a_boolean_expr() {
1456        let atom = Variable::new("x");
1457
1458        let expr1: BooleanExpression<Variable> = BooleanExpression::ComparisonExpression(
1459            Box::new(IntegerExpression::Atom(atom.clone())),
1460            ComparisonOp::Eq,
1461            Box::new(IntegerExpression::Const(1)),
1462        );
1463        assert!(expr1.contains_atom_a(&atom));
1464
1465        let expr2: BooleanExpression<Variable> = BooleanExpression::ComparisonExpression(
1466            Box::new(IntegerExpression::Atom(Variable::new("y"))),
1467            ComparisonOp::Eq,
1468            Box::new(IntegerExpression::Const(2)),
1469        );
1470        assert!(!expr2.contains_atom_a(&atom));
1471
1472        let expr3: BooleanExpression<Variable> = BooleanExpression::BinaryExpression(
1473            Box::new(BooleanExpression::ComparisonExpression(
1474                Box::new(IntegerExpression::Atom(atom.clone())),
1475                ComparisonOp::Eq,
1476                Box::new(IntegerExpression::Const(1)),
1477            )),
1478            BooleanConnective::And,
1479            Box::new(BooleanExpression::True),
1480        );
1481        assert!(expr3.contains_atom_a(&atom));
1482
1483        let expr4: BooleanExpression<Variable> =
1484            BooleanExpression::Not(Box::new(BooleanExpression::ComparisonExpression(
1485                Box::new(IntegerExpression::Atom(atom.clone())),
1486                ComparisonOp::Eq,
1487                Box::new(IntegerExpression::Const(1)),
1488            )));
1489        assert!(expr4.contains_atom_a(&atom));
1490
1491        let expr5: BooleanExpression<Variable> = BooleanExpression::True;
1492        assert!(!expr5.contains_atom_a(&atom));
1493
1494        let expr6: BooleanExpression<Variable> = BooleanExpression::False;
1495        assert!(!expr6.contains_atom_a(&atom));
1496    }
1497
1498    #[test]
1499    fn test_boolean_expression_complex() {
1500        let env = HashMap::from([(Location::new("loc"), 1)]);
1501        let param_env = HashMap::from([(Parameter::new("n"), 1)]);
1502
1503        let expr = BooleanExpression::BinaryExpression(
1504            Box::new(BooleanExpression::ComparisonExpression(
1505                Box::new(IntegerExpression::Const(5)),
1506                ComparisonOp::Eq,
1507                Box::new(IntegerExpression::Const(5)),
1508            )),
1509            BooleanConnective::And,
1510            Box::new(BooleanExpression::ComparisonExpression(
1511                Box::new(IntegerExpression::Const(3)),
1512                ComparisonOp::Lt,
1513                Box::new(IntegerExpression::Const(10)),
1514            )),
1515        );
1516        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(true));
1517
1518        let expr = BooleanExpression::BinaryExpression(
1519            Box::new(BooleanExpression::ComparisonExpression(
1520                Box::new(IntegerExpression::Const(5)),
1521                ComparisonOp::Eq,
1522                Box::new(IntegerExpression::Const(3)),
1523            )),
1524            BooleanConnective::Or,
1525            Box::new(BooleanExpression::ComparisonExpression(
1526                Box::new(IntegerExpression::Const(3)),
1527                ComparisonOp::Lt,
1528                Box::new(IntegerExpression::Const(10)),
1529            )),
1530        );
1531        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(true));
1532
1533        let expr = BooleanExpression::Not(Box::new(BooleanExpression::ComparisonExpression(
1534            Box::new(IntegerExpression::Const(5)),
1535            ComparisonOp::Eq,
1536            Box::new(IntegerExpression::Const(3)),
1537        )));
1538        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(true));
1539    }
1540
1541    #[test]
1542    fn test_integer_expression_substitute_atom() {
1543        let atom = Variable::new("x");
1544        let replacement = IntegerExpression::Const(42);
1545
1546        let expr1: IntegerExpression<Variable> = IntegerExpression::Atom(atom.clone());
1547        let mut result = expr1.clone();
1548        result.substitute_atom_with(&atom, &replacement);
1549        assert_eq!(result, replacement);
1550
1551        let expr2: IntegerExpression<Variable> = IntegerExpression::Const(1);
1552        let mut result = expr2.clone();
1553        result.substitute_atom_with(&atom, &replacement);
1554        assert_eq!(result, expr2);
1555
1556        let expr3: IntegerExpression<Variable> = IntegerExpression::Param(Parameter::new("y"));
1557        let mut result = expr3.clone();
1558        result.substitute_atom_with(&atom, &replacement);
1559        assert_eq!(result, expr3);
1560
1561        let expr4: IntegerExpression<Variable> =
1562            IntegerExpression::Neg(Box::new(IntegerExpression::Atom(atom.clone())));
1563        let expected = IntegerExpression::Neg(Box::new(replacement.clone()));
1564        let mut result = expr4;
1565        result.substitute_atom_with(&atom, &replacement);
1566        assert_eq!(result, expected);
1567
1568        let expr5: IntegerExpression<Variable> = IntegerExpression::BinaryExpr(
1569            Box::new(IntegerExpression::Atom(atom.clone())),
1570            IntegerOp::Add,
1571            Box::new(IntegerExpression::Const(1)),
1572        );
1573        let expected = IntegerExpression::BinaryExpr(
1574            Box::new(replacement.clone()),
1575            IntegerOp::Add,
1576            Box::new(IntegerExpression::Const(1)),
1577        );
1578        let mut result = expr5.clone();
1579        result.substitute_atom_with(&atom, &replacement);
1580        assert_eq!(result, expected);
1581
1582        let expr6: IntegerExpression<Variable> = IntegerExpression::BinaryExpr(
1583            Box::new(IntegerExpression::Const(1)),
1584            IntegerOp::Add,
1585            Box::new(IntegerExpression::Const(2)),
1586        );
1587        let mut result = expr6.clone();
1588        result.substitute_atom_with(&atom, &replacement);
1589        assert_eq!(result, expr6);
1590    }
1591
1592    #[test]
1593    fn test_boolean_expr_substitute_atom() {
1594        let atom = Variable::new("x");
1595        let replacement = IntegerExpression::Const(42);
1596
1597        let expr1: BooleanExpression<Variable> = BooleanExpression::ComparisonExpression(
1598            Box::new(IntegerExpression::Atom(atom.clone())),
1599            ComparisonOp::Eq,
1600            Box::new(IntegerExpression::Const(1)),
1601        );
1602        let expected = BooleanExpression::ComparisonExpression(
1603            Box::new(replacement.clone()),
1604            ComparisonOp::Eq,
1605            Box::new(IntegerExpression::Const(1)),
1606        );
1607        let mut result = expr1.clone();
1608        result.substitute_atom_with(&atom, &replacement);
1609        assert_eq!(result, expected);
1610
1611        let expr2: BooleanExpression<Variable> = BooleanExpression::BinaryExpression(
1612            Box::new(BooleanExpression::ComparisonExpression(
1613                Box::new(IntegerExpression::Atom(atom.clone())),
1614                ComparisonOp::Eq,
1615                Box::new(IntegerExpression::Const(1)),
1616            )),
1617            BooleanConnective::And,
1618            Box::new(BooleanExpression::True),
1619        );
1620        let expected = BooleanExpression::BinaryExpression(
1621            Box::new(BooleanExpression::ComparisonExpression(
1622                Box::new(replacement.clone()),
1623                ComparisonOp::Eq,
1624                Box::new(IntegerExpression::Const(1)),
1625            )),
1626            BooleanConnective::And,
1627            Box::new(BooleanExpression::True),
1628        );
1629        let mut result = expr2.clone();
1630        result.substitute_atom_with(&atom, &replacement);
1631        assert_eq!(result, expected);
1632
1633        let expr3: BooleanExpression<Variable> =
1634            BooleanExpression::Not(Box::new(BooleanExpression::ComparisonExpression(
1635                Box::new(IntegerExpression::Atom(atom.clone())),
1636                ComparisonOp::Eq,
1637                Box::new(IntegerExpression::Const(1)),
1638            )));
1639        let expected = BooleanExpression::Not(Box::new(BooleanExpression::ComparisonExpression(
1640            Box::new(replacement.clone()),
1641            ComparisonOp::Eq,
1642            Box::new(IntegerExpression::Const(1)),
1643        )));
1644        let mut result = expr3.clone();
1645        result.substitute_atom_with(&atom, &replacement);
1646        assert_eq!(result, expected);
1647
1648        let expr4: BooleanExpression<Variable> = BooleanExpression::True;
1649        let mut result = expr4.clone();
1650        result.substitute_atom_with(&atom, &replacement);
1651        assert_eq!(result, expr4);
1652
1653        let expr5: BooleanExpression<Variable> = BooleanExpression::False;
1654        let mut result = expr5.clone();
1655        result.substitute_atom_with(&atom, &replacement);
1656        assert_eq!(result, expr5);
1657    }
1658
1659    #[test]
1660    fn test_try_check_expr_constraints_to_zero() {
1661        let atom = Location::new("loc");
1662        let expr = BooleanExpression::ComparisonExpression(
1663            Box::new(IntegerExpression::Atom(atom.clone())),
1664            ComparisonOp::Eq,
1665            Box::new(IntegerExpression::Const(0)),
1666        );
1667        assert!(expr.try_check_expr_constraints_to_zero(&atom));
1668
1669        let expr = BooleanExpression::ComparisonExpression(
1670            Box::new(IntegerExpression::Atom(atom.clone())),
1671            ComparisonOp::Leq,
1672            Box::new(IntegerExpression::Const(0)),
1673        );
1674        assert!(expr.try_check_expr_constraints_to_zero(&atom));
1675
1676        let expr = BooleanExpression::ComparisonExpression(
1677            Box::new(IntegerExpression::Atom(atom.clone())),
1678            ComparisonOp::Lt,
1679            Box::new(IntegerExpression::Const(1)),
1680        );
1681        assert!(expr.try_check_expr_constraints_to_zero(&atom));
1682
1683        let expr = BooleanExpression::ComparisonExpression(
1684            Box::new(IntegerExpression::Atom(atom.clone())),
1685            ComparisonOp::Geq,
1686            Box::new(IntegerExpression::Const(0)),
1687        );
1688        assert!(!expr.try_check_expr_constraints_to_zero(&atom));
1689
1690        let expr = BooleanExpression::ComparisonExpression(
1691            Box::new(IntegerExpression::Atom(Location::new("otherloc"))),
1692            ComparisonOp::Eq,
1693            Box::new(IntegerExpression::Const(0)),
1694        );
1695        assert!(!expr.try_check_expr_constraints_to_zero(&atom));
1696
1697        let expr = !BooleanExpression::ComparisonExpression(
1698            Box::new(IntegerExpression::Atom(atom.clone())),
1699            ComparisonOp::Gt,
1700            Box::new(IntegerExpression::Const(1)),
1701        );
1702        assert!(!expr.try_check_expr_constraints_to_zero(&atom));
1703
1704        let atom = Location::new("loc");
1705        let expr = BooleanExpression::ComparisonExpression(
1706            Box::new(IntegerExpression::Const(0)),
1707            ComparisonOp::Eq,
1708            Box::new(IntegerExpression::Atom(atom.clone())),
1709        );
1710        assert!(expr.try_check_expr_constraints_to_zero(&atom));
1711    }
1712
1713    #[test]
1714    fn test_try_const_from_integer() {
1715        let expr: IntegerExpression<Location> = 1_u32.into();
1716        assert_eq!(expr, IntegerExpression::Const(1));
1717    }
1718
1719    #[test]
1720    fn test_integer_expr_from_location() {
1721        let loc = Location::new("loc");
1722        let expected_expr = IntegerExpression::Atom(Location::new("loc"));
1723        assert_eq!(IntegerExpression::from(loc), expected_expr);
1724    }
1725
1726    #[test]
1727    fn test_contains_parameter() {
1728        // Parameter inside an IntegerExpression over Variables
1729        let expr1: IntegerExpression<Variable> = IntegerExpression::Param(Parameter::new("x"));
1730        assert!(expr1.contains_parameter());
1731
1732        // No parameter present
1733        let expr2: IntegerExpression<Variable> = IntegerExpression::Const(1);
1734        assert!(!expr2.contains_parameter());
1735
1736        // Parameter nested in a binary expression lhs
1737        let expr3: IntegerExpression<Variable> =
1738            IntegerExpression::Param(Parameter::new("n")) + IntegerExpression::Const(2);
1739        assert!(expr3.contains_parameter());
1740
1741        // Parameter nested in a binary expression rhs
1742        let expr4: IntegerExpression<Variable> =
1743            IntegerExpression::Const(2) + IntegerExpression::Param(Parameter::new("n"));
1744        assert!(expr4.contains_parameter());
1745
1746        // No parameter in binary expression
1747        let expr5: IntegerExpression<Variable> =
1748            IntegerExpression::Const(2) + IntegerExpression::Const(2);
1749        assert!(!expr5.contains_parameter());
1750
1751        // Parameter in neg
1752        let expr6: IntegerExpression<Variable> =
1753            IntegerExpression::Neg(Box::new(IntegerExpression::Param(Parameter::new("n"))));
1754        assert!(expr6.contains_parameter());
1755
1756        // No parameter in neg
1757        let expr7: IntegerExpression<Variable> =
1758            IntegerExpression::Neg(Box::new(IntegerExpression::Const(1)));
1759        assert!(!expr7.contains_parameter());
1760
1761        // When the expression is over `Parameter` as the atomic type,
1762        // an `Atom(Parameter)` is NOT a parameter node and should return false.
1763        let expr8: IntegerExpression<Parameter> = IntegerExpression::Atom(Parameter::new("x"));
1764        assert!(!expr8.contains_parameter());
1765
1766        // But an explicit Param node still counts as a parameter.
1767        let expr9: IntegerExpression<Parameter> = IntegerExpression::Param(Parameter::new("y"));
1768        assert!(expr9.contains_parameter());
1769    }
1770}
taco_threshold_automaton/expressions/properties.rs

taco_threshold_automaton/expressions/
properties.rs
