//! Integration tests for neuro-symbolic reasoning engine\n\nuse anyhow::Result;\nuse theory_core::*;\nuse eenn::tensor::Tensor;\n\n#[tokio::test]\nasync fn test_basic_neuro_symbolic_reasoning() -> Result<()> {\n // Create theory generator and solver surrogate\n let theory_generator = Box::new(NeuralTheoryGenerator::new(\n TheoryGeneratorConfig::default(),\n ));\n \n let solver_surrogate = Box::new(NeuralSolverSurrogate::new(\n SurrogateConfig::default(),\n ));\n \n // Create SMT backend\n let smt_backend = SmtBackend::new(SmtBackendConfig::default())?;\n \n // Create neuro-symbolic engine\n let mut engine = NeuroSymbolicEngine::new(\n theory_generator,\n solver_surrogate,\n smt_backend,\n )?;\n \n // Create test input\n let input = Tensor::from_data(&[1.0, 2.0, 3.0], &[3]);\n \n // Reason about the input\n let result = engine.reason(&input).await?;\n \n // Verify we got some result\n match result {\n ReasoningResult::Speculated(_) => println!(\"Used speculation\"),\n ReasoningResult::Verified(_) => println!(\"Used verification\"),\n ReasoningResult::Hybrid { .. } => println!(\"Used hybrid approach\"),\n }\n \n Ok(())\n}\n\n#[test]\nfn test_constraint_ir_creation() -> Result<()> {\n let mut ir = ConstraintIR::new();\n \n // Add variables\n use theory_core::ir::{Variable, Domain, VariableMetadata};\n \n let x = Variable {\n name: \"x\".to_string(),\n domain: Domain::Real { min: Some(0.0), max: Some(10.0) },\n metadata: VariableMetadata::default(),\n };\n \n let y = Variable {\n name: \"y\".to_string(),\n domain: Domain::Real { min: Some(0.0), max: Some(10.0) },\n metadata: VariableMetadata::default(),\n };\n \n let x_id = ir.add_variable(x);\n let y_id = ir.add_variable(y);\n \n // Add constraint: x + y <= 5\n use theory_core::ir::{Constraint, Expr, BinaryOp, ConstValue};\n \n let constraint = Constraint::LessEqual {\n lhs: Expr::Binary {\n op: BinaryOp::Add,\n lhs: Box::new(Expr::Var(x_id)),\n rhs: Box::new(Expr::Var(y_id)),\n },\n rhs: Expr::Const(ConstValue::Real(5.0)),\n };\n \n ir.add_constraint(constraint);\n ir.add_theory_tag(theory_core::ir::TheoryTag::LRA);\n \n // Verify IR structure\n assert_eq!(ir.variables.len(), 2);\n assert_eq!(ir.constraints.len(), 1);\n assert_eq!(ir.theory_tags.len(), 1);\n \n Ok(())\n}\n\n#[test]\nfn test_plausibility_checking() -> Result<()> {\n let checker = PlausibilityChecker::new(PlausibilityConfig::default());\n \n // Create constraint IR\n let mut ir = ConstraintIR::new();\n use theory_core::ir::{Variable, Domain, VariableMetadata};\n \n let var = Variable {\n name: \"x\".to_string(),\n domain: Domain::Real { min: Some(0.0), max: Some(10.0) },\n metadata: VariableMetadata::default(),\n };\n \n ir.add_variable(var);\n \n // Create solution result\n use std::collections::HashMap;\n let mut assignment = HashMap::new();\n assignment.insert(\"v0\".to_string(), SolutionValue::Real(5.0)); // Valid\n \n let solution = SolutionResult {\n satisfiable: true,\n assignment,\n confidence: 0.9,\n estimated_time_ms: 10.0,\n };\n \n // Check plausibility\n let result = checker.check_plausibility(&ir, &solution)?;\n \n assert!(result.plausible);\n assert!(result.confidence > 0.8);\n assert!(result.violations.is_empty());\n \n Ok(())\n}\n\n#[test]\nfn test_constraint_evaluation() -> Result<()> {\n use theory_core::constraint::*;\n use std::collections::HashMap;\n \n let checker = BasicConstraintChecker::new(1e-6);\n \n // Create context with variable assignments\n let mut assignments = HashMap::new();\n assignments.insert(VarId(0), ConstraintValue::Real(2.0));\n assignments.insert(VarId(1), ConstraintValue::Real(3.0));\n \n let context = ConstraintContext {\n assignments,\n tolerance: 1e-6,\n };\n \n // Test expression evaluation: x + y\n use theory_core::ir::{Expr, BinaryOp};\n \n let expr = Expr::Binary {\n op: BinaryOp::Add,\n lhs: Box::new(Expr::Var(VarId(0))),\n rhs: Box::new(Expr::Var(VarId(1))),\n };\n \n let result = checker.evaluate_expression(&expr, &context)?;\n \n match result {\n ConstraintValue::Real(val) => {\n assert!((val - 5.0).abs() < 1e-6);\n }\n _ => panic!(\"Expected real value\"),\n }\n \n Ok(())\n}\n\n#[test]\nfn test_routing_decisions() -> Result<()> {\n let router = SpeculateVerifyRouter::new();\n \n // Create simple constraint IR\n let mut ir = ConstraintIR::new();\n use theory_core::ir::{Variable, Domain, VariableMetadata};\n \n let var = Variable {\n name: \"x\".to_string(),\n domain: Domain::Real { min: Some(0.0), max: Some(1.0) },\n metadata: VariableMetadata::default(),\n };\n \n ir.add_variable(var);\n ir.add_theory_tag(theory_core::ir::TheoryTag::LRA);\n \n // Get routing decision\n let strategy = router.route(&ir)?;\n \n // Should return some valid strategy\n match strategy {\n ReasoningStrategy::Speculate => println!(\"Router chose speculation\"),\n ReasoningStrategy::Verify => println!(\"Router chose verification\"),\n ReasoningStrategy::Hybrid => println!(\"Router chose hybrid approach\"),\n }\n \n Ok(())\n}\n