eenn 0.1.0

//! Integration tests for Phase 4 features: Backend Auto-Selection, Advanced Analytics, and Z3 SMT Integration

#[cfg(test)]
mod phase4_tests {
    use theory_core::{
        AnalyticsSummary, BackendSelector, ComputeBackend, ComputeIntensity, MemoryRequirements,
        OptimizationParameters, TheoryTag, TimeSensitivity, WorkloadProfile,
    };

    #[test]
    fn test_backend_selector_creation() {
        let selector = BackendSelector::new();
        // Should successfully create a backend selector with system detection
        // This test verifies the basic initialization works
    }

    #[test]
    fn test_backend_selection_light_workload() {
        let selector = BackendSelector::new();

        let profile = WorkloadProfile {
            complexity: 0.3,
            variable_count: 5,
            constraint_count: 10,
            theories: vec![TheoryTag::LIA],
            compute_intensity: ComputeIntensity::Light,
            memory_requirements: MemoryRequirements::Small,
            time_sensitivity: TimeSensitivity::Interactive,
        };

        let backend = selector.select_backend(&profile).unwrap();

        // Light workload should prefer CPU
        assert_eq!(backend, ComputeBackend::CPU);
    }

    #[test]
    fn test_backend_selection_heavy_nonlinear() {
        let selector = BackendSelector::new();

        let profile = WorkloadProfile {
            complexity: 0.9,
            variable_count: 100,
            constraint_count: 200,
            theories: vec![TheoryTag::NLA],
            compute_intensity: ComputeIntensity::Extreme,
            memory_requirements: MemoryRequirements::Large,
            time_sensitivity: TimeSensitivity::Batch,
        };

        let backend = selector.select_backend(&profile).unwrap();

        // Heavy nonlinear workload with NLA should prefer SMT if available
        #[cfg(feature = "z3-solver")]
        {
            assert_eq!(backend, ComputeBackend::SMT);
        }

        // Without SMT, should fall back to CPU or hybrid
        #[cfg(not(feature = "z3-solver"))]
        {
            match backend {
                ComputeBackend::CPU => {}
                ComputeBackend::Hybrid { .. } => {}
                _ => panic!("Expected CPU or Hybrid for heavy workload without SMT"),
            }
        }
    }

    #[test]
    fn test_backend_selection_medium_workload() {
        let selector = BackendSelector::new();

        let profile = WorkloadProfile {
            complexity: 0.5,
            variable_count: 50,
            constraint_count: 100,
            theories: vec![TheoryTag::LRA],
            compute_intensity: ComputeIntensity::Medium,
            memory_requirements: MemoryRequirements::Medium,
            time_sensitivity: TimeSensitivity::Interactive,
        };

        let backend = selector.select_backend(&profile).unwrap();

        // Medium workload could be CPU or GPU depending on system
        match backend {
            ComputeBackend::CPU | ComputeBackend::GPU | ComputeBackend::Hybrid { .. } => {}
            _ => panic!("Unexpected backend for medium workload"),
        }
    }

    #[test]
    fn test_backend_selection_realtime() {
        let selector = BackendSelector::new();

        let profile = WorkloadProfile {
            complexity: 0.4,
            variable_count: 20,
            constraint_count: 30,
            theories: vec![TheoryTag::LIA],
            compute_intensity: ComputeIntensity::Medium,
            memory_requirements: MemoryRequirements::Small,
            time_sensitivity: TimeSensitivity::RealTime,
        };

        let backend = selector.select_backend(&profile).unwrap();

        // Real-time should prefer fastest backends
        match backend {
            ComputeBackend::CPU | ComputeBackend::Neural => {}
            _ => panic!("Real-time should use CPU or Neural"),
        }
    }

    #[test]
    #[cfg(feature = "z3-solver")]
    fn test_z3_backend_creation() {
        use theory_core::z3_backend::Z3Backend;

        let backend = Z3Backend::new(5000);
        assert!(backend.is_ok(), "Z3 backend should initialize successfully");
    }

    #[test]
    #[cfg(feature = "z3-solver")]
    fn test_z3_simple_constraint() {
        use theory_core::{BinaryOp, Constraint, ConstraintIR, Expr, VarId, z3_backend::Z3Backend};

        let backend = Z3Backend::new(5000).unwrap();

        // Create a simple constraint: x + y = 10, x = 3
        let x = VarId(0);
        let y = VarId(1);

        let mut ir = ConstraintIR::new();

        // x = 3
        ir.add_constraint(Constraint::Equal {
            lhs: Expr::Var(x.clone()),
            rhs: Expr::Const(3.0),
        });

        // x + y = 10 (so y should be 7)
        ir.add_constraint(Constraint::Equal {
            lhs: Expr::Binary {
                op: BinaryOp::Add,
                lhs: Box::new(Expr::Var(x.clone())),
                rhs: Box::new(Expr::Var(y.clone())),
            },
            rhs: Expr::Const(10.0),
        });

        let result = backend.solve(&ir);

        assert!(result.is_ok(), "Z3 should solve simple constraints");
        let solution = result.unwrap();
        assert!(solution.satisfiable, "Constraints should be satisfiable");
        assert_eq!(
            solution.confidence, 1.0,
            "Z3 solutions should have confidence 1.0"
        );
        assert_eq!(solution.method, "Z3-SMT");
    }

    #[test]
    #[cfg(feature = "z3-solver")]
    fn test_z3_unsatisfiable_constraint() {
        use theory_core::{Constraint, ConstraintIR, Expr, VarId, z3_backend::Z3Backend};

        let backend = Z3Backend::new(5000).unwrap();

        // Create unsatisfiable constraints: x = 5 and x = 10
        let x = VarId(0);

        let mut ir = ConstraintIR::new();
        ir.add_constraint(Constraint::Equal {
            lhs: Expr::Var(x.clone()),
            rhs: Expr::Const(5.0),
        });
        ir.add_constraint(Constraint::Equal {
            lhs: Expr::Var(x.clone()),
            rhs: Expr::Const(10.0),
        });

        let result = backend.solve(&ir);

        // Should detect unsatisfiability
        assert!(
            result.is_err(),
            "Z3 should detect unsatisfiable constraints"
        );
    }
}