theory_core 0.1.0

//! Phase 2B-1: Neural Constraint Learning Demo
//! 
//! This demo showcases the constraint learning system that improves
//! solving performance by learning from historical solution patterns.

use theory_core::*;
use anyhow::Result;

fn main() -> Result<()> {
    println!("🧠 Phase 2B-1: Neural Constraint Learning Demo");
    println!("===============================================");
    
    demo_constraint_learning()?;
    demo_pattern_extraction()?;
    demo_solution_suggestions()?;
    
    println!("\n🎉 Phase 2B-1 Neural Constraint Learning is operational!");
    println!("✓ Solution history recording");
    println!("✓ Pattern extraction from successful solutions");
    println!("✓ Variable relationship learning");
    println!("✓ Constraint template optimization");
    println!("✓ Performance-based pattern weighting");
    
    Ok(())
}

fn demo_constraint_learning() -> Result<()> {
    println!("\n🎯 Test 1: Basic Constraint Learning");
    
    let mut learner = ConstraintLearner::new(LearningConfig::default());
    
    // Simulate several constraint-solving sessions
    for i in 0..5 {
        let constraints = create_sample_constraints(i)?;
        let solution = create_sample_solution(i)?;
        let solve_time = 50.0 + i as f64 * 10.0; // Simulate varying solve times
        let strategy = if i % 2 == 0 { "speculative" } else { "verified" };
        
        learner.record_solution(
            constraints,
            solution,
            solve_time,
            strategy.to_string(),
        )?;
        
        println!("✓ Recorded solution session {} (strategy: {})", i + 1, strategy);
    }
    
    let stats = learner.get_learning_stats();
    println!("📊 Learning Statistics:");
    println!("  Solutions recorded: {}", stats.total_solutions_recorded);
    println!("  Patterns discovered: {}", stats.patterns_discovered);
    if stats.patterns_discovered > 0 {
        println!("  Average pattern confidence: {:.2}", stats.avg_pattern_confidence);
        if let Some(best_pattern) = stats.most_successful_pattern {
            println!("  Most successful pattern: {}", best_pattern);
        }
    }
    
    Ok(())
}

fn demo_pattern_extraction() -> Result<()> {
    println!("\n🔍 Test 2: Pattern Extraction and Analysis");
    
    let mut learner = ConstraintLearner::new(LearningConfig {
        max_history_size: 20,
        min_pattern_confidence: 0.6,
        learning_rate: 0.05,
        enable_optimization: true,
    });
    
    // Create a more realistic learning scenario with patterns
    for session in 0..15 {
        let constraints = create_patterned_constraints(session)?;
        let solution = create_correlated_solution(session)?;
        let solve_time = if session % 3 == 0 { 25.0 } else { 75.0 }; // Pattern in solve times
        
        learner.record_solution(
            constraints,
            solution,
            solve_time,
            "hybrid".to_string(),
        )?;
    }
    
    let stats = learner.get_learning_stats();
    println!("✓ Processed {} learning sessions", stats.total_solutions_recorded);
    println!("✓ Discovered {} patterns", stats.patterns_discovered);
    
    if stats.patterns_discovered > 0 {
        println!("✓ Pattern extraction successful!");
        println!("  Average confidence: {:.2}", stats.avg_pattern_confidence);
    } else {
        println!("ℹ️  No strong patterns detected yet (need more data)");
    }
    
    Ok(())
}

fn demo_solution_suggestions() -> Result<()> {
    println!("\n💡 Test 3: Solution Suggestions");
    
    let mut learner = ConstraintLearner::new(LearningConfig::default());
    
    // Train the learner with several successful solutions
    for i in 0..8 {
        let constraints = create_sample_constraints(i)?;
        let solution = create_successful_solution(i)?;
        
        learner.record_solution(
            constraints,
            solution,
            30.0,
            "learned_pattern".to_string(),
        )?;
    }
    
    // Now ask for suggestions on a new problem
    let test_constraints = create_sample_constraints(99)?;
    let suggestions = learner.suggest_constraint_improvements(&test_constraints)?;
    
    println!("✓ Generated {} improvement suggestions", suggestions.len());
    
    if suggestions.is_empty() {
        println!("ℹ️  No specific suggestions available yet (learning in progress)");
    } else {
        println!("💡 Suggestions:");
        for (i, suggestion) in suggestions.iter().enumerate() {
            println!("   {}. {}", i + 1, suggestion);
        }
    }
    
    Ok(())
}

// Helper functions to create sample data

fn create_sample_constraints(seed: usize) -> Result<ConstraintIR> {
    let mut ir = ConstraintIR::new();
    
    use theory_core::ir::{Variable, Domain, VariableMetadata, TheoryTag};
    
    // Create variables based on seed for variety
    let var1 = Variable {
        name: format!("x{}", seed),
        domain: Domain::Real { min: Some(0.0), max: Some(10.0) },
        metadata: VariableMetadata::default(),
    };
    
    let var2 = Variable {
        name: format!("y{}", seed),
        domain: Domain::Integer { min: Some(0), max: Some(100) },
        metadata: VariableMetadata::default(),
    };
    
    ir.add_variable(var1);
    ir.add_variable(var2);
    ir.add_theory_tag(TheoryTag::LRA);
    
    Ok(ir)
}

fn create_sample_solution(seed: usize) -> Result<SolutionResult> {
    use std::collections::HashMap;
    
    let mut assignment = HashMap::new();
    assignment.insert(format!("v{}", seed * 2), SolutionValue::Real((seed as f32 * 1.5) as f64));
    assignment.insert(format!("v{}", seed * 2 + 1), SolutionValue::Integer(seed as i64 * 10));
    
    Ok(SolutionResult {
        satisfiable: true,
        assignment,
        confidence: 0.8 + (seed % 3) as f32 * 0.05,
        estimated_time_ms: 45.0,
        winning_branch_id: None,
        winning_strategy: None,
        winning_backend: None,
        variable_ranges: None,
    })
}

fn create_patterned_constraints(session: usize) -> Result<ConstraintIR> {
    let mut ir = ConstraintIR::new();
    
    use theory_core::ir::{Variable, Domain, VariableMetadata, TheoryTag};
    
    // Create variables with some pattern (alternating types)
    if session % 2 == 0 {
        let var = Variable {
            name: format!("bool_var_{}", session),
            domain: Domain::Boolean,
            metadata: VariableMetadata::default(),
        };
        ir.add_variable(var);
    } else {
        let var = Variable {
            name: format!("real_var_{}", session),
            domain: Domain::Real { min: Some(-1.0), max: Some(1.0) },
            metadata: VariableMetadata::default(),
        };
        ir.add_variable(var);
    }
    
    ir.add_theory_tag(if session % 3 == 0 { 
        TheoryTag::LRA 
    } else { 
        TheoryTag::LIA 
    });
    
    Ok(ir)
}

fn create_correlated_solution(session: usize) -> Result<SolutionResult> {
    use std::collections::HashMap;
    
    let mut assignment = HashMap::new();
    
    // Create solutions with some correlation patterns
    let base_value = (session as f32 / 3.0).sin();
    
    assignment.insert("v0".to_string(), if session % 2 == 0 {
        SolutionValue::Bool(base_value > 0.0)
    } else {
        SolutionValue::Real(base_value as f64)
    });
    
    Ok(SolutionResult {
        satisfiable: true,
        assignment,
        confidence: 0.75 + base_value.abs() * 0.2,
        estimated_time_ms: 40.0 + session as f64 * 2.0,
        winning_branch_id: None,
        winning_strategy: None,
        winning_backend: None,
        variable_ranges: None,
    })
}

fn create_successful_solution(seed: usize) -> Result<SolutionResult> {
    use std::collections::HashMap;
    
    let mut assignment = HashMap::new();
    
    // Create consistently successful solutions
    assignment.insert("v0".to_string(), SolutionValue::Real(((seed as f32 % 5.0) + 1.0) as f64));
    assignment.insert("v1".to_string(), SolutionValue::Integer(seed as i64 % 50));
    
    Ok(SolutionResult {
        satisfiable: true,
        assignment,
        confidence: 0.9 + (seed as f32 % 10.0) / 100.0, // High confidence
        estimated_time_ms: 25.0,
        winning_branch_id: None,
        winning_strategy: None,
        winning_backend: None,
        variable_ranges: None,
    })
}