use std::fmt;

use merc_data::DataVariable;

use merc_utilities::MercError;

use oxidd::ManagerRef;

use oxidd::ldd::LDDFunction;

use oxidd::ldd::LDDManagerRef;

use oxidd::ldd::Value;

use crate::DependencyGraph;

use crate::Relation;

/// A generic trait for symbolic LDD-based state-space exploration.

///

/// Any type with an initial state and transition groups can be explored via [crate::reachability].

pub trait SymbolicLPS {

    /// The transition group type backing this LTS.

    type Group: TransitionGroup;

    /// Returns the LDD representing the initial state(s).

    fn initial_state(&self) -> &LDDFunction;

    /// Returns the transition groups.

    fn transition_groups(&self) -> &[Self::Group];

    /// Returns the transition groups (mutable), needed for on-the-fly learning.

    fn transition_groups_mut(&mut self) -> &mut [Self::Group];

    /// Creates a fresh learning context, threaded through [TransitionGroup::learn_successors].

    ///

    /// The context owns the per-run mutable state shared by all groups (e.g. an enumeration backend

    /// and value interning), so the groups themselves need no interior mutability. It is created once

    /// per reachability run and must outlive every learning call.

    fn create_context(&self) -> <Self::Group as TransitionGroup>::Context;

    /// Computes the dependency graph from the read/write indices of each transition group.

                )

}

/// A single LDD-based transition group for a set of summands (short vector encoding).

pub trait TransitionGroup: fmt::Debug {

    /// Per-run mutable state threaded into [Self::learn_successors]; `()` when nothing is learned.

    type Context;

    /// Returns the transition relation T' -> U' for this summand group.

    fn relation(&self) -> &LDDFunction;

    /// Returns the read indices for this summand group.

    fn read_indices(&self) -> &[u32];

    /// Returns the write indices for this summand group.

    fn write_indices(&self) -> &[u32];

    /// Returns the action label index for this summand group, if any.

    fn action_label_index(&self) -> Option<usize>;

    /// Returns the meta LDD required to perform the relational product.

    fn meta(&self) -> &LDDFunction;

    /// Learns the successors of `todo` and incorporates them into [Self::relation].

    fn learn_successors(

        &mut self,

        context: &mut Self::Context,

        manager: &LDDManagerRef,

        todo: &LDDFunction,

    ) -> Result<(), MercError>;

}

/// A short vector transition relation for a group of summands.

///

/// A short transition vector is part of a transition relation T -> U, where we

/// store T' -> U' with T' being the projection of T on the read parameters and

/// U' the projection of U on the write parameters, as a LDD. Formally,

///

/// (t, u) in (T -> U)  iff  (t', u') in (T' -> U') where t' and u' are the projections

///     of t and u on the read and write parameters respectively.

pub struct SummandGroup {

    read_parameters: Vec<DataVariable>,

    read_parameter_indices: Vec<Value>,

    write_parameters: Vec<DataVariable>,

    write_parameter_indices: Vec<Value>,

    relation: LDDFunction,

    meta: LDDFunction,

    action_label_index: usize,

}

impl SummandGroup {

    /// Creates a new summand group.

    ///

    /// Fails if a read or write parameter is not found in `parameters`.

            .meta;

    /// Returns the read parameters for this summand group.

    /// Returns the write parameters for this summand group.

}

impl TransitionGroup for SummandGroup {

    type Context = ();

}

impl fmt::Debug for SummandGroup {

            "{:?} -> {:?}",

            self.read_parameter_indices, self.write_parameter_indices

        )

}