theory_core 0.1.0

//! Phase 2C: Performance Optimization Engine
//!
//! This module implements intelligent performance optimization including:
//! - Adaptive backend selection (CPU vs GPU vs SMT vs Neural)
//! - Workload analysis and resource allocation
//! - Dynamic parameter tuning based on constraint characteristics
//! - Performance prediction and bottleneck identification

use crate::ReasoningStrategy;
use crate::ir::{ConstraintIR, TheoryTag};
use crate::meta_reasoning::SessionPerformance;
use anyhow::Result;
use serde::{Deserialize, Serialize};
use std::collections::HashMap;
use std::time::Instant;

/// Configuration for the performance optimization engine
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct OptimizationConfig {
    /// Enable adaptive backend selection
    pub enable_backend_selection: bool,
    /// Enable dynamic parameter tuning
    pub enable_parameter_tuning: bool,
    /// Enable performance prediction
    pub enable_performance_prediction: bool,
    /// Threshold for switching backends based on performance
    pub backend_switch_threshold: f32,
    /// Maximum time to spend on optimization analysis (ms)
    pub max_analysis_time_ms: f64,
    /// Sample size for performance calibration
    pub calibration_sample_size: usize,
}

impl Default for OptimizationConfig {
    fn default() -> Self {
        Self {
            enable_backend_selection: true,
            enable_parameter_tuning: true,
            enable_performance_prediction: true,
            backend_switch_threshold: 0.3, // 30% improvement needed to switch
            max_analysis_time_ms: 50.0,
            calibration_sample_size: 100,
        }
    }
}

/// Available computation backends
#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
pub enum ComputeBackend {
    /// CPU-based computation
    CPU,
    /// GPU-accelerated computation  
    GPU,
    /// SMT solver backend
    SMT,
    /// Neural network approximation
    Neural,
    /// Hybrid approach combining multiple backends
    Hybrid {
        primary: Box<ComputeBackend>,
        fallback: Box<ComputeBackend>,
    },
}

/// Performance characteristics of a computation backend
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct BackendPerformance {
    /// Average processing time in milliseconds
    pub avg_time_ms: f64,
    /// Success rate (0.0 to 1.0)
    pub success_rate: f32,
    /// Memory usage in MB
    pub memory_usage_mb: f64,
    /// Throughput in operations per second
    pub throughput_ops_per_sec: f64,
    /// Confidence in accuracy (0.0 to 1.0)
    pub accuracy_confidence: f32,
    /// Number of samples this is based on
    pub sample_count: u32,
    /// Last updated timestamp
    pub last_updated: u64,
}

impl Default for BackendPerformance {
    fn default() -> Self {
        Self {
            avg_time_ms: 1000.0,
            success_rate: 0.7,
            memory_usage_mb: 100.0,
            throughput_ops_per_sec: 1.0,
            accuracy_confidence: 0.8,
            sample_count: 0,
            last_updated: 0,
        }
    }
}

/// Workload characteristics for optimization decisions
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct WorkloadProfile {
    /// Constraint complexity (0.0 to 1.0)
    pub complexity: f32,
    /// Number of variables
    pub variable_count: u32,
    /// Number of constraints
    pub constraint_count: u32,
    /// Theory tags involved
    pub theories: Vec<TheoryTag>,
    /// Expected computation intensity
    pub compute_intensity: ComputeIntensity,
    /// Memory requirements
    pub memory_requirements: MemoryRequirements,
    /// Time sensitivity (real-time vs batch)
    pub time_sensitivity: TimeSensitivity,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub enum ComputeIntensity {
    Light,   // Simple linear constraints
    Medium,  // Moderate nonlinear problems
    Heavy,   // Complex optimization problems
    Extreme, // Highly constrained or large-scale problems
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub enum MemoryRequirements {
    Small,  // < 10 MB
    Medium, // 10-100 MB
    Large,  // 100MB - 1GB
    Huge,   // > 1GB
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub enum TimeSensitivity {
    RealTime,    // < 10ms required
    Interactive, // < 100ms preferred
    Batch,       // seconds acceptable
    Offline,     // minutes acceptable
}

/// Optimization recommendation from the performance engine
#[derive(Debug, Clone)]
pub struct OptimizationRecommendation {
    /// Recommended backend
    pub backend: ComputeBackend,
    /// Recommended reasoning strategy
    pub strategy: ReasoningStrategy,
    /// Optimized parameters
    pub parameters: OptimizationParameters,
    /// Confidence in recommendation (0.0 to 1.0)
    pub confidence: f32,
    /// Reasoning for the recommendation
    pub reasoning: String,
    /// Expected performance metrics
    pub expected_performance: ExpectedPerformance,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct OptimizationParameters {
    /// Timeout for computation (milliseconds)
    pub timeout_ms: f64,
    /// Parallel worker threads
    pub worker_threads: u32,
    /// Memory budget (MB)
    pub memory_budget_mb: f64,
    /// Precision requirements
    pub precision_level: PrecisionLevel,
    /// Caching strategy
    pub caching_strategy: CachingStrategy,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub enum PrecisionLevel {
    Low,    // Fast approximation
    Medium, // Balanced accuracy
    High,   // Maximum precision
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub enum CachingStrategy {
    None,       // No caching
    Aggressive, // Cache everything
    Selective,  // Cache based on cost/benefit
    Adaptive,   // Learn optimal caching
}

#[derive(Debug, Clone)]
pub struct ExpectedPerformance {
    pub estimated_time_ms: f64,
    pub success_probability: f32,
    pub memory_usage_mb: f64,
    pub accuracy_confidence: f32,
}

/// Performance optimization engine
pub struct PerformanceOptimizer {
    config: OptimizationConfig,
    backend_stats: HashMap<ComputeBackend, BackendPerformance>,
    workload_history: Vec<(WorkloadProfile, SessionPerformance)>,
    parameter_tuner: ParameterTuner,
    backend_selector: BackendSelector,
}

impl PerformanceOptimizer {
    pub fn new(config: OptimizationConfig) -> Self {
        Self {
            config,
            backend_stats: HashMap::new(),
            workload_history: Vec::new(),
            parameter_tuner: ParameterTuner::new(),
            backend_selector: BackendSelector::new(),
        }
    }

    /// Analyze constraints and recommend optimal configuration
    pub fn optimize(
        &mut self,
        constraints: &ConstraintIR,
        verbose: bool,
    ) -> Result<OptimizationRecommendation> {
        let start_time = Instant::now();

        if verbose {
            println!("🚀 Performance Optimizer: Analyzing constraints...");
        }

        // 1. Profile the workload
        let profile = self.analyze_workload(constraints)?;

        if verbose {
            println!(
                "   Workload: {} variables, {} constraints, complexity {:.2}",
                profile.variable_count, profile.constraint_count, profile.complexity
            );
        }

        // 2. Select optimal backend based on workload characteristics
        let backend = if self.config.enable_backend_selection {
            match (&profile.compute_intensity, profile.variable_count) {
                (ComputeIntensity::Light, _) => ComputeBackend::CPU,
                (ComputeIntensity::Medium, v) if v > 10 => ComputeBackend::GPU,
                (ComputeIntensity::Heavy, _) => ComputeBackend::GPU,
                (ComputeIntensity::Extreme, _) => ComputeBackend::GPU,
                _ => {
                    // Use theory tags to decide
                    if profile.theories.contains(&TheoryTag::NLA)
                        || profile.theories.contains(&TheoryTag::BV)
                    {
                        ComputeBackend::GPU // Nonlinear and bitvector benefit from parallel computation
                    } else {
                        ComputeBackend::CPU
                    }
                }
            }
        } else {
            ComputeBackend::CPU // Default fallback
        };

        if verbose {
            println!("   Recommended backend: {:?}", backend);
        }

        // 3. Tune parameters for this workload
        let parameters = if self.config.enable_parameter_tuning {
            self.parameter_tuner
                .tune_parameters(&profile, &backend, &self.workload_history)?
        } else {
            OptimizationParameters::default(&profile)
        };

        // 4. Predict performance
        let expected_performance = if self.config.enable_performance_prediction {
            self.predict_performance(&profile, &backend, &parameters)?
        } else {
            ExpectedPerformance::default()
        };

        // 5. Select reasoning strategy
        let strategy = self.select_strategy(&profile, &backend)?;

        let elapsed = start_time.elapsed().as_millis() as f64;
        if verbose {
            println!("   Optimization analysis completed in {:.1}ms", elapsed);
        }

        Ok(OptimizationRecommendation {
            backend,
            strategy,
            parameters,
            confidence: 0.85, // TODO: Compute based on data quality
            reasoning: format!(
                "Selected based on workload analysis: {:?} complexity, {:?} time sensitivity",
                profile.compute_intensity, profile.time_sensitivity
            ),
            expected_performance,
        })
    }

    /// Record actual performance for learning
    pub fn record_performance(
        &mut self,
        constraints: &ConstraintIR,
        backend: &ComputeBackend,
        performance: &SessionPerformance,
    ) -> Result<()> {
        let profile = self.analyze_workload(constraints)?;

        // Update backend statistics
        {
            let stats = self.backend_stats.entry(backend.clone()).or_default();
            let alpha = 0.1f64; // Learning rate
            stats.avg_time_ms =
                (1.0 - alpha) * stats.avg_time_ms + alpha * performance.total_solve_time_ms;
            stats.success_rate = ((1.0 - alpha) * stats.success_rate as f64
                + alpha * if performance.success { 1.0 } else { 0.0 })
                as f32;
            stats.accuracy_confidence = ((1.0 - alpha) * stats.accuracy_confidence as f64
                + alpha * performance.confidence_achieved as f64)
                as f32;
            stats.sample_count += 1;
            stats.last_updated = std::time::SystemTime::now()
                .duration_since(std::time::UNIX_EPOCH)
                .unwrap_or_default()
                .as_secs();
        }

        // Add to workload history
        self.workload_history.push((profile, performance.clone()));

        // Keep history bounded
        if self.workload_history.len() > self.config.calibration_sample_size {
            self.workload_history.remove(0);
        }

        // Note: verbose parameter removed - callers should print if needed

        Ok(())
    }

    fn analyze_workload(&self, constraints: &ConstraintIR) -> Result<WorkloadProfile> {
        let variable_count = constraints.variables.len() as u32;
        let constraint_count = constraints.constraints.len() as u32;

        // Compute complexity based on problem characteristics
        let complexity = self.compute_complexity(constraints);

        // Determine compute intensity
        let compute_intensity = match (variable_count, constraint_count, complexity) {
            (v, c, _) if v <= 5 && c <= 3 => ComputeIntensity::Light,
            (v, c, x) if v <= 20 && c <= 10 && x < 0.5 => ComputeIntensity::Medium,
            (v, c, x) if v <= 100 && c <= 50 && x < 0.8 => ComputeIntensity::Heavy,
            _ => ComputeIntensity::Extreme,
        };

        // Estimate memory requirements
        let memory_requirements = match variable_count + constraint_count {
            n if n <= 10 => MemoryRequirements::Small,
            n if n <= 100 => MemoryRequirements::Medium,
            n if n <= 1000 => MemoryRequirements::Large,
            _ => MemoryRequirements::Huge,
        };

        // Default to interactive for now
        let time_sensitivity = TimeSensitivity::Interactive;

        Ok(WorkloadProfile {
            complexity,
            variable_count,
            constraint_count,
            theories: constraints.theory_tags.to_vec(),
            compute_intensity,
            memory_requirements,
            time_sensitivity,
        })
    }

    fn compute_complexity(&self, constraints: &ConstraintIR) -> f32 {
        let var_factor = (constraints.variables.len() as f32).ln() / 10.0;
        let constraint_factor = (constraints.constraints.len() as f32).ln() / 5.0;

        // Theory complexity weights
        let theory_complexity: f32 = constraints
            .theory_tags
            .iter()
            .map(|tag| match tag {
                TheoryTag::LIA | TheoryTag::LRA => 0.2,
                TheoryTag::NLA => 0.8,
                TheoryTag::BV => 0.4,
                TheoryTag::Array => 0.6,
                TheoryTag::String => 0.5,
                _ => 0.3,
            })
            .sum();

        ((var_factor + constraint_factor + theory_complexity) / 3.0).min(1.0)
    }

    fn select_strategy(
        &self,
        profile: &WorkloadProfile,
        backend: &ComputeBackend,
    ) -> Result<ReasoningStrategy> {
        match (
            backend,
            &profile.time_sensitivity,
            &profile.compute_intensity,
        ) {
            (ComputeBackend::Neural, _, _) => Ok(ReasoningStrategy::Speculate),
            (ComputeBackend::SMT, _, _) => Ok(ReasoningStrategy::Verify),
            (_, TimeSensitivity::RealTime, _) => Ok(ReasoningStrategy::Speculate),
            (_, _, ComputeIntensity::Extreme) => Ok(ReasoningStrategy::Verify),
            _ => Ok(ReasoningStrategy::Hybrid),
        }
    }

    fn predict_performance(
        &self,
        profile: &WorkloadProfile,
        backend: &ComputeBackend,
        parameters: &OptimizationParameters,
    ) -> Result<ExpectedPerformance> {
        // Apply parameter-based adjustments
        let timeout_factor = if parameters.timeout_ms > 0.0 {
            1.0 + (parameters.timeout_ms / 1000.0).ln() / 10.0
        } else {
            1.0
        };

        let parallel_factor = if parameters.worker_threads > 1 {
            0.7 // Parallel execution improves performance
        } else {
            1.0
        };

        // Use historical data if available
        if let Some(stats) = self.backend_stats.get(backend) {
            let complexity_factor = 1.0 + profile.complexity as f64;
            let size_factor = 1.0 + (profile.variable_count as f64).ln() / 10.0;

            Ok(ExpectedPerformance {
                estimated_time_ms: stats.avg_time_ms
                    * complexity_factor
                    * size_factor
                    * timeout_factor
                    * parallel_factor,
                success_probability: stats.success_rate,
                memory_usage_mb: stats.memory_usage_mb * size_factor,
                accuracy_confidence: stats.accuracy_confidence,
            })
        } else {
            // Fallback estimates with parameter adjustments
            let mut fallback = ExpectedPerformance::default();
            fallback.estimated_time_ms *= timeout_factor * parallel_factor;
            Ok(fallback)
        }
    }
}

impl OptimizationParameters {
    fn default(profile: &WorkloadProfile) -> Self {
        let timeout_ms = match profile.compute_intensity {
            ComputeIntensity::Light => 100.0,
            ComputeIntensity::Medium => 1000.0,
            ComputeIntensity::Heavy => 5000.0,
            ComputeIntensity::Extreme => 30000.0,
        };

        let worker_threads = match profile.compute_intensity {
            ComputeIntensity::Light => 1,
            ComputeIntensity::Medium => 2,
            ComputeIntensity::Heavy => 4,
            ComputeIntensity::Extreme => 8,
        };

        let memory_budget_mb = match profile.memory_requirements {
            MemoryRequirements::Small => 50.0,
            MemoryRequirements::Medium => 200.0,
            MemoryRequirements::Large => 1000.0,
            MemoryRequirements::Huge => 4000.0,
        };

        Self {
            timeout_ms,
            worker_threads,
            memory_budget_mb,
            precision_level: PrecisionLevel::Medium,
            caching_strategy: CachingStrategy::Selective,
        }
    }
}

impl Default for ExpectedPerformance {
    fn default() -> Self {
        Self {
            estimated_time_ms: 1000.0,
            success_probability: 0.8,
            memory_usage_mb: 100.0,
            accuracy_confidence: 0.85,
        }
    }
}

/// Parameter tuning component
pub struct ParameterTuner {
    // Placeholder for ML-based parameter tuning
}

impl ParameterTuner {
    pub fn new() -> Self {
        Self {}
    }

    pub fn tune_parameters(
        &self,
        profile: &WorkloadProfile,
        _backend: &ComputeBackend,
        history: &[(WorkloadProfile, SessionPerformance)],
    ) -> Result<OptimizationParameters> {
        // Find similar workloads in history
        let similar_workloads: Vec<_> = history
            .iter()
            .filter(|(p, _)| self.workload_similarity(profile, p) > 0.7)
            .collect();

        if similar_workloads.is_empty() {
            return Ok(OptimizationParameters::default(profile));
        }

        // Analyze what parameters worked best
        let avg_success_rate: f32 = similar_workloads
            .iter()
            .map(|(_, perf)| if perf.success { 1.0 } else { 0.0 })
            .sum::<f32>()
            / similar_workloads.len() as f32;

        let avg_time: f64 = similar_workloads
            .iter()
            .map(|(_, perf)| perf.total_solve_time_ms)
            .sum::<f64>()
            / similar_workloads.len() as f64;

        // Adjust parameters based on historical performance
        let mut params = OptimizationParameters::default(profile);

        if avg_success_rate < 0.7 {
            // Increase timeout and resources for better success rate
            params.timeout_ms *= 1.5;
            params.worker_threads = (params.worker_threads * 2).min(16);
        }

        if avg_time > 5000.0 {
            // Problem tends to be slow, prepare accordingly
            params.precision_level = PrecisionLevel::Medium;
            params.caching_strategy = CachingStrategy::Aggressive;
        }

        Ok(params)
    }

    fn workload_similarity(&self, a: &WorkloadProfile, b: &WorkloadProfile) -> f32 {
        let complexity_sim = 1.0 - (a.complexity - b.complexity).abs();
        let var_sim = 1.0
            - ((a.variable_count as f32 - b.variable_count as f32).abs()
                / a.variable_count.max(b.variable_count).max(1) as f32);
        let theory_sim = self.theory_similarity(&a.theories, &b.theories);

        (complexity_sim + var_sim + theory_sim) / 3.0
    }

    fn theory_similarity(&self, a: &[TheoryTag], b: &[TheoryTag]) -> f32 {
        if a.is_empty() && b.is_empty() {
            return 1.0;
        }

        let intersection: usize = a.iter().filter(|tag| b.contains(tag)).count();
        let union: usize = a.len() + b.len() - intersection;

        if union == 0 {
            1.0
        } else {
            intersection as f32 / union as f32
        }
    }
}

/// Backend selection component with intelligent routing
pub struct BackendSelector {
    /// Performance history for each backend
    backend_stats: HashMap<ComputeBackend, BackendPerformance>,
    /// System capabilities (GPU availability, etc.)
    gpu_available: bool,
    /// SMT solver availability
    smt_available: bool,
}

impl Default for BackendSelector {
    fn default() -> Self {
        Self::new()
    }
}

impl BackendSelector {
    pub fn new() -> Self {
        // Detect system capabilities
        let gpu_available = Self::detect_gpu();
        let smt_available = Self::detect_smt();

        Self {
            backend_stats: HashMap::new(),
            gpu_available,
            smt_available,
        }
    }

    /// Detect if GPU is available
    fn detect_gpu() -> bool {
        // Check if WGPU can create an adapter
        #[cfg(feature = "gpu")]
        {
            // In real implementation, we'd try to create a WGPU adapter
            // For now, assume GPU might be available
            true
        }
        #[cfg(not(feature = "gpu"))]
        {
            false
        }
    }

    /// Detect if SMT solver is available
    fn detect_smt() -> bool {
        #[cfg(feature = "z3-solver")]
        {
            true
        }
        #[cfg(not(feature = "z3-solver"))]
        {
            false
        }
    }

    /// Update performance statistics for a backend
    pub fn update_stats(&mut self, backend: ComputeBackend, perf: BackendPerformance) {
        self.backend_stats.insert(backend, perf);
    }

    pub fn select_backend(&self, profile: &WorkloadProfile) -> Result<ComputeBackend> {
        // Use instance stats and system capabilities
        let stats = &self.backend_stats;

        // Calculate problem size score
        let problem_size = profile.variable_count * profile.constraint_count;

        // Rule-based selection with performance history and system capabilities
        match (&profile.time_sensitivity, &profile.compute_intensity) {
            (TimeSensitivity::RealTime, _) => {
                // Prefer fastest backends for real-time
                if self.is_fast_enough(&ComputeBackend::Neural, stats, 10.0) {
                    Ok(ComputeBackend::Neural)
                } else {
                    Ok(ComputeBackend::CPU)
                }
            }
            (TimeSensitivity::Interactive, ComputeIntensity::Light) => {
                // Light workload - CPU is fine
                Ok(ComputeBackend::CPU)
            }
            (TimeSensitivity::Interactive, ComputeIntensity::Medium) => {
                // Medium workload - use GPU if available and problem is large enough
                if self.gpu_available
                    && problem_size > 500
                    && self.is_available(&ComputeBackend::GPU, stats)
                {
                    Ok(ComputeBackend::GPU)
                } else {
                    Ok(ComputeBackend::CPU)
                }
            }
            (_, ComputeIntensity::Heavy | ComputeIntensity::Extreme) => {
                // Heavy workloads - prefer SMT solver for accuracy on nonlinear problems
                if self.smt_available && profile.theories.contains(&TheoryTag::NLA) {
                    Ok(ComputeBackend::SMT)
                } else if self.gpu_available && problem_size > 1000 {
                    // Large problem - use GPU with CPU fallback
                    Ok(ComputeBackend::Hybrid {
                        primary: Box::new(ComputeBackend::GPU),
                        fallback: Box::new(ComputeBackend::CPU),
                    })
                } else {
                    Ok(ComputeBackend::CPU)
                }
            }
            _ => Ok(ComputeBackend::CPU), // Safe default
        }
    }

    fn is_fast_enough(
        &self,
        backend: &ComputeBackend,
        stats: &HashMap<ComputeBackend, BackendPerformance>,
        threshold_ms: f64,
    ) -> bool {
        stats
            .get(backend)
            .map(|s| s.avg_time_ms < threshold_ms)
            .unwrap_or(false)
    }

    fn is_available(
        &self,
        backend: &ComputeBackend,
        stats: &HashMap<ComputeBackend, BackendPerformance>,
    ) -> bool {
        stats
            .get(backend)
            .map(|s| s.success_rate > 0.5)
            .unwrap_or(false)
    }
}