theory_core 0.1.0

//! Verification Utilities for Neuro-Symbolic Systems
//!
//! Provides fast plausibility checks and constraint validation
//! to avoid expensive SMT solver calls when possible.

use crate::ir::ConstraintIR;
use crate::surrogate::SolutionResult;
use anyhow::Result;
use serde::{Deserialize, Serialize};

/// Fast plausibility checker to validate solutions before SMT calls
pub struct PlausibilityChecker {
    config: PlausibilityConfig,
}

/// Configuration for plausibility checking
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct PlausibilityConfig {
    /// Enable numeric range checks
    pub check_numeric_ranges: bool,
    /// Enable NaN/infinity checks
    pub check_numeric_validity: bool,
    /// Enable constraint satisfaction approximation
    pub check_constraint_approximation: bool,
    /// Tolerance for approximate constraint satisfaction
    pub constraint_tolerance: f64,
}

impl Default for PlausibilityConfig {
    fn default() -> Self {
        Self {
            check_numeric_ranges: true,
            check_numeric_validity: true,
            check_constraint_approximation: true,
            constraint_tolerance: 1e-6,
        }
    }
}

/// Result of plausibility check
#[derive(Debug, Clone)]
pub struct PlausibilityResult {
    /// Whether the solution passes plausibility checks
    pub plausible: bool,
    /// Confidence in plausibility assessment
    pub confidence: f32,
    /// Specific violations found
    pub violations: Vec<PlausibilityViolation>,
}

/// Specific plausibility violation
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct PlausibilityViolation {
    /// Type of violation
    pub violation_type: ViolationType,
    /// Description of the violation
    pub description: String,
    /// Severity (0.0 = minor, 1.0 = major)
    pub severity: f32,
}

/// Types of plausibility violations
#[derive(Debug, Clone, Serialize, Deserialize)]
pub enum ViolationType {
    /// Numeric value out of expected range
    NumericRange,
    /// Invalid numeric value (NaN, infinity)
    NumericInvalid,
    /// Constraint approximately violated
    ConstraintViolation,
    /// Type mismatch
    TypeMismatch,
    /// Missing required variable
    MissingVariable,
}

impl PlausibilityChecker {
    pub fn new(config: PlausibilityConfig) -> Self {
        Self { config }
    }

    /// Check if a solution is plausible given the constraints
    pub fn check_plausibility(
        &self,
        constraints: &ConstraintIR,
        solution: &SolutionResult,
    ) -> Result<PlausibilityResult> {
        let mut violations = Vec::new();

        if !solution.satisfiable {
            // If solution claims unsatisfiable, always accept for now
            // (Could add unsat core validation later)
            return Ok(PlausibilityResult {
                plausible: true,
                confidence: 1.0,
                violations,
            });
        }

        // Check variable assignments against domains
        if self.config.check_numeric_ranges {
            self.check_variable_domains(constraints, solution, &mut violations)?;
        }

        // Check for invalid numeric values
        if self.config.check_numeric_validity {
            self.check_numeric_validity(solution, &mut violations)?;
        }

        // Approximately check constraint satisfaction
        if self.config.check_constraint_approximation {
            self.check_constraint_satisfaction(constraints, solution, &mut violations)?;
        }

        // Compute overall plausibility
        let plausible = violations.is_empty() || violations.iter().all(|v| v.severity < 0.5);

        let confidence = if violations.is_empty() {
            0.95
        } else {
            let max_severity = violations.iter().map(|v| v.severity).fold(0.0, f32::max);
            (1.0 - max_severity).max(0.1)
        };

        Ok(PlausibilityResult {
            plausible,
            confidence,
            violations,
        })
    }

    /// Check variable assignments against their domains
    fn check_variable_domains(
        &self,
        constraints: &ConstraintIR,
        solution: &SolutionResult,
        violations: &mut Vec<PlausibilityViolation>,
    ) -> Result<()> {
        for (var_id, variable) in &constraints.variables {
            let var_name = format!("v{}", var_id.0);

            if let Some(value) = solution.assignment.get(&var_name) {
                match (&variable.domain, value) {
                    (
                        crate::ir::Domain::Real { min, max },
                        crate::surrogate::SolutionValue::Real(val),
                    ) => {
                        if let Some(min_val) = min {
                            if val < min_val {
                                violations.push(PlausibilityViolation {
                                    violation_type: ViolationType::NumericRange,
                                    description: format!(
                                        "Variable {} value {} below minimum {}",
                                        var_name, val, min_val
                                    ),
                                    severity: 0.8,
                                });
                            }
                        }

                        if let Some(max_val) = max {
                            if val > max_val {
                                violations.push(PlausibilityViolation {
                                    violation_type: ViolationType::NumericRange,
                                    description: format!(
                                        "Variable {} value {} above maximum {}",
                                        var_name, val, max_val
                                    ),
                                    severity: 0.8,
                                });
                            }
                        }
                    }
                    (
                        crate::ir::Domain::Integer { min, max },
                        crate::surrogate::SolutionValue::Integer(val),
                    ) => {
                        if let Some(min_val) = min {
                            if val < min_val {
                                violations.push(PlausibilityViolation {
                                    violation_type: ViolationType::NumericRange,
                                    description: format!(
                                        "Variable {} value {} below minimum {}",
                                        var_name, val, min_val
                                    ),
                                    severity: 0.9,
                                });
                            }
                        }

                        if let Some(max_val) = max {
                            if val > max_val {
                                violations.push(PlausibilityViolation {
                                    violation_type: ViolationType::NumericRange,
                                    description: format!(
                                        "Variable {} value {} above maximum {}",
                                        var_name, val, max_val
                                    ),
                                    severity: 0.9,
                                });
                            }
                        }
                    }
                    _ => {
                        // Type mismatch or unsupported domain type
                        violations.push(PlausibilityViolation {
                            violation_type: ViolationType::TypeMismatch,
                            description: format!(
                                "Variable {} has type mismatch between domain and assignment",
                                var_name
                            ),
                            severity: 0.7,
                        });
                    }
                }
            } else {
                // Missing variable assignment
                violations.push(PlausibilityViolation {
                    violation_type: ViolationType::MissingVariable,
                    description: format!("Missing assignment for variable {}", var_name),
                    severity: 0.9,
                });
            }
        }

        Ok(())
    }

    /// Check for invalid numeric values (NaN, infinity)
    fn check_numeric_validity(
        &self,
        solution: &SolutionResult,
        violations: &mut Vec<PlausibilityViolation>,
    ) -> Result<()> {
        for (var_name, value) in &solution.assignment {
            match value {
                crate::surrogate::SolutionValue::Real(val) => {
                    if val.is_nan() {
                        violations.push(PlausibilityViolation {
                            violation_type: ViolationType::NumericInvalid,
                            description: format!("Variable {} has NaN value", var_name),
                            severity: 1.0,
                        });
                    } else if val.is_infinite() {
                        violations.push(PlausibilityViolation {
                            violation_type: ViolationType::NumericInvalid,
                            description: format!("Variable {} has infinite value", var_name),
                            severity: 0.9,
                        });
                    }
                }
                _ => {}
            }
        }

        Ok(())
    }

    /// Approximately check constraint satisfaction
    fn check_constraint_satisfaction(
        &self,
        constraints: &ConstraintIR,
        solution: &SolutionResult,
        violations: &mut Vec<PlausibilityViolation>,
    ) -> Result<()> {
        // Check each constraint against the solution
        for (i, constraint) in constraints.constraints.iter().enumerate() {
            match constraint {
                crate::ir::Constraint::LessEqual { lhs, rhs } => {
                    // Evaluate both sides and check satisfaction
                    if let (Some(lhs_val), Some(rhs_val)) = (
                        self.evaluate_expr_approx(lhs, solution),
                        self.evaluate_expr_approx(rhs, solution),
                    ) {
                        let tolerance = 1e-6;
                        if lhs_val > rhs_val + tolerance {
                            violations.push(PlausibilityViolation {
                                violation_type: ViolationType::ConstraintViolation,
                                description: format!(
                                    "LessEqual constraint {} violated: {} > {} (difference: {})",
                                    i,
                                    lhs_val,
                                    rhs_val,
                                    lhs_val - rhs_val
                                ),
                                severity: 0.9, // High severity
                            });
                        }
                    }
                }
                crate::ir::Constraint::Equal { lhs, rhs } => {
                    // Check equality within tolerance
                    if let (Some(lhs_val), Some(rhs_val)) = (
                        self.evaluate_expr_approx(lhs, solution),
                        self.evaluate_expr_approx(rhs, solution),
                    ) {
                        let tolerance = self.config.constraint_tolerance;
                        if (lhs_val - rhs_val).abs() > tolerance {
                            violations.push(PlausibilityViolation {
                                violation_type: ViolationType::ConstraintViolation,
                                description: format!(
                                    "Equality constraint {} violated: {} ≠ {} (difference: {})",
                                    i,
                                    lhs_val,
                                    rhs_val,
                                    (lhs_val - rhs_val).abs()
                                ),
                                severity: 0.7, // Medium severity
                            });
                        }
                    }
                }
                _ => {
                    // Other constraint types not yet implemented
                }
            }
        }

        Ok(())
    }

    /// Approximately evaluate an expression given a solution
    fn evaluate_expr_approx(
        &self,
        expr: &crate::ir::Expr,
        solution: &SolutionResult,
    ) -> Option<f64> {
        use crate::ir::Expr;
        match expr {
            Expr::Var(var_id) => {
                // Look up variable value in solution (convert VarId to String)
                let var_key = var_id.to_string();
                solution.assignment.get(&var_key).and_then(|val| match val {
                    crate::surrogate::SolutionValue::Real(r) => Some(*r),
                    crate::surrogate::SolutionValue::Integer(i) => Some(*i as f64),
                    crate::surrogate::SolutionValue::Bool(b) => Some(if *b { 1.0 } else { 0.0 }),
                    _ => None, // String and BitVector not convertible to f64
                })
            }
            Expr::Const(val) => match val {
                crate::ir::ConstValue::Real(r) => Some(*r),
                crate::ir::ConstValue::Integer(i) => Some(*i as f64),
                crate::ir::ConstValue::Bool(b) => Some(if *b { 1.0 } else { 0.0 }),
                crate::ir::ConstValue::String(_) => None,
                crate::ir::ConstValue::BitVector { .. } => None,
            },
            Expr::Binary { op, lhs, rhs } => {
                let lhs_val = self.evaluate_expr_approx(lhs, solution)?;
                let rhs_val = self.evaluate_expr_approx(rhs, solution)?;
                match op {
                    crate::ir::BinaryOp::Add => Some(lhs_val + rhs_val),
                    crate::ir::BinaryOp::Sub => Some(lhs_val - rhs_val),
                    crate::ir::BinaryOp::Mul => Some(lhs_val * rhs_val),
                    crate::ir::BinaryOp::Div => {
                        if rhs_val.abs() > 1e-10 {
                            Some(lhs_val / rhs_val)
                        } else {
                            None // Division by zero
                        }
                    }
                    _ => None, // Other operators not implemented
                }
            }
            _ => None, // Other expression types not implemented
        }
    }
}

impl Default for PlausibilityChecker {
    fn default() -> Self {
        Self::new(PlausibilityConfig::default())
    }
}