liquid_fixpoint/
constraint.rs

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

liquid_fixpoint/
constraint.rs
