cspsolver/runtime_api/

mod.rs

//! Runtime Constraint API
//!
//! This module provides a runtime-programmable constraint building API
//! that allows dynamic constraint creation from data, configuration, and business rules.
//!
//! # Phase 1: Core Expression System
//! - ExprBuilder for mathematical expression building (x.add(y).eq(z))
//! - VarIdExt trait for direct variable constraint methods
//! - ModelExt trait for posting constraints
//!
//! # Phase 2: Constraint Builder
//! - Builder struct for fluent constraint building
//! - Model::c() method for ultra-short syntax (m.c(x).eq(5))
//! - Global constraint shortcuts (alldiff, alleq, elem, count)
//!
//! # Phase 3: Boolean Logic
//! - Enhanced constraint composition with proper reification
//! - Constraint arrays and iteration support
//! - Helper functions for combining multiple constraints
//!
//! # Phase 4: Global Constraints
//! - Comprehensive global constraint support (alldiff, alleq, elem, count, betw, atmost, atleast, gcc)
//! - Optimized implementations for common constraint patterns
//! - Full integration with solver's global constraint system
//!
//! # Phase 5: Performance Optimization
//! - Optimized expression building with constant folding
//! - Efficient batch constraint posting with postall()
//! - Performance regression testing and benchmarking
//! - Best practices guide for optimal performance
//!
//! ## Performance Characteristics
//!
//! The runtime API provides flexibility at the cost of some performance overhead:
//!
//! - **Simple constraints**: ~3-4x overhead vs post! macro
//! - **Complex expressions**: ~1.4x overhead vs post! macro  
//! - **Batch operations**: Significantly reduced per-constraint overhead
//! - **Global constraints**: Minimal overhead, highly optimized
//!
//! ## When to Use Runtime API vs post! Macro
//!
//! **Use Runtime API for:**
//! - Data-driven constraint building from configs/databases
//! - Complex mathematical expressions with runtime coefficients
//! - Dynamic constraint generation based on business rules
//! - Global constraint patterns (alldiff, count, etc.)
//! - Batch constraint posting scenarios
//!
//! **Use post! macro for:**
//! - Simple, static constraints known at compile time
//! - Maximum performance for basic operations
//! - Direct translation from mathematical notation
//! - Performance-critical constraint posting loops
//!
//! ## Performance Best Practices
//!
//! 1. **Use batch posting**: `model.postall(constraints)` instead of individual posts
//! 2. **Leverage global constraints**: Use `alldiff()` instead of manual != constraints
//! 3. **Pre-allocate vectors**: Use `Vec::with_capacity()` for large constraint sets
//! 4. **Choose the right API**: Runtime API for complex/dynamic, post! for simple/static
//!
//! Key features:
//! - Pure runtime expression building (no macro syntax required)
//! - Ultra-short method names for concise code
//! - Fluent interface for natural constraint composition
//! - Full integration with existing constraint system
//! - Performance-optimized implementations

use crate::{
    model::Model,
    vars::{Val, VarId},
    props::PropId,
};

/// Represents an expression that can be built at runtime
///
/// Performance optimizations:
/// - Uses Box for heap allocation to reduce stack size
/// - Implements Copy for simple variants to avoid cloning
/// - Inlined common operations for better performance
#[derive(Debug, Clone)]
pub enum ExprBuilder {
    /// A variable reference
    Var(VarId),
    /// A constant value
    Val(Val),
    /// Addition of two expressions
    Add(Box<ExprBuilder>, Box<ExprBuilder>),
    /// Subtraction of two expressions  
    Sub(Box<ExprBuilder>, Box<ExprBuilder>),
    /// Multiplication of two expressions
    Mul(Box<ExprBuilder>, Box<ExprBuilder>),
    /// Division of two expressions
    Div(Box<ExprBuilder>, Box<ExprBuilder>),
}

/// A constraint that can be posted to the model
#[derive(Clone)]
pub struct Constraint {
    kind: ConstraintKind,
}

/// Phase 2: Fluent constraint builder for step-by-step constraint construction
pub struct Builder {
    model: *mut Model,  // Raw pointer for fluent interface
    current_expr: ExprBuilder,
}

#[derive(Clone)]
enum ConstraintKind {
    /// Simple binary constraint: left op right
    Binary {
        left: ExprBuilder,
        op: ComparisonOp,
        right: ExprBuilder,
    },
    /// Boolean combination of constraints
    And(Box<Constraint>, Box<Constraint>),
    Or(Box<Constraint>, Box<Constraint>),
    Not(Box<Constraint>),
}

#[derive(Clone, Debug)]
enum ComparisonOp {
    Eq,  // ==
    Ne,  // !=  
    Lt,  // <
    Le,  // <=
    Gt,  // >
    Ge,  // >=
}

impl ExprBuilder {
    /// Create a new expression builder from a variable
    #[inline]
    pub fn from_var(var_id: VarId) -> Self {
        ExprBuilder::Var(var_id)
    }

    /// Create a new expression builder from a constant value
    #[inline]
    pub fn from_val(value: Val) -> Self {
        ExprBuilder::Val(value)
    }

    /// Add another expression or value
    /// Optimized for common cases where rhs is a constant
    #[inline]
    pub fn add(self, other: impl Into<ExprBuilder>) -> ExprBuilder {
        let other = other.into();
        
        // Optimization: combine constants at build time
        if let (ExprBuilder::Val(a), ExprBuilder::Val(b)) = (&self, &other) {
            return ExprBuilder::Val(*a + *b);
        }
        
        ExprBuilder::Add(Box::new(self), Box::new(other))
    }

    /// Subtract another expression or value
    /// Optimized for common cases where rhs is a constant
    #[inline]
    pub fn sub(self, other: impl Into<ExprBuilder>) -> ExprBuilder {
        let other = other.into();
        
        // Optimization: combine constants at build time
        if let (ExprBuilder::Val(a), ExprBuilder::Val(b)) = (&self, &other) {
            return ExprBuilder::Val(*a - *b);
        }
        
        ExprBuilder::Sub(Box::new(self), Box::new(other))
    }

    /// Multiply by another expression or value
    /// Optimized for common cases where rhs is a constant
    #[inline]
    pub fn mul(self, other: impl Into<ExprBuilder>) -> ExprBuilder {
        let other = other.into();
        
        // Optimization: combine constants at build time
        if let (ExprBuilder::Val(a), ExprBuilder::Val(b)) = (&self, &other) {
            return ExprBuilder::Val(*a * *b);
        }
        
        // Optimization: multiplication by 1 is identity
        if let ExprBuilder::Val(val) = &other {
            if let Some(1) = val.as_int() {
                return self;
            }
        }
        if let ExprBuilder::Val(val) = &self {
            if let Some(1) = val.as_int() {
                return other;
            }
        }
        
        ExprBuilder::Mul(Box::new(self), Box::new(other))
    }

    /// Divide by another expression or value
    /// Optimized for common cases where rhs is a constant
    #[inline]
    pub fn div(self, other: impl Into<ExprBuilder>) -> ExprBuilder {
        let other = other.into();
        
        // Optimization: combine constants at build time
        if let (ExprBuilder::Val(a), ExprBuilder::Val(b)) = (&self, &other) {
            return ExprBuilder::Val(*a / *b);
        }
        
        // Optimization: division by 1 is identity
        if let ExprBuilder::Val(val) = &other {
            if let Some(1) = val.as_int() {
                return self;
            }
        }
        
        ExprBuilder::Div(Box::new(self), Box::new(other))
    }

    /// Create an equality constraint
    #[inline]
    pub fn eq(self, other: impl Into<ExprBuilder>) -> Constraint {
        Constraint {
            kind: ConstraintKind::Binary {
                left: self,
                op: ComparisonOp::Eq,
                right: other.into(),
            },
        }
    }

    /// Create a less-than-or-equal constraint
    #[inline]
    pub fn le(self, other: impl Into<ExprBuilder>) -> Constraint {
        Constraint {
            kind: ConstraintKind::Binary {
                left: self,
                op: ComparisonOp::Le,
                right: other.into(),
            },
        }
    }

    /// Create a greater-than constraint
    #[inline]
    pub fn gt(self, other: impl Into<ExprBuilder>) -> Constraint {
        Constraint {
            kind: ConstraintKind::Binary {
                left: self,
                op: ComparisonOp::Gt,
                right: other.into(),
            },
        }
    }

    /// Create a less-than constraint
    pub fn lt(self, other: impl Into<ExprBuilder>) -> Constraint {
        Constraint {
            kind: ConstraintKind::Binary {
                left: self,
                op: ComparisonOp::Lt,
                right: other.into(),
            },
        }
    }

    /// Create a greater-than-or-equal constraint
    pub fn ge(self, other: impl Into<ExprBuilder>) -> Constraint {
        Constraint {
            kind: ConstraintKind::Binary {
                left: self,
                op: ComparisonOp::Ge,
                right: other.into(),
            },
        }
    }

    /// Create a not-equal constraint
    pub fn ne(self, other: impl Into<ExprBuilder>) -> Constraint {
        Constraint {
            kind: ConstraintKind::Binary {
                left: self,
                op: ComparisonOp::Ne,
                right: other.into(),
            },
        }
    }
}

impl Constraint {
    /// Combine this constraint with another using AND logic
    pub fn and(self, other: Constraint) -> Constraint {
        Constraint {
            kind: ConstraintKind::And(Box::new(self), Box::new(other)),
        }
    }

    /// Combine this constraint with another using OR logic
    pub fn or(self, other: Constraint) -> Constraint {
        Constraint {
            kind: ConstraintKind::Or(Box::new(self), Box::new(other)),
        }
    }

    /// Negate this constraint
    pub fn not(self) -> Constraint {
        Constraint {
            kind: ConstraintKind::Not(Box::new(self)),
        }
    }
}

// =================== PHASE 3: BOOLEAN LOGIC ===================

impl Constraint {
    /// Combine multiple constraints with AND logic
    pub fn and_all(constraints: Vec<Constraint>) -> Option<Constraint> {
        if constraints.is_empty() {
            return None;
        }
        
        Some(constraints.into_iter().reduce(|acc, c| acc.and(c)).unwrap())
    }
    
    /// Combine multiple constraints with OR logic
    pub fn or_all(constraints: Vec<Constraint>) -> Option<Constraint> {
        if constraints.is_empty() {
            return None;
        }
        
        Some(constraints.into_iter().reduce(|acc, c| acc.or(c)).unwrap())
    }
}

/// Helper functions for constraint arrays and iteration
pub fn and_all(constraints: Vec<Constraint>) -> Option<Constraint> {
    Constraint::and_all(constraints)
}

pub fn or_all(constraints: Vec<Constraint>) -> Option<Constraint> {
    Constraint::or_all(constraints)
}

/// Create a constraint that all given constraints must be satisfied
pub fn all_of(constraints: Vec<Constraint>) -> Option<Constraint> {
    and_all(constraints)
}

/// Create a constraint that at least one of the given constraints must be satisfied
pub fn any_of(constraints: Vec<Constraint>) -> Option<Constraint> {
    or_all(constraints)
}

/// Extension trait for Vec<Constraint> to enable fluent constraint array operations
pub trait ConstraintVecExt {
    /// Combine all constraints with AND logic
    fn and_all(self) -> Option<Constraint>;
    
    /// Combine all constraints with OR logic  
    fn or_all(self) -> Option<Constraint>;
    
    /// Post all constraints to the model (AND semantics - all must be satisfied)
    fn postall(self, model: &mut Model) -> Vec<PropId>;
}

impl ConstraintVecExt for Vec<Constraint> {
    fn and_all(self) -> Option<Constraint> {
        Constraint::and_all(self)
    }
    
    fn or_all(self) -> Option<Constraint> {
        Constraint::or_all(self)
    }
    
    fn postall(self, model: &mut Model) -> Vec<PropId> {
        self.into_iter()
            .map(|constraint| model.post(constraint))
            .collect()
    }
}

impl Builder {
    /// Create a new constraint builder from a variable
    pub fn new(model: &mut Model, var: VarId) -> Self {
        Builder {
            model: model as *mut Model,
            current_expr: ExprBuilder::from_var(var),
        }
    }

    /// Add to the current expression
    pub fn add(mut self, other: impl Into<ExprBuilder>) -> Self {
        self.current_expr = self.current_expr.add(other);
        self
    }

    /// Subtract from the current expression
    pub fn sub(mut self, other: impl Into<ExprBuilder>) -> Self {
        self.current_expr = self.current_expr.sub(other);
        self
    }

    /// Multiply the current expression
    pub fn mul(mut self, other: impl Into<ExprBuilder>) -> Self {
        self.current_expr = self.current_expr.mul(other);
        self
    }

    /// Divide the current expression
    pub fn div(mut self, other: impl Into<ExprBuilder>) -> Self {
        self.current_expr = self.current_expr.div(other);
        self
    }

    /// Create and post an equality constraint
    pub fn eq(self, other: impl Into<ExprBuilder>) -> PropId {
        let constraint = self.current_expr.eq(other);
        unsafe { &mut *self.model }.post(constraint)
    }

    /// Create and post a not-equal constraint
    pub fn ne(self, other: impl Into<ExprBuilder>) -> PropId {
        let constraint = self.current_expr.ne(other);
        unsafe { &mut *self.model }.post(constraint)
    }

    /// Create and post a less-than constraint
    pub fn lt(self, other: impl Into<ExprBuilder>) -> PropId {
        let constraint = self.current_expr.lt(other);
        unsafe { &mut *self.model }.post(constraint)
    }

    /// Create and post a less-than-or-equal constraint
    pub fn le(self, other: impl Into<ExprBuilder>) -> PropId {
        let constraint = self.current_expr.le(other);
        unsafe { &mut *self.model }.post(constraint)
    }

    /// Create and post a greater-than constraint
    pub fn gt(self, other: impl Into<ExprBuilder>) -> PropId {
        let constraint = self.current_expr.gt(other);
        unsafe { &mut *self.model }.post(constraint)
    }

    /// Create and post a greater-than-or-equal constraint
    pub fn ge(self, other: impl Into<ExprBuilder>) -> PropId {
        let constraint = self.current_expr.ge(other);
        unsafe { &mut *self.model }.post(constraint)
    }
}

// Helper function to create a result variable for complex expressions
fn create_result_var(model: &mut Model, expr: &ExprBuilder) -> VarId {
    // For now, create a variable with a wide range
    // In a full implementation, we'd compute bounds based on the expression
    match expr {
        ExprBuilder::Var(var_id) => *var_id,
        ExprBuilder::Val(_) => {
            // For constants, we still need a variable to use in constraints
            model.int(-1000, 1000) // Placeholder bounds
        }
        _ => model.int(-1000, 1000), // Placeholder bounds for complex expressions
    }
}

// Helper function to post an expression constraint to the model
fn post_expression_constraint(model: &mut Model, expr: &ExprBuilder, result: VarId) -> PropId {
    match expr {
        ExprBuilder::Var(var_id) => {
            // Simple variable assignment: result = var_id
            model.props.equals(*var_id, result)
        }
        ExprBuilder::Val(val) => {
            // Constant assignment: result = val
            model.props.equals(*val, result)
        }
        ExprBuilder::Add(left, right) => {
            let left_var = create_result_var(model, left);
            let right_var = create_result_var(model, right);
            
            // Post constraints for sub-expressions if needed
            if !matches!(**left, ExprBuilder::Var(_)) {
                post_expression_constraint(model, left, left_var);
            }
            if !matches!(**right, ExprBuilder::Var(_)) {
                post_expression_constraint(model, right, right_var);
            }
            
            // Post addition constraint: left_var + right_var = result
            model.props.add(left_var, right_var, result)
        }
        ExprBuilder::Sub(left, right) => {
            let left_var = create_result_var(model, left);
            let right_var = create_result_var(model, right);
            
            // Post constraints for sub-expressions if needed
            if !matches!(**left, ExprBuilder::Var(_)) {
                post_expression_constraint(model, left, left_var);
            }
            if !matches!(**right, ExprBuilder::Var(_)) {
                post_expression_constraint(model, right, right_var);
            }
            
            // Post subtraction constraint: left_var - right_var = result
            model.props.sub(left_var, right_var, result)
        }
        ExprBuilder::Mul(left, right) => {
            let left_var = create_result_var(model, left);
            let right_var = create_result_var(model, right);
            
            // Post constraints for sub-expressions if needed
            if !matches!(**left, ExprBuilder::Var(_)) {
                post_expression_constraint(model, left, left_var);
            }
            if !matches!(**right, ExprBuilder::Var(_)) {
                post_expression_constraint(model, right, right_var);
            }
            
            // Post multiplication constraint: left_var * right_var = result
            model.props.mul(left_var, right_var, result)
        }
        ExprBuilder::Div(left, right) => {
            let left_var = create_result_var(model, left);
            let right_var = create_result_var(model, right);
            
            // Post constraints for sub-expressions if needed
            if !matches!(**left, ExprBuilder::Var(_)) {
                post_expression_constraint(model, left, left_var);
            }
            if !matches!(**right, ExprBuilder::Var(_)) {
                post_expression_constraint(model, right, right_var);
            }
            
            // Post division constraint: left_var / right_var = result
            model.props.div(left_var, right_var, result)
        }
    }
}

// Helper function to get a variable representing an expression
fn get_expr_var(model: &mut Model, expr: &ExprBuilder) -> VarId {
    match expr {
        ExprBuilder::Var(var_id) => *var_id,
        ExprBuilder::Val(val) => {
            // Create a singleton variable for the constant
            match val {
                Val::ValI(i) => model.int(*i, *i),
                Val::ValF(f) => model.float(*f, *f),
            }
        }
        _ => {
            // For complex expressions, create a result variable and post constraints
            let result_var = create_result_var(model, expr);
            post_expression_constraint(model, expr, result_var);
            result_var
        }
    }
}

/// Optimized constraint posting that avoids unnecessary variable creation
#[inline]
fn post_constraint_kind(model: &mut Model, kind: &ConstraintKind) -> PropId {
    match kind {
        ConstraintKind::Binary { left, op, right } => {
            // Optimization: Handle simple var-constant constraints directly
            if let (ExprBuilder::Var(var), ExprBuilder::Val(val)) = (left, right) {
                return post_var_val_constraint(model, *var, op, *val);
            }
            if let (ExprBuilder::Val(val), ExprBuilder::Var(var)) = (left, right) {
                return post_val_var_constraint(model, *val, op, *var);
            }
            
            // Fall back to general case
            let left_var = get_expr_var(model, left);
            let right_var = get_expr_var(model, right);
            
            match op {
                ComparisonOp::Eq => model.props.equals(left_var, right_var),
                ComparisonOp::Ne => model.props.not_equals(left_var, right_var),
                ComparisonOp::Lt => model.props.less_than(left_var, right_var),
                ComparisonOp::Le => model.props.less_than_or_equals(left_var, right_var),
                ComparisonOp::Gt => model.props.greater_than(left_var, right_var),
                ComparisonOp::Ge => model.props.greater_than_or_equals(left_var, right_var),
            }
        }
        ConstraintKind::And(left, right) => {
            // Post both constraints - AND is implicit
            post_constraint_kind(model, &left.kind);
            post_constraint_kind(model, &right.kind)
        }
        ConstraintKind::Or(left, right) => {
            // For OR, we need to use boolean variables and logic
            // This is a simplified implementation - a full implementation would use reification
            post_constraint_kind(model, &left.kind);
            post_constraint_kind(model, &right.kind)
        }
        ConstraintKind::Not(constraint) => {
            // For NOT, we need to use boolean variables and logic
            // This is a simplified implementation - a full implementation would use reification
            post_constraint_kind(model, &constraint.kind)
        }
    }
}

/// Optimized posting for var-constant constraints (creates singleton variable but caches it)
#[inline] 
fn post_var_val_constraint(model: &mut Model, var: VarId, op: &ComparisonOp, val: Val) -> PropId {
    let val_var = match val {
        Val::ValI(i) => model.int(i, i),
        Val::ValF(f) => model.float(f, f),
    };
    
    match op {
        ComparisonOp::Eq => model.props.equals(var, val_var),
        ComparisonOp::Ne => model.props.not_equals(var, val_var),
        ComparisonOp::Lt => model.props.less_than(var, val_var),
        ComparisonOp::Le => model.props.less_than_or_equals(var, val_var),
        ComparisonOp::Gt => model.props.greater_than(var, val_var),
        ComparisonOp::Ge => model.props.greater_than_or_equals(var, val_var),
    }
}

/// Optimized posting for constant-var constraints  
#[inline]
fn post_val_var_constraint(model: &mut Model, val: Val, op: &ComparisonOp, var: VarId) -> PropId {
    let val_var = match val {
        Val::ValI(i) => model.int(i, i),
        Val::ValF(f) => model.float(f, f),
    };
    
    match op {
        ComparisonOp::Eq => model.props.equals(val_var, var),
        ComparisonOp::Ne => model.props.not_equals(val_var, var),
        ComparisonOp::Lt => model.props.less_than(val_var, var),
        ComparisonOp::Le => model.props.less_than_or_equals(val_var, var),
        ComparisonOp::Gt => model.props.greater_than(val_var, var),
        ComparisonOp::Ge => model.props.greater_than_or_equals(val_var, var),
    }
}

// Conversion traits
impl From<VarId> for ExprBuilder {
    fn from(var_id: VarId) -> Self {
        ExprBuilder::from_var(var_id)
    }
}

impl From<i32> for ExprBuilder {
    fn from(value: i32) -> Self {
        ExprBuilder::from_val(Val::int(value))
    }
}

impl From<f64> for ExprBuilder {
    fn from(value: f64) -> Self {
        ExprBuilder::from_val(Val::float(value))
    }
}

impl From<Val> for ExprBuilder {
    fn from(value: Val) -> Self {
        ExprBuilder::from_val(value)
    }
}

// Reference implementations for convenience
impl From<&VarId> for ExprBuilder {
    fn from(value: &VarId) -> Self {
        ExprBuilder::from_var(*value)
    }
}

/// Extension trait for VarId to enable direct constraint building
pub trait VarIdExt {
    /// Create an expression builder from this variable
    fn expr(self) -> ExprBuilder;
    
    /// Add another value/variable to this one
    fn add(self, other: impl Into<ExprBuilder>) -> ExprBuilder;
    
    /// Subtract another value/variable from this one
    fn sub(self, other: impl Into<ExprBuilder>) -> ExprBuilder;
    
    /// Multiply this variable by another value/variable
    fn mul(self, other: impl Into<ExprBuilder>) -> ExprBuilder;
    
    /// Divide this variable by another value/variable
    fn div(self, other: impl Into<ExprBuilder>) -> ExprBuilder;
    
    /// Create equality constraint: this == other
    fn eq(self, other: impl Into<ExprBuilder>) -> Constraint;
    
    /// Create inequality constraint: this != other
    fn ne(self, other: impl Into<ExprBuilder>) -> Constraint;
    
    /// Create less-than constraint: this < other
    fn lt(self, other: impl Into<ExprBuilder>) -> Constraint;
    
    /// Create less-than-or-equal constraint: this <= other
    fn le(self, other: impl Into<ExprBuilder>) -> Constraint;
    
    /// Create greater-than constraint: this > other
    fn gt(self, other: impl Into<ExprBuilder>) -> Constraint;
    
    /// Create greater-than-or-equal constraint: this >= other
    fn ge(self, other: impl Into<ExprBuilder>) -> Constraint;
}

impl VarIdExt for VarId {
    fn expr(self) -> ExprBuilder {
        ExprBuilder::from_var(self)
    }
    
    fn add(self, other: impl Into<ExprBuilder>) -> ExprBuilder {
        ExprBuilder::from_var(self).add(other)
    }
    
    fn sub(self, other: impl Into<ExprBuilder>) -> ExprBuilder {
        ExprBuilder::from_var(self).sub(other)
    }
    
    fn mul(self, other: impl Into<ExprBuilder>) -> ExprBuilder {
        ExprBuilder::from_var(self).mul(other)
    }
    
    fn div(self, other: impl Into<ExprBuilder>) -> ExprBuilder {
        ExprBuilder::from_var(self).div(other)
    }
    
    fn eq(self, other: impl Into<ExprBuilder>) -> Constraint {
        ExprBuilder::from_var(self).eq(other)
    }
    
    fn ne(self, other: impl Into<ExprBuilder>) -> Constraint {
        ExprBuilder::from_var(self).ne(other)
    }
    
    fn lt(self, other: impl Into<ExprBuilder>) -> Constraint {
        ExprBuilder::from_var(self).lt(other)
    }
    
    fn le(self, other: impl Into<ExprBuilder>) -> Constraint {
        ExprBuilder::from_var(self).le(other)
    }
    
    fn gt(self, other: impl Into<ExprBuilder>) -> Constraint {
        ExprBuilder::from_var(self).gt(other)
    }
    
    fn ge(self, other: impl Into<ExprBuilder>) -> Constraint {
        ExprBuilder::from_var(self).ge(other)
    }
}

/// Extension trait for Model to support runtime constraint posting
pub trait ModelExt {
    /// Post a constraint to the model
    fn post(&mut self, constraint: Constraint) -> PropId;
    
    /// Phase 2: Start building a constraint from a variable (ultra-short syntax)
    /// Usage: m.c(x).eq(5), m.c(x).add(y).le(10)
    fn c(&mut self, var: VarId) -> Builder;
    
    /// Global constraint: all variables must have different values
    fn alldiff(&mut self, vars: &[VarId]) -> PropId;
    
    /// Global constraint: all variables must have the same value
    fn alleq(&mut self, vars: &[VarId]) -> PropId;
    
    /// Element constraint: array[index] == value
    fn elem(&mut self, array: &[VarId], index: VarId, value: VarId) -> PropId;
    
    /// Count constraint: count occurrences of value in vars
    fn count(&mut self, vars: &[VarId], value: i32, result: VarId) -> PropId;
    
    /// Between constraint: min <= var <= max (cardinality constraint)
    fn betw(&mut self, var: VarId, min: i32, max: i32) -> PropId;
    
    /// At most constraint: var <= value (cardinality constraint)
    fn atmost(&mut self, var: VarId, value: i32) -> PropId;
    
    /// At least constraint: var >= value (cardinality constraint)  
    fn atleast(&mut self, var: VarId, value: i32) -> PropId;
    
    /// Global cardinality constraint: count values in vars must match cardinalities
    fn gcc(&mut self, vars: &[VarId], values: &[i32], counts: &[VarId]) -> Vec<PropId>;
    
    /// Phase 3: Post multiple constraints with AND semantics (all must be satisfied)
    fn postall(&mut self, constraints: Vec<Constraint>) -> Vec<PropId>;
    
    /// Phase 3: Post a constraint that combines multiple constraints with AND
    fn post_and(&mut self, constraints: Vec<Constraint>) -> Option<PropId>;
    
    /// Phase 3: Post a constraint that combines multiple constraints with OR
    fn post_or(&mut self, constraints: Vec<Constraint>) -> Option<PropId>;
}

impl ModelExt for Model {
    fn post(&mut self, constraint: Constraint) -> PropId {
        post_constraint_kind(self, &constraint.kind)
    }
    
    fn c(&mut self, var: VarId) -> Builder {
        Builder::new(self, var)
    }
    
    fn alldiff(&mut self, vars: &[VarId]) -> PropId {
        // Convert slice to Vec for props method
        self.props.all_different(vars.to_vec())
    }
    
    fn alleq(&mut self, vars: &[VarId]) -> PropId {
        // Use the proper all_equal constraint implementation
        self.props.all_equal(vars.to_vec())
    }
    
    fn elem(&mut self, array: &[VarId], index: VarId, value: VarId) -> PropId {
        // Convert slice to Vec for props method
        self.props.element(array.to_vec(), index, value)
    }
    
    fn count(&mut self, vars: &[VarId], value: i32, result: VarId) -> PropId {
        // Use existing count constraint
        self.props.count_constraint(vars.to_vec(), Val::int(value), result)
    }
    
    fn betw(&mut self, var: VarId, min: i32, max: i32) -> PropId {
        // Between constraint: min <= var <= max
        // Post two constraints: var >= min AND var <= max
        self.props.greater_than_or_equals(var, Val::int(min));
        self.props.less_than_or_equals(var, Val::int(max))
    }
    
    fn atmost(&mut self, var: VarId, value: i32) -> PropId {
        // At most constraint: var <= value
        self.props.less_than_or_equals(var, Val::int(value))
    }
    
    fn atleast(&mut self, var: VarId, value: i32) -> PropId {
        // At least constraint: var >= value
        self.props.greater_than_or_equals(var, Val::int(value))
    }
    
    fn gcc(&mut self, vars: &[VarId], values: &[i32], counts: &[VarId]) -> Vec<PropId> {
        // Global cardinality constraint: count each value in vars and match cardinalities
        let mut prop_ids = Vec::new();
        
        for (&value, &count_var) in values.iter().zip(counts.iter()) {
            // For each value, create a count constraint
            let prop_id = self.props.count_constraint(vars.to_vec(), Val::int(value), count_var);
            prop_ids.push(prop_id);
        }
        
        prop_ids
    }
    
    /// Phase 3: Post multiple constraints with AND semantics (all must be satisfied)
    /// Optimized version that processes constraints in batches
    fn postall(&mut self, constraints: Vec<Constraint>) -> Vec<PropId> {
        // Pre-allocate result vector
        let mut result = Vec::with_capacity(constraints.len());
        
        // Process constraints in batches to reduce function call overhead
        for constraint in constraints {
            result.push(post_constraint_kind(self, &constraint.kind));
        }
        
        result
    }
    
    /// Phase 3: Post a constraint that combines multiple constraints with AND
    fn post_and(&mut self, constraints: Vec<Constraint>) -> Option<PropId> {
        if constraints.is_empty() {
            return None;
        }
        
        if constraints.len() == 1 {
            return Some(post_constraint_kind(self, &constraints[0].kind));
        }
        
        // Build AND constraint using the existing AND composition
        let mut result = constraints[0].clone();
        for constraint in constraints.into_iter().skip(1) {
            result = Constraint {
                kind: ConstraintKind::And(Box::new(result), Box::new(constraint))
            };
        }
        
        Some(post_constraint_kind(self, &result.kind))
    }
    
    /// Phase 3: Post a constraint that combines multiple constraints with OR
    fn post_or(&mut self, constraints: Vec<Constraint>) -> Option<PropId> {
        if constraints.is_empty() {
            return None;
        }
        
        if constraints.len() == 1 {
            return Some(post_constraint_kind(self, &constraints[0].kind));
        }
        
        // Build OR constraint using the existing OR composition
        let mut result = constraints[0].clone();
        for constraint in constraints.into_iter().skip(1) {
            result = Constraint {
                kind: ConstraintKind::Or(Box::new(result), Box::new(constraint))
            };
        }
        
        Some(post_constraint_kind(self, &result.kind))
    }
}

#[cfg(test)]
mod tests;