// See www.openfst.org for extensive documentation on this weighted
// finite-state transducer library.
//
// Functions and classes to determine the equivalence of two FSTs.

#ifndef FST_EQUIVALENT_H_
#define FST_EQUIVALENT_H_

#include <algorithm>
#include <deque>
#include <unordered_map>
#include <utility>
#include <vector>
#include <fst/log.h>

#include <fst/encode.h>
#include <fst/push.h>
#include <fst/union-find.h>
#include <fst/vector-fst.h>


namespace fst {
namespace internal {

// Traits-like struct holding utility functions/typedefs/constants for
// the equivalence algorithm.
//
// Encoding device: in order to make the statesets of the two acceptors
// disjoint, we map Arc::StateId on the type MappedId. The states of
// the first acceptor are mapped on odd numbers (s -> 2s + 1), and
// those of the second one on even numbers (s -> 2s + 2). The number 0
// is reserved for an implicit (non-final) dead state (required for
// the correct treatment of non-coaccessible states; kNoStateId is mapped to
// kDeadState for both acceptors). The union-find algorithm operates on the
// mapped IDs.
template <class Arc>
struct EquivalenceUtil {
  using StateId = typename Arc::StateId;
  using Weight = typename Arc::Weight;

  using MappedId = StateId;  // ID for an equivalence class.

  // MappedId for an implicit dead state.
  static constexpr MappedId kDeadState = 0;

  // MappedId for lookup failure.
  static constexpr MappedId kInvalidId = -1;

  // Maps state ID to the representative of the corresponding
  // equivalence class. The parameter 'which_fst' takes the values 1
  // and 2, identifying the input FST.
  static MappedId MapState(StateId s, int32 which_fst) {
    return (kNoStateId == s) ? kDeadState
                             : (static_cast<MappedId>(s) << 1) + which_fst;
  }

  // Maps set ID to State ID.
  static StateId UnMapState(MappedId id) {
    return static_cast<StateId>((--id) >> 1);
  }

  // Convenience function: checks if state with MappedId s is final in
  // acceptor fa.
  static bool IsFinal(const Fst<Arc> &fa, MappedId s) {
    return (kDeadState == s) ? false
                             : (fa.Final(UnMapState(s)) != Weight::Zero());
  }
  // Convenience function: returns the representative of ID in sets,
  // creating a new set if needed.
  static MappedId FindSet(UnionFind<MappedId> *sets, MappedId id) {
    const auto repr = sets->FindSet(id);
    if (repr != kInvalidId) {
      return repr;
    } else {
      sets->MakeSet(id);
      return id;
    }
  }
};

template <class Arc>
constexpr
    typename EquivalenceUtil<Arc>::MappedId EquivalenceUtil<Arc>::kDeadState;

template <class Arc>
constexpr
    typename EquivalenceUtil<Arc>::MappedId EquivalenceUtil<Arc>::kInvalidId;

}  // namespace internal

// Equivalence checking algorithm: determines if the two FSTs fst1 and fst2
// are equivalent. The input FSTs must be deterministic input-side epsilon-free
// acceptors, unweighted or with weights over a left semiring. Two acceptors are
// considered equivalent if they accept exactly the same set of strings (with
// the same weights).
//
// The algorithm (cf. Aho, Hopcroft and Ullman, "The Design and Analysis of
// Computer Programs") successively constructs sets of states that can be
// reached by the same prefixes, starting with a set containing the start states
// of both acceptors. A disjoint tree forest (the union-find algorithm) is used
// to represent the sets of states. The algorithm returns false if one of the
// constructed sets contains both final and non-final states. Returns an
// optional error value (useful when FLAGS_error_fatal = false).
//
// Complexity:
//
// Quasi-linear, i.e., O(n G(n)), where
//
//   n = |S1| + |S2| is the number of states in both acceptors
//
//   G(n) is a very slowly growing function that can be approximated
//        by 4 by all practical purposes.
template <class Arc>
bool Equivalent(const Fst<Arc> &fst1, const Fst<Arc> &fst2,
                float delta = kDelta, bool *error = nullptr) {
  using Weight = typename Arc::Weight;
  if (error) *error = false;
  // Check that the symbol table are compatible.
  if (!CompatSymbols(fst1.InputSymbols(), fst2.InputSymbols()) ||
      !CompatSymbols(fst1.OutputSymbols(), fst2.OutputSymbols())) {
    FSTERROR() << "Equivalent: Input/output symbol tables of 1st argument "
               << "do not match input/output symbol tables of 2nd argument";
    if (error) *error = true;
    return false;
  }
  // Check properties first.
  static constexpr auto props = kNoEpsilons | kIDeterministic | kAcceptor;
  if (fst1.Properties(props, true) != props) {
    FSTERROR() << "Equivalent: 1st argument not an"
               << " epsilon-free deterministic acceptor";
    if (error) *error = true;
    return false;
  }
  if (fst2.Properties(props, true) != props) {
    FSTERROR() << "Equivalent: 2nd argument not an"
               << " epsilon-free deterministic acceptor";
    if (error) *error = true;
    return false;
  }
  if ((fst1.Properties(kUnweighted, true) != kUnweighted) ||
      (fst2.Properties(kUnweighted, true) != kUnweighted)) {
    VectorFst<Arc> efst1(fst1);
    VectorFst<Arc> efst2(fst2);
    Push(&efst1, REWEIGHT_TO_INITIAL, delta);
    Push(&efst2, REWEIGHT_TO_INITIAL, delta);
    ArcMap(&efst1, QuantizeMapper<Arc>(delta));
    ArcMap(&efst2, QuantizeMapper<Arc>(delta));
    EncodeMapper<Arc> mapper(kEncodeWeights | kEncodeLabels, ENCODE);
    ArcMap(&efst1, &mapper);
    ArcMap(&efst2, &mapper);
    return Equivalent(efst1, efst2);
  }
  using Util = internal::EquivalenceUtil<Arc>;
  using MappedId = typename Util::MappedId;
  enum { FST1 = 1, FST2 = 2 };  // Required by Util::MapState(...)
  auto s1 = Util::MapState(fst1.Start(), FST1);
  auto s2 = Util::MapState(fst2.Start(), FST2);
  // The union-find structure.
  UnionFind<MappedId> eq_classes(1000, Util::kInvalidId);
  // Initializes the union-find structure.
  eq_classes.MakeSet(s1);
  eq_classes.MakeSet(s2);
  // Data structure for the (partial) acceptor transition function of fst1 and
  // fst2: input labels mapped to pairs of MappedIds representing destination
  // states of the corresponding arcs in fst1 and fst2, respectively.
  using Label2StatePairMap =
      std::unordered_map<typename Arc::Label, std::pair<MappedId, MappedId>>;
  Label2StatePairMap arc_pairs;
  // Pairs of MappedId's to be processed, organized in a queue.
  std::deque<std::pair<MappedId, MappedId>> q;
  bool ret = true;
  // Returns early if the start states differ w.r.t. finality.
  if (Util::IsFinal(fst1, s1) != Util::IsFinal(fst2, s2)) ret = false;
  // Main loop: explores the two acceptors in a breadth-first manner, updating
  // the equivalence relation on the statesets. Loop invariant: each block of
  // the states contains either final states only or non-final states only.
  for (q.push_back(std::make_pair(s1, s2)); ret && !q.empty(); q.pop_front()) {
    s1 = q.front().first;
    s2 = q.front().second;
    // Representatives of the equivalence classes of s1/s2.
    const auto rep1 = Util::FindSet(&eq_classes, s1);
    const auto rep2 = Util::FindSet(&eq_classes, s2);
    if (rep1 != rep2) {
      eq_classes.Union(rep1, rep2);
      arc_pairs.clear();
      // Copies outgoing arcs starting at s1 into the hash-table.
      if (Util::kDeadState != s1) {
        ArcIterator<Fst<Arc>> arc_iter(fst1, Util::UnMapState(s1));
        for (; !arc_iter.Done(); arc_iter.Next()) {
          const auto &arc = arc_iter.Value();
          // Zero-weight arcs are treated as if they did not exist.
          if (arc.weight != Weight::Zero()) {
            arc_pairs[arc.ilabel].first = Util::MapState(arc.nextstate, FST1);
          }
        }
      }
      // Copies outgoing arcs starting at s2 into the hashtable.
      if (Util::kDeadState != s2) {
        ArcIterator<Fst<Arc>> arc_iter(fst2, Util::UnMapState(s2));
        for (; !arc_iter.Done(); arc_iter.Next()) {
          const auto &arc = arc_iter.Value();
          // Zero-weight arcs are treated as if they did not exist.
          if (arc.weight != Weight::Zero()) {
            arc_pairs[arc.ilabel].second = Util::MapState(arc.nextstate, FST2);
          }
        }
      }
      // Iterates through the hashtable and process pairs of target states.
      for (const auto &arc_iter : arc_pairs) {
        const auto &pair = arc_iter.second;
        if (Util::IsFinal(fst1, pair.first) !=
            Util::IsFinal(fst2, pair.second)) {
          // Detected inconsistency: return false.
          ret = false;
          break;
        }
        q.push_back(pair);
      }
    }
  }
  if (fst1.Properties(kError, false) || fst2.Properties(kError, false)) {
    if (error) *error = true;
    return false;
  }
  return ret;
}

}  // namespace fst

#endif  // FST_EQUIVALENT_H_