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::{IntegerExpression, Location, 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> ops::BitAnd for BooleanExpression<T>
709where
710    T: Atomic,
711{
712    type Output = BooleanExpression<T>;
713
714    // Overload the `&` operator to represent the logical AND operation
715    fn bitand(self, other: BooleanExpression<T>) -> BooleanExpression<T> {
716        BooleanExpression::BinaryExpression(
717            Box::new(self),
718            super::BooleanConnective::And,
719            Box::new(other),
720        )
721    }
722}
723
724impl<T> ops::BitOr for BooleanExpression<T>
725where
726    T: Atomic,
727{
728    type Output = BooleanExpression<T>;
729
730    // Overload the `|` operator to represent the logical OR operation
731    fn bitor(self, other: BooleanExpression<T>) -> BooleanExpression<T> {
732        BooleanExpression::BinaryExpression(
733            Box::new(self),
734            super::BooleanConnective::Or,
735            Box::new(other),
736        )
737    }
738}
739
740impl ComparisonOp {
741    /// Invert the operation
742    ///
743    /// This function can for example be useful when negating a comparison
744    /// expression
745    ///
746    /// # Example
747    ///
748    /// ```
749    /// use taco_threshold_automaton::expressions::ComparisonOp;
750    ///
751    /// assert_eq!(ComparisonOp::Eq.invert(), ComparisonOp::Neq);
752    /// assert_eq!(ComparisonOp::Lt.invert(), ComparisonOp::Geq);
753    /// ```
754    pub fn invert(self) -> Self {
755        match self {
756            ComparisonOp::Eq => ComparisonOp::Neq,
757            ComparisonOp::Neq => ComparisonOp::Eq,
758            ComparisonOp::Lt => ComparisonOp::Geq,
759            ComparisonOp::Leq => ComparisonOp::Gt,
760            ComparisonOp::Gt => ComparisonOp::Leq,
761            ComparisonOp::Geq => ComparisonOp::Lt,
762        }
763    }
764
765    /// Swap the side of the comparison operator
766    ///
767    /// This is for example required when multiplying with negative constants
768    ///
769    /// # Example
770    ///
771    /// ```
772    /// use taco_threshold_automaton::expressions::ComparisonOp;
773    ///
774    /// assert_eq!(ComparisonOp::Eq.get_swap_side(), ComparisonOp::Eq);
775    /// assert_eq!(ComparisonOp::Lt.get_swap_side(), ComparisonOp::Gt);
776    /// ```
777    pub fn get_swap_side(self) -> Self {
778        match self {
779            ComparisonOp::Gt => ComparisonOp::Lt,
780            ComparisonOp::Geq => ComparisonOp::Leq,
781            ComparisonOp::Eq => ComparisonOp::Eq,
782            ComparisonOp::Neq => ComparisonOp::Neq,
783            ComparisonOp::Leq => ComparisonOp::Geq,
784            ComparisonOp::Lt => ComparisonOp::Gt,
785        }
786    }
787}
788
789impl BooleanConnective {
790    /// Get the dual operator of the connective
791    ///
792    /// # Example
793    ///
794    /// ```
795    /// use taco_threshold_automaton::expressions::*;
796    ///
797    /// assert_eq!(BooleanConnective::And.invert(), BooleanConnective::Or);
798    /// assert_eq!(BooleanConnective::Or.invert(), BooleanConnective::And);
799    /// ```
800    pub fn invert(self) -> Self {
801        match self {
802            BooleanConnective::And => BooleanConnective::Or,
803            BooleanConnective::Or => BooleanConnective::And,
804        }
805    }
806}
807
808#[cfg(test)]
809mod tests {
810    use std::collections::HashMap;
811
812    use crate::expressions::{
813        BooleanConnective, BooleanExpression, ComparisonOp, IntegerExpression, IntegerOp, Location,
814        Parameter, Variable, properties::EvaluationError,
815    };
816
817    #[test]
818    fn test_is_atomic() {
819        let expr: IntegerExpression<Variable> = IntegerExpression::Param(Parameter::new("x"));
820        assert!(expr.is_atomic());
821
822        let expr: IntegerExpression<Variable> = IntegerExpression::Atom(Variable::new("x"));
823        assert!(expr.is_atomic());
824
825        let expr: IntegerExpression<Variable> = IntegerExpression::Const(1);
826        assert!(!expr.is_atomic());
827
828        let expr: IntegerExpression<Variable> = IntegerExpression::BinaryExpr(
829            Box::new(IntegerExpression::Const(1)),
830            IntegerOp::Add,
831            Box::new(IntegerExpression::Const(1)),
832        );
833        assert!(!expr.is_atomic());
834
835        let expr: IntegerExpression<Variable> =
836            IntegerExpression::Neg(Box::new(IntegerExpression::Const(1)));
837        assert!(!expr.is_atomic());
838    }
839
840    #[test]
841    fn test_is_param_to_var() {
842        let expr: IntegerExpression<Parameter> = IntegerExpression::Atom(Parameter::new("x"));
843        let expected_expr: IntegerExpression<Variable> =
844            IntegerExpression::Param(Parameter::new("x"));
845        assert_eq!(
846            Into::<IntegerExpression<Variable>>::into(expr),
847            expected_expr
848        );
849
850        let expr: IntegerExpression<Parameter> = IntegerExpression::Param(Parameter::new("x"));
851        let expected_expr: IntegerExpression<Variable> =
852            IntegerExpression::Param(Parameter::new("x"));
853        assert_eq!(
854            Into::<IntegerExpression<Variable>>::into(expr),
855            expected_expr
856        );
857
858        let expr: IntegerExpression<Parameter> =
859            IntegerExpression::Neg(Box::new(IntegerExpression::Atom(Parameter::new("x"))));
860        let expected_expr: IntegerExpression<Variable> =
861            IntegerExpression::Neg(Box::new(IntegerExpression::Param(Parameter::new("x"))));
862        assert_eq!(
863            Into::<IntegerExpression<Variable>>::into(expr),
864            expected_expr
865        );
866
867        let expr: IntegerExpression<Parameter> = IntegerExpression::BinaryExpr(
868            Box::new(IntegerExpression::Atom(Parameter::new("x"))),
869            IntegerOp::Add,
870            Box::new(IntegerExpression::Const(1)),
871        );
872        let expected_expr: IntegerExpression<Variable> = IntegerExpression::BinaryExpr(
873            Box::new(IntegerExpression::Param(Parameter::new("x"))),
874            IntegerOp::Add,
875            Box::new(IntegerExpression::Const(1)),
876        );
877        assert_eq!(
878            Into::<IntegerExpression<Variable>>::into(expr),
879            expected_expr
880        );
881    }
882
883    #[test]
884    fn test_is_param_to_loc() {
885        let expr: IntegerExpression<Parameter> = IntegerExpression::Atom(Parameter::new("x"));
886        let expected_expr: IntegerExpression<Location> =
887            IntegerExpression::Param(Parameter::new("x"));
888        assert_eq!(
889            Into::<IntegerExpression<Location>>::into(expr),
890            expected_expr
891        );
892
893        let expr: IntegerExpression<Parameter> = IntegerExpression::Param(Parameter::new("x"));
894        let expected_expr: IntegerExpression<Location> =
895            IntegerExpression::Param(Parameter::new("x"));
896        assert_eq!(
897            Into::<IntegerExpression<Location>>::into(expr),
898            expected_expr
899        );
900
901        let expr: IntegerExpression<Parameter> =
902            IntegerExpression::Neg(Box::new(IntegerExpression::Atom(Parameter::new("x"))));
903        let expected_expr: IntegerExpression<Location> =
904            IntegerExpression::Neg(Box::new(IntegerExpression::Param(Parameter::new("x"))));
905        assert_eq!(
906            Into::<IntegerExpression<Location>>::into(expr),
907            expected_expr
908        );
909
910        let expr: IntegerExpression<Parameter> = IntegerExpression::BinaryExpr(
911            Box::new(IntegerExpression::Atom(Parameter::new("x"))),
912            IntegerOp::Add,
913            Box::new(IntegerExpression::Const(1)),
914        );
915        let expected_expr: IntegerExpression<Location> = IntegerExpression::BinaryExpr(
916            Box::new(IntegerExpression::Param(Parameter::new("x"))),
917            IntegerOp::Add,
918            Box::new(IntegerExpression::Const(1)),
919        );
920        assert_eq!(
921            Into::<IntegerExpression<Location>>::into(expr),
922            expected_expr
923        );
924    }
925
926    #[test]
927    fn test_integer_expression_addition() {
928        let expr1: IntegerExpression<Variable> = IntegerExpression::Const(1);
929        let expr2: IntegerExpression<Variable> = IntegerExpression::Const(2);
930        let result = expr1 + expr2;
931        assert_eq!(
932            result,
933            IntegerExpression::BinaryExpr(
934                Box::new(IntegerExpression::Const(1)),
935                IntegerOp::Add,
936                Box::new(IntegerExpression::Const(2)),
937            )
938        );
939    }
940
941    #[test]
942    fn test_integer_expression_subtraction() {
943        let expr1: IntegerExpression<Variable> = IntegerExpression::Const(3);
944        let expr2: IntegerExpression<Variable> = IntegerExpression::Const(2);
945        let result = expr1 - expr2;
946        assert_eq!(
947            result,
948            IntegerExpression::BinaryExpr(
949                Box::new(IntegerExpression::Const(3)),
950                IntegerOp::Sub,
951                Box::new(IntegerExpression::Const(2)),
952            )
953        );
954    }
955
956    #[test]
957    fn test_integer_expression_multiplication() {
958        let expr1: IntegerExpression<Variable> = IntegerExpression::Const(4);
959        let expr2: IntegerExpression<Variable> = IntegerExpression::Const(5);
960        let result = expr1 * expr2;
961        assert_eq!(
962            result,
963            IntegerExpression::BinaryExpr(
964                Box::new(IntegerExpression::Const(4)),
965                IntegerOp::Mul,
966                Box::new(IntegerExpression::Const(5)),
967            )
968        );
969    }
970
971    #[test]
972    fn test_integer_expression_division() {
973        let expr1: IntegerExpression<Variable> = IntegerExpression::Const(10);
974        let expr2: IntegerExpression<Variable> = IntegerExpression::Const(2);
975        let result = expr1 / expr2;
976        assert_eq!(
977            result,
978            IntegerExpression::BinaryExpr(
979                Box::new(IntegerExpression::Const(10)),
980                IntegerOp::Div,
981                Box::new(IntegerExpression::Const(2)),
982            )
983        );
984    }
985
986    #[test]
987    fn test_integer_expression_negation() {
988        let expr: IntegerExpression<Variable> = IntegerExpression::Const(5);
989        let result = -expr;
990        assert_eq!(
991            result,
992            IntegerExpression::Neg(Box::new(IntegerExpression::Const(5)))
993        );
994    }
995
996    #[test]
997    fn test_boolean_expression_negation() {
998        let expr: BooleanExpression<Variable> = BooleanExpression::True;
999        let result = !expr;
1000        assert_eq!(
1001            result,
1002            BooleanExpression::Not(Box::new(BooleanExpression::True))
1003        );
1004    }
1005
1006    #[test]
1007    fn test_boolean_expression_and() {
1008        let expr1: BooleanExpression<Variable> = BooleanExpression::True;
1009        let expr2: BooleanExpression<Variable> = BooleanExpression::True;
1010        let result = expr1 & expr2;
1011        assert_eq!(
1012            result,
1013            BooleanExpression::BinaryExpression(
1014                Box::new(BooleanExpression::True),
1015                BooleanConnective::And,
1016                Box::new(BooleanExpression::True),
1017            )
1018        );
1019    }
1020
1021    #[test]
1022    fn test_boolean_expression_or() {
1023        let expr1: BooleanExpression<Variable> = BooleanExpression::True;
1024        let expr2: BooleanExpression<Variable> = BooleanExpression::True;
1025        let result = expr1 | expr2;
1026        assert_eq!(
1027            result,
1028            BooleanExpression::BinaryExpression(
1029                Box::new(BooleanExpression::True),
1030                BooleanConnective::Or,
1031                Box::new(BooleanExpression::True),
1032            )
1033        );
1034    }
1035
1036    #[test]
1037    fn test_boolean_expr_param_to_loc() {
1038        let expr: BooleanExpression<Parameter> = BooleanExpression::True;
1039        let expected_expr: BooleanExpression<Location> = BooleanExpression::True;
1040        assert_eq!(
1041            Into::<BooleanExpression<Location>>::into(expr),
1042            expected_expr
1043        );
1044
1045        let expr: BooleanExpression<Parameter> = BooleanExpression::False;
1046        let expected_expr: BooleanExpression<Location> = BooleanExpression::False;
1047        assert_eq!(
1048            Into::<BooleanExpression<Location>>::into(expr),
1049            expected_expr
1050        );
1051
1052        let expr: BooleanExpression<Parameter> =
1053            BooleanExpression::Not(Box::new(BooleanExpression::True));
1054        let expected_expr: BooleanExpression<Location> =
1055            BooleanExpression::Not(Box::new(BooleanExpression::True));
1056        assert_eq!(
1057            Into::<BooleanExpression<Location>>::into(expr),
1058            expected_expr
1059        );
1060
1061        let expr: BooleanExpression<Parameter> = BooleanExpression::BinaryExpression(
1062            Box::new(BooleanExpression::True),
1063            BooleanConnective::And,
1064            Box::new(BooleanExpression::False),
1065        );
1066        let expected_expr: BooleanExpression<Location> = BooleanExpression::BinaryExpression(
1067            Box::new(BooleanExpression::True),
1068            BooleanConnective::And,
1069            Box::new(BooleanExpression::False),
1070        );
1071        assert_eq!(
1072            Into::<BooleanExpression<Location>>::into(expr),
1073            expected_expr
1074        );
1075
1076        let expr: BooleanExpression<Parameter> = BooleanExpression::ComparisonExpression(
1077            Box::new(IntegerExpression::Const(42)),
1078            ComparisonOp::Leq,
1079            Box::new(IntegerExpression::Atom(Parameter::new("n"))),
1080        );
1081        let expected_expr: BooleanExpression<Location> = BooleanExpression::ComparisonExpression(
1082            Box::new(IntegerExpression::Const(42)),
1083            ComparisonOp::Leq,
1084            Box::new(IntegerExpression::Param(Parameter::new("n"))),
1085        );
1086        assert_eq!(
1087            Into::<BooleanExpression<Location>>::into(expr),
1088            expected_expr
1089        );
1090    }
1091
1092    #[test]
1093    fn test_boolean_expr_param_to_var() {
1094        let expr: BooleanExpression<Parameter> = BooleanExpression::True;
1095        let expected_expr: BooleanExpression<Variable> = BooleanExpression::True;
1096        assert_eq!(
1097            Into::<BooleanExpression<Variable>>::into(expr),
1098            expected_expr
1099        );
1100
1101        let expr: BooleanExpression<Parameter> = BooleanExpression::False;
1102        let expected_expr: BooleanExpression<Variable> = BooleanExpression::False;
1103        assert_eq!(
1104            Into::<BooleanExpression<Variable>>::into(expr),
1105            expected_expr
1106        );
1107
1108        let expr: BooleanExpression<Parameter> =
1109            BooleanExpression::Not(Box::new(BooleanExpression::True));
1110        let expected_expr: BooleanExpression<Variable> =
1111            BooleanExpression::Not(Box::new(BooleanExpression::True));
1112        assert_eq!(
1113            Into::<BooleanExpression<Variable>>::into(expr),
1114            expected_expr
1115        );
1116
1117        let expr: BooleanExpression<Parameter> = BooleanExpression::BinaryExpression(
1118            Box::new(BooleanExpression::True),
1119            BooleanConnective::And,
1120            Box::new(BooleanExpression::False),
1121        );
1122        let expected_expr: BooleanExpression<Variable> = BooleanExpression::BinaryExpression(
1123            Box::new(BooleanExpression::True),
1124            BooleanConnective::And,
1125            Box::new(BooleanExpression::False),
1126        );
1127        assert_eq!(
1128            Into::<BooleanExpression<Variable>>::into(expr),
1129            expected_expr
1130        );
1131
1132        let expr: BooleanExpression<Parameter> = BooleanExpression::ComparisonExpression(
1133            Box::new(IntegerExpression::Const(42)),
1134            ComparisonOp::Leq,
1135            Box::new(IntegerExpression::Atom(Parameter::new("n"))),
1136        );
1137        let expected_expr: BooleanExpression<Variable> = BooleanExpression::ComparisonExpression(
1138            Box::new(IntegerExpression::Const(42)),
1139            ComparisonOp::Leq,
1140            Box::new(IntegerExpression::Param(Parameter::new("n"))),
1141        );
1142        assert_eq!(
1143            Into::<BooleanExpression<Variable>>::into(expr),
1144            expected_expr
1145        );
1146    }
1147
1148    #[test]
1149    fn test_integer_expression_contains_atom() {
1150        let expr1: IntegerExpression<Variable> = IntegerExpression::Atom(Variable::new("x"));
1151        assert!(expr1.contains_atom());
1152
1153        let expr2: IntegerExpression<Variable> = IntegerExpression::Const(1);
1154        assert!(!expr2.contains_atom());
1155
1156        let expr3: IntegerExpression<Variable> = IntegerExpression::Param(Parameter::new("y"));
1157        assert!(!expr3.contains_atom());
1158
1159        let expr4: IntegerExpression<Variable> =
1160            IntegerExpression::Neg(Box::new(IntegerExpression::Atom(Variable::new("z"))));
1161        assert!(expr4.contains_atom());
1162
1163        let expr5: IntegerExpression<Variable> = IntegerExpression::BinaryExpr(
1164            Box::new(IntegerExpression::Atom(Variable::new("a"))),
1165            IntegerOp::Add,
1166            Box::new(IntegerExpression::Const(1)),
1167        );
1168        assert!(expr5.contains_atom());
1169    }
1170
1171    #[test]
1172    fn test_swap_side_comp_op() {
1173        assert_eq!(ComparisonOp::Eq.get_swap_side(), ComparisonOp::Eq);
1174        assert_eq!(ComparisonOp::Neq.get_swap_side(), ComparisonOp::Neq);
1175        assert_eq!(ComparisonOp::Lt.get_swap_side(), ComparisonOp::Gt);
1176        assert_eq!(ComparisonOp::Leq.get_swap_side(), ComparisonOp::Geq);
1177        assert_eq!(ComparisonOp::Gt.get_swap_side(), ComparisonOp::Lt);
1178        assert_eq!(ComparisonOp::Geq.get_swap_side(), ComparisonOp::Leq);
1179    }
1180
1181    #[test]
1182    fn test_invert_comp_op() {
1183        assert_eq!(ComparisonOp::Eq.invert(), ComparisonOp::Neq);
1184        assert_eq!(ComparisonOp::Neq.invert(), ComparisonOp::Eq);
1185        assert_eq!(ComparisonOp::Lt.invert(), ComparisonOp::Geq);
1186        assert_eq!(ComparisonOp::Leq.invert(), ComparisonOp::Gt);
1187        assert_eq!(ComparisonOp::Gt.invert(), ComparisonOp::Leq);
1188        assert_eq!(ComparisonOp::Geq.invert(), ComparisonOp::Lt);
1189    }
1190
1191    #[test]
1192    fn test_invert_boolean_connective() {
1193        assert_eq!(BooleanConnective::And.invert(), BooleanConnective::Or);
1194        assert_eq!(BooleanConnective::Or.invert(), BooleanConnective::And);
1195    }
1196
1197    #[test]
1198    fn test_try_to_evaluate_to_const() {
1199        let expr = IntegerExpression::<Location>::Const(5) + IntegerExpression::Const(3);
1200        assert_eq!(expr.try_to_evaluate_to_const(), Some(8));
1201
1202        let expr = IntegerExpression::<Location>::Const(5) - IntegerExpression::Const(3);
1203        assert_eq!(expr.try_to_evaluate_to_const(), Some(2));
1204
1205        let expr = IntegerExpression::<Location>::Const(10) / IntegerExpression::Const(5);
1206        assert_eq!(expr.try_to_evaluate_to_const(), Some(2));
1207
1208        let expr = -IntegerExpression::Const(42) / IntegerExpression::<Location>::Const(2);
1209        assert_eq!(expr.try_to_evaluate_to_const(), Some(-21));
1210
1211        let expr = -IntegerExpression::<Location>::Const(42) * IntegerExpression::Const(2);
1212        assert_eq!(expr.try_to_evaluate_to_const(), Some(-84));
1213
1214        let expr = IntegerExpression::<Location>::Param(Parameter::new("n"));
1215        assert_eq!(expr.try_to_evaluate_to_const(), None);
1216
1217        let expr = -IntegerExpression::Const(42) / IntegerExpression::Atom(Location::new("loc"));
1218        assert_eq!(expr.try_to_evaluate_to_const(), None);
1219    }
1220
1221    #[test]
1222    fn test_try_to_evaluate_to_const_with_env() {
1223        let env = HashMap::from([(Location::new("loc"), 1)]);
1224        let param_env = HashMap::from([(Parameter::new("n"), 1)]);
1225
1226        let expr = IntegerExpression::<Location>::Const(5) + IntegerExpression::Const(3);
1227        assert_eq!(
1228            expr.try_to_evaluate_to_const_with_env(&env, &param_env),
1229            Ok(8)
1230        );
1231
1232        let expr = IntegerExpression::<Location>::Const(5) - IntegerExpression::Const(3);
1233        assert_eq!(
1234            expr.try_to_evaluate_to_const_with_env(&env, &param_env),
1235            Ok(2)
1236        );
1237
1238        let expr = IntegerExpression::<Location>::Const(10) / IntegerExpression::Const(5);
1239        assert_eq!(
1240            expr.try_to_evaluate_to_const_with_env(&env, &param_env),
1241            Ok(2)
1242        );
1243
1244        let expr = -IntegerExpression::Const(42) / IntegerExpression::<Location>::Const(2);
1245        assert_eq!(
1246            expr.try_to_evaluate_to_const_with_env(&env, &param_env),
1247            Ok(-21)
1248        );
1249
1250        let expr = -IntegerExpression::<Location>::Const(42) * IntegerExpression::Const(2);
1251        assert_eq!(
1252            expr.try_to_evaluate_to_const_with_env(&env, &param_env),
1253            Ok(-84)
1254        );
1255
1256        let expr = IntegerExpression::Atom(Location::new("loc"));
1257        assert_eq!(
1258            expr.try_to_evaluate_to_const_with_env(&env, &param_env),
1259            Ok(1)
1260        );
1261
1262        let expr = -IntegerExpression::Const(42) / IntegerExpression::Atom(Location::new("loc"));
1263        assert_eq!(
1264            expr.try_to_evaluate_to_const_with_env(&env, &param_env),
1265            Ok(-42)
1266        );
1267
1268        let expr = IntegerExpression::<Location>::Param(Parameter::new("n"));
1269        assert_eq!(
1270            expr.try_to_evaluate_to_const_with_env(&HashMap::new(), &param_env),
1271            Ok(1)
1272        );
1273
1274        let expr = IntegerExpression::<Location>::Param(Parameter::new("n"));
1275        assert_eq!(
1276            expr.try_to_evaluate_to_const_with_env(&env, &HashMap::new()),
1277            Err(EvaluationError::ParameterNotFound(Parameter::new("n")))
1278        );
1279
1280        let expr = IntegerExpression::Atom(Location::new("loc"));
1281        assert_eq!(
1282            expr.try_to_evaluate_to_const_with_env(&HashMap::new(), &param_env),
1283            Err(EvaluationError::AtomicNotFound(Location::new("loc")))
1284        );
1285    }
1286
1287    #[test]
1288    fn test_boolean_expr_check_satisfied() {
1289        let env = HashMap::from([(Location::new("loc"), 1)]);
1290        let param_env = HashMap::from([(Parameter::new("n"), 1)]);
1291
1292        let expr = BooleanExpression::ComparisonExpression(
1293            Box::new(IntegerExpression::Const(5)),
1294            ComparisonOp::Eq,
1295            Box::new(IntegerExpression::Const(5)),
1296        );
1297        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(true));
1298
1299        let expr = BooleanExpression::ComparisonExpression(
1300            Box::new(IntegerExpression::Const(5)),
1301            ComparisonOp::Eq,
1302            Box::new(IntegerExpression::Const(3)),
1303        );
1304        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(false));
1305
1306        let expr = BooleanExpression::ComparisonExpression(
1307            Box::new(IntegerExpression::Const(5)),
1308            ComparisonOp::Lt,
1309            Box::new(IntegerExpression::Const(3)),
1310        );
1311        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(false));
1312
1313        let expr = BooleanExpression::ComparisonExpression(
1314            Box::new(IntegerExpression::Const(5)),
1315            ComparisonOp::Lt,
1316            Box::new(IntegerExpression::Const(10)),
1317        );
1318        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(true));
1319
1320        let expr = BooleanExpression::ComparisonExpression(
1321            Box::new(IntegerExpression::Const(5)),
1322            ComparisonOp::Leq,
1323            Box::new(IntegerExpression::Const(5)),
1324        );
1325        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(true));
1326
1327        let expr = BooleanExpression::ComparisonExpression(
1328            Box::new(IntegerExpression::Const(5)),
1329            ComparisonOp::Leq,
1330            Box::new(IntegerExpression::Const(3)),
1331        );
1332        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(false));
1333
1334        let expr = BooleanExpression::ComparisonExpression(
1335            Box::new(IntegerExpression::Const(5)),
1336            ComparisonOp::Gt,
1337            Box::new(IntegerExpression::Const(3)),
1338        );
1339        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(true));
1340
1341        let expr = BooleanExpression::ComparisonExpression(
1342            Box::new(IntegerExpression::Const(5)),
1343            ComparisonOp::Gt,
1344            Box::new(IntegerExpression::Const(10)),
1345        );
1346        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(false));
1347
1348        let expr = BooleanExpression::ComparisonExpression(
1349            Box::new(IntegerExpression::Const(5)),
1350            ComparisonOp::Neq,
1351            Box::new(IntegerExpression::Const(5)),
1352        );
1353        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(false));
1354
1355        let expr = BooleanExpression::ComparisonExpression(
1356            Box::new(IntegerExpression::Const(5)),
1357            ComparisonOp::Neq,
1358            Box::new(IntegerExpression::Const(3)),
1359        );
1360        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(true));
1361
1362        let expr = BooleanExpression::ComparisonExpression(
1363            Box::new(IntegerExpression::Const(5)),
1364            ComparisonOp::Geq,
1365            Box::new(IntegerExpression::Const(3)),
1366        );
1367        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(true));
1368
1369        let expr = BooleanExpression::ComparisonExpression(
1370            Box::new(IntegerExpression::Const(5)),
1371            ComparisonOp::Geq,
1372            Box::new(IntegerExpression::Const(10)),
1373        );
1374        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(false));
1375
1376        let expr = BooleanExpression::BinaryExpression(
1377            Box::new(BooleanExpression::True),
1378            BooleanConnective::And,
1379            Box::new(BooleanExpression::True),
1380        );
1381        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(true));
1382
1383        let expr = BooleanExpression::BinaryExpression(
1384            Box::new(BooleanExpression::True),
1385            BooleanConnective::Or,
1386            Box::new(BooleanExpression::False),
1387        );
1388        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(true));
1389
1390        let expr = !BooleanExpression::False;
1391        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(true));
1392
1393        let expr = BooleanExpression::False;
1394        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(false));
1395    }
1396
1397    #[test]
1398    fn test_display_evaluation_error() {
1399        let error = EvaluationError::AtomicNotFound(Location::new("loc"));
1400        assert!(
1401            error
1402                .to_string()
1403                .contains(&Location::new("loc").to_string())
1404        );
1405
1406        let error: EvaluationError<Location> =
1407            EvaluationError::ParameterNotFound(Parameter::new("n"));
1408        assert!(error.to_string().contains("n"));
1409    }
1410
1411    #[test]
1412    fn test_contains_atom_a_integer_expr() {
1413        let atom = Variable::new("x");
1414
1415        let expr1: IntegerExpression<Variable> = IntegerExpression::Atom(atom.clone());
1416        assert!(expr1.contains_atom_a(&atom));
1417
1418        let expr2: IntegerExpression<Variable> = IntegerExpression::Const(1);
1419        assert!(!expr2.contains_atom_a(&atom));
1420
1421        let expr3: IntegerExpression<Variable> = IntegerExpression::Param(Parameter::new("y"));
1422        assert!(!expr3.contains_atom_a(&atom));
1423
1424        let expr4: IntegerExpression<Variable> =
1425            IntegerExpression::Neg(Box::new(IntegerExpression::Atom(atom.clone())));
1426        assert!(expr4.contains_atom_a(&atom));
1427
1428        let expr5: IntegerExpression<Variable> = IntegerExpression::BinaryExpr(
1429            Box::new(IntegerExpression::Atom(atom.clone())),
1430            IntegerOp::Add,
1431            Box::new(IntegerExpression::Const(1)),
1432        );
1433        assert!(expr5.contains_atom_a(&atom));
1434
1435        let expr6: IntegerExpression<Variable> = IntegerExpression::BinaryExpr(
1436            Box::new(IntegerExpression::Const(1)),
1437            IntegerOp::Add,
1438            Box::new(IntegerExpression::Const(2)),
1439        );
1440        assert!(!expr6.contains_atom_a(&atom));
1441    }
1442
1443    #[test]
1444    fn test_contains_atom_a_boolean_expr() {
1445        let atom = Variable::new("x");
1446
1447        let expr1: BooleanExpression<Variable> = BooleanExpression::ComparisonExpression(
1448            Box::new(IntegerExpression::Atom(atom.clone())),
1449            ComparisonOp::Eq,
1450            Box::new(IntegerExpression::Const(1)),
1451        );
1452        assert!(expr1.contains_atom_a(&atom));
1453
1454        let expr2: BooleanExpression<Variable> = BooleanExpression::ComparisonExpression(
1455            Box::new(IntegerExpression::Atom(Variable::new("y"))),
1456            ComparisonOp::Eq,
1457            Box::new(IntegerExpression::Const(2)),
1458        );
1459        assert!(!expr2.contains_atom_a(&atom));
1460
1461        let expr3: BooleanExpression<Variable> = BooleanExpression::BinaryExpression(
1462            Box::new(BooleanExpression::ComparisonExpression(
1463                Box::new(IntegerExpression::Atom(atom.clone())),
1464                ComparisonOp::Eq,
1465                Box::new(IntegerExpression::Const(1)),
1466            )),
1467            BooleanConnective::And,
1468            Box::new(BooleanExpression::True),
1469        );
1470        assert!(expr3.contains_atom_a(&atom));
1471
1472        let expr4: BooleanExpression<Variable> =
1473            BooleanExpression::Not(Box::new(BooleanExpression::ComparisonExpression(
1474                Box::new(IntegerExpression::Atom(atom.clone())),
1475                ComparisonOp::Eq,
1476                Box::new(IntegerExpression::Const(1)),
1477            )));
1478        assert!(expr4.contains_atom_a(&atom));
1479
1480        let expr5: BooleanExpression<Variable> = BooleanExpression::True;
1481        assert!(!expr5.contains_atom_a(&atom));
1482
1483        let expr6: BooleanExpression<Variable> = BooleanExpression::False;
1484        assert!(!expr6.contains_atom_a(&atom));
1485    }
1486
1487    #[test]
1488    fn test_boolean_expression_complex() {
1489        let env = HashMap::from([(Location::new("loc"), 1)]);
1490        let param_env = HashMap::from([(Parameter::new("n"), 1)]);
1491
1492        let expr = BooleanExpression::BinaryExpression(
1493            Box::new(BooleanExpression::ComparisonExpression(
1494                Box::new(IntegerExpression::Const(5)),
1495                ComparisonOp::Eq,
1496                Box::new(IntegerExpression::Const(5)),
1497            )),
1498            BooleanConnective::And,
1499            Box::new(BooleanExpression::ComparisonExpression(
1500                Box::new(IntegerExpression::Const(3)),
1501                ComparisonOp::Lt,
1502                Box::new(IntegerExpression::Const(10)),
1503            )),
1504        );
1505        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(true));
1506
1507        let expr = BooleanExpression::BinaryExpression(
1508            Box::new(BooleanExpression::ComparisonExpression(
1509                Box::new(IntegerExpression::Const(5)),
1510                ComparisonOp::Eq,
1511                Box::new(IntegerExpression::Const(3)),
1512            )),
1513            BooleanConnective::Or,
1514            Box::new(BooleanExpression::ComparisonExpression(
1515                Box::new(IntegerExpression::Const(3)),
1516                ComparisonOp::Lt,
1517                Box::new(IntegerExpression::Const(10)),
1518            )),
1519        );
1520        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(true));
1521
1522        let expr = BooleanExpression::Not(Box::new(BooleanExpression::ComparisonExpression(
1523            Box::new(IntegerExpression::Const(5)),
1524            ComparisonOp::Eq,
1525            Box::new(IntegerExpression::Const(3)),
1526        )));
1527        assert_eq!(expr.check_satisfied(&env, &param_env), Ok(true));
1528    }
1529
1530    #[test]
1531    fn test_integer_expression_substitute_atom() {
1532        let atom = Variable::new("x");
1533        let replacement = IntegerExpression::Const(42);
1534
1535        let expr1: IntegerExpression<Variable> = IntegerExpression::Atom(atom.clone());
1536        let mut result = expr1.clone();
1537        result.substitute_atom_with(&atom, &replacement);
1538        assert_eq!(result, replacement);
1539
1540        let expr2: IntegerExpression<Variable> = IntegerExpression::Const(1);
1541        let mut result = expr2.clone();
1542        result.substitute_atom_with(&atom, &replacement);
1543        assert_eq!(result, expr2);
1544
1545        let expr3: IntegerExpression<Variable> = IntegerExpression::Param(Parameter::new("y"));
1546        let mut result = expr3.clone();
1547        result.substitute_atom_with(&atom, &replacement);
1548        assert_eq!(result, expr3);
1549
1550        let expr4: IntegerExpression<Variable> =
1551            IntegerExpression::Neg(Box::new(IntegerExpression::Atom(atom.clone())));
1552        let expected = IntegerExpression::Neg(Box::new(replacement.clone()));
1553        let mut result = expr4;
1554        result.substitute_atom_with(&atom, &replacement);
1555        assert_eq!(result, expected);
1556
1557        let expr5: IntegerExpression<Variable> = IntegerExpression::BinaryExpr(
1558            Box::new(IntegerExpression::Atom(atom.clone())),
1559            IntegerOp::Add,
1560            Box::new(IntegerExpression::Const(1)),
1561        );
1562        let expected = IntegerExpression::BinaryExpr(
1563            Box::new(replacement.clone()),
1564            IntegerOp::Add,
1565            Box::new(IntegerExpression::Const(1)),
1566        );
1567        let mut result = expr5.clone();
1568        result.substitute_atom_with(&atom, &replacement);
1569        assert_eq!(result, expected);
1570
1571        let expr6: IntegerExpression<Variable> = IntegerExpression::BinaryExpr(
1572            Box::new(IntegerExpression::Const(1)),
1573            IntegerOp::Add,
1574            Box::new(IntegerExpression::Const(2)),
1575        );
1576        let mut result = expr6.clone();
1577        result.substitute_atom_with(&atom, &replacement);
1578        assert_eq!(result, expr6);
1579    }
1580
1581    #[test]
1582    fn test_boolean_expr_substitute_atom() {
1583        let atom = Variable::new("x");
1584        let replacement = IntegerExpression::Const(42);
1585
1586        let expr1: BooleanExpression<Variable> = BooleanExpression::ComparisonExpression(
1587            Box::new(IntegerExpression::Atom(atom.clone())),
1588            ComparisonOp::Eq,
1589            Box::new(IntegerExpression::Const(1)),
1590        );
1591        let expected = BooleanExpression::ComparisonExpression(
1592            Box::new(replacement.clone()),
1593            ComparisonOp::Eq,
1594            Box::new(IntegerExpression::Const(1)),
1595        );
1596        let mut result = expr1.clone();
1597        result.substitute_atom_with(&atom, &replacement);
1598        assert_eq!(result, expected);
1599
1600        let expr2: BooleanExpression<Variable> = BooleanExpression::BinaryExpression(
1601            Box::new(BooleanExpression::ComparisonExpression(
1602                Box::new(IntegerExpression::Atom(atom.clone())),
1603                ComparisonOp::Eq,
1604                Box::new(IntegerExpression::Const(1)),
1605            )),
1606            BooleanConnective::And,
1607            Box::new(BooleanExpression::True),
1608        );
1609        let expected = BooleanExpression::BinaryExpression(
1610            Box::new(BooleanExpression::ComparisonExpression(
1611                Box::new(replacement.clone()),
1612                ComparisonOp::Eq,
1613                Box::new(IntegerExpression::Const(1)),
1614            )),
1615            BooleanConnective::And,
1616            Box::new(BooleanExpression::True),
1617        );
1618        let mut result = expr2.clone();
1619        result.substitute_atom_with(&atom, &replacement);
1620        assert_eq!(result, expected);
1621
1622        let expr3: BooleanExpression<Variable> =
1623            BooleanExpression::Not(Box::new(BooleanExpression::ComparisonExpression(
1624                Box::new(IntegerExpression::Atom(atom.clone())),
1625                ComparisonOp::Eq,
1626                Box::new(IntegerExpression::Const(1)),
1627            )));
1628        let expected = BooleanExpression::Not(Box::new(BooleanExpression::ComparisonExpression(
1629            Box::new(replacement.clone()),
1630            ComparisonOp::Eq,
1631            Box::new(IntegerExpression::Const(1)),
1632        )));
1633        let mut result = expr3.clone();
1634        result.substitute_atom_with(&atom, &replacement);
1635        assert_eq!(result, expected);
1636
1637        let expr4: BooleanExpression<Variable> = BooleanExpression::True;
1638        let mut result = expr4.clone();
1639        result.substitute_atom_with(&atom, &replacement);
1640        assert_eq!(result, expr4);
1641
1642        let expr5: BooleanExpression<Variable> = BooleanExpression::False;
1643        let mut result = expr5.clone();
1644        result.substitute_atom_with(&atom, &replacement);
1645        assert_eq!(result, expr5);
1646    }
1647
1648    #[test]
1649    fn test_try_check_expr_constraints_to_zero() {
1650        let atom = Location::new("loc");
1651        let expr = BooleanExpression::ComparisonExpression(
1652            Box::new(IntegerExpression::Atom(atom.clone())),
1653            ComparisonOp::Eq,
1654            Box::new(IntegerExpression::Const(0)),
1655        );
1656        assert!(expr.try_check_expr_constraints_to_zero(&atom));
1657
1658        let expr = BooleanExpression::ComparisonExpression(
1659            Box::new(IntegerExpression::Atom(atom.clone())),
1660            ComparisonOp::Leq,
1661            Box::new(IntegerExpression::Const(0)),
1662        );
1663        assert!(expr.try_check_expr_constraints_to_zero(&atom));
1664
1665        let expr = BooleanExpression::ComparisonExpression(
1666            Box::new(IntegerExpression::Atom(atom.clone())),
1667            ComparisonOp::Lt,
1668            Box::new(IntegerExpression::Const(1)),
1669        );
1670        assert!(expr.try_check_expr_constraints_to_zero(&atom));
1671
1672        let expr = BooleanExpression::ComparisonExpression(
1673            Box::new(IntegerExpression::Atom(atom.clone())),
1674            ComparisonOp::Geq,
1675            Box::new(IntegerExpression::Const(0)),
1676        );
1677        assert!(!expr.try_check_expr_constraints_to_zero(&atom));
1678
1679        let expr = BooleanExpression::ComparisonExpression(
1680            Box::new(IntegerExpression::Atom(Location::new("otherloc"))),
1681            ComparisonOp::Eq,
1682            Box::new(IntegerExpression::Const(0)),
1683        );
1684        assert!(!expr.try_check_expr_constraints_to_zero(&atom));
1685
1686        let expr = !BooleanExpression::ComparisonExpression(
1687            Box::new(IntegerExpression::Atom(atom.clone())),
1688            ComparisonOp::Gt,
1689            Box::new(IntegerExpression::Const(1)),
1690        );
1691        assert!(!expr.try_check_expr_constraints_to_zero(&atom));
1692
1693        let atom = Location::new("loc");
1694        let expr = BooleanExpression::ComparisonExpression(
1695            Box::new(IntegerExpression::Const(0)),
1696            ComparisonOp::Eq,
1697            Box::new(IntegerExpression::Atom(atom.clone())),
1698        );
1699        assert!(expr.try_check_expr_constraints_to_zero(&atom));
1700    }
1701
1702    #[test]
1703    fn test_try_const_from_integer() {
1704        let expr: IntegerExpression<Location> = 1_u32.into();
1705        assert_eq!(expr, IntegerExpression::Const(1));
1706    }
1707
1708    #[test]
1709    fn test_integer_expr_from_location() {
1710        let loc = Location::new("loc");
1711        let expected_expr = IntegerExpression::Atom(Location::new("loc"));
1712        assert_eq!(IntegerExpression::from(loc), expected_expr);
1713    }
1714
1715    #[test]
1716    fn test_contains_parameter() {
1717        // Parameter inside an IntegerExpression over Variables
1718        let expr1: IntegerExpression<Variable> = IntegerExpression::Param(Parameter::new("x"));
1719        assert!(expr1.contains_parameter());
1720
1721        // No parameter present
1722        let expr2: IntegerExpression<Variable> = IntegerExpression::Const(1);
1723        assert!(!expr2.contains_parameter());
1724
1725        // Parameter nested in a binary expression lhs
1726        let expr3: IntegerExpression<Variable> =
1727            IntegerExpression::Param(Parameter::new("n")) + IntegerExpression::Const(2);
1728        assert!(expr3.contains_parameter());
1729
1730        // Parameter nested in a binary expression rhs
1731        let expr4: IntegerExpression<Variable> =
1732            IntegerExpression::Const(2) + IntegerExpression::Param(Parameter::new("n"));
1733        assert!(expr4.contains_parameter());
1734
1735        // No parameter in binary expression
1736        let expr5: IntegerExpression<Variable> =
1737            IntegerExpression::Const(2) + IntegerExpression::Const(2);
1738        assert!(!expr5.contains_parameter());
1739
1740        // Parameter in neg
1741        let expr6: IntegerExpression<Variable> =
1742            IntegerExpression::Neg(Box::new(IntegerExpression::Param(Parameter::new("n"))));
1743        assert!(expr6.contains_parameter());
1744
1745        // No parameter in neg
1746        let expr7: IntegerExpression<Variable> =
1747            IntegerExpression::Neg(Box::new(IntegerExpression::Const(1)));
1748        assert!(!expr7.contains_parameter());
1749
1750        // When the expression is over `Parameter` as the atomic type,
1751        // an `Atom(Parameter)` is NOT a parameter node and should return false.
1752        let expr8: IntegerExpression<Parameter> = IntegerExpression::Atom(Parameter::new("x"));
1753        assert!(!expr8.contains_parameter());
1754
1755        // But an explicit Param node still counts as a parameter.
1756        let expr9: IntegerExpression<Parameter> = IntegerExpression::Param(Parameter::new("y"));
1757        assert!(expr9.contains_parameter());
1758    }
1759}
taco_threshold_automaton/expressions/properties.rs

taco_threshold_automaton/expressions/
properties.rs
