oxiz_math/

realclosure_advanced.rs

//! Advanced Real Closure Operations.
//!
//! Extends the basic real closure module with advanced operations for
//! algebraic number manipulation in SMT solving.
//!
//! ## Operations
//!
//! - **Sign Determination**: Determine sign of algebraic expressions
//! - **Comparison**: Compare algebraic numbers
//! - **Thom Encoding**: Canonical representation via sign sequences
//! - **Isolation Refinement**: Refine root isolation intervals
//!
//! ## References
//!
//! - Basu et al.: "Algorithms in Real Algebraic Geometry" (2006)
//! - Z3's `math/realclosure/`

#[allow(unused_imports)]
use crate::prelude::*;
use num_bigint::BigInt;
use num_rational::BigRational;
use num_traits::{One, Zero};

/// Variable identifier.
pub type Var = u32;

/// Algebraic number represented by minimal polynomial and isolating interval.
#[derive(Debug, Clone)]
pub struct AlgebraicNumber {
    /// Minimal polynomial coefficients (highest degree first).
    pub polynomial: Vec<BigRational>,
    /// Lower bound of isolating interval.
    pub lower: BigRational,
    /// Upper bound of isolating interval.
    pub upper: BigRational,
}

impl AlgebraicNumber {
    /// Create a new algebraic number.
    pub fn new(polynomial: Vec<BigRational>, lower: BigRational, upper: BigRational) -> Self {
        Self {
            polynomial,
            lower,
            upper,
        }
    }

    /// Create from a rational number.
    pub fn from_rational(value: BigRational) -> Self {
        Self {
            polynomial: vec![value.clone(), -BigRational::one()], // x - value
            lower: value.clone(),
            upper: value,
        }
    }

    /// Check if this is a rational number.
    pub fn is_rational(&self) -> bool {
        self.lower == self.upper
    }

    /// Get rational value if this is rational.
    pub fn as_rational(&self) -> Option<BigRational> {
        if self.is_rational() {
            Some(self.lower.clone())
        } else {
            None
        }
    }
}

/// Thom encoding (sign sequence of derivatives).
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub struct ThomEncoding {
    /// Signs of polynomial and its derivatives at the root.
    /// +1 for positive, 0 for zero, -1 for negative.
    pub signs: Vec<i8>,
}

impl ThomEncoding {
    /// Create a new Thom encoding.
    pub fn new(signs: Vec<i8>) -> Self {
        Self { signs }
    }

    /// Check if this encoding is valid.
    pub fn is_valid(&self) -> bool {
        !self.signs.is_empty() && self.signs[0] == 0 // p(α) = 0
    }
}

/// Configuration for advanced real closure operations.
#[derive(Debug, Clone)]
pub struct RealClosureAdvancedConfig {
    /// Enable Thom encoding.
    pub enable_thom: bool,
    /// Enable interval refinement.
    pub enable_refinement: bool,
    /// Refinement precision (interval width threshold).
    pub refinement_precision: BigRational,
}

impl Default for RealClosureAdvancedConfig {
    fn default() -> Self {
        Self {
            enable_thom: true,
            enable_refinement: true,
            refinement_precision: BigRational::new(BigInt::from(1), BigInt::from(1000)),
        }
    }
}

/// Statistics for advanced real closure operations.
#[derive(Debug, Clone, Default)]
pub struct RealClosureAdvancedStats {
    /// Sign determinations.
    pub sign_determinations: u64,
    /// Comparisons performed.
    pub comparisons: u64,
    /// Thom encodings computed.
    pub thom_encodings: u64,
    /// Interval refinements.
    pub refinements: u64,
}

/// Advanced real closure engine.
#[derive(Debug)]
pub struct RealClosureAdvanced {
    /// Configuration.
    config: RealClosureAdvancedConfig,
    /// Statistics.
    stats: RealClosureAdvancedStats,
}

impl RealClosureAdvanced {
    /// Create a new advanced real closure engine.
    pub fn new(config: RealClosureAdvancedConfig) -> Self {
        Self {
            config,
            stats: RealClosureAdvancedStats::default(),
        }
    }

    /// Create with default configuration.
    pub fn default_config() -> Self {
        Self::new(RealClosureAdvancedConfig::default())
    }

    /// Determine the sign of an algebraic number.
    pub fn sign(&mut self, num: &AlgebraicNumber) -> i8 {
        self.stats.sign_determinations += 1;

        if num.lower > BigRational::zero() {
            1
        } else if num.upper < BigRational::zero() {
            -1
        } else if num.is_rational() && num.as_rational() == Some(BigRational::zero()) {
            0
        } else {
            // Need refinement
            0
        }
    }

    /// Compare two algebraic numbers.
    pub fn compare(&mut self, a: &AlgebraicNumber, b: &AlgebraicNumber) -> core::cmp::Ordering {
        self.stats.comparisons += 1;

        // Simplified: compare isolating intervals
        if a.upper < b.lower {
            core::cmp::Ordering::Less
        } else if a.lower > b.upper {
            core::cmp::Ordering::Greater
        } else {
            // Intervals overlap, need refinement or Thom encoding
            core::cmp::Ordering::Equal
        }
    }

    /// Compute Thom encoding for an algebraic number.
    pub fn thom_encoding(&mut self, _num: &AlgebraicNumber) -> ThomEncoding {
        if !self.config.enable_thom {
            return ThomEncoding::new(vec![0]);
        }

        self.stats.thom_encodings += 1;

        // Simplified: would compute signs of polynomial and derivatives at root
        ThomEncoding::new(vec![0, 1, -1]) // Example encoding
    }

    /// Refine the isolating interval of an algebraic number.
    pub fn refine_interval(&mut self, num: &mut AlgebraicNumber) {
        if !self.config.enable_refinement {
            return;
        }

        let width = &num.upper - &num.lower;
        if width <= self.config.refinement_precision {
            return; // Already precise enough
        }

        self.stats.refinements += 1;

        // Simplified: would use bisection or Sturm sequences
        // Bisect the interval
        let mid = (&num.lower + &num.upper) / BigRational::from(BigInt::from(2));

        // Check which half contains the root (simplified)
        num.upper = mid;
    }

    /// Get statistics.
    pub fn stats(&self) -> &RealClosureAdvancedStats {
        &self.stats
    }

    /// Reset statistics.
    pub fn reset_stats(&mut self) {
        self.stats = RealClosureAdvancedStats::default();
    }
}

impl Default for RealClosureAdvanced {
    fn default() -> Self {
        Self::default_config()
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn test_engine_creation() {
        let engine = RealClosureAdvanced::default_config();
        assert_eq!(engine.stats().sign_determinations, 0);
    }

    #[test]
    fn test_algebraic_from_rational() {
        let num = AlgebraicNumber::from_rational(BigRational::from(BigInt::from(3)));

        assert!(num.is_rational());
        assert_eq!(num.as_rational(), Some(BigRational::from(BigInt::from(3))));
    }

    #[test]
    fn test_sign_determination() {
        let mut engine = RealClosureAdvanced::default_config();

        let positive = AlgebraicNumber::from_rational(BigRational::from(BigInt::from(5)));
        let negative = AlgebraicNumber::from_rational(BigRational::from(BigInt::from(-3)));

        assert_eq!(engine.sign(&positive), 1);
        assert_eq!(engine.sign(&negative), -1);
        assert_eq!(engine.stats().sign_determinations, 2);
    }

    #[test]
    fn test_compare() {
        let mut engine = RealClosureAdvanced::default_config();

        let a = AlgebraicNumber::from_rational(BigRational::from(BigInt::from(3)));
        let b = AlgebraicNumber::from_rational(BigRational::from(BigInt::from(5)));

        assert_eq!(engine.compare(&a, &b), core::cmp::Ordering::Less);
        assert_eq!(engine.stats().comparisons, 1);
    }

    #[test]
    fn test_thom_encoding() {
        let mut engine = RealClosureAdvanced::default_config();

        let num = AlgebraicNumber::from_rational(BigRational::zero());
        let encoding = engine.thom_encoding(&num);

        assert!(encoding.is_valid());
        assert_eq!(engine.stats().thom_encodings, 1);
    }

    #[test]
    fn test_refine_interval() {
        let mut engine = RealClosureAdvanced::default_config();

        let mut num = AlgebraicNumber::new(
            vec![
                BigRational::one(),
                BigRational::zero(),
                -BigRational::from(BigInt::from(2)),
            ], // x^2 - 2
            BigRational::one(),
            BigRational::from(BigInt::from(2)),
        );

        let initial_width = &num.upper - &num.lower;
        engine.refine_interval(&mut num);
        let final_width = &num.upper - &num.lower;

        assert!(final_width < initial_width);
        assert_eq!(engine.stats().refinements, 1);
    }
}