smt_lang/problem/expression/
is_same.rs

1use super::*;
2
3pub trait IsSame {
4    fn is_same(&self, other: &Self) -> bool;
5
6    fn all_same(v1: &Vec<Expr>, v2: &Vec<Expr>) -> bool {
7        v1.iter().zip(v2.iter()).all(|(x, y)| x.is_same(y))
8    }
9}
10
11impl IsSame for Expr {
12    fn is_same(&self, other: &Self) -> bool {
13        match (self, other) {
14            (Expr::BoolValue(x, _), Expr::BoolValue(y, _)) => x == y,
15            (Expr::IntValue(x, _), Expr::IntValue(y, _)) => x == y,
16            (Expr::RealValue(x, _), Expr::RealValue(y, _)) => x == y,
17            (Expr::Unary(o1, e1, _), Expr::Unary(o2, e2, _)) => o1 == o2 && e1.is_same(e2),
18            (Expr::Binary(l1, o1, r1, _), Expr::Binary(l2, o2, r2, _)) => {
19                o1 == o2 && l1.is_same(l2) && r1.is_same(r2)
20            }
21            (Expr::Nary(o1, k1, _), Expr::Nary(o2, k2, _)) => o1 == o2 && Self::all_same(k1, k2),
22            (Expr::FunctionCall(i1, p1, _), Expr::FunctionCall(i2, p2, _)) => {
23                i1 == i2 && Self::all_same(p1, p2)
24            }
25            (Expr::Variable(i1, _), Expr::Variable(i2, _)) => i1 == i2,
26            (Expr::Parameter(p1), Expr::Parameter(p2)) => p1.is_same(p2),
27            (Expr::Instance(i1, _), Expr::Instance(i2, _)) => i1 == i2,
28            (Expr::StrucSelf(i1, _), Expr::StrucSelf(i2, _)) => i1 == i2,
29            (Expr::StrucAttribute(_, i1, _), Expr::StrucAttribute(_, i2, _)) => i1 == i2,
30            (Expr::StrucMetCall(e1, i1, a1, _), Expr::StrucMetCall(e2, i2, a2, _)) => {
31                e1.is_same(e2) && i1 == i2 && Self::all_same(a1, a2)
32            }
33            (Expr::ClassSelf(i1, _), Expr::ClassSelf(i2, _)) => i1 == i2,
34            (Expr::ClassAttribute(_, i1, _), Expr::ClassAttribute(_, i2, _)) => i1 == i2,
35            (Expr::ClassMetCall(e1, i1, a1, _), Expr::ClassMetCall(e2, i2, a2, _)) => {
36                e1.is_same(e2) && i1 == i2 && Self::all_same(a1, a2)
37            }
38            (Expr::AsClass(e1, i1), Expr::AsClass(e2, i2)) => i1 == i2 && e1.is_same(e2),
39            (Expr::AsInterval(e1, min1, max1, _), Expr::AsInterval(e2, min2, max2, _)) => {
40                min1 == min2 && max1 == max2 && e1.is_same(e2)
41            }
42            (Expr::AsInt(e1, _), Expr::AsInt(e2, _)) => e1.is_same(&e2),
43            (Expr::AsReal(e1, _), Expr::AsReal(e2, _)) => e1.is_same(&e2),
44            (Expr::IfThenElse(c1, t1, l1, e1, _), Expr::IfThenElse(c2, t2, l2, e2, _)) => {
45                c1.is_same(c2)
46                    && t1.is_same(t2)
47                    && l1.len() == l2.len()
48                    && l1
49                        .iter()
50                        .zip(l2.iter())
51                        .all(|((x1, y1), (x2, y2))| x1.is_same(x2) && y1.is_same(y2))
52                    && e1.is_same(e2)
53            }
54            (Expr::Quantifier(op1, p1, e1, _), Expr::Quantifier(op2, p2, e2, _)) => {
55                op1 == op2
56                    && p1.len() == p2.len()
57                    && p1.iter().zip(p2.iter()).all(|(x1, x2)| x1.is_same(x2))
58                    && e1.is_same(e2)
59            }
60            _ => false,
61        }
62    }
63}
smt_lang/problem/expression/is_same.rs

smt_lang/problem/expression/
is_same.rs
