smt_lang/problem/expression/
expr.rs

1use crate::parser::Position;
2use fraction::Fraction;
3
4use crate::problem::*;
5
6//-------------------------------------------------- Unary --------------------------------------------------
7
8#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
9pub enum UnaryOp {
10    Not,
11    Minus,
12}
13
14impl std::fmt::Display for UnaryOp {
15    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
16        match self {
17            Self::Not => write!(f, "not"),
18            Self::Minus => write!(f, "-"),
19        }
20    }
21}
22
23//-------------------------------------------------- Nary --------------------------------------------------
24
25#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
26pub enum NaryOp {
27    Min,
28    Max,
29}
30
31impl std::fmt::Display for NaryOp {
32    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
33        match self {
34            Self::Min => write!(f, "min"),
35            Self::Max => write!(f, "max"),
36        }
37    }
38}
39
40//-------------------------------------------------- Bin --------------------------------------------------
41
42#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
43pub enum BinOp {
44    Eq,
45    Ne,
46    Lt,
47    Le,
48    Ge,
49    Gt,
50    //
51    And,
52    Or,
53    Implies,
54    //
55    Add,
56    Sub,
57    Mul,
58    Div,
59}
60
61impl std::fmt::Display for BinOp {
62    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
63        match self {
64            Self::Eq => write!(f, "="),
65            Self::Ne => write!(f, "!="),
66            Self::Lt => write!(f, "<"),
67            Self::Le => write!(f, "<="),
68            Self::Ge => write!(f, ">="),
69            Self::Gt => write!(f, ">"),
70            //
71            Self::And => write!(f, "and"),
72            Self::Or => write!(f, "or"),
73            Self::Implies => write!(f, "=>"),
74            //
75            Self::Add => write!(f, "+"),
76            Self::Sub => write!(f, "-"),
77            Self::Mul => write!(f, "*"),
78            Self::Div => write!(f, "/"),
79        }
80    }
81}
82
83//-------------------------------------------------- Qt --------------------------------------------------
84
85#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
86pub enum QtOp {
87    Forall,
88    Exists,
89    Sum,
90    Prod,
91    Min,
92    Max,
93}
94
95impl std::fmt::Display for QtOp {
96    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
97        match self {
98            QtOp::Forall => write!(f, "forall"),
99            QtOp::Exists => write!(f, "exists"),
100            QtOp::Sum => write!(f, "sum"),
101            QtOp::Prod => write!(f, "prod"),
102            QtOp::Min => write!(f, "min"),
103            QtOp::Max => write!(f, "max"),
104        }
105    }
106}
107
108//-------------------------------------------------- Expr --------------------------------------------------
109
110#[derive(Clone, Debug)]
111pub enum Expr {
112    BoolValue(bool, Option<Position>),
113    IntValue(isize, Option<Position>),
114    RealValue(Fraction, Option<Position>),
115    //
116    Unary(UnaryOp, Box<Expr>, Option<Position>),
117    //
118    Binary(Box<Expr>, BinOp, Box<Expr>, Option<Position>),
119    //
120    Nary(NaryOp, Vec<Expr>, Option<Position>),
121    //
122    Variable(VariableId, Option<Position>),
123    Parameter(Parameter),
124    FunctionCall(FunctionId, Vec<Expr>, Option<Position>),
125    //
126    Instance(InstanceId, Option<Position>),
127    // Structure
128    StrucSelf(StructureId, Option<Position>),
129    StrucAttribute(Box<Expr>, AttributeId<StructureId>, Option<Position>),
130    StrucMetCall(
131        Box<Expr>,
132        MethodId<StructureId>,
133        Vec<Expr>,
134        Option<Position>,
135    ),
136    // Class
137    ClassSelf(ClassId, Option<Position>),
138    ClassAttribute(Box<Expr>, AttributeId<ClassId>, Option<Position>),
139    ClassMetCall(Box<Expr>, MethodId<ClassId>, Vec<Expr>, Option<Position>),
140    //
141    AsClass(Box<Expr>, ClassId),
142    AsInterval(Box<Expr>, isize, isize, Option<Position>),
143    AsInt(Box<Expr>, Option<Position>),
144    AsReal(Box<Expr>, Option<Position>),
145    //
146    IfThenElse(
147        Box<Expr>,
148        Box<Expr>,
149        Vec<(Expr, Expr)>,
150        Box<Expr>,
151        Option<Position>,
152    ),
153    //
154    Quantifier(QtOp, Vec<Parameter>, Box<Expr>, Option<Position>),
155    //
156    Unresolved(String, Option<Position>),
157    UnresolvedFunCall(String, Vec<Expr>, Option<Position>),
158    UnresolvedAttribute(Box<Expr>, String, Option<Position>),
159    UnresolvedMethCall(Box<Expr>, String, Vec<Expr>, Option<Position>),
160}
161
162//------------------------- To Lang -------------------------
163
164impl ToLang for Expr {
165    fn to_lang(&self, problem: &Problem) -> String {
166        match self {
167            Expr::BoolValue(value, _) => format!("{}", value),
168            Expr::IntValue(value, _) => format!("{}", value),
169            Expr::RealValue(value, _) => format!("{}", value),
170            Expr::Unary(op, kid, _) => format!("({} {})", op, kid.to_lang(problem)),
171            Expr::Binary(left, op, right, _) => format!(
172                "({} {} {})",
173                left.to_lang(problem),
174                op,
175                right.to_lang(problem)
176            ),
177            Expr::Nary(op, kids, _) => {
178                let mut s = format!("{}(", op);
179                if let Some((first, others)) = kids.split_first() {
180                    s.push_str(&first.to_lang(problem));
181                    for p in others.iter() {
182                        s.push_str(&format!(", {}", p.to_lang(problem)));
183                    }
184                }
185                s.push_str(")");
186                s
187            }
188            Expr::FunctionCall(id, params, _) => {
189                let fun = problem.get(*id).unwrap();
190                let mut s = format!("{}(", fun.name());
191                if let Some((first, others)) = params.split_first() {
192                    s.push_str(&first.to_lang(problem));
193                    for p in others.iter() {
194                        s.push_str(&format!(", {}", p.to_lang(problem)));
195                    }
196                }
197                s.push_str(")");
198                s
199            }
200            Expr::Instance(id, _) => problem.get(*id).unwrap().name().into(),
201            Expr::Variable(id, _) => problem.get(*id).unwrap().name().into(),
202            Expr::Parameter(p) => p.name().to_string(),
203            Expr::StrucSelf(_, _) => "self".to_string(),
204            Expr::StrucAttribute(e, id, _) => {
205                format!(
206                    "({}.{})",
207                    e.to_lang(problem),
208                    problem.get(*id).unwrap().name()
209                )
210            }
211            Expr::StrucMetCall(e, id, args, _) => {
212                let name = problem.get(*id).unwrap().name();
213                let mut s = format!("{}.{}(", e.to_lang(problem), name,);
214                if let Some((first, others)) = args.split_first() {
215                    s.push_str(&first.to_lang(problem));
216                    for p in others.iter() {
217                        s.push_str(&format!(", {}", p.to_lang(problem)));
218                    }
219                }
220                s.push_str(")");
221                s
222            }
223            Expr::ClassSelf(_, _) => "self".to_string(),
224            Expr::ClassAttribute(e, id, _) => {
225                format!(
226                    "({}.{})",
227                    e.to_lang(problem),
228                    problem.get(*id).unwrap().name()
229                )
230            }
231            Expr::ClassMetCall(e, id, args, _) => {
232                let name = problem.get(*id).unwrap().name();
233                let mut s = format!("{}.{}(", e.to_lang(problem), name,);
234                if let Some((first, others)) = args.split_first() {
235                    s.push_str(&first.to_lang(problem));
236                    for p in others.iter() {
237                        s.push_str(&format!(", {}", p.to_lang(problem)));
238                    }
239                }
240                s.push_str(")");
241                s
242            }
243            Expr::AsClass(e, id) => format!(
244                "({} as {})",
245                e.to_lang(problem),
246                problem.get(*id).unwrap().name()
247            ),
248            Expr::AsInterval(e, min, max, _) => {
249                format!("({} as {}..{})", e.to_lang(problem), min, max)
250            }
251            Expr::AsInt(e, _) => format!("({} as Int)", e.to_lang(problem)),
252            Expr::AsReal(e, _) => format!("({} as Real)", e.to_lang(problem)),
253            Expr::IfThenElse(c, t, l, e, _) => {
254                let mut s = format!("if {} then {}", c.to_lang(problem), t.to_lang(problem));
255                for (x, y) in l.iter() {
256                    s.push_str(&format!(
257                        " elif {} then {}",
258                        x.to_lang(problem),
259                        y.to_lang(problem)
260                    ));
261                }
262                s.push_str(&format!(" else {} end", e.to_lang(problem)));
263                s
264            }
265            Expr::Quantifier(op, p, e, _) => {
266                let mut s = format!("{} ", op);
267                if let Some((first, others)) = p.split_first() {
268                    s.push_str(&first.to_lang(problem));
269                    for x in others.iter() {
270                        s.push_str(&format!(", {}", x.to_lang(problem)));
271                    }
272                }
273                s.push_str(&format!(" | {} end", e.to_lang(problem)));
274                s
275            }
276            Expr::Unresolved(name, _) => format!("{}?", name),
277            Expr::UnresolvedFunCall(name, params, _) => {
278                let mut s = format!("{}?(", name);
279                if let Some((first, others)) = params.split_first() {
280                    s.push_str(&first.to_lang(problem));
281                    for p in others.iter() {
282                        s.push_str(&format!(", {}", p.to_lang(problem)));
283                    }
284                }
285                s.push_str(")");
286                s
287            }
288            Expr::UnresolvedAttribute(e, name, _) => format!("({}.{})?", e.to_lang(problem), name),
289            Expr::UnresolvedMethCall(e, name, args, _) => {
290                let mut s = format!("{}.{}(", e.to_lang(problem), name,);
291                if let Some((first, others)) = args.split_first() {
292                    s.push_str(&first.to_lang(problem));
293                    for p in others.iter() {
294                        s.push_str(&format!(", {}", p.to_lang(problem)));
295                    }
296                }
297                s.push_str(")");
298                s
299            }
300        }
301    }
302}
smt_lang/problem/expression/expr.rs

smt_lang/problem/expression/
expr.rs
