ommx 3.0.0-beta.5

//! Instance classes for structural input capabilities.
//!
//! An [`InstanceClass`] is a set of [`crate::Instance`] values defined by OMMX
//! structural conditions. Consumers such as adapters and format writers use
//! membership in that set to describe the exact model structures they accept.
//! An [`InstanceClassClause`] is one conjunctive clause in the representation;
//! an instance class is the finite union of its clauses.
//!
//! For adapters, membership defines whether the exact input is applicable. It
//! does not perform preparation or lowering, handle wire-format
//! `ommx.v2.Feature` values, or guarantee that later conversion and backend
//! operations succeed. If preparation produces another instance to use as
//! input, membership must be checked on that value. Other consumers retain
//! responsibility for side effects and information-loss policies outside
//! these structural conditions.

mod instance_facts;

use crate::{
    ConstraintID, Degree, Equality, IndicatorConstraintID, Instance, Kind, OneHotConstraintID,
    Sense, Sos1ConstraintID, VariableIDSet,
};
use instance_facts::{ConstraintFacts, FunctionClassification, InstanceFacts};
use std::collections::{BTreeMap, BTreeSet};

/// Polynomial requirement in an [`InstanceClassClause`].
///
/// `AtMost(n)` includes every polynomial degree up to and including `n`.
/// `AnyDegree` includes every polynomial degree. Neither variant includes
/// non-polynomial [`crate::Function`] values.
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub enum PolynomialRequirement {
    AtMost(Degree),
    AnyDegree,
}

impl PolynomialRequirement {
    /// Require a polynomial degree up to and including `degree`.
    pub fn at_most(degree: u32) -> Self {
        Self::AtMost(degree.into())
    }

    /// Require any polynomial degree representable by OMMX.
    pub fn any_degree() -> Self {
        Self::AnyDegree
    }

    /// Return whether `actual` satisfies this polynomial requirement.
    pub fn accepts_degree(self, actual: Degree) -> bool {
        match self {
            Self::AtMost(maximum) => actual <= maximum,
            Self::AnyDegree => true,
        }
    }

    /// Return the inclusive maximum degree, or `None` for any degree.
    pub fn maximum_degree(self) -> Option<Degree> {
        match self {
            Self::AtMost(maximum) => Some(maximum),
            Self::AnyDegree => None,
        }
    }
}

impl std::fmt::Display for PolynomialRequirement {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::AtMost(maximum) => write!(f, "degree <= {maximum}"),
            Self::AnyDegree => f.write_str("any polynomial degree"),
        }
    }
}

/// Polynomial requirements for the allowed relations of one constraint family.
///
/// An empty value excludes every constraint in that family. Absence of one
/// [`Equality`] excludes that relation.
#[derive(Debug, Clone, PartialEq, Eq, Default)]
struct RelationPolynomialRequirements(BTreeMap<Equality, PolynomialRequirement>);

impl RelationPolynomialRequirements {
    fn new() -> Self {
        Self::default()
    }

    fn with(mut self, relation: Equality, requirement: PolynomialRequirement) -> Self {
        self.0.insert(relation, requirement);
        self
    }

    fn requirement_for(&self, relation: Equality) -> Option<PolynomialRequirement> {
        self.0.get(&relation).copied()
    }

    fn relations(&self) -> BTreeSet<Equality> {
        self.0.keys().copied().collect()
    }

    fn iter(&self) -> impl Iterator<Item = (Equality, PolynomialRequirement)> + '_ {
        self.0
            .iter()
            .map(|(relation, requirement)| (*relation, *requirement))
    }

    fn is_empty(&self) -> bool {
        self.0.is_empty()
    }
}

impl FromIterator<(Equality, PolynomialRequirement)> for RelationPolynomialRequirements {
    fn from_iter<T: IntoIterator<Item = (Equality, PolynomialRequirement)>>(iter: T) -> Self {
        Self(iter.into_iter().collect())
    }
}

/// One conjunctive clause in an [`InstanceClass`].
///
/// Every condition in a clause must hold for an instance to belong to that
/// clause. The containing [`InstanceClass`] is the union of its clauses, so a
/// continuous-QP clause and a MILP clause do not imply MIQP membership.
///
/// `allowed_variable_kinds` is a set rather than one field per known [`Kind`],
/// allowing future kinds such as Spin to participate without changing the
/// clause shape.
#[derive(Debug, Clone)]
pub struct InstanceClassClause {
    label: String,
    allowed_variable_kinds: BTreeSet<Kind>,
    objective_polynomial_requirement: PolynomialRequirement,
    regular_constraints: RelationPolynomialRequirements,
    indicator_constraints: RelationPolynomialRequirements,
    allows_one_hot: bool,
    allows_sos1: bool,
    allowed_senses: BTreeSet<Sense>,
}

impl InstanceClassClause {
    /// Construct a clause with no allowed constraint families.
    ///
    /// An empty `allowed_senses` set makes the clause contain no instances.
    /// `label` is diagnostic metadata and need not be unique.
    pub fn new(
        label: impl Into<String>,
        allowed_variable_kinds: BTreeSet<Kind>,
        objective_polynomial_requirement: PolynomialRequirement,
        allowed_senses: BTreeSet<Sense>,
    ) -> Self {
        Self {
            label: label.into(),
            allowed_variable_kinds,
            objective_polynomial_requirement,
            regular_constraints: RelationPolynomialRequirements::new(),
            indicator_constraints: RelationPolynomialRequirements::new(),
            allows_one_hot: false,
            allows_sos1: false,
            allowed_senses,
        }
    }

    /// Include one regular-constraint relation whose function is polynomial
    /// and satisfies `requirement`.
    pub fn with_regular_constraint(
        mut self,
        relation: Equality,
        requirement: PolynomialRequirement,
    ) -> Self {
        self.regular_constraints = self.regular_constraints.with(relation, requirement);
        self
    }

    /// Include one Indicator body relation whose function is polynomial and
    /// satisfies `body_requirement`.
    pub fn with_indicator_constraint(
        mut self,
        relation: Equality,
        body_requirement: PolynomialRequirement,
    ) -> Self {
        self.indicator_constraints = self.indicator_constraints.with(relation, body_requirement);
        self
    }

    /// Include instances with active OneHot constraints.
    pub fn with_one_hot(mut self) -> Self {
        self.allows_one_hot = true;
        self
    }

    /// Include instances with active SOS1 constraints.
    pub fn with_sos1(mut self) -> Self {
        self.allows_sos1 = true;
        self
    }

    /// Human-readable diagnostic label. Labels do not affect membership and
    /// need not be unique.
    pub fn label(&self) -> &str {
        &self.label
    }

    /// Return the variable kinds admitted by this clause.
    pub fn allowed_variable_kinds(&self) -> &BTreeSet<Kind> {
        &self.allowed_variable_kinds
    }

    /// Return the objective's polynomial requirement.
    pub fn objective_polynomial_requirement(&self) -> PolynomialRequirement {
        self.objective_polynomial_requirement
    }

    /// Iterate over admitted regular-constraint relations and polynomial requirements.
    pub fn regular_constraint_polynomial_requirements(
        &self,
    ) -> impl Iterator<Item = (Equality, PolynomialRequirement)> + '_ {
        self.regular_constraints.iter()
    }

    /// Iterate over admitted Indicator-body relations and polynomial requirements.
    pub fn indicator_body_polynomial_requirements(
        &self,
    ) -> impl Iterator<Item = (Equality, PolynomialRequirement)> + '_ {
        self.indicator_constraints.iter()
    }

    /// Return whether active OneHot constraints are admitted.
    pub fn allows_one_hot(&self) -> bool {
        self.allows_one_hot
    }

    /// Return whether active SOS1 constraints are admitted.
    pub fn allows_sos1(&self) -> bool {
        self.allows_sos1
    }

    /// Return the optimization senses admitted by this clause.
    pub fn allowed_senses(&self) -> &BTreeSet<Sense> {
        &self.allowed_senses
    }

    fn check(&self, clause_index: usize, facts: &InstanceFacts) -> InstanceClassClauseReport {
        let mut mismatches = Vec::new();

        for (kind, variable_ids) in facts.used_variables_by_kind() {
            if !self.allowed_variable_kinds.contains(kind) {
                mismatches.push(InstanceClassMismatch::VariableKindNotAllowed {
                    kind: *kind,
                    variable_ids: variable_ids.clone(),
                    allowed_kinds: self.allowed_variable_kinds.clone(),
                });
            }
        }

        match facts.objective_classification() {
            FunctionClassification::Polynomial(actual_degree)
                if !self
                    .objective_polynomial_requirement
                    .accepts_degree(actual_degree) =>
            {
                mismatches.push(InstanceClassMismatch::ObjectiveDegreeExceedsBound {
                    actual_degree,
                    bound: self.objective_polynomial_requirement,
                });
            }
            FunctionClassification::NonPolynomial => {
                mismatches.push(InstanceClassMismatch::ObjectiveFunctionNotPolynomial);
            }
            FunctionClassification::Polynomial(_) => {}
        }

        check_regular_constraints(
            &mut mismatches,
            facts.regular_constraints(),
            &self.regular_constraints,
        );
        check_indicator_constraints(
            &mut mismatches,
            facts.indicator_constraints(),
            &self.indicator_constraints,
        );

        if !self.allows_one_hot && !facts.one_hot_constraint_ids().is_empty() {
            mismatches.push(InstanceClassMismatch::OneHotConstraintsNotAllowed {
                constraint_ids: facts.one_hot_constraint_ids().clone(),
            });
        }
        if !self.allows_sos1 && !facts.sos1_constraint_ids().is_empty() {
            mismatches.push(InstanceClassMismatch::Sos1ConstraintsNotAllowed {
                constraint_ids: facts.sos1_constraint_ids().clone(),
            });
        }
        if !self.allowed_senses.contains(&facts.sense()) {
            mismatches.push(InstanceClassMismatch::SenseNotAllowed {
                sense: facts.sense(),
                allowed_senses: self.allowed_senses.clone(),
            });
        }

        InstanceClassClauseReport {
            clause_index,
            clause_label: self.label.clone(),
            mismatches,
        }
    }
}

fn group_constraint_facts<ID: Copy + Ord>(
    facts: &BTreeMap<ID, ConstraintFacts>,
) -> BTreeMap<Equality, BTreeMap<ID, FunctionClassification>> {
    let mut grouped = BTreeMap::<Equality, BTreeMap<ID, FunctionClassification>>::new();
    for (id, fact) in facts {
        grouped
            .entry(fact.relation())
            .or_default()
            .insert(*id, fact.classification());
    }
    grouped
}

fn check_regular_constraints(
    mismatches: &mut Vec<InstanceClassMismatch>,
    facts: &BTreeMap<ConstraintID, ConstraintFacts>,
    allowed: &RelationPolynomialRequirements,
) {
    for (relation, constraints) in group_constraint_facts(facts) {
        let Some(requirement) = allowed.requirement_for(relation) else {
            mismatches.push(InstanceClassMismatch::RegularConstraintRelationNotAllowed {
                relation,
                constraint_ids: constraints.keys().copied().collect(),
                allowed_relations: allowed.relations(),
            });
            continue;
        };
        let non_polynomial_ids = constraints
            .iter()
            .filter_map(|(id, classification)| {
                matches!(classification, FunctionClassification::NonPolynomial).then_some(*id)
            })
            .collect::<BTreeSet<_>>();
        if !non_polynomial_ids.is_empty() {
            mismatches.push(
                InstanceClassMismatch::RegularConstraintFunctionNotPolynomial {
                    relation,
                    constraint_ids: non_polynomial_ids,
                },
            );
        }
        let actual_degrees = constraints
            .into_iter()
            .filter_map(|(id, classification)| match classification {
                FunctionClassification::Polynomial(degree) => Some((id, degree)),
                FunctionClassification::NonPolynomial => None,
            })
            .filter(|(_, degree)| !requirement.accepts_degree(*degree))
            .collect::<BTreeMap<_, _>>();
        if !actual_degrees.is_empty() {
            mismatches.push(InstanceClassMismatch::RegularConstraintDegreeExceedsBound {
                relation,
                actual_degrees,
                bound: requirement,
            });
        }
    }
}

fn check_indicator_constraints(
    mismatches: &mut Vec<InstanceClassMismatch>,
    facts: &BTreeMap<IndicatorConstraintID, ConstraintFacts>,
    allowed: &RelationPolynomialRequirements,
) {
    if facts.is_empty() {
        return;
    }
    if allowed.is_empty() {
        mismatches.push(InstanceClassMismatch::IndicatorConstraintsNotAllowed {
            constraint_ids: facts.keys().copied().collect(),
        });
        return;
    }
    for (relation, constraints) in group_constraint_facts(facts) {
        let Some(requirement) = allowed.requirement_for(relation) else {
            mismatches.push(
                InstanceClassMismatch::IndicatorConstraintRelationNotAllowed {
                    relation,
                    constraint_ids: constraints.keys().copied().collect(),
                    allowed_relations: allowed.relations(),
                },
            );
            continue;
        };
        let non_polynomial_ids = constraints
            .iter()
            .filter_map(|(id, classification)| {
                matches!(classification, FunctionClassification::NonPolynomial).then_some(*id)
            })
            .collect::<BTreeSet<_>>();
        if !non_polynomial_ids.is_empty() {
            mismatches.push(InstanceClassMismatch::IndicatorBodyFunctionNotPolynomial {
                relation,
                constraint_ids: non_polynomial_ids,
            });
        }
        let actual_degrees = constraints
            .into_iter()
            .filter_map(|(id, classification)| match classification {
                FunctionClassification::Polynomial(degree) => Some((id, degree)),
                FunctionClassification::NonPolynomial => None,
            })
            .filter(|(_, degree)| !requirement.accepts_degree(*degree))
            .collect::<BTreeMap<_, _>>();
        if !actual_degrees.is_empty() {
            mismatches.push(InstanceClassMismatch::IndicatorBodyDegreeExceedsBound {
                relation,
                actual_degrees,
                bound: requirement,
            });
        }
    }
}

/// A set of [`Instance`] values represented as a finite union of
/// [`InstanceClassClause`] values.
///
/// The empty clause list represents the empty class. Clause order, duplicate
/// clauses, and clause labels are representation details rather than
/// extensional class identity, so this type deliberately does not implement
/// [`PartialEq`] or [`Eq`].
#[derive(Debug, Clone, Default)]
pub struct InstanceClass {
    clauses: Vec<InstanceClassClause>,
}

impl InstanceClass {
    /// Construct the finite union of `clauses`.
    pub fn new(clauses: Vec<InstanceClassClause>) -> Self {
        Self { clauses }
    }

    /// Return the class of QUBO solver inputs.
    ///
    /// # Postconditions
    ///
    /// The returned class admits only unconstrained minimization models over
    /// Binary variables whose objective degree is at most two.
    ///
    /// ```
    /// use ommx::{
    ///     linear, monomial, Constraint, ConstraintID, DecisionVariable, Function,
    ///     Instance, InstanceClass, Sense, VariableID,
    /// };
    /// use std::collections::BTreeMap;
    ///
    /// let variable = VariableID::from(1);
    /// let binary = BTreeMap::from([(variable, DecisionVariable::binary())]);
    /// let build = |sense, objective, constraints| {
    ///     Instance::builder()
    ///         .sense(sense)
    ///         .objective(objective)
    ///         .decision_variables(binary.clone())
    ///         .constraints(constraints)
    ///         .build()
    ///         .unwrap()
    /// };
    /// let linear = build(Sense::Minimize, Function::from(linear!(1)), BTreeMap::new());
    /// let quadratic = build(
    ///     Sense::Minimize,
    ///     Function::from(monomial!(1, 1)),
    ///     BTreeMap::new(),
    /// );
    /// let cubic = build(
    ///     Sense::Minimize,
    ///     Function::from(monomial!(1, 1, 1)),
    ///     BTreeMap::new(),
    /// );
    /// let maximizing = build(Sense::Maximize, Function::from(linear!(1)), BTreeMap::new());
    /// let constrained = build(
    ///     Sense::Minimize,
    ///     Function::from(linear!(1)),
    ///     BTreeMap::from([(
    ///         ConstraintID::from(1),
    ///         Constraint::equal_to_zero(Function::from(linear!(1))),
    ///     )]),
    /// );
    /// let non_binary = Instance::builder()
    ///     .sense(Sense::Minimize)
    ///     .objective(Function::from(linear!(1)))
    ///     .decision_variables(BTreeMap::from([(variable, DecisionVariable::continuous())]))
    ///     .constraints(BTreeMap::new())
    ///     .build()
    ///     .unwrap();
    ///
    /// let class = InstanceClass::qubo();
    /// assert!(class.contains(&linear));
    /// assert!(class.contains(&quadratic));
    /// assert!(!class.contains(&cubic));
    /// assert!(!class.contains(&maximizing));
    /// assert!(!class.contains(&constrained));
    /// assert!(!class.contains(&non_binary));
    /// ```
    pub fn qubo() -> Self {
        InstanceClassClause::new(
            "qubo",
            BTreeSet::from([Kind::Binary]),
            PolynomialRequirement::at_most(2),
            BTreeSet::from([Sense::Minimize]),
        )
        .into()
    }

    /// Return the class of Binary HUBO solver inputs.
    ///
    /// # Postconditions
    ///
    /// The returned class admits unconstrained minimization models over Binary
    /// variables with any polynomial objective degree.
    ///
    /// ```
    /// use ommx::{
    ///     linear, monomial, Constraint, ConstraintID, DecisionVariable, Function,
    ///     Instance, InstanceClass, Sense, VariableID,
    /// };
    /// use std::collections::BTreeMap;
    ///
    /// let variable = VariableID::from(1);
    /// let build = |sense, objective, decision_variable| {
    ///     Instance::builder()
    ///         .sense(sense)
    ///         .objective(objective)
    ///         .decision_variables(BTreeMap::from([(variable, decision_variable)]))
    ///         .constraints(BTreeMap::new())
    ///         .build()
    ///         .unwrap()
    /// };
    /// let linear = build(Sense::Minimize, Function::from(linear!(1)), DecisionVariable::binary());
    /// let cubic = build(
    ///     Sense::Minimize,
    ///     Function::from(monomial!(1, 1, 1)),
    ///     DecisionVariable::binary(),
    /// );
    /// let maximizing = build(Sense::Maximize, Function::from(linear!(1)), DecisionVariable::binary());
    /// let non_binary = build(
    ///     Sense::Minimize,
    ///     Function::from(linear!(1)),
    ///     DecisionVariable::continuous(),
    /// );
    /// let constrained = Instance::builder()
    ///     .sense(Sense::Minimize)
    ///     .objective(Function::from(linear!(1)))
    ///     .decision_variables(BTreeMap::from([(variable, DecisionVariable::binary())]))
    ///     .constraints(BTreeMap::from([(
    ///         ConstraintID::from(1),
    ///         Constraint::equal_to_zero(Function::from(linear!(1))),
    ///     )]))
    ///     .build()
    ///     .unwrap();
    ///
    /// let class = InstanceClass::hubo();
    /// assert!(class.contains(&linear));
    /// assert!(class.contains(&cubic));
    /// assert!(!class.contains(&maximizing));
    /// assert!(!class.contains(&non_binary));
    /// assert!(!class.contains(&constrained));
    /// ```
    pub fn hubo() -> Self {
        InstanceClassClause::new(
            "hubo",
            BTreeSet::from([Kind::Binary]),
            PolynomialRequirement::any_degree(),
            BTreeSet::from([Sense::Minimize]),
        )
        .into()
    }

    /// Return the clauses representing this class.
    pub fn clauses(&self) -> &[InstanceClassClause] {
        &self.clauses
    }

    /// Return the finite union of `self` and `other`.
    pub fn union(mut self, other: Self) -> Self {
        self.clauses.extend(other.clauses);
        self
    }

    /// Return whether `instance` belongs to this class.
    pub fn contains(&self, instance: &Instance) -> bool {
        self.check_membership(instance).is_member()
    }

    /// Evaluate membership without mutating or preparing `instance`.
    ///
    /// Facts are derived from the exact instance on every call. Callers that
    /// prepare an instance must check membership again on the prepared value.
    pub fn check_membership(&self, instance: &Instance) -> InstanceClassMembershipReport {
        let facts = InstanceFacts::from(instance);
        InstanceClassMembershipReport {
            clause_reports: self
                .clauses
                .iter()
                .enumerate()
                .map(|(index, clause)| clause.check(index, &facts))
                .collect(),
        }
    }
}

impl From<InstanceClassClause> for InstanceClass {
    fn from(clause: InstanceClassClause) -> Self {
        Self::new(vec![clause])
    }
}

impl FromIterator<InstanceClassClause> for InstanceClass {
    fn from_iter<T: IntoIterator<Item = InstanceClassClause>>(iter: T) -> Self {
        Self::new(iter.into_iter().collect())
    }
}

/// One reason an [`Instance`] does not belong to an
/// [`InstanceClassClause`].
#[non_exhaustive]
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum InstanceClassMismatch {
    VariableKindNotAllowed {
        kind: Kind,
        variable_ids: VariableIDSet,
        allowed_kinds: BTreeSet<Kind>,
    },
    ObjectiveDegreeExceedsBound {
        actual_degree: Degree,
        bound: PolynomialRequirement,
    },
    ObjectiveFunctionNotPolynomial,
    RegularConstraintRelationNotAllowed {
        relation: Equality,
        constraint_ids: BTreeSet<ConstraintID>,
        allowed_relations: BTreeSet<Equality>,
    },
    RegularConstraintDegreeExceedsBound {
        relation: Equality,
        actual_degrees: BTreeMap<ConstraintID, Degree>,
        bound: PolynomialRequirement,
    },
    RegularConstraintFunctionNotPolynomial {
        relation: Equality,
        constraint_ids: BTreeSet<ConstraintID>,
    },
    IndicatorConstraintsNotAllowed {
        constraint_ids: BTreeSet<IndicatorConstraintID>,
    },
    IndicatorConstraintRelationNotAllowed {
        relation: Equality,
        constraint_ids: BTreeSet<IndicatorConstraintID>,
        allowed_relations: BTreeSet<Equality>,
    },
    IndicatorBodyDegreeExceedsBound {
        relation: Equality,
        actual_degrees: BTreeMap<IndicatorConstraintID, Degree>,
        bound: PolynomialRequirement,
    },
    IndicatorBodyFunctionNotPolynomial {
        relation: Equality,
        constraint_ids: BTreeSet<IndicatorConstraintID>,
    },
    OneHotConstraintsNotAllowed {
        constraint_ids: BTreeSet<OneHotConstraintID>,
    },
    Sos1ConstraintsNotAllowed {
        constraint_ids: BTreeSet<Sos1ConstraintID>,
    },
    SenseNotAllowed {
        sense: Sense,
        allowed_senses: BTreeSet<Sense>,
    },
}

impl std::fmt::Display for InstanceClassMismatch {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::VariableKindNotAllowed {
                kind,
                variable_ids,
                allowed_kinds,
            } => write!(
                f,
                "variable kind {kind:?} for IDs {variable_ids:?} is not allowed; allowed kinds are {allowed_kinds:?}"
            ),
            Self::ObjectiveDegreeExceedsBound {
                actual_degree,
                bound,
            } => write!(f, "objective degree {actual_degree} exceeds {bound}"),
            Self::ObjectiveFunctionNotPolynomial => {
                f.write_str("objective function is not polynomial")
            }
            Self::RegularConstraintRelationNotAllowed {
                relation,
                constraint_ids,
                allowed_relations,
            } => write!(
                f,
                "regular-constraint relation {relation:?} for IDs {constraint_ids:?} is not allowed; allowed relations are {allowed_relations:?}"
            ),
            Self::RegularConstraintDegreeExceedsBound {
                relation,
                actual_degrees,
                bound,
            } => write!(
                f,
                "regular {relation:?} constraint degrees {actual_degrees:?} exceed {bound}"
            ),
            Self::RegularConstraintFunctionNotPolynomial {
                relation,
                constraint_ids,
            } => write!(
                f,
                "regular {relation:?} constraint functions for IDs {constraint_ids:?} are not polynomial"
            ),
            Self::IndicatorConstraintsNotAllowed { constraint_ids } => {
                write!(f, "indicator constraints {constraint_ids:?} are not allowed")
            }
            Self::IndicatorConstraintRelationNotAllowed {
                relation,
                constraint_ids,
                allowed_relations,
            } => write!(
                f,
                "indicator relation {relation:?} for IDs {constraint_ids:?} is not allowed; allowed relations are {allowed_relations:?}"
            ),
            Self::IndicatorBodyDegreeExceedsBound {
                relation,
                actual_degrees,
                bound,
            } => write!(
                f,
                "indicator {relation:?} body degrees {actual_degrees:?} exceed {bound}"
            ),
            Self::IndicatorBodyFunctionNotPolynomial {
                relation,
                constraint_ids,
            } => write!(
                f,
                "indicator {relation:?} body functions for IDs {constraint_ids:?} are not polynomial"
            ),
            Self::OneHotConstraintsNotAllowed { constraint_ids } => {
                write!(f, "one-hot constraints {constraint_ids:?} are not allowed")
            }
            Self::Sos1ConstraintsNotAllowed { constraint_ids } => {
                write!(f, "SOS1 constraints {constraint_ids:?} are not allowed")
            }
            Self::SenseNotAllowed {
                sense,
                allowed_senses,
            } => write!(
                f,
                "optimization sense {sense:?} is not allowed; allowed senses are {allowed_senses:?}"
            ),
        }
    }
}

/// Membership result for one conjunctive clause.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct InstanceClassClauseReport {
    clause_index: usize,
    clause_label: String,
    mismatches: Vec<InstanceClassMismatch>,
}

impl InstanceClassClauseReport {
    /// Return the clause's position in its containing class.
    pub fn clause_index(&self) -> usize {
        self.clause_index
    }

    /// Return the clause's diagnostic label.
    pub fn clause_label(&self) -> &str {
        &self.clause_label
    }

    /// Return every reason the instance is outside this clause.
    pub fn mismatches(&self) -> &[InstanceClassMismatch] {
        &self.mismatches
    }

    /// Return whether the instance belongs to this clause.
    pub fn is_member(&self) -> bool {
        self.mismatches.is_empty()
    }
}

/// Side-effect-free [`InstanceClass`] membership report.
///
/// An instance is a member when at least one complete clause contains it.
/// Adapters use this membership report directly when checking applicability;
/// they do not add another applicability condition. Other consumers may turn
/// the same report into operation-specific diagnostics without implementing a
/// second structural validator.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct InstanceClassMembershipReport {
    clause_reports: Vec<InstanceClassClauseReport>,
}

impl InstanceClassMembershipReport {
    /// Return one membership report per class clause, in clause order.
    pub fn clause_reports(&self) -> &[InstanceClassClauseReport] {
        &self.clause_reports
    }

    /// Return whether at least one clause contains the instance.
    pub fn is_member(&self) -> bool {
        self.clause_reports
            .iter()
            .any(InstanceClassClauseReport::is_member)
    }

    /// Iterate over the indices and labels of clauses containing the instance.
    pub fn matching_clauses(&self) -> impl Iterator<Item = (usize, &str)> {
        self.clause_reports
            .iter()
            .filter(|clause| clause.is_member())
            .map(|clause| (clause.clause_index(), clause.clause_label()))
    }
}

impl std::fmt::Display for InstanceClassMembershipReport {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        if self.is_member() {
            let clauses = self
                .matching_clauses()
                .map(|(index, label)| format!("{index}: `{label}`"))
                .collect::<Vec<_>>()
                .join(", ");
            return write!(f, "Instance belongs via clause(s) {clauses}");
        }
        writeln!(f, "Instance does not belong to any clause:")?;
        for clause in &self.clause_reports {
            writeln!(
                f,
                "- clause {} (`{}`):",
                clause.clause_index, clause.clause_label
            )?;
            for mismatch in &clause.mismatches {
                writeln!(f, "  - {mismatch}")?;
            }
        }
        Ok(())
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::{
        linear, quadratic, Constraint, DecisionVariable, Function, FunctionParameters,
        IndicatorConstraint, InstanceParameters, OneHotConstraint, OneHotConstraintID,
        PolynomialParameters, Sos1Constraint, Sos1ConstraintID, VariableID,
    };
    use proptest::prelude::*;

    fn clause(
        label: &str,
        allowed_variable_kinds: &[Kind],
        objective_polynomial_requirement: PolynomialRequirement,
    ) -> InstanceClassClause {
        InstanceClassClause::new(
            label,
            allowed_variable_kinds.iter().copied().collect(),
            objective_polynomial_requirement,
            BTreeSet::from([Sense::Minimize, Sense::Maximize]),
        )
    }

    fn covering_clause(facts: &InstanceFacts) -> Option<InstanceClassClause> {
        let FunctionClassification::Polynomial(objective_degree) = facts.objective_classification()
        else {
            return None;
        };
        let mut clause = InstanceClassClause::new(
            "covering",
            facts.used_variables_by_kind().keys().copied().collect(),
            PolynomialRequirement::AtMost(objective_degree),
            BTreeSet::from([facts.sense()]),
        );

        let mut regular = BTreeMap::<Equality, Degree>::new();
        for fact in facts.regular_constraints().values() {
            let FunctionClassification::Polynomial(fact_degree) = fact.classification() else {
                return None;
            };
            regular
                .entry(fact.relation())
                .and_modify(|degree| *degree = (*degree).max(fact_degree))
                .or_insert(fact_degree);
        }
        for (relation, degree) in regular {
            clause =
                clause.with_regular_constraint(relation, PolynomialRequirement::AtMost(degree));
        }

        let mut indicator = BTreeMap::<Equality, Degree>::new();
        for fact in facts.indicator_constraints().values() {
            let FunctionClassification::Polynomial(fact_degree) = fact.classification() else {
                return None;
            };
            indicator
                .entry(fact.relation())
                .and_modify(|degree| *degree = (*degree).max(fact_degree))
                .or_insert(fact_degree);
        }
        for (relation, degree) in indicator {
            clause =
                clause.with_indicator_constraint(relation, PolynomialRequirement::AtMost(degree));
        }
        if !facts.one_hot_constraint_ids().is_empty() {
            clause = clause.with_one_hot();
        }
        if !facts.sos1_constraint_ids().is_empty() {
            clause = clause.with_sos1();
        }
        Some(clause)
    }

    fn polynomial_full_v3_parameters() -> InstanceParameters {
        let function = FunctionParameters::polynomial_only(PolynomialParameters::default());
        InstanceParameters {
            objective: function,
            constraint: function,
            named_function: function,
            ..InstanceParameters::full_v3()
        }
    }

    #[test]
    fn polynomial_requirement_is_cumulative_and_inclusive() {
        let linear = PolynomialRequirement::at_most(1);
        assert!(linear.accepts_degree(0.into()));
        assert!(linear.accepts_degree(1.into()));
        assert!(!linear.accepts_degree(2.into()));
        assert_eq!(linear.maximum_degree(), Some(1.into()));
        assert!(PolynomialRequirement::any_degree().accepts_degree(10_000.into()));
        assert_eq!(PolynomialRequirement::any_degree().maximum_degree(), None);
    }

    #[test]
    fn union_does_not_combine_conditions_across_clauses() {
        let x = VariableID::from(1);
        let instance = crate::Instance::new(
            Sense::Minimize,
            Function::Quadratic(quadratic!(x, x).into()),
            BTreeMap::from([(x, DecisionVariable::binary())]),
            BTreeMap::new(),
        )
        .unwrap();

        let milp = clause(
            "milp",
            &[Kind::Binary, Kind::Integer, Kind::Continuous],
            PolynomialRequirement::at_most(1),
        )
        .with_regular_constraint(Equality::EqualToZero, PolynomialRequirement::at_most(1))
        .with_regular_constraint(
            Equality::LessThanOrEqualToZero,
            PolynomialRequirement::at_most(1),
        );
        let continuous_qp = clause(
            "continuous-qp",
            &[Kind::Continuous],
            PolynomialRequirement::at_most(2),
        )
        .with_regular_constraint(Equality::EqualToZero, PolynomialRequirement::at_most(1))
        .with_regular_constraint(
            Equality::LessThanOrEqualToZero,
            PolynomialRequirement::at_most(1),
        );
        let instance_class = InstanceClass::new(vec![milp, continuous_qp]);

        let report = instance_class.check_membership(&instance);
        assert!(!report.is_member());
        assert!(matches!(
            report.clause_reports()[0].mismatches(),
            [InstanceClassMismatch::ObjectiveDegreeExceedsBound { .. }]
        ));
        assert!(matches!(
            report.clause_reports()[1].mismatches(),
            [InstanceClassMismatch::VariableKindNotAllowed { .. }]
        ));
        assert!(!instance_class.contains(&instance));
    }

    #[test]
    fn structured_mismatches_preserve_relations_degrees_and_ids() {
        let x = VariableID::from(1);
        let y = VariableID::from(2);
        let regular_eq = ConstraintID::from(10);
        let regular_le = ConstraintID::from(11);
        let indicator_eq = IndicatorConstraintID::from(20);
        let indicator_le = IndicatorConstraintID::from(21);
        let one_hot = OneHotConstraintID::from(30);
        let sos1 = Sos1ConstraintID::from(40);
        let quadratic_y = || Function::Quadratic(quadratic!(y, y).into());
        let instance = crate::Instance::builder()
            .sense(Sense::Maximize)
            .objective(Function::Quadratic(quadratic!(x, y).into()))
            .decision_variables(BTreeMap::from([
                (x, DecisionVariable::binary()),
                (y, DecisionVariable::continuous()),
            ]))
            .constraints(BTreeMap::from([
                (regular_eq, Constraint::equal_to_zero(quadratic_y())),
                (
                    regular_le,
                    Constraint::less_than_or_equal_to_zero(Function::from(linear!(y))),
                ),
            ]))
            .indicator_constraints(BTreeMap::from([
                (
                    indicator_eq,
                    IndicatorConstraint::new(x, Equality::EqualToZero, quadratic_y()),
                ),
                (
                    indicator_le,
                    IndicatorConstraint::new(
                        x,
                        Equality::LessThanOrEqualToZero,
                        Function::from(linear!(y)),
                    ),
                ),
            ]))
            .one_hot_constraints(BTreeMap::from([(
                one_hot,
                OneHotConstraint::new(BTreeSet::from([x])).unwrap(),
            )]))
            .sos1_constraints(BTreeMap::from([(
                sos1,
                Sos1Constraint::new(BTreeSet::from([y])).unwrap(),
            )]))
            .build()
            .unwrap();

        // Compare serialized bytes to make the side-effect-free contract
        // observable across the complete instance.
        let before = instance.to_v2_bytes();
        let limited = InstanceClassClause::new(
            "limited",
            BTreeSet::from([Kind::Binary]),
            PolynomialRequirement::at_most(1),
            BTreeSet::from([Sense::Minimize]),
        )
        .with_regular_constraint(Equality::EqualToZero, PolynomialRequirement::at_most(1))
        .with_indicator_constraint(Equality::EqualToZero, PolynomialRequirement::at_most(1));
        let report = InstanceClass::new(vec![limited]).check_membership(&instance);

        assert!(!report.is_member());
        assert_eq!(
            report.clause_reports()[0].mismatches(),
            &[
                InstanceClassMismatch::VariableKindNotAllowed {
                    kind: Kind::Continuous,
                    variable_ids: BTreeSet::from([y]),
                    allowed_kinds: BTreeSet::from([Kind::Binary]),
                },
                InstanceClassMismatch::ObjectiveDegreeExceedsBound {
                    actual_degree: 2.into(),
                    bound: PolynomialRequirement::at_most(1),
                },
                InstanceClassMismatch::RegularConstraintDegreeExceedsBound {
                    relation: Equality::EqualToZero,
                    actual_degrees: BTreeMap::from([(regular_eq, 2.into())]),
                    bound: PolynomialRequirement::at_most(1),
                },
                InstanceClassMismatch::RegularConstraintRelationNotAllowed {
                    relation: Equality::LessThanOrEqualToZero,
                    constraint_ids: BTreeSet::from([regular_le]),
                    allowed_relations: BTreeSet::from([Equality::EqualToZero]),
                },
                InstanceClassMismatch::IndicatorBodyDegreeExceedsBound {
                    relation: Equality::EqualToZero,
                    actual_degrees: BTreeMap::from([(indicator_eq, 2.into())]),
                    bound: PolynomialRequirement::at_most(1),
                },
                InstanceClassMismatch::IndicatorConstraintRelationNotAllowed {
                    relation: Equality::LessThanOrEqualToZero,
                    constraint_ids: BTreeSet::from([indicator_le]),
                    allowed_relations: BTreeSet::from([Equality::EqualToZero]),
                },
                InstanceClassMismatch::OneHotConstraintsNotAllowed {
                    constraint_ids: BTreeSet::from([one_hot]),
                },
                InstanceClassMismatch::Sos1ConstraintsNotAllowed {
                    constraint_ids: BTreeSet::from([sos1]),
                },
                InstanceClassMismatch::SenseNotAllowed {
                    sense: Sense::Maximize,
                    allowed_senses: BTreeSet::from([Sense::Minimize]),
                },
            ]
        );
        assert_eq!(instance.to_v2_bytes(), before);
    }

    #[test]
    fn every_polynomial_requirement_rejects_non_polynomial_functions() {
        let x = VariableID::from(1);
        let regular_id = ConstraintID::from(10);
        let indicator_id = IndicatorConstraintID::from(20);
        let absolute_x = || Function::from(linear!(x)).abs();
        let instance = crate::Instance::builder()
            .sense(Sense::Minimize)
            .objective(absolute_x())
            .decision_variables(BTreeMap::from([(x, DecisionVariable::binary())]))
            .constraints(BTreeMap::from([(
                regular_id,
                Constraint::equal_to_zero(absolute_x()),
            )]))
            .indicator_constraints(BTreeMap::from([(
                indicator_id,
                IndicatorConstraint::new(x, Equality::EqualToZero, absolute_x()),
            )]))
            .build()
            .unwrap();

        for requirement in [
            PolynomialRequirement::at_most(2),
            PolynomialRequirement::any_degree(),
        ] {
            let polynomial_only = InstanceClass::from(
                clause("polynomial-only", &[Kind::Binary], requirement)
                    .with_regular_constraint(Equality::EqualToZero, requirement)
                    .with_indicator_constraint(Equality::EqualToZero, requirement),
            );

            let report = polynomial_only.check_membership(&instance);
            assert_eq!(
                report.clause_reports()[0].mismatches(),
                &[
                    InstanceClassMismatch::ObjectiveFunctionNotPolynomial,
                    InstanceClassMismatch::RegularConstraintFunctionNotPolynomial {
                        relation: Equality::EqualToZero,
                        constraint_ids: BTreeSet::from([regular_id]),
                    },
                    InstanceClassMismatch::IndicatorBodyFunctionNotPolynomial {
                        relation: Equality::EqualToZero,
                        constraint_ids: BTreeSet::from([indicator_id]),
                    },
                ]
            );
            assert!(!report.is_member());
            assert!(!polynomial_only.contains(&instance));
        }
    }

    #[test]
    fn omitted_constraint_relations_include_unconstrained_instances() {
        let x = VariableID::from(1);
        let instance = crate::Instance::new(
            Sense::Maximize,
            Function::Quadratic(quadratic!(x, x).into()),
            BTreeMap::from([(x, DecisionVariable::binary())]),
            BTreeMap::new(),
        )
        .unwrap();
        let qubo = clause("qubo", &[Kind::Binary], PolynomialRequirement::at_most(2));
        let report = InstanceClass::from(qubo).check_membership(&instance);
        assert!(report.is_member());
        assert_eq!(report.matching_clauses().collect::<Vec<_>>(), [(0, "qubo")]);
    }

    #[test]
    fn membership_is_recomputed_after_explicit_lowering() {
        let x = VariableID::from(1);
        let y = VariableID::from(2);
        let one_hot_id = OneHotConstraintID::from(7);
        let mut instance = crate::Instance::builder()
            .sense(Sense::Minimize)
            .objective(Function::from((linear!(x) + linear!(y)).unwrap()))
            .decision_variables(BTreeMap::from([
                (x, DecisionVariable::binary()),
                (y, DecisionVariable::binary()),
            ]))
            .constraints(BTreeMap::new())
            .one_hot_constraints(BTreeMap::from([(
                one_hot_id,
                OneHotConstraint::new(BTreeSet::from([x, y])).unwrap(),
            )]))
            .build()
            .unwrap();
        let linear_binary = InstanceClass::from(
            clause(
                "linear-binary",
                &[Kind::Binary],
                PolynomialRequirement::at_most(1),
            )
            .with_regular_constraint(Equality::EqualToZero, PolynomialRequirement::at_most(1)),
        );

        assert!(!linear_binary.contains(&instance));
        instance.convert_one_hot_to_constraint(one_hot_id).unwrap();
        assert!(linear_binary.contains(&instance));
    }

    #[test]
    fn empty_class_and_empty_clause_represent_empty_sets() {
        let instance = crate::Instance::new(
            Sense::Minimize,
            Function::zero(),
            BTreeMap::new(),
            BTreeMap::new(),
        )
        .unwrap();
        assert!(!InstanceClass::default().contains(&instance));

        let empty_clause = InstanceClassClause::new(
            "empty",
            BTreeSet::new(),
            PolynomialRequirement::any_degree(),
            BTreeSet::new(),
        );
        assert!(!InstanceClass::from(empty_clause).contains(&instance));
    }

    #[test]
    fn union_is_disjunction_and_duplicate_labels_are_diagnostic_only() {
        let x = VariableID::from(1);
        let binary = crate::Instance::new(
            Sense::Minimize,
            Function::from(linear!(x)),
            BTreeMap::from([(x, DecisionVariable::binary())]),
            BTreeMap::new(),
        )
        .unwrap();
        let continuous = crate::Instance::new(
            Sense::Minimize,
            Function::from(linear!(x)),
            BTreeMap::from([(x, DecisionVariable::continuous())]),
            BTreeMap::new(),
        )
        .unwrap();
        let binary_class = InstanceClass::from(clause(
            "linear",
            &[Kind::Binary],
            PolynomialRequirement::at_most(1),
        ));
        let continuous_class = InstanceClass::from(clause(
            "linear",
            &[Kind::Continuous],
            PolynomialRequirement::at_most(1),
        ));
        let union = binary_class.clone().union(continuous_class.clone());

        assert!(union.contains(&binary));
        assert!(union.contains(&continuous));
        assert!(InstanceClass::default()
            .union(binary_class)
            .contains(&binary));
        assert!(continuous_class
            .union(InstanceClass::default())
            .contains(&continuous));
        assert_eq!(
            union
                .check_membership(&binary)
                .matching_clauses()
                .collect::<Vec<_>>(),
            [(0, "linear")]
        );
        assert_eq!(
            union
                .check_membership(&continuous)
                .matching_clauses()
                .collect::<Vec<_>>(),
            [(1, "linear")]
        );
    }

    proptest! {
        #[test]
        fn union_membership_is_disjunction(
            instance in any_with::<crate::Instance>(InstanceParameters::full_v3())
        ) {
            let binary = InstanceClass::from(clause(
                "binary-linear",
                &[Kind::Binary],
                PolynomialRequirement::at_most(1),
            ));
            let continuous = InstanceClass::from(clause(
                "continuous-quadratic",
                &[Kind::Continuous],
                PolynomialRequirement::at_most(2),
            ));
            let expected = binary.contains(&instance) || continuous.contains(&instance);
            let union = binary.union(continuous);

            prop_assert_eq!(union.contains(&instance), expected);
        }

        #[test]
        fn covering_clause_contains_every_polynomial_instance(
            instance in any_with::<crate::Instance>(polynomial_full_v3_parameters())
        ) {
            let facts = InstanceFacts::from(&instance);
            let clause = covering_clause(&facts)
                .expect("polynomial-only parameters must produce a covering clause");
            let instance_class = InstanceClass::from(clause);
            let report = instance_class.check_membership(&instance);
            prop_assert!(report.is_member(), "{report}");
            prop_assert!(instance_class.contains(&instance));
        }
    }
}