liquid_fixpoint/
constraint_with_env.rs

1use std::collections::{HashMap, VecDeque};
2
3use derive_where::derive_where;
4use itertools::Itertools;
5
6use crate::{
7    KVarDecl, Types,
8    constraint::{Constraint, Qualifier},
9    is_constraint_satisfiable,
10    parser::ParsingTypes,
11};
12
13#[derive_where(Hash)]
14pub struct ConstraintWithEnv<T: Types> {
15    pub kvar_decls: Vec<KVarDecl<T>>,
16    pub qualifiers: Vec<Qualifier<T>>,
17    pub constraint: Constraint<T>,
18}
19
20impl ConstraintWithEnv<ParsingTypes> {
21    pub fn is_satisfiable(&self) -> bool {
22        if self.kvar_decls.is_empty() {
23            self.constraint.is_satisfiable()
24        } else {
25            self.solve_by_fusion()
26        }
27    }
28
29    pub fn uniquify(&mut self) {
30        self.constraint.uniquify();
31    }
32
33    pub fn solve_by_fusion(&self) -> bool {
34        let mut cstr = self.constraint.clone();
35        let mut dep_map = self.constraint.kvar_mappings().1;
36        let mut acyclic_kvars: Vec<String> = dep_map
37            .into_iter()
38            .filter(|(_, dependencies)| dependencies.is_empty())
39            .map(|(kvar, _)| kvar)
40            .collect();
41        while !acyclic_kvars.is_empty() {
42            cstr = cstr.elim(&acyclic_kvars);
43            dep_map = cstr.kvar_mappings().1;
44            acyclic_kvars = dep_map
45                .into_iter()
46                .filter(|(_, dependencies)| dependencies.is_empty())
47                .map(|(kvar, _)| kvar)
48                .collect();
49        }
50        ConstraintWithEnv {
51            kvar_decls: self.kvar_decls.to_vec(),
52            qualifiers: self.qualifiers.to_vec(),
53            constraint: cstr,
54        }
55        .solve_by_predicate_abstraction()
56    }
57
58    pub fn solve_by_predicate_abstraction(&self) -> bool {
59        let mut qualifiers: Vec<Qualifier<ParsingTypes>> = vec![];
60        qualifiers.extend(self.qualifiers.to_vec().into_iter());
61        let kvar_assignment = self.solve_for_kvars(&qualifiers);
62        let no_kvar_cstr = self.constraint.sub_all_kvars(&kvar_assignment);
63        is_constraint_satisfiable(&no_kvar_cstr)
64    }
65
66    pub fn compute_initial_assignments<'a>(
67        &'a self,
68        qualifiers: &'a Vec<Qualifier<ParsingTypes>>,
69    ) -> HashMap<String, Vec<(&'a Qualifier<ParsingTypes>, Vec<usize>)>> {
70        let mut assignments = HashMap::new();
71
72        for decl in &self.kvar_decls {
73            let kvar_arg_count = decl.sorts.len();
74            for qualifier in qualifiers {
75                let qualifier_arg_count = qualifier.args.len();
76                for argument_combination in (0..kvar_arg_count).combinations(qualifier_arg_count) {
77                    assignments
78                        .entry(decl.kvid.clone())
79                        .or_insert(vec![])
80                        .extend(
81                            argument_combination
82                                .into_iter()
83                                .permutations(qualifier_arg_count)
84                                .filter(|arg_permutation| {
85                                    type_signature_matches(arg_permutation, decl, qualifier)
86                                })
87                                .map(|arg_permutation| (qualifier, arg_permutation)),
88                        );
89                }
90            }
91        }
92
93        assignments
94    }
95
96    pub fn solve_for_kvars<'a>(
97        &'a self,
98        qualifiers: &'a Vec<Qualifier<ParsingTypes>>,
99    ) -> HashMap<String, Vec<(&'a Qualifier<ParsingTypes>, Vec<usize>)>> {
100        let mut assignments = self.compute_initial_assignments(qualifiers);
101        let (kvars_to_fragments, _) = self.constraint.kvar_mappings();
102        let topo_order_fragments = self.constraint.topo_order_fragments();
103        let mut work_list = VecDeque::from_iter(topo_order_fragments.iter());
104        while !work_list.is_empty() {
105            if let Some(fragment) = work_list.pop_front() {
106                if let Some(kvar_name) = fragment.fragment_kvar_head() {
107                    let subbed = fragment.sub_kvars_except_head(&assignments);
108                    let assignment = assignments.get_mut(&kvar_name);
109                    if let Some(assignment) = assignment {
110                        let initial_length = assignment.len();
111                        assignment.retain(|assignment| {
112                            let vc = subbed.sub_head(assignment);
113                            is_constraint_satisfiable(&vc)
114                        });
115                        if initial_length > qualifiers.len() {
116                            work_list.extend(
117                                fragment
118                                    .kvar_deps()
119                                    .iter()
120                                    .map(|kvar| kvars_to_fragments.get(kvar).unwrap().iter())
121                                    .flatten(),
122                            );
123                        }
124                    }
125                }
126            }
127        }
128        assignments
129    }
130}
131
132fn type_signature_matches(
133    argument_permutation: &Vec<usize>,
134    kvar_decl: &KVarDecl<ParsingTypes>,
135    qualifier: &Qualifier<ParsingTypes>,
136) -> bool {
137    if argument_permutation.len() != qualifier.args.len() {
138        return false;
139    }
140
141    for (qs, ks) in qualifier.args.iter().map(|arg| arg.1.clone()).zip(
142        argument_permutation
143            .iter()
144            .map(|arg_idx| kvar_decl.sorts[*arg_idx].clone()),
145    ) {
146        if qs.to_string().ne(&ks.to_string()) {
147            return false;
148        }
149    }
150
151    true
152}
liquid_fixpoint/constraint_with_env.rs

liquid_fixpoint/
constraint_with_env.rs
