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 "word-range.hpp"  // for ToWord
 
#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);

    template <typename Char>
    IsObviouslyInfinite& add_rules_no_checks(
        std::basic_string<Char> const&                                lphbt,
        typename std::vector<std::basic_string<Char>>::const_iterator first,
        typename std::vector<std::basic_string<Char>>::const_iterator last) {
#ifdef LIBSEMIGROUPS_EIGEN_ENABLED
      auto matrix_start = _matrix.rows();
      _matrix.conservativeResize(matrix_start + (last - first) / 2,
                                 Eigen::NoChange);
      _matrix.block(matrix_start, 0, (last - first) / 2, _matrix.cols())
          .setZero();
#else
      auto matrix_start = 0;
      std::fill(_matrix.begin(), _matrix.end(), 0);
#endif
 
      v4::ToWord stw(lphbt);
      word_type  lhs, rhs;
      for (auto it = first; it < last; ++it) {
        stw(lhs, *it++);  // lhs changed in-place
        stw(rhs, *it);    // rhs changed in-place
        private_add_rule(matrix_start + (it - first) / 2, lhs, rhs);
      }
      _nr_letter_components = _letter_components.number_of_blocks();
      return *this;
    }

    IsObviouslyInfinite& add_rules_no_checks(
        char const*                                       lphbt,
        typename std::vector<std::string>::const_iterator first,
        typename std::vector<std::string>::const_iterator last) {
      std::vector<std::string> copy(first, last);
      return add_rules_no_checks(std::string(lphbt), copy.begin(), copy.end());
    }

    template <typename Char>
    IsObviouslyInfinite&
    add_rules_no_checks(std::basic_string<Char> const& lphbt,
                        const_iterator_word_type       first,
                        const_iterator_word_type       last) {
#ifdef LIBSEMIGROUPS_EIGEN_ENABLED
      auto matrix_start = _matrix.rows();
      _matrix.conservativeResize(matrix_start + (last - first) / 2,
                                 Eigen::NoChange);
      _matrix.block(matrix_start, 0, (last - first) / 2, _matrix.cols())
          .setZero();
#else
      auto matrix_start = 0;
      std::fill(_matrix.begin(), _matrix.end(), 0);
#endif
 
      v4::ToWord              to_word(lphbt);
      word_type               lhs, rhs;
      std::basic_string<Char> tmp;
      for (auto it = first; it < last; ++it) {
        // changes lhs in-place
        tmp.assign(it->begin(), it->end());
        to_word(lhs, tmp);
        ++it;
        // changes rhs in-place
        tmp.assign(it->begin(), it->end());
        to_word(rhs, tmp);
        private_add_rule(matrix_start + (it - first) / 2, lhs, rhs);
      }
      _nr_letter_components = _letter_components.number_of_blocks();
      return *this;
    }

    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_