theory_core 0.1.0

//! Phase 2B-1: Neural Constraint Learning System
//! 
//! This module implements learning systems that improve constraint generation
//! and solving strategies based on historical solution patterns.

use crate::ir::{ConstraintIR, VarId};
use crate::surrogate::{SolutionResult, SolutionValue};
use anyhow::Result;
use serde::{Deserialize, Serialize};
use std::collections::{HashMap, VecDeque};

/// Configuration for neural constraint learning
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct LearningConfig {
    /// Maximum number of solution patterns to remember
    pub max_history_size: usize,
    /// Minimum confidence threshold for pattern extraction
    pub min_pattern_confidence: f32,
    /// Learning rate for pattern weight updates
    pub learning_rate: f32,
    /// Enable pattern-based constraint optimization
    pub enable_optimization: bool,
}

impl Default for LearningConfig {
    fn default() -> Self {
        Self {
            max_history_size: 1000,
            min_pattern_confidence: 0.7,
            learning_rate: 0.01,
            enable_optimization: true,
        }
    }
}

/// A learned pattern from historical constraint solutions
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ConstraintPattern {
    /// Pattern identifier
    pub id: String,
    /// Frequency of this pattern in successful solutions
    pub frequency: u32,
    /// Average confidence of solutions using this pattern
    pub avg_confidence: f32,
    /// Variable relationships discovered
    pub variable_relationships: Vec<VariableRelation>,
    /// Constraint templates that often succeed
    pub successful_templates: Vec<ConstraintTemplate>,
    /// Performance metrics
    pub performance_metrics: PatternMetrics,
}

/// Relationship between variables in successful solutions
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct VariableRelation {
    pub var1: VarId,
    pub var2: VarId,
    pub relation_type: RelationType,
    pub strength: f32, // 0.0 to 1.0
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub enum RelationType {
    /// Variables tend to have similar values
    Correlated,
    /// Variables tend to have opposite values  
    AntiCorrelated,
    /// One variable constrains the other
    Dominates,
    /// Variables are independent
    Independent,
    /// Custom learned relationship
    Custom(String),
}

/// Template for generating effective constraints
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ConstraintTemplate {
    pub template_id: String,
    pub success_rate: f32,
    pub avg_solve_time: f64,
    pub applicable_domains: Vec<String>,
    pub template_pattern: String, // Symbolic representation
}

/// Performance metrics for constraint patterns
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct PatternMetrics {
    pub total_uses: u32,
    pub successful_uses: u32,
    pub avg_solve_time_ms: f64,
    pub complexity_reduction: f32,
}

/// Historical record of a constraint-solving session
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct SolutionHistory {
    pub constraints: ConstraintIR,
    pub solution: SolutionResult,
    pub solve_time_ms: f64,
    pub strategy_used: String,
    pub timestamp: u64,
}

/// Neural constraint learning engine
pub struct ConstraintLearner {
    config: LearningConfig,
    solution_history: VecDeque<SolutionHistory>,
    learned_patterns: HashMap<String, ConstraintPattern>,
    pattern_weights: HashMap<String, f32>,
}

impl ConstraintLearner {
    pub fn new(config: LearningConfig) -> Self {
        let capacity = config.max_history_size;
        Self {
            config,
            solution_history: VecDeque::with_capacity(capacity),
            learned_patterns: HashMap::new(),
            pattern_weights: HashMap::new(),
        }
    }

    /// Record a new solution for learning
    pub fn record_solution(
        &mut self,
        constraints: ConstraintIR,
        solution: SolutionResult,
        solve_time_ms: f64,
        strategy_used: String,
    ) -> Result<()> {
        let history = SolutionHistory {
            constraints,
            solution,
            solve_time_ms,
            strategy_used,
            timestamp: std::time::SystemTime::now()
                .duration_since(std::time::UNIX_EPOCH)?
                .as_secs(),
        };

        // Add to history, removing oldest if at capacity
        if self.solution_history.len() >= self.config.max_history_size {
            self.solution_history.pop_front();
        }
        self.solution_history.push_back(history);

        // Trigger pattern learning if we have enough data
        if self.solution_history.len() >= 10 {
            self.extract_patterns()?;
        }

        Ok(())
    }

    /// Extract patterns from solution history
    fn extract_patterns(&mut self) -> Result<()> {
        println!("🧠 Extracting patterns from {} solution records...", 
                 self.solution_history.len());

        // Analyze variable relationships
        self.learn_variable_relationships()?;
        
        // Extract successful constraint templates
        self.learn_constraint_templates()?;
        
        // Update pattern weights based on recent performance
        self.update_pattern_weights()?;

        Ok(())
    }

    /// Learn relationships between variables from successful solutions
    fn learn_variable_relationships(&mut self) -> Result<()> {
        let mut var_correlations: HashMap<(VarId, VarId), Vec<f32>> = HashMap::new();

        // Collect variable value pairs from successful solutions
        for history in &self.solution_history {
            if !history.solution.satisfiable || history.solution.confidence < self.config.min_pattern_confidence {
                continue;
            }

            let vars: Vec<_> = history.constraints.variables.keys().cloned().collect();
            
            // Analyze all variable pairs
            for (i, &var1) in vars.iter().enumerate() {
                for &var2 in vars.iter().skip(i + 1) {
                    if let (Some(val1), Some(val2)) = (
                        self.get_numeric_value(&history.solution, var1)?,
                        self.get_numeric_value(&history.solution, var2)?,
                    ) {
                        var_correlations
                            .entry((var1, var2))
                            .or_default()
                            .push(val1 * val2); // Simple correlation measure
                    }
                }
            }
        }

        // Convert correlations to relationship patterns
        for ((var1, var2), correlations) in var_correlations {
            if correlations.len() >= 3 {
                let avg_correlation = correlations.iter().sum::<f32>() / correlations.len() as f32;
                let relation_type = if avg_correlation > 0.7 {
                    RelationType::Correlated
                } else if avg_correlation < -0.7 {
                    RelationType::AntiCorrelated
                } else {
                    RelationType::Independent
                };

                let relation = VariableRelation {
                    var1,
                    var2,
                    relation_type,
                    strength: avg_correlation.abs(),
                };

                // Store in learned patterns
                let pattern_id = format!("var_rel_{}_{}", var1.0, var2.0);
                self.learned_patterns
                    .entry(pattern_id.clone())
                    .or_insert_with(|| ConstraintPattern {
                        id: pattern_id,
                        frequency: 0,
                        avg_confidence: 0.0,
                        variable_relationships: Vec::new(),
                        successful_templates: Vec::new(),
                        performance_metrics: PatternMetrics {
                            total_uses: 0,
                            successful_uses: 0,
                            avg_solve_time_ms: 0.0,
                            complexity_reduction: 0.0,
                        },
                    })
                    .variable_relationships
                    .push(relation);
            }
        }

        println!("✓ Learned {} variable relationship patterns", 
                 self.learned_patterns.len());
        Ok(())
    }

    /// Learn effective constraint templates from successful solutions
    fn learn_constraint_templates(&mut self) -> Result<()> {
        let mut template_performance: HashMap<String, (u32, f64, f32)> = HashMap::new();

        for history in &self.solution_history {
            if !history.solution.satisfiable {
                continue;
            }

            // Analyze constraint structure
            let constraint_signature = self.extract_constraint_signature(&history.constraints);
            
            let entry = template_performance
                .entry(constraint_signature.clone())
                .or_insert((0, 0.0, 0.0));
            
            entry.0 += 1; // Count
            entry.1 += history.solve_time_ms; // Total solve time
            entry.2 += history.solution.confidence; // Total confidence
        }

        let template_count = template_performance.len();
        
        // Convert to constraint templates
        for (signature, (count, total_time, total_confidence)) in template_performance {
            if count >= 2 {
                let template = ConstraintTemplate {
                    template_id: signature.clone(),
                    success_rate: 1.0, // All recorded solutions were successful
                    avg_solve_time: total_time / count as f64,
                    applicable_domains: vec!["general".to_string()],
                    template_pattern: signature,
                };

                // Add to patterns
                let pattern_id = format!("template_{}", template.template_id);
                self.learned_patterns
                    .entry(pattern_id.clone())
                    .or_insert_with(|| ConstraintPattern {
                        id: pattern_id,
                        frequency: count,
                        avg_confidence: total_confidence / count as f32,
                        variable_relationships: Vec::new(),
                        successful_templates: Vec::new(),
                        performance_metrics: PatternMetrics {
                            total_uses: count,
                            successful_uses: count,
                            avg_solve_time_ms: total_time / count as f64,
                            complexity_reduction: 0.1, // Estimated
                        },
                    })
                    .successful_templates
                    .push(template);
            }
        }

        println!("✓ Learned {} constraint templates", template_count);
        Ok(())
    }

    /// Update pattern weights based on recent performance
    fn update_pattern_weights(&mut self) -> Result<()> {
        for (pattern_id, pattern) in &self.learned_patterns {
            let weight = if pattern.performance_metrics.total_uses > 0 {
                let success_rate = pattern.performance_metrics.successful_uses as f32 
                    / pattern.performance_metrics.total_uses as f32;
                success_rate * pattern.avg_confidence
            } else {
                0.5 // Default weight for unused patterns
            };
            
            self.pattern_weights.insert(pattern_id.clone(), weight);
        }

        println!("✓ Updated weights for {} patterns", self.pattern_weights.len());
        Ok(())
    }

    /// Suggest constraint improvements based on learned patterns
    pub fn suggest_constraint_improvements(&self, constraints: &ConstraintIR) -> Result<Vec<String>> {
        let mut suggestions = Vec::new();

        // Check for known variable relationships
        for pattern in self.learned_patterns.values() {
            if pattern.variable_relationships.is_empty() {
                continue;
            }

            for relation in &pattern.variable_relationships {
                if constraints.variables.contains_key(&relation.var1) 
                    && constraints.variables.contains_key(&relation.var2)
                    && relation.strength > 0.8 {
                    
                    suggestions.push(format!(
                        "Consider {} relationship between variables {} and {} (strength: {:.2})",
                        match relation.relation_type {
                            RelationType::Correlated => "correlated",
                            RelationType::AntiCorrelated => "anti-correlated",
                            RelationType::Dominates => "dominance",
                            RelationType::Independent => "independence",
                            RelationType::Custom(ref s) => s,
                        },
                        relation.var1.0,
                        relation.var2.0,
                        relation.strength
                    ));
                }
            }
        }

        // Suggest high-performing templates
        for pattern in self.learned_patterns.values() {
            if pattern.performance_metrics.successful_uses >= 3 
                && pattern.avg_confidence > self.config.min_pattern_confidence {
                
                suggestions.push(format!(
                    "Template '{}' has {:.1}% success rate with avg confidence {:.2}",
                    pattern.id,
                    (pattern.performance_metrics.successful_uses as f32 
                     / pattern.performance_metrics.total_uses as f32) * 100.0,
                    pattern.avg_confidence
                ));
            }
        }

        Ok(suggestions)
    }

    /// Get current learning statistics
    pub fn get_learning_stats(&self) -> LearningStats {
        LearningStats {
            total_solutions_recorded: self.solution_history.len(),
            patterns_discovered: self.learned_patterns.len(),
            avg_pattern_confidence: self.learned_patterns.values()
                .map(|p| p.avg_confidence)
                .sum::<f32>() / self.learned_patterns.len() as f32,
            most_successful_pattern: self.find_most_successful_pattern(),
        }
    }

    // Helper methods
    fn get_numeric_value(&self, solution: &SolutionResult, var_id: VarId) -> Result<Option<f32>> {
        let var_name = format!("v{}", var_id.0);
        
        if let Some(value) = solution.assignment.get(&var_name) {
            let numeric = match value {
                SolutionValue::Bool(b) => if *b { 1.0 } else { 0.0 },
                SolutionValue::Integer(i) => *i as f32,
                SolutionValue::Real(r) => *r as f32,
                SolutionValue::BitVector { value, .. } => *value as f32,
                SolutionValue::String(_) => return Ok(None), // Can't convert to numeric
            };
            Ok(Some(numeric))
        } else {
            Ok(None)
        }
    }

    fn extract_constraint_signature(&self, constraints: &ConstraintIR) -> String {
        // Simple signature based on constraint count and variable types
        format!("vars:{}_constraints:{}_theories:{:?}", 
                constraints.variables.len(),
                constraints.constraints.len(),
                constraints.theory_tags)
    }

    fn find_most_successful_pattern(&self) -> Option<String> {
        self.learned_patterns
            .values()
            .max_by(|a, b| {
                let a_score = a.performance_metrics.successful_uses as f32 * a.avg_confidence;
                let b_score = b.performance_metrics.successful_uses as f32 * b.avg_confidence;
                a_score.partial_cmp(&b_score).unwrap_or(std::cmp::Ordering::Equal)
            })
            .map(|p| p.id.clone())
    }
}

/// Statistics about the learning process
#[derive(Debug, Clone)]
pub struct LearningStats {
    pub total_solutions_recorded: usize,
    pub patterns_discovered: usize,
    pub avg_pattern_confidence: f32,
    pub most_successful_pattern: Option<String>,
}