theory_core 0.1.0

//! Hybrid Reasoning Engine: Neuro-Symbolic Fusion
//!
//! Combines Lightning Strike's symbolic reasoning with neural surrogate prediction
//! to create a truly hybrid neuro-symbolic system where both components learn from each other.

use crate::ir::ConstraintIR;
use crate::lightning_strike::LightningStrikeEngine;
use crate::surrogate::{NeuralSolverSurrogate, SolutionResult, SolverSurrogate, SurrogateConfig};
use anyhow::Result;
use serde::{Deserialize, Serialize};
use std::time::Instant;

/// Configuration for hybrid neuro-symbolic reasoning
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct HybridConfig {
    /// Neural surrogate configuration
    pub surrogate_config: SurrogateConfig,
    /// Hybrid reasoning parameters
    pub neural_guidance_weight: f32,
    pub symbolic_verification_threshold: f32,
    pub learning_rate: f32,
    /// Adaptive thresholds
    pub confidence_threshold: f32,
    pub neural_timeout_ms: u64,
    pub symbolic_timeout_ms: u64,
    /// Learning parameters
    pub enable_cross_learning: bool,
    pub neural_feedback_weight: f32,
}

impl Default for HybridConfig {
    fn default() -> Self {
        Self {
            surrogate_config: SurrogateConfig::default(),
            neural_guidance_weight: 0.6,
            symbolic_verification_threshold: 0.8,
            learning_rate: 0.01,
            confidence_threshold: 0.7,
            neural_timeout_ms: 50,
            symbolic_timeout_ms: 1000,
            enable_cross_learning: true,
            neural_feedback_weight: 0.3,
        }
    }
}

/// Strategy for hybrid reasoning execution
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum HybridStrategy {
    /// Neural-first with symbolic verification
    NeuralFirst,
    /// Symbolic-first with neural guidance
    SymbolicFirst,
    /// Parallel execution with best-of-both
    Parallel,
    /// Adaptive based on problem characteristics
    Adaptive,
}

/// Fusion mode for combining neural and symbolic results
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum FusionMode {
    /// Neural provides initial guess, symbolic refines
    NeuralGuided,
    /// Symbolic explores, neural predicts best branches
    SymbolicGuided,
    /// Both work independently, combine results
    Independent,
    /// Interleaved: alternate between neural and symbolic steps
    Interleaved,
}

/// Performance metrics for hybrid reasoning
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct HybridMetrics {
    /// Neural performance
    pub neural_solve_time_ms: f64,
    pub neural_confidence: f32,
    pub neural_accuracy: f32,
    /// Symbolic performance
    pub symbolic_solve_time_ms: f64,
    pub symbolic_steps: u32,
    pub symbolic_branches_explored: u32,
    /// Hybrid performance
    pub total_time_ms: f64,
    pub fusion_overhead_ms: f64,
    pub speedup_factor: f32,
    /// Learning metrics
    pub neural_updates: u32,
    pub symbolic_feedback_signals: u32,
}

/// Learning sample for cross-training
#[derive(Debug, Clone)]
pub struct LearningSample {
    pub constraints: ConstraintIR,
    pub neural_prediction: SolutionResult,
    pub symbolic_solution: SolutionResult,
    pub hybrid_confidence: f32,
    pub performance_delta: f32,
}

/// Hybrid Reasoning Engine combining neural and symbolic approaches
pub struct HybridReasoningEngine {
    config: HybridConfig,
    lightning_strike: LightningStrikeEngine,
    neural_surrogate: Box<dyn SolverSurrogate>,
    /// Learning history for adaptive behavior
    learning_samples: Vec<LearningSample>,
    /// Performance tracking
    metrics_history: Vec<HybridMetrics>,
    /// Adaptive parameters
    current_strategy: HybridStrategy,
    neural_trust_score: f32,
    symbolic_trust_score: f32,
}

impl HybridReasoningEngine {
    /// Create new hybrid reasoning engine
    pub fn new(config: HybridConfig, lightning_strike: LightningStrikeEngine) -> Self {
        let neural_surrogate =
            Box::new(NeuralSolverSurrogate::new(config.surrogate_config.clone()));

        Self {
            config,
            lightning_strike,
            neural_surrogate,
            learning_samples: Vec::new(),
            metrics_history: Vec::new(),
            current_strategy: HybridStrategy::Adaptive,
            neural_trust_score: 0.5,
            symbolic_trust_score: 0.8,
        }
    }

    /// Solve constraints using hybrid neuro-symbolic approach
    pub fn solve_hybrid(&mut self, constraints: &ConstraintIR) -> Result<SolutionResult> {
        let start_time = Instant::now();
        let mut metrics = HybridMetrics {
            neural_solve_time_ms: 0.0,
            neural_confidence: 0.0,
            neural_accuracy: 0.0,
            symbolic_solve_time_ms: 0.0,
            symbolic_steps: 0,
            symbolic_branches_explored: 0,
            total_time_ms: 0.0,
            fusion_overhead_ms: 0.0,
            speedup_factor: 1.0,
            neural_updates: 0,
            symbolic_feedback_signals: 0,
        };

        // Determine strategy based on problem characteristics
        let strategy = self.select_strategy(constraints);

        let result = match strategy {
            HybridStrategy::NeuralFirst => self.neural_first_solve(constraints, &mut metrics),
            HybridStrategy::SymbolicFirst => self.symbolic_first_solve(constraints, &mut metrics),
            HybridStrategy::Parallel => self.parallel_solve(constraints, &mut metrics),
            HybridStrategy::Adaptive => self.adaptive_solve(constraints, &mut metrics),
        }?;

        metrics.total_time_ms = start_time.elapsed().as_millis() as f64;
        self.metrics_history.push(metrics);

        // Learn from this solving session
        if self.config.enable_cross_learning {
            self.update_learning_from_session(constraints, &result)?;
        }

        Ok(result)
    }

    /// Neural-first strategy: Neural prediction → Symbolic verification
    fn neural_first_solve(
        &mut self,
        constraints: &ConstraintIR,
        metrics: &mut HybridMetrics,
    ) -> Result<SolutionResult> {
        // Phase 1: Neural prediction
        let neural_start = Instant::now();
        let neural_prediction = self.neural_surrogate.predict_solution(constraints)?;
        metrics.neural_solve_time_ms = neural_start.elapsed().as_millis() as f64;
        metrics.neural_confidence = neural_prediction.confidence;

        // Phase 2: Symbolic verification if needed
        if neural_prediction.confidence < self.config.symbolic_verification_threshold {
            let symbolic_start = Instant::now();
            let symbolic_result = self.lightning_strike.solve(constraints, false)?;
            metrics.symbolic_solve_time_ms = symbolic_start.elapsed().as_millis() as f64;

            // Fuse results
            Ok(self.fuse_results(neural_prediction, symbolic_result, FusionMode::NeuralGuided))
        } else {
            Ok(neural_prediction)
        }
    }

    /// Symbolic-first strategy: Lightning Strike with neural branch guidance
    fn symbolic_first_solve(
        &mut self,
        constraints: &ConstraintIR,
        metrics: &mut HybridMetrics,
    ) -> Result<SolutionResult> {
        // Phase 1: Neural guidance for branch exploration
        let neural_start = Instant::now();
        let neural_hint = self.neural_surrogate.predict_solution(constraints)?;
        metrics.neural_solve_time_ms = neural_start.elapsed().as_millis() as f64;

        // Phase 2: Symbolic solving with neural guidance
        let symbolic_start = Instant::now();
        let symbolic_result = self.lightning_strike_with_guidance(constraints, &neural_hint)?;
        metrics.symbolic_solve_time_ms = symbolic_start.elapsed().as_millis() as f64;

        Ok(symbolic_result)
    }

    /// Parallel strategy: Run both simultaneously, use best result
    fn parallel_solve(
        &mut self,
        constraints: &ConstraintIR,
        metrics: &mut HybridMetrics,
    ) -> Result<SolutionResult> {
        // TODO: Implement true parallel execution
        // For now, simulate with sequential execution

        let neural_start = Instant::now();
        let neural_result = self.neural_surrogate.predict_solution(constraints)?;
        metrics.neural_solve_time_ms = neural_start.elapsed().as_millis() as f64;

        let symbolic_start = Instant::now();
        let symbolic_result = self.lightning_strike.solve(constraints, false)?;
        metrics.symbolic_solve_time_ms = symbolic_start.elapsed().as_millis() as f64;

        // Choose best result based on confidence and trust scores
        if neural_result.confidence * self.neural_trust_score
            > symbolic_result.confidence * self.symbolic_trust_score
        {
            Ok(neural_result)
        } else {
            Ok(symbolic_result)
        }
    }

    /// Adaptive strategy: Choose approach based on problem characteristics
    fn adaptive_solve(
        &mut self,
        constraints: &ConstraintIR,
        metrics: &mut HybridMetrics,
    ) -> Result<SolutionResult> {
        let complexity = self.estimate_complexity(constraints);
        let neural_confidence = self.neural_surrogate.prediction_confidence(constraints)?;

        if complexity < 0.3 && neural_confidence > 0.8 {
            // Simple problem, trust neural network
            self.neural_first_solve(constraints, metrics)
        } else if complexity > 0.7 || neural_confidence < 0.5 {
            // Complex problem, use symbolic reasoning
            self.symbolic_first_solve(constraints, metrics)
        } else {
            // Medium complexity, use parallel approach
            self.parallel_solve(constraints, metrics)
        }
    }

    /// Lightning Strike solving with neural guidance
    /// 
    /// # Planned Implementation
    /// This feature will integrate neural predictions with symbolic reasoning:
    /// 1. Use `neural_hint` to bias branch exploration priorities
    /// 2. Map neural solution to initial variable assignments for SMT solver
    /// 3. Implement early termination when neural and symbolic agree (confidence > 0.9)
    /// 4. Track disagreements for future neural surrogate training
    /// 
    /// # Current Behavior
    /// Falls back to standard Lightning Strike solving without neural guidance.
    #[allow(unused_variables)]  // neural_hint reserved for future implementation
    fn lightning_strike_with_guidance(
        &mut self,
        constraints: &ConstraintIR,
        neural_hint: &SolutionResult,
    ) -> Result<SolutionResult> {
        // TODO(Phase 4): Implement neural guidance integration
        // Requires: Neural surrogate training pipeline, assignment mapping utilities
        self.lightning_strike.solve(constraints, false)
    }

    /// Fuse neural and symbolic results
    fn fuse_results(
        &self,
        neural_result: SolutionResult,
        symbolic_result: SolutionResult,
        mode: FusionMode,
    ) -> SolutionResult {
        match mode {
            FusionMode::NeuralGuided => {
                // Use symbolic result but with neural confidence weighting
                let mut result = symbolic_result;
                result.confidence = (result.confidence + neural_result.confidence) / 2.0;
                result
            }
            FusionMode::SymbolicGuided => {
                // Use symbolic result as authoritative
                symbolic_result
            }
            FusionMode::Independent => {
                // Choose based on confidence
                if neural_result.confidence > symbolic_result.confidence {
                    neural_result
                } else {
                    symbolic_result
                }
            }
            FusionMode::Interleaved => {
                // Complex fusion strategy (TODO: implement)
                symbolic_result
            }
        }
    }

    /// Select strategy based on problem characteristics
    fn select_strategy(&self, constraints: &ConstraintIR) -> HybridStrategy {
        let complexity = self.estimate_complexity(constraints);
        let var_count = constraints.variables.len();
        let constraint_count = constraints.constraints.len();

        // Adaptive strategy selection
        if var_count < 5 && constraint_count < 3 {
            HybridStrategy::NeuralFirst
        } else if complexity > 0.8 || constraint_count > 10 {
            HybridStrategy::SymbolicFirst
        } else {
            HybridStrategy::Parallel
        }
    }

    /// Estimate problem complexity
    fn estimate_complexity(&self, constraints: &ConstraintIR) -> f32 {
        let var_count = constraints.variables.len() as f32;
        let constraint_count = constraints.constraints.len() as f32;
        let theory_complexity = constraints.theory_tags.len() as f32 * 0.2;

        (var_count * 0.1 + constraint_count * 0.3 + theory_complexity).min(1.0)
    }

    /// Update learning from solving session
    /// 
    /// # Planned Implementation
    /// Cross-learning between neural and symbolic components:
    /// 1. Use `result` from symbolic solving as training data for neural surrogate
    /// 2. Compare neural predictions with symbolic solutions to compute accuracy
    /// 3. Update `neural_trust_score` and `symbolic_trust_score` based on agreement
    /// 4. Store `LearningSample` for offline training
    /// 
    /// # Current Behavior
    /// Stub - no learning updates performed.
    #[allow(unused_variables)]  // constraints, result reserved for future implementation
    fn update_learning_from_session(
        &mut self,
        constraints: &ConstraintIR,
        result: &SolutionResult,
    ) -> Result<()> {
        // TODO(Phase 4): Implement cross-learning pipeline
        // Requires: Neural network training integration, accuracy tracking
        Ok(())
    }

    /// Get current performance metrics
    pub fn get_metrics(&self) -> &[HybridMetrics] {
        &self.metrics_history
    }

    /// Get learning samples for analysis
    pub fn get_learning_samples(&self) -> &[LearningSample] {
        &self.learning_samples
    }

    /// Update trust scores based on performance
    pub fn update_trust_scores(&mut self, neural_accuracy: f32, symbolic_accuracy: f32) {
        let alpha = self.config.learning_rate;
        self.neural_trust_score = (1.0 - alpha) * self.neural_trust_score + alpha * neural_accuracy;
        self.symbolic_trust_score =
            (1.0 - alpha) * self.symbolic_trust_score + alpha * symbolic_accuracy;
    }

    /// Reset learning history
    pub fn reset_learning(&mut self) {
        self.learning_samples.clear();
        self.metrics_history.clear();
        self.neural_trust_score = 0.5;
        self.symbolic_trust_score = 0.8;
    }
}

/// Builder for convenient hybrid engine construction
pub struct HybridReasoningBuilder {
    config: HybridConfig,
}

impl HybridReasoningBuilder {
    pub fn new() -> Self {
        Self {
            config: HybridConfig::default(),
        }
    }

    pub fn neural_guidance_weight(mut self, weight: f32) -> Self {
        self.config.neural_guidance_weight = weight;
        self
    }

    pub fn confidence_threshold(mut self, threshold: f32) -> Self {
        self.config.confidence_threshold = threshold;
        self
    }

    pub fn enable_cross_learning(mut self, enable: bool) -> Self {
        self.config.enable_cross_learning = enable;
        self
    }

    pub fn build(self, lightning_strike: LightningStrikeEngine) -> HybridReasoningEngine {
        HybridReasoningEngine::new(self.config, lightning_strike)
    }
}

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