mod all_different;
mod arithmetic;
mod linear;
mod nogood;
mod time_table;

use pumpkin_checking::SupportingInference;
use pumpkin_checking::VariableState;

use crate::model::Atomic;
use crate::model::Model;

#[derive(Clone, Debug, PartialEq, Eq)]
pub struct Fact {
    pub premises: Vec<Atomic>,
    pub consequent: Option<Atomic>,
}

impl From<SupportingInference<Atomic>> for Fact {
    fn from(value: SupportingInference<Atomic>) -> Self {
        Fact {
            premises: value.premises,
            consequent: value.consequent,
        }
    }
}

impl Fact {
    /// Create a fact `premises -> false`.
    pub fn nogood(premises: Vec<Atomic>) -> Self {
        Fact {
            premises,
            consequent: None,
        }
    }
}

/// The reasons an inference can be rejected.
#[derive(Clone, Copy, thiserror::Error, Debug)]
#[error("invalid inference")]
pub enum InvalidInference {
    /// The inference is not annotated with a label when we expect it to be.
    #[error("inference does not have a label")]
    MissingLabel,

    /// The label of the inference is not recognized by the checker.
    #[error("inference is not supported")]
    UnsupportedLabel,

    /// The inference label is not sound for the constraint that generated the inference.
    #[error("indicated constraint cannot generate inferences with the indicated label")]
    ConstraintLabelMismatch,

    /// The constraint that generated the inference does not exist in the model.
    #[error("generated by undefined constraint")]
    UndefinedConstraint,

    /// The inference does not state which constraint generated it.
    #[error("the constraint hint points to an unknown constraint ID")]
    MissingConstraint,

    /// The premises of the inference are inconsistent.
    #[error("inconsistent premises")]
    InconsistentPremises,

    /// The inference is unsound for the constraint.
    #[error("inference is unsound")]
    Unsound,
}

pub(crate) fn verify_inference(
    model: &Model,
    inference: &drcp_format::Inference<std::rc::Rc<str>, i32, std::rc::Rc<str>>,
) -> Result<Fact, InvalidInference> {
    let fact = Fact {
        premises: inference.premises.iter().cloned().map(Into::into).collect(),
        consequent: inference.consequent.clone().map(Into::into),
    };

    let label = inference
        .label
        .as_ref()
        .map(|label| label.as_ref())
        .ok_or(InvalidInference::MissingLabel)?;

    // The initial domain inference is handled separately since it is the only inference that
    // does not expect a constraint hint.
    if label == "initial_domain" {
        let Some(atomic) = inference.consequent.clone() else {
            // The initial domain inference requires a consequent.
            return Err(InvalidInference::Unsound);
        };

        let atomic: Atomic = atomic.into();

        if !model.is_trivially_true(&atomic) {
            // If the consequent is not trivially true in the model then the inference
            // is unsound.
            return Err(InvalidInference::Unsound);
        }

        return Ok(fact);
    }

    // Setup the state for a conflict check.
    let variable_state =
        VariableState::prepare_for_conflict_check(fact.premises.clone(), fact.consequent.clone())
            .map_err(|_| InvalidInference::InconsistentPremises)?;

    // Get the constraint that generated the inference from the model.
    let generated_by_constraint_id = inference
        .generated_by
        .ok_or(InvalidInference::MissingConstraint)?;
    let generated_by = model
        .get_constraint(generated_by_constraint_id)
        .ok_or(InvalidInference::MissingConstraint)?;

    match label {
        "linear_bounds" => {
            linear::verify_linear_bounds(&fact, generated_by, variable_state)?;
        }

        "nogood" => {
            nogood::verify_nogood(&fact, generated_by, variable_state)?;
        }

        "time_table" => {
            time_table::verify_time_table(&fact, generated_by, variable_state)?;
        }

        "all_different" => {
            all_different::verify_all_different(&fact, generated_by, variable_state)?;
        }

        "binary_equals" => {
            arithmetic::verify_binary_equals(&fact, generated_by, variable_state)?;
        }

        "binary_not_equals" => {
            arithmetic::verify_binary_not_equals(&fact, generated_by, variable_state)?;
        }

        _ => return Err(InvalidInference::UnsupportedLabel),
    }

    Ok(fact)
}
