use std::cmp::Ordering;
use ruff_index::{Idx, IndexVec};
use rustc_hash::FxHashMap;
use crate::narrowing_constraints::{NarrowingConstraintsBuilder, ScopedNarrowingConstraint};
use crate::predicate::ScopedPredicateId;
use crate::rank::{RankBitBox, RankBitBoxVec};
#[derive(Clone, Copy, Eq, Hash, PartialEq, get_size2::GetSize)]
pub struct ScopedReachabilityConstraintId(u32);
impl std::fmt::Debug for ScopedReachabilityConstraintId {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
let mut f = f.debug_tuple("ScopedReachabilityConstraintId");
match *self {
ALWAYS_TRUE => f.field(&format_args!("AlwaysTrue")),
AMBIGUOUS => f.field(&format_args!("Ambiguous")),
ALWAYS_FALSE => f.field(&format_args!("AlwaysFalse")),
_ => f.field(&self.0),
};
f.finish()
}
}
#[derive(Clone, Copy, Debug, Eq, Hash, PartialEq, get_size2::GetSize)]
pub struct InteriorNode {
atom: ScopedPredicateId,
if_true: ScopedReachabilityConstraintId,
if_ambiguous: ScopedReachabilityConstraintId,
if_false: ScopedReachabilityConstraintId,
}
impl InteriorNode {
pub const fn atom(self) -> ScopedPredicateId {
self.atom
}
pub const fn if_true(self) -> ScopedReachabilityConstraintId {
self.if_true
}
pub const fn if_ambiguous(self) -> ScopedReachabilityConstraintId {
self.if_ambiguous
}
pub const fn if_false(self) -> ScopedReachabilityConstraintId {
self.if_false
}
}
impl ScopedReachabilityConstraintId {
pub const ALWAYS_TRUE: ScopedReachabilityConstraintId =
ScopedReachabilityConstraintId(0xffff_ffff);
pub const AMBIGUOUS: ScopedReachabilityConstraintId =
ScopedReachabilityConstraintId(0xffff_fffe);
pub const ALWAYS_FALSE: ScopedReachabilityConstraintId =
ScopedReachabilityConstraintId(0xffff_fffd);
pub(crate) fn is_terminal(self) -> bool {
self.0 >= SMALLEST_TERMINAL.0
}
fn as_u32(self) -> u32 {
self.0
}
}
impl Idx for ScopedReachabilityConstraintId {
#[inline]
fn new(value: usize) -> Self {
assert!(value <= (SMALLEST_TERMINAL.0 as usize));
#[expect(clippy::cast_possible_truncation)]
Self(value as u32)
}
#[inline]
fn index(self) -> usize {
debug_assert!(!self.is_terminal());
self.0 as usize
}
}
const ALWAYS_TRUE: ScopedReachabilityConstraintId = ScopedReachabilityConstraintId::ALWAYS_TRUE;
const AMBIGUOUS: ScopedReachabilityConstraintId = ScopedReachabilityConstraintId::AMBIGUOUS;
const ALWAYS_FALSE: ScopedReachabilityConstraintId = ScopedReachabilityConstraintId::ALWAYS_FALSE;
const SMALLEST_TERMINAL: ScopedReachabilityConstraintId = ALWAYS_FALSE;
const MAX_INTERIOR_NODES: usize = 512 * 1024;
#[derive(Debug, PartialEq, Eq, get_size2::GetSize)]
pub struct ReachabilityConstraints {
used_interiors: Box<[InteriorNode]>,
used_indices: Option<RankBitBox>,
}
impl ReachabilityConstraints {
pub fn get_interior_node(&self, id: ScopedReachabilityConstraintId) -> InteriorNode {
debug_assert!(!id.is_terminal());
let raw_index = id.as_u32() as usize;
if let Some(used_indices) = &self.used_indices {
debug_assert!(
used_indices.get_bit(raw_index).unwrap_or(false),
"all used reachability constraints should have been marked as used",
);
let index = used_indices.rank(raw_index) as usize;
self.used_interiors[index]
} else {
self.used_interiors[raw_index]
}
}
pub fn used_interiors(&self) -> &[InteriorNode] {
&self.used_interiors
}
}
#[derive(Debug, Default, PartialEq, Eq)]
pub struct ReachabilityConstraintsBuilder {
interiors: IndexVec<ScopedReachabilityConstraintId, InteriorNode>,
interior_used: RankBitBoxVec,
interior_cache: FxHashMap<InteriorNode, ScopedReachabilityConstraintId>,
not_cache: FxHashMap<ScopedReachabilityConstraintId, ScopedReachabilityConstraintId>,
and_cache: FxHashMap<
(
ScopedReachabilityConstraintId,
ScopedReachabilityConstraintId,
),
ScopedReachabilityConstraintId,
>,
or_cache: FxHashMap<
(
ScopedReachabilityConstraintId,
ScopedReachabilityConstraintId,
),
ScopedReachabilityConstraintId,
>,
}
impl ReachabilityConstraintsBuilder {
pub(crate) fn is_saturated(&self) -> bool {
self.interiors.len() >= MAX_INTERIOR_NODES
}
pub(crate) fn build(self) -> ReachabilityConstraints {
if self.interior_used.first_zero().is_none() {
ReachabilityConstraints {
used_interiors: self.interiors.raw.into_boxed_slice(),
used_indices: None,
}
} else {
let used_interiors = (self.interiors.into_iter())
.zip(&self.interior_used)
.filter_map(|(interior, used)| used.then_some(interior))
.collect();
let used_indices = RankBitBox::from_bits(self.interior_used);
ReachabilityConstraints {
used_interiors,
used_indices: Some(used_indices),
}
}
}
pub(crate) fn mark_used(&mut self, node: ScopedReachabilityConstraintId) {
if !node.is_terminal() && !self.interior_used[node.index()] {
self.interior_used.set(node.index(), true);
let node = self.interiors[node];
self.mark_used(node.if_true);
self.mark_used(node.if_ambiguous);
self.mark_used(node.if_false);
}
}
pub(crate) fn narrowing_gate(
&self,
root: ScopedReachabilityConstraintId,
narrowing_constraints: &mut NarrowingConstraintsBuilder,
) -> ScopedNarrowingConstraint {
enum Action {
Visit(ScopedReachabilityConstraintId),
Finish(ScopedReachabilityConstraintId),
}
let terminal = |id| match id {
ScopedReachabilityConstraintId::ALWAYS_TRUE
| ScopedReachabilityConstraintId::AMBIGUOUS => {
Some(ScopedNarrowingConstraint::ALWAYS_TRUE)
}
ScopedReachabilityConstraintId::ALWAYS_FALSE => {
Some(ScopedNarrowingConstraint::ALWAYS_FALSE)
}
_ => None,
};
if let Some(root) = terminal(root) {
return root;
}
let root_node = self.interiors[root];
if let (Some(if_true), Some(if_false)) =
(terminal(root_node.if_true), terminal(root_node.if_false))
{
return narrowing_constraints.add_conditional(root_node.atom, if_true, if_false);
}
let mut converted = FxHashMap::default();
let mut actions = vec![Action::Visit(root)];
while let Some(action) = actions.pop() {
match action {
Action::Visit(id) => {
if terminal(id).is_some() || converted.contains_key(&id) {
continue;
}
let node = self.interiors[id];
actions.push(Action::Finish(id));
actions.push(Action::Visit(node.if_false));
actions.push(Action::Visit(node.if_true));
}
Action::Finish(id) => {
let node = self.interiors[id];
let if_true =
terminal(node.if_true).unwrap_or_else(|| converted[&node.if_true]);
let if_false =
terminal(node.if_false).unwrap_or_else(|| converted[&node.if_false]);
let result =
narrowing_constraints.add_conditional(node.atom, if_true, if_false);
converted.insert(id, result);
}
}
}
converted[&root]
}
fn cmp_atoms(
&self,
a: ScopedReachabilityConstraintId,
b: ScopedReachabilityConstraintId,
) -> Ordering {
if a == b || (a.is_terminal() && b.is_terminal()) {
Ordering::Equal
} else if a.is_terminal() {
Ordering::Greater
} else if b.is_terminal() {
Ordering::Less
} else {
self.interiors[a]
.atom
.cmp(&self.interiors[b].atom)
.reverse()
}
}
fn add_interior(&mut self, node: InteriorNode) -> ScopedReachabilityConstraintId {
if node.if_true == node.if_false {
return node.if_true;
}
*self.interior_cache.entry(node).or_insert_with(|| {
self.interior_used.push(false);
self.interiors.push(node)
})
}
pub(crate) fn add_atom(
&mut self,
predicate: ScopedPredicateId,
) -> ScopedReachabilityConstraintId {
if predicate == ScopedPredicateId::ALWAYS_FALSE {
ALWAYS_FALSE
} else if predicate == ScopedPredicateId::ALWAYS_TRUE {
ALWAYS_TRUE
} else {
self.add_interior(InteriorNode {
atom: predicate,
if_true: ALWAYS_TRUE,
if_ambiguous: AMBIGUOUS,
if_false: ALWAYS_FALSE,
})
}
}
pub(crate) fn add_not_constraint(
&mut self,
a: ScopedReachabilityConstraintId,
) -> ScopedReachabilityConstraintId {
if a == ALWAYS_TRUE {
return ALWAYS_FALSE;
} else if a == AMBIGUOUS {
return AMBIGUOUS;
} else if a == ALWAYS_FALSE {
return ALWAYS_TRUE;
}
if let Some(cached) = self.not_cache.get(&a) {
return *cached;
}
if self.interiors.len() >= MAX_INTERIOR_NODES {
return AMBIGUOUS;
}
let a_node = self.interiors[a];
let if_true = self.add_not_constraint(a_node.if_true);
let if_ambiguous = self.add_not_constraint(a_node.if_ambiguous);
let if_false = self.add_not_constraint(a_node.if_false);
let result = self.add_interior(InteriorNode {
atom: a_node.atom,
if_true,
if_ambiguous,
if_false,
});
self.not_cache.insert(a, result);
result
}
pub(crate) fn add_or_constraint(
&mut self,
a: ScopedReachabilityConstraintId,
b: ScopedReachabilityConstraintId,
) -> ScopedReachabilityConstraintId {
match (a, b) {
(ALWAYS_TRUE, _) | (_, ALWAYS_TRUE) => return ALWAYS_TRUE,
(ALWAYS_FALSE, other) | (other, ALWAYS_FALSE) => return other,
_ if a == b => return a,
_ => {}
}
let (a, b) = if b.0 < a.0 { (b, a) } else { (a, b) };
if let Some(cached) = self.or_cache.get(&(a, b)) {
return *cached;
}
if self.interiors.len() >= MAX_INTERIOR_NODES {
return AMBIGUOUS;
}
let (atom, if_true, if_ambiguous, if_false) = match self.cmp_atoms(a, b) {
Ordering::Equal => {
let a_node = self.interiors[a];
let b_node = self.interiors[b];
let if_true = self.add_or_constraint(a_node.if_true, b_node.if_true);
let if_false = self.add_or_constraint(a_node.if_false, b_node.if_false);
let if_ambiguous = if if_true == if_false {
if_true
} else {
self.add_or_constraint(a_node.if_ambiguous, b_node.if_ambiguous)
};
(a_node.atom, if_true, if_ambiguous, if_false)
}
Ordering::Less => {
let a_node = self.interiors[a];
let if_true = self.add_or_constraint(a_node.if_true, b);
let if_false = self.add_or_constraint(a_node.if_false, b);
let if_ambiguous = if if_true == if_false {
if_true
} else {
self.add_or_constraint(a_node.if_ambiguous, b)
};
(a_node.atom, if_true, if_ambiguous, if_false)
}
Ordering::Greater => {
let b_node = self.interiors[b];
let if_true = self.add_or_constraint(a, b_node.if_true);
let if_false = self.add_or_constraint(a, b_node.if_false);
let if_ambiguous = if if_true == if_false {
if_true
} else {
self.add_or_constraint(a, b_node.if_ambiguous)
};
(b_node.atom, if_true, if_ambiguous, if_false)
}
};
let result = self.add_interior(InteriorNode {
atom,
if_true,
if_ambiguous,
if_false,
});
self.or_cache.insert((a, b), result);
result
}
pub(crate) fn add_and_constraint(
&mut self,
a: ScopedReachabilityConstraintId,
b: ScopedReachabilityConstraintId,
) -> ScopedReachabilityConstraintId {
match (a, b) {
(ALWAYS_FALSE, _) | (_, ALWAYS_FALSE) => return ALWAYS_FALSE,
(ALWAYS_TRUE, other) | (other, ALWAYS_TRUE) => return other,
_ if a == b => return a,
_ => {}
}
let (a, b) = if b.0 < a.0 { (b, a) } else { (a, b) };
if let Some(cached) = self.and_cache.get(&(a, b)) {
return *cached;
}
if self.interiors.len() >= MAX_INTERIOR_NODES {
return AMBIGUOUS;
}
let (atom, if_true, if_ambiguous, if_false) = match self.cmp_atoms(a, b) {
Ordering::Equal => {
let a_node = self.interiors[a];
let b_node = self.interiors[b];
let if_true = self.add_and_constraint(a_node.if_true, b_node.if_true);
let if_false = self.add_and_constraint(a_node.if_false, b_node.if_false);
let if_ambiguous = if if_true == if_false {
if_true
} else {
self.add_and_constraint(a_node.if_ambiguous, b_node.if_ambiguous)
};
(a_node.atom, if_true, if_ambiguous, if_false)
}
Ordering::Less => {
let a_node = self.interiors[a];
let if_true = self.add_and_constraint(a_node.if_true, b);
let if_false = self.add_and_constraint(a_node.if_false, b);
let if_ambiguous = if if_true == if_false {
if_true
} else {
self.add_and_constraint(a_node.if_ambiguous, b)
};
(a_node.atom, if_true, if_ambiguous, if_false)
}
Ordering::Greater => {
let b_node = self.interiors[b];
let if_true = self.add_and_constraint(a, b_node.if_true);
let if_false = self.add_and_constraint(a, b_node.if_false);
let if_ambiguous = if if_true == if_false {
if_true
} else {
self.add_and_constraint(a, b_node.if_ambiguous)
};
(b_node.atom, if_true, if_ambiguous, if_false)
}
};
let result = self.add_interior(InteriorNode {
atom,
if_true,
if_ambiguous,
if_false,
});
self.and_cache.insert((a, b), result);
result
}
}