theory_core 0.1.0

//! Phase 2B-2: Meta-Reasoning Engine
//!
//! This module implements a meta-reasoning system that reasons about reasoning strategies,
//! analyzes their effectiveness, and makes intelligent decisions about which approach
//! to use for different types of constraint problems.

use crate::ir::{ConstraintIR, Domain, TheoryTag};
use crate::learning::{ConstraintLearner, LearningStats};
use crate::{ReasoningStrategy, SolutionResult};
use anyhow::Result;
use serde::{Deserialize, Serialize};
use std::collections::{HashMap, VecDeque};

/// Configuration for the meta-reasoning engine
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct MetaReasoningConfig {
    /// Maximum history of reasoning sessions to track
    pub max_session_history: usize,
    /// Minimum confidence threshold for strategy recommendations
    pub min_strategy_confidence: f32,
    /// Learning rate for strategy performance updates
    pub strategy_learning_rate: f32,
    /// Enable predictive performance modeling
    pub enable_prediction: bool,
    /// Threshold for switching to adaptive strategies
    pub adaptation_threshold: f32,
}

impl Default for MetaReasoningConfig {
    fn default() -> Self {
        Self {
            max_session_history: 500,
            min_strategy_confidence: 0.75,
            strategy_learning_rate: 0.02,
            enable_prediction: true,
            adaptation_threshold: 0.6,
        }
    }
}

/// Record of a complete reasoning session including meta-analysis
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ReasoningSession {
    /// Unique session identifier
    pub session_id: String,
    /// Input constraints
    pub constraints: ConstraintIR,
    /// Strategy that was used
    pub strategy_used: ReasoningStrategy,
    /// Alternative strategies that were considered
    pub strategies_considered: Vec<ReasoningStrategy>,
    /// Actual solution obtained
    pub solution: SolutionResult,
    /// Performance metrics
    pub performance: SessionPerformance,
    /// Meta-analysis of the session
    pub meta_analysis: MetaAnalysis,
    /// Timestamp
    pub timestamp: u64,
}

/// Performance metrics for a reasoning session
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct SessionPerformance {
    pub total_solve_time_ms: f64,
    pub neural_time_ms: f64,
    pub smt_time_ms: f64,
    pub confidence_achieved: f32,
    pub success: bool,
    pub iterations_required: u32,
}

/// Meta-analysis of reasoning effectiveness
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct MetaAnalysis {
    /// Was the chosen strategy optimal?
    pub strategy_optimality: StrategyOptimality,
    /// Predicted vs actual performance
    pub performance_prediction_error: f32,
    /// Factors that influenced performance
    pub performance_factors: Vec<PerformanceFactor>,
    /// Lessons learned for future sessions
    pub insights: Vec<String>,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub enum StrategyOptimality {
    /// Strategy was optimal given available information
    Optimal,
    /// A better strategy was available and should have been chosen
    Suboptimal {
        better_strategy: ReasoningStrategy,
        estimated_improvement: f32,
    },
    /// Strategy was reasonable but not clearly optimal or suboptimal
    Acceptable,
    /// Not enough information to determine optimality
    Unknown,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct PerformanceFactor {
    pub factor_name: String,
    pub impact_score: f32, // -1.0 to 1.0
    pub confidence: f32,   // 0.0 to 1.0
}

/// Strategic recommendation from meta-reasoning analysis
#[derive(Debug, Clone)]
pub struct StrategyRecommendation {
    pub recommended_strategy: ReasoningStrategy,
    pub confidence: f32,
    pub predicted_performance: PredictedPerformance,
    pub reasoning: String,
    pub alternatives: Vec<(ReasoningStrategy, f32)>, // (strategy, confidence)
}

#[derive(Debug, Clone)]
pub struct PredictedPerformance {
    pub estimated_solve_time_ms: f64,
    pub estimated_confidence: f32,
    pub success_probability: f32,
}

/// Learned patterns about strategy effectiveness
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct StrategyPattern {
    pub pattern_id: String,
    pub constraint_characteristics: ConstraintCharacteristics,
    pub best_strategy: ReasoningStrategy,
    pub performance_statistics: StrategyPerformanceStats,
    pub confidence: f32,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ConstraintCharacteristics {
    pub variable_count: u32,
    pub constraint_count: u32,
    pub domain_types: Vec<String>,
    pub theory_tags: Vec<TheoryTag>,
    pub complexity_estimate: f32,
    pub nonlinearity_score: f32,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct StrategyPerformanceStats {
    pub avg_solve_time_ms: f64,
    pub avg_confidence: f32,
    pub success_rate: f32,
    pub sample_count: u32,
}

/// Meta-reasoning engine that analyzes and improves reasoning strategies
pub struct MetaReasoningEngine {
    config: MetaReasoningConfig,
    session_history: VecDeque<ReasoningSession>,
    strategy_patterns: HashMap<String, StrategyPattern>,
    strategy_performance: HashMap<ReasoningStrategy, StrategyPerformanceStats>,
    constraint_learner: ConstraintLearner,
}

impl MetaReasoningEngine {
    pub fn new(config: MetaReasoningConfig, constraint_learner: ConstraintLearner) -> Self {
        let max_history = config.max_session_history;
        Self {
            config,
            session_history: VecDeque::with_capacity(max_history),
            strategy_patterns: HashMap::new(),
            strategy_performance: HashMap::new(),
            constraint_learner,
        }
    }

    /// Analyze constraints and recommend the best reasoning strategy
    pub fn recommend_strategy(
        &self,
        constraints: &ConstraintIR,
        verbose: bool,
    ) -> Result<StrategyRecommendation> {
        let characteristics = self.extract_characteristics(constraints)?;

        if verbose {
            println!("🤔 Meta-reasoning: Analyzing constraint characteristics...");
            println!(
                "   Variables: {}, Constraints: {}",
                characteristics.variable_count, characteristics.constraint_count
            );
            println!(
                "   Complexity: {:.2}, Theories: {:?}",
                characteristics.complexity_estimate, characteristics.theory_tags
            );
        }

        // Check for known patterns
        if let Some(pattern) = self.find_matching_pattern(&characteristics) {
            return Ok(StrategyRecommendation {
                recommended_strategy: pattern.best_strategy.clone(),
                confidence: pattern.confidence,
                predicted_performance: PredictedPerformance {
                    estimated_solve_time_ms: pattern.performance_statistics.avg_solve_time_ms,
                    estimated_confidence: pattern.performance_statistics.avg_confidence,
                    success_probability: pattern.performance_statistics.success_rate,
                },
                reasoning: format!(
                    "Based on learned pattern '{}' with {:.1}% confidence",
                    pattern.pattern_id,
                    pattern.confidence * 100.0
                ),
                alternatives: self.get_alternative_strategies(&pattern.best_strategy),
            });
        }

        // Fallback to heuristic-based recommendation
        let strategy = self.heuristic_strategy_selection(&characteristics)?;
        let predicted_perf = self.predict_performance(&strategy, &characteristics)?;

        Ok(StrategyRecommendation {
            recommended_strategy: strategy.clone(),
            confidence: 0.5, // Lower confidence for heuristic-based
            predicted_performance: predicted_perf,
            reasoning: "Based on heuristic analysis (no matching patterns found)".to_string(),
            alternatives: self.get_alternative_strategies(&strategy),
        })
    }

    /// Record and analyze a completed reasoning session
    pub fn record_session(
        &mut self,
        session_id: String,
        constraints: ConstraintIR,
        strategy_used: ReasoningStrategy,
        strategies_considered: Vec<ReasoningStrategy>,
        solution: SolutionResult,
        performance: SessionPerformance,
    ) -> Result<()> {
        // Perform meta-analysis
        let meta_analysis = self.analyze_session_effectiveness(
            &constraints,
            &strategy_used,
            &strategies_considered,
            &solution,
            &performance,
        )?;

        let session = ReasoningSession {
            session_id: session_id.clone(),
            constraints: constraints.clone(),
            strategy_used: strategy_used.clone(),
            strategies_considered,
            solution,
            performance: performance.clone(),
            meta_analysis,
            timestamp: std::time::SystemTime::now()
                .duration_since(std::time::UNIX_EPOCH)?
                .as_secs(),
        };

        // Add to history
        if self.session_history.len() >= self.config.max_session_history {
            self.session_history.pop_front();
        }
        self.session_history.push_back(session.clone());

        // Update strategy performance statistics
        self.update_strategy_performance(&strategy_used, &performance)?;

        // Update constraint learner
        self.constraint_learner.record_solution(
            constraints,
            session.solution,
            performance.total_solve_time_ms,
            format!("{:?}", strategy_used),
        )?;

        // Extract new patterns if we have enough data
        if self.session_history.len() >= 20 {
            self.update_strategy_patterns()?;
        }

        // Note: verbose parameter comes from outer scope when this is called from record_session()
        // The full record_session() above has different parameters

        Ok(())
    }

    /// Get meta-reasoning insights and statistics
    pub fn get_insights(&self) -> MetaReasoningInsights {
        let total_sessions = self.session_history.len();

        let strategy_success_rates: HashMap<ReasoningStrategy, f32> = self
            .strategy_performance
            .iter()
            .map(|(strategy, stats)| (strategy.clone(), stats.success_rate))
            .collect();

        let avg_optimality = self
            .session_history
            .iter()
            .map(|s| match &s.meta_analysis.strategy_optimality {
                StrategyOptimality::Optimal => 1.0,
                StrategyOptimality::Acceptable => 0.7,
                StrategyOptimality::Suboptimal { .. } => 0.3,
                StrategyOptimality::Unknown => 0.5,
            })
            .sum::<f32>()
            / total_sessions as f32;

        let learning_stats = self.constraint_learner.get_learning_stats();

        MetaReasoningInsights {
            total_sessions,
            patterns_discovered: self.strategy_patterns.len(),
            strategy_success_rates,
            average_optimality_score: avg_optimality,
            constraint_learning_stats: learning_stats,
            most_effective_strategy: self.find_most_effective_strategy(),
        }
    }

    // Helper methods

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

        let domain_types: Vec<String> = constraints
            .variables
            .values()
            .map(|var| match &var.domain {
                Domain::Boolean => "Boolean".to_string(),
                Domain::Integer { .. } => "Integer".to_string(),
                Domain::Real { .. } => "Real".to_string(),
                Domain::BitVector { .. } => "BitVector".to_string(),
                Domain::String { .. } => "String".to_string(),
                Domain::Array { .. } => "Array".to_string(),
                Domain::Enum { .. } => "Enum".to_string(),
            })
            .collect();

        // Simple complexity heuristic
        let complexity_estimate =
            (variable_count as f32 * 0.1 + constraint_count as f32 * 0.2).min(1.0);

        // Simple nonlinearity score (placeholder)
        let nonlinearity_score = if constraints.theory_tags.contains(&TheoryTag::NLA) {
            0.8
        } else {
            0.2
        };

        Ok(ConstraintCharacteristics {
            variable_count,
            constraint_count,
            domain_types,
            theory_tags: constraints.theory_tags.to_vec(),
            complexity_estimate,
            nonlinearity_score,
        })
    }

    fn find_matching_pattern(
        &self,
        characteristics: &ConstraintCharacteristics,
    ) -> Option<&StrategyPattern> {
        // Simple pattern matching based on similar characteristics
        self.strategy_patterns
            .values()
            .filter(|pattern| {
                // Match if variable counts are similar (within 50%)
                let var_diff = (pattern.constraint_characteristics.variable_count as f32
                    - characteristics.variable_count as f32)
                    .abs();
                let var_similarity =
                    1.0 - (var_diff / characteristics.variable_count.max(1) as f32);

                // Match if theory tags overlap
                let theory_overlap = characteristics
                    .theory_tags
                    .iter()
                    .any(|tag| pattern.constraint_characteristics.theory_tags.contains(tag));

                var_similarity > 0.5 && (theory_overlap || characteristics.theory_tags.is_empty())
            })
            .max_by(|a, b| {
                a.confidence
                    .partial_cmp(&b.confidence)
                    .unwrap_or(std::cmp::Ordering::Equal)
            })
    }

    fn heuristic_strategy_selection(
        &self,
        characteristics: &ConstraintCharacteristics,
    ) -> Result<ReasoningStrategy> {
        // Simple heuristics for strategy selection
        if characteristics.complexity_estimate < 0.3 && characteristics.variable_count <= 5 {
            Ok(ReasoningStrategy::Speculate)
        } else if characteristics.nonlinearity_score > 0.7 || characteristics.variable_count > 20 {
            Ok(ReasoningStrategy::Verify)
        } else {
            Ok(ReasoningStrategy::Hybrid)
        }
    }

    fn predict_performance(
        &self,
        strategy: &ReasoningStrategy,
        characteristics: &ConstraintCharacteristics,
    ) -> Result<PredictedPerformance> {
        let base_time = characteristics.variable_count as f64 * 10.0
            + characteristics.constraint_count as f64 * 5.0;

        let (time_multiplier, confidence_estimate, success_prob) = match strategy {
            ReasoningStrategy::Speculate => (0.5, 0.75, 0.85),
            ReasoningStrategy::Verify => (2.0, 0.95, 0.95),
            ReasoningStrategy::Hybrid => (1.0, 0.90, 0.90),
        };

        Ok(PredictedPerformance {
            estimated_solve_time_ms: base_time * time_multiplier,
            estimated_confidence: confidence_estimate,
            success_probability: success_prob,
        })
    }

    fn get_alternative_strategies(
        &self,
        primary: &ReasoningStrategy,
    ) -> Vec<(ReasoningStrategy, f32)> {
        let strategies = [
            ReasoningStrategy::Speculate,
            ReasoningStrategy::Verify,
            ReasoningStrategy::Hybrid,
        ];

        strategies
            .iter()
            .filter(|&s| s != primary)
            .map(|s: &ReasoningStrategy| (s.clone(), 0.6)) // Default alternative confidence
            .collect()
    }

    fn analyze_session_effectiveness(
        &self,
        _constraints: &ConstraintIR,
        strategy_used: &ReasoningStrategy,
        _strategies_considered: &[ReasoningStrategy],
        solution: &SolutionResult,
        performance: &SessionPerformance,
    ) -> Result<MetaAnalysis> {
        // Simple optimality analysis
        let optimality = if performance.success && performance.confidence_achieved > 0.8 {
            if performance.total_solve_time_ms < 100.0 {
                StrategyOptimality::Optimal
            } else {
                StrategyOptimality::Acceptable
            }
        } else if !performance.success {
            StrategyOptimality::Suboptimal {
                better_strategy: ReasoningStrategy::Hybrid,
                estimated_improvement: 0.3,
            }
        } else {
            StrategyOptimality::Acceptable
        };

        let factors = vec![
            PerformanceFactor {
                factor_name: "Solution Confidence".to_string(),
                impact_score: if solution.confidence > 0.8 { 0.5 } else { -0.3 },
                confidence: 0.8,
            },
            PerformanceFactor {
                factor_name: "Solve Time".to_string(),
                impact_score: if performance.total_solve_time_ms < 50.0 {
                    0.4
                } else {
                    -0.2
                },
                confidence: 0.9,
            },
        ];

        let insights = vec![format!(
            "Strategy {:?} achieved {:.1}% confidence in {:.1}ms",
            strategy_used,
            performance.confidence_achieved * 100.0,
            performance.total_solve_time_ms
        )];

        Ok(MetaAnalysis {
            strategy_optimality: optimality,
            performance_prediction_error: 0.1, // Placeholder
            performance_factors: factors,
            insights,
        })
    }

    fn update_strategy_performance(
        &mut self,
        strategy: &ReasoningStrategy,
        performance: &SessionPerformance,
    ) -> Result<()> {
        let stats = self
            .strategy_performance
            .entry(strategy.clone())
            .or_insert_with(|| StrategyPerformanceStats {
                avg_solve_time_ms: 0.0,
                avg_confidence: 0.0,
                success_rate: 0.0,
                sample_count: 0,
            });

        // Update running averages with exponential moving average using learning rate
        let alpha = self.config.strategy_learning_rate;
        
        // Apply exponential moving average: new_value = (1-alpha)*old + alpha*new
        // This gives more weight to recent samples when alpha is higher
        stats.avg_solve_time_ms = (1.0 - alpha as f64) * stats.avg_solve_time_ms 
            + (alpha as f64) * performance.total_solve_time_ms;
        stats.avg_confidence = (1.0 - alpha) * stats.avg_confidence 
            + alpha * performance.confidence_achieved;
        // Update success rate with exponential moving average
        let success_value = if performance.success { 1.0 } else { 0.0 };
        stats.success_rate = (1.0 - alpha) * stats.success_rate + alpha * success_value;
        stats.sample_count += 1;

        Ok(())
    }

    fn update_strategy_patterns(&mut self) -> Result<()> {
        // Extract patterns from recent sessions
        let recent_sessions: Vec<_> = self.session_history.iter().rev().take(50).collect();

        // Group sessions by strategy and analyze effectiveness
        let mut strategy_groups: HashMap<ReasoningStrategy, Vec<_>> = HashMap::new();

        for session in recent_sessions {
            strategy_groups
                .entry(session.strategy_used.clone())
                .or_default()
                .push(session);
        }

        for (strategy, sessions) in strategy_groups {
            if sessions.len() >= 3_usize {
                let pattern_id = format!(
                    "pattern_{}_{}",
                    format!("{:?}", strategy).to_lowercase(),
                    sessions.len()
                );

                let avg_performance = self.calculate_average_performance(&sessions);
                let characteristics = self.extract_common_characteristics(&sessions)?;

                let pattern = StrategyPattern {
                    pattern_id: pattern_id.clone(),
                    constraint_characteristics: characteristics,
                    best_strategy: strategy,
                    performance_statistics: avg_performance,
                    confidence: 0.8, // Base confidence for learned patterns
                };

                self.strategy_patterns.insert(pattern_id.clone(), pattern);
                println!("✅ Discovered new strategy pattern: {}", pattern_id);
            }
        }

        Ok(())
    }

    fn calculate_average_performance(
        &self,
        sessions: &[&ReasoningSession],
    ) -> StrategyPerformanceStats {
        let count = sessions.len() as f32;

        let avg_solve_time = sessions
            .iter()
            .map(|s| s.performance.total_solve_time_ms)
            .sum::<f64>()
            / count as f64;

        let avg_confidence = sessions
            .iter()
            .map(|s| s.performance.confidence_achieved)
            .sum::<f32>()
            / count;

        let success_rate = sessions
            .iter()
            .map(|s| if s.performance.success { 1.0 } else { 0.0 })
            .sum::<f32>()
            / count;

        StrategyPerformanceStats {
            avg_solve_time_ms: avg_solve_time,
            avg_confidence,
            success_rate,
            sample_count: count as u32,
        }
    }

    fn extract_common_characteristics(
        &self,
        sessions: &[&ReasoningSession],
    ) -> Result<ConstraintCharacteristics> {
        // Extract common characteristics across sessions
        let avg_var_count = sessions
            .iter()
            .map(|s| s.constraints.variables.len() as f32)
            .sum::<f32>()
            / sessions.len() as f32;

        let avg_constraint_count = sessions
            .iter()
            .map(|s| s.constraints.constraints.len() as f32)
            .sum::<f32>()
            / sessions.len() as f32;

        // Find most common theory tags
        let mut theory_counts: HashMap<TheoryTag, usize> = HashMap::new();
        for session in sessions {
            for tag in &session.constraints.theory_tags {
                *theory_counts.entry(tag.clone()).or_default() += 1;
            }
        }

        let common_theories: Vec<TheoryTag> = theory_counts
            .into_iter()
            .filter(|(_, count)| *count >= sessions.len() / 2)
            .map(|(tag, _)| tag)
            .collect();

        Ok(ConstraintCharacteristics {
            variable_count: avg_var_count.round() as u32,
            constraint_count: avg_constraint_count.round() as u32,
            domain_types: vec!["Mixed".to_string()], // Simplified
            theory_tags: common_theories,
            complexity_estimate: (avg_var_count * 0.1 + avg_constraint_count * 0.2).min(1.0),
            nonlinearity_score: 0.3, // Default estimate
        })
    }

    fn find_most_effective_strategy(&self) -> Option<ReasoningStrategy> {
        self.strategy_performance
            .iter()
            .max_by(|a, b| {
                let score_a =
                    a.1.success_rate * a.1.avg_confidence / (a.1.avg_solve_time_ms as f32 / 1000.0);
                let score_b =
                    b.1.success_rate * b.1.avg_confidence / (b.1.avg_solve_time_ms as f32 / 1000.0);
                score_a
                    .partial_cmp(&score_b)
                    .unwrap_or(std::cmp::Ordering::Equal)
            })
            .map(|(strategy, _): (&ReasoningStrategy, &StrategyPerformanceStats)| strategy.clone())
    }
}

/// Insights and statistics from meta-reasoning analysis
#[derive(Debug, Clone)]
pub struct MetaReasoningInsights {
    pub total_sessions: usize,
    pub patterns_discovered: usize,
    pub strategy_success_rates: HashMap<ReasoningStrategy, f32>,
    pub average_optimality_score: f32,
    pub constraint_learning_stats: LearningStats,
    pub most_effective_strategy: Option<ReasoningStrategy>,
}