veryl-analyzer 0.22.0

//! Guarded composition of non-zero positional cycles.
//!
//! # Correctness
//!
//! Every `GuardedCycle` is a first-return walk at one anchor. A sequence of
//! them is a closed positional walk exactly when their conditions have a
//! common branch valuation and their composed relation intersects identity.
//!
//! For exact translations, relation composition adds the two-dimensional
//! displacement while `compose_feasible_positions` computes exactly the
//! anchor positions for which the concatenation exists. If non-zero integer
//! vectors have a non-negative sum of zero, a support-minimal such sum in two
//! dimensions uses either an opposing pair or three vectors surrounding the
//! origin. Therefore `compatible_cycle_displacements_cancel` can safely reject
//! the exact-only case when it finds neither. The cyclic order of any closed
//! word also lies in one strongly connected component of the feasible
//! relation-to-relation transition graph, so components without a cancelling
//! displacement set are safely rejected. The pair and triple paths construct
//! feasible repetitions directly; the fallback worklist retains the exact
//! accumulated displacement, feasible positions, and condition. Hence it finds
//! every remaining feasible zero-displacement word.
//!
//! A closed word containing a non-translation relation can be rotated at its
//! concrete intermediate position to start with that relation. Thus
//! `guarded_relations_close` loses nothing by seeding only non-translations and
//! appending every first-return relation thereafter. Relational composition is
//! exact, and discarding a state only when a weaker condition carries a
//! superset relation is safe by monotonicity of composition. The specialized
//! repeated-translation checks construct a feasible composition intersecting
//! identity. A pair with a fixed return coordinate also admits an exact
//! negative decision: every intervening run has a unique length, whose
//! divisibility and endpoint extrema decide feasibility without enumeration.

use super::relation::PositionRelationSet;
use super::{FeasiblePosition, SearchBudget, insert_cycle_state, intersect_axis};
use crate::comb_loop_detect::model::BitDependency;
use crate::comb_loop_detect::ssa::PathCondition;
use crate::{HashMap, HashSet};
use daggy::petgraph::Graph;
use daggy::petgraph::algo::kosaraju_scc;
use std::collections::VecDeque;

#[derive(Clone, Debug, PartialEq, Eq, Hash)]
pub(super) struct GuardedCycle {
    pub(super) relation: PositionRelationSet,
    pub(super) condition: PathCondition,
}

pub(super) fn guarded_cycle_displacements_cancel(
    cycles: &HashSet<GuardedCycle>,
    budget: &mut SearchBudget,
) -> bool {
    let mut grouped: HashMap<(BitDependency, PathCondition), Vec<FeasiblePosition>> =
        HashMap::default();
    let mut all_exact = true;
    for cycle in cycles {
        if !budget.spend_product(cycle.relation.piece_count(), 1) {
            return false;
        }
        if let Some((dependency, feasible)) = cycle.relation.exact_translation() {
            grouped
                .entry((dependency, cycle.condition.clone()))
                .or_default()
                .extend(feasible);
        } else {
            all_exact = false;
        }
    }
    // Equivalent translations reached through separate read views describe
    // one relation on the union of their domains. Coalesce adjacent strips
    // before composing cycles; enumerating their paths loses that sharing.
    let translations = grouped
        .into_iter()
        .map(|((dependency, condition), mut feasible)| {
            coalesce_feasible_positions(&mut feasible);
            GuardedTranslation {
                dependency,
                condition,
                feasible,
            }
        })
        .collect::<Vec<_>>();

    if closed_translation_domain(&translations, budget)
        || guarded_translations_cancel(&translations, budget)
    {
        return true;
    }
    if budget.exhausted || all_exact {
        return false;
    }
    for cycle in cycles {
        for translation in &translations {
            if !budget.spend_conditions(&cycle.condition, &translation.condition) {
                return false;
            }
            if cycle
                .condition
                .conjoin_if_compatible(&translation.condition)
                .is_some()
                && translation.dependency.exact_offset().is_some_and(|offset| {
                    cycle.relation.closes_after_repeating_translation(
                        offset,
                        &translation.feasible,
                        budget,
                    )
                })
            {
                return true;
            }
        }
    }

    guarded_relations_close(cycles, budget)
}

/// A nonempty finite domain with an enabled successor inside itself contains
/// a cycle. All translations here must admit one common branch valuation.
/// Their source domains cover the candidate set by construction, and every
/// image must remain inside it. This proves rotations without enumerating
/// positions or searching for a word of width/gcd(width, shift) translations.
/// Failure of this sufficient check leaves the exact solver unchanged.
fn closed_translation_domain(cycles: &[GuardedTranslation], budget: &mut SearchBudget) -> bool {
    let mut condition = PathCondition::default();
    let mut domain = Vec::new();
    for cycle in cycles {
        if !budget.spend_conditions(&condition, &cycle.condition) {
            return false;
        }
        let Some(next) = condition.conjoin_if_compatible(&cycle.condition) else {
            return false;
        };
        condition = next;
        for &position in &cycle.feasible {
            if !budget.spend(1) {
                return false;
            }
            let (Some(array), Some(packed)) = (position.array, position.packed) else {
                return false;
            };
            if array.0 >= array.1 || packed.0 >= packed.1 {
                return false;
            }
            domain.push(position);
        }
    }
    if domain.is_empty() {
        return false;
    }
    coalesce_feasible_positions(&mut domain);
    for cycle in cycles {
        let Some((array, packed)) = cycle.dependency.exact_offset() else {
            return false;
        };
        for position in &cycle.feasible {
            let translated = |axis: Option<(isize, isize)>, offset| {
                let (lo, hi) = axis?;
                Some((lo.checked_add(offset)?, hi.checked_add(offset)?))
            };
            let (Some(array), Some(packed)) = (
                translated(position.array, array),
                translated(position.packed, packed),
            ) else {
                return false;
            };
            let mut covered = false;
            for region in &domain {
                if !budget.spend(1) {
                    return false;
                }
                if axis_contains(region.array, Some(array))
                    && axis_contains(region.packed, Some(packed))
                {
                    covered = true;
                    break;
                }
            }
            if !covered {
                return false;
            }
        }
    }
    true
}

// Merge only rectangles with an identical other axis. This preserves gaps,
// both positional axes, and every possible transition; it never takes a
// bounding box of rectangles that would introduce extra points.
fn coalesce_feasible_positions(positions: &mut Vec<FeasiblePosition>) {
    for packed in [false, true] {
        let axes = |position: &FeasiblePosition| {
            if packed {
                (position.array, position.packed)
            } else {
                (position.packed, position.array)
            }
        };
        positions.sort_unstable_by_key(axes);
        let mut end = 0;
        for index in 0..positions.len() {
            let next = positions[index];
            if end != 0 {
                let previous = &mut positions[end - 1];
                let (fixed, interval) = axes(previous);
                let (next_fixed, next_interval) = axes(&next);
                if fixed == next_fixed {
                    let merged = match (interval, next_interval) {
                        (None, _) | (_, None) => Some(None),
                        (Some((lo, hi)), Some((next_lo, next_hi))) if next_lo <= hi => {
                            Some(Some((lo.min(next_lo), hi.max(next_hi))))
                        }
                        _ => None,
                    };
                    if let Some(merged) = merged {
                        if packed {
                            previous.packed = merged;
                        } else {
                            previous.array = merged;
                        }
                        continue;
                    }
                }
            }
            positions[end] = next;
            end += 1;
        }
        positions.truncate(end);
    }
}

fn guarded_relations_close(cycles: &HashSet<GuardedCycle>, budget: &mut SearchBudget) -> bool {
    let cycles = cycles.iter().collect::<Vec<_>>();
    let mut reached: Vec<(PositionRelationSet, PathCondition)> = Vec::new();
    let mut queue = VecDeque::new();
    // Exact-only closed walks were decided above. Any remaining closed walk
    // contains a non-translation relation and can be rotated to start there,
    // so do not enumerate arbitrarily long exact prefixes here.
    for cycle in cycles
        .iter()
        .filter(|cycle| cycle.relation.exact_translation().is_none())
    {
        insert_guarded_relation(
            &mut reached,
            &mut queue,
            cycle.relation.clone(),
            cycle.condition.clone(),
            budget,
        );
    }
    while let Some((relation, condition)) = queue.pop_front() {
        for cycle in &cycles {
            if !budget.spend(1) {
                return false;
            }
            let Some(next_condition) = condition.conjoin_if_compatible(&cycle.condition) else {
                continue;
            };
            if !budget.spend_product(relation.piece_count(), cycle.relation.piece_count()) {
                return false;
            }
            let next_relation = relation.then(&cycle.relation);
            if next_relation.is_empty() {
                continue;
            }
            if next_relation.intersects_identity() {
                return true;
            }
            insert_guarded_relation(
                &mut reached,
                &mut queue,
                next_relation,
                next_condition,
                budget,
            );
        }
    }
    false
}

fn insert_guarded_relation(
    reached: &mut Vec<(PositionRelationSet, PathCondition)>,
    queue: &mut VecDeque<(PositionRelationSet, PathCondition)>,
    relation: PositionRelationSet,
    condition: PathCondition,
    budget: &mut SearchBudget,
) {
    if let Some(condition) = insert_cycle_state(
        reached,
        &relation,
        condition,
        PositionRelationSet::piecewise_covers,
        PositionRelationSet::piece_count,
        budget,
    ) {
        queue.push_back((relation, condition));
    }
}

#[derive(Clone, Debug)]
struct GuardedTranslation {
    dependency: BitDependency,
    condition: PathCondition,
    feasible: Vec<FeasiblePosition>,
}

fn displacements_have_common_strict_sign(offsets: impl Iterator<Item = (isize, isize)>) -> bool {
    let mut signs = [true; 4];
    for (array, packed) in offsets {
        signs[0] &= array > 0;
        signs[1] &= array < 0;
        signs[2] &= packed > 0;
        signs[3] &= packed < 0;
    }
    signs.into_iter().any(|sign| sign)
}

fn guarded_translations_cancel(cycles: &[GuardedTranslation], budget: &mut SearchBudget) -> bool {
    if !budget.spend(cycles.len().saturating_mul(4)) {
        return false;
    }
    // A common sign on either axis cannot sum to zero. This also avoids the
    // cubic cancellation prefilter for acyclic shift fanout at instance inputs.
    if displacements_have_common_strict_sign(
        cycles
            .iter()
            .map(|cycle| cycle.dependency.exact_offset().unwrap()),
    ) {
        return false;
    }
    // Look for a feasible opposing pair before constructing the transition
    // graph. Charge each comparison and composition as it is reached: a
    // simple witness must not pay for every possible pair and triple.
    // GCD-derived repetition counts also handle +1 repeated 999_999 times
    // followed by one -999_999 wrap without enumerating the declared width.
    let references = cycles.iter().collect::<Vec<_>>();
    if let Some(closes) = fixed_coordinate_pair_closes(&references, budget) {
        return closes;
    }
    if guarded_opposing_pair_closes(&references, budget) {
        return true;
    }
    let Some(components) = guarded_transition_components_that_can_cancel(cycles, budget) else {
        return false;
    };
    for cycles in components {
        if let Some(closes) = fixed_coordinate_pair_closes(&cycles, budget) {
            if closes {
                return true;
            }
            continue;
        }
        // Three non-collinear displacements can also cancel. Their repetition
        // counts and feasible endpoints do not depend on the declared width.
        if guarded_three_cycle_closes(&cycles, budget) {
            return true;
        }
        // The remaining irregular cases retain the exact cumulative
        // translation. A state is reusable only when its branch condition and
        // valid starting positions cover the new state as well.
        let mut reached: HashMap<BitDependency, Vec<(Vec<FeasiblePosition>, PathCondition)>> =
            HashMap::default();
        let mut queue = VecDeque::new();
        for cycle in &cycles {
            insert_guarded_walk(
                &mut reached,
                &mut queue,
                cycle.dependency,
                cycle.condition.clone(),
                cycle.feasible.clone(),
                budget,
            );
        }

        while let Some((dependency, condition, feasible)) = queue.pop_front() {
            for cycle in &cycles {
                if !budget.spend(1) {
                    return false;
                }
                let Some(next_condition) = condition.conjoin_if_compatible(&cycle.condition) else {
                    continue;
                };
                let offset = dependency
                    .exact_offset()
                    .expect("an exact guarded walk must retain its displacement");
                let Some(next_feasible) =
                    compose_feasible_positions(&feasible, offset, &cycle.feasible, budget)
                else {
                    return false;
                };
                if next_feasible.is_empty() {
                    continue;
                }
                let next_dependency = dependency.compose(cycle.dependency);
                if next_dependency == BitDependency::identity() {
                    return true;
                }
                insert_guarded_walk(
                    &mut reached,
                    &mut queue,
                    next_dependency,
                    next_condition,
                    next_feasible,
                    budget,
                );
            }
        }
    }
    false
}

/// If one translation can start only at one coordinate, every closed word
/// using it must return to that coordinate before using it again. With just
/// one other translation, the intervening run has a uniquely determined
/// length. Divisibility and the extrema of that run decide both feasibility
/// and infeasibility without enumerating the coordinate range. Require one
/// rectangular run guard: a union could admit steps in different rectangles.
fn fixed_coordinate_pair_closes(
    cycles: &[&GuardedTranslation],
    budget: &mut SearchBudget,
) -> Option<bool> {
    let [first, second] = cycles else {
        return None;
    };
    for (anchor, run) in [(first, second), (second, first)] {
        let [run_guard] = run.feasible.as_slice() else {
            continue;
        };
        let anchor_offset = anchor.dependency.exact_offset()?;
        let run_offset = run.dependency.exact_offset()?;
        if anchor_offset == (0, 0) || run_offset == (0, 0) {
            return None;
        }
        for packed in [false, true] {
            if !budget.spend(anchor.feasible.len().saturating_add(1)) {
                return None;
            }
            let coordinate =
                |guard: &FeasiblePosition| if packed { guard.packed } else { guard.array };
            let Some(fixed) = anchor.feasible.first().and_then(coordinate) else {
                continue;
            };
            if fixed.1 as i128 - fixed.0 as i128 != 1
                || !anchor
                    .feasible
                    .iter()
                    .all(|guard| coordinate(guard) == Some(fixed))
            {
                continue;
            }
            let (jump, step) = if packed {
                (anchor_offset.1 as i128, run_offset.1 as i128)
            } else {
                (anchor_offset.0 as i128, run_offset.0 as i128)
            };
            if step == 0 {
                continue;
            }
            if -jump % step != 0 || -jump / step <= 0 {
                return Some(false);
            }
            let count = -jump / step;
            if anchor_offset.0 as i128 + count * run_offset.0 as i128 != 0
                || anchor_offset.1 as i128 + count * run_offset.1 as i128 != 0
            {
                return Some(false);
            }
            if !budget.spend_conditions(&anchor.condition, &run.condition) {
                return None;
            }
            if anchor
                .condition
                .conjoin_if_compatible(&run.condition)
                .is_none()
            {
                return Some(false);
            }
            return Some(anchor.feasible.iter().any(|guard| {
                fixed_return_axis_is_feasible(
                    guard.array,
                    run_guard.array,
                    anchor_offset.0,
                    run_offset.0,
                    count,
                ) && fixed_return_axis_is_feasible(
                    guard.packed,
                    run_guard.packed,
                    anchor_offset.1,
                    run_offset.1,
                    count,
                )
            }));
        }
    }
    None
}

fn fixed_return_axis_is_feasible(
    anchor: Option<(isize, isize)>,
    run: Option<(isize, isize)>,
    jump: isize,
    step: isize,
    count: i128,
) -> bool {
    let Some((low, high)) = run else {
        return true;
    };
    let first = jump as i128;
    let last = first + (count - 1) * step as i128;
    let low = low as i128 - first.min(last);
    let high = high as i128 - first.max(last);
    let (anchor_low, anchor_high) = anchor.map_or((i128::MIN, i128::MAX), |(low, high)| {
        (low as i128, high as i128)
    });
    low.max(anchor_low) < high.min(anchor_high)
}

/// A closed word induces a directed cycle between the first-return relations
/// it uses: every relation must be able to hand its output position to the next
/// one. Its displacement vectors must therefore cancel inside one strongly
/// connected component of this coarse transition graph. Rejecting components
/// that cannot cancel avoids enumerating a declared width when opposing
/// translations are separated by a positional gap.
fn guarded_transition_components_that_can_cancel<'a>(
    cycles: &'a [GuardedTranslation],
    budget: &mut SearchBudget,
) -> Option<Vec<Vec<&'a GuardedTranslation>>> {
    if !budget.spend(cycles.len()) {
        return None;
    }
    let mut transitions = Graph::<usize, ()>::new();
    let nodes = (0..cycles.len())
        .map(|cycle| transitions.add_node(cycle))
        .collect::<Vec<_>>();
    for (left_index, left) in cycles.iter().enumerate() {
        let offset = left
            .dependency
            .exact_offset()
            .expect("guarded translations must retain exact offsets");
        for (right_index, right) in cycles.iter().enumerate() {
            if !budget.spend_conditions(&left.condition, &right.condition) {
                return None;
            }
            if left
                .condition
                .conjoin_if_compatible(&right.condition)
                .is_none()
                || compose_feasible_positions(&left.feasible, offset, &right.feasible, budget)?
                    .is_empty()
            {
                continue;
            }
            transitions.add_edge(nodes[left_index], nodes[right_index], ());
        }
    }

    if !budget.spend(
        transitions
            .node_count()
            .saturating_add(transitions.edge_count()),
    ) {
        return None;
    }
    let mut components = Vec::new();
    for component in kosaraju_scc(&transitions) {
        let cycles = component
            .into_iter()
            .map(|node| &cycles[transitions[node]])
            .collect::<Vec<_>>();
        let displacements = cycles
            .iter()
            .map(|cycle| (cycle.dependency, cycle.condition.clone()))
            .collect();
        if compatible_cycle_displacements_cancel(&displacements, budget) {
            components.push(cycles);
        } else if budget.exhausted {
            return None;
        }
    }
    Some(components)
}

fn guarded_opposing_pair_closes(cycles: &[&GuardedTranslation], budget: &mut SearchBudget) -> bool {
    for left in 0..cycles.len() {
        for right in (left + 1)..cycles.len() {
            if !budget.spend_conditions(&cycles[left].condition, &cycles[right].condition) {
                return false;
            }
            if cycles[left]
                .condition
                .conjoin_if_compatible(&cycles[right].condition)
                .is_none()
            {
                continue;
            }
            let (Some(left_offset), Some(right_offset)) = (
                cycles[left].dependency.exact_offset(),
                cycles[right].dependency.exact_offset(),
            ) else {
                continue;
            };
            let (Some(cross), Some(dot)) = (
                cross_product(left_offset, right_offset),
                dot_product(left_offset, right_offset),
            ) else {
                continue;
            };
            if cross != 0 || dot >= 0 {
                continue;
            }
            let Some((left_count, right_count)) =
                opposing_repetition_counts(left_offset, right_offset)
            else {
                continue;
            };
            let Some(left_walk) = repeat_guarded_cycle(cycles[left], left_count, budget) else {
                continue;
            };
            let Some(right_walk) = repeat_guarded_cycle(cycles[right], right_count, budget) else {
                continue;
            };
            debug_assert_eq!(left_walk.0.compose(right_walk.0), BitDependency::identity());
            if compose_guarded_walk(&left_walk, &right_walk, budget).is_some()
                || compose_guarded_walk(&right_walk, &left_walk, budget).is_some()
            {
                return true;
            }
        }
    }
    false
}

fn guarded_three_cycle_closes(cycles: &[&GuardedTranslation], budget: &mut SearchBudget) -> bool {
    const ORDERS: [[usize; 3]; 6] = [
        [0, 1, 2],
        [0, 2, 1],
        [1, 0, 2],
        [1, 2, 0],
        [2, 0, 1],
        [2, 1, 0],
    ];
    for first in 0..cycles.len() {
        for second in (first + 1)..cycles.len() {
            if !budget.spend_conditions(&cycles[first].condition, &cycles[second].condition) {
                return false;
            }
            let Some(condition) = cycles[first]
                .condition
                .conjoin_if_compatible(&cycles[second].condition)
            else {
                continue;
            };
            for third in (second + 1)..cycles.len() {
                if !budget.spend_conditions(&condition, &cycles[third].condition) {
                    return false;
                }
                if condition
                    .conjoin_if_compatible(&cycles[third].condition)
                    .is_none()
                {
                    continue;
                }
                let selected = [cycles[first], cycles[second], cycles[third]];
                let Some(offsets) = selected
                    .iter()
                    .map(|cycle| cycle.dependency.exact_offset())
                    .collect::<Option<Vec<_>>>()
                    .and_then(|offsets| <[(isize, isize); 3]>::try_from(offsets).ok())
                else {
                    continue;
                };
                let [Some(a), Some(b), Some(c)] = [
                    cross_product(offsets[1], offsets[2]),
                    cross_product(offsets[2], offsets[0]),
                    cross_product(offsets[0], offsets[1]),
                ] else {
                    continue;
                };
                let same_sign = [a, b, c].iter().all(|coefficient| *coefficient > 0)
                    || [a, b, c].iter().all(|coefficient| *coefficient < 0);
                if !same_sign {
                    continue;
                }
                let divisor = greatest_common_divisor(
                    greatest_common_divisor(a.unsigned_abs(), b.unsigned_abs()),
                    c.unsigned_abs(),
                );
                let counts = [
                    a.unsigned_abs() / divisor,
                    b.unsigned_abs() / divisor,
                    c.unsigned_abs() / divisor,
                ];
                let Some(walks) = selected
                    .iter()
                    .zip(counts)
                    .map(|(cycle, count)| repeat_guarded_cycle(cycle, count, budget))
                    .collect::<Option<Vec<_>>>()
                    .and_then(|walks| <[_; 3]>::try_from(walks).ok())
                else {
                    continue;
                };
                for order in ORDERS {
                    let Some(combined) =
                        compose_guarded_walk(&walks[order[0]], &walks[order[1]], budget)
                            .and_then(|walk| compose_guarded_walk(&walk, &walks[order[2]], budget))
                    else {
                        continue;
                    };
                    if combined.0 == BitDependency::identity() {
                        return true;
                    }
                }
            }
        }
    }
    false
}

fn compose_guarded_walk(
    left: &(BitDependency, Vec<FeasiblePosition>),
    right: &(BitDependency, Vec<FeasiblePosition>),
    budget: &mut SearchBudget,
) -> Option<(BitDependency, Vec<FeasiblePosition>)> {
    let feasible = compose_feasible_positions(&left.1, left.0.exact_offset()?, &right.1, budget)?;
    (!feasible.is_empty()).then_some((left.0.compose(right.0), feasible))
}

fn opposing_repetition_counts(
    left: (isize, isize),
    right: (isize, isize),
) -> Option<(usize, usize)> {
    let (left, right) = if left.0 != 0 {
        (left.0.unsigned_abs(), right.0.unsigned_abs())
    } else {
        (left.1.unsigned_abs(), right.1.unsigned_abs())
    };
    if left == 0 || right == 0 {
        return None;
    }
    let divisor = greatest_common_divisor(left, right);
    Some((right / divisor, left / divisor))
}

fn greatest_common_divisor(mut left: usize, mut right: usize) -> usize {
    while right != 0 {
        (left, right) = (right, left % right);
    }
    left
}

fn repeat_guarded_cycle(
    cycle: &GuardedTranslation,
    count: usize,
    budget: &mut SearchBudget,
) -> Option<(BitDependency, Vec<FeasiblePosition>)> {
    if !budget.spend_product(cycle.feasible.len(), 1) {
        return None;
    }
    let offset = cycle.dependency.exact_offset()?;
    let repetitions = count.checked_sub(1)?;
    let repetitions = isize::try_from(repetitions).ok()?;
    let count = isize::try_from(count).ok()?;
    let array_shift = offset.0.checked_mul(repetitions)?;
    let packed_shift = offset.1.checked_mul(repetitions)?;
    let mut feasible = cycle
        .feasible
        .iter()
        .filter_map(|position| {
            Some(FeasiblePosition {
                array: repeat_axis(position.array, array_shift)?,
                packed: repeat_axis(position.packed, packed_shift)?,
            })
        })
        .collect::<Vec<_>>();
    feasible.sort_unstable();
    feasible.dedup();
    if feasible.is_empty() {
        return None;
    }
    Some((
        BitDependency {
            array: Some(offset.0.checked_mul(count)?),
            packed: Some(offset.1.checked_mul(count)?),
        },
        feasible,
    ))
}

fn repeat_axis(
    range: Option<(isize, isize)>,
    total_shift: isize,
) -> Option<Option<(isize, isize)>> {
    let Some((start, end)) = range else {
        return Some(None);
    };
    let repeated = if total_shift >= 0 {
        (start, end.checked_sub(total_shift)?)
    } else {
        (start.checked_sub(total_shift)?, end)
    };
    (repeated.0 < repeated.1).then_some(Some(repeated))
}

fn insert_guarded_walk(
    reached: &mut HashMap<BitDependency, Vec<(Vec<FeasiblePosition>, PathCondition)>>,
    queue: &mut VecDeque<(BitDependency, PathCondition, Vec<FeasiblePosition>)>,
    dependency: BitDependency,
    condition: PathCondition,
    mut feasible: Vec<FeasiblePosition>,
    budget: &mut SearchBudget,
) {
    feasible.sort_unstable();
    feasible.dedup();
    if let Some(condition) = insert_cycle_state(
        reached.entry(dependency).or_default(),
        &feasible,
        condition,
        |outer, inner| feasible_positions_contain(outer, inner),
        Vec::len,
        budget,
    ) {
        queue.push_back((dependency, condition, feasible));
    }
}

fn compose_feasible_positions(
    current: &[FeasiblePosition],
    current_offset: (isize, isize),
    next: &[FeasiblePosition],
    budget: &mut SearchBudget,
) -> Option<Vec<FeasiblePosition>> {
    if !budget.spend_product(current.len(), next.len()) {
        return None;
    }
    let mut result = Vec::new();
    for &current in current {
        for &next in next {
            let next_array = translate_axis_to_initial(next.array, current_offset.0);
            let next_packed = translate_axis_to_initial(next.packed, current_offset.1);
            let Some(array) = intersect_axis(current.array, next_array) else {
                continue;
            };
            let Some(packed) = intersect_axis(current.packed, next_packed) else {
                continue;
            };
            result.push(FeasiblePosition { array, packed });
        }
    }
    result.sort_unstable();
    result.dedup();
    Some(result)
}

fn translate_axis_to_initial(
    range: Option<(isize, isize)>,
    offset: isize,
) -> Option<(isize, isize)> {
    range.map(|(start, end)| {
        (
            start
                .checked_sub(offset)
                .expect("translated guard start must fit in isize"),
            end.checked_sub(offset)
                .expect("translated guard end must fit in isize"),
        )
    })
}

fn feasible_positions_contain(outer: &[FeasiblePosition], inner: &[FeasiblePosition]) -> bool {
    inner.iter().all(|inner| {
        outer.iter().any(|outer| {
            axis_contains(outer.array, inner.array) && axis_contains(outer.packed, inner.packed)
        })
    })
}

fn axis_contains(outer: Option<(isize, isize)>, inner: Option<(isize, isize)>) -> bool {
    match (outer, inner) {
        (None, _) => true,
        (Some(_), None) => false,
        (Some(outer), Some(inner)) => outer.0 <= inner.0 && inner.1 <= outer.1,
    }
}

pub(super) fn compatible_cycle_displacements_cancel(
    cycles: &HashSet<(BitDependency, PathCondition)>,
    budget: &mut SearchBudget,
) -> bool {
    if !budget.spend(cycles.len().saturating_mul(4)) {
        return false;
    }
    // A closed walk is a non-negative combination of its coarse cycles. In
    // two positional dimensions, a zero displacement needs at most three
    // cycle vectors. Keep the associated path conditions so mutually
    // exclusive cycles are never combined.
    let exact: Vec<_> = cycles
        .iter()
        .filter_map(|(dependency, condition)| {
            dependency.exact_offset().map(|offset| (offset, condition))
        })
        .collect();

    // A transition component can have a common sign even when the full set
    // did not, for example when opposite shifts occur in exclusive arms.
    if displacements_have_common_strict_sign(exact.iter().map(|(offset, _)| *offset)) {
        return false;
    }

    for left in 0..exact.len() {
        for right in (left + 1)..exact.len() {
            if !budget.spend_conditions(exact[left].1, exact[right].1) {
                return false;
            }
            let Some(condition) = exact[left].1.conjoin_if_compatible(exact[right].1) else {
                continue;
            };
            if opposite_collinear(exact[left].0, exact[right].0) {
                return true;
            }
            for third in (right + 1)..exact.len() {
                if !budget.spend_conditions(&condition, exact[third].1) {
                    return false;
                }
                if condition.conjoin_if_compatible(exact[third].1).is_some()
                    && origin_is_in_positive_cone(exact[left].0, exact[right].0, exact[third].0)
                {
                    return true;
                }
            }
        }
    }
    false
}

fn opposite_collinear(left: (isize, isize), right: (isize, isize)) -> bool {
    let Some(cross) = cross_product(left, right) else {
        return true;
    };
    let Some(dot) = dot_product(left, right) else {
        return true;
    };
    cross == 0 && dot < 0
}

fn origin_is_in_positive_cone(a: (isize, isize), b: (isize, isize), c: (isize, isize)) -> bool {
    let [Some(first), Some(second), Some(third)] = [
        cross_product(b, c),
        cross_product(c, a),
        cross_product(a, b),
    ] else {
        return true;
    };
    let coefficients = [first, second, third];
    let has_positive = coefficients.iter().any(|&coefficient| coefficient > 0);
    let has_negative = coefficients.iter().any(|&coefficient| coefficient < 0);
    (has_positive || has_negative) && !(has_positive && has_negative)
}

fn cross_product(left: (isize, isize), right: (isize, isize)) -> Option<isize> {
    left.0
        .checked_mul(right.1)?
        .checked_sub(left.1.checked_mul(right.0)?)
}

fn dot_product(left: (isize, isize), right: (isize, isize)) -> Option<isize> {
    left.0
        .checked_mul(right.0)?
        .checked_add(left.1.checked_mul(right.1)?)
}

#[cfg(test)]
mod fixed_return_tests {
    use super::*;
    use crate::comb_loop_detect::ssa::BranchId;
    use daggy::petgraph::algo::is_cyclic_directed;

    #[test]
    fn finite_closed_domains_prove_rotations_without_enumerating_coordinates() {
        for width in [64, 256, 1_000_003] {
            let mut cycles = vec![
                GuardedTranslation {
                    dependency: BitDependency {
                        array: Some(3),
                        packed: Some(0),
                    },
                    condition: PathCondition::default(),
                    feasible: vec![FeasiblePosition {
                        array: Some((0, width - 3)),
                        packed: Some((0, 1)),
                    }],
                },
                GuardedTranslation {
                    dependency: BitDependency {
                        array: Some(3 - width),
                        packed: Some(0),
                    },
                    condition: PathCondition::default(),
                    feasible: vec![FeasiblePosition {
                        array: Some((width - 3, width)),
                        packed: Some((0, 1)),
                    }],
                },
            ];
            let mut budget = SearchBudget {
                remaining: 100,
                exhausted: false,
            };
            assert!(closed_translation_domain(&cycles, &mut budget));
            assert!(!budget.exhausted);

            let branch = BranchId::new(1, 0, 2);
            cycles[0].condition = PathCondition::default().with_choice(branch, 0);
            cycles[1].condition = PathCondition::default().with_choice(branch, 1);
            assert!(!closed_translation_domain(
                &cycles,
                &mut SearchBudget::new()
            ));
            cycles[0].condition = PathCondition::default();
            cycles[1].condition = PathCondition::default();

            // A missing source point breaks the invariant: its incoming
            // image is not a successor state. A bounding box is insufficient.
            cycles[0].feasible[0].array = Some((0, width - 4));
            assert!(!closed_translation_domain(
                &cycles,
                &mut SearchBudget::new()
            ));
            cycles[0].feasible[0].array = None;
            assert!(!closed_translation_domain(
                &cycles,
                &mut SearchBudget::new()
            ));
        }
    }

    #[test]
    fn coalescing_return_domains_preserves_gaps_and_corners() {
        let mut seed = 37u64;
        let mut next = || {
            seed = seed.wrapping_mul(6364136223846793005).wrapping_add(1);
            ((seed >> 32) % 8) as isize
        };
        for count in 1..128 {
            let mut domains = Vec::new();
            for index in 0..count {
                let array = next();
                let packed = next();
                domains.push(FeasiblePosition {
                    array: (index % 13 != 12).then_some((array, array + 1 + next() % 3)),
                    packed: (index % 17 != 16).then_some((packed, packed + 1 + next() % 3)),
                });
            }
            let original = domains.clone();
            coalesce_feasible_positions(&mut domains);
            for array in -1..12 {
                for packed in -1..12 {
                    let contains = |domains: &[FeasiblePosition]| {
                        domains.iter().any(|domain| {
                            domain
                                .array
                                .is_none_or(|(lo, hi)| lo <= array && array < hi)
                                && domain
                                    .packed
                                    .is_none_or(|(lo, hi)| lo <= packed && packed < hi)
                        })
                    };
                    assert_eq!(
                        contains(&domains),
                        contains(&original),
                        "count={count}, point=({array}, {packed})"
                    );
                }
            }
        }
    }

    // Independent reference: enumerate coordinates in the small guards and
    // detect an ordinary graph cycle for each complete branch valuation.
    fn expanded_cycle(cycles: &[GuardedTranslation], branch: BranchId) -> bool {
        for arm in 0..2 {
            let choices = PathCondition::default().with_choice(branch, arm);
            let mut graph = Graph::<(), ()>::new();
            let mut nodes = HashMap::default();
            for cycle in cycles {
                if cycle.condition.conjoin_if_compatible(&choices).is_none() {
                    continue;
                }
                let (da, dp) = cycle.dependency.exact_offset().unwrap();
                for array in -4..=4 {
                    for packed in -4..=4 {
                        if !cycle.feasible.iter().any(|guard| {
                            guard
                                .array
                                .is_none_or(|(low, high)| low <= array && array < high)
                                && guard
                                    .packed
                                    .is_none_or(|(low, high)| low <= packed && packed < high)
                        }) {
                            continue;
                        }
                        let source = *nodes
                            .entry((array, packed))
                            .or_insert_with(|| graph.add_node(()));
                        let destination = *nodes
                            .entry((array + da, packed + dp))
                            .or_insert_with(|| graph.add_node(()));
                        graph.add_edge(source, destination, ());
                    }
                }
            }
            if is_cyclic_directed(&graph) {
                return true;
            }
        }
        false
    }

    #[test]
    fn fixed_coordinate_pairs_match_expanded_guarded_coordinates() {
        let branch = BranchId::new(0, 0, 2);
        let mut state = 193u32;
        let mut random = || {
            state = state.wrapping_mul(1_664_525).wrapping_add(1_013_904_223);
            (state >> 16) as usize
        };
        let mut decided = 0;
        let mut positive = 0;
        for case in 0..512 {
            let step = [
                (0, 1),
                (0, -1),
                (1, 0),
                (-1, 0),
                (1, 1),
                (1, -1),
                (-1, 1),
                (-1, -1),
            ][random() % 8];
            let count = 1 + random() as isize % 3;
            let mut jump = (-step.0 * count, -step.1 * count);
            if case % 4 == 0 {
                jump.1 += 1;
            }
            if jump == (0, 0) {
                jump.1 = 2;
            }
            let fixed = random() as isize % 5 - 2;
            let mut guard = FeasiblePosition {
                array: Some((-3, 4)),
                packed: Some((-3, 4)),
            };
            if step.1 == 0 || step.0 != 0 && case % 2 == 0 {
                guard.array = Some((fixed, fixed + 1));
            } else {
                guard.packed = Some((fixed, fixed + 1));
            }
            let mut feasible = vec![guard];
            if case % 3 == 0 {
                let mut second = guard;
                if guard.array == Some((fixed, fixed + 1)) {
                    feasible[0].packed = Some((-3, -1));
                    second.packed = Some((1, 4));
                } else {
                    feasible[0].array = Some((-3, -1));
                    second.array = Some((1, 4));
                }
                feasible.push(second);
            }
            let run_guard = if case % 5 == 0 {
                FeasiblePosition {
                    array: Some((-1, 2)),
                    packed: Some((-1, 2)),
                }
            } else {
                FeasiblePosition {
                    array: Some((-4, 5)),
                    packed: Some((-4, 5)),
                }
            };
            let cycles = [
                GuardedTranslation {
                    dependency: BitDependency {
                        array: Some(jump.0),
                        packed: Some(jump.1),
                    },
                    condition: PathCondition::default().with_choice(branch, case % 2),
                    feasible,
                },
                GuardedTranslation {
                    dependency: BitDependency {
                        array: Some(step.0),
                        packed: Some(step.1),
                    },
                    condition: if case % 7 == 0 {
                        PathCondition::default().with_choice(branch, 1 - case % 2)
                    } else {
                        PathCondition::default()
                    },
                    feasible: vec![run_guard],
                },
            ];
            if let Some(actual) = fixed_coordinate_pair_closes(
                &cycles.iter().collect::<Vec<_>>(),
                &mut SearchBudget::new(),
            ) {
                let expected = expanded_cycle(&cycles, branch);
                assert_eq!(actual, expected, "case={case}, cycles={cycles:?}");
                decided += 1;
                positive += usize::from(actual);
            }
        }
        assert_eq!(decided, 512);
        assert!(positive > 50);
    }

    #[test]
    fn fixed_return_counts_can_exceed_isize_without_overflow() {
        let cycles = [
            GuardedTranslation {
                dependency: BitDependency {
                    array: Some(0),
                    packed: Some(isize::MIN),
                },
                condition: PathCondition::default(),
                feasible: vec![FeasiblePosition {
                    array: Some((0, 1)),
                    packed: Some((0, 1)),
                }],
            },
            GuardedTranslation {
                dependency: BitDependency {
                    array: Some(0),
                    packed: Some(1),
                },
                condition: PathCondition::default(),
                feasible: vec![FeasiblePosition {
                    array: Some((0, 1)),
                    packed: Some((isize::MIN, 0)),
                }],
            },
        ];
        assert_eq!(
            fixed_coordinate_pair_closes(
                &cycles.iter().collect::<Vec<_>>(),
                &mut SearchBudget::new()
            ),
            Some(true)
        );
        let mut clipped = cycles.clone();
        clipped[1].feasible[0].packed = Some((isize::MIN + 1, 0));
        assert_eq!(
            fixed_coordinate_pair_closes(
                &clipped.iter().collect::<Vec<_>>(),
                &mut SearchBudget::new()
            ),
            Some(false)
        );
    }

    #[test]
    fn split_run_guards_require_the_general_solver() {
        let branch = BranchId::new(0, 0, 2);
        let translation = |packed, ranges: &[(isize, isize)]| GuardedTranslation {
            dependency: BitDependency {
                array: Some(0),
                packed: Some(packed),
            },
            condition: PathCondition::default(),
            feasible: ranges
                .iter()
                .map(|&packed| FeasiblePosition {
                    array: Some((0, 1)),
                    packed: Some(packed),
                })
                .collect(),
        };
        let cycles = [
            translation(-2, &[(2, 3)]),
            translation(1, &[(0, 1), (1, 2)]),
        ];
        assert_eq!(
            fixed_coordinate_pair_closes(
                &cycles.iter().collect::<Vec<_>>(),
                &mut SearchBudget::new()
            ),
            None
        );
        assert!(expanded_cycle(&cycles, branch));
        assert!(guarded_translations_cancel(
            &cycles,
            &mut SearchBudget::new()
        ));
    }
}