selen 0.15.5

mod abs;
mod add;
mod alldiff;
mod allequal;
pub mod between;
mod bool_logic;
pub mod cardinality;
pub mod conditional;
mod count;
mod div;
mod element;
mod eq;
mod leq;
mod linear;
mod max;
mod min;
mod modulo;
mod mul;
mod neq;
mod noop;
mod reification;
mod sum;
mod table;

use std::ops::{Index, IndexMut};
use std::rc::Rc;

use crate::{
    variables::VarId,
    variables::views::{Context, View, ViewExt},
};

// Type aliases for cleaner Rc-based sharing
type PropagatorBox = Box<dyn Prune>;
type SharedPropagator = Rc<PropagatorBox>;

/// Enforce a specific constraint by pruning domain of decision variables.
///
/// The `Any` supertrait allows downcasting to concrete propagator types,
/// which is used for LP solver integration (extracting linear constraints).
pub trait Prune: core::fmt::Debug + std::any::Any {
    /// Perform pruning based on variable domains and internal state.
    fn prune(&self, ctx: &mut Context) -> Option<()>;
}

/// Isolate methods that prevent propagator from being used as a trait-object.
pub trait Propagate: Prune + 'static {
    /// List variables that schedule the propagator when their domain changes.
    fn list_trigger_vars(&self) -> impl Iterator<Item = VarId>;
}

/// Store internal state for each propagators, along with dependencies for when to schedule each.
#[doc(hidden)]
#[derive(Clone, Debug, Default)]
pub struct Propagators {
    state: Vec<SharedPropagator>,
    dependencies: Vec<Vec<PropId>>,
    /// Counter for the number of propagation steps performed
    propagation_count: usize,
    /// Counter for the number of search nodes (branching points) explored
    node_count: usize,
    /// Constraint metadata registry for optimization introspection
    constraint_registry: crate::optimization::constraint_metadata::ConstraintRegistry,
}

#[doc(hidden)]
impl Propagators {
    /// Extend dependencies matrix with a row for the new decision variable.
    pub fn on_new_var(&mut self) {
        self.dependencies.push(Vec::new());
    }

    /// List ids of all registered propagators.
    pub fn get_prop_ids_iter(&self) -> impl Iterator<Item = PropId> {
        (0..self.state.len()).map(PropId)
    }

    /// Acquire immutable reference to propagator state (for constraint analysis).
    pub fn get_state(&self, p: PropId) -> &SharedPropagator {
        &self.state[p.0]
    }

    /// Get list of propagators that should be scheduled when a bound of variable `v` changes.
    pub fn on_bound_change(&self, v: VarId) -> impl Iterator<Item = PropId> + '_ {
        self.dependencies[v].iter().copied()
    }

    /// Get the number of propagation steps performed so far.
    pub fn get_propagation_count(&self) -> usize {
        self.propagation_count
    }

    /// Increment the propagation step counter.
    pub fn increment_propagation_count(&mut self) {
        self.propagation_count += 1;
    }

    /// Get the number of search nodes explored so far.
    pub fn get_node_count(&self) -> usize {
        self.node_count
    }

    /// Increment the search node counter.
    pub fn increment_node_count(&mut self) {
        self.node_count += 1;
    }

    /// Get the number of propagators in this collection.
    pub fn count(&self) -> usize {
        self.state.len()
    }

    /// Get access to the constraint metadata registry
    pub fn get_constraint_registry(
        &self,
    ) -> &crate::optimization::constraint_metadata::ConstraintRegistry {
        &self.constraint_registry
    }

    /// Get mutable access to the constraint metadata registry
    pub fn get_constraint_registry_mut(
        &mut self,
    ) -> &mut crate::optimization::constraint_metadata::ConstraintRegistry {
        &mut self.constraint_registry
    }

    /// Extract linear constraints from propagators for LP solving.
    ///
    /// Scans all propagators and extracts FloatLinEq and FloatLinLe constraints
    /// into a LinearConstraintSystem that can be passed to the LP solver.
    ///
    /// # Returns
    /// A `LinearConstraintSystem` containing all linear constraints found in the model.
    ///
    /// # Example
    /// ```ignore
    /// // After creating a model with linear constraints
    /// let linear_system = model.propagators().extract_linear_system();
    /// if linear_system.is_suitable_for_lp() {
    ///     let lp_problem = linear_system.to_lp_problem(&model.vars());
    ///     // Solve with LP solver...
    /// }
    /// ```
    pub fn extract_linear_system(&self) -> crate::lpsolver::LinearConstraintSystem {
        use crate::lpsolver::{LinearConstraint, LinearConstraintSystem};
        use crate::variables::VarId;
        use std::collections::HashMap;

        let mut system = LinearConstraintSystem::new();

        // Phase 1: Build map of derived variables to their linear expressions
        // e.g., sum = x + y  stores  sum -> ([(x, 1.0), (y, 1.0)], 0.0)
        let mut derived_vars: HashMap<VarId, (Vec<(VarId, f64)>, f64)> = HashMap::new();

        // Phase 1: Extract direct constraints and build derived variable map
        for prop_rc in &self.state {
            let prop_box: &Box<dyn Prune> = prop_rc.as_ref();
            let prop_ref: &dyn Prune = prop_box.as_ref();

            if let Some(eq) = (prop_ref as &dyn std::any::Any).downcast_ref::<linear::FloatLinEq>()
            {
                // Direct linear equality constraint
                let constraint = LinearConstraint::equality(
                    eq.coefficients().to_vec(),
                    eq.variables().to_vec(),
                    eq.constant(),
                );
                system.add_constraint(constraint);
            } else if let Some(le) =
                (prop_ref as &dyn std::any::Any).downcast_ref::<linear::FloatLinLe>()
            {
                // Direct linear inequality constraint
                let constraint = LinearConstraint::less_or_equal(
                    le.coefficients().to_vec(),
                    le.variables().to_vec(),
                    le.constant(),
                );
                system.add_constraint(constraint);
            } else if let Some(add) =
                (prop_ref as &dyn std::any::Any).downcast_ref::<add::Add<VarId, VarId>>()
            {
                // Add: x + y = s (derived variable definition)
                // Store: s -> ([(x, 1.0), (y, 1.0)], 0.0)
                let x = *add.x();
                let y = *add.y();
                let s = add.s();
                // Debug: eprintln!("LP EXTRACTION: Found Add constraint: {:?} + {:?} = {:?}", x, y, s);
                derived_vars.insert(s, (vec![(x, 1.0), (y, 1.0)], 0.0));

                // Also add as linear equality for LP: x + y - s = 0
                let constraint =
                    LinearConstraint::equality(vec![1.0, 1.0, -1.0], vec![x, y, s], 0.0);
                system.add_constraint(constraint);
            }
        }

        // Phase 2: Extract LessThanOrEquals constraints: x <= y becomes x - y <= 0
        // The LP solver will handle variable bounds from domains automatically
        for prop_rc in &self.state {
            let prop_box: &Box<dyn Prune> = prop_rc.as_ref();
            let prop_ref: &dyn Prune = prop_box.as_ref();

            if let Some(leq) = (prop_ref as &dyn std::any::Any)
                .downcast_ref::<leq::LessThanOrEquals<VarId, VarId>>()
            {
                let x_var = *leq.x();
                let y_var = *leq.y();

                // Debug: eprintln!("LP EXTRACTION: Found LessThanOrEquals constraint: {:?} <= {:?}", x_var, y_var);

                // x <= y  →  x - y <= 0  →  1.0*x + (-1.0)*y <= 0
                let constraint =
                    LinearConstraint::less_or_equal(vec![1.0, -1.0], vec![x_var, y_var], 0.0);
                system.add_constraint(constraint);
            }
        }

        system
    }

    /// Optimize the order of AllDifferent constraints using multiple universal heuristics.
    ///
    /// Uses a combination of three heuristics to determine priority:
    /// 1. Domain tightness: Constraints with smaller average domain sizes (closer to failure)
    /// 2. Variable connectivity: Constraints affecting variables with higher connectivity
    /// 3. Constraint saturation: Constraints with higher ratio of fixed variables
    ///
    /// This approach is universal and works for any constraint satisfaction problem.
    pub fn optimize_alldiff_order(&mut self, vars: &crate::variables::Vars) {
        use crate::optimization::constraint_metadata::ConstraintType;

        // Get all AllDifferent constraints from the registry
        let alldiff_constraint_ids = self
            .constraint_registry
            .get_constraints_by_type(&ConstraintType::AllDifferent);

        if alldiff_constraint_ids.len() <= 1 {
            return; // Nothing to optimize with 0 or 1 AllDifferent constraints
        }

        // Pre-calculate variable connectivity map
        let variable_connectivity = self.calculate_variable_connectivity_map();

        // Create a vector of (prop_id, priority_scores) for AllDifferent constraints only
        let mut alldiff_priorities: Vec<(usize, (f64, f64, f64))> = Vec::new();

        for constraint_id in alldiff_constraint_ids {
            if let Some(metadata) = self.constraint_registry.get_constraint(constraint_id) {
                // Extract variables from this AllDifferent constraint
                let constraint_vars = match &metadata.data {
                    crate::optimization::constraint_metadata::ConstraintData::NAry { operands } => {
                        operands
                            .iter()
                            .filter_map(|op| match op {
                                crate::optimization::constraint_metadata::ViewInfo::Variable {
                                    var_id,
                                } => Some(*var_id),
                                _ => None,
                            })
                            .collect::<Vec<_>>()
                    }
                    _ => continue, // Skip non-NAry constraints
                };

                // Calculate domain tightness score (smaller average domain = higher priority)
                let tightness_score = self.calculate_domain_tightness(&constraint_vars, vars);

                // Calculate variable connectivity score (higher connectivity = higher priority)
                let connectivity_score =
                    self.calculate_variable_connectivity(&constraint_vars, &variable_connectivity);

                // Calculate constraint saturation score (higher fixed ratio = higher priority)
                let saturation_score = self.calculate_constraint_saturation(&constraint_vars, vars);

                // Map constraint_id to propagator index
                let prop_index = constraint_id.0;
                if prop_index < self.state.len() {
                    alldiff_priorities.push((
                        prop_index,
                        (tightness_score, connectivity_score, saturation_score),
                    ));
                }
            }
        }

        if alldiff_priorities.is_empty() {
            return; // No AllDifferent constraints found
        }

        // Sort AllDifferent constraints by priority (lexicographic ordering):
        // Primary: domain tightness (ascending - smaller domains = higher priority)
        // Secondary: constraint saturation (descending - higher fixed ratio = higher priority)
        // Tertiary: variable connectivity (descending - higher connectivity = higher priority)
        alldiff_priorities.sort_by(|a, b| {
            // First compare by domain tightness (ascending)
            let tightness_cmp =
                a.1.0
                    .partial_cmp(&b.1.0)
                    .unwrap_or(std::cmp::Ordering::Equal);
            if tightness_cmp != std::cmp::Ordering::Equal {
                return tightness_cmp;
            }
            // Then by constraint saturation (descending)
            let saturation_cmp =
                b.1.2
                    .partial_cmp(&a.1.2)
                    .unwrap_or(std::cmp::Ordering::Equal);
            if saturation_cmp != std::cmp::Ordering::Equal {
                return saturation_cmp;
            }
            // Finally by variable connectivity (descending)
            b.1.1
                .partial_cmp(&a.1.1)
                .unwrap_or(std::cmp::Ordering::Equal)
        });

        // Check if reordering would actually change anything
        let mut needs_reordering = false;
        for (i, &(prop_idx, _)) in alldiff_priorities.iter().enumerate() {
            if i < alldiff_priorities.len() - 1 {
                let next_prop_idx = alldiff_priorities[i + 1].0;
                if prop_idx > next_prop_idx {
                    needs_reordering = true;
                    break;
                }
            }
        }

        if !needs_reordering {
            return; // Already in optimal order
        }

        // Create new ordered vectors for reordering
        let original_state = self.state.clone();
        let original_dependencies = self.dependencies.clone();

        // Extract AllDifferent constraint indices for reordering
        let alldiff_indices: std::collections::HashSet<usize> =
            alldiff_priorities.iter().map(|&(idx, _)| idx).collect();

        // Build the new state with AllDifferent constraints in optimized order
        self.state.clear();
        let mut index_mapping = vec![0; original_state.len()];
        let mut new_idx = 0;

        // First, add AllDifferent constraints in priority order
        for &(old_idx, _) in &alldiff_priorities {
            if old_idx < original_state.len() {
                self.state.push(original_state[old_idx].clone());
                index_mapping[old_idx] = new_idx;
                new_idx += 1;
            }
        }

        // Then, add all non-AllDifferent constraints in their original order
        for (old_idx, constraint) in original_state.iter().enumerate() {
            if !alldiff_indices.contains(&old_idx) {
                self.state.push(constraint.clone());
                index_mapping[old_idx] = new_idx;
                new_idx += 1;
            }
        }

        // Update dependency mapping with new indices
        self.dependencies = vec![Vec::new(); original_dependencies.len()];
        for (var_id, deps) in original_dependencies.into_iter().enumerate() {
            for old_prop_id in deps {
                if old_prop_id.0 < index_mapping.len() {
                    let new_prop_id = PropId(index_mapping[old_prop_id.0]);
                    self.dependencies[var_id].push(new_prop_id);
                }
            }
        }
    }


    /// Calculate domain tightness score for a constraint.
    /// Lower scores indicate tighter constraints (smaller domains) which should be prioritized.
    fn calculate_domain_tightness(
        &self,
        constraint_vars: &[VarId],
        vars: &crate::variables::Vars,
    ) -> f64 {
        if constraint_vars.is_empty() {
            return f64::INFINITY; // Invalid constraint, lowest priority
        }

        let total_domain_size: f64 = constraint_vars
            .iter()
            .map(|&var_id| self.calculate_variable_domain_size(var_id, vars))
            .sum();

        // Return average domain size (smaller = tighter = higher priority)
        total_domain_size / (constraint_vars.len() as f64)
    }

    /// Calculate the effective domain size for a variable.
    /// For integer variables, this is the actual domain size.
    /// For float variables, this estimates discrete steps within the interval.
    fn calculate_variable_domain_size(&self, var_id: VarId, vars: &crate::variables::Vars) -> f64 {
        match &vars[var_id] {
            crate::variables::Var::VarI(sparse_set) => sparse_set.size() as f64,
            crate::variables::Var::VarF(interval) => {
                // For float variables, estimate the number of discrete steps
                let range = interval.max - interval.min;
                if range <= 0.0 {
                    return 1.0; // Single value
                }

                // Estimate discrete domain size based on step size
                let estimated_steps = (range / interval.step).ceil();
                estimated_steps.max(1.0) // At least 1 step
            }
        }
    }

    /// Calculate variable connectivity map - how many constraints each variable participates in.
    /// This builds a connectivity graph to understand variable importance in the constraint network.
    fn calculate_variable_connectivity_map(&self) -> std::collections::HashMap<VarId, usize> {
        let mut connectivity_map = std::collections::HashMap::new();

        // Since we don't have direct access to all constraints, we'll iterate through
        // all constraint types and collect their constraint IDs
        use crate::optimization::constraint_metadata::ConstraintType;

        let constraint_types = [
            ConstraintType::AllDifferent,
            ConstraintType::Addition,
            ConstraintType::Multiplication,
            ConstraintType::Modulo,
            ConstraintType::Division,
            ConstraintType::AbsoluteValue,
            ConstraintType::Minimum,
            ConstraintType::Maximum,
            ConstraintType::Sum,
            ConstraintType::Equals,
            ConstraintType::NotEquals,
            ConstraintType::LessThanOrEquals,
            ConstraintType::LessThan,
            ConstraintType::GreaterThanOrEquals,
            ConstraintType::GreaterThan,
            ConstraintType::BooleanAnd,
            ConstraintType::BooleanOr,
            ConstraintType::BooleanNot,
        ];

        // Iterate through all constraint types to count variable participation
        for constraint_type in &constraint_types {
            for constraint_id in self
                .constraint_registry
                .get_constraints_by_type(constraint_type)
            {
                if let Some(metadata) = self.constraint_registry.get_constraint(constraint_id) {
                    // Extract variables from this constraint and increment their connectivity
                    for var_id in &metadata.variables {
                        *connectivity_map.entry(*var_id).or_insert(0) += 1;
                    }
                }
            }
        }

        connectivity_map
    }

    /// Calculate average variable connectivity for a constraint.
    /// Higher connectivity indicates variables that are more constrained and likely to propagate.
    fn calculate_variable_connectivity(
        &self,
        constraint_vars: &[VarId],
        connectivity_map: &std::collections::HashMap<VarId, usize>,
    ) -> f64 {
        if constraint_vars.is_empty() {
            return 0.0; // No variables, lowest connectivity
        }

        let total_connectivity: usize = constraint_vars
            .iter()
            .map(|var_id| connectivity_map.get(var_id).copied().unwrap_or(0))
            .sum();

        // Return average connectivity (higher = more constrained = higher priority)
        total_connectivity as f64 / constraint_vars.len() as f64
    }

    /// Calculate constraint saturation score - ratio of fixed variables to total variables.
    /// Higher saturation indicates constraints closer to completion and likely to propagate effectively.
    fn calculate_constraint_saturation(
        &self,
        constraint_vars: &[VarId],
        vars: &crate::variables::Vars,
    ) -> f64 {
        if constraint_vars.is_empty() {
            return 0.0; // No variables, lowest saturation
        }

        let fixed_variables = constraint_vars
            .iter()
            .filter(|&&var_id| {
                match &vars[var_id] {
                    crate::variables::Var::VarI(sparse_set) => sparse_set.size() == 1,
                    crate::variables::Var::VarF(interval) => {
                        // For float variables, consider fixed if the range is very small
                        let range = interval.max - interval.min;
                        range <= interval.step
                    }
                }
            })
            .count();

        // Return saturation ratio (higher = more fixed = higher priority)
        fixed_variables as f64 / constraint_vars.len() as f64
    }

    /// Declare a new propagator to enforce `x + y == s`.
    pub fn add(&mut self, x: impl View, y: impl View, s: VarId) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let x_info = self.analyze_view(&x);
        let y_info = self.analyze_view(&y);
        let s_info = ViewInfo::Variable { var_id: s };

        let variables: Vec<_> = x
            .get_underlying_var()
            .into_iter()
            .chain(y.get_underlying_var())
            .chain(std::iter::once(s))
            .collect();

        let metadata = ConstraintData::NAry {
            operands: vec![x_info, y_info, s_info],
        };

        self.push_new_prop_with_metadata(
            self::add::Add::new(x, y, s),
            ConstraintType::Addition,
            variables,
            metadata,
        )
    }

    /// Declare a new propagator to enforce `x - y == s`.
    /// This reuses the Add propagator by transforming to `x + (-y) == s`.
    pub fn sub(&mut self, x: impl View, y: impl View, s: VarId) -> PropId {
        use crate::variables::Val;
        // x - y = s  =>  x + (-y) = s
        self.add(x, y.times_neg(Val::ValI(-1)), s)
    }

    /// Declare a new propagator to enforce `x * y == s`.
    pub fn mul(&mut self, x: impl View, y: impl View, s: VarId) -> PropId {
        use crate::optimization::constraint_metadata::{
            ConstraintData, ConstraintType, ConstraintValue, ViewInfo,
        };

        // Special handling for TypedConstant detection
        fn analyze_view_for_constants<T: View>(view: &T) -> ViewInfo {
            if let Some(var_id) = view.get_underlying_var() {
                ViewInfo::Variable { var_id }
            } else {
                // This view has no underlying variable - it might be a constant
                // For TypedConstant, we can detect this by checking min == max
                // Since both are the constant value
                let min_val = view.min_raw(&crate::variables::Vars::default());
                let max_val = view.max_raw(&crate::variables::Vars::default());

                if min_val == max_val {
                    // This is likely a constant value
                    let const_val = match min_val {
                        crate::variables::Val::ValI(i) => ConstraintValue::Integer(i),
                        crate::variables::Val::ValF(f) => ConstraintValue::Float(f),
                    };
                    ViewInfo::Constant { value: const_val }
                } else {
                    ViewInfo::Complex
                }
            }
        }

        let x_info = analyze_view_for_constants(&x);
        let y_info = analyze_view_for_constants(&y);
        let s_info = ViewInfo::Variable { var_id: s };

        let variables: Vec<_> = x
            .get_underlying_var()
            .into_iter()
            .chain(y.get_underlying_var())
            .chain(std::iter::once(s))
            .collect();

        let metadata = ConstraintData::NAry {
            operands: vec![x_info, y_info, s_info],
        };

        self.push_new_prop_with_metadata(
            self::mul::Mul::new(x, y, s),
            ConstraintType::Multiplication,
            variables,
            metadata,
        )
    }

    /// Declare a new propagator to enforce `x % y == s`.
    pub fn modulo(&mut self, x: impl View, y: impl View, s: VarId) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let x_info = self.analyze_view(&x);
        let y_info = self.analyze_view(&y);
        let s_info = ViewInfo::Variable { var_id: s };

        let variables: Vec<_> = x
            .get_underlying_var()
            .into_iter()
            .chain(y.get_underlying_var())
            .chain(std::iter::once(s))
            .collect();

        let metadata = ConstraintData::NAry {
            operands: vec![x_info, y_info, s_info],
        };

        self.push_new_prop_with_metadata(
            self::modulo::Modulo::new(x, y, s),
            ConstraintType::Modulo,
            variables,
            metadata,
        )
    }

    /// Declare a new propagator to enforce `|x| == s`.
    pub fn abs(&mut self, x: impl View, s: VarId) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let x_info = self.analyze_view(&x);
        let s_info = ViewInfo::Variable { var_id: s };

        let variables: Vec<_> = x
            .get_underlying_var()
            .into_iter()
            .chain(std::iter::once(s))
            .collect();

        let metadata = ConstraintData::NAry {
            operands: vec![x_info, s_info],
        };

        self.push_new_prop_with_metadata(
            self::abs::Abs::new(x, s),
            ConstraintType::AbsoluteValue,
            variables,
            metadata,
        )
    }

    /// Declare a new propagator to enforce `min(vars...) == result`.
    pub fn min(&mut self, vars: Vec<VarId>, result: VarId) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let operands: Vec<ViewInfo> = vars
            .iter()
            .map(|&var| ViewInfo::Variable { var_id: var })
            .chain(std::iter::once(ViewInfo::Variable { var_id: result }))
            .collect();

        let variables: Vec<_> = vars
            .iter()
            .cloned()
            .chain(std::iter::once(result))
            .collect();

        let metadata = ConstraintData::NAry { operands };

        self.push_new_prop_with_metadata(
            self::min::Min::new(vars, result),
            ConstraintType::Minimum,
            variables,
            metadata,
        )
    }

    /// Declare a new propagator to enforce `max(vars...) == result`.
    pub fn max(&mut self, vars: Vec<VarId>, result: VarId) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let operands: Vec<ViewInfo> = vars
            .iter()
            .map(|&var| ViewInfo::Variable { var_id: var })
            .chain(std::iter::once(ViewInfo::Variable { var_id: result }))
            .collect();

        let variables: Vec<_> = vars
            .iter()
            .cloned()
            .chain(std::iter::once(result))
            .collect();

        let metadata = ConstraintData::NAry { operands };

        self.push_new_prop_with_metadata(
            self::max::Max::new(vars, result),
            ConstraintType::Maximum,
            variables,
            metadata,
        )
    }

    /// Declare a new propagator to enforce `x / y == s`.
    pub fn div(&mut self, x: impl View, y: impl View, s: VarId) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let x_info = self.analyze_view(&x);
        let y_info = self.analyze_view(&y);
        let s_info = ViewInfo::Variable { var_id: s };

        let variables: Vec<_> = x
            .get_underlying_var()
            .into_iter()
            .chain(y.get_underlying_var())
            .chain(std::iter::once(s))
            .collect();

        let metadata = ConstraintData::NAry {
            operands: vec![x_info, y_info, s_info],
        };

        self.push_new_prop_with_metadata(
            self::div::Div::new(x, y, s),
            ConstraintType::Division,
            variables,
            metadata,
        )
    }

    /// Declare a new propagator to enforce `sum(xs) == s`.
    pub fn sum(&mut self, xs: Vec<impl View>, s: VarId) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let mut operands = Vec::new();
        let mut variables = Vec::new();

        // Analyze all variables in the sum
        for x in &xs {
            operands.push(self.analyze_view(x));
            if let Some(var_id) = x.get_underlying_var() {
                variables.push(var_id);
            }
        }

        // Add the result variable
        operands.push(ViewInfo::Variable { var_id: s });
        variables.push(s);

        let metadata = ConstraintData::NAry { operands };

        self.push_new_prop_with_metadata(
            self::sum::Sum::new(xs, s),
            ConstraintType::Sum,
            variables,
            metadata,
        )
    }

    /// Declare a new propagator to enforce `x == y`.
    pub fn equals(&mut self, x: impl View, y: impl View) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType};

        let x_info = self.analyze_view(&x);
        let y_info = self.analyze_view(&y);

        let variables: Vec<_> = x
            .get_underlying_var()
            .into_iter()
            .chain(y.get_underlying_var())
            .collect();

        let metadata = ConstraintData::Binary {
            left: x_info,
            right: y_info,
        };

        self.push_new_prop_with_metadata(
            self::eq::Eq::new(x, y),
            ConstraintType::Equals,
            variables,
            metadata,
        )
    }

    /// Declare a new propagator to enforce `x != y`.
    pub fn not_equals(&mut self, x: impl View, y: impl View) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType};

        let x_info = self.analyze_view(&x);
        let y_info = self.analyze_view(&y);

        let variables: Vec<_> = x
            .get_underlying_var()
            .into_iter()
            .chain(y.get_underlying_var())
            .collect();

        let metadata = ConstraintData::Binary {
            left: x_info,
            right: y_info,
        };

        self.push_new_prop_with_metadata(
            self::neq::NotEquals::new(x, y),
            ConstraintType::NotEquals,
            variables,
            metadata,
        )
    }

    /// Declare a new propagator to enforce `x <= y`.
    pub fn less_than_or_equals(&mut self, x: impl View, y: impl View) -> PropId {
        // Use the metadata collection version
        self.less_than_or_equals_with_metadata(x, y)
    }

    /// Declare a type-aware propagator to enforce `x < y`.
    /// This version uses ULP-based precision by implementing x < y as x + 1 <= y for integers
    /// and appropriate ULP-based bounds for floats.
    pub fn less_than(&mut self, x: impl View, y: impl View) -> PropId {
        // Use the metadata collection version
        self.less_than_with_metadata(x, y)
    }

    /// Declare a new propagator to enforce `x >= y`.
    pub fn greater_than_or_equals(&mut self, x: impl View, y: impl View) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType};

        let x_info = self.analyze_view(&x);
        let y_info = self.analyze_view(&y);

        let variables: Vec<_> = x
            .get_underlying_var()
            .into_iter()
            .chain(y.get_underlying_var())
            .collect();

        let metadata = ConstraintData::Binary {
            left: x_info,
            right: y_info,
        };

        self.push_new_prop_with_metadata(
            self::leq::LessThanOrEquals::new(y, x), // x >= y  =>  y <= x
            ConstraintType::GreaterThanOrEquals,
            variables,
            metadata,
        )
    }

    /// Declare a type-aware propagator to enforce `x > y`.
    /// This version uses ULP-based precision by implementing x > y as x >= y + 1 for integers
    /// and appropriate ULP-based bounds for floats.
    pub fn greater_than(&mut self, x: impl View, y: impl View) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType};

        let x_info = self.analyze_view(&x);
        let y_info = self.analyze_view(&y);

        // For constraint metadata, we want to preserve the original relationship x > y
        // The metadata represents the logical constraint, not the implementation details
        let metadata = ConstraintData::Binary {
            left: x_info,
            right: y_info,
        };

        let variables: Vec<_> = x
            .get_underlying_var()
            .into_iter()
            .chain(y.get_underlying_var())
            .collect();

        self.push_new_prop_with_metadata(
            self::leq::LessThanOrEquals::new(y.next(), x), // x > y  =>  y.next() <= x
            ConstraintType::GreaterThan,
            variables,
            metadata,
        )
    }

    /// Declare a new propagator to enforce that all variables have different values.
    /// This is more efficient than pairwise not-equals constraints.
    /// Uses the ultra-efficient AllDifferent implementation with adaptive algorithms.
    pub fn all_different(&mut self, vars: Vec<VarId>) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let operands: Vec<_> = vars
            .iter()
            .map(|&var_id| ViewInfo::Variable { var_id })
            .collect();

        let metadata = ConstraintData::NAry { operands };

        self.push_new_prop_with_metadata(
            self::alldiff::AllDiff::new(vars.clone()),
            ConstraintType::AllDifferent,
            vars,
            metadata,
        )
    }

    /// Declare a new propagator to enforce that all variables have the same value.
    /// This is the complement of AllDifferent constraint.
    /// Uses efficient domain intersection for value propagation.
    pub fn all_equal(&mut self, vars: Vec<VarId>) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let operands: Vec<_> = vars
            .iter()
            .map(|&var_id| ViewInfo::Variable { var_id })
            .collect();

        let metadata = ConstraintData::NAry { operands };

        self.push_new_prop_with_metadata(
            self::allequal::AllEqual::new(vars.clone()),
            ConstraintType::AllEqual,
            vars,
            metadata,
        )
    }

    /// Declare a new propagator to enforce that exactly count_var variables in vars equal target_var.
    /// This is the unified count constraint that works with variable targets.
    /// For constant values, create a fixed variable (e.g., m.int(3, 3)) and pass it as target_var.
    pub fn count_constraint(
        &mut self,
        vars: Vec<VarId>,
        target_var: impl crate::variables::View,
        count_var: VarId,
    ) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let target_info = self.analyze_view(&target_var);
        let count_instance = count::Count::new(vars.clone(), target_var, count_var);

        let mut operands: Vec<ViewInfo> = vars
            .iter()
            .map(|&var_id| ViewInfo::Variable { var_id })
            .collect();
        operands.push(target_info);
        operands.push(ViewInfo::Variable { var_id: count_var });

        let metadata = ConstraintData::NAry { operands };

        let mut all_vars = vars.clone();
        all_vars.extend(target_var.get_underlying_var());
        all_vars.push(count_var);

        self.push_new_prop_with_metadata(count_instance, ConstraintType::Count, all_vars, metadata)
    }

    /// Declare a new propagator to enforce that array[index] == value.
    /// This is the element constraint for array indexing operations.
    /// Supports both constant and variable indices with bidirectional propagation.
    pub fn element(&mut self, array: Vec<VarId>, index: VarId, value: VarId) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let mut operands: Vec<ViewInfo> = array
            .iter()
            .map(|&var_id| ViewInfo::Variable { var_id })
            .collect();
        operands.push(ViewInfo::Variable { var_id: index });
        operands.push(ViewInfo::Variable { var_id: value });

        let metadata = ConstraintData::NAry { operands };
        let trigger_vars = {
            let mut vars = array.clone();
            vars.push(index);
            vars.push(value);
            vars
        };

        self.push_new_prop_with_metadata(
            self::element::Element::new(array, index, value),
            ConstraintType::Element,
            trigger_vars,
            metadata,
        )
    }

    /// Declare a new propagator to enforce a between constraint: lower <= middle <= upper
    pub fn between_constraint(&mut self, lower: VarId, middle: VarId, upper: VarId) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let variables = vec![lower, middle, upper];
        let operands = vec![
            ViewInfo::Variable { var_id: lower },
            ViewInfo::Variable { var_id: middle },
            ViewInfo::Variable { var_id: upper },
        ];

        let metadata = ConstraintData::NAry { operands };

        self.push_new_prop_with_metadata(
            self::between::BetweenConstraint::new(lower, middle, upper),
            ConstraintType::Between,
            variables,
            metadata,
        )
    }

    /// Declare a new propagator to enforce "at least N" cardinality constraint
    pub fn at_least_constraint(
        &mut self,
        vars: Vec<VarId>,
        target_value: i32,
        count: i32,
    ) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let operands: Vec<ViewInfo> = vars
            .iter()
            .map(|&var_id| ViewInfo::Variable { var_id })
            .collect();

        let metadata = ConstraintData::NAry { operands };

        self.push_new_prop_with_metadata(
            self::cardinality::CardinalityConstraint::at_least(vars.clone(), target_value, count),
            ConstraintType::AtLeast,
            vars,
            metadata,
        )
    }

    /// Declare a new propagator to enforce "at most N" cardinality constraint
    pub fn at_most_constraint(
        &mut self,
        vars: Vec<VarId>,
        target_value: i32,
        count: i32,
    ) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let operands: Vec<ViewInfo> = vars
            .iter()
            .map(|&var_id| ViewInfo::Variable { var_id })
            .collect();

        let metadata = ConstraintData::NAry { operands };

        self.push_new_prop_with_metadata(
            self::cardinality::CardinalityConstraint::at_most(vars.clone(), target_value, count),
            ConstraintType::AtMost,
            vars,
            metadata,
        )
    }

    /// Declare a new propagator to enforce "exactly N" cardinality constraint
    pub fn exactly_constraint(
        &mut self,
        vars: Vec<VarId>,
        target_value: i32,
        count: i32,
    ) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let operands: Vec<ViewInfo> = vars
            .iter()
            .map(|&var_id| ViewInfo::Variable { var_id })
            .collect();

        let metadata = ConstraintData::NAry { operands };

        self.push_new_prop_with_metadata(
            self::cardinality::CardinalityConstraint::exactly(vars.clone(), target_value, count),
            ConstraintType::Exactly,
            vars,
            metadata,
        )
    }

    /// Declare a new propagator to enforce if-then-else constraint
    pub fn if_then_else_constraint(
        &mut self,
        condition: self::conditional::Condition,
        then_constraint: self::conditional::SimpleConstraint,
        else_constraint: Option<self::conditional::SimpleConstraint>,
    ) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let constraint = self::conditional::IfThenElseConstraint::new(
            condition,
            then_constraint,
            else_constraint,
        );
        let variables = constraint.variables();

        let operands: Vec<ViewInfo> = variables
            .iter()
            .map(|&var_id| ViewInfo::Variable { var_id })
            .collect();

        let metadata = ConstraintData::NAry { operands };

        self.push_new_prop_with_metadata(
            constraint,
            ConstraintType::IfThenElse,
            variables,
            metadata,
        )
    }

    /// Declare a new propagator to enforce a table constraint.
    /// Variables must take values that correspond to tuples in the allowed table.
    /// This constraint is useful for expressing complex relationships between variables
    /// by explicitly listing all valid combinations.
    pub fn table_constraint(
        &mut self,
        vars: Vec<VarId>,
        tuples: Vec<Vec<crate::variables::Val>>,
    ) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let operands: Vec<ViewInfo> = vars
            .iter()
            .map(|&var_id| ViewInfo::Variable { var_id })
            .collect();

        let metadata = ConstraintData::NAry { operands };

        self.push_new_prop_with_metadata(
            self::table::Table::new(vars.clone(), tuples),
            ConstraintType::Table,
            vars,
            metadata,
        )
    }

    /// Create a no-operation propagator for branching operations that have already applied domain filtering.
    pub fn noop(&mut self) -> PropId {
        self.push_new_prop(self::noop::NoOp::new())
    }

    /// Register propagator dependencies and store its state as a trait object.
    fn push_new_prop(&mut self, state: impl Propagate) -> PropId {
        // Create new handle to refer to propagator state and dependencies
        let p = PropId(self.state.len());

        // Register dependencies listed by trait implementor
        for v in state.list_trigger_vars() {
            // Ensure the dependencies matrix is large enough
            while self.dependencies.len() <= v.to_index() {
                self.dependencies.push(Vec::new());
            }
            self.dependencies[v].push(p);
        }

        // Store propagator state as shared trait object
        let boxed = Box::new(state);
        self.state.push(Rc::new(boxed));

        p
    }

    /// Register propagator with metadata collection
    fn push_new_prop_with_metadata(
        &mut self,
        state: impl Propagate,
        constraint_type: crate::optimization::constraint_metadata::ConstraintType,
        variables: Vec<VarId>,
        metadata: crate::optimization::constraint_metadata::ConstraintData,
    ) -> PropId {
        // Create propagator first
        let prop_id = self.push_new_prop(state);

        // Register constraint metadata
        let _constraint_id =
            self.constraint_registry
                .register_constraint(constraint_type, variables, metadata);

        prop_id
    }

    /// Get the number of constraints for analysis
    pub fn constraint_count(&self) -> usize {
        self.state.len()
    }

    // Helper functions for constraint metadata collection

    /// Analyze a view to extract constraint information
    fn analyze_view<T: View>(
        &self,
        view: &T,
    ) -> crate::optimization::constraint_metadata::ViewInfo {
        use crate::optimization::constraint_metadata::{ConstraintValue, ViewInfo};

        if let Some(var_id) = view.get_underlying_var() {
            ViewInfo::Variable { var_id }
        } else {
            // Check if this is a constant value by creating a dummy context
            // Constants will have the same min and max values
            let mut vars = crate::variables::Vars::default();
            let mut events = Vec::new();
            let ctx = crate::variables::views::Context::new(&mut vars, &mut events);

            let min_val = view.min(&ctx);
            let max_val = view.max(&ctx);

            if min_val == max_val {
                // This is a constant value
                let value = match min_val {
                    crate::variables::Val::ValI(i) => ConstraintValue::Integer(i),
                    crate::variables::Val::ValF(f) => ConstraintValue::Float(f),
                };
                ViewInfo::Constant { value }
            } else {
                // For now, mark complex views as such
                // A full implementation would detect transformations
                ViewInfo::Complex
            }
        }
    }

    // Create enhanced constraint methods with metadata collection

    /// Declare a new propagator to enforce `x <= y` with metadata collection.
    pub fn less_than_or_equals_with_metadata(&mut self, x: impl View, y: impl View) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType};

        let x_info = self.analyze_view(&x);
        let y_info = self.analyze_view(&y);
        let variables: Vec<_> = x
            .get_underlying_var()
            .into_iter()
            .chain(y.get_underlying_var())
            .collect();

        let metadata = ConstraintData::Binary {
            left: x_info,
            right: y_info,
        };

        self.push_new_prop_with_metadata(
            self::leq::LessThanOrEquals::new(x, y),
            ConstraintType::LessThanOrEquals,
            variables,
            metadata,
        )
    }

    /// Declare a type-aware propagator to enforce `x < y` with metadata collection.
    pub fn less_than_with_metadata(&mut self, x: impl View, y: impl View) -> PropId {
        use crate::optimization::constraint_metadata::{
            ConstraintData, ConstraintType, TransformationType, ViewInfo,
        };

        let x_info = self.analyze_view(&x);
        let y_info = self.analyze_view(&y);

        // For x < y implemented as x.next() <= y, we need to track the transformation
        let transformed_x_info = if let ViewInfo::Variable { var_id } = x_info {
            ViewInfo::Transformed {
                base_var: var_id,
                transformation: TransformationType::Next,
            }
        } else {
            ViewInfo::Complex
        };

        let variables: Vec<_> = x
            .get_underlying_var()
            .into_iter()
            .chain(y.get_underlying_var())
            .collect();

        let metadata = ConstraintData::Binary {
            left: transformed_x_info,
            right: y_info,
        };

        self.push_new_prop_with_metadata(
            self::leq::LessThanOrEquals::new(x.next(), y),
            ConstraintType::LessThan,
            variables,
            metadata,
        )
    }

    /// Declare a new propagator to enforce `result = a AND b AND c AND ...`.
    /// All variables are treated as boolean: 0 = false, non-zero = true.
    pub fn bool_and(&mut self, operands: Vec<VarId>, result: VarId) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let operand_infos: Vec<_> = operands
            .iter()
            .map(|&var_id| ViewInfo::Variable { var_id })
            .collect();

        let variables: Vec<_> = operands
            .iter()
            .cloned()
            .chain(std::iter::once(result))
            .collect();

        let metadata = ConstraintData::NAry {
            operands: operand_infos,
        };

        self.push_new_prop_with_metadata(
            self::bool_logic::BoolAnd::new(operands, result),
            ConstraintType::BooleanAnd,
            variables,
            metadata,
        )
    }

    /// Declare a new propagator to enforce `result = a OR b OR c OR ...`.
    /// All variables are treated as boolean: 0 = false, non-zero = true.
    pub fn bool_or(&mut self, operands: Vec<VarId>, result: VarId) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let operand_infos: Vec<_> = operands
            .iter()
            .map(|&var_id| ViewInfo::Variable { var_id })
            .collect();

        let variables: Vec<_> = operands
            .iter()
            .cloned()
            .chain(std::iter::once(result))
            .collect();

        let metadata = ConstraintData::NAry {
            operands: operand_infos,
        };

        self.push_new_prop_with_metadata(
            self::bool_logic::BoolOr::new(operands, result),
            ConstraintType::BooleanOr,
            variables,
            metadata,
        )
    }

    /// Declare a new propagator to enforce `result = NOT operand`.
    /// Variables are treated as boolean: 0 = false, non-zero = true.
    pub fn bool_not(&mut self, operand: VarId, result: VarId) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let operand_info = ViewInfo::Variable { var_id: operand };
        let result_info = ViewInfo::Variable { var_id: result };

        let variables = vec![operand, result];

        let metadata = ConstraintData::Binary {
            left: operand_info,
            right: result_info,
        };

        self.push_new_prop_with_metadata(
            self::bool_logic::BoolNot::new(operand, result),
            ConstraintType::BooleanNot,
            variables,
            metadata,
        )
    }

    pub fn bool_xor(&mut self, x: VarId, y: VarId, result: VarId) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let x_info = ViewInfo::Variable { var_id: x };
        let y_info = ViewInfo::Variable { var_id: y };
        let result_info = ViewInfo::Variable { var_id: result };

        let variables = vec![x, y, result];

        let metadata = ConstraintData::NAry {
            operands: vec![x_info, y_info, result_info],
        };

        self.push_new_prop_with_metadata(
            self::bool_logic::BoolXor::new(x, y, result),
            ConstraintType::BooleanXor,
            variables,
            metadata,
        )
    }

    // ═══════════════════════════════════════════════════════════════════════
    // 🔄 Reification Constraints
    // ═══════════════════════════════════════════════════════════════════════

    /// Declare a reified equality constraint: `b ⇔ (x = y)`.
    ///
    /// The boolean variable `b` is 1 if and only if `x = y`.
    /// - If b = 1, then x must equal y
    /// - If b = 0, then x must not equal y
    /// - If x = y, then b must be 1
    /// - If x ≠ y, then b must be 0
    pub fn int_eq_reif(&mut self, x: VarId, y: VarId, b: VarId) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let x_info = ViewInfo::Variable { var_id: x };
        let y_info = ViewInfo::Variable { var_id: y };

        let variables = vec![x, y, b];

        let metadata = ConstraintData::Binary {
            left: x_info,
            right: y_info,
        };

        self.push_new_prop_with_metadata(
            self::reification::IntEqReif::new(x, y, b),
            ConstraintType::EqualityReified,
            variables,
            metadata,
        )
    }

    /// Declare a reified inequality constraint: `b ⇔ (x ≠ y)`.
    ///
    /// The boolean variable `b` is 1 if and only if `x ≠ y`.
    /// - If b = 1, then x must not equal y
    /// - If b = 0, then x must equal y
    /// - If x ≠ y, then b must be 1
    /// - If x = y, then b must be 0
    pub fn int_ne_reif(&mut self, x: VarId, y: VarId, b: VarId) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let x_info = ViewInfo::Variable { var_id: x };
        let y_info = ViewInfo::Variable { var_id: y };

        let variables = vec![x, y, b];

        let metadata = ConstraintData::Binary {
            left: x_info,
            right: y_info,
        };

        self.push_new_prop_with_metadata(
            self::reification::IntNeReif::new(x, y, b),
            ConstraintType::InequalityReified,
            variables,
            metadata,
        )
    }

    /// Declare a reified less-than constraint: `b ⇔ (x < y)`.
    ///
    /// The boolean variable `b` is 1 if and only if `x < y`.
    pub fn int_lt_reif(&mut self, x: VarId, y: VarId, b: VarId) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let x_info = ViewInfo::Variable { var_id: x };
        let y_info = ViewInfo::Variable { var_id: y };

        let variables = vec![x, y, b];

        let metadata = ConstraintData::Binary {
            left: x_info,
            right: y_info,
        };

        self.push_new_prop_with_metadata(
            self::reification::IntLtReif::new(x, y, b),
            ConstraintType::LessThanReified,
            variables,
            metadata,
        )
    }

    /// Declare a reified less-than-or-equal constraint: `b ⇔ (x ≤ y)`.
    ///
    /// The boolean variable `b` is 1 if and only if `x ≤ y`.
    pub fn int_le_reif(&mut self, x: VarId, y: VarId, b: VarId) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let x_info = ViewInfo::Variable { var_id: x };
        let y_info = ViewInfo::Variable { var_id: y };

        let variables = vec![x, y, b];

        let metadata = ConstraintData::Binary {
            left: x_info,
            right: y_info,
        };

        self.push_new_prop_with_metadata(
            self::reification::IntLeReif::new(x, y, b),
            ConstraintType::LessEqualReified,
            variables,
            metadata,
        )
    }

    /// Declare a reified greater-than constraint: `b ⇔ (x > y)`.
    ///
    /// The boolean variable `b` is 1 if and only if `x > y`.
    pub fn int_gt_reif(&mut self, x: VarId, y: VarId, b: VarId) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let x_info = ViewInfo::Variable { var_id: x };
        let y_info = ViewInfo::Variable { var_id: y };

        let variables = vec![x, y, b];

        let metadata = ConstraintData::Binary {
            left: x_info,
            right: y_info,
        };

        self.push_new_prop_with_metadata(
            self::reification::IntGtReif::new(x, y, b),
            ConstraintType::GreaterThanReified,
            variables,
            metadata,
        )
    }

    /// Declare a reified greater-than-or-equal constraint: `b ⇔ (x ≥ y)`.
    ///
    /// The boolean variable `b` is 1 if and only if `x ≥ y`.
    pub fn int_ge_reif(&mut self, x: VarId, y: VarId, b: VarId) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let x_info = ViewInfo::Variable { var_id: x };
        let y_info = ViewInfo::Variable { var_id: y };

        let variables = vec![x, y, b];

        let metadata = ConstraintData::Binary {
            left: x_info,
            right: y_info,
        };

        self.push_new_prop_with_metadata(
            self::reification::IntGeReif::new(x, y, b),
            ConstraintType::GreaterEqualReified,
            variables,
            metadata,
        )
    }

    // ═══════════════════════════════════════════════════════════════════════
    // Linear Constraint Propagators
    // ═══════════════════════════════════════════════════════════════════════

    /// Declare an integer linear equality constraint: `sum(coeffs[i] * vars[i]) = constant`.
    pub fn int_lin_eq(
        &mut self,
        coefficients: Vec<i32>,
        variables: Vec<VarId>,
        constant: i32,
    ) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let operands: Vec<ViewInfo> = variables
            .iter()
            .map(|&v| ViewInfo::Variable { var_id: v })
            .collect();

        let metadata = ConstraintData::NAry { operands };

        self.push_new_prop_with_metadata(
            self::linear::IntLinEq::new(coefficients, variables.clone(), constant),
            ConstraintType::Equals,
            variables,
            metadata,
        )
    }

    /// Declare an integer linear less-or-equal constraint: `sum(coeffs[i] * vars[i]) ≤ constant`.
    pub fn int_lin_le(
        &mut self,
        coefficients: Vec<i32>,
        variables: Vec<VarId>,
        constant: i32,
    ) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let operands: Vec<ViewInfo> = variables
            .iter()
            .map(|&v| ViewInfo::Variable { var_id: v })
            .collect();

        let metadata = ConstraintData::NAry { operands };

        self.push_new_prop_with_metadata(
            self::linear::IntLinLe::new(coefficients, variables.clone(), constant),
            ConstraintType::LessThanOrEquals,
            variables,
            metadata,
        )
    }

    /// Declare an integer linear not-equal constraint: `sum(coeffs[i] * vars[i]) ≠ constant`.
    pub fn int_lin_ne(
        &mut self,
        coefficients: Vec<i32>,
        variables: Vec<VarId>,
        constant: i32,
    ) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let operands: Vec<ViewInfo> = variables
            .iter()
            .map(|&v| ViewInfo::Variable { var_id: v })
            .collect();

        let metadata = ConstraintData::NAry { operands };

        self.push_new_prop_with_metadata(
            self::linear::IntLinNe::new(coefficients, variables.clone(), constant),
            ConstraintType::NotEquals,
            variables,
            metadata,
        )
    }

    /// Declare a reified integer linear equality constraint: `b ⟺ sum(coeffs[i] * vars[i]) = constant`.
    pub fn int_lin_eq_reif(
        &mut self,
        coefficients: Vec<i32>,
        variables: Vec<VarId>,
        constant: i32,
        reif_var: VarId,
    ) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let mut operands: Vec<ViewInfo> = variables
            .iter()
            .map(|&v| ViewInfo::Variable { var_id: v })
            .collect();
        operands.push(ViewInfo::Variable { var_id: reif_var });

        let metadata = ConstraintData::NAry { operands };

        let mut all_vars = variables.clone();
        all_vars.push(reif_var);

        self.push_new_prop_with_metadata(
            self::linear::IntLinEqReif::new(coefficients, variables, constant, reif_var),
            ConstraintType::EqualityReified,
            all_vars,
            metadata,
        )
    }

    /// Declare a reified integer linear less-or-equal constraint: `b ⟺ sum(coeffs[i] * vars[i]) ≤ constant`.
    pub fn int_lin_le_reif(
        &mut self,
        coefficients: Vec<i32>,
        variables: Vec<VarId>,
        constant: i32,
        reif_var: VarId,
    ) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let mut operands: Vec<ViewInfo> = variables
            .iter()
            .map(|&v| ViewInfo::Variable { var_id: v })
            .collect();
        operands.push(ViewInfo::Variable { var_id: reif_var });

        let metadata = ConstraintData::NAry { operands };

        let mut all_vars = variables.clone();
        all_vars.push(reif_var);

        self.push_new_prop_with_metadata(
            self::linear::IntLinLeReif::new(coefficients, variables, constant, reif_var),
            ConstraintType::InequalityReified,
            all_vars,
            metadata,
        )
    }

    /// Declare a reified integer linear not-equal constraint: `b ⟺ sum(coeffs[i] * vars[i]) ≠ constant`.
    pub fn int_lin_ne_reif(
        &mut self,
        coefficients: Vec<i32>,
        variables: Vec<VarId>,
        constant: i32,
        reif_var: VarId,
    ) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let mut operands: Vec<ViewInfo> = variables
            .iter()
            .map(|&v| ViewInfo::Variable { var_id: v })
            .collect();
        operands.push(ViewInfo::Variable { var_id: reif_var });

        let metadata = ConstraintData::NAry { operands };

        let mut all_vars = variables.clone();
        all_vars.push(reif_var);

        self.push_new_prop_with_metadata(
            self::linear::IntLinNeReif::new(coefficients, variables, constant, reif_var),
            ConstraintType::InequalityReified,
            all_vars,
            metadata,
        )
    }

    /// Declare a float linear equality constraint: `sum(coeffs[i] * vars[i]) = constant`.
    pub fn float_lin_eq(
        &mut self,
        coefficients: Vec<f64>,
        variables: Vec<VarId>,
        constant: f64,
    ) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let operands: Vec<ViewInfo> = variables
            .iter()
            .map(|&v| ViewInfo::Variable { var_id: v })
            .collect();

        let metadata = ConstraintData::NAry { operands };

        self.push_new_prop_with_metadata(
            self::linear::FloatLinEq::new(coefficients, variables.clone(), constant),
            ConstraintType::Equals,
            variables,
            metadata,
        )
    }

    /// Declare a float linear less-or-equal constraint: `sum(coeffs[i] * vars[i]) ≤ constant`.
    pub fn float_lin_le(
        &mut self,
        coefficients: Vec<f64>,
        variables: Vec<VarId>,
        constant: f64,
    ) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let operands: Vec<ViewInfo> = variables
            .iter()
            .map(|&v| ViewInfo::Variable { var_id: v })
            .collect();

        let metadata = ConstraintData::NAry { operands };

        self.push_new_prop_with_metadata(
            self::linear::FloatLinLe::new(coefficients, variables.clone(), constant),
            ConstraintType::LessThanOrEquals,
            variables,
            metadata,
        )
    }

    /// Declare a float linear not-equal constraint: `sum(coeffs[i] * vars[i]) ≠ constant`.
    pub fn float_lin_ne(
        &mut self,
        coefficients: Vec<f64>,
        variables: Vec<VarId>,
        constant: f64,
    ) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let operands: Vec<ViewInfo> = variables
            .iter()
            .map(|&v| ViewInfo::Variable { var_id: v })
            .collect();

        let metadata = ConstraintData::NAry { operands };

        self.push_new_prop_with_metadata(
            self::linear::FloatLinNe::new(coefficients, variables.clone(), constant),
            ConstraintType::NotEquals,
            variables,
            metadata,
        )
    }

    /// Declare a reified float linear equality constraint: `b ⟺ sum(coeffs[i] * vars[i]) = constant`.
    pub fn float_lin_eq_reif(
        &mut self,
        coefficients: Vec<f64>,
        variables: Vec<VarId>,
        constant: f64,
        reif_var: VarId,
    ) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let mut operands: Vec<ViewInfo> = variables
            .iter()
            .map(|&v| ViewInfo::Variable { var_id: v })
            .collect();
        operands.push(ViewInfo::Variable { var_id: reif_var });

        let metadata = ConstraintData::NAry { operands };

        let mut all_vars = variables.clone();
        all_vars.push(reif_var);

        self.push_new_prop_with_metadata(
            self::linear::FloatLinEqReif::new(coefficients, variables, constant, reif_var),
            ConstraintType::EqualityReified,
            all_vars,
            metadata,
        )
    }

    /// Declare a reified float linear less-or-equal constraint: `b ⟺ sum(coeffs[i] * vars[i]) ≤ constant`.
    pub fn float_lin_le_reif(
        &mut self,
        coefficients: Vec<f64>,
        variables: Vec<VarId>,
        constant: f64,
        reif_var: VarId,
    ) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let mut operands: Vec<ViewInfo> = variables
            .iter()
            .map(|&v| ViewInfo::Variable { var_id: v })
            .collect();
        operands.push(ViewInfo::Variable { var_id: reif_var });

        let metadata = ConstraintData::NAry { operands };

        let mut all_vars = variables.clone();
        all_vars.push(reif_var);

        self.push_new_prop_with_metadata(
            self::linear::FloatLinLeReif::new(coefficients, variables, constant, reif_var),
            ConstraintType::InequalityReified,
            all_vars,
            metadata,
        )
    }

    /// Declare a reified float linear not-equal constraint: `b ⟺ sum(coeffs[i] * vars[i]) ≠ constant`.
    pub fn float_lin_ne_reif(
        &mut self,
        coefficients: Vec<f64>,
        variables: Vec<VarId>,
        constant: f64,
        reif_var: VarId,
    ) -> PropId {
        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};

        let mut operands: Vec<ViewInfo> = variables
            .iter()
            .map(|&v| ViewInfo::Variable { var_id: v })
            .collect();
        operands.push(ViewInfo::Variable { var_id: reif_var });

        let metadata = ConstraintData::NAry { operands };

        let mut all_vars = variables.clone();
        all_vars.push(reif_var);

        self.push_new_prop_with_metadata(
            self::linear::FloatLinNeReif::new(coefficients, variables, constant, reif_var),
            ConstraintType::InequalityReified,
            all_vars,
            metadata,
        )
    }
}

/// Propagator handle that is not bound to a specific memory location.
#[derive(Clone, Copy, Debug, Eq, Hash, PartialEq)]
pub struct PropId(pub usize);

impl Index<PropId> for Vec<Box<dyn Prune>> {
    type Output = Box<dyn Prune>;

    fn index(&self, index: PropId) -> &Self::Output {
        &self[index.0]
    }
}

impl IndexMut<PropId> for Vec<Box<dyn Prune>> {
    fn index_mut(&mut self, index: PropId) -> &mut Self::Output {
        &mut self[index.0]
    }
}

// Public exports
#[doc(hidden)]
pub use alldiff::AllDiff;
#[doc(hidden)]
pub use allequal::AllEqual;
#[doc(hidden)]
pub use count::Count;