liquid_fixpoint/
constraint.rs

1use std::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    pub fn is_concrete(&self) -> bool {
38        match self {
39            Constraint::Conj(cs) => cs.iter().any(Constraint::is_concrete),
40            Constraint::ForAll(_, c) => c.is_concrete(),
41            Constraint::Pred(p, _) => p.is_concrete() && !p.is_trivially_true(),
42        }
43    }
44}
45
46#[derive_where(Hash, Clone)]
47pub struct DataDecl<T: Types> {
48    pub name: T::Sort,
49    pub vars: usize,
50    pub ctors: Vec<DataCtor<T>>,
51}
52
53#[derive_where(Hash, Clone)]
54pub struct DataCtor<T: Types> {
55    pub name: T::Var,
56    pub fields: Vec<DataField<T>>,
57}
58
59#[derive_where(Hash, Clone)]
60pub struct DataField<T: Types> {
61    pub name: T::Var,
62    pub sort: Sort<T>,
63}
64
65#[derive_where(Hash, Clone, Debug)]
66pub enum Sort<T: Types> {
67    Int,
68    Bool,
69    Real,
70    Str,
71    BitVec(Box<Sort<T>>),
72    BvSize(u32),
73    Var(usize),
74    Func(Box<[Self; 2]>),
75    Abs(usize, Box<Self>),
76    App(SortCtor<T>, Vec<Self>),
77}
78
79impl<T: Types> Sort<T> {
80    pub fn mk_func<I>(params: usize, inputs: I, output: Sort<T>) -> Sort<T>
81    where
82        I: IntoIterator<Item = Sort<T>>,
83        I::IntoIter: DoubleEndedIterator,
84    {
85        let sort = inputs
86            .into_iter()
87            .rev()
88            .fold(output, |output, input| Sort::Func(Box::new([input, output])));
89
90        (0..params)
91            .rev()
92            .fold(sort, |sort, i| Sort::Abs(i, Box::new(sort)))
93    }
94
95    pub(crate) fn peel_out_abs(&self) -> (usize, &Sort<T>) {
96        let mut n = 0;
97        let mut curr = self;
98        while let Sort::Abs(i, sort) = curr {
99            assert_eq!(*i, n);
100            n += 1;
101            curr = sort;
102        }
103        (n, curr)
104    }
105}
106
107#[derive_where(Hash, Clone, Debug)]
108pub enum SortCtor<T: Types> {
109    Set,
110    Map,
111    Data(T::Sort),
112}
113
114#[derive_where(Hash, Clone, Debug)]
115pub enum Pred<T: Types> {
116    And(Vec<Self>),
117    KVar(T::KVar, Vec<T::Var>),
118    Expr(Expr<T>),
119}
120
121impl<T: Types> Pred<T> {
122    pub const TRUE: Self = Pred::Expr(Expr::Constant(Constant::Boolean(true)));
123
124    pub fn and(mut preds: Vec<Self>) -> Self {
125        if preds.len() == 0 {
126            Pred::TRUE
127        } else if preds.len() == 1 {
128            preds.remove(0)
129        } else {
130            Self::And(preds)
131        }
132    }
133
134    pub fn is_trivially_true(&self) -> bool {
135        match self {
136            Pred::Expr(Expr::Constant(Constant::Boolean(true))) => true,
137            Pred::And(ps) => ps.is_empty(),
138            _ => false,
139        }
140    }
141
142    pub fn is_concrete(&self) -> bool {
143        match self {
144            Pred::And(ps) => ps.iter().any(Pred::is_concrete),
145            Pred::KVar(_, _) => false,
146            Pred::Expr(_) => true,
147        }
148    }
149
150    #[cfg(feature = "rust-fixpoint")]
151    pub(crate) fn simplify(&mut self) {
152        if let Pred::And(conjuncts) = self {
153            if conjuncts.is_empty() {
154                *self = Pred::TRUE;
155            } else if conjuncts.len() == 1 {
156                *self = conjuncts[0].clone();
157            } else {
158                conjuncts.iter_mut().for_each(|pred| pred.simplify());
159            }
160        }
161    }
162}
163
164#[derive(Hash, Debug, Copy, Clone, PartialEq, Eq)]
165pub enum BinRel {
166    Eq,
167    Ne,
168    Gt,
169    Ge,
170    Lt,
171    Le,
172}
173
174impl BinRel {
175    pub const INEQUALITIES: [BinRel; 4] = [BinRel::Gt, BinRel::Ge, BinRel::Lt, BinRel::Le];
176}
177
178#[derive_where(Hash, Clone, Debug)]
179pub enum Expr<T: Types> {
180    Constant(Constant<T>),
181    Var(T::Var),
182    App(Box<Self>, Vec<Self>),
183    Neg(Box<Self>),
184    BinaryOp(BinOp, Box<[Self; 2]>),
185    IfThenElse(Box<[Self; 3]>),
186    And(Vec<Self>),
187    Or(Vec<Self>),
188    Not(Box<Self>),
189    Imp(Box<[Self; 2]>),
190    Iff(Box<[Self; 2]>),
191    Atom(BinRel, Box<[Self; 2]>),
192    Let(T::Var, Box<[Self; 2]>),
193    ThyFunc(ThyFunc),
194    IsCtor(T::Var, Box<Self>),
195}
196
197impl<T: Types> From<Constant<T>> for Expr<T> {
198    fn from(v: Constant<T>) -> Self {
199        Self::Constant(v)
200    }
201}
202
203impl<T: Types> Expr<T> {
204    pub const fn int(val: u128) -> Expr<T> {
205        Expr::Constant(Constant::Numeral(val))
206    }
207
208    pub fn eq(self, other: Self) -> Self {
209        Expr::Atom(BinRel::Eq, Box::new([self, other]))
210    }
211
212    pub fn and(mut exprs: Vec<Self>) -> Self {
213        if exprs.len() == 1 { exprs.remove(0) } else { Self::And(exprs) }
214    }
215}
216
217#[derive_where(Hash, Clone, Debug)]
218pub enum Constant<T: Types> {
219    Numeral(u128),
220    // Currently we only support parsing integers as decimals. We should extend this to allow
221    // rational numbers as a numer/denom.
222    Real(u128),
223    Boolean(bool),
224    String(T::String),
225    BitVec(u128, u32),
226}
227
228#[derive_where(Debug, Clone, Hash)]
229pub struct Qualifier<T: Types> {
230    pub name: String,
231    pub args: Vec<(T::Var, Sort<T>)>,
232    pub body: Expr<T>,
233}
234
235#[derive(Clone, Copy, PartialEq, Eq, Hash)]
236pub enum BinOp {
237    Add,
238    Sub,
239    Mul,
240    Div,
241    Mod,
242}
liquid_fixpoint/constraint.rs

liquid_fixpoint/
constraint.rs
