liquid_fixpoint/
constraint.rs

1use std::{collections::HashSet, hash::Hash};
2
3use derive_where::derive_where;
4use itertools::Itertools;
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    /// Returns true if the constraint has at least one concrete RHS ("head") predicates.
37    /// If `!c.is_concrete` then `c` is trivially satisfiable and we can avoid calling fixpoint.
38    /// Returns the number of concrete, non-trivial head predicates in the constraint.
39    pub fn concrete_head_count(&self) -> usize {
40        fn go<T: Types>(c: &Constraint<T>, count: &mut usize) {
41            match c {
42                Constraint::Conj(cs) => cs.iter().for_each(|c| go(c, count)),
43                Constraint::ForAll(_, c) => go(c, count),
44                Constraint::Pred(p, _) => {
45                    if p.is_concrete() && !p.is_trivially_true() {
46                        *count += 1;
47                    }
48                }
49            }
50        }
51        let mut count = 0;
52        go(self, &mut count);
53        count
54    }
55}
56
57#[derive_where(Hash, Clone)]
58pub struct DataDecl<T: Types> {
59    pub name: T::Sort,
60    pub vars: usize,
61    pub ctors: Vec<DataCtor<T>>,
62}
63
64#[derive_where(Hash, Clone)]
65pub struct SortDecl<T: Types> {
66    pub name: T::Sort,
67    pub vars: usize,
68}
69
70#[derive_where(Hash, Clone)]
71pub struct DataCtor<T: Types> {
72    pub name: T::Var,
73    pub fields: Vec<DataField<T>>,
74}
75
76#[derive_where(Hash, Clone)]
77pub struct DataField<T: Types> {
78    pub name: T::Var,
79    pub sort: Sort<T>,
80}
81
82#[derive_where(Hash, Clone, Debug)]
83pub enum Sort<T: Types> {
84    Int,
85    Bool,
86    Real,
87    Str,
88    BitVec(Box<Sort<T>>),
89    BvSize(u32),
90    Var(usize),
91    Func(Box<[Self; 2]>),
92    Abs(usize, Box<Self>),
93    App(SortCtor<T>, Vec<Self>),
94}
95
96impl<T: Types> Sort<T> {
97    pub fn mk_func<I>(params: usize, inputs: I, output: Sort<T>) -> Sort<T>
98    where
99        I: IntoIterator<Item = Sort<T>>,
100        I::IntoIter: DoubleEndedIterator,
101    {
102        let sort = inputs
103            .into_iter()
104            .rev()
105            .fold(output, |output, input| Sort::Func(Box::new([input, output])));
106
107        (0..params)
108            .rev()
109            .fold(sort, |sort, i| Sort::Abs(i, Box::new(sort)))
110    }
111
112    pub(crate) fn peel_out_abs(&self) -> (usize, &Sort<T>) {
113        let mut n = 0;
114        let mut curr = self;
115        while let Sort::Abs(i, sort) = curr {
116            assert_eq!(*i, n);
117            n += 1;
118            curr = sort;
119        }
120        (n, curr)
121    }
122}
123
124#[derive_where(Hash, Clone, Debug)]
125pub enum SortCtor<T: Types> {
126    Set,
127    Map,
128    Data(T::Sort),
129}
130
131#[derive_where(Hash, Clone, Debug)]
132pub enum Pred<T: Types> {
133    And(Vec<Self>),
134    KVar(T::KVar, Vec<T::Var>),
135    Expr(Expr<T>),
136}
137
138impl<T: Types> Pred<T> {
139    pub const TRUE: Self = Pred::Expr(Expr::Constant(Constant::Boolean(true)));
140
141    pub fn and(mut preds: Vec<Self>) -> Self {
142        if preds.is_empty() {
143            Pred::TRUE
144        } else if preds.len() == 1 {
145            preds.remove(0)
146        } else {
147            Self::And(preds)
148        }
149    }
150
151    pub fn is_trivially_true(&self) -> bool {
152        match self {
153            Pred::Expr(Expr::Constant(Constant::Boolean(true))) => true,
154            Pred::And(ps) => ps.is_empty(),
155            _ => false,
156        }
157    }
158
159    pub fn is_concrete(&self) -> bool {
160        match self {
161            Pred::And(ps) => ps.iter().any(Pred::is_concrete),
162            Pred::KVar(_, _) => false,
163            Pred::Expr(_) => true,
164        }
165    }
166
167    #[cfg(feature = "rust-fixpoint")]
168    pub(crate) fn simplify(&mut self) {
169        if let Pred::And(conjuncts) = self {
170            if conjuncts.is_empty() {
171                *self = Pred::TRUE;
172            } else if conjuncts.len() == 1 {
173                *self = conjuncts[0].clone();
174            } else {
175                conjuncts.iter_mut().for_each(|pred| pred.simplify());
176            }
177        }
178    }
179}
180
181#[derive(Hash, Debug, Copy, Clone, PartialEq, Eq)]
182pub enum BinRel {
183    Eq,
184    Ne,
185    Gt,
186    Ge,
187    Lt,
188    Le,
189}
190
191impl BinRel {
192    pub const INEQUALITIES: [BinRel; 4] = [BinRel::Gt, BinRel::Ge, BinRel::Lt, BinRel::Le];
193}
194
195#[derive(Hash, Debug, Copy, Clone, PartialEq, Eq)]
196pub struct BoundVar {
197    pub level: usize,
198    pub idx: usize,
199}
200
201impl BoundVar {
202    pub fn new(level: usize, idx: usize) -> Self {
203        Self { level, idx }
204    }
205}
206
207#[derive_where(Hash, Clone, Debug)]
208pub enum Expr<T: Types> {
209    Constant(Constant<T>),
210    Var(T::Var),
211    // This is kept separate from [`T::Var`] because we need to always support
212    // having bound variables for [`Expr::Exists`]. We reuse these as well
213    // for kvar solutions, which is a bit of a hack.
214    BoundVar(BoundVar),
215    App(Box<Self>, Vec<Self>),
216    Neg(Box<Self>),
217    BinaryOp(BinOp, Box<[Self; 2]>),
218    IfThenElse(Box<[Self; 3]>),
219    And(Vec<Self>),
220    Or(Vec<Self>),
221    Not(Box<Self>),
222    Imp(Box<[Self; 2]>),
223    Iff(Box<[Self; 2]>),
224    Atom(BinRel, Box<[Self; 2]>),
225    Let(T::Var, Box<[Self; 2]>),
226    ThyFunc(ThyFunc),
227    IsCtor(T::Var, Box<Self>),
228    Exists(Vec<Sort<T>>, Box<Self>),
229}
230
231impl<T: Types> From<Constant<T>> for Expr<T> {
232    fn from(v: Constant<T>) -> Self {
233        Self::Constant(v)
234    }
235}
236
237impl<T: Types> Expr<T> {
238    pub const fn int(val: u128) -> Expr<T> {
239        Expr::Constant(Constant::Numeral(val))
240    }
241
242    pub fn eq(self, other: Self) -> Self {
243        Expr::Atom(BinRel::Eq, Box::new([self, other]))
244    }
245
246    pub fn and(mut exprs: Vec<Self>) -> Self {
247        if exprs.len() == 1 { exprs.remove(0) } else { Self::And(exprs) }
248    }
249
250    pub fn free_vars(&self) -> HashSet<T::Var> {
251        let mut vars = HashSet::new();
252        match self {
253            Expr::Constant(_) | Expr::ThyFunc(_) | Expr::BoundVar { .. } => {}
254            Expr::Var(x) => {
255                vars.insert(x.clone());
256            }
257            Expr::App(func, args) => {
258                vars.extend(func.free_vars());
259                for arg in args {
260                    vars.extend(arg.free_vars());
261                }
262            }
263            Expr::Neg(e) | Expr::Not(e) => {
264                vars = e.free_vars();
265            }
266            Expr::BinaryOp(_, exprs)
267            | Expr::Imp(exprs)
268            | Expr::Iff(exprs)
269            | Expr::Atom(_, exprs) => {
270                let [e1, e2] = &**exprs;
271                vars.extend(e1.free_vars());
272                vars.extend(e2.free_vars());
273            }
274            Expr::IfThenElse(exprs) => {
275                let [p, e1, e2] = &**exprs;
276                vars.extend(p.free_vars());
277                vars.extend(e1.free_vars());
278                vars.extend(e2.free_vars());
279            }
280            Expr::And(exprs) | Expr::Or(exprs) => {
281                for e in exprs {
282                    vars.extend(e.free_vars());
283                }
284            }
285            Expr::Let(name, exprs) => {
286                // Fixpoint only support one binder per let expressions, but it parses a singleton
287                // list of binders to be forward-compatible
288                let [var_e, body_e] = &**exprs;
289                vars.extend(var_e.free_vars());
290                let mut body_vars = body_e.free_vars();
291                body_vars.remove(name);
292                vars.extend(body_vars);
293            }
294            Expr::IsCtor(_v, expr) => {
295                // NOTE: (ck) I'm pretty sure this isn't a binder so I'm not going to
296                // bother with `v`.
297                vars.extend(expr.free_vars());
298            }
299            Expr::Exists(_sorts, expr) => {
300                // NOTE: (ck) No variable names here so it seems this is nameless.
301                vars.extend(expr.free_vars());
302            }
303        };
304        vars
305    }
306
307    pub fn substitute_bvar(&self, subst_layer: &[Expr<T>], current_level: usize) -> Self {
308        match self {
309            Expr::Constant(_) | Expr::Var(_) | Expr::ThyFunc(_) => self.clone(),
310            Expr::BoundVar(bound_var) => {
311                if bound_var.level == current_level
312                    && let Some(subst) = subst_layer.get(bound_var.idx)
313                {
314                    subst.clone()
315                } else {
316                    self.clone()
317                }
318            }
319            Expr::App(expr, exprs) => {
320                Expr::App(
321                    Box::new(expr.substitute_bvar(subst_layer, current_level)),
322                    exprs
323                        .iter()
324                        .map(|e| e.substitute_bvar(subst_layer, current_level))
325                        .collect_vec(),
326                )
327            }
328            Expr::Neg(expr) => {
329                Expr::Neg(Box::new(expr.substitute_bvar(subst_layer, current_level)))
330            }
331            Expr::BinaryOp(bin_op, args) => {
332                Expr::BinaryOp(
333                    *bin_op,
334                    Box::new([
335                        args[0].substitute_bvar(subst_layer, current_level),
336                        args[1].substitute_bvar(subst_layer, current_level),
337                    ]),
338                )
339            }
340            Expr::IfThenElse(args) => {
341                Expr::IfThenElse(Box::new([
342                    args[0].substitute_bvar(subst_layer, current_level),
343                    args[1].substitute_bvar(subst_layer, current_level),
344                    args[2].substitute_bvar(subst_layer, current_level),
345                ]))
346            }
347            Expr::And(exprs) => {
348                Expr::And(
349                    exprs
350                        .iter()
351                        .map(|e| e.substitute_bvar(subst_layer, current_level))
352                        .collect_vec(),
353                )
354            }
355            Expr::Or(exprs) => {
356                Expr::Or(
357                    exprs
358                        .iter()
359                        .map(|e| e.substitute_bvar(subst_layer, current_level))
360                        .collect_vec(),
361                )
362            }
363            Expr::Not(expr) => {
364                Expr::Not(Box::new(expr.substitute_bvar(subst_layer, current_level)))
365            }
366            Expr::Imp(args) => {
367                Expr::Imp(Box::new([
368                    args[0].substitute_bvar(subst_layer, current_level),
369                    args[1].substitute_bvar(subst_layer, current_level),
370                ]))
371            }
372            Expr::Iff(args) => {
373                Expr::Iff(Box::new([
374                    args[0].substitute_bvar(subst_layer, current_level),
375                    args[1].substitute_bvar(subst_layer, current_level),
376                ]))
377            }
378            Expr::Atom(bin_rel, args) => {
379                Expr::Atom(
380                    *bin_rel,
381                    Box::new([
382                        args[0].substitute_bvar(subst_layer, current_level),
383                        args[1].substitute_bvar(subst_layer, current_level),
384                    ]),
385                )
386            }
387            Expr::Let(var, args) => {
388                Expr::Let(
389                    var.clone(),
390                    Box::new([
391                        args[0].substitute_bvar(subst_layer, current_level),
392                        args[1].substitute_bvar(subst_layer, current_level),
393                    ]),
394                )
395            }
396            Expr::IsCtor(var, expr) => {
397                Expr::IsCtor(
398                    var.clone(),
399                    Box::new(expr.substitute_bvar(subst_layer, current_level)),
400                )
401            }
402            Expr::Exists(sorts, expr) => {
403                Expr::Exists(
404                    sorts.clone(),
405                    Box::new(expr.substitute_bvar(subst_layer, current_level + 1)),
406                )
407            }
408        }
409    }
410}
411
412#[derive_where(Hash, Clone, Debug)]
413pub enum Constant<T: Types> {
414    Numeral(u128),
415    // Currently we only support parsing integers as decimals. We should extend this to allow
416    // rational numbers as a numer/denom.
417    Real(u128),
418    Boolean(bool),
419    String(T::String),
420    BitVec(u128, u32),
421}
422
423#[derive_where(Debug, Clone, Hash)]
424pub struct Qualifier<T: Types> {
425    pub name: String,
426    pub args: Vec<(T::Var, Sort<T>)>,
427    pub body: Expr<T>,
428}
429
430#[derive(Clone, Copy, PartialEq, Eq, Hash)]
431pub enum BinOp {
432    Add,
433    Sub,
434    Mul,
435    Div,
436    Mod,
437}
liquid_fixpoint/constraint.rs

liquid_fixpoint/
constraint.rs
