theory_core 0.1.0

//! Phase 2A Neuro-Symbolic Integration Simple Demo

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

fn main() -> Result<()> {
    println!("🧠 Phase 2A: Neuro-Symbolic Integration DEMO");
    println!("=============================================");
    
    // Test 1: Constraint IR Construction  
    println!("\n🔧 Test 1: Constraint IR Construction");
    let mut ir = ConstraintIR::new();
    
    use theory_core::ir::{Variable, Domain, VariableMetadata, TheoryTag};
    let var = Variable {
        name: "x".to_string(),
        domain: Domain::Boolean,
        metadata: VariableMetadata::default(),
    };
    
    ir.add_variable(var);
    ir.add_theory_tag(TheoryTag::LRA);
    
    println!("✓ Created constraint IR with {} variables", ir.variables.len());
    println!("✓ Theory tags: {:?}", ir.theory_tags);
    
    // Test 2: Routing Strategy
    println!("\n🎯 Test 2: Routing Strategy Engine");
    let router = SpeculateVerifyRouter::new();
    let strategy = router.route(&ir)?;
    
    match strategy {
        ReasoningStrategy::Speculate => println!("✓ Router chose speculative strategy"),
        ReasoningStrategy::Verify => println!("✓ Router chose verification strategy"), 
        ReasoningStrategy::Hybrid => println!("✓ Router chose hybrid strategy"),
    }
    
    // Test 3: Plausibility Checking
    println!("\n✅ Test 3: Plausibility Checking");
    let checker = PlausibilityChecker::new(PlausibilityConfig::default());
    
    use std::collections::HashMap;
    let mut assignment = HashMap::new();
    assignment.insert("v0".to_string(), SolutionValue::Bool(true));
    
    let solution = SolutionResult {
        satisfiable: true,
        assignment,
        confidence: 0.95,
        estimated_time_ms: 5.0,
        winning_branch_id: None,
        winning_strategy: None,
        winning_backend: None,
        variable_ranges: None,
    };
    
    let result = checker.check_plausibility(&ir, &solution)?;
    
    println!("✓ Plausibility check complete");
    println!("  Plausible: {}", result.plausible);
    println!("  Confidence: {:.2}", result.confidence);
    println!("  Violations: {}", result.violations.len());
    
    println!("\n🎉 Phase 2A Neuro-Symbolic Integration is WORKING!");
    println!("✓ Constraint IR: Operational");
    println!("✓ Routing Logic: Operational");
    println!("✓ Plausibility Checking: Operational");
    println!("✓ Solution Pipeline: Ready");
    
    Ok(())
}