liquid_fixpoint/
constraint_with_env.rs

1#[cfg(feature = "rust-fixpoint")]
2use std::collections::HashMap;
3
4use derive_where::derive_where;
5use itertools::Itertools;
6use rustc_data_structures::fx::FxIndexMap;
7#[cfg(feature = "rust-fixpoint")]
8use {
9    crate::{
10        FixpointStatus, Identifier,
11        cstr2smt2::{Env, is_constraint_satisfiable, new_binding, new_datatype},
12    },
13    std::collections::VecDeque,
14    z3::Solver,
15};
16
17use crate::{
18    ConstDecl, DataDecl, KVarDecl, Sort, SortCtor, Types,
19    constraint::{Constraint, Qualifier},
20    graph,
21};
22
23#[derive_where(Hash)]
24pub struct ConstraintWithEnv<T: Types> {
25    datatype_decls: Vec<DataDecl<T>>,
26    kvar_decls: Vec<KVarDecl<T>>,
27    qualifiers: Vec<Qualifier<T>>,
28    constants: Vec<ConstDecl<T>>,
29    constraint: Constraint<T>,
30}
31#[cfg(feature = "rust-fixpoint")]
32use crate::Assignments;
33
34#[cfg(not(feature = "rust-fixpoint"))]
35impl<T: Types> ConstraintWithEnv<T> {
36    #[allow(unused)]
37    pub fn new(
38        datatype_decls: Vec<DataDecl<T>>,
39        kvar_decls: Vec<KVarDecl<T>>,
40        qualifiers: Vec<Qualifier<T>>,
41        constants: Vec<ConstDecl<T>>,
42        constraint: Constraint<T>,
43    ) -> Self {
44        Self { datatype_decls, kvar_decls, qualifiers, constants, constraint }
45    }
46}
47
48#[cfg(feature = "rust-fixpoint")]
49impl<T: Types> ConstraintWithEnv<T> {
50    pub fn new(
51        datatype_decls: Vec<DataDecl<T>>,
52        kvar_decls: Vec<KVarDecl<T>>,
53        qualifiers: Vec<Qualifier<T>>,
54        constants: Vec<ConstDecl<T>>,
55        constraint: Constraint<T>,
56    ) -> Self {
57        let datatype_decls = topo_sort_data_declarations(datatype_decls);
58        Self { datatype_decls, kvar_decls, qualifiers, constants, constraint }
59    }
60
61    pub fn compute_initial_assignments(&self) -> Assignments<'_, T> {
62        let mut assignments = HashMap::new();
63
64        for decl in &self.kvar_decls {
65            let kvar_arg_count = decl.sorts.len();
66            assignments.insert(decl.kvid.clone(), vec![]);
67            for qualifier in &self.qualifiers {
68                // TODO: assignments index into the kvar's arguments, so there's no way to name a
69                // literal here. Skip wildcards rather than silently treat them as ordinary params.
70                if qualifier.args.iter().any(|param| param.is_wildcard) {
71                    continue;
72                }
73                let qualifier_arg_count = qualifier.args.len();
74                for argument_combination in (0..kvar_arg_count).combinations(qualifier_arg_count) {
75                    assignments.get_mut(&decl.kvid).unwrap().extend(
76                        argument_combination
77                            .into_iter()
78                            .permutations(qualifier_arg_count)
79                            .filter(|arg_permutation| {
80                                type_signature_matches(arg_permutation, decl, qualifier)
81                            })
82                            .map(|arg_permutation| (qualifier, arg_permutation)),
83                    );
84                }
85            }
86        }
87
88        assignments
89    }
90
91    fn solve_for_kvars(&self, solver: &Solver, env: &mut Env<T>) -> Assignments<'_, T> {
92        let mut assignments = self.compute_initial_assignments();
93        let kvars_to_fragments = self.constraint.kvar_mappings();
94        let topo_order_fragments = self.constraint.topo_order_fragments();
95        let mut work_list = VecDeque::from_iter(topo_order_fragments.iter());
96        while let Some(fragment) = work_list.pop_front() {
97            if let Some(kvar_name) = fragment.fragment_kvar_head()
98                && let subbed = fragment.sub_kvars_except_head(&assignments)
99                && let Some(assignment) = assignments.get_mut(&kvar_name)
100            {
101                let initial_length = assignment.len();
102                assignment.retain(|assignment| {
103                    let vc = subbed.sub_head(assignment);
104                    is_constraint_satisfiable(&vc, solver, env).is_safe()
105                });
106                if initial_length > assignment.len() {
107                    work_list.extend(
108                        fragment
109                            .kvar_deps()
110                            .iter()
111                            .flat_map(|kvar| kvars_to_fragments.get(kvar).unwrap().iter()),
112                    );
113                }
114            }
115        }
116        assignments
117    }
118
119    pub fn is_satisfiable(&mut self) -> FixpointStatus<T::Tag> {
120        self.solve_by_fusion()
121    }
122
123    pub(crate) fn eliminate_acyclic_kvars(&mut self) {
124        let mut dep_graph = self.constraint.kvar_dep_graph();
125        let mut acyclic_kvars: Vec<T::KVar> = dep_graph
126            .into_iter()
127            .filter(|(_, dependencies)| dependencies.is_empty())
128            .map(|(kvar, _)| kvar)
129            .collect();
130        while !acyclic_kvars.is_empty() {
131            self.constraint = self.constraint.elim(&acyclic_kvars);
132            dep_graph = self.constraint.kvar_dep_graph();
133            acyclic_kvars = dep_graph
134                .into_iter()
135                .filter(|(_, dependencies)| dependencies.is_empty())
136                .map(|(kvar, _)| kvar)
137                .collect();
138        }
139    }
140
141    pub fn solve_by_fusion(&mut self) -> FixpointStatus<T::Tag> {
142        self.eliminate_acyclic_kvars();
143        self.solve_by_predicate_abstraction()
144    }
145
146    pub fn solve_by_predicate_abstraction(&mut self) -> FixpointStatus<T::Tag> {
147        let solver = Solver::new();
148        let mut vars: Env<T> = Env::new();
149        self.constants.iter().for_each(|const_decl| {
150            vars.insert(
151                const_decl.name.clone(),
152                new_binding(&const_decl.name.display().to_string(), &const_decl.sort, &vars),
153            );
154        });
155        self.datatype_decls.iter().for_each(|data_decl| {
156            let datatype_sort = new_datatype(&data_decl.name, data_decl, &mut vars);
157            vars.insert_data_decl(data_decl.name.clone(), datatype_sort);
158        });
159        let kvar_assignment = self.solve_for_kvars(&solver, &mut vars);
160        self.constraint = self.constraint.sub_all_kvars(&kvar_assignment);
161        is_constraint_satisfiable(&self.constraint, &solver, &mut vars)
162    }
163}
164
165pub fn topo_sort_data_declarations<T: Types>(datatype_decls: Vec<DataDecl<T>>) -> Vec<DataDecl<T>> {
166    let mut datatype_dependencies: FxIndexMap<T::Sort, Vec<T::Sort>> = FxIndexMap::default();
167    for datatype_decl in &datatype_decls {
168        datatype_dependencies.insert(datatype_decl.name.clone(), vec![]);
169    }
170    let mut data_decls_by_name = FxIndexMap::default();
171    for datatype_decl in datatype_decls {
172        for data_constructor in &datatype_decl.ctors {
173            for accessor in &data_constructor.fields {
174                if let Sort::App(ctor, _) = &accessor.sort
175                    && let SortCtor::Data(data_ctor) = &ctor
176                    // We skip undeclared opaque sorts, which are currently
177                    // encoded as Int.
178                    && datatype_dependencies.contains_key(data_ctor)
179                {
180                    datatype_dependencies
181                        .get_mut(&datatype_decl.name)
182                        .unwrap()
183                        .push(data_ctor.clone());
184                }
185            }
186        }
187        data_decls_by_name.insert(datatype_decl.name.clone(), datatype_decl);
188    }
189    graph::topological_sort_sccs(&datatype_dependencies)
190        .into_iter()
191        .flatten()
192        .rev()
193        .map(|datatype_decl_name| {
194            data_decls_by_name
195                .shift_remove(&datatype_decl_name)
196                .unwrap()
197        })
198        .collect_vec()
199}
200
201#[cfg(feature = "rust-fixpoint")]
202fn type_signature_matches<T: Types>(
203    argument_permutation: &[usize],
204    kvar_decl: &KVarDecl<T>,
205    qualifier: &Qualifier<T>,
206) -> bool {
207    if argument_permutation.len() != qualifier.args.len() {
208        return false;
209    }
210
211    for (qs, ks) in qualifier.args.iter().map(|param| param.sort.clone()).zip(
212        argument_permutation
213            .iter()
214            .map(|arg_idx| kvar_decl.sorts[*arg_idx].clone()),
215    ) {
216        if qs.to_string().ne(&ks.to_string()) {
217            return false;
218        }
219    }
220
221    true
222}
liquid_fixpoint/constraint_with_env.rs

liquid_fixpoint/
constraint_with_env.rs
