liquid_fixpoint/
parser.rs

1use std::fmt;
2
3use indexmap::IndexSet;
4use itertools::Itertools;
5
6use crate::{
7    BinOp, BinRel, Bind, Constant, Expr, Identifier, Pred, Sort, SortCtor, ThyFunc, Types,
8    constraint::BoundVar,
9    sexp::{Atom, ParseError as SexpParseError, Sexp},
10};
11
12#[derive(Debug)]
13pub enum ParseError {
14    SexpParseError(SexpParseError),
15    MalformedSexpError(String),
16}
17
18impl ParseError {
19    pub fn err(msg: impl Into<String>) -> Self {
20        ParseError::MalformedSexpError(msg.into())
21    }
22}
23
24impl Identifier for String {
25    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
26        write!(f, "{self}")
27    }
28}
29
30pub trait FromSexp<T: Types> {
31    // These are the only methods required to implement FromSexp
32    fn var(&self, name: &str) -> Result<T::Var, ParseError>;
33    fn kvar(&self, name: &str) -> Result<T::KVar, ParseError>;
34    fn string(&self, s: &str) -> Result<T::String, ParseError>;
35    fn sort(&self, name: &str) -> Result<T::Sort, ParseError>;
36    fn into_wrapper(self) -> FromSexpWrapper<T, Self>
37    where
38        Self: Sized,
39    {
40        FromSexpWrapper { parser: self, _phantom: std::marker::PhantomData, scopes: vec![] }
41    }
42}
43
44pub struct FromSexpWrapper<T: Types, Parser> {
45    pub parser: Parser,
46    pub _phantom: std::marker::PhantomData<T>,
47    scopes: Vec<IndexSet<String>>,
48}
49
50type KvarSolution<T> = (Vec<Sort<T>>, Expr<T>);
51
52impl<T, Parser: FromSexp<T>> FromSexpWrapper<T, Parser>
53where
54    T: Types,
55{
56    fn parse_bv_size(&self, sexp: &Sexp) -> Result<Sort<T>, ParseError> {
57        match sexp {
58            Sexp::Atom(Atom::S(s)) if s.starts_with("Size") => {
59                let maybe_size = s
60                    .strip_prefix("Size")
61                    .and_then(|sz_str| sz_str.parse::<u32>().ok());
62                if let Some(size) = maybe_size {
63                    Ok(Sort::BvSize(size))
64                } else {
65                    Err(ParseError::err("Could not parse number for bvsize"))
66                }
67            }
68            _ => Err(ParseError::err("Expected bitvec size to be in the form Size{\\d+}")),
69        }
70    }
71
72    pub fn parse_name(&self, sexp: &Sexp) -> Result<T::Var, ParseError> {
73        let name = match sexp {
74            Sexp::Atom(Atom::S(s)) => self.parser.var(s),
75            _ => Err(ParseError::err("Expected bind name to be a string")),
76        }?;
77        Ok(name)
78    }
79
80    pub fn parse_bind(&mut self, sexp: &Sexp) -> Result<Bind<T>, ParseError> {
81        match sexp {
82            Sexp::List(items) => {
83                match &items[0] {
84                    Sexp::List(name_and_sort) => {
85                        let name = self.parse_name(&name_and_sort[0])?;
86                        let sort = self.parse_sort(&name_and_sort[1])?;
87                        let pred = self.parse_pred_inner(&items[1])?;
88                        Ok(Bind { name, sort, pred })
89                    }
90                    _ => Err(ParseError::err("Expected list for name and sort in bind")),
91                }
92            }
93            _ => Err(ParseError::err("Expected list for bind")),
94        }
95    }
96
97    fn parse_pred_inner(&mut self, sexp: &Sexp) -> Result<Pred<T>, ParseError> {
98        match sexp {
99            Sexp::List(items) => {
100                match &items[0] {
101                    Sexp::Atom(Atom::S(s)) if s == "and" => {
102                        items[1..]
103                            .to_vec()
104                            .iter()
105                            .map(|item| self.parse_pred_inner(item))
106                            .try_collect()
107                            .map(Pred::And)
108                    }
109                    Sexp::Atom(Atom::S(s)) if s.starts_with("$") => self.parse_kvar(sexp),
110                    _ => self.parse_expr_possibly_nested(sexp).map(Pred::Expr),
111                }
112            }
113            _ => Err(ParseError::err("Expected list for pred")),
114        }
115    }
116
117    pub fn parse_kvar(&self, sexp: &Sexp) -> Result<Pred<T>, ParseError> {
118        match sexp {
119            Sexp::List(items) => {
120                if items.len() < 2 {
121                    Err(ParseError::err("Kvar application requires at least two elements"))
122                } else {
123                    let maybe_strs: Option<Vec<String>> = items
124                        .iter()
125                        .map(|s| {
126                            if let Sexp::Atom(Atom::S(sym)) = s { Some(sym.clone()) } else { None }
127                        })
128                        .collect();
129                    match maybe_strs {
130                        Some(strs) => {
131                            let kvar = self.parser.kvar(&strs[0])?;
132                            let args =
133                                strs[1..].iter().map(|s| self.parser.var(s)).try_collect()?;
134                            Ok(Pred::KVar(kvar, args))
135                        }
136                        _ => Err(ParseError::err("Expected all list elements to be strings")),
137                    }
138                }
139            }
140            _ => Err(ParseError::err("Expected list for kvar")),
141        }
142    }
143
144    fn parse_expr_possibly_nested(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError> {
145        through_nested_list(sexp, |s| self.parse_expr(s))
146    }
147
148    fn parse_is_ctor(&mut self, ctor_name: &str, arg: &Sexp) -> Result<Expr<T>, ParseError> {
149        let ctor = self.parser.var(ctor_name)?;
150        let arg = self.parse_expr(arg)?;
151        Ok(Expr::IsCtor(ctor, Box::new(arg)))
152    }
153
154    pub fn parse_expr(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError> {
155        match sexp {
156            Sexp::List(items) => {
157                if let Sexp::Atom(Atom::S(s)) = &items[0] {
158                    match s.as_str() {
159                        "exists" => self.parse_exists(&items[1..]),
160                        "let" => self.parse_let(sexp),
161                        "not" => self.parse_not(sexp),
162                        "or" => self.parse_or(sexp),
163                        "and" => self.parse_and(sexp),
164                        "lit" => parse_bitvec(sexp),
165                        "-" if items.len() == 2 => self.parse_neg(sexp),
166                        "+" | "-" | "*" | "/" | "mod" => self.parse_binary_op(sexp),
167                        "=" | "!=" | "<" | "<=" | ">" | ">=" => self.parse_atom(sexp),
168                        "<=>" => self.parse_iff(sexp),
169                        "=>" => self.parse_imp(sexp),
170                        "cast_as_int" => self.parse_expr(&items[1]), // some odd thing that fixpoint-hs seems to add for sets...
171                        _ if s.starts_with("is$") => self.parse_is_ctor(&s[3..], &items[1]),
172                        _ => self.parse_app(sexp),
173                    }
174                } else {
175                    self.parse_app(sexp)
176                }
177            }
178            Sexp::Atom(Atom::S(s)) => {
179                if let Some(thy_func) = parse_thy_func(s) {
180                    Ok(Expr::ThyFunc(thy_func))
181                } else if let Some(bv) = self.parse_bound_var(s) {
182                    Ok(bv)
183                } else {
184                    Ok(Expr::Var(self.parser.var(s)?))
185                }
186            }
187            Sexp::Atom(Atom::Q(s)) => Ok(Expr::Constant(Constant::String(self.parser.string(s)?))),
188            Sexp::Atom(Atom::B(b)) => Ok(Expr::Constant(Constant::Boolean(*b))),
189            Sexp::Atom(Atom::I(i)) => Ok(Expr::Constant(Constant::Numeral(*i as u128))),
190            Sexp::Atom(Atom::F(f)) => Ok(Expr::Constant(Constant::Real(*f as u128))),
191        }
192    }
193
194    fn parse_neg(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError> {
195        match sexp {
196            Sexp::List(items) => {
197                Ok(Expr::Neg(Box::new(self.parse_expr_possibly_nested(&items[1])?)))
198            }
199            _ => Err(ParseError::err("Expected list for neg")),
200        }
201    }
202
203    fn parse_not(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError> {
204        match sexp {
205            Sexp::List(items) => {
206                Ok(Expr::Not(Box::new(self.parse_expr_possibly_nested(&items[1])?)))
207            }
208            _ => Err(ParseError::err("Expected list for \"not\"")),
209        }
210    }
211
212    fn parse_iff(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError> {
213        match sexp {
214            Sexp::List(items) => {
215                match &items[0] {
216                    Sexp::Atom(Atom::S(s)) if s == "<=>" => {
217                        let exp1 = self.parse_expr_possibly_nested(&items[1])?;
218                        let exp2 = self.parse_expr_possibly_nested(&items[2])?;
219                        Ok(Expr::Iff(Box::new([exp1, exp2])))
220                    }
221                    _ => Err(ParseError::err("Expected iff to start with \"<=>\"")),
222                }
223            }
224            _ => Err(ParseError::err("Expected list for iff")),
225        }
226    }
227
228    fn parse_imp(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError> {
229        match sexp {
230            Sexp::List(items) => {
231                match &items[0] {
232                    Sexp::Atom(Atom::S(s)) if s == "=>" => {
233                        let exp1 = self.parse_expr_possibly_nested(&items[1])?;
234                        let exp2 = self.parse_expr_possibly_nested(&items[2])?;
235                        Ok(Expr::Imp(Box::new([exp1, exp2])))
236                    }
237                    _ => Err(ParseError::err("Expected imp to start with \"=>\"")),
238                }
239            }
240            _ => Err(ParseError::err("Expected list for implication")),
241        }
242    }
243
244    fn parse_and(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError> {
245        match sexp {
246            Sexp::List(items) => {
247                match &items[0] {
248                    Sexp::Atom(Atom::S(s)) if s == "and" => {
249                        items[1..]
250                            .to_vec()
251                            .iter()
252                            .map(|sexp| self.parse_expr_possibly_nested(sexp))
253                            .try_collect()
254                            .map(Expr::And)
255                    }
256                    _ => Err(ParseError::err("Expected \"and\" expression to start with \"and\"")),
257                }
258            }
259            _ => Err(ParseError::err("Expected list for \"and\"")),
260        }
261    }
262
263    fn parse_or(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError> {
264        match sexp {
265            Sexp::List(items) => {
266                match &items[0] {
267                    Sexp::Atom(Atom::S(s)) if s == "or" => {
268                        items[1..]
269                            .to_vec()
270                            .iter()
271                            .map(|sexp| self.parse_expr_possibly_nested(sexp))
272                            .try_collect()
273                            .map(Expr::Or)
274                    }
275                    _ => Err(ParseError::err("Expected \"or\" expression to start with \"or\"")),
276                }
277            }
278            _ => Err(ParseError::err("Expected list for \"or\"")),
279        }
280    }
281
282    fn parse_atom(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError> {
283        match sexp {
284            Sexp::List(items) => {
285                let exp1 = self.parse_expr_possibly_nested(&items[1])?;
286                let exp2 = self.parse_expr_possibly_nested(&items[2])?;
287                let exp_pair = Box::new([exp1, exp2]);
288                match &items[0] {
289                    Sexp::Atom(Atom::S(s)) if s == "=" => Ok(Expr::Atom(BinRel::Eq, exp_pair)),
290                    Sexp::Atom(Atom::S(s)) if s == "!=" => Ok(Expr::Atom(BinRel::Ne, exp_pair)),
291                    Sexp::Atom(Atom::S(s)) if s == "<=" => Ok(Expr::Atom(BinRel::Le, exp_pair)),
292                    Sexp::Atom(Atom::S(s)) if s == "<" => Ok(Expr::Atom(BinRel::Lt, exp_pair)),
293                    Sexp::Atom(Atom::S(s)) if s == ">=" => Ok(Expr::Atom(BinRel::Ge, exp_pair)),
294                    Sexp::Atom(Atom::S(s)) if s == ">" => Ok(Expr::Atom(BinRel::Gt, exp_pair)),
295                    _ => Err(ParseError::err("Unsupported atom")),
296                }
297            }
298            _ => Err(ParseError::err("Expected list for atom")),
299        }
300    }
301
302    fn parse_app(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError> {
303        match sexp {
304            Sexp::List(items) => {
305                let exp1 = self.parse_expr_possibly_nested(&items[0])?;
306                let args: Vec<Expr<T>> = items[1..]
307                    .to_vec()
308                    .iter()
309                    .map(|sexp| self.parse_expr_possibly_nested(sexp))
310                    .try_collect()?;
311                Ok(Expr::App(Box::new(exp1), args))
312            }
313            _ => Err(ParseError::err("Expected list for app")),
314        }
315    }
316
317    fn parse_binary_op(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError> {
318        match sexp {
319            Sexp::List(items) => {
320                let exp1 = self.parse_expr_possibly_nested(&items[1])?;
321                let exp2 = self.parse_expr_possibly_nested(&items[2])?;
322                let exp_pair = Box::new([exp1, exp2]);
323                match &items[0] {
324                    Sexp::Atom(Atom::S(s)) if s == "+" => Ok(Expr::BinaryOp(BinOp::Add, exp_pair)),
325                    Sexp::Atom(Atom::S(s)) if s == "-" => Ok(Expr::BinaryOp(BinOp::Sub, exp_pair)),
326                    Sexp::Atom(Atom::S(s)) if s == "*" => Ok(Expr::BinaryOp(BinOp::Mul, exp_pair)),
327                    Sexp::Atom(Atom::S(s)) if s == "/" => Ok(Expr::BinaryOp(BinOp::Div, exp_pair)),
328                    Sexp::Atom(Atom::S(s)) if s == "mod" => {
329                        Ok(Expr::BinaryOp(BinOp::Mod, exp_pair))
330                    }
331                    _ => Err(ParseError::err("Unsupported atom")),
332                }
333            }
334            _ => Err(ParseError::err("Expected list for binary operation")),
335        }
336    }
337    fn parse_exists(&mut self, items: &[Sexp]) -> Result<Expr<T>, ParseError> {
338        let [Sexp::List(var_sorts), body] = items else {
339            return Err(ParseError::err("Expected list for vars and sorts in exists"));
340        };
341        let mut names = Vec::new();
342        let mut sorts = Vec::new();
343        for var_sort in var_sorts {
344            if let Sexp::List(items) = var_sort
345                && let [var, sort] = &items[..]
346            {
347                let Sexp::Atom(Atom::S(name)) = var else {
348                    return Err(ParseError::err("Expected variable name to be string {var:?}"));
349                };
350                names.push(name.clone());
351                sorts.push(self.parse_sort(sort)?);
352            } else {
353                return Err(ParseError::err(format!(
354                    "Expected list for var and sort in exists {var_sort:?}"
355                )));
356            }
357        }
358        self.push_scope(&names);
359        let body = self.parse_expr_possibly_nested(body)?;
360        self.pop_scope();
361        Ok(Expr::Exists(sorts, Box::new(body)))
362    }
363
364    fn parse_let(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError> {
365        match sexp {
366            Sexp::List(items) => {
367                through_nested_list(&items[1], |bottom| {
368                    match bottom {
369                        Sexp::List(var_and_binding) => {
370                            match &var_and_binding[0] {
371                                Sexp::Atom(Atom::S(s)) => {
372                                    let binding =
373                                        self.parse_expr_possibly_nested(&var_and_binding[1])?;
374                                    let body = self.parse_expr_possibly_nested(&items[2])?;
375                                    let var = self.parser.var(s)?;
376                                    Ok(Expr::Let(var, Box::new([binding, body])))
377                                }
378                                _ => Err(ParseError::err("Expected variable name to be string")),
379                            }
380                        }
381                        _ => Err(ParseError::err("Expected list for var and binding")),
382                    }
383                })
384            }
385            _ => Err(ParseError::err("Expected list for let")),
386        }
387    }
388
389    fn parse_list_sort(&self, sexp: &Sexp) -> Result<Sort<T>, ParseError> {
390        let Sexp::List(items) = sexp else {
391            return Err(ParseError::err("Expected list for func or app sort"));
392        };
393        if items.is_empty() {
394            return Err(ParseError::err("Empty list encountered when parsing sort"));
395        }
396        let Sexp::Atom(Atom::S(ctor)) = &items[0] else {
397            return Err(ParseError::err("Unexpected sort constructor encountered"));
398        };
399        if ctor == "func" && items.len() == 4 {
400            return self.parse_func_sort(&items[1..]);
401        }
402        if ctor == "function" && items.len() == 3 {
403            let input = self.parse_sort(&items[1])?;
404            let output = self.parse_sort(&items[2])?;
405            return Ok(Sort::mk_func(0, vec![input], output));
406        }
407        let args: Vec<_> = items[1..]
408            .to_vec()
409            .iter()
410            .map(|sexp| self.parse_sort(sexp))
411            .try_collect()?;
412        if ctor == "Set_Set" && args.len() == 1 {
413            return Ok(Sort::App(SortCtor::Set, args));
414        }
415        if (ctor == "Map_t") && args.len() == 2 {
416            return Ok(Sort::App(SortCtor::Map, args));
417        }
418        if ctor == "BitVec" && args.len() == 1 {
419            return parse_bitvec_sort(sexp);
420        }
421        let ctor = SortCtor::Data(self.parser.sort(ctor)?);
422        Ok(Sort::App(ctor, args))
423    }
424
425    pub fn parse_sort(&self, sexp: &Sexp) -> Result<Sort<T>, ParseError> {
426        match sexp {
427            Sexp::List(_items) => self.parse_list_sort(sexp),
428            Sexp::Atom(Atom::S(s)) => {
429                if s == "Int" || s == "int" {
430                    Ok(Sort::Int)
431                } else if s == "Bool" || s == "bool" {
432                    Ok(Sort::Bool)
433                } else if s == "Real" || s == "real" {
434                    Ok(Sort::Real)
435                } else if s == "Str" || s == "str" {
436                    Ok(Sort::Str)
437                } else if s.starts_with("Size") {
438                    self.parse_bv_size(sexp)
439                } else {
440                    let ctor = SortCtor::Data(self.parser.sort(s)?);
441                    Ok(Sort::App(ctor, vec![]))
442                }
443            }
444            // Sexp::Atom(Atom::S(ref s)) => Ok(Sort::Var(s.clone())),
445            _ => panic!("Unknown sort encountered {sexp:?}"), // Err(ParseError::err(format!("Unknown sort encountered {sexp:?}"))),
446        }
447    }
448
449    fn parse_func_sort(&self, items: &[Sexp]) -> Result<Sort<T>, ParseError> {
450        if let Sexp::Atom(Atom::I(params)) = &items[0]
451            && *params >= 0
452            && let Sexp::List(inputs) = &items[1]
453        {
454            let params = *params as usize;
455            let inputs: Vec<_> = inputs
456                .iter()
457                .map(|sexp| self.parse_sort(sexp))
458                .try_collect()?;
459            let output = self.parse_sort(&items[2])?;
460            Ok(Sort::mk_func(params, inputs, output))
461        } else {
462            Err(ParseError::err("Expected arity to be an integer"))
463        }
464    }
465
466    pub fn parse_solution(&mut self, sexp: &Sexp) -> Result<KvarSolution<T>, ParseError> {
467        if let Sexp::List(items) = sexp
468            && let [_lambda, params, body] = &items[..]
469            && let Sexp::List(sexp_params) = params
470        {
471            let mut kvar_args = vec![];
472            let mut sorts = vec![];
473
474            for param in sexp_params {
475                if let Sexp::List(bind) = param
476                    && let [_name, sort] = &bind[..]
477                    && let Sexp::Atom(Atom::S(s)) = _name
478                {
479                    kvar_args.push(s.clone());
480                    sorts.push(sort);
481                } else {
482                    return Err(ParseError::err("expected parameter names to be symbols"));
483                }
484            }
485            let sorts = sorts
486                .into_iter()
487                .map(|sexp| self.parse_sort(sexp))
488                .try_collect()?;
489            self.push_scope(&kvar_args);
490
491            let expr = self.parse_expr(body)?;
492            Ok((sorts, expr))
493        } else {
494            Err(ParseError::err("expected (lambda (params) body)"))
495        }
496    }
497
498    fn push_scope(&mut self, names: &[String]) {
499        self.scopes.push(names.iter().cloned().collect());
500    }
501
502    fn pop_scope(&mut self) {
503        self.scopes.pop();
504    }
505
506    fn parse_bound_var(&self, name: &str) -> Option<Expr<T>> {
507        for (level, scope) in self.scopes.iter().rev().enumerate() {
508            if let Some(idx) = scope.get_index_of(name) {
509                return Some(Expr::BoundVar(BoundVar { level, idx }));
510            }
511        }
512        None
513    }
514}
515
516fn parse_bv_size<T: Types>(sexp: &Sexp) -> Result<Sort<T>, ParseError> {
517    match sexp {
518        Sexp::Atom(Atom::S(s)) if s.starts_with("Size") => {
519            let maybe_size = s
520                .strip_prefix("Size")
521                .and_then(|sz_str| sz_str.parse::<u32>().ok());
522            if let Some(size) = maybe_size {
523                Ok(Sort::BvSize(size))
524            } else {
525                Err(ParseError::err("Could not parse number for bvsize"))
526            }
527        }
528        _ => Err(ParseError::err("Expected bitvec size to be in the form Size{\\d+}")),
529    }
530}
531
532fn parse_bitvec_sort<T: Types>(sexp: &Sexp) -> Result<Sort<T>, ParseError> {
533    match sexp {
534        Sexp::List(items) if items.len() == 2 => {
535            let bitvec_size = parse_bv_size(&items[1])?;
536            Ok(Sort::BitVec(Box::new(bitvec_size)))
537        }
538        _ => Err(ParseError::err("Expected list of length 2 for bitvec sort")),
539    }
540}
541
542fn size_form_bv_sort(sort: Sort<StringTypes>) -> Result<u32, ParseError> {
543    match sort {
544        Sort::BitVec(ref bv_size_box) => {
545            match **bv_size_box {
546                Sort::BvSize(size) => Ok(size),
547                _ => Err(ParseError::err("BitVec sort should contain BvSize sort")),
548            }
549        }
550        _ => Err(ParseError::err("Expected BitVec variant to be provided")),
551    }
552}
553
554fn parse_bitvec<PT: Types>(sexp: &Sexp) -> Result<Expr<PT>, ParseError> {
555    match sexp {
556        Sexp::List(items) => {
557            match &items[1] {
558                Sexp::Atom(Atom::Q(lit)) if lit.starts_with("#b") => {
559                    let bitvec = u128::from_str_radix(&lit[3..], 2).expect("Invalid binary string");
560                    let bvsize = size_form_bv_sort(parse_bitvec_sort(&items[2])?)?;
561                    Ok(Expr::Constant(Constant::BitVec(bitvec, bvsize)))
562                }
563                _ => Err(ParseError::err("Expected binary literal for bitvec")),
564            }
565        }
566        _ => Err(ParseError::err("Expected list for bitvector literal")),
567    }
568}
569
570fn parse_thy_func(name: &str) -> Option<ThyFunc> {
571    match name {
572        // STRINGS
573        "strLen" => Some(ThyFunc::StrLen),
574
575        // BIT VECTORS - conversions
576        "int_to_bv8" => Some(ThyFunc::IntToBv8),
577        "bv8_to_int" => Some(ThyFunc::Bv8ToInt),
578        "int_to_bv32" => Some(ThyFunc::IntToBv32),
579        "bv32_to_int" => Some(ThyFunc::Bv32ToInt),
580        "int_to_bv64" => Some(ThyFunc::IntToBv64),
581        "bv64_to_int" => Some(ThyFunc::Bv64ToInt),
582
583        // BIT VECTORS - comparisons
584        "bvule" => Some(ThyFunc::BvUle),
585        "bvsle" => Some(ThyFunc::BvSle),
586        "bvuge" => Some(ThyFunc::BvUge),
587        "bvsge" => Some(ThyFunc::BvSge),
588        "bvugt" => Some(ThyFunc::BvUgt),
589        "bvsgt" => Some(ThyFunc::BvSgt),
590        "bvult" => Some(ThyFunc::BvUlt),
591        "bvslt" => Some(ThyFunc::BvSlt),
592
593        // BIT VECTORS - arithmetic/logical operations
594        "bvudiv" => Some(ThyFunc::BvUdiv),
595        "bvsdiv" => Some(ThyFunc::BvSdiv),
596        "bvurem" => Some(ThyFunc::BvUrem),
597        "bvsrem" => Some(ThyFunc::BvSrem),
598        "bvlshr" => Some(ThyFunc::BvLshr),
599        "bvashr" => Some(ThyFunc::BvAshr),
600        "bvand" => Some(ThyFunc::BvAnd),
601        "bvor" => Some(ThyFunc::BvOr),
602        "bvxor" => Some(ThyFunc::BvXor),
603        "bvnot" => Some(ThyFunc::BvNot),
604        "bvadd" => Some(ThyFunc::BvAdd),
605        "bvneg" => Some(ThyFunc::BvNeg),
606        "bvsub" => Some(ThyFunc::BvSub),
607        "bvmul" => Some(ThyFunc::BvMul),
608        "bvshl" => Some(ThyFunc::BvShl),
609
610        // SETS
611        "Set_empty" => Some(ThyFunc::SetEmpty),
612        "Set_sng" => Some(ThyFunc::SetSng),
613        "Set_cup" => Some(ThyFunc::SetCup),
614        "Set_cap" => Some(ThyFunc::SetCap),
615        "Set_dif" => Some(ThyFunc::SetDif),
616        "Set_mem" => Some(ThyFunc::SetMem),
617        "Set_sub" => Some(ThyFunc::SetSub),
618
619        // MAPS
620        "Map_default" => Some(ThyFunc::MapDefault),
621        "Map_select" | "arr_select_m" => Some(ThyFunc::MapSelect),
622        "Map_store" | "arr_store_m" => Some(ThyFunc::MapStore),
623
624        // Note: BvZeroExtend and BvSignExtend have parametric forms like "app (_ zero_extend N)"
625        // These would need special parsing in the caller
626        _ => None,
627    }
628}
629
630fn through_nested_list<T, F>(sexp: &Sexp, mut at_bottom: F) -> T
631where
632    F: FnMut(&Sexp) -> T,
633{
634    let mut current = sexp;
635    while let Sexp::List(items) = current {
636        if items.len() == 1 {
637            current = &items[0];
638        } else {
639            break;
640        }
641    }
642    at_bottom(current)
643}
644
645/// Trivial implementation of Types using `String` for all associated types -----------------------------------
646pub struct StringTypes;
647impl Types for StringTypes {
648    type Sort = String;
649    type KVar = String;
650    type Var = String;
651    type Tag = String;
652    type String = String;
653}
654
655impl FromSexp<StringTypes> for StringTypes {
656    fn var(&self, name: &str) -> Result<String, ParseError> {
657        Ok(name.to_string())
658    }
659
660    fn kvar(&self, name: &str) -> Result<String, ParseError> {
661        Ok(name.to_string())
662    }
663
664    fn string(&self, s: &str) -> Result<String, ParseError> {
665        Ok(s.to_string())
666    }
667
668    fn sort(&self, name: &str) -> Result<String, ParseError> {
669        Ok(name.to_string())
670    }
671}
liquid_fixpoint/parser.rs

liquid_fixpoint/
parser.rs
