theory_core 0.1.0

//! Theory Core: Neuro-Symbolic Reasoning Engine
//!
//! This crate provides the foundation for Phase 2A neuro-symbolic integration,
//! combining Lightning Strike's cognitive architecture with formal constraint
//! satisfaction and SMT solver verification.
//!
//! # Architecture Overview
//!
//! The theory core follows a modular architecture:
//! - **Constraint IR**: Typed intermediate representation for constraints
//! - **Theory Generator**: Neural network that maps inputs to constraint IR
//! - **Solver Surrogate**: Fast neural approximation of solver results
//! - **SMT Backend**: Integration with Z3 and other SMT solvers
//! - **Speculate-Verify**: Fast surrogate proposals with solver verification

pub mod constraint;
pub mod display;
pub mod generator;
pub mod hybrid;
pub mod ir;
pub mod learning;
pub mod lightning_strike;
pub mod meta_reasoning;
pub mod optimization;
pub mod router;
pub mod smt_stub;
pub mod z3_backend;

use serde::{Deserialize, Serialize};
pub use smt_stub as smt;
pub mod surrogate;
pub mod verify;

// Public re-exports
pub use constraint::*;
pub use generator::*;
pub use hybrid::*;
pub use ir::*;
pub use learning::*;
pub use lightning_strike::*;
pub use meta_reasoning::*;
pub use optimization::*;
pub use router::*;
pub use smt_stub::*; // Includes SmtBackend
pub use surrogate::*;
pub use verify::*;
pub use z3_backend::*;

use anyhow::Result;
// use eenn::tensor::Tensor;  // Removed due to circular dependency
// use lightning_strike::session::Session;  // Temporarily disabled

/// Main neuro-symbolic reasoning engine that combines Lightning Strike
/// cognitive architecture with formal constraint satisfaction.
pub struct NeuroSymbolicEngine {
    /// Lightning Strike session for cognitive reasoning (placeholder)
    // cognitive_session: Session,
    /// Theory generator (neural network)
    theory_generator: Box<dyn TheoryGenerator>,
    /// Solver surrogate (fast neural approximation)
    solver_surrogate: Box<dyn SolverSurrogate>,
    /// SMT solver backend
    smt_backend: SmtBackend,
    /// Routing decisions for speculation vs verification
    router: SpeculateVerifyRouter,
}

impl NeuroSymbolicEngine {
    /// Create a new neuro-symbolic engine
    pub fn new(
        theory_generator: Box<dyn TheoryGenerator>,
        solver_surrogate: Box<dyn SolverSurrogate>,
        smt_backend: SmtBackend,
    ) -> Result<Self> {
        // let cognitive_session = Session::new()?;
        let router = SpeculateVerifyRouter::new();

        Ok(Self {
            // cognitive_session,
            theory_generator,
            solver_surrogate,
            smt_backend,
            router,
        })
    }

    /// Reason about a problem using neuro-symbolic integration
    pub async fn reason(&mut self, input: &Tensor) -> Result<ReasoningResult> {
        // Generate constraint IR from input using neural theory generator
        let constraint_ir = self.theory_generator.generate_constraints(input)?;

        // Use router to decide between speculation and verification
        let strategy = self.router.route(&constraint_ir)?;

        match strategy {
            ReasoningStrategy::Speculate => {
                // Use fast neural surrogate
                let result = self.solver_surrogate.predict_solution(&constraint_ir)?;

                // Validate with plausibility checks
                if self.validate_plausibility(&constraint_ir, &result)? {
                    Ok(ReasoningResult::Speculated(result))
                } else {
                    // Fallback to verification
                    self.verify_with_smt(&constraint_ir).await
                }
            }
            ReasoningStrategy::Verify => {
                // Use SMT solver directly
                self.verify_with_smt(&constraint_ir).await
            }
            ReasoningStrategy::Hybrid => {
                // Use both and compare
                let speculated = self.solver_surrogate.predict_solution(&constraint_ir)?;
                let verified = self.verify_with_smt(&constraint_ir).await?;

                Ok(ReasoningResult::Hybrid {
                    speculated,
                    verified: match verified {
                        ReasoningResult::Verified(sol) => sol,
                        _ => return Err(anyhow::anyhow!("Expected verified result")),
                    },
                })
            }
        }
    }

    /// Validate solution using fast plausibility checks
    fn validate_plausibility(
        &self,
        constraint_ir: &ConstraintIR,
        result: &SolutionResult,
    ) -> Result<bool> {
        use crate::verify::{PlausibilityChecker, PlausibilityConfig};

        let checker = PlausibilityChecker::new(PlausibilityConfig::default());
        let plausibility_result = checker.check_plausibility(constraint_ir, result)?;

        Ok(plausibility_result.plausible)
    }

    /// Verify constraints using SMT solver
    async fn verify_with_smt(&mut self, constraint_ir: &ConstraintIR) -> Result<ReasoningResult> {
        let solution = self.smt_backend.solve(constraint_ir).await?;
        Ok(ReasoningResult::Verified(solution))
    }
}

/// Strategy for reasoning about constraints
#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
pub enum ReasoningStrategy {
    /// Use fast neural surrogate only
    Speculate,
    /// Use SMT solver verification only
    Verify,
    /// Use both and compare results
    Hybrid,
}

/// Result of neuro-symbolic reasoning
#[derive(Debug, Clone)]
pub enum ReasoningResult {
    /// Result from neural surrogate only
    Speculated(SolutionResult),
    /// Result from SMT solver verification
    Verified(SolutionResult),
    /// Results from both approaches
    Hybrid {
        speculated: SolutionResult,
        verified: SolutionResult,
    },
}