oxiz-solver 0.2.0

//! Finite Model Finding
//!
//! This module implements finite model finding for quantified formulas.
//! The goal is to find a finite model that satisfies all quantified formulas,
//! or prove that no such model exists within a given bound.
//!
//! # Algorithm
//!
//! 1. **Bounded Search**: Search for models up to a maximum universe size
//! 2. **Symmetry Breaking**: Add constraints to eliminate symmetric models
//! 3. **Incremental Refinement**: Start with small domains and expand
//! 4. **Conflict-Driven**: Learn from failed attempts

#![allow(missing_docs)]
#![allow(dead_code)]

#[allow(unused_imports)]
use crate::prelude::*;
use core::fmt;
use oxiz_core::ast::{TermId, TermManager};
use oxiz_core::sort::SortId;

use super::QuantifiedFormula;
use super::model_completion::CompletedModel;

/// Size of a finite universe
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub struct UniverseSize(pub usize);

impl UniverseSize {
    /// Create a new universe size
    pub fn new(size: usize) -> Self {
        Self(size)
    }

    /// Get the size
    pub fn size(&self) -> usize {
        self.0
    }

    /// Check if this is a trivial size
    pub fn is_trivial(&self) -> bool {
        self.0 <= 1
    }

    /// Get the next larger size
    pub fn next(&self) -> Self {
        Self(self.0 + 1)
    }

    /// Get total number of possible assignments for n variables
    pub fn total_assignments(&self, num_vars: usize) -> usize {
        self.0.pow(num_vars as u32)
    }
}

impl fmt::Display for UniverseSize {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        write!(f, "|U|={}", self.0)
    }
}

/// A finite model with bounded universes
#[derive(Debug, Clone)]
pub struct FiniteModel {
    /// Base completed model
    pub model: CompletedModel,
    /// Universe sizes for each sort
    pub universe_sizes: FxHashMap<SortId, UniverseSize>,
    /// Total number of elements in all universes
    pub total_elements: usize,
}

impl FiniteModel {
    /// Create a new finite model
    pub fn new(model: CompletedModel) -> Self {
        let mut total_elements = 0;
        let mut universe_sizes = FxHashMap::default();

        for (sort, universe) in &model.universes {
            let size = UniverseSize::new(universe.len());
            universe_sizes.insert(*sort, size);
            total_elements += universe.len();
        }

        Self {
            model,
            universe_sizes,
            total_elements,
        }
    }

    /// Get the universe size for a sort
    pub fn universe_size(&self, sort: SortId) -> Option<UniverseSize> {
        self.universe_sizes.get(&sort).copied()
    }

    /// Check if this model satisfies a quantified formula (approximation)
    pub fn satisfies(
        &self,
        _quantifier: &QuantifiedFormula,
        _manager: &TermManager,
    ) -> Option<bool> {
        // Placeholder - full implementation would evaluate the quantifier
        None
    }
}

/// Finite model finder
#[derive(Debug)]
pub struct FiniteModelFinder {
    /// Minimum universe size to try
    min_size: UniverseSize,
    /// Maximum universe size to try
    max_size: UniverseSize,
    /// Current search bound
    current_bound: UniverseSize,
    /// Symmetry breaker
    symmetry_breaker: SymmetryBreaker,
    /// Statistics
    stats: FinderStats,
    /// Learned constraints (for conflict-driven search)
    learned_constraints: Vec<TermId>,
}

impl FiniteModelFinder {
    /// Create a new finite model finder
    pub fn new() -> Self {
        Self {
            min_size: UniverseSize::new(1),
            max_size: UniverseSize::new(8),
            current_bound: UniverseSize::new(1),
            symmetry_breaker: SymmetryBreaker::new(),
            stats: FinderStats::default(),
            learned_constraints: Vec::new(),
        }
    }

    /// Create with custom size bounds
    pub fn with_bounds(min: usize, max: usize) -> Self {
        let mut finder = Self::new();
        finder.min_size = UniverseSize::new(min);
        finder.max_size = UniverseSize::new(max);
        finder.current_bound = UniverseSize::new(min);
        finder
    }

    /// Find a finite model for the given quantifiers
    pub fn find_model(
        &mut self,
        quantifiers: &[QuantifiedFormula],
        partial_model: &FxHashMap<TermId, TermId>,
        manager: &mut TermManager,
    ) -> Result<FiniteModel, FinderError> {
        self.stats.num_searches += 1;
        self.current_bound = self.min_size;

        // Incremental search with increasing bounds
        while self.current_bound <= self.max_size {
            self.stats.num_iterations += 1;

            match self.find_model_with_bound(
                quantifiers,
                partial_model,
                manager,
                self.current_bound,
            ) {
                Ok(model) => {
                    self.stats.num_models_found += 1;
                    return Ok(model);
                }
                Err(FinderError::UnsatAtBound) => {
                    // Try larger bound
                    self.current_bound = self.current_bound.next();
                }
                Err(e) => return Err(e),
            }
        }

        Err(FinderError::ExceededMaxBound)
    }

    /// Find a model with a specific universe size bound
    fn find_model_with_bound(
        &mut self,
        quantifiers: &[QuantifiedFormula],
        partial_model: &FxHashMap<TermId, TermId>,
        manager: &mut TermManager,
        bound: UniverseSize,
    ) -> Result<FiniteModel, FinderError> {
        // Build base model
        let mut model = CompletedModel::new();
        model.assignments = partial_model.clone();

        // Identify sorts that need finite universes
        let uninterp_sorts = self.identify_uninterpreted_sorts(quantifiers, manager);

        // Create universes for each sort
        for sort in uninterp_sorts {
            let universe = self.create_universe(sort, bound, manager);
            model.universes.insert(sort, universe);
        }

        // Add symmetry breaking constraints
        let sb_constraints =
            self.symmetry_breaker
                .generate_constraints(&model, quantifiers, manager);
        self.learned_constraints.extend(sb_constraints);

        // Check if this model works (simplified)
        let finite_model = FiniteModel::new(model);

        // Verify against quantifiers
        for quantifier in quantifiers {
            if let Some(false) = finite_model.satisfies(quantifier, manager) {
                return Err(FinderError::UnsatAtBound);
            }
        }

        Ok(finite_model)
    }

    /// Identify uninterpreted sorts in quantifiers
    fn identify_uninterpreted_sorts(
        &self,
        quantifiers: &[QuantifiedFormula],
        manager: &TermManager,
    ) -> Vec<SortId> {
        let mut sorts = Vec::new();
        let mut seen = FxHashSet::default();

        for quantifier in quantifiers {
            for &(_name, sort) in &quantifier.bound_vars {
                if self.is_uninterpreted(sort, manager) && seen.insert(sort) {
                    sorts.push(sort);
                }
            }
        }

        sorts
    }

    fn is_uninterpreted(&self, sort: SortId, manager: &TermManager) -> bool {
        sort != manager.sorts.bool_sort
            && sort != manager.sorts.int_sort
            && sort != manager.sorts.real_sort
    }

    /// Create a universe of the given size for a sort
    fn create_universe(
        &self,
        sort: SortId,
        size: UniverseSize,
        manager: &mut TermManager,
    ) -> Vec<TermId> {
        let mut universe = Vec::new();

        for i in 0..size.size() {
            let name = format!("u!{}!{}", sort.0, i);
            let elem = manager.mk_var(&name, sort);
            universe.push(elem);
        }

        universe
    }

    /// Get statistics
    pub fn stats(&self) -> &FinderStats {
        &self.stats
    }

    /// Reset the finder
    pub fn reset(&mut self) {
        self.current_bound = self.min_size;
        self.learned_constraints.clear();
    }
}

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

/// Symmetry breaker for reducing search space
#[derive(Debug)]
pub struct SymmetryBreaker {
    /// Strategy for breaking symmetries
    strategy: SymmetryStrategy,
    /// Statistics
    stats: SymmetryStats,
}

impl SymmetryBreaker {
    /// Create a new symmetry breaker
    pub fn new() -> Self {
        Self {
            strategy: SymmetryStrategy::LeastNumber,
            stats: SymmetryStats::default(),
        }
    }

    /// Create with specific strategy
    pub fn with_strategy(strategy: SymmetryStrategy) -> Self {
        let mut breaker = Self::new();
        breaker.strategy = strategy;
        breaker
    }

    /// Generate symmetry breaking constraints
    pub fn generate_constraints(
        &mut self,
        model: &CompletedModel,
        quantifiers: &[QuantifiedFormula],
        manager: &mut TermManager,
    ) -> Vec<TermId> {
        let mut constraints = Vec::new();

        match self.strategy {
            SymmetryStrategy::None => {}
            SymmetryStrategy::LeastNumber => {
                constraints.extend(self.generate_least_number_constraints(model, manager));
            }
            SymmetryStrategy::OrderConstraints => {
                constraints.extend(self.generate_order_constraints(model, quantifiers, manager));
            }
            SymmetryStrategy::PredecessorConstraints => {
                constraints.extend(self.generate_predecessor_constraints(model, manager));
            }
        }

        self.stats.num_constraints_generated += constraints.len();
        constraints
    }

    /// Generate least-number symmetry breaking constraints
    /// Ensures that if element i is used, all elements 0..i-1 must be used
    fn generate_least_number_constraints(
        &self,
        model: &CompletedModel,
        manager: &mut TermManager,
    ) -> Vec<TermId> {
        let mut constraints = Vec::new();

        for universe in model.universes.values() {
            // For each pair (i, j) where i < j,
            // if j is used then i must be used
            for i in 0..universe.len() {
                for j in (i + 1)..universe.len() {
                    // Create: used(j) => used(i)
                    // We approximate "used" by existence in model
                    let elem_i = universe[i];
                    let elem_j = universe[j];

                    // Placeholder constraint (in real impl, would track usage)
                    // Build arguments first to avoid multiple mutable borrows
                    let cond = manager.mk_eq(elem_j, elem_j); // j is used
                    let conseq = manager.mk_eq(elem_i, elem_i); // i is used
                    let constraint = manager.mk_implies(cond, conseq);
                    constraints.push(constraint);
                }
            }
        }

        constraints
    }

    /// Generate order constraints for breaking symmetries
    fn generate_order_constraints(
        &self,
        model: &CompletedModel,
        _quantifiers: &[QuantifiedFormula],
        manager: &mut TermManager,
    ) -> Vec<TermId> {
        let mut constraints = Vec::new();

        for universe in model.universes.values() {
            // Add ordering constraints between elements
            for i in 0..(universe.len().saturating_sub(1)) {
                let elem_i = universe[i];
                let elem_j = universe[i + 1];

                // Add: elem_i < elem_j (if applicable)
                // This is a simplification - real implementation would use
                // a designated ordering predicate
                let constraint = manager.mk_lt(elem_i, elem_j);
                constraints.push(constraint);
            }
        }

        constraints
    }

    /// Generate predecessor constraints
    fn generate_predecessor_constraints(
        &self,
        model: &CompletedModel,
        manager: &mut TermManager,
    ) -> Vec<TermId> {
        let mut constraints = Vec::new();

        for universe in model.universes.values() {
            if universe.len() < 2 {
                continue;
            }

            // For each element except the first, require a distinct predecessor
            for i in 1..universe.len() {
                let elem = universe[i];
                let mut predecessors = Vec::new();

                #[allow(clippy::needless_range_loop)]
                for j in 0..i {
                    predecessors.push(universe[j]);
                }

                // Create disjunction: elem has at least one predecessor
                if !predecessors.is_empty() {
                    let mut disj_terms = Vec::new();
                    for pred in predecessors {
                        // Create some relation (simplified)
                        let rel = manager.mk_eq(pred, elem);
                        disj_terms.push(rel);
                    }
                    let constraint = manager.mk_or(disj_terms);
                    constraints.push(constraint);
                }
            }
        }

        constraints
    }

    /// Get statistics
    pub fn stats(&self) -> &SymmetryStats {
        &self.stats
    }
}

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

/// Strategy for symmetry breaking
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum SymmetryStrategy {
    /// No symmetry breaking
    None,
    /// Least number heuristic
    LeastNumber,
    /// Order-based constraints
    OrderConstraints,
    /// Predecessor constraints
    PredecessorConstraints,
}

/// Domain enumerator for exploring all possible assignments
#[derive(Debug)]
pub struct DomainEnumerator {
    /// Maximum assignments to enumerate
    max_assignments: usize,
    /// Current assignment index
    current_index: usize,
}

impl DomainEnumerator {
    /// Create a new enumerator
    pub fn new(max_assignments: usize) -> Self {
        Self {
            max_assignments,
            current_index: 0,
        }
    }

    /// Enumerate all assignments for variables over domains
    pub fn enumerate(&mut self, domains: &[Vec<TermId>]) -> Vec<Vec<TermId>> {
        let mut results = Vec::new();
        let mut indices = vec![0usize; domains.len()];

        while results.len() < self.max_assignments {
            // Build current assignment
            let assignment: Vec<TermId> = indices
                .iter()
                .enumerate()
                .filter_map(|(i, &idx)| domains.get(i).and_then(|d| d.get(idx).copied()))
                .collect();

            if assignment.len() == domains.len() {
                results.push(assignment);
            }

            // Increment indices
            let mut carry = true;
            for (i, idx) in indices.iter_mut().enumerate() {
                if carry {
                    *idx += 1;
                    let limit = domains.get(i).map_or(1, |d| d.len());
                    if *idx >= limit {
                        *idx = 0;
                    } else {
                        carry = false;
                    }
                }
            }

            if carry {
                break; // Exhausted all assignments
            }
        }

        results
    }

    /// Reset the enumerator
    pub fn reset(&mut self) {
        self.current_index = 0;
    }
}

/// Bounded model checker for quantified formulas
#[derive(Debug)]
pub struct BoundedModelChecker {
    /// Current depth bound
    depth_bound: usize,
    /// Maximum depth to explore
    max_depth: usize,
}

impl BoundedModelChecker {
    /// Create a new bounded model checker
    pub fn new() -> Self {
        Self {
            depth_bound: 0,
            max_depth: 10,
        }
    }

    /// Check if quantifiers are satisfiable within bound
    pub fn check(
        &mut self,
        _quantifiers: &[QuantifiedFormula],
        _model: &CompletedModel,
        _manager: &TermManager,
    ) -> CheckResult {
        // Placeholder implementation
        CheckResult::Unknown
    }

    /// Increment depth bound
    pub fn increase_bound(&mut self) {
        self.depth_bound += 1;
    }

    /// Check if at max depth
    pub fn at_max_depth(&self) -> bool {
        self.depth_bound >= self.max_depth
    }
}

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

/// Result of bounded model checking
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum CheckResult {
    /// Satisfiable
    Sat,
    /// Unsatisfiable within bound
    Unsat,
    /// Unknown
    Unknown,
}

/// Error during finite model finding
#[derive(Debug, Clone)]
pub enum FinderError {
    /// Unsatisfiable at the current bound
    UnsatAtBound,
    /// Exceeded maximum universe size bound
    ExceededMaxBound,
    /// Resource limit exceeded
    ResourceLimit,
    /// Invalid configuration
    InvalidConfig(String),
}

impl fmt::Display for FinderError {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::UnsatAtBound => write!(f, "Unsatisfiable at current bound"),
            Self::ExceededMaxBound => write!(f, "Exceeded maximum universe size"),
            Self::ResourceLimit => write!(f, "Resource limit exceeded"),
            Self::InvalidConfig(msg) => write!(f, "Invalid configuration: {}", msg),
        }
    }
}

impl core::error::Error for FinderError {}

/// Statistics for finite model finding
#[derive(Debug, Clone, Default)]
pub struct FinderStats {
    /// Number of search attempts
    pub num_searches: usize,
    /// Number of iterations (bound increases)
    pub num_iterations: usize,
    /// Number of models found
    pub num_models_found: usize,
}

/// Statistics for symmetry breaking
#[derive(Debug, Clone, Default)]
pub struct SymmetryStats {
    /// Number of constraints generated
    pub num_constraints_generated: usize,
}

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

    #[test]
    fn test_universe_size_creation() {
        let size = UniverseSize::new(5);
        assert_eq!(size.size(), 5);
    }

    #[test]
    fn test_universe_size_trivial() {
        assert!(UniverseSize::new(0).is_trivial());
        assert!(UniverseSize::new(1).is_trivial());
        assert!(!UniverseSize::new(2).is_trivial());
    }

    #[test]
    fn test_universe_size_next() {
        let size = UniverseSize::new(3);
        assert_eq!(size.next().size(), 4);
    }

    #[test]
    fn test_universe_size_assignments() {
        let size = UniverseSize::new(2);
        assert_eq!(size.total_assignments(3), 8); // 2^3
    }

    #[test]
    fn test_universe_size_display() {
        let size = UniverseSize::new(5);
        assert_eq!(format!("{}", size), "|U|=5");
    }

    #[test]
    fn test_finite_model_creation() {
        let model = CompletedModel::new();
        let finite = FiniteModel::new(model);
        assert_eq!(finite.total_elements, 0);
    }

    #[test]
    fn test_finite_model_finder_creation() {
        let finder = FiniteModelFinder::new();
        assert_eq!(finder.min_size.size(), 1);
        assert_eq!(finder.max_size.size(), 8);
    }

    #[test]
    fn test_finite_model_finder_with_bounds() {
        let finder = FiniteModelFinder::with_bounds(2, 10);
        assert_eq!(finder.min_size.size(), 2);
        assert_eq!(finder.max_size.size(), 10);
    }

    #[test]
    fn test_symmetry_breaker_creation() {
        let breaker = SymmetryBreaker::new();
        assert_eq!(breaker.strategy, SymmetryStrategy::LeastNumber);
    }

    #[test]
    fn test_symmetry_breaker_with_strategy() {
        let breaker = SymmetryBreaker::with_strategy(SymmetryStrategy::OrderConstraints);
        assert_eq!(breaker.strategy, SymmetryStrategy::OrderConstraints);
    }

    #[test]
    fn test_symmetry_strategy_equality() {
        assert_eq!(SymmetryStrategy::None, SymmetryStrategy::None);
        assert_ne!(SymmetryStrategy::None, SymmetryStrategy::LeastNumber);
    }

    #[test]
    fn test_domain_enumerator_creation() {
        let enumerator = DomainEnumerator::new(100);
        assert_eq!(enumerator.max_assignments, 100);
    }

    #[test]
    fn test_domain_enumerator_enumerate_empty() {
        let mut enumerator = DomainEnumerator::new(100);
        let results = enumerator.enumerate(&[]);
        assert_eq!(results.len(), 1);
        assert!(results[0].is_empty());
    }

    #[test]
    fn test_domain_enumerator_enumerate_single() {
        let mut enumerator = DomainEnumerator::new(100);
        let domains = vec![vec![TermId::new(1), TermId::new(2)]];
        let results = enumerator.enumerate(&domains);
        assert_eq!(results.len(), 2);
    }

    #[test]
    fn test_bounded_model_checker_creation() {
        let checker = BoundedModelChecker::new();
        assert_eq!(checker.depth_bound, 0);
        assert_eq!(checker.max_depth, 10);
    }

    #[test]
    fn test_bounded_model_checker_depth() {
        let mut checker = BoundedModelChecker::new();
        assert!(!checker.at_max_depth());
        for _ in 0..10 {
            checker.increase_bound();
        }
        assert!(checker.at_max_depth());
    }

    #[test]
    fn test_check_result_equality() {
        assert_eq!(CheckResult::Sat, CheckResult::Sat);
        assert_ne!(CheckResult::Sat, CheckResult::Unsat);
    }

    #[test]
    fn test_finder_error_display() {
        let err = FinderError::UnsatAtBound;
        assert!(format!("{}", err).contains("Unsatisfiable"));
    }
}