1use std::cmp::Ordering;
6
7use ruff_index::{Idx, IndexVec};
8use rustc_hash::FxHashMap;
9
10use crate::narrowing_constraints::{NarrowingConstraintsBuilder, ScopedNarrowingConstraint};
11use crate::predicate::ScopedPredicateId;
12use crate::rank::{RankBitBox, RankBitBoxVec};
13
14#[derive(Clone, Copy, Eq, Hash, PartialEq, get_size2::GetSize)]
34pub struct ScopedReachabilityConstraintId(u32);
35
36impl std::fmt::Debug for ScopedReachabilityConstraintId {
37 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
38 let mut f = f.debug_tuple("ScopedReachabilityConstraintId");
39 match *self {
40 ALWAYS_TRUE => f.field(&format_args!("AlwaysTrue")),
44 AMBIGUOUS => f.field(&format_args!("Ambiguous")),
45 ALWAYS_FALSE => f.field(&format_args!("AlwaysFalse")),
46 _ => f.field(&self.0),
47 };
48 f.finish()
49 }
50}
51
52#[derive(Clone, Copy, Debug, Eq, Hash, PartialEq, get_size2::GetSize)]
63pub struct InteriorNode {
64 atom: ScopedPredicateId,
68 if_true: ScopedReachabilityConstraintId,
69 if_ambiguous: ScopedReachabilityConstraintId,
70 if_false: ScopedReachabilityConstraintId,
71}
72
73impl InteriorNode {
74 pub const fn atom(self) -> ScopedPredicateId {
75 self.atom
76 }
77
78 pub const fn if_true(self) -> ScopedReachabilityConstraintId {
79 self.if_true
80 }
81
82 pub const fn if_ambiguous(self) -> ScopedReachabilityConstraintId {
83 self.if_ambiguous
84 }
85
86 pub const fn if_false(self) -> ScopedReachabilityConstraintId {
87 self.if_false
88 }
89}
90
91impl ScopedReachabilityConstraintId {
92 pub const ALWAYS_TRUE: ScopedReachabilityConstraintId =
94 ScopedReachabilityConstraintId(0xffff_ffff);
95
96 pub const AMBIGUOUS: ScopedReachabilityConstraintId =
98 ScopedReachabilityConstraintId(0xffff_fffe);
99
100 pub const ALWAYS_FALSE: ScopedReachabilityConstraintId =
102 ScopedReachabilityConstraintId(0xffff_fffd);
103
104 pub(crate) fn is_terminal(self) -> bool {
105 self.0 >= SMALLEST_TERMINAL.0
106 }
107
108 fn as_u32(self) -> u32 {
109 self.0
110 }
111}
112
113impl Idx for ScopedReachabilityConstraintId {
114 #[inline]
115 fn new(value: usize) -> Self {
116 assert!(value <= (SMALLEST_TERMINAL.0 as usize));
117 #[expect(clippy::cast_possible_truncation)]
118 Self(value as u32)
119 }
120
121 #[inline]
122 fn index(self) -> usize {
123 debug_assert!(!self.is_terminal());
124 self.0 as usize
125 }
126}
127
128const ALWAYS_TRUE: ScopedReachabilityConstraintId = ScopedReachabilityConstraintId::ALWAYS_TRUE;
130const AMBIGUOUS: ScopedReachabilityConstraintId = ScopedReachabilityConstraintId::AMBIGUOUS;
131const ALWAYS_FALSE: ScopedReachabilityConstraintId = ScopedReachabilityConstraintId::ALWAYS_FALSE;
132const SMALLEST_TERMINAL: ScopedReachabilityConstraintId = ALWAYS_FALSE;
133
134const MAX_INTERIOR_NODES: usize = 512 * 1024;
139
140#[derive(Debug, PartialEq, Eq, get_size2::GetSize)]
142pub struct ReachabilityConstraints {
143 used_interiors: Box<[InteriorNode]>,
145 used_indices: Option<RankBitBox>,
151}
152
153impl ReachabilityConstraints {
154 pub fn get_interior_node(&self, id: ScopedReachabilityConstraintId) -> InteriorNode {
156 debug_assert!(!id.is_terminal());
157 let raw_index = id.as_u32() as usize;
158 if let Some(used_indices) = &self.used_indices {
159 debug_assert!(
160 used_indices.get_bit(raw_index).unwrap_or(false),
161 "all used reachability constraints should have been marked as used",
162 );
163 let index = used_indices.rank(raw_index) as usize;
164 self.used_interiors[index]
165 } else {
166 self.used_interiors[raw_index]
167 }
168 }
169
170 pub fn used_interiors(&self) -> &[InteriorNode] {
171 &self.used_interiors
172 }
173}
174
175#[derive(Debug, Default, PartialEq, Eq)]
176pub struct ReachabilityConstraintsBuilder {
177 interiors: IndexVec<ScopedReachabilityConstraintId, InteriorNode>,
178 interior_used: RankBitBoxVec,
179 interior_cache: FxHashMap<InteriorNode, ScopedReachabilityConstraintId>,
180 not_cache: FxHashMap<ScopedReachabilityConstraintId, ScopedReachabilityConstraintId>,
181 and_cache: FxHashMap<
182 (
183 ScopedReachabilityConstraintId,
184 ScopedReachabilityConstraintId,
185 ),
186 ScopedReachabilityConstraintId,
187 >,
188 or_cache: FxHashMap<
189 (
190 ScopedReachabilityConstraintId,
191 ScopedReachabilityConstraintId,
192 ),
193 ScopedReachabilityConstraintId,
194 >,
195}
196
197impl ReachabilityConstraintsBuilder {
198 pub(crate) fn is_saturated(&self) -> bool {
200 self.interiors.len() >= MAX_INTERIOR_NODES
201 }
202
203 pub(crate) fn build(self) -> ReachabilityConstraints {
204 if self.interior_used.first_zero().is_none() {
205 ReachabilityConstraints {
206 used_interiors: self.interiors.raw.into_boxed_slice(),
207 used_indices: None,
208 }
209 } else {
210 let used_interiors = (self.interiors.into_iter())
211 .zip(&self.interior_used)
212 .filter_map(|(interior, used)| used.then_some(interior))
213 .collect();
214 let used_indices = RankBitBox::from_bits(self.interior_used);
215 ReachabilityConstraints {
216 used_interiors,
217 used_indices: Some(used_indices),
218 }
219 }
220 }
221
222 pub(crate) fn mark_used(&mut self, node: ScopedReachabilityConstraintId) {
226 if !node.is_terminal() && !self.interior_used[node.index()] {
227 self.interior_used.set(node.index(), true);
228 let node = self.interiors[node];
229 self.mark_used(node.if_true);
230 self.mark_used(node.if_ambiguous);
231 self.mark_used(node.if_false);
232 }
233 }
234
235 pub(crate) fn narrowing_gate(
242 &self,
243 root: ScopedReachabilityConstraintId,
244 narrowing_constraints: &mut NarrowingConstraintsBuilder,
245 ) -> ScopedNarrowingConstraint {
246 enum Action {
247 Visit(ScopedReachabilityConstraintId),
248 Finish(ScopedReachabilityConstraintId),
249 }
250
251 let terminal = |id| match id {
252 ScopedReachabilityConstraintId::ALWAYS_TRUE
253 | ScopedReachabilityConstraintId::AMBIGUOUS => {
254 Some(ScopedNarrowingConstraint::ALWAYS_TRUE)
255 }
256 ScopedReachabilityConstraintId::ALWAYS_FALSE => {
257 Some(ScopedNarrowingConstraint::ALWAYS_FALSE)
258 }
259 _ => None,
260 };
261
262 if let Some(root) = terminal(root) {
263 return root;
264 }
265
266 let root_node = self.interiors[root];
267 if let (Some(if_true), Some(if_false)) =
268 (terminal(root_node.if_true), terminal(root_node.if_false))
269 {
270 return narrowing_constraints.add_conditional(root_node.atom, if_true, if_false);
271 }
272
273 let mut converted = FxHashMap::default();
274 let mut actions = vec![Action::Visit(root)];
275
276 while let Some(action) = actions.pop() {
277 match action {
278 Action::Visit(id) => {
279 if terminal(id).is_some() || converted.contains_key(&id) {
280 continue;
281 }
282
283 let node = self.interiors[id];
284 actions.push(Action::Finish(id));
285 actions.push(Action::Visit(node.if_false));
286 actions.push(Action::Visit(node.if_true));
287 }
288 Action::Finish(id) => {
289 let node = self.interiors[id];
290 let if_true =
291 terminal(node.if_true).unwrap_or_else(|| converted[&node.if_true]);
292 let if_false =
293 terminal(node.if_false).unwrap_or_else(|| converted[&node.if_false]);
294 let result =
295 narrowing_constraints.add_conditional(node.atom, if_true, if_false);
296 converted.insert(id, result);
297 }
298 }
299 }
300
301 converted[&root]
302 }
303
304 fn cmp_atoms(
325 &self,
326 a: ScopedReachabilityConstraintId,
327 b: ScopedReachabilityConstraintId,
328 ) -> Ordering {
329 if a == b || (a.is_terminal() && b.is_terminal()) {
330 Ordering::Equal
331 } else if a.is_terminal() {
332 Ordering::Greater
333 } else if b.is_terminal() {
334 Ordering::Less
335 } else {
336 self.interiors[a]
339 .atom
340 .cmp(&self.interiors[b].atom)
341 .reverse()
342 }
343 }
344
345 fn add_interior(&mut self, node: InteriorNode) -> ScopedReachabilityConstraintId {
348 if node.if_true == node.if_false {
351 return node.if_true;
352 }
353
354 *self.interior_cache.entry(node).or_insert_with(|| {
355 self.interior_used.push(false);
356 self.interiors.push(node)
357 })
358 }
359
360 pub(crate) fn add_atom(
372 &mut self,
373 predicate: ScopedPredicateId,
374 ) -> ScopedReachabilityConstraintId {
375 if predicate == ScopedPredicateId::ALWAYS_FALSE {
376 ALWAYS_FALSE
377 } else if predicate == ScopedPredicateId::ALWAYS_TRUE {
378 ALWAYS_TRUE
379 } else {
380 self.add_interior(InteriorNode {
381 atom: predicate,
382 if_true: ALWAYS_TRUE,
383 if_ambiguous: AMBIGUOUS,
384 if_false: ALWAYS_FALSE,
385 })
386 }
387 }
388
389 pub(crate) fn add_not_constraint(
391 &mut self,
392 a: ScopedReachabilityConstraintId,
393 ) -> ScopedReachabilityConstraintId {
394 if a == ALWAYS_TRUE {
395 return ALWAYS_FALSE;
396 } else if a == AMBIGUOUS {
397 return AMBIGUOUS;
398 } else if a == ALWAYS_FALSE {
399 return ALWAYS_TRUE;
400 }
401
402 if let Some(cached) = self.not_cache.get(&a) {
403 return *cached;
404 }
405
406 if self.interiors.len() >= MAX_INTERIOR_NODES {
407 return AMBIGUOUS;
408 }
409
410 let a_node = self.interiors[a];
411 let if_true = self.add_not_constraint(a_node.if_true);
412 let if_ambiguous = self.add_not_constraint(a_node.if_ambiguous);
413 let if_false = self.add_not_constraint(a_node.if_false);
414 let result = self.add_interior(InteriorNode {
415 atom: a_node.atom,
416 if_true,
417 if_ambiguous,
418 if_false,
419 });
420 self.not_cache.insert(a, result);
421 result
422 }
423
424 pub(crate) fn add_or_constraint(
426 &mut self,
427 a: ScopedReachabilityConstraintId,
428 b: ScopedReachabilityConstraintId,
429 ) -> ScopedReachabilityConstraintId {
430 match (a, b) {
431 (ALWAYS_TRUE, _) | (_, ALWAYS_TRUE) => return ALWAYS_TRUE,
432 (ALWAYS_FALSE, other) | (other, ALWAYS_FALSE) => return other,
433 _ if a == b => return a,
434 _ => {}
435 }
436
437 let (a, b) = if b.0 < a.0 { (b, a) } else { (a, b) };
439 if let Some(cached) = self.or_cache.get(&(a, b)) {
440 return *cached;
441 }
442
443 if self.interiors.len() >= MAX_INTERIOR_NODES {
444 return AMBIGUOUS;
445 }
446
447 let (atom, if_true, if_ambiguous, if_false) = match self.cmp_atoms(a, b) {
448 Ordering::Equal => {
449 let a_node = self.interiors[a];
450 let b_node = self.interiors[b];
451 let if_true = self.add_or_constraint(a_node.if_true, b_node.if_true);
452 let if_false = self.add_or_constraint(a_node.if_false, b_node.if_false);
453 let if_ambiguous = if if_true == if_false {
454 if_true
455 } else {
456 self.add_or_constraint(a_node.if_ambiguous, b_node.if_ambiguous)
457 };
458 (a_node.atom, if_true, if_ambiguous, if_false)
459 }
460 Ordering::Less => {
461 let a_node = self.interiors[a];
462 let if_true = self.add_or_constraint(a_node.if_true, b);
463 let if_false = self.add_or_constraint(a_node.if_false, b);
464 let if_ambiguous = if if_true == if_false {
465 if_true
466 } else {
467 self.add_or_constraint(a_node.if_ambiguous, b)
468 };
469 (a_node.atom, if_true, if_ambiguous, if_false)
470 }
471 Ordering::Greater => {
472 let b_node = self.interiors[b];
473 let if_true = self.add_or_constraint(a, b_node.if_true);
474 let if_false = self.add_or_constraint(a, b_node.if_false);
475 let if_ambiguous = if if_true == if_false {
476 if_true
477 } else {
478 self.add_or_constraint(a, b_node.if_ambiguous)
479 };
480 (b_node.atom, if_true, if_ambiguous, if_false)
481 }
482 };
483
484 let result = self.add_interior(InteriorNode {
485 atom,
486 if_true,
487 if_ambiguous,
488 if_false,
489 });
490 self.or_cache.insert((a, b), result);
491 result
492 }
493
494 pub(crate) fn add_and_constraint(
496 &mut self,
497 a: ScopedReachabilityConstraintId,
498 b: ScopedReachabilityConstraintId,
499 ) -> ScopedReachabilityConstraintId {
500 match (a, b) {
501 (ALWAYS_FALSE, _) | (_, ALWAYS_FALSE) => return ALWAYS_FALSE,
502 (ALWAYS_TRUE, other) | (other, ALWAYS_TRUE) => return other,
503 _ if a == b => return a,
504 _ => {}
505 }
506
507 let (a, b) = if b.0 < a.0 { (b, a) } else { (a, b) };
509 if let Some(cached) = self.and_cache.get(&(a, b)) {
510 return *cached;
511 }
512
513 if self.interiors.len() >= MAX_INTERIOR_NODES {
514 return AMBIGUOUS;
515 }
516
517 let (atom, if_true, if_ambiguous, if_false) = match self.cmp_atoms(a, b) {
518 Ordering::Equal => {
519 let a_node = self.interiors[a];
520 let b_node = self.interiors[b];
521 let if_true = self.add_and_constraint(a_node.if_true, b_node.if_true);
522 let if_false = self.add_and_constraint(a_node.if_false, b_node.if_false);
523 let if_ambiguous = if if_true == if_false {
524 if_true
525 } else {
526 self.add_and_constraint(a_node.if_ambiguous, b_node.if_ambiguous)
527 };
528 (a_node.atom, if_true, if_ambiguous, if_false)
529 }
530 Ordering::Less => {
531 let a_node = self.interiors[a];
532 let if_true = self.add_and_constraint(a_node.if_true, b);
533 let if_false = self.add_and_constraint(a_node.if_false, b);
534 let if_ambiguous = if if_true == if_false {
535 if_true
536 } else {
537 self.add_and_constraint(a_node.if_ambiguous, b)
538 };
539 (a_node.atom, if_true, if_ambiguous, if_false)
540 }
541 Ordering::Greater => {
542 let b_node = self.interiors[b];
543 let if_true = self.add_and_constraint(a, b_node.if_true);
544 let if_false = self.add_and_constraint(a, b_node.if_false);
545 let if_ambiguous = if if_true == if_false {
546 if_true
547 } else {
548 self.add_and_constraint(a, b_node.if_ambiguous)
549 };
550 (b_node.atom, if_true, if_ambiguous, if_false)
551 }
552 };
553
554 let result = self.add_interior(InteriorNode {
555 atom,
556 if_true,
557 if_ambiguous,
558 if_false,
559 });
560 self.and_cache.insert((a, b), result);
561 result
562 }
563}