theory_core 0.1.0

//! Phase 3: Lightning Strike Integration
//!
//! This module integrates Lightning Strike's dynamic cognitive architecture
//! with the neuro-symbolic reasoning system, creating a unified approach that
//! combines neural reasoning, formal verification, and creative problem solving.

use crate::ir::{ConstraintIR, TheoryTag};
use crate::meta_reasoning::{MetaReasoningEngine, SessionPerformance};
use crate::optimization::{ComputeBackend, PerformanceOptimizer};
use crate::{ReasoningStrategy, SolutionResult};
use anyhow::Result;
use serde::{Deserialize, Serialize};
use std::collections::HashMap;
use std::time::{Duration, Instant};

/// Search optimization mode for Lightning Strike
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
pub enum SearchMode {
    /// Find the FASTEST acceptable solution (first solution with confidence > threshold)
    Fastest,
    /// Find the BEST solution (most accurate, comprehensive, high-quality)
    Best,
    /// BALANCED approach (reasonable speed + good quality)
    Balanced,
}

/// Configuration for Lightning Strike cognitive integration
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct CognitiveConfig {
    /// Search optimization mode (fastest vs best vs balanced)
    pub search_mode: SearchMode,
    /// Initial voltage (problem tension)
    pub initial_voltage: f32,
    /// Total cognitive budget per session
    pub cognitive_budget: f32,
    /// Maximum number of active reasoning branches
    pub max_active_branches: usize,
    /// Maximum number of paused branches to maintain
    pub max_paused_branches: usize,
    /// Resistance decay rate for successful paths
    pub resistance_decay: f32,
    /// Current threshold for pausing branches
    pub pause_threshold: f32,
    /// Revival threshold for reactivating paused branches
    pub revival_threshold: f32,
    /// Enable cross-branch resonance
    pub enable_resonance: bool,
    /// Enable adaptive exploration
    pub enable_exploration: bool,
    /// Solution confidence threshold (when to accept solutions)
    pub solution_confidence_threshold: f32,
    /// Maximum solving steps (when to give up)
    pub max_steps: u32,
}

impl Default for CognitiveConfig {
    fn default() -> Self {
        Self {
            search_mode: SearchMode::Balanced,
            initial_voltage: 10.0,
            cognitive_budget: 100.0,
            max_active_branches: 8,
            max_paused_branches: 32,
            resistance_decay: 0.1,
            pause_threshold: 0.1,
            revival_threshold: 0.5,
            enable_resonance: true,
            enable_exploration: true,
            solution_confidence_threshold: 0.8,
            max_steps: 100,
        }
    }
}

impl CognitiveConfig {
    /// Create configuration optimized for FASTEST solution finding
    pub fn fastest() -> Self {
        Self {
            search_mode: SearchMode::Fastest,
            initial_voltage: 15.0,              // High urgency
            cognitive_budget: 50.0,             // Limited resources for speed
            max_active_branches: 3,             // Focused search, less branching
            max_paused_branches: 8,             // Minimal branch memory
            resistance_decay: 0.3,              // Rapid elimination of poor branches
            pause_threshold: 0.3,               // Aggressive pruning for speed
            revival_threshold: 0.7,             // High bar for branch revival
            enable_resonance: false,            // Skip complex cross-branch learning
            enable_exploration: false,          // No speculative exploration
            solution_confidence_threshold: 0.6, // Lower bar for solution acceptance
            max_steps: 50,                      // Give up quickly if no solution
        }
    }

    /// Create configuration optimized for BEST (most comprehensive) solution
    pub fn best() -> Self {
        Self {
            search_mode: SearchMode::Best,
            initial_voltage: 10.0,              // Steady, thorough exploration
            cognitive_budget: 200.0,            // Ample resources for quality
            max_active_branches: 12,            // Broad parallel search
            max_paused_branches: 64,            // Extensive branch memory
            resistance_decay: 0.05,             // Gradual, conservative pruning
            pause_threshold: 0.05,              // Lenient, keep more branches alive
            revival_threshold: 0.3,             // Low bar for branch revival
            enable_resonance: true,             // Full cross-branch learning
            enable_exploration: true,           // Aggressive speculative exploration
            solution_confidence_threshold: 0.9, // High bar for solution acceptance
            max_steps: 200,                     // Allow extensive search time
        }
    }

    /// Create configuration for BALANCED speed and quality
    pub fn balanced() -> Self {
        Self::default() // Use the default balanced configuration
    }

    /// Get utility function weights for the configured search mode
    pub fn get_utility_weights(&self) -> [f32; 9] {
        // [correctness, info_gain, generalizability, explanatory_power,
        //  conceptual_depth, falsifiability, integration_potential, novelty, efficiency]

        match self.search_mode {
            SearchMode::Fastest => [
                0.35, // correctness - need basic accuracy
                0.10, // info_gain - minimal exploration
                0.05, // generalizability - don't optimize for reuse
                0.05, // explanatory_power - don't need deep insights
                0.05, // conceptual_depth - surface-level is fine
                0.05, // falsifiability - don't worry about testing
                0.10, // integration_potential - some composability value
                0.05, // novelty - prefer known approaches
                0.20, // efficiency - CRITICAL for speed optimization
            ],
            SearchMode::Best => [
                0.25, // correctness - important but not everything
                0.20, // info_gain - HIGH (comprehensive understanding)
                0.15, // generalizability - HIGH (broadly applicable solutions)
                0.15, // explanatory_power - HIGH (deep insights valued)
                0.10, // conceptual_depth - MEDIUM (theoretical understanding)
                0.05, // falsifiability - MEDIUM (testable results)
                0.10, // integration_potential - MEDIUM (composable solutions)
                0.05, // novelty - LOW (prioritize robustness)
                0.05, // efficiency - LOW (speed not important)
            ],
            SearchMode::Balanced => [
                0.30, // correctness - primary requirement
                0.15, // info_gain - good understanding
                0.10, // generalizability - moderate reusability
                0.10, // explanatory_power - some insights
                0.08, // conceptual_depth - basic understanding
                0.07, // falsifiability - some testability
                0.10, // integration_potential - good composability
                0.05, // novelty - limited value in production
                0.15, // efficiency - moderate importance
            ],
        }
    }
}

/// A reasoning branch in the cognitive architecture
#[derive(Debug, Clone)]
pub struct CognitiveBranch {
    /// Unique identifier for this branch
    pub id: String,
    /// Current resistance (inverse of effectiveness)
    pub resistance: f32,
    /// Current flowing through this branch
    pub current: f32,
    /// Reasoning strategy being used
    pub strategy: ReasoningStrategy,
    /// Backend being used for computation
    pub backend: ComputeBackend,
    /// Constraints being worked on
    pub constraints: ConstraintIR,
    /// Partial solution state
    pub partial_solution: Option<SolutionResult>,
    /// Branch creation time
    pub created_at: Instant,
    /// Last activity time
    pub last_active: Instant,
    /// Contribution metrics
    pub metrics: ContributionMetrics,
    /// Prerequisites this branch is waiting for
    pub prerequisites: Vec<String>,
    /// Discoveries made by this branch
    pub discoveries: Vec<Artifact>,
}

/// Metrics for evaluating branch contribution
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ContributionMetrics {
    /// Correctness of the approach (0.0 to 1.0)
    pub correctness: f32,
    /// Information gain provided (0.0 to 1.0)
    pub info_gain: f32,
    /// Generalizability to other problems (0.0 to 1.0)
    pub generalizability: f32,
    /// Explanatory power of the solution (0.0 to 1.0)
    pub explanatory_power: f32,
    /// Conceptual depth and insight (0.0 to 1.0)
    pub conceptual_depth: f32,
    /// Falsifiability and testability (0.0 to 1.0)
    pub falsifiability: f32,
    /// Integration potential with other branches (0.0 to 1.0)
    pub integration_potential: f32,
    /// Novelty and uniqueness (0.0 to 1.0)
    pub novelty: f32,
    /// Efficiency and resource usage (higher is better)
    pub efficiency: f32,
}

impl Default for ContributionMetrics {
    fn default() -> Self {
        Self {
            correctness: 0.5,
            info_gain: 0.5,
            generalizability: 0.5,
            explanatory_power: 0.5,
            conceptual_depth: 0.5,
            falsifiability: 0.5,
            integration_potential: 0.5,
            novelty: 0.5,
            efficiency: 0.5,
        }
    }
}

/// A paused reasoning path stored for later revival
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct PausedPath {
    /// Original branch ID
    pub branch_id: String,
    /// Stored voltage when paused
    pub voltage: f32,
    /// Stored resistance
    pub resistance: f32,
    /// Stored "charge" (potential energy)
    pub capacitance: f32,
    /// What this path is waiting for
    pub waiting_for: Vec<String>,
    /// Embedding of what this path needs
    pub waiting_for_embedding: Vec<f32>,
    /// When this path was paused
    pub paused_at_tick: u64,
    /// Potential discoveries that could enable this path
    pub potential_enablers: Vec<String>,
    /// Revival score (computed dynamically)
    pub revival_score: f32,
}

/// Artifact produced by reasoning branches
#[derive(Debug, Clone)]
pub struct Artifact {
    /// Unique identifier
    pub id: String,
    /// Type of artifact (lemma, proof, counterexample, etc.)
    pub artifact_type: ArtifactType,
    /// Content of the artifact
    pub content: String,
    /// Properties and tags
    pub properties: Vec<String>,
    /// Confidence in this artifact (0.0 to 1.0)
    pub confidence: f32,
    /// Branch that created this artifact
    pub created_by: String,
    /// When it was created  
    pub created_at: Instant,
}

#[derive(Debug, Clone)]
pub enum ArtifactType {
    Lemma,
    Proof,
    Counterexample,
    Insight,
    Pattern,
    Constraint,
    Solution,
    Heuristic,
}

/// Result of a Lightning Strike reasoning step
#[derive(Debug, Clone)]
pub enum StepResult {
    /// Continue reasoning
    Continue,
    /// Found a solution
    Solved(SolutionResult),
    /// Need more resources or time
    Stalled,
    /// Encountered an error
    Error(String),
}

/// Main Lightning Strike cognitive reasoning engine
pub struct LightningStrikeEngine {
    /// Configuration
    config: CognitiveConfig,
    /// Current voltage (problem tension)
    voltage: f32,
    /// Current cognitive budget available
    current_budget: f32,
    /// Currently active reasoning branches
    active_branches: Vec<CognitiveBranch>,
    /// Paused branches waiting for revival
    paused_branches: Vec<PausedPath>,
    /// Main solution path being constructed
    trunk_path: Vec<Artifact>,
    /// All discoveries made so far
    discovery_log: Vec<Artifact>,
    /// Current reasoning tick
    tick: u64,
    /// Integrated components
    meta_reasoner: MetaReasoningEngine,
    optimizer: PerformanceOptimizer,
    /// Session performance tracking
    session_start: Instant,
    /// Verbose output flag
    verbose: bool,
    /// Cached SMT backend for performance
    smt_backend: crate::smt_stub::SmtBackend,
    /// Cached tokio runtime for async operations
    runtime: tokio::runtime::Runtime,
}

impl LightningStrikeEngine {
    pub fn new(
        config: CognitiveConfig,
        meta_reasoner: MetaReasoningEngine,
        optimizer: PerformanceOptimizer,
    ) -> Self {
        Self {
            voltage: config.initial_voltage,
            current_budget: config.cognitive_budget,
            active_branches: Vec::new(),
            paused_branches: Vec::new(),
            trunk_path: Vec::new(),
            discovery_log: Vec::new(),
            tick: 0,
            meta_reasoner,
            optimizer,
            session_start: Instant::now(),
            config,
            verbose: false,
            smt_backend: crate::smt_stub::SmtBackend::new(
                crate::smt_stub::SmtBackendConfig::default(),
            )
            .expect("Failed to create SMT backend"),
            runtime: tokio::runtime::Runtime::new().expect("Failed to create runtime"),
        }
    }

    /// Main reasoning loop step
    pub fn step(&mut self, constraints: &ConstraintIR) -> Result<StepResult> {
        self.tick += 1;

        if self.verbose {
            println!(
                "⚡ Lightning Strike Step {} (V={:.1}, Budget={:.1})",
                self.tick, self.voltage, self.current_budget
            );
        }

        // 1) Expand each active branch one step
        let mut updates = Vec::new();
        let mut solutions_found = Vec::new();

        // First pass: collect branch data to avoid borrow conflicts
        let branch_data: Vec<(usize, f32, f32, f32)> = self
            .active_branches
            .iter()
            .enumerate()
            .map(|(idx, branch)| {
                let progress = self.compute_branch_progress(branch, constraints);
                (idx, progress, branch.resistance, branch.metrics.efficiency)
            })
            .collect();

        // Second pass: update branches and check for solutions
        for (idx, progress, old_resistance, old_efficiency) in branch_data {
            let branch = &mut self.active_branches[idx];

            // Update metrics based on actual progress
            branch.metrics.info_gain += progress * 0.1;
            branch.metrics.efficiency = (old_efficiency + progress * 0.05).min(1.0);

            // Check if this branch found a solution
            // Check if branch has enough progress to generate a solution
            // For NLA problems, try solving earlier since brute-force can be effective
            let threshold = if constraints.theory_tags.contains(&TheoryTag::NLA) {
                0.5 // Lower threshold for NLA - try solving earlier
            } else {
                0.9 // Standard threshold
            };

            if progress > threshold && branch.partial_solution.is_none() {
                // Mark for solution generation (we'll do it later to avoid borrow conflicts)
                solutions_found.push((idx, progress));
            }

            // Update resistance based on actual progress
            let utility = (progress + old_resistance * 0.5).min(1.0);
            let new_resistance = if progress > 0.5 {
                (old_resistance * 0.8).max(0.01) // Reduce resistance on progress
            } else {
                (old_resistance * 1.05).min(10.0) // Increase resistance on stagnation
            };

            updates.push((idx, new_resistance, utility, progress));
            branch.last_active = Instant::now();
        }

        // Apply updates and check for solutions
        for (idx, new_resistance, _utility, progress) in updates {
            self.active_branches[idx].resistance = new_resistance;

            // Update voltage based on progress
            if progress > 0.3 {
                self.voltage = (self.voltage * 1.02).min(20.0); // Boost voltage on progress
            } else {
                self.voltage = (self.voltage * 0.98).max(5.0); // Reduce voltage on stagnation
            }
        }

        // Generate solutions for successful branches
        if !solutions_found.is_empty() {
            let (branch_idx, progress) = solutions_found[0];
            let winning_branch = &self.active_branches[branch_idx];
            let solution =
                self.create_solution_for_branch_with_details(constraints, winning_branch, progress);
            self.active_branches[branch_idx].partial_solution = Some(solution.clone());
            return Ok(StepResult::Solved(solution));
        }

        // 2) Recompute current flow with normalized budget
        self.recompute_currents();

        // 3) Handle pausing of low-current branches
        self.consolidate_branches();

        // 4) Check for surplus and probe paused paths
        let total_active_current: f32 = self.active_branches.iter().map(|b| b.current).sum();

        if total_active_current < self.current_budget * 0.5 {
            self.probe_paused_paths()?;
        }

        // 5) Broadcast recent discoveries
        if !self.discovery_log.is_empty() {
            let latest = self.discovery_log.last().unwrap().clone();
            self.broadcast_discovery(&latest);
        }

        // 6) Allocate resources optimally
        self.allocate_resources()?;

        // 7) Check for solution
        if let Some(solution) = self.check_for_solution() {
            return Ok(StepResult::Solved(solution));
        }

        // 8) Occasional exploration injection
        if self.config.enable_exploration && self.should_explore() {
            self.inject_exploration(constraints)?;
        }

        Ok(StepResult::Continue)
    }

    /// Initialize reasoning with the given constraints
    pub fn initialize(&mut self, constraints: &ConstraintIR, verbose: bool) -> Result<()> {
        if verbose {
            println!("🧠 Initializing Lightning Strike reasoning...");
        }

        // Get meta-reasoning recommendation for initial strategy
        let recommendation = self
            .meta_reasoner
            .recommend_strategy(constraints, verbose)?;

        if verbose {
            println!(
                "   Initial strategy: {:?}",
                recommendation.recommended_strategy
            );
        }

        // Get optimization recommendation for backend
        let optimization = self.optimizer.optimize(constraints, verbose)?;

        if verbose {
            println!("   Recommended backend: {:?}", optimization.backend);
        } // Create initial branches with different approaches
        let initial_strategies = vec![
            (ReasoningStrategy::Speculate, ComputeBackend::Neural),
            (ReasoningStrategy::Verify, ComputeBackend::SMT),
            (ReasoningStrategy::Hybrid, optimization.backend.clone()),
        ];

        for (i, (strategy, backend)) in initial_strategies.into_iter().enumerate() {
            let branch = CognitiveBranch {
                id: format!("initial_{}", i),
                resistance: 1.0,
                current: 0.0,
                strategy,
                backend,
                constraints: constraints.clone(),
                partial_solution: None,
                created_at: Instant::now(),
                last_active: Instant::now(),
                metrics: ContributionMetrics::default(),
                prerequisites: Vec::new(),
                discoveries: Vec::new(),
            };

            self.active_branches.push(branch);
        }

        if verbose {
            println!("   Created {} initial branches", self.active_branches.len());
        }
        Ok(())
    }

    /// Solve the given constraints using cognitive reasoning
    pub fn solve(&mut self, constraints: &ConstraintIR, verbose: bool) -> Result<SolutionResult> {
        self.verbose = verbose;
        self.initialize(constraints, verbose)?;

        let max_steps = self.config.max_steps;
        for _ in 0..max_steps {
            match self.step(constraints)? {
                StepResult::Solved(solution) => {
                    if self.verbose {
                        println!("✅ Lightning Strike found solution in {} steps!", self.tick);
                    }
                    self.record_session_performance(constraints, true)?;
                    return Ok(solution);
                }
                StepResult::Continue => continue,
                StepResult::Stalled => {
                    if self.verbose {
                        println!("🔄 Lightning Strike stalled, trying exploration...");
                    }
                    if self.active_branches.is_empty() && self.paused_branches.is_empty() {
                        break;
                    }
                }
                StepResult::Error(err) => {
                    println!("❌ Lightning Strike error: {}", err);
                    break;
                }
            }
        }

        println!("⏱️ Lightning Strike reached max steps without solution");
        self.record_session_performance(constraints, false)?;

        // Return best partial solution if available
        Ok(self
            .get_best_partial_solution()
            .unwrap_or_else(|| SolutionResult {
                satisfiable: false,
                assignment: HashMap::new(),
                confidence: 0.0,
                estimated_time_ms: self.session_start.elapsed().as_millis() as f64,
                method: "LightningStrike-Partial".to_string(),
                winning_branch_id: None,
                winning_strategy: None,
                winning_backend: None,
                variable_ranges: None,
            }))
    }

    #[allow(dead_code)]
    fn expand_branch(
        &mut self,
        branch: &mut CognitiveBranch,
        _constraints: &ConstraintIR,
    ) -> Result<()> {
        // Placeholder for branch expansion logic
        // In a full implementation, this would:
        // 1. Apply the branch's strategy to the constraints
        // 2. Use the branch's backend for computation
        // 3. Generate new insights or partial solutions
        // 4. Update branch metrics based on progress

        // Simulate progress
        branch.metrics.info_gain += 0.1;
        branch.metrics.correctness = (branch.metrics.correctness + 0.05).min(1.0);

        // Occasionally create discoveries
        if self.tick % 5 == 0 && branch.discoveries.len() < 3 {
            let artifact = Artifact {
                id: format!("discovery_{}_{}", branch.id, self.tick),
                artifact_type: ArtifactType::Insight,
                content: format!(
                    "Branch {} made progress on {:?}",
                    branch.id, branch.strategy
                ),
                properties: vec!["progress".to_string()],
                confidence: branch.metrics.correctness,
                created_by: branch.id.clone(),
                created_at: Instant::now(),
            };

            branch.discoveries.push(artifact.clone());
            self.discovery_log.push(artifact);
        }

        Ok(())
    }

    fn recompute_currents(&mut self) {
        let total_resistance: f32 = self
            .active_branches
            .iter()
            .map(|b| 1.0 / (b.resistance + 0.01))
            .sum();

        if total_resistance > 0.0 {
            for branch in &mut self.active_branches {
                let conductance = 1.0 / (branch.resistance + 0.01);
                branch.current = self.current_budget * conductance / total_resistance;
            }
        }
    }

    fn should_pause_branch(&self, branch: &CognitiveBranch) -> bool {
        branch.current < self.config.pause_threshold
            || branch.last_active.elapsed() > Duration::from_secs(10)
    }

    fn consolidate_branches(&mut self) {
        let mut to_pause = Vec::new();

        for (i, branch) in self.active_branches.iter().enumerate() {
            if self.should_pause_branch(branch) {
                to_pause.push(i);
            }
        }

        // Pause branches in reverse order to maintain indices
        for &i in to_pause.iter().rev() {
            let branch = self.active_branches.remove(i);
            let paused = PausedPath {
                branch_id: branch.id,
                voltage: self.voltage,
                resistance: branch.resistance,
                capacitance: branch.current * 10.0, // Store "charge"
                waiting_for: branch.prerequisites,
                waiting_for_embedding: vec![0.0; 64], // Placeholder embedding
                paused_at_tick: self.tick,
                potential_enablers: Vec::new(),
                revival_score: 0.0,
            };

            self.paused_branches.push(paused);
        }

        // Limit paused branches
        if self.paused_branches.len() > self.config.max_paused_branches {
            self.paused_branches
                .sort_by(|a, b| a.revival_score.partial_cmp(&b.revival_score).unwrap());
            self.paused_branches
                .truncate(self.config.max_paused_branches);
        }
    }

    fn probe_paused_paths(&mut self) -> Result<()> {
        // Recompute revival scores
        for path in &mut self.paused_branches {
            let potential_current = self.voltage / (path.resistance + 0.01);
            path.revival_score = potential_current * path.capacitance;
        }

        // Sort by revival score
        self.paused_branches
            .sort_by(|a, b| b.revival_score.partial_cmp(&a.revival_score).unwrap());

        // Revive top candidates
        let revival_budget = self.current_budget * 0.2;
        let mut revived = 0;

        while let Some(path) = self.paused_branches.pop() {
            if revived as f32 * 10.0 > revival_budget {
                self.paused_branches.push(path);
                break;
            }

            if path.revival_score > self.config.revival_threshold {
                println!(
                    "   Reviving branch {} (score: {:.2})",
                    path.branch_id, path.revival_score
                );
                // Create new branch from paused path
                // This is a placeholder - full implementation would restore complete state
                revived += 1;
            } else {
                self.paused_branches.push(path);
                break;
            }
        }

        Ok(())
    }

    fn broadcast_discovery(&mut self, discovery: &Artifact) {
        if !self.config.enable_resonance {
            return;
        }

        // Collect resonance updates to avoid borrowing conflicts
        let mut updates = Vec::new();
        for (idx, path) in self.paused_branches.iter().enumerate() {
            let resonance = self.compute_resonance(discovery, path);
            let new_resistance = (path.resistance * (1.0 - 0.5 * resonance)).max(0.1);
            updates.push((idx, new_resistance, discovery.id.clone()));
        }

        // Apply updates
        for (idx, new_resistance, discovery_id) in updates {
            self.paused_branches[idx].resistance = new_resistance;
            self.paused_branches[idx]
                .potential_enablers
                .push(discovery_id);
        }
    }

    fn compute_resonance(&self, discovery: &Artifact, path: &PausedPath) -> f32 {
        // Placeholder resonance computation
        // Full implementation would use semantic similarity between discovery and path needs
        let base_resonance = if discovery
            .properties
            .iter()
            .any(|p| path.waiting_for.contains(p))
        {
            0.8
        } else {
            0.2
        };

        base_resonance * discovery.confidence
    }

    fn allocate_resources(&mut self) -> Result<()> {
        // Resource allocation is handled by current flow computation
        // Additional logic could be added here for memory/compute allocation
        Ok(())
    }

    fn check_for_solution(&self) -> Option<SolutionResult> {
        // Check if any branch has found a complete solution
        for branch in &self.active_branches {
            if let Some(ref solution) = branch.partial_solution {
                if solution.satisfiable
                    && solution.confidence > self.config.solution_confidence_threshold
                {
                    return Some(solution.clone());
                }
            }
        }

        // Check trunk path for accumulated solution
        if self.trunk_path.len() > 3 {
            // Placeholder - combine artifacts into solution
            return Some(SolutionResult {
                satisfiable: true,
                assignment: HashMap::new(),
                confidence: 0.7,
                estimated_time_ms: self.session_start.elapsed().as_millis() as f64,
                method: "TrunkPath".to_string(),
                winning_branch_id: None,
                winning_strategy: Some("TrunkPath".to_string()),
                winning_backend: None,
                variable_ranges: None,
            });
        }

        None
    }

    fn should_explore(&self) -> bool {
        // Inject exploration when system is stagnating
        let entropy = self.compute_branch_entropy();
        entropy < 0.5 && self.tick % 10 == 0
    }

    fn compute_branch_entropy(&self) -> f32 {
        if self.active_branches.is_empty() {
            return 0.0;
        }

        let total_current: f32 = self.active_branches.iter().map(|b| b.current).sum();
        if total_current < 1e-6 {
            return 0.0;
        }

        -self
            .active_branches
            .iter()
            .map(|b| {
                let p = b.current / total_current;
                if p > 1e-6 { p * p.ln() } else { 0.0 }
            })
            .sum::<f32>()
    }

    fn inject_exploration(&mut self, constraints: &ConstraintIR) -> Result<()> {
        println!("   Injecting exploration branch...");

        let exploration_branch = CognitiveBranch {
            id: format!("explore_{}", self.tick),
            resistance: 2.0, // Higher resistance for exploration
            current: 0.0,
            strategy: ReasoningStrategy::Hybrid,
            backend: ComputeBackend::Neural, // Fast exploration
            constraints: constraints.clone(),
            partial_solution: None,
            created_at: Instant::now(),
            last_active: Instant::now(),
            metrics: ContributionMetrics {
                novelty: 0.9, // High novelty for exploration
                ..Default::default()
            },
            prerequisites: Vec::new(),
            discoveries: Vec::new(),
        };

        self.active_branches.push(exploration_branch);
        Ok(())
    }

    /// Compute progress for a branch without mutable borrowing
    fn compute_branch_progress(&self, branch: &CognitiveBranch, constraints: &ConstraintIR) -> f32 {
        // Simulate actual constraint solving progress based on problem characteristics
        let base_progress = match constraints.variables.len() {
            1..=2 => 0.3 + (self.tick as f32 * 0.02), // Simple problems make steady progress
            3..=5 => 0.2 + (self.tick as f32 * 0.015), // Medium problems slower
            _ => 0.1 + (self.tick as f32 * 0.01),     // Complex problems very slow
        };

        // Adjust based on theory complexity
        let theory_multiplier = if constraints.theory_tags.contains(&TheoryTag::NLA) {
            0.7 // Nonlinear arithmetic is harder
        } else if constraints.theory_tags.contains(&TheoryTag::LRA) {
            1.2 // Linear arithmetic is easier
        } else {
            1.0
        };

        // Add some randomness and branch-specific factors
        let branch_factor = (branch.resistance * 0.5 + branch.metrics.efficiency * 0.5).min(1.0);
        let randomness = (self.tick % 7) as f32 * 0.05; // Simple deterministic "randomness"

        (base_progress * theory_multiplier * branch_factor + randomness).min(1.0)
    }

    /// Create a solution for a branch by ID
    fn create_solution_for_branch_with_details(
        &self,
        constraints: &ConstraintIR,
        winning_branch: &CognitiveBranch,
        progress: f32,
    ) -> SolutionResult {
        // Actually solve the constraints using cached SMT backend
        let smt_result = self
            .runtime
            .block_on(self.smt_backend.solve(constraints))
            .expect("SMT solving failed");

        // Calibrate confidence based on branch strategy and progress
        let strategy_confidence_boost = match winning_branch.strategy {
            ReasoningStrategy::Verify => 0.10, // Symbolic verification is most reliable
            ReasoningStrategy::Speculate => -0.05, // Neural speculation less certain
            ReasoningStrategy::Hybrid => 0.05, // Hybrid gets moderate boost
        };

        // Higher progress indicates more exploration was needed (lower confidence)
        let progress_penalty = progress * 0.1;
        let adjusted_confidence = (smt_result.confidence + strategy_confidence_boost
            - progress_penalty)
            .max(0.0)
            .min(1.0);

        // Create solution with analytics-adjusted confidence
        let mut solution = smt_result;
        solution.confidence = adjusted_confidence;
        solution.winning_strategy = Some(format!("{:?}", winning_branch.strategy));
        solution.winning_backend = Some(format!("{:?}", winning_branch.backend));
        solution.winning_branch_id = Some(winning_branch.id.clone());

        // Return the analytics-adjusted solution
        solution

        /* OLD FAKE SOLUTION CODE - COMMENTED OUT
        let mut assignment = HashMap::new();

        // Generate reasonable assignments based on variable domains
        for (var_id, variable) in &constraints.variables {
            let var_name = format!("var_{}", var_id.0);
            let value = match &variable.domain {
                Domain::Boolean => crate::SolutionValue::Bool(self.tick % 2 == 0),
                Domain::Integer { min, max } => {
                    let min_val = min.unwrap_or(0);
                    let max_val = max.unwrap_or(10);
                    let val =
                        min_val + ((self.tick as i64 + var_id.0 as i64) % (max_val - min_val + 1));
                    eprintln!("DEBUG: Integer var_{}: min={}, max={}, tick={}, val={}",
                        var_id.0, min_val, max_val, self.tick, val);
                    crate::SolutionValue::Integer(val)
                }
                Domain::Real { min, max } => {
                    let min_val = min.unwrap_or(0.0);
                    let max_val = max.unwrap_or(10.0);
                    let val = min_val
                        + ((self.tick as f64 * 0.1 + var_id.0 as f64) % (max_val - min_val));
                    crate::SolutionValue::Real(val)
                }
                Domain::BitVector { width } => {
                    let val = (self.tick as u64 + var_id.0 as u64) & ((1u64 << width) - 1);
                    crate::SolutionValue::Integer(val as i64)
                }
                Domain::String { .. } => {
                    crate::SolutionValue::String(format!("solution_{}", var_id.0))
                }
                Domain::Array { .. } => {
                    // For arrays, just return a simple string representation
                    crate::SolutionValue::String(format!("array_{}", var_id.0))
                }
                Domain::Enum { .. } => {
                    // For enums, return a simple integer value
                    crate::SolutionValue::Integer(self.tick as i64 % 5)
                }
            };
            assignment.insert(var_name, value);
        }

        // Get strategy and backend names from the winning branch
        let strategy_name = match winning_branch.strategy {
            ReasoningStrategy::Speculate => "Speculate",
            ReasoningStrategy::Verify => "Verify",
            ReasoningStrategy::Hybrid => "Hybrid",
        };

        let backend_name = match &winning_branch.backend {
            ComputeBackend::CPU => "CPU",
            ComputeBackend::GPU => "GPU",
            ComputeBackend::SMT => "SMT",
            ComputeBackend::Neural => "Neural",
            ComputeBackend::Hybrid { primary, .. } => match **primary {
                ComputeBackend::CPU => "Hybrid-CPU",
                ComputeBackend::GPU => "Hybrid-GPU",
                ComputeBackend::SMT => "Hybrid-SMT",
                ComputeBackend::Neural => "Hybrid-Neural",
                _ => "Hybrid",
            },
        };

        SolutionResult {
            satisfiable: true,
            assignment,
            confidence: progress,
            estimated_time_ms: self.session_start.elapsed().as_millis() as f64,
            winning_branch_id: Some(winning_branch.id.clone()),
            winning_strategy: Some(strategy_name.to_string()),
            winning_backend: Some(backend_name.to_string()),
        }
        */
    }

    #[allow(dead_code)]
    fn compute_utility(&self, metrics: &ContributionMetrics) -> f32 {
        // Multi-dimensional utility function with configurable weights based on search mode
        let weights = self.config.get_utility_weights();

        weights[0] * metrics.correctness
            + weights[1] * metrics.info_gain
            + weights[2] * metrics.generalizability
            + weights[3] * metrics.explanatory_power
            + weights[4] * metrics.conceptual_depth
            + weights[5] * metrics.falsifiability
            + weights[6] * metrics.integration_potential
            + weights[7] * metrics.novelty
            + weights[8] * metrics.efficiency
    }

    fn record_session_performance(
        &mut self,
        constraints: &ConstraintIR,
        success: bool,
    ) -> Result<()> {
        let elapsed = self.session_start.elapsed();
        let performance = SessionPerformance {
            total_solve_time_ms: elapsed.as_millis() as f64,
            neural_time_ms: elapsed.as_millis() as f64 * 0.4,
            smt_time_ms: elapsed.as_millis() as f64 * 0.6,
            confidence_achieved: if success { 0.9 } else { 0.3 },
            success,
            iterations_required: self.tick as u32,
        };

        // Record with meta-reasoner
        self.meta_reasoner.record_session(
            format!("lightning_strike_{}", self.tick),
            constraints.clone(),
            ReasoningStrategy::Hybrid,
            vec![
                ReasoningStrategy::Speculate,
                ReasoningStrategy::Verify,
                ReasoningStrategy::Hybrid,
            ],
            if success {
                SolutionResult {
                    satisfiable: true,
                    assignment: HashMap::new(),
                    confidence: 0.9,
                    estimated_time_ms: performance.total_solve_time_ms,
                    method: "MetaReasoning".to_string(),
                    winning_branch_id: Some("Meta".to_string()),
                    winning_strategy: Some("MetaReasoning".to_string()),
                    winning_backend: Some("SMT".to_string()),
                    variable_ranges: None,
                }
            } else {
                SolutionResult {
                    satisfiable: false,
                    assignment: HashMap::new(),
                    confidence: 0.3,
                    estimated_time_ms: performance.total_solve_time_ms,
                    method: "MetaReasoning".to_string(),
                    winning_branch_id: None,
                    winning_strategy: Some("MetaReasoning".to_string()),
                    winning_backend: Some("SMT".to_string()),
                    variable_ranges: None,
                }
            },
            performance.clone(),
        )?;

        // Record with optimizer
        self.optimizer.record_performance(
            constraints,
            &ComputeBackend::Hybrid {
                primary: Box::new(ComputeBackend::Neural),
                fallback: Box::new(ComputeBackend::SMT),
            },
            &performance,
        )?;

        Ok(())
    }

    fn get_best_partial_solution(&self) -> Option<SolutionResult> {
        self.active_branches
            .iter()
            .filter_map(|b| b.partial_solution.as_ref())
            .max_by(|a, b| a.confidence.partial_cmp(&b.confidence).unwrap())
            .cloned()
    }

    /// Get insights about the cognitive reasoning process
    pub fn get_cognitive_insights(&self) -> CognitiveInsights {
        CognitiveInsights {
            total_ticks: self.tick,
            active_branches: self.active_branches.len(),
            paused_branches: self.paused_branches.len(),
            discoveries_made: self.discovery_log.len(),
            average_resistance: self
                .active_branches
                .iter()
                .map(|b| b.resistance)
                .sum::<f32>()
                / self.active_branches.len().max(1) as f32,
            voltage: self.voltage,
            budget_remaining: self.current_budget,
            session_duration: self.session_start.elapsed(),
        }
    }
}

/// Insights about the cognitive reasoning process
#[derive(Debug, Clone)]
pub struct CognitiveInsights {
    pub total_ticks: u64,
    pub active_branches: usize,
    pub paused_branches: usize,
    pub discoveries_made: usize,
    pub average_resistance: f32,
    pub voltage: f32,
    pub budget_remaining: f32,
    pub session_duration: Duration,
}