liquid_fixpoint/
constraint.rs

1use std::{collections::HashSet, hash::Hash};
2
3use derive_where::derive_where;
4use indexmap::{IndexMap, IndexSet};
5
6use crate::{ThyFunc, Types};
7
8#[derive_where(Hash, Clone, Debug)]
9pub struct Bind<T: Types> {
10    pub name: T::Var,
11    pub sort: Sort<T>,
12    pub pred: Pred<T>,
13}
14
15#[derive_where(Hash, Clone, Debug)]
16pub enum Constraint<T: Types> {
17    Pred(Pred<T>, #[derive_where(skip)] Option<T::Tag>),
18    Conj(Vec<Self>),
19    ForAll(Bind<T>, Box<Self>),
20}
21
22impl<T: Types> Constraint<T> {
23    pub const TRUE: Self = Self::Pred(Pred::TRUE, None);
24
25    pub fn foralls(bindings: Vec<Bind<T>>, c: Self) -> Self {
26        bindings
27            .into_iter()
28            .rev()
29            .fold(c, |c, bind| Constraint::ForAll(bind, Box::new(c)))
30    }
31
32    pub fn conj(mut cstrs: Vec<Self>) -> Self {
33        if cstrs.len() == 1 { cstrs.remove(0) } else { Self::Conj(cstrs) }
34    }
35
36    fn variable_sorts_help(&self, acc: &mut IndexMap<T::Var, Sort<T>>) {
37        match self {
38            Constraint::ForAll(bind, inner) => {
39                acc.insert(bind.name.clone(), bind.sort.clone());
40                inner.variable_sorts_help(acc);
41            }
42            Constraint::Conj(cstrs) => {
43                cstrs.iter().for_each(|cstr| cstr.variable_sorts_help(acc));
44            }
45            Constraint::Pred(..) => {}
46        }
47    }
48
49    pub fn variable_sorts(&self) -> IndexMap<T::Var, Sort<T>> {
50        let mut res = IndexMap::new();
51        self.variable_sorts_help(&mut res);
52        res
53    }
54
55    /// Returns true if the constraint has at least one concrete RHS ("head") predicates.
56    /// If `!c.is_concrete` then `c` is trivially satisfiable and we can avoid calling fixpoint.
57    /// Returns the number of concrete, non-trivial head predicates in the constraint.
58    pub fn concrete_head_count(&self) -> usize {
59        fn go<T: Types>(c: &Constraint<T>, count: &mut usize) {
60            match c {
61                Constraint::Conj(cs) => cs.iter().for_each(|c| go(c, count)),
62                Constraint::ForAll(_, c) => go(c, count),
63                Constraint::Pred(p, _) => {
64                    if p.is_concrete() && !p.is_trivially_true() {
65                        *count += 1;
66                    }
67                }
68            }
69        }
70        let mut count = 0;
71        go(self, &mut count);
72        count
73    }
74}
75
76#[derive_where(Hash, Clone, Debug)]
77pub struct DataDecl<T: Types> {
78    pub name: T::Sort,
79    pub vars: usize,
80    pub ctors: Vec<DataCtor<T>>,
81}
82
83impl<T: Types> DataDecl<T> {
84    pub fn deps(&self, acc: &mut Vec<T::Sort>) {
85        for ctor in &self.ctors {
86            for field in &ctor.fields {
87                field.sort.deps(acc);
88            }
89        }
90    }
91}
92
93#[derive_where(Hash, Clone, Debug)]
94pub struct SortDecl<T: Types> {
95    pub name: T::Sort,
96    pub vars: usize,
97}
98
99#[derive_where(Hash, Clone, Debug)]
100pub struct DataCtor<T: Types> {
101    pub name: T::Var,
102    pub fields: Vec<DataField<T>>,
103}
104
105#[derive_where(Hash, Clone, Debug)]
106pub struct DataField<T: Types> {
107    pub name: T::Var,
108    pub sort: Sort<T>,
109}
110
111#[derive_where(Hash, Clone, Debug)]
112pub enum Sort<T: Types> {
113    Int,
114    Bool,
115    Real,
116    Str,
117    BitVec(Box<Sort<T>>),
118    BvSize(u32),
119    Var(usize),
120    Func(Box<[Self; 2]>),
121    Abs(usize, Box<Self>),
122    App(SortCtor<T>, Vec<Self>),
123}
124
125impl<T: Types> Sort<T> {
126    pub fn deps(&self, acc: &mut Vec<T::Sort>) {
127        match self {
128            Sort::App(SortCtor::Data(dt_name), args) => {
129                acc.push(dt_name.clone());
130                for arg in args {
131                    arg.deps(acc);
132                }
133            }
134            Sort::Func(input_and_output) => {
135                let [input, output] = &**input_and_output;
136                input.deps(acc);
137                output.deps(acc);
138            }
139            Sort::Abs(_, sort) => {
140                sort.deps(acc);
141            }
142            _ => {}
143        }
144    }
145
146    pub fn mk_func<I>(params: usize, inputs: I, output: Sort<T>) -> Sort<T>
147    where
148        I: IntoIterator<Item = Sort<T>>,
149        I::IntoIter: DoubleEndedIterator,
150    {
151        let sort = inputs
152            .into_iter()
153            .rev()
154            .fold(output, |output, input| Sort::Func(Box::new([input, output])));
155
156        (0..params)
157            .rev()
158            .fold(sort, |sort, i| Sort::Abs(i, Box::new(sort)))
159    }
160
161    pub(crate) fn peel_out_abs(&self) -> (usize, &Sort<T>) {
162        let mut n = 0;
163        let mut curr = self;
164        while let Sort::Abs(i, sort) = curr {
165            assert_eq!(*i, n);
166            n += 1;
167            curr = sort;
168        }
169        (n, curr)
170    }
171
172    fn free_var_sorts_to_int_help(&mut self, bound: &mut HashSet<usize>) {
173        match self {
174            Sort::Int
175            | Sort::Real
176            | Sort::Bool
177            | Sort::Str
178            | Sort::BvSize(..)
179            | Sort::BitVec(..) => {}
180            Sort::Abs(var, inner) => {
181                bound.insert(*var);
182                inner.free_var_sorts_to_int_help(bound);
183                bound.remove(var);
184            }
185            Sort::App(_, args) => {
186                for arg in args {
187                    arg.free_var_sorts_to_int_help(bound);
188                }
189            }
190            Sort::Func(inner) => {
191                let [arg, out] = &mut **inner;
192                arg.free_var_sorts_to_int_help(bound);
193                out.free_var_sorts_to_int_help(bound);
194            }
195            Sort::Var(v) => {
196                if !bound.contains(v) {
197                    *self = Sort::Int;
198                }
199            }
200        }
201    }
202
203    pub(crate) fn free_var_sorts_to_int(&mut self) {
204        let mut bound = HashSet::new();
205        self.free_var_sorts_to_int_help(&mut bound);
206    }
207}
208
209#[derive_where(Hash, Debug)]
210pub struct FunSort<T: Types> {
211    pub params: usize,
212    pub inputs: Vec<Sort<T>>,
213    pub output: Sort<T>,
214}
215
216impl<T: Types> FunSort<T> {
217    pub fn deps(&self, acc: &mut Vec<T::Sort>) {
218        for sort in &self.inputs {
219            sort.deps(acc);
220        }
221        self.output.deps(acc);
222    }
223
224    pub fn into_sort(self) -> Sort<T> {
225        Sort::mk_func(self.params, self.inputs, self.output)
226    }
227}
228
229#[derive_where(Hash, Clone, Debug)]
230pub enum SortCtor<T: Types> {
231    Set,
232    Map,
233    Data(T::Sort),
234}
235
236#[derive_where(Hash, Clone, Debug)]
237pub enum Pred<T: Types> {
238    And(Vec<Self>),
239    KVar(T::KVar, Vec<Expr<T>>),
240    Expr(Expr<T>),
241}
242
243impl<T: Types> Pred<T> {
244    pub const TRUE: Self = Pred::Expr(Expr::Constant(Constant::Boolean(true)));
245
246    pub fn and(mut preds: Vec<Self>) -> Self {
247        if preds.is_empty() {
248            Pred::TRUE
249        } else if preds.len() == 1 {
250            preds.remove(0)
251        } else {
252            Self::And(preds)
253        }
254    }
255
256    pub fn is_trivially_true(&self) -> bool {
257        match self {
258            Pred::Expr(Expr::Constant(Constant::Boolean(true))) => true,
259            Pred::And(ps) => ps.is_empty(),
260            _ => false,
261        }
262    }
263
264    pub fn is_concrete(&self) -> bool {
265        match self {
266            Pred::And(ps) => ps.iter().any(Pred::is_concrete),
267            Pred::KVar(_, _) => false,
268            Pred::Expr(_) => true,
269        }
270    }
271
272    #[cfg(feature = "rust-fixpoint")]
273    pub(crate) fn simplify(&mut self) {
274        if let Pred::And(conjuncts) = self {
275            if conjuncts.is_empty() {
276                *self = Pred::TRUE;
277            } else if conjuncts.len() == 1 {
278                *self = conjuncts[0].clone();
279            } else {
280                conjuncts.iter_mut().for_each(|pred| pred.simplify());
281            }
282        }
283    }
284}
285
286#[derive(Hash, Debug, Copy, Clone, PartialEq, Eq)]
287pub enum BinRel {
288    Eq,
289    Ne,
290    Gt,
291    Ge,
292    Lt,
293    Le,
294}
295
296impl BinRel {
297    pub const INEQUALITIES: [BinRel; 4] = [BinRel::Gt, BinRel::Ge, BinRel::Lt, BinRel::Le];
298}
299
300#[derive(Hash, Debug, Copy, Clone, PartialEq, Eq)]
301pub struct BoundVar {
302    pub level: usize,
303    pub idx: usize,
304}
305
306impl BoundVar {
307    pub fn new(level: usize, idx: usize) -> Self {
308        Self { level, idx }
309    }
310}
311
312#[derive_where(Hash, Clone, Debug)]
313pub enum Expr<T: Types> {
314    Constant(Constant<T>),
315    Var(T::Var),
316    App(Box<Self>, Option<Vec<Sort<T>>>, Vec<Self>, Option<Sort<T>>),
317    Neg(Box<Self>),
318    BinaryOp(BinOp, Box<[Self; 2]>),
319    IfThenElse(Box<[Self; 3]>),
320    And(Vec<Self>),
321    Or(Vec<Self>),
322    Not(Box<Self>),
323    Imp(Box<[Self; 2]>),
324    Iff(Box<[Self; 2]>),
325    Atom(BinRel, Box<[Self; 2]>),
326    Let(T::Var, Box<[Self; 2]>),
327    ThyFunc(ThyFunc),
328    IsCtor(T::Var, Box<Self>),
329    Exists(Vec<(T::Var, Sort<T>)>, Box<Self>),
330}
331
332impl<T: Types> From<Constant<T>> for Expr<T> {
333    fn from(v: Constant<T>) -> Self {
334        Self::Constant(v)
335    }
336}
337
338impl<T: Types> Expr<T> {
339    pub const fn int(val: u128) -> Expr<T> {
340        Expr::Constant(Constant::Numeral(val))
341    }
342
343    pub fn eq(self, other: Self) -> Self {
344        Expr::Atom(BinRel::Eq, Box::new([self, other]))
345    }
346
347    pub fn and(mut exprs: Vec<Self>) -> Self {
348        if exprs.len() == 1 { exprs.remove(0) } else { Self::And(exprs) }
349    }
350
351    pub fn var_sorts_to_int(&mut self) {
352        match self {
353            Expr::Constant(_) | Expr::ThyFunc(_) | Expr::Var(_) => {}
354            Expr::App(func, sort_args, args, out_sort) => {
355                func.var_sorts_to_int();
356                for arg in args {
357                    arg.var_sorts_to_int();
358                }
359                if let Some(sort_args) = sort_args {
360                    for sort_arg in sort_args {
361                        sort_arg.free_var_sorts_to_int();
362                    }
363                }
364                if let Some(out_sort) = out_sort {
365                    out_sort.free_var_sorts_to_int();
366                }
367            }
368            Expr::Neg(e) | Expr::Not(e) => {
369                e.var_sorts_to_int();
370            }
371            Expr::BinaryOp(_, exprs)
372            | Expr::Imp(exprs)
373            | Expr::Iff(exprs)
374            | Expr::Atom(_, exprs) => {
375                let [e1, e2] = &mut **exprs;
376                e1.var_sorts_to_int();
377                e2.var_sorts_to_int();
378            }
379            Expr::IfThenElse(exprs) => {
380                let [p, e1, e2] = &mut **exprs;
381                p.var_sorts_to_int();
382                e1.var_sorts_to_int();
383                e2.var_sorts_to_int();
384            }
385            Expr::And(exprs) | Expr::Or(exprs) => {
386                for e in exprs {
387                    e.var_sorts_to_int();
388                }
389            }
390            Expr::Let(_, exprs) => {
391                let [var_e, body_e] = &mut **exprs;
392                var_e.var_sorts_to_int();
393                body_e.var_sorts_to_int();
394            }
395            Expr::IsCtor(_v, expr) => {
396                expr.var_sorts_to_int();
397            }
398            Expr::Exists(binder, expr) => {
399                for (_, sort) in binder {
400                    sort.free_var_sorts_to_int();
401                }
402                expr.var_sorts_to_int();
403            }
404        }
405    }
406
407    pub fn free_vars(&self) -> IndexSet<T::Var> {
408        let mut vars = IndexSet::new();
409        match self {
410            Expr::Constant(_) | Expr::ThyFunc(_) => {}
411            Expr::Var(x) => {
412                vars.insert(x.clone());
413            }
414            Expr::App(func, _sort_args, args, _out_sort) => {
415                vars.extend(func.free_vars());
416                for arg in args {
417                    vars.extend(arg.free_vars());
418                }
419            }
420            Expr::Neg(e) | Expr::Not(e) => {
421                vars = e.free_vars();
422            }
423            Expr::BinaryOp(_, exprs)
424            | Expr::Imp(exprs)
425            | Expr::Iff(exprs)
426            | Expr::Atom(_, exprs) => {
427                let [e1, e2] = &**exprs;
428                vars.extend(e1.free_vars());
429                vars.extend(e2.free_vars());
430            }
431            Expr::IfThenElse(exprs) => {
432                let [p, e1, e2] = &**exprs;
433                vars.extend(p.free_vars());
434                vars.extend(e1.free_vars());
435                vars.extend(e2.free_vars());
436            }
437            Expr::And(exprs) | Expr::Or(exprs) => {
438                for e in exprs {
439                    vars.extend(e.free_vars());
440                }
441            }
442            Expr::Let(name, exprs) => {
443                // Fixpoint only support one binder per let expressions, but it parses a singleton
444                // list of binders to be forward-compatible
445                let [var_e, body_e] = &**exprs;
446                vars.extend(var_e.free_vars());
447                let mut body_vars = body_e.free_vars();
448                body_vars.swap_remove(name);
449                vars.extend(body_vars);
450            }
451            Expr::IsCtor(_v, expr) => {
452                // NOTE: (ck) I'm pretty sure this isn't a binder so I'm not going to
453                // bother with `v`.
454                vars.extend(expr.free_vars());
455            }
456            Expr::Exists(binder, expr) => {
457                let mut inner = expr.free_vars();
458                for (var, _sort) in binder {
459                    inner.swap_remove(var);
460                }
461                vars.extend(inner);
462            }
463        };
464        vars
465    }
466}
467
468#[derive_where(Hash, Clone, Debug)]
469pub enum Constant<T: Types> {
470    Numeral(u128),
471    // Currently we only support parsing integers as decimals. We should extend this to allow
472    // rational numbers as a numer/denom.
473    //
474    // NOTE: If this type is updated, then update parse_expr in the parser
475    // (see the unimplemented!() related to float parsing).
476    Real(u128),
477    Boolean(bool),
478    String(T::String),
479    BitVec(u128, u32),
480}
481
482#[derive_where(Debug, Clone, Hash)]
483pub struct Qualifier<T: Types> {
484    pub name: String,
485    pub args: Vec<(T::Var, Sort<T>)>,
486    pub body: Expr<T>,
487}
488
489#[derive(Clone, Copy, PartialEq, Eq, Hash)]
490pub enum BinOp {
491    Add,
492    Sub,
493    Mul,
494    Div,
495    Mod,
496}
liquid_fixpoint/constraint.rs

liquid_fixpoint/
constraint.rs
