liquid_fixpoint/
constraint.rs

1use std::sync::LazyLock;
2
3use derive_where::derive_where;
4
5use crate::{DefaultTypes, Types};
6
7pub(crate) static DEFAULT_QUALIFIERS: LazyLock<[Qualifier<DefaultTypes>; 13]> =
8    LazyLock::new(|| {
9        // -----
10        // UNARY
11        // -----
12        // (qualif EqTrue ((v bool)) (v))
13        let eqtrue = Qualifier {
14            args: vec![("v", Sort::Bool)],
15            body: Expr::Var("v"),
16            name: String::from("EqTrue"),
17        };
18        // (qualif EqFalse ((v bool)) (!v))
19        let eqfalse = Qualifier {
20            args: vec![("v", Sort::Bool)],
21            body: Expr::Neg(Box::new(Expr::Var("v"))),
22            name: String::from("EqFalse"),
23        };
24        // (qualif EqZero ((v int)) (v == 0))
25        let eqzero = Qualifier {
26            args: vec![("v", Sort::Int)],
27            body: Expr::Atom(BinRel::Eq, Box::new([Expr::Var("v"), Expr::int(0)])),
28            name: String::from("EqZero"),
29        };
30
31        // (qualif GtZero ((v int)) (v > 0))
32        let gtzero = Qualifier {
33            args: vec![("v", Sort::Int)],
34            body: Expr::Atom(BinRel::Gt, Box::new([Expr::Var("v"), Expr::int(0)])),
35            name: String::from("GtZero"),
36        };
37
38        // (qualif GeZero ((v int)) (v >= 0))
39        let gezero = Qualifier {
40            args: vec![("v", Sort::Int)],
41            body: Expr::Atom(BinRel::Ge, Box::new([Expr::Var("v"), Expr::int(0)])),
42            name: String::from("GeZero"),
43        };
44
45        // (qualif LtZero ((v int)) (v < 0))
46        let ltzero = Qualifier {
47            args: vec![("v", Sort::Int)],
48            body: Expr::Atom(BinRel::Lt, Box::new([Expr::Var("v"), Expr::int(0)])),
49            name: String::from("LtZero"),
50        };
51
52        // (qualif LeZero ((v int)) (v <= 0))
53        let lezero = Qualifier {
54            args: vec![("v", Sort::Int)],
55            body: Expr::Atom(BinRel::Le, Box::new([Expr::Var("v"), Expr::int(0)])),
56            name: String::from("LeZero"),
57        };
58
59        // ------
60        // BINARY
61        // ------
62
63        // (qualif Eq ((a int) (b int)) (a == b))
64        let eq = Qualifier {
65            args: vec![("a", Sort::Int), ("b", Sort::Int)],
66            body: Expr::Atom(BinRel::Eq, Box::new([Expr::Var("a"), Expr::Var("b")])),
67            name: String::from("Eq"),
68        };
69
70        // (qualif Gt ((a int) (b int)) (a > b))
71        let gt = Qualifier {
72            args: vec![("a", Sort::Int), ("b", Sort::Int)],
73            body: Expr::Atom(BinRel::Gt, Box::new([Expr::Var("a"), Expr::Var("b")])),
74            name: String::from("Gt"),
75        };
76
77        // (qualif Lt ((a int) (b int)) (a < b))
78        let ge = Qualifier {
79            args: vec![("a", Sort::Int), ("b", Sort::Int)],
80            body: Expr::Atom(BinRel::Ge, Box::new([Expr::Var("a"), Expr::Var("b")])),
81            name: String::from("Ge"),
82        };
83
84        // (qualif Ge ((a int) (b int)) (a >= b))
85        let lt = Qualifier {
86            args: vec![("a", Sort::Int), ("b", Sort::Int)],
87            body: Expr::Atom(BinRel::Lt, Box::new([Expr::Var("a"), Expr::Var("b")])),
88            name: String::from("Lt"),
89        };
90
91        // (qualif Le ((a int) (b int)) (a <= b))
92        let le = Qualifier {
93            args: vec![("a", Sort::Int), ("b", Sort::Int)],
94            body: Expr::Atom(BinRel::Le, Box::new([Expr::Var("a"), Expr::Var("b")])),
95            name: String::from("Le"),
96        };
97
98        // (qualif Le1 ((a int) (b int)) (a < b - 1))
99        let le1 = Qualifier {
100            args: vec![("a", Sort::Int), ("b", Sort::Int)],
101            body: Expr::Atom(
102                BinRel::Le,
103                Box::new([
104                    Expr::Var("a"),
105                    Expr::BinaryOp(BinOp::Sub, Box::new([Expr::Var("b"), Expr::int(1)])),
106                ]),
107            ),
108            name: String::from("Le1"),
109        };
110
111        [eqtrue, eqfalse, eqzero, gtzero, gezero, ltzero, lezero, eq, gt, ge, lt, le, le1]
112    });
113
114#[derive_where(Hash)]
115pub struct Bind<T: Types> {
116    pub name: T::Var,
117    pub sort: Sort<T>,
118    pub pred: Pred<T>,
119}
120
121#[derive_where(Hash)]
122pub enum Constraint<T: Types> {
123    Pred(Pred<T>, #[derive_where(skip)] Option<T::Tag>),
124    Conj(Vec<Self>),
125    ForAll(Bind<T>, Box<Self>),
126}
127
128impl<T: Types> Constraint<T> {
129    pub const TRUE: Self = Self::Pred(Pred::TRUE, None);
130
131    pub fn foralls(bindings: Vec<Bind<T>>, c: Self) -> Self {
132        bindings
133            .into_iter()
134            .rev()
135            .fold(c, |c, bind| Constraint::ForAll(bind, Box::new(c)))
136    }
137
138    pub fn conj(mut cstrs: Vec<Self>) -> Self {
139        if cstrs.len() == 1 { cstrs.remove(0) } else { Self::Conj(cstrs) }
140    }
141
142    /// Returns true if the constraint has at least one concrete RHS ("head") predicates.
143    /// If `!c.is_concrete` then `c` is trivially satisfiable and we can avoid calling fixpoint.
144    pub fn is_concrete(&self) -> bool {
145        match self {
146            Constraint::Conj(cs) => cs.iter().any(Constraint::is_concrete),
147            Constraint::ForAll(_, c) => c.is_concrete(),
148            Constraint::Pred(p, _) => p.is_concrete() && !p.is_trivially_true(),
149        }
150    }
151}
152
153#[derive_where(Hash)]
154pub struct DataDecl<T: Types> {
155    pub name: T::Sort,
156    pub vars: usize,
157    pub ctors: Vec<DataCtor<T>>,
158}
159
160#[derive_where(Hash)]
161pub struct DataCtor<T: Types> {
162    pub name: T::Var,
163    pub fields: Vec<DataField<T>>,
164}
165
166#[derive_where(Hash)]
167pub struct DataField<T: Types> {
168    pub name: T::Var,
169    pub sort: Sort<T>,
170}
171
172#[derive_where(Hash, Clone)]
173pub enum Sort<T: Types> {
174    Int,
175    Bool,
176    Real,
177    Str,
178    BitVec(Box<Sort<T>>),
179    BvSize(u32),
180    Var(usize),
181    Func(Box<[Self; 2]>),
182    Abs(usize, Box<Self>),
183    App(SortCtor<T>, Vec<Self>),
184}
185
186impl<T: Types> Sort<T> {
187    pub fn mk_func<I>(params: usize, inputs: I, output: Sort<T>) -> Sort<T>
188    where
189        I: IntoIterator<Item = Sort<T>>,
190        I::IntoIter: DoubleEndedIterator,
191    {
192        let sort = inputs
193            .into_iter()
194            .rev()
195            .fold(output, |output, input| Sort::Func(Box::new([input, output])));
196
197        (0..params)
198            .rev()
199            .fold(sort, |sort, i| Sort::Abs(i, Box::new(sort)))
200    }
201
202    pub(crate) fn peel_out_abs(&self) -> (usize, &Sort<T>) {
203        let mut n = 0;
204        let mut curr = self;
205        while let Sort::Abs(i, sort) = curr {
206            assert_eq!(*i, n);
207            n += 1;
208            curr = sort;
209        }
210        (n, curr)
211    }
212}
213
214#[derive_where(Hash, Clone)]
215pub enum SortCtor<T: Types> {
216    Set,
217    Map,
218    Data(T::Sort),
219}
220
221#[derive_where(Hash)]
222pub enum Pred<T: Types> {
223    And(Vec<Self>),
224    KVar(T::KVar, Vec<T::Var>),
225    Expr(Expr<T>),
226}
227
228impl<T: Types> Pred<T> {
229    pub const TRUE: Self = Pred::Expr(Expr::Constant(Constant::Boolean(true)));
230
231    pub fn and(mut preds: Vec<Self>) -> Self {
232        if preds.len() == 1 { preds.remove(0) } else { Self::And(preds) }
233    }
234
235    pub fn is_trivially_true(&self) -> bool {
236        match self {
237            Pred::Expr(Expr::Constant(Constant::Boolean(true))) => true,
238            Pred::And(ps) => ps.is_empty(),
239            _ => false,
240        }
241    }
242
243    pub fn is_concrete(&self) -> bool {
244        match self {
245            Pred::And(ps) => ps.iter().any(Pred::is_concrete),
246            Pred::KVar(_, _) => false,
247            Pred::Expr(_) => true,
248        }
249    }
250}
251
252#[derive(Hash, Debug, Copy, Clone, PartialEq, Eq)]
253pub enum BinRel {
254    Eq,
255    Ne,
256    Gt,
257    Ge,
258    Lt,
259    Le,
260}
261
262impl BinRel {
263    pub const INEQUALITIES: [BinRel; 4] = [BinRel::Gt, BinRel::Ge, BinRel::Lt, BinRel::Le];
264}
265
266#[derive_where(Hash)]
267pub enum Expr<T: Types> {
268    Constant(Constant<T>),
269    Var(T::Var),
270    App(Box<Self>, Vec<Self>),
271    Neg(Box<Self>),
272    BinaryOp(BinOp, Box<[Self; 2]>),
273    IfThenElse(Box<[Self; 3]>),
274    And(Vec<Self>),
275    Or(Vec<Self>),
276    Not(Box<Self>),
277    Imp(Box<[Self; 2]>),
278    Iff(Box<[Self; 2]>),
279    Atom(BinRel, Box<[Self; 2]>),
280    Let(T::Var, Box<[Self; 2]>),
281}
282
283impl<T: Types> From<Constant<T>> for Expr<T> {
284    fn from(v: Constant<T>) -> Self {
285        Self::Constant(v)
286    }
287}
288
289impl<T: Types> Expr<T> {
290    pub const fn int(val: u128) -> Expr<T> {
291        Expr::Constant(Constant::Numeral(val))
292    }
293
294    pub fn eq(self, other: Self) -> Self {
295        Expr::Atom(BinRel::Eq, Box::new([self, other]))
296    }
297
298    pub fn and(mut exprs: Vec<Self>) -> Self {
299        if exprs.len() == 1 { exprs.remove(0) } else { Self::And(exprs) }
300    }
301}
302
303#[derive_where(Hash)]
304pub enum Constant<T: Types> {
305    Numeral(u128),
306    Decimal(T::Decimal),
307    Boolean(bool),
308    String(T::String),
309    BitVec(u128, u32),
310}
311
312#[derive_where(Hash)]
313pub struct Qualifier<T: Types> {
314    pub name: String,
315    pub args: Vec<(T::Var, Sort<T>)>,
316    pub body: Expr<T>,
317}
318
319#[derive(Clone, Copy, PartialEq, Eq, Hash)]
320pub enum BinOp {
321    Add,
322    Sub,
323    Mul,
324    Div,
325    Mod,
326}
liquid_fixpoint/constraint.rs

liquid_fixpoint/
constraint.rs
