//! Error types for the verifier.

use thiserror::Error;

/// Verifier error types.
#[derive(Error, Debug)]
pub enum VerifierError {
    /// Parse error in specification.
    #[error("Parse error at line {line}: {message}")]
    ParseError { line: usize, message: String },

    /// Type error in expression.
    #[error("Type error: {0}")]
    TypeError(String),

    /// Unknown variable reference.
    #[error("Unknown variable: {0}")]
    UnknownVariable(String),

    /// Unknown function reference.
    #[error("Unknown function: {0}")]
    UnknownFunction(String),

    /// SMT solver error.
    #[error("SMT solver error: {0}")]
    SmtError(String),

    /// Timeout during verification.
    #[error("Verification timeout after {0}ms")]
    Timeout(u64),

    /// Verification proved false.
    #[error("Property falsified: {0}")]
    Falsified(String),

    /// Internal error.
    #[error("Internal error: {0}")]
    Internal(String),

    /// Unsupported feature.
    #[error("Unsupported: {0}")]
    Unsupported(String),

    /// IO error.
    #[error("IO error: {0}")]
    Io(#[from] std::io::Error),

    /// JSON error.
    #[error("JSON error: {0}")]
    Json(#[from] serde_json::Error),
}

/// Result type for verifier operations.
pub type VerifierResult<T> = Result<T, VerifierError>;