obvinf.hpp

//
// libsemigroups - C++ library for semigroups and monoids
// Copyright (C) 2020-2025 James D. Mitchell + Reinis Cirpons
//
// This program is free software: you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation, either version 3 of the License, or
// (at your option) any later version.
//
// This program is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU General Public License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
//
 
// This file contains a helper class for checking whether or not a congruence
// defined by generating pairs or finitely presented semigroup or monoid is
// obviously infinite.
 
#ifndef LIBSEMIGROUPS_OBVINF_HPP_
#define LIBSEMIGROUPS_OBVINF_HPP_
 
#include <cstddef>  // for size_t
#include <numeric>  // for accumulate
#include <string>   // for string
#include <utility>  // for pair
#include <vector>   // for vector
 
#include "config.hpp"      // for LIBSEMIGROUPS_EIGEN_ENABLED
#include "ranges.hpp"      // for rx/ranges
#include "types.hpp"       // for word_type etc
#include "word-graph.hpp"  // for is_acyclic
 
#include "detail/eigen.hpp"  // for eigen
#include "detail/uf.hpp"     // for Duf
 
namespace libsemigroups {
#ifndef LIBSEMIGROUPS_PARSED_BY_DOXYGEN
 
  namespace detail {
    template <typename Rewriter, typename ReductionOrder>
    class KnuthBendixImpl;  // forward decl
    class ToddCoxeterImpl;  // forward decl
  }                         // namespace detail
 
  template <typename Word>
  class Congruence;  // forward decl
 
  template <typename Word>
  class Kambites;  // forward decl
 
  template <typename Word>
  class Presentation;  // forward decl
#endif
 
  namespace presentation {
    template <typename Word>
    void change_alphabet(Presentation<Word>&, Word const&);
  }


  // TODO(1) there are definitely some assumptions about the calls to the member
  // functions of an IsObviouslyInfinite (see for example the function
  // is_obviously_infinite for a Presentation). These should be documented.
  //
  // TODO(1) this class should be more generic, like detail::CongruenceCommon
  // and its derived classes, allowing arbitrary iterators of rules to be added
  class IsObviouslyInfinite {
    // The default constructor is private since an object that is default
    // constructed isn't usable with the current public API.
    IsObviouslyInfinite() = default;
 
   public:
    using const_iterator_word_type =
        typename std::vector<word_type>::const_iterator;

    using const_iterator_pair_string = typename std::vector<
        std::pair<std::string, std::string>>::const_iterator;

    using const_iterator_string =
        typename std::vector<std::string>::const_iterator;

    explicit IsObviouslyInfinite(size_t n);

    IsObviouslyInfinite& init(size_t n);

    explicit IsObviouslyInfinite(std::string const& lphbt)
        : IsObviouslyInfinite(lphbt.size()) {}

    IsObviouslyInfinite& init(std::string const& lphbt) {
      return init(lphbt.size());
    }

    IsObviouslyInfinite(IsObviouslyInfinite const&) = delete;

    IsObviouslyInfinite(IsObviouslyInfinite&&) = delete;

    IsObviouslyInfinite& operator=(IsObviouslyInfinite const&) = delete;

    IsObviouslyInfinite& operator=(IsObviouslyInfinite&&) = delete;
 
    ~IsObviouslyInfinite();

    IsObviouslyInfinite& add_rules_no_checks(word_type const&,
                                             const_iterator_word_type first,
                                             const_iterator_word_type last);

    IsObviouslyInfinite& add_rules_no_checks(std::string const&    lphbt,
                                             const_iterator_string first,
                                             const_iterator_string last);

    IsObviouslyInfinite& add_rules_no_checks(std::string const&       lphbt,
                                             const_iterator_word_type first,
                                             const_iterator_word_type last);

    IsObviouslyInfinite& add_rules_no_checks(std::string const&         lphbt,
                                             const_iterator_pair_string first,
                                             const_iterator_pair_string last);

    bool result() const;
 
    // TODO(1) certificate() returning why the thing is obviously infinite
 
   private:
    void private_add_rule(size_t const, word_type const&, word_type const&);
 
    inline void letters_in_word(size_t row, word_type const& w, int64_t adv) {
      for (size_t const& x : w) {
        matrix(row, x) += adv;
        _seen[x] = true;
      }
    }
 
    inline void plus_letters_in_word(size_t row, word_type const& w) {
      letters_in_word(row, w, 1);
    }
 
    inline void minus_letters_in_word(size_t row, word_type const& w) {
      letters_in_word(row, w, -1);
    }
 
    inline int64_t& matrix(size_t row, size_t col) {
#ifdef LIBSEMIGROUPS_EIGEN_ENABLED
      return _matrix(row, col);
#else
      (void) row;
      return _matrix[col];
#endif
    }
 
    inline bool matrix_row_sums_to_0(size_t row) {
#ifdef LIBSEMIGROUPS_EIGEN_ENABLED
      return _matrix.row(row).sum() == 0;
#else
      (void) row;
      return std::accumulate(_matrix.cbegin(), _matrix.cend(), 0) == 0;
#endif
    }
 
    // letter_type i belongs to "preserve" if there exists a relation where
    // the number of occurrences of i is not the same on both sides of the
    // relation letter_type i belongs to "unique" if there is a relation
    // where one side consists solely of i.
    bool              _empty_word;
    detail::Duf<>     _letter_components;
    size_t            _nr_gens;
    size_t            _nr_letter_components;
    size_t            _nr_relations;
    bool              _preserve_length;
    std::vector<bool> _preserve;
    std::vector<bool> _seen;
    std::vector<bool> _unique;
 
#ifdef LIBSEMIGROUPS_EIGEN_ENABLED
    Eigen::Matrix<int64_t, Eigen::Dynamic, Eigen::Dynamic> _matrix;
#else
    std::vector<int64_t> _matrix;
#endif
  };

  template <typename Word>
  bool is_obviously_infinite(Presentation<Word> const& p) {
    p.throw_if_bad_alphabet_or_rules();
    if (p.alphabet().empty()) {
      return false;
    }
    auto it
        = std::max_element(std::begin(p.alphabet()), std::end(p.alphabet()));
 
    if (*it != p.alphabet().size() - 1) {
      auto copy_p = p;
      presentation::change_alphabet(
          copy_p,
          rx::seq<typename Presentation<Word>::letter_type>(0)
              | rx::take(p.alphabet().size()) | rx::to_vector());
      IsObviouslyInfinite ioi(copy_p.alphabet().size());
      ioi.add_rules_no_checks(
          p.alphabet(), copy_p.rules.cbegin(), copy_p.rules.cend());
      return ioi.result();
    }
 
    IsObviouslyInfinite ioi(p.alphabet().size());
    ioi.add_rules_no_checks(p.alphabet(), p.rules.cbegin(), p.rules.cend());
    return ioi.result();
  }

  template <>
  bool is_obviously_infinite(Presentation<std::string> const& p);

  bool is_obviously_infinite(detail::ToddCoxeterImpl const& tc);

  // This function is implemented in cong-class.tpp
  template <typename Word>
  bool is_obviously_infinite(Congruence<Word>& c);

  template <typename Word>
  bool is_obviously_infinite(Kambites<Word>& k) {
    if (k.finished() && k.small_overlap_class() >= 3) {
      return true;
    }
    if (is_obviously_infinite(k.presentation())) {
      return true;
    }
    return k.small_overlap_class() >= 3;
  }

  template <typename Rewriter, typename ReductionOrder>
  bool
  is_obviously_infinite(detail::KnuthBendixImpl<Rewriter, ReductionOrder>& kb) {
    if (kb.finished()) {
      return !word_graph::is_acyclic(kb.gilman_graph());
    }
    auto const& p = kb.internal_presentation();
    if (p.alphabet().empty()) {
      return false;
    }
    IsObviouslyInfinite ioi(p.alphabet().size());
    ioi.add_rules_no_checks(p.alphabet(), p.rules.cbegin(), p.rules.cend());
    ioi.add_rules_no_checks(p.alphabet(),
                            kb.internal_generating_pairs().cbegin(),
                            kb.internal_generating_pairs().cend());
    return ioi.result();
  }
 
}  // namespace libsemigroups
#endif  // LIBSEMIGROUPS_OBVINF_HPP_