knuth-bendix-impl.hpp

//
// libsemigroups - C++ library for semigroups and monoids
// Copyright (C) 2019-2025 James D. Mitchell + Joseph Edwards
//
// 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 class KnuthBendixImpl which implements the Knuth-Bendix
// algorithm for finitely presented monoids.
 
// TODO(1)
// * noexcept
// * separate rule container from Rules
// * nodiscard
 
#ifndef LIBSEMIGROUPS_DETAIL_KNUTH_BENDIX_IMPL_HPP_
#define LIBSEMIGROUPS_DETAIL_KNUTH_BENDIX_IMPL_HPP_
 
#include <algorithm>      // for max, min, copy
#include <atomic>         // for atomic_bool
#include <cctype>         // for isprint
#include <chrono>         // for duration_cast
#include <cmath>          // for pow
#include <cstddef>        // for size_t
#include <cstdint>        // for int64_t, uint32_t
#include <iterator>       // for back_inserter
#include <memory>         // for allocator, uni...
#include <ostream>        // for ostream
#include <string>         // for basic_string
#include <string_view>    // for basic_string_view
#include <type_traits>    // for is_same_v
#include <unordered_map>  // for unordered_map
#include <utility>        // for move, make_pair
#include <vector>         // for vector
 
#include "libsemigroups/adapters.hpp"      // for Hash
#include "libsemigroups/constants.hpp"     // for POSITIVE_INFINITY
#include "libsemigroups/debug.hpp"         // for LIBSEMIGROUPS_...
#include "libsemigroups/obvinf.hpp"        // for is_obviously_infinite
#include "libsemigroups/order.hpp"         // for ShortLexCompare
#include "libsemigroups/presentation.hpp"  // for operator!=
#include "libsemigroups/ranges.hpp"        // for count, iterato...
#include "libsemigroups/types.hpp"         // for congruence_kind
#include "libsemigroups/word-graph.hpp"    // for WordGraph, to_...
#include "libsemigroups/word-range.hpp"    // for to_human_reada...
 
#include "cong-common-class.hpp"  // for CongruenceInte...
#include "fmt.hpp"                // for format, print
#include "report.hpp"             // for report_no_prefix
#include "rewriters.hpp"          // for Rule, internal...
#include "string.hpp"             // for group_digits
#include "timer.hpp"              // for string_time
 
namespace libsemigroups {
  // Forward declarations
  namespace detail {
    template <typename KnuthBendix_>
    class KBE;




 
    template <typename Rewriter       = detail::RewriteTrie,
              typename ReductionOrder = ShortLexCompare>
    class KnuthBendixImpl : public CongruenceCommon {
     public:
      // Aliases
 
      using native_word_type = typename Rewriter::native_word_type;
      using rule_type        = std::pair<native_word_type, native_word_type>;
      using rewriter_type    = Rewriter;

      // Nested classes - public
 
      struct options {
        enum class overlap { ABC = 0, AB_BC = 1, MAX_AB_BC = 2 };
      };
 
     private:
      // Nested classes - private
 
      // Overlap measures
      struct OverlapMeasure {
        virtual size_t
        operator()(detail::Rule const*,
                   detail::Rule const* examples,
                   typename native_word_type::const_iterator const&)
            = 0;
        virtual ~OverlapMeasure() {}
      };
 
      struct ABC;
      struct AB_BC;
      struct MAX_AB_BC;
 
      struct Settings {
        Settings() noexcept;
        Settings& init() noexcept;
 
        Settings(Settings const&) noexcept            = default;
        Settings(Settings&&) noexcept                 = default;
        Settings& operator=(Settings const&) noexcept = default;
        Settings& operator=(Settings&&) noexcept      = default;
 
        size_t                    max_pending_rules;
        size_t                    check_confluence_interval;
        size_t                    max_overlap;
        size_t                    max_rules;
        typename options::overlap overlap_policy;
      };
 
      struct Stats {
        Stats() noexcept;
        Stats& init() noexcept;
 
        Stats(Stats const&) noexcept            = default;
        Stats(Stats&&) noexcept                 = default;
        Stats& operator=(Stats const&) noexcept = default;
        Stats& operator=(Stats&&) noexcept      = default;
 
        size_t prev_active_rules;
        size_t prev_inactive_rules;
        size_t prev_total_rules;
      };

      // KnuthBendixImpl - data - private
 
      bool                            _gen_pairs_initted;
      WordGraph<uint32_t>             _gilman_graph;
      std::vector<native_word_type>   _gilman_graph_node_labels;
      std::unique_ptr<OverlapMeasure> _overlap_measure;
      Presentation<native_word_type>  _presentation;
      mutable Rewriter                _rewriter;
      Settings                        _settings;
      mutable Stats                   _stats;
      mutable native_word_type        _tmp_element1;
 
     public:
      // KnuthBendixImpl - constructors and destructor - public
 
      KnuthBendixImpl();
      KnuthBendixImpl& init();
      KnuthBendixImpl(KnuthBendixImpl const& that);
 
      KnuthBendixImpl(KnuthBendixImpl&&);
 
      KnuthBendixImpl& operator=(KnuthBendixImpl const&);
 
      KnuthBendixImpl& operator=(KnuthBendixImpl&&);
 
      ~KnuthBendixImpl();
 
      KnuthBendixImpl(congruence_kind                       knd,
                      Presentation<native_word_type> const& p);
 
      KnuthBendixImpl& init(congruence_kind                       knd,
                            Presentation<native_word_type> const& p);
 
      KnuthBendixImpl(congruence_kind knd, Presentation<native_word_type>&& p);
 
      KnuthBendixImpl& init(congruence_kind                  knd,
                            Presentation<native_word_type>&& p);
 
      // TODO(1) construct/init from kind and KnuthBendixImpl const&, for
      // consistency with ToddCoxeterImpl
 
     private:
      void init_from_generating_pairs();
      void init_from_internal_presentation();

      // KnuthBendixImpl - interface requirements - add_generating_pair
 
     public:
      // NOTE THAT this is not the same as in ToddCoxeterImpl, because the
      // generating pairs contained in CongruenceCommon are word_types, and
      // so we don't require any conversion here (since chars can be converted
      // implicitly to letter_types)
      template <typename Iterator1,
                typename Iterator2,
                typename Iterator3,
                typename Iterator4>
      KnuthBendixImpl& add_generating_pair_no_checks(Iterator1 first1,
                                                     Iterator2 last1,
                                                     Iterator3 first2,
                                                     Iterator4 last2) {
        LIBSEMIGROUPS_ASSERT(!started());
        return CongruenceCommon::add_internal_generating_pair_no_checks<
            KnuthBendixImpl>(first1, last1, first2, last2);
      }
 
      template <typename Iterator1,
                typename Iterator2,
                typename Iterator3,
                typename Iterator4>
      KnuthBendixImpl& add_generating_pair(Iterator1 first1,
                                           Iterator2 last1,
                                           Iterator3 first2,
                                           Iterator4 last2) {
        LIBSEMIGROUPS_ASSERT(!started());
        return CongruenceCommon::add_generating_pair<KnuthBendixImpl>(
            first1, last1, first2, last2);
      }

      // KnuthBendixImpl - interface requirements - number_of_classes

      [[nodiscard]] uint64_t number_of_classes();

      // KnuthBendixImpl - interface requirements - contains

      template <typename Iterator1,
                typename Iterator2,
                typename Iterator3,
                typename Iterator4>
      [[nodiscard]] tril currently_contains_no_checks(Iterator1 first1,
                                                      Iterator2 last1,
                                                      Iterator3 first2,
                                                      Iterator4 last2) const;
 
      // Documented in KnuthBendix (because it appears there because we call
      // CongruenceCommon::currently_contains directly so that bounds checks are
      // done in KnuthBendix)
      template <typename Iterator1,
                typename Iterator2,
                typename Iterator3,
                typename Iterator4>
      [[nodiscard]] tril currently_contains(Iterator1 first1,
                                            Iterator2 last1,
                                            Iterator3 first2,
                                            Iterator4 last2) const {
        return CongruenceCommon::currently_contains<KnuthBendixImpl>(
            first1, last1, first2, last2);
      }

      template <typename Iterator1,
                typename Iterator2,
                typename Iterator3,
                typename Iterator4>
      [[nodiscard]] bool contains_no_checks(Iterator1 first1,
                                            Iterator2 last1,
                                            Iterator3 first2,
                                            Iterator4 last2) {
        return CongruenceCommon::contains_no_checks<KnuthBendixImpl>(
            first1, last1, first2, last2);
      }
 
      // Documented in KnuthBendix (because it appears there because we call
      // CongruenceCommon::contains directly so that bounds checks are
      // done in KnuthBendix)
      template <typename Iterator1,
                typename Iterator2,
                typename Iterator3,
                typename Iterator4>
      [[nodiscard]] bool contains(Iterator1 first1,
                                  Iterator2 last1,
                                  Iterator3 first2,
                                  Iterator4 last2) {
        return CongruenceCommon::contains<KnuthBendixImpl>(
            first1, last1, first2, last2);
      }

      // KnuthBendixImpl - interface requirements - reduce
 
      template <typename OutputIterator,
                typename InputIterator1,
                typename InputIterator2>
      OutputIterator reduce_no_run_no_checks(OutputIterator d_first,
                                             InputIterator1 first,
                                             InputIterator2 last) const;
 
      // Documented in KnuthBendix (because it appears there because we call
      // CongruenceCommon::reduce_no_run directly so that bounds checks are
      // done in KnuthBendix)
      template <typename OutputIterator,
                typename InputIterator1,
                typename InputIterator2>
      OutputIterator reduce_no_run(OutputIterator d_first,
                                   InputIterator1 first,
                                   InputIterator2 last) const {
        return CongruenceCommon::reduce_no_run<KnuthBendixImpl>(
            d_first, first, last);
      }
 
      template <typename OutputIterator,
                typename InputIterator1,
                typename InputIterator2>
      OutputIterator reduce_no_checks(OutputIterator d_first,
                                      InputIterator1 first,
                                      InputIterator2 last) {
        return CongruenceCommon::reduce_no_checks<KnuthBendixImpl>(
            d_first, first, last);
      }
 
      // Documented in KnuthBendix (because it appears there because we call
      // CongruenceCommon::reduce directly so that bounds checks are
      // done in KnuthBendix)
      template <typename OutputIterator,
                typename InputIterator1,
                typename InputIterator2>
      OutputIterator reduce(OutputIterator d_first,
                            InputIterator1 first,
                            InputIterator2 last) {
        return CongruenceCommon::reduce<KnuthBendixImpl>(d_first, first, last);
      }
 
      // TODO(1) implement reduce_inplace x4 if possible.

      // KnuthBendixImpl - setters for optional parameters - public

      KnuthBendixImpl& max_pending_rules(size_t val) {
        _settings.max_pending_rules = val;
        return *this;
      }

      [[nodiscard]] size_t max_pending_rules() const noexcept {
        return _settings.max_pending_rules;
      }

      KnuthBendixImpl& check_confluence_interval(size_t val) {
        _settings.check_confluence_interval = val;
        return *this;
      }

      [[nodiscard]] size_t check_confluence_interval() const noexcept {
        return _settings.check_confluence_interval;
      }

      KnuthBendixImpl& max_overlap(size_t val) {
        _settings.max_overlap = val;
        return *this;
      }

      [[nodiscard]] size_t max_overlap() const noexcept {
        return _settings.max_overlap;
      }

      KnuthBendixImpl& max_rules(size_t val) {
        _settings.max_rules = val;
        return *this;
      }

      [[nodiscard]] size_t max_rules() const noexcept {
        return _settings.max_rules;
      }

      KnuthBendixImpl& overlap_policy(typename options::overlap val);

      [[nodiscard]] typename options::overlap overlap_policy() const noexcept {
        return _settings.overlap_policy;
      }

      // KnuthBendixImpl - member functions for rules and rewriting - public
 
      // TODO(1) remove
      template <typename Iterator1, typename Iterator2>
      void throw_if_letter_not_in_alphabet(Iterator1 first,
                                           Iterator2 last) const {
        internal_presentation().throw_if_letter_not_in_alphabet(first, last);
      }
 
      [[nodiscard]] Presentation<native_word_type> const&
      internal_presentation() const noexcept {
        return _presentation;
      }

      [[nodiscard]] size_t number_of_active_rules() const noexcept;

      [[nodiscard]] size_t number_of_inactive_rules() const noexcept {
        return _rewriter.number_of_inactive_rules();
      }

      [[nodiscard]] size_t number_of_pending_rules() const noexcept {
        return _rewriter.number_of_pending_rules();
      }

      [[nodiscard]] size_t total_rules() const noexcept {
        return _rewriter.stats().total_rules;
      }
 
      Rewriter& rewriter() noexcept {
        return _rewriter;
      }
 
      // Documented in KnuthBendix
      // TODO(1) should be const
      // TODO(1) add note about empty active rules after, or better discuss that
      // there are three kinds of rules in the system: active, inactive, and
      // pending.
      [[nodiscard]] auto active_rules();

      KnuthBendixImpl& process_pending_rules() {
        _rewriter.process_pending_rules();
        return *this;
      }
 
     private:
      // TODO(1) remove this ...
      void rewrite_inplace(native_word_type& w);
 
      // TODO(1) remove this ...
      [[nodiscard]] native_word_type rewrite(native_word_type w) {
        rewrite_inplace(w);
        return w;
      }
 
     public:
      // KnuthBendixImpl - main member functions - public

      [[nodiscard]] bool confluent() const;

      [[nodiscard]] bool confluent_known() const noexcept;

      WordGraph<uint32_t> const& gilman_graph();
 
      // Documented in KnuthBendix
      [[nodiscard]] std::vector<native_word_type> const&
      gilman_graph_node_labels() {
        gilman_graph();  // to ensure that gilman_graph is initialised
        return _gilman_graph_node_labels;
      }
 
     protected:
      // run_impl is called by KnuthBendix
      void run_impl() override;
 
     private:
      // KnuthBendixImpl - private member functions
 
      void report_presentation() const;
      void report_before_run();
      void report_progress_from_thread(std::atomic_bool const&);
      void report_after_run();
 
      void stats_check_point();
 
      void add_octo(native_word_type& w) const;
      void rm_octo(native_word_type& w) const;
 
      void add_rule_impl(native_word_type const& p, native_word_type const& q);
 
      void overlap(detail::Rule const* u, detail::Rule const* v);
 
      [[nodiscard]] size_t max_active_word_length() const {
        return _rewriter.max_active_word_length();
      }
 
      void               run_real(std::atomic_bool&);
      [[nodiscard]] bool stop_running() const;

      // Runner - pure virtual member functions - private
 
      bool finished_impl() const override;
    };  // class KnuthBendixImpl
  }     // namespace detail

  // global functions - to_human_readable_repr
 
  // TODO(1) for consistency (with ToddCoxeter), the next two functions should
  // really be in knuth-bendix.hpp.

#ifdef LIBSEMIGROUPS_PARSED_BY_DOXYGEN
  template <typename Word, typename Rewriter, typename ReductionOrder>
  std::ostream&
  operator<<(std::ostream&                                      os,
             KnuthBendix<Word, Rewriter, ReductionOrder> const& kb);
#else
  template <typename Rewriter, typename ReductionOrder>
  std::ostream&
  operator<<(std::ostream&                                            os,
             detail::KnuthBendixImpl<Rewriter, ReductionOrder> const& kb);
#endif

  // TODO(1) preferably kb would be a const&
#ifdef LIBSEMIGROUPS_PARSED_BY_DOXYGEN
  template <typename Word, typename Rewriter, typename ReductionOrder>
  std::string
  to_human_readable_repr(KnuthBendix<Word, Rewriter, ReductionOrder>& kb);
#else
  template <typename Rewriter, typename ReductionOrder>
  std::string
  to_human_readable_repr(detail::KnuthBendixImpl<Rewriter, ReductionOrder>& kb);
#endif

  // TODO(1) kb should be const
  template <typename Result, typename Rewriter, typename ReductionOrder>
  auto to(detail::KnuthBendixImpl<Rewriter, ReductionOrder>& kb)
      -> std::enable_if_t<
          std::is_same_v<Presentation<typename Result::word_type>, Result>,
          Result>;
 
}  // namespace libsemigroups
 
#include "knuth-bendix-impl.tpp"
 
#endif  // LIBSEMIGROUPS_DETAIL_KNUTH_BENDIX_IMPL_HPP_