//! Proof generation and verification.
//!
//! Integrates with SMT solvers to prove or disprove properties.

use serde::{Deserialize, Serialize};
use std::time::{Duration, Instant};

use crate::ast::Expression;
use crate::error::{VerifierError, VerifierResult};
use crate::smt::{SmtContext, SmtResult};
use crate::symbolic::SymbolicState;

/// Prover configuration.
#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct ProverConfig {
    /// Timeout in milliseconds.
    pub timeout_ms: u64,
    /// Maximum symbolic execution depth.
    pub max_depth: usize,
    /// Maximum loop unrolling iterations.
    pub max_loop_unroll: usize,
    /// Enable counterexample generation.
    pub generate_counterexamples: bool,
    /// Enable proof caching.
    pub enable_caching: bool,
}

impl Default for ProverConfig {
    fn default() -> Self {
        Self {
            timeout_ms: 30000,
            max_depth: 100,
            max_loop_unroll: 10,
            generate_counterexamples: true,
            enable_caching: true,
        }
    }
}

/// Result of a proof attempt.
#[derive(Clone, Debug, Serialize, Deserialize)]
pub enum ProofResult {
    /// Property is proven to hold.
    Proven {
        /// Time taken in milliseconds.
        time_ms: u64,
    },
    /// Property is disproven with counterexample.
    Disproven {
        /// Counterexample assignments.
        counterexample: Counterexample,
        /// Time taken.
        time_ms: u64,
    },
    /// Could not determine (timeout, resource limit).
    Unknown {
        /// Reason for unknown result.
        reason: String,
        /// Time taken.
        time_ms: u64,
    },
}

impl ProofResult {
    /// Returns true if property is proven.
    pub fn is_proven(&self) -> bool {
        matches!(self, ProofResult::Proven { .. })
    }

    /// Returns the counterexample if disproven.
    pub fn counterexample(&self) -> Option<&Counterexample> {
        if let ProofResult::Disproven { counterexample, .. } = self {
            Some(counterexample)
        } else {
            None
        }
    }
}

/// Counterexample showing how property can fail.
#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct Counterexample {
    /// Variable assignments that cause failure.
    pub assignments: Vec<(String, String)>,
    /// Execution trace leading to failure.
    pub trace: Vec<String>,
    /// The failing property.
    pub property: String,
}

impl Counterexample {
    /// Creates a new counterexample.
    pub fn new(property: &str) -> Self {
        Self {
            assignments: Vec::new(),
            trace: Vec::new(),
            property: property.to_string(),
        }
    }

    /// Adds a variable assignment.
    pub fn add_assignment(&mut self, var: &str, value: &str) {
        self.assignments.push((var.to_string(), value.to_string()));
    }

    /// Adds a trace step.
    pub fn add_trace(&mut self, step: &str) {
        self.trace.push(step.to_string());
    }

    /// Formats the counterexample for display.
    pub fn format(&self) -> String {
        let mut s = format!("Counterexample for '{}':\n", self.property);
        s.push_str("  Assignments:\n");
        for (var, val) in &self.assignments {
            s.push_str(&format!("    {} = {}\n", var, val));
        }
        if !self.trace.is_empty() {
            s.push_str("  Trace:\n");
            for (i, step) in self.trace.iter().enumerate() {
                s.push_str(&format!("    {}. {}\n", i + 1, step));
            }
        }
        s
    }
}

/// Main prover interface.
pub struct Prover {
    config: ProverConfig,
    smt: SmtContext,
}

impl Prover {
    /// Creates a new prover with configuration.
    pub fn new(config: ProverConfig) -> Self {
        Self {
            smt: SmtContext::new(config.timeout_ms),
            config,
        }
    }

    /// Proves or disproves an expression holds in all states.
    pub fn prove(&self, expr: &Expression, state: &SymbolicState) -> VerifierResult<ProofResult> {
        let start = Instant::now();
        let _timeout = Duration::from_millis(self.config.timeout_ms);

        // Convert expression and state to SMT constraints
        let constraints = self.smt.encode_state(state)?;
        let property = self.smt.encode_expression(expr)?;

        // Check if negation is unsatisfiable (property always holds)
        let negated = self.smt.negate(&property)?;

        let result = self.smt.check_sat_with_constraints(&constraints, &negated)?;

        let elapsed = start.elapsed().as_millis() as u64;

        if elapsed > self.config.timeout_ms {
            return Ok(ProofResult::Unknown {
                reason: "Timeout".to_string(),
                time_ms: elapsed,
            });
        }

        match result {
            SmtResult::Unsat => {
                // Negation is unsat, so property always holds
                Ok(ProofResult::Proven { time_ms: elapsed })
            }
            SmtResult::Sat(model) => {
                // Found counterexample
                let counterexample = if self.config.generate_counterexamples {
                    self.extract_counterexample(&model, expr)
                } else {
                    Counterexample::new("(counterexample generation disabled)")
                };
                Ok(ProofResult::Disproven {
                    counterexample,
                    time_ms: elapsed,
                })
            }
            SmtResult::Unknown(reason) => Ok(ProofResult::Unknown {
                reason,
                time_ms: elapsed,
            }),
        }
    }

    /// Proves an implication: precondition => postcondition.
    pub fn prove_implication(
        &self,
        precondition: &Expression,
        postcondition: &Expression,
        state: &SymbolicState,
    ) -> VerifierResult<ProofResult> {
        let start = Instant::now();

        // Encode: precondition AND NOT postcondition
        let pre = self.smt.encode_expression(precondition)?;
        let post = self.smt.encode_expression(postcondition)?;
        let neg_post = self.smt.negate(&post)?;

        let constraints = self.smt.encode_state(state)?;

        // If pre AND NOT post is unsat, then pre => post
        let combined = self.smt.and(&pre, &neg_post)?;
        let result = self.smt.check_sat_with_constraints(&constraints, &combined)?;

        let elapsed = start.elapsed().as_millis() as u64;

        match result {
            SmtResult::Unsat => Ok(ProofResult::Proven { time_ms: elapsed }),
            SmtResult::Sat(model) => {
                let counterexample = self.extract_counterexample(&model, postcondition);
                Ok(ProofResult::Disproven {
                    counterexample,
                    time_ms: elapsed,
                })
            }
            SmtResult::Unknown(reason) => Ok(ProofResult::Unknown {
                reason,
                time_ms: elapsed,
            }),
        }
    }

    /// Extracts a counterexample from an SMT model.
    fn extract_counterexample(
        &self,
        model: &[(String, String)],
        expr: &Expression,
    ) -> Counterexample {
        let mut ce = Counterexample::new(&format!("{:?}", expr));

        for (var, val) in model {
            ce.add_assignment(var, val);
        }

        ce
    }

    /// Checks if an expression is satisfiable.
    pub fn check_sat(&self, expr: &Expression) -> VerifierResult<bool> {
        let encoded = self.smt.encode_expression(expr)?;
        let result = self.smt.check_sat(&encoded)?;

        match result {
            SmtResult::Sat(_) => Ok(true),
            SmtResult::Unsat => Ok(false),
            SmtResult::Unknown(reason) => Err(VerifierError::SmtError(reason)),
        }
    }

    /// Simplifies an expression using the SMT solver.
    pub fn simplify(&self, expr: &Expression) -> VerifierResult<Expression> {
        // For now, just return the original expression
        // Full implementation would use SMT solver's simplify
        Ok(expr.clone())
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn test_prover_config_default() {
        let config = ProverConfig::default();
        assert_eq!(config.timeout_ms, 30000);
        assert_eq!(config.max_depth, 100);
        assert!(config.generate_counterexamples);
    }

    #[test]
    fn test_counterexample_format() {
        let mut ce = Counterexample::new("x > 0");
        ce.add_assignment("x", "-1");
        ce.add_trace("Entered function foo");
        ce.add_trace("x assigned -1");

        let formatted = ce.format();
        assert!(formatted.contains("x = -1"));
        assert!(formatted.contains("Entered function foo"));
    }

    #[test]
    fn test_proof_result() {
        let proven = ProofResult::Proven { time_ms: 100 };
        assert!(proven.is_proven());
        assert!(proven.counterexample().is_none());

        let ce = Counterexample::new("test");
        let disproven = ProofResult::Disproven {
            counterexample: ce,
            time_ms: 50,
        };
        assert!(!disproven.is_proven());
        assert!(disproven.counterexample().is_some());
    }

    #[test]
    fn test_prover_creation() {
        let prover = Prover::new(ProverConfig::default());
        assert_eq!(prover.config.timeout_ms, 30000);
    }
}