smt_lang/problem/expression/
typ.rs

1use crate::problem::*;
2
3impl Expr {
4    pub fn typ(&self, problem: &Problem) -> Type {
5        match self {
6            Expr::BoolValue(_, _) => Type::Bool,
7            Expr::IntValue(value, _) => Type::Interval(*value, *value),
8            Expr::RealValue(_, _) => Type::Real,
9            Expr::Unary(op, e, _) => match op {
10                UnaryOp::Not => Type::Bool,
11                UnaryOp::Minus => match e.typ(problem) {
12                    Type::Int => Type::Int,
13                    Type::Real => Type::Real,
14                    Type::Interval(min, max) => Type::Interval(-max, -min),
15                    _ => Type::Undefined,
16                },
17            },
18            Expr::Binary(left, op, right, _) => match op {
19                BinOp::Eq => Type::Bool,
20                BinOp::Ne => Type::Bool,
21                BinOp::Lt => Type::Bool,
22                BinOp::Le => Type::Bool,
23                BinOp::Ge => Type::Bool,
24                BinOp::Gt => Type::Bool,
25                BinOp::And => Type::Bool,
26                BinOp::Or => Type::Bool,
27                BinOp::Implies => Type::Bool,
28                //
29                BinOp::Add => match (left.typ(problem), right.typ(problem)) {
30                    (Type::Int, _) => Type::Int,
31                    (Type::Real, _) => Type::Real,
32                    (Type::Interval(_, _), Type::Int) => Type::Int,
33                    (Type::Interval(min1, max1), Type::Interval(min2, max2)) => {
34                        Type::Interval(min1 + min2, max1 + max2)
35                    }
36                    _ => Type::Undefined,
37                },
38                BinOp::Sub => match (left.typ(problem), right.typ(problem)) {
39                    (Type::Int, _) => Type::Int,
40                    (Type::Real, _) => Type::Real,
41                    (Type::Interval(_, _), Type::Int) => Type::Int,
42                    (Type::Interval(min1, max1), Type::Interval(min2, max2)) => {
43                        Type::Interval(min1 - min2, max1 - max2)
44                    }
45                    _ => Type::Undefined,
46                },
47                BinOp::Mul => match (left.typ(problem), right.typ(problem)) {
48                    (Type::Int, _) => Type::Int,
49                    (Type::Real, _) => Type::Real,
50                    (Type::Interval(_, _), Type::Int) => Type::Int,
51                    (Type::Interval(min1, max1), Type::Interval(min2, max2)) => {
52                        Type::Interval(min1 * min2, max1 * max2)
53                    }
54                    _ => Type::Undefined,
55                },
56                BinOp::Div => Type::Real,
57            },
58            Expr::Nary(o, v, _) => {
59                if let Some((first, others)) = v.split_first() {
60                    let mut t = first.typ(problem);
61                    for e in others {
62                        let tt = t.clone();
63                        let te = e.typ(problem);
64                        if tt != te {
65                            match (tt, te) {
66                                (Type::Interval(min1, max1), Type::Interval(min2, max2)) => match o
67                                {
68                                    NaryOp::Min => {
69                                        t = Type::Interval(min1.min(min2), max1.min(max2))
70                                    }
71                                    NaryOp::Max => {
72                                        t = Type::Interval(min1.max(min2), max1.max(max2))
73                                    }
74                                },
75                                (Type::Int, Type::Interval(_, _)) => {}
76                                (Type::Interval(_, _), Type::Int) => t = Type::Int,
77                                _ => return Type::Undefined,
78                            }
79                        }
80                    }
81                    t
82                } else {
83                    Type::Undefined
84                }
85            }
86            Expr::FunctionCall(id, _, _) => problem.get(*id).unwrap().typ().clone(),
87            Expr::Instance(id, _) => problem.get(*id).unwrap().typ().clone(),
88            Expr::Variable(id, _) => problem.get(*id).unwrap().typ().clone(),
89            Expr::Parameter(p) => p.typ().clone(),
90            Expr::StrucSelf(id, _) => Type::Structure(*id),
91            Expr::StrucAttribute(_, id, _) => problem.get(*id).unwrap().typ().clone(),
92            Expr::StrucMetCall(_, id, _, _) => problem.get(*id).unwrap().typ().clone(),
93            Expr::ClassSelf(id, _) => Type::Class(*id),
94            Expr::ClassAttribute(_, id, _) => problem.get(*id).unwrap().typ().clone(),
95            Expr::ClassMetCall(_, id, _, _) => problem.get(*id).unwrap().typ().clone(),
96            Expr::AsClass(_, id) => Type::Class(*id),
97            Expr::AsInterval(_, min, max, _) => Type::Interval(*min, *max),
98            Expr::AsInt(_, _) => Type::Int,
99            Expr::AsReal(_, _) => Type::Real,
100            Expr::IfThenElse(_, t, l, e, _) => {
101                let mut res = t.typ(problem);
102                for (_, x) in l.iter() {
103                    res = res.common_type(problem, &x.typ(problem));
104                }
105                res = res.common_type(problem, &e.typ(problem));
106                res
107            }
108            Expr::Quantifier(op, _, e, _) => match op {
109                QtOp::Forall => Type::Bool,
110                QtOp::Exists => Type::Bool,
111                QtOp::Sum => match e.typ(problem) {
112                    t @ Type::Real => t,
113                    t @ Type::Int => t,
114                    Type::Interval(_, _) => Type::Int,
115                    _ => Type::Undefined,
116                },
117                QtOp::Prod => match e.typ(problem) {
118                    t @ Type::Real => t,
119                    t @ Type::Int => t,
120                    Type::Interval(_, _) => Type::Int,
121                    _ => Type::Undefined,
122                },
123                QtOp::Min => e.typ(problem),
124                QtOp::Max => e.typ(problem),
125            },
126            Expr::Unresolved(_, _) => Type::Undefined,
127            Expr::UnresolvedFunCall(_, _, _) => Type::Undefined,
128            Expr::UnresolvedAttribute(_, _, _) => Type::Undefined,
129            Expr::UnresolvedMethCall(_, _, _, _) => Type::Undefined,
130        }
131    }
132}
smt_lang/problem/expression/typ.rs

smt_lang/problem/expression/
typ.rs
