liquid_fixpoint/
constraint.rs

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

liquid_fixpoint/
constraint.rs
