eenn 0.1.0

//! Phase 2A Neuro-Symbolic Integration Demo
//!
//! This demo showcases the core components of our neuro-symbolic reasoning engine
//! combining Lightning Strike cognitive architecture with formal constraint solving.

use anyhow::Result;
use theory_core::smt_stub::SmtBackend;
use theory_core::*;

fn main() -> Result<()> {
    println!("🧠 Phase 2A: Neuro-Symbolic Integration Demo");
    println!("============================================");

    demo_constraint_ir()?;
    demo_smt_backend()?;
    demo_routing_strategy()?;
    demo_solution_generation()?;

    println!("\n🎉 Phase 2A neuro-symbolic integration is operational!");
    println!("✓ Constraint IR system working");
    println!("✓ SMT backend integration (stub) functional");
    println!("✓ Routing strategy engine operational");
    println!("✓ Solution generation pipeline complete");

    Ok(())
}

fn demo_constraint_ir() -> Result<()> {
    println!("\n🔧 Testing Constraint IR Construction...");

    let mut ir = ConstraintIR::new();

    // Create variables for a simple optimization problem
    use theory_core::ir::{
        BinaryOp, ConstValue, Constraint, Domain, Expr, TheoryTag, Variable, VariableMetadata,
    };

    let x = Variable {
        name: "x".to_string(),
        domain: Domain::Real {
            min: Some(0.0),
            max: Some(10.0),
        },
        metadata: VariableMetadata::default(),
    };

    let y = Variable {
        name: "y".to_string(),
        domain: Domain::Real {
            min: Some(0.0),
            max: Some(10.0),
        },
        metadata: VariableMetadata::default(),
    };

    let x_id = ir.add_variable(x);
    let y_id = ir.add_variable(y);

    // Add constraint: x + y <= 8
    let constraint = Constraint::LessEqual {
        lhs: Expr::Binary {
            op: BinaryOp::Add,
            lhs: Box::new(Expr::Var(x_id)),
            rhs: Box::new(Expr::Var(y_id)),
        },
        rhs: Expr::Const(ConstValue::Real(8.0)),
    };

    ir.add_constraint(constraint);
    ir.add_theory_tag(TheoryTag::LRA);

    println!(
        "✓ Created constraint IR with {} variables, {} constraints",
        ir.variables.len(),
        ir.constraints.len()
    );
    println!("✓ Theory tags: {:?}", ir.theory_tags);

    Ok(())
}

fn demo_smt_backend() -> Result<()> {
    println!("\n🔍 Testing SMT Backend (Stub Implementation)...");

    let backend = SmtBackend::new(SmtBackendConfig::default())?;

    // Create constraint IR
    let mut ir = ConstraintIR::new();

    use theory_core::ir::{Domain, Variable, VariableMetadata};
    let var = Variable {
        name: "optimization_var".to_string(),
        domain: Domain::Real {
            min: Some(-5.0),
            max: Some(5.0),
        },
        metadata: VariableMetadata::default(),
    };

    ir.add_variable(var);

    // Solve using async runtime
    let rt = tokio::runtime::Runtime::new().unwrap();
    let result = rt.block_on(async { backend.solve(&ir).await })?;

    println!("✓ SMT Solver Result:");
    println!("  Satisfiable: {}", result.satisfiable);
    println!("  Confidence: {:.2}", result.confidence);
    println!("  Variables solved: {}", result.assignment.len());
    println!("  Solve time: {:.2}ms", result.estimated_time_ms);

    Ok(())
}

fn demo_routing_strategy() -> Result<()> {
    println!("\n🎯 Testing Routing Strategy Engine...");

    let router = SpeculateVerifyRouter::new();

    // Test different complexity scenarios
    let scenarios = vec![
        ("Simple Boolean", Domain::Boolean),
        (
            "Integer Range",
            Domain::Integer {
                min: Some(0),
                max: Some(100),
            },
        ),
        (
            "Real Numbers",
            Domain::Real {
                min: Some(0.0),
                max: Some(1.0),
            },
        ),
    ];

    for (name, domain) in scenarios {
        let mut ir = ConstraintIR::new();

        use theory_core::ir::{TheoryTag, Variable, VariableMetadata};
        let var = Variable {
            name: name.to_lowercase().replace(" ", "_"),
            domain,
            metadata: VariableMetadata::default(),
        };

        ir.add_variable(var);
        ir.add_theory_tag(TheoryTag::LRA);

        let strategy = router.route(&ir)?;

        println!("✓ {} problem -> {:?}", name, strategy);
    }

    Ok(())
}

fn demo_solution_generation() -> Result<()> {
    println!("\n🎲 Testing Solution Generation Pipeline...");

    // Create surrogate solver
    let surrogate = NeuralSolverSurrogate::new(SurrogateConfig::default());

    // Create simple constraint problem
    let mut ir = ConstraintIR::new();

    use theory_core::ir::{Domain, Variable, VariableMetadata};
    let var = Variable {
        name: "demo_var".to_string(),
        domain: Domain::Integer {
            min: Some(1),
            max: Some(10),
        },
        metadata: VariableMetadata::default(),
    };

    ir.add_variable(var);

    // Generate speculative solution
    let solution = surrogate.predict_solution(&ir)?;

    println!("✓ Neural Surrogate Solution:");
    println!("  Satisfiable: {}", solution.satisfiable);
    println!("  Confidence: {:.2}", solution.confidence);

    // Test plausibility checking
    let checker = PlausibilityChecker::new(PlausibilityConfig::default());
    let plausibility = checker.check_plausibility(&ir, &solution)?;

    println!("✓ Plausibility Check:");
    println!("  Plausible: {}", plausibility.plausible);
    println!("  Confidence: {:.2}", plausibility.confidence);
    println!("  Violations found: {}", plausibility.violations.len());

    Ok(())
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn test_demo_runs() -> Result<()> {
        // Just test that the demo functions don't crash
        demo_constraint_ir()?;
        demo_smt_backend()?;
        demo_routing_strategy()?;
        demo_solution_generation()?;
        Ok(())
    }
}