//! Semantic SAT encoding decisions. Clauses and solver literals belong to the adaptor.

use crate::ast::Expression;

use serde::{Deserialize, Serialize};

use std::fmt::{Display, Formatter};

use uniplate::Uniplate;

// One listing defines each family's labels, parsing and heuristic iteration order.

macro_rules! encoding_labels {

    ($type:ident, $family:literal, $len:literal, [$($variant:ident => $label:literal),+ $(,)?]) => {

        impl $type {

            /// Algorithms in heuristic and command-line order.

            pub const ALL: [Self; $len] = [$(Self::$variant),+];

            /// Canonical command-line labels in the same order as `ALL`.

            pub const LABELS: [&'static str; $len] = [$($label),+];

        }

        impl Display for $type {

        }

        impl std::str::FromStr for $type {

            type Err = String;

                }

        }

    };

}

/// A Boolean operation whose truth is asserted or bound to a named output.

#[derive(Clone, Debug, PartialEq, Eq, Hash, Serialize, Deserialize, Uniplate)]

#[biplate(to=Expression)]

#[biplate(to=crate::ast::DeclarationPtr)]

pub enum SatEncodingDecision {

    /// Assert the semantic Boolean expression; the adaptor chooses clauses and witnesses.

    Assert(Expression),

    /// At most one input may be true; the selected library algorithm is recorded explicitly.

    AtMostOne {

        inputs: Vec<Expression>,

        encoding: Option<EncodingSelection<AmoEncoding>>,

    },

    /// Compare the number of true operands with a mathematical integer bound.

    Cardinality {

        inputs: Vec<Expression>,

        relation: CardinalityRelation,

        bound: i64,

        encoding: Option<EncodingSelection<CardinalityEncoding>>,

    },

    /// Define the truth of a Boolean count comparison using cardinality and AMO providers.

    CountRelation {

        output: Expression,

        inputs: Vec<Expression>,

        relation: IntegerRelation,

        bound: i64,

        encoding: Option<EncodingSelection<CardinalityEncoding>>,

        /// Selected when either implication includes an at-most-one threshold.

        amo_encoding: Option<EncodingSelection<AmoEncoding>>,

    },

    /// Compare a signed weighted Boolean sum with an integer bound.

    PseudoBoolean {

        terms: Vec<(i64, Expression)>,

        /// Relationships already guaranteed by the integer representation constraints.

        #[serde(default, skip_serializing_if = "Vec::is_empty")]

        groups: Vec<PbTermGroup>,

        relation: CardinalityRelation,

        bound: i64,

        encoding: Option<EncodingSelection<PbEncoding>>,

    },

    /// Define an integer relation over a signed weighted view of the numeric operands.

    IntegerRelation {

        output: Expression,

        terms: Vec<(i64, Expression)>,

        groups: Vec<PbTermGroup>,

        relation: IntegerRelation,

        bound: i64,

        encoding: Option<EncodingSelection<PbEncoding>>,

    },

    /// Minimise or maximise an actual-value integer view using the selected PB provider.

    Objective {

        minimise: bool,

        value: SatIntegerView,

        encoding: Option<EncodingSelection<PbEncoding>>,

    },

    /// Define scalar or whole-value distinctness, with an optional repeated exception value.

    AllDifferent {

        output: Expression,

        inputs: Vec<SatIntegerView>,

        /// Pair conditions for compound values, lowered through the existing equality rules.

        #[serde(default, skip_serializing_if = "Option::is_none")]

        comparisons: Option<Vec<Expression>>,

        /// This value may occur repeatedly.

        #[serde(default, skip_serializing_if = "Option::is_none")]

        except: Option<SatIntegerView>,

        encoding: Option<EncodingSelection<AllDifferentEncoding>>,

        amo_encoding: Option<EncodingSelection<AmoEncoding>>,

        pb_encoding: Option<EncodingSelection<PbEncoding>>,

    },

    /// Define membership in an integer/Boolean relation.

    Table {

        output: Expression,

        inputs: Vec<SatIntegerView>,

        rows: Vec<Vec<i64>>,

        /// Non-constant relation cells retain their numeric representation views.

        #[serde(default, skip_serializing_if = "Option::is_none")]

        row_views: Option<Vec<Vec<SatIntegerView>>>,

        negative: bool,

        encoding: Option<EncodingSelection<TableEncoding>>,

        pb_encoding: Option<EncodingSelection<PbEncoding>>,

    },

    /// Define a selected scalar value; out-of-domain indices leave it unconstrained.

    Element {

        index_view: SatIntegerView,

        value: SatIntegerView,

        entries: Vec<(i64, SatIntegerView)>,

        encoding: Option<EncodingSelection<ElementEncoding>>,

        pb_encoding: Option<EncodingSelection<PbEncoding>>,

    },

    /// Define an output as equivalent to a semantic Boolean expression.

    Boolean {

        output: Expression,

        expression: Expression,

    },

}

impl Display for SatEncodingDecision {

                "at-most-one({}) using {:?}",

            ),

            Self::Cardinality {

                inputs,

                relation,

                bound,

                encoding,

            ),

            Self::CountRelation {

                output,

                inputs,

                relation,

                bound,

                encoding,

                amo_encoding,

            ),

            Self::PseudoBoolean {

                terms,

                groups,

                relation,

                bound,

                encoding,

            } => {

                        .collect::<Vec<_>>()

            }

            Self::IntegerRelation {

                output,

                terms,

                groups,

                relation,

                bound,

                encoding,

                    .collect::<Vec<_>>()

            ),

            Self::AllDifferent {

                output,

                inputs,

                except,

                comparisons,

                encoding,

                amo_encoding,

                pb_encoding,

            } => {

                        "allDifferentComparisons({})",

                    )

                } else {

                        }

                    }

                };

                )

            }

            Self::Table {

                output,

                inputs,

                rows,

                row_views,

                negative,

                encoding,

                pb_encoding,

            ),

            Self::Element {

                index_view,

                value,

                entries,

                encoding,

                pb_encoding,

                    .collect::<Vec<_>>()

            ),

            Self::Objective {

                minimise,

                value,

                encoding,

            ),

            Self::Boolean { output, expression } => {

            }

        }

}

/// Numeric relation between a weighted integer view and its bound.

#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, Serialize, Deserialize, Uniplate)]

pub enum IntegerRelation {

    Equal,

    NotEqual,

    Less,

    LessEqual,

    Greater,

    GreaterEqual,

}

/// A contiguous group of weighted terms with an existing representation invariant.

#[derive(Clone, Debug, PartialEq, Eq, Hash, Serialize, Deserialize, Uniplate)]

pub struct PbTermGroup {

    /// First term index, inclusive.

    pub start: usize,

    /// Last term index, exclusive.

    pub end: usize,

    /// The relationship between these terms, independent of library literals.

    pub structure: PbTermStructure,

}

/// Representation structure available to a pseudo-Boolean encoder.

#[derive(Clone, Debug, PartialEq, Eq, Hash, Serialize, Deserialize, Uniplate)]

pub enum PbTermStructure {

    /// At most one Boolean input in the group is true.

    Choice,

    /// Each Boolean input is implied by the next input in the group.

    Chain,

    /// Binary terms bounded by the representation's inclusive domain.

    BoundedBinary { lower: i64, upper: i64 },

}

impl SatEncodingDecision {

    /// Semantic expressions held by this decision.

            Self::AtMostOne { inputs, .. } | Self::Cardinality { inputs, .. } => {

            }

                .map(|(_, expression)| expression)

                .collect(),

            Self::CountRelation { output, inputs, .. } => {

            }

                .collect(),

            Self::AllDifferent {

                output,

                inputs,

                except,

                comparisons,

                ..

                        .map(|(_, term)| term)

                .collect(),

            Self::Table {

                output,

                inputs,

                row_views,

                ..

                .chain(

                                .map(|(_, term)| term)

                )

                .collect(),

            Self::Element {

                index_view,

                value,

                entries,

                ..

                        .map(|(_, term)| term)

                .collect(),

        }

}

/// A numeric view whose representation constraints remain independently enforced.

#[derive(Clone, Debug, PartialEq, Eq, Hash, Serialize, Deserialize, Uniplate)]

#[biplate(to=Expression)]

#[biplate(to=crate::ast::DeclarationPtr)]

pub struct SatIntegerView {

    /// Constant contribution to the actual numeric value.

    pub constant: i64,

    /// Signed weights over Boolean representation operands.

    pub terms: Vec<(i64, Expression)>,

    /// Independently guaranteed representation structure.

    pub groups: Vec<PbTermGroup>,

    /// Actual values and their exactly-one indicators, when available.

    pub choices: Option<Vec<(i64, Expression)>>,

}

impl Display for SatIntegerView {

            "{}+weighted({}) with {:?}",

                .collect::<Vec<_>>()

                " choices({})",

                    .collect::<Vec<_>>()

}

/// Library compositions available for element.

#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, Serialize, Deserialize)]

pub enum ElementEncoding {

    /// Each valid index selector implies its scalar equality.

    Implication,

    /// One support disjunction, with an explicit out-of-domain alternative.

    Support,

}

encoding_labels!(ElementEncoding, "element encoding", 2, [

    Implication => "implication",

    Support => "support",

]);

/// Library compositions available for table.

#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, Serialize, Deserialize)]

pub enum TableEncoding {

    /// Disjunction of matching rows, sharing each numeric cell comparison.

    Tuple,

    /// Reduced layered decision diagram, sharing equal suffix relations.

    Mdd,

    /// Bidirectional value supports for constant binary relations.

    BinarySupport,

}

encoding_labels!(TableEncoding, "table encoding", 3, [

    Tuple => "tuple",

    Mdd => "mdd",

    BinarySupport => "binary-support",

]);

/// Library compositions available for allDifferent.

#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, Serialize, Deserialize)]

pub enum AllDifferentEncoding {

    /// Pairwise numeric disequalities, for every numeric representation.

    Pairwise,

    /// AMO over equal-value indicators; requires choice views for all operands.

    ValueAmo,

}

encoding_labels!(AllDifferentEncoding, "allDifferent encoding", 2, [

    Pairwise => "pairwise",

    ValueAmo => "value-amo",

]);

/// The origin of a resolved compilation choice.

#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, Serialize, Deserialize)]

pub enum SelectionProvenance {

    ExplicitConfiguration,

    Heuristic,

}

/// A resolved algorithm and the source of that choice, reusable across encoding classes.

#[derive(Clone, Debug, PartialEq, Eq, Hash, Serialize, Deserialize)]

pub struct EncodingSelection<T> {

    pub algorithm: T,

    pub provenance: SelectionProvenance,

}

/// Library algorithms available for asserted and reified at-most-one constraints.

#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, Serialize, Deserialize)]

pub enum AmoEncoding {

    Pairwise,

    Ladder,

    Bitwise,

    Commander,

    Bimander,

    TwoProduct,

    PindakaasPairwise,

    PindakaasLadder,

    PindakaasBitwise,

}

encoding_labels!(AmoEncoding, "AMO encoding", 9, [

    Pairwise => "pairwise",

    Ladder => "ladder",

    Bitwise => "bitwise",

    Commander => "commander",

    Bimander => "bimander",

    TwoProduct => "two-product",

    PindakaasPairwise => "pindakaas-pairwise",

    PindakaasLadder => "pindakaas-ladder",

    PindakaasBitwise => "pindakaas-bitwise",

]);

/// Bound direction for a semantic cardinality constraint.

#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, Serialize, Deserialize)]

pub enum CardinalityRelation {

    AtMost,

    AtLeast,

    Exactly,

}

/// Provider and algorithm for a cardinality constraint.

#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, Serialize, Deserialize)]

pub enum CardinalityEncoding {

    RustsatTotalizer,

    PindakaasSortingNetwork,

}

encoding_labels!(CardinalityEncoding, "cardinality encoder", 2, [

    RustsatTotalizer => "rustsat-totalizer",

    PindakaasSortingNetwork => "pindakaas-sorting-network",

]);

/// Provider and algorithm for signed weighted pseudo-Boolean constraints.

#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, Serialize, Deserialize)]

pub enum PbEncoding {

    RustsatGeneralizedTotalizer,

    RustsatBinaryAdder,

    PindakaasBdd,

    RustsatDynamicPolyWatchdog,

    PindakaasSwc,

}

encoding_labels!(PbEncoding, "pseudo-Boolean encoder", 5, [

    RustsatGeneralizedTotalizer => "rustsat-generalized-totalizer",

    RustsatBinaryAdder => "rustsat-binary-adder",

    PindakaasBdd => "pindakaas-bdd",

    RustsatDynamicPolyWatchdog => "rustsat-dynamic-poly-watchdog",

    PindakaasSwc => "pindakaas-swc",

]);