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