smt_lang/problem/expression/
substitute.rs

1use crate::problem::*;
2
3impl Expr {
4    pub fn substitute(&self, old: &Expr, expr: &Expr) -> Expr {
5        if self.is_same(old) {
6            expr.clone()
7        } else {
8            match self {
9                Expr::BoolValue(_, _) => self.clone(),
10                Expr::IntValue(_, _) => self.clone(),
11                Expr::RealValue(_, _) => self.clone(),
12                Expr::Unary(op, e, pos) => {
13                    Expr::Unary(*op, Box::new(e.substitute(old, expr)), pos.clone())
14                }
15                Expr::Binary(left, op, right, pos) => {
16                    let left = Box::new(left.substitute(old, expr));
17                    let right = Box::new(right.substitute(old, expr));
18                    Expr::Binary(left, *op, right, pos.clone())
19                }
20                Expr::Nary(op, kids, pos) => {
21                    let v = kids.iter().map(|p| p.substitute(old, expr)).collect();
22                    Expr::Nary(*op, v, pos.clone())
23                }
24                Expr::FunctionCall(id, params, pos) => {
25                    let params = params.iter().map(|p| p.substitute(old, expr)).collect();
26                    Expr::FunctionCall(*id, params, pos.clone())
27                }
28                Expr::Instance(_, _) => self.clone(),
29                Expr::Variable(_, _) => self.clone(),
30                Expr::Parameter(_) => self.clone(),
31                Expr::StrucSelf(_, _) => self.clone(),
32                Expr::StrucAttribute(e, id, pos) => {
33                    Expr::StrucAttribute(Box::new(e.substitute(old, expr)), *id, pos.clone())
34                }
35                Expr::StrucMetCall(e, id, args, pos) => {
36                    let e = e.substitute(old, expr);
37                    let args = args.iter().map(|a| a.substitute(old, expr)).collect();
38                    Expr::StrucMetCall(Box::new(e), *id, args, pos.clone())
39                }
40                Expr::ClassSelf(_, _) => self.clone(),
41                Expr::ClassAttribute(e, id, pos) => {
42                    Expr::ClassAttribute(Box::new(e.substitute(old, expr)), *id, pos.clone())
43                }
44                Expr::ClassMetCall(e, id, args, pos) => {
45                    let e = e.substitute(old, expr);
46                    let args = args.iter().map(|a| a.substitute(old, expr)).collect();
47                    Expr::ClassMetCall(Box::new(e), *id, args, pos.clone())
48                }
49                Expr::AsClass(e, id) => Expr::AsClass(Box::new(e.substitute(old, expr)), *id),
50                Expr::AsInterval(e, min, max, pos) => {
51                    Expr::AsInterval(Box::new(e.substitute(old, expr)), *min, *max, pos.clone())
52                }
53                Expr::AsInt(e, pos) => {
54                    let e = Box::new(e.substitute(old, expr));
55                    let pos = pos.clone();
56                    Expr::AsInt(e, pos)
57                }
58                Expr::AsReal(e, pos) => {
59                    let e = Box::new(e.substitute(old, expr));
60                    let pos = pos.clone();
61                    Expr::AsReal(e, pos)
62                }
63                Expr::IfThenElse(c, t, l, e, pos) => {
64                    let c = Box::new(c.substitute(old, expr));
65                    let t = Box::new(t.substitute(old, expr));
66                    let l = l
67                        .iter()
68                        .map(|(x, y)| (x.substitute(old, expr), y.substitute(old, expr)))
69                        .collect();
70                    let e = Box::new(e.substitute(old, expr));
71                    let pos = pos.clone();
72                    Expr::IfThenElse(c, t, l, e, pos)
73                }
74                Expr::Quantifier(op, p, e, pos) => {
75                    let p = p.clone();
76                    let e = Box::new(e.substitute(old, expr));
77                    let pos = pos.clone();
78                    Expr::Quantifier(*op, p, e, pos)
79                }
80                Expr::Unresolved(_, _) => self.clone(),
81                Expr::UnresolvedFunCall(_, _, _) => panic!(),
82                Expr::UnresolvedAttribute(_, _, _) => panic!(),
83                Expr::UnresolvedMethCall(_, _, _, _) => panic!(),
84            }
85        }
86    }
87
88    pub fn substitute_all(&self, all: Vec<(Expr, Expr)>) -> Expr {
89        let mut expr = self.clone();
90        for (o, e) in all.iter() {
91            expr = expr.substitute(o, e);
92        }
93        expr
94    }
95}
smt_lang/problem/expression/substitute.rs

smt_lang/problem/expression/
substitute.rs
