Quelle knuth-bendix-impl.hpp Sprache: C

//
// libsemigroups - C++ library for semigroups and monoids
// Copyright (C) 2019 James D. Mitchell
//
// 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 the implementation of the class KnuthBendixImpl, which is
// the main implementation for the class KnuthBendix.

#ifndef LIBSEMIGROUPS_SRC_KNUTH_BENDIX_IMPL_HPP_
#define LIBSEMIGROUPS_SRC_KNUTH_BENDIX_IMPL_HPP_

#include <algorithm>    // for max, min
#include <atomic>       // for atomic
#include <cinttypes>    // for int64_t
#include <cstddef>      // for size_t
#include <limits>       // for numeric_limits
#include <list>         // for list, list<>::iterator
#include <ostream>      // for string
#include <set>          // for set
#include <stack>        // for stack
#include <string>       // for operator!=, basic_strin...
#include <type_traits>  // for swap
#include <utility>      // for pair
#include <vector>       // for vector

#ifdef LIBSEMIGROUPS_VERBOSE
#include <unordered_set>  // for unordered_set
#endif

#include "libsemigroups/config.hpp"        // for LIBSEMIGROUPS_DEBUG
#include "libsemigroups/constants.hpp"     // for POSITIVE_INFINITY
#include "libsemigroups/debug.hpp"         // for LIBSEMIGROUPS_ASSERT
#include "libsemigroups/knuth-bendix.hpp"  // for KnuthBendix, KnuthBendi...
#include "libsemigroups/order.hpp"         // for shortlex_compare
#include "libsemigroups/report.hpp"        // for REPORT
#include "libsemigroups/string.hpp"  // for detail::is_suffix, maximum_comm...
#include "libsemigroups/timer.hpp"   // for detail::Timer
#include "libsemigroups/types.hpp"   // for word_type

namespace libsemigroups {
  namespace detail {
    class KBE;  // Forward declarations
  }
  namespace fpsemigroup {

    class KnuthBendix::KnuthBendixImpl {
      ////////////////////////////////////////////////////////////////////////
      // KnuthBendixImpl - typedefs/aliases - private
      ////////////////////////////////////////////////////////////////////////

      using external_string_type = std::string;
      using internal_string_type = std::string;
      using external_char_type   = char;
      using internal_char_type   = char;

      ////////////////////////////////////////////////////////////////////////
      // KnuthBendixImpl - nested subclasses - private
      ////////////////////////////////////////////////////////////////////////

      // Rule and RuleLookup classes
      class Rule {
       public:
        // Construct from KnuthBendix with new but empty internal_string_type's
        explicit Rule(KnuthBendixImpl const* kbimpl, int64_t id)
            : _kbimpl(kbimpl),
              _lhs(new internal_string_type()),
              _rhs(new internal_string_type()),
              _id(-1 * id) {
          LIBSEMIGROUPS_ASSERT(_id < 0);
        }

        // The Rule class does not support an assignment constructor to avoid
        // accidental copying.
        Rule& operator=(Rule const& copy) = delete;

        // The Rule class does not support a copy constructor to avoid
        // accidental copying.
        Rule(Rule const& copy) = delete;

        // Destructor, deletes pointers used to create the rule.
        ~Rule() {
          delete _lhs;
          delete _rhs;
        }

        // Returns the left hand side of the rule, which is guaranteed to be
        // greater than its right hand side according to the reduction ordering
        // of the KnuthBendix used to construct this.
        internal_string_type* lhs() const {
          return _lhs;
        }

        // Returns the right hand side of the rule, which is guaranteed to be
        // less than its left hand side according to the reduction ordering of
        // the KnuthBendix used to construct this.
        internal_string_type* rhs() const {
          return _rhs;
        }

        void rewrite() {
          LIBSEMIGROUPS_ASSERT(_id != 0);
          _kbimpl->internal_rewrite(_lhs);
          _kbimpl->internal_rewrite(_rhs);
          // reorder if necessary
          if (shortlex_compare(_lhs, _rhs)) {
            std::swap(_lhs, _rhs);
          }
        }

        void clear() {
          LIBSEMIGROUPS_ASSERT(_id != 0);
          _lhs->clear();
          _rhs->clear();
        }

        inline bool active() const {
          LIBSEMIGROUPS_ASSERT(_id != 0);
          return (_id > 0);
        }

        void deactivate() {
          LIBSEMIGROUPS_ASSERT(_id != 0);
          if (active()) {
            _id *= -1;
          }
        }

        void activate() {
          LIBSEMIGROUPS_ASSERT(_id != 0);
          if (!active()) {
            _id *= -1;
          }
        }

        void set_id(int64_t id) {
          LIBSEMIGROUPS_ASSERT(id > 0);
          LIBSEMIGROUPS_ASSERT(!active());
          _id = -1 * id;
        }

        int64_t id() const {
          LIBSEMIGROUPS_ASSERT(_id != 0);
          return _id;
        }

        KnuthBendixImpl const* _kbimpl;
        internal_string_type*  _lhs;
        internal_string_type*  _rhs;
        int64_t                _id;
      };  // struct Rule

      // Simple class wrapping a two iterators to an internal_string_type and a
      // Rule const*

      class RuleLookup {
       public:
        RuleLookup() : _rule(nullptr) {}

        explicit RuleLookup(Rule* rule)
            : _first(rule->lhs()->cbegin()),
              _last(rule->lhs()->cend()),
              _rule(rule) {}

        RuleLookup& operator()(internal_string_type::iterator const& first,
                               internal_string_type::iterator const& last) {
          _first = first;
          _last  = last;
          return *this;
        }

        Rule const* rule() const {
          return _rule;
        }

        // This implements reverse lex comparison of this and that, which
        // satisfies the requirement of std::set that equivalent items be
        // incomparable, so, for example bcbc and abcbc are considered
        // equivalent, but abcba and bcbc are not.
        bool operator<(RuleLookup const& that) const {
          auto it_this = _last - 1;
          auto it_that = that._last - 1;
          while (it_this > _first && it_that > that._first
                 && *it_this == *it_that) {
            --it_that;
            --it_this;
          }
          return *it_this < *it_that;
        }

       private:
        internal_string_type::const_iterator _first;
        internal_string_type::const_iterator _last;
        Rule const*                          _rule;
      };  // class RuleLookup

      // Overlap measures
      struct OverlapMeasure {
        virtual size_t operator()(Rule const*,
                                  Rule const*,
                                  internal_string_type::const_iterator const&)
            = 0;
        virtual ~OverlapMeasure() {}
      };

      struct ABC : OverlapMeasure {
        size_t
        operator()(Rule const*                                 AB,
                   Rule const*                                 BC,
                   internal_string_type::const_iterator const& it) override {
          LIBSEMIGROUPS_ASSERT(AB->active() && BC->active());
          LIBSEMIGROUPS_ASSERT(AB->lhs()->cbegin() <= it);
          LIBSEMIGROUPS_ASSERT(it < AB->lhs()->cend());
          // |A| + |BC|
          return (it - AB->lhs()->cbegin()) + BC->lhs()->size();
        }
      };

      struct AB_BC : OverlapMeasure {
        size_t
        operator()(Rule const*                                 AB,
                   Rule const*                                 BC,
                   internal_string_type::const_iterator const& it) override {
          LIBSEMIGROUPS_ASSERT(AB->active() && BC->active());
          LIBSEMIGROUPS_ASSERT(AB->lhs()->cbegin() <= it);
          LIBSEMIGROUPS_ASSERT(it < AB->lhs()->cend());
          (void) it;
          // |AB| + |BC|
          return AB->lhs()->size() + BC->lhs()->size();
        }
      };

      struct MAX_AB_BC : OverlapMeasure {
        size_t
        operator()(Rule const*                                 AB,
                   Rule const*                                 BC,
                   internal_string_type::const_iterator const& it) override {
          LIBSEMIGROUPS_ASSERT(AB->active() && BC->active());
          LIBSEMIGROUPS_ASSERT(AB->lhs()->cbegin() <= it);
          LIBSEMIGROUPS_ASSERT(it < AB->lhs()->cend());
          (void) it;
          // max(|AB|, |BC|)
          return std::max(AB->lhs()->size(), BC->lhs()->size());
        }
      };

      //////////////////////////////////////////////////////////////////////////
      // KnuthBendixImpl - friend declarations - private
      //////////////////////////////////////////////////////////////////////////

      friend class Rule;                          // defined in this file
      friend class ::libsemigroups::detail::KBE;  // defined in detail::kbe.hpp

     public:
      //////////////////////////////////////////////////////////////////////////
      // KnuthBendixImpl - constructors + destructor - public
      //////////////////////////////////////////////////////////////////////////

      explicit KnuthBendixImpl(KnuthBendix* kb)
          : _active_rules(),
            _confluent(false),
            _confluence_known(false),
            _inactive_rules(),
            _internal_is_same_as_external(false),
            _contains_empty_string(false),
            _kb(kb),
            _min_length_lhs_rule(std::numeric_limits<size_t>::max()),
            _overlap_measure(nullptr),
            _stack(),
            _tmp_word1(new internal_string_type()),
            _tmp_word2(new internal_string_type()),
            _total_rules(0) {
        _next_rule_it1 = _active_rules.end();  // null
        _next_rule_it2 = _active_rules.end();  // null
        this->set_overlap_policy(options::overlap::ABC);
#ifdef LIBSEMIGROUPS_VERBOSE
        _max_stack_depth        = 0;
        _max_word_length        = 0;
        _max_active_word_length = 0;
        _max_active_rules       = 0;
#endif
      }

      ~KnuthBendixImpl() {
        delete _overlap_measure;
        delete _tmp_word1;
        delete _tmp_word2;
        for (Rule const* rule : _active_rules) {
          delete const_cast<Rule*>(rule);
        }
        for (Rule* rule : _inactive_rules) {
          delete rule;
        }
        while (!_stack.empty()) {
          Rule* rule = _stack.top();
          _stack.pop();
          delete rule;
        }
      }

     private:
      //////////////////////////////////////////////////////////////////////////
      // KnuthBendixImpl - converting ints <-> string/char - private
      //////////////////////////////////////////////////////////////////////////

      static size_t internal_char_to_uint(internal_char_type c) {
#ifdef LIBSEMIGROUPS_DEBUG
        LIBSEMIGROUPS_ASSERT(c >= 97);
        return static_cast<size_t>(c - 97);
#else
        return static_cast<size_t>(c - 1);
#endif
      }

      static internal_char_type uint_to_internal_char(size_t a) {
        LIBSEMIGROUPS_ASSERT(
            a <= size_t(std::numeric_limits<internal_char_type>::max()));
#ifdef LIBSEMIGROUPS_DEBUG
        LIBSEMIGROUPS_ASSERT(
            a <= size_t(std::numeric_limits<internal_char_type>::max() - 97));
        return static_cast<internal_char_type>(a + 97);
#else
        return static_cast<internal_char_type>(a + 1);
#endif
      }

      static internal_string_type uint_to_internal_string(size_t i) {
        LIBSEMIGROUPS_ASSERT(
            i <= size_t(std::numeric_limits<internal_char_type>::max()));
        return internal_string_type({uint_to_internal_char(i)});
      }

      static word_type internal_string_to_word(internal_string_type const& s) {
        word_type w;
        w.reserve(s.size());
        for (internal_char_type const& c : s) {
          w.push_back(internal_char_to_uint(c));
        }
        return w;
      }

      static internal_string_type*
      word_to_internal_string(word_type const& w, internal_string_type* ww) {
        ww->clear();
        for (size_t const& a : w) {
          (*ww) += uint_to_internal_char(a);
        }
        return ww;
      }

      static internal_string_type word_to_internal_string(word_type const& u) {
        internal_string_type v;
        v.reserve(u.size());
        for (size_t const& l : u) {
          v += uint_to_internal_char(l);
        }
        return v;
      }

      internal_char_type external_to_internal_char(external_char_type c) const {
        LIBSEMIGROUPS_ASSERT(!_internal_is_same_as_external);
        return uint_to_internal_char(_kb->char_to_uint(c));
      }

      external_char_type internal_to_external_char(internal_char_type a) const {
        LIBSEMIGROUPS_ASSERT(!_internal_is_same_as_external);
        return _kb->uint_to_char(internal_char_to_uint(a));
      }

      void external_to_internal_string(external_string_type& w) const {
        if (_internal_is_same_as_external) {
          return;
        }
        for (auto& a : w) {
          a = external_to_internal_char(a);
        }
      }

      void internal_to_external_string(internal_string_type& w) const {
        if (_internal_is_same_as_external) {
          return;
        }
        for (auto& a : w) {
          a = internal_to_external_char(a);
        }
      }

     public:
      //////////////////////////////////////////////////////////////////////////
      // KnuthBendixImpl - methods for rules - public
      //////////////////////////////////////////////////////////////////////////

      void add_rule(std::string const& p, std::string const& q) {
        LIBSEMIGROUPS_ASSERT(p != q);
        auto pp = new external_string_type(p);
        auto qq = new external_string_type(q);
        external_to_internal_string(*pp);
        external_to_internal_string(*qq);
        push_stack(new_rule(pp, qq));
      }

      void add_rules(KnuthBendixImpl const* impl) {
        for (Rule const* rule : impl->_active_rules) {
          add_rule(new_rule(rule));
        }
      }

      std::vector<std::pair<std::string, std::string>> rules() const {
        std::vector<std::pair<external_string_type, external_string_type>>
            rules;
        rules.reserve(_active_rules.size());
        for (Rule const* rule : _active_rules) {
          internal_string_type lhs = internal_string_type(*rule->lhs());
          internal_string_type rhs = internal_string_type(*rule->rhs());
          internal_to_external_string(lhs);
          internal_to_external_string(rhs);
          rules.emplace_back(lhs, rhs);
        }
        std::sort(
            rules.begin(),
            rules.end(),
            [](std::pair<external_string_type, external_string_type> rule1,
               std::pair<external_string_type, external_string_type> rule2) {
              return shortlex_compare(rule1.first, rule2.first)
                     || (rule1.first == rule2.first
                         && shortlex_compare(rule1.second, rule2.second));
            });
        return rules;
      }

      size_t number_of_rules() const {
        return _active_rules.size();
      }

     private:
      //////////////////////////////////////////////////////////////////////////
      // KnuthBendixImpl - methods for rules - private
      //////////////////////////////////////////////////////////////////////////

      Rule* new_rule() const {
        ++_total_rules;
        Rule* rule;
        if (!_inactive_rules.empty()) {
          rule = _inactive_rules.front();
          rule->clear();
          rule->set_id(_total_rules);
          _inactive_rules.erase(_inactive_rules.begin());
        } else {
          rule = new Rule(this, _total_rules);
        }
        LIBSEMIGROUPS_ASSERT(!rule->active());
        return rule;
      }

      Rule* new_rule(internal_string_type* lhs,
                     internal_string_type* rhs) const {
        Rule* rule = new_rule();
        delete rule->_lhs;
        delete rule->_rhs;
        if (shortlex_compare(rhs, lhs)) {
          rule->_lhs = lhs;
          rule->_rhs = rhs;
        } else {
          rule->_lhs = rhs;
          rule->_rhs = lhs;
        }
        return rule;
      }

      Rule* new_rule(Rule const* rule1) const {
        Rule* rule2 = new_rule();
        rule2->_lhs->append(*rule1->lhs());  // copies lhs
        rule2->_rhs->append(*rule1->rhs());  // copies rhs
        return rule2;
      }

      Rule* new_rule(internal_string_type::const_iterator begin_lhs,
                     internal_string_type::const_iterator end_lhs,
                     internal_string_type::const_iterator begin_rhs,
                     internal_string_type::const_iterator end_rhs) const {
        Rule* rule = new_rule();
        rule->_lhs->append(begin_lhs, end_lhs);
        rule->_rhs->append(begin_rhs, end_rhs);
        return rule;
      }

      void add_rule(Rule* rule) {
        LIBSEMIGROUPS_ASSERT(*rule->lhs() != *rule->rhs());
#ifdef LIBSEMIGROUPS_VERBOSE
        _max_word_length  = std::max(_max_word_length, rule->lhs()->size());
        _max_active_rules = std::max(_max_active_rules, _active_rules.size());
        _unique_lhs_rules.insert(*rule->lhs());
#endif
        LIBSEMIGROUPS_ASSERT(_set_rules.emplace(RuleLookup(rule)).second);
#ifndef LIBSEMIGROUPS_DEBUG
        _set_rules.emplace(RuleLookup(rule));
#endif
        rule->activate();
        _active_rules.push_back(rule);
        if (_next_rule_it1 == _active_rules.end()) {
          --_next_rule_it1;
        }
        if (_next_rule_it2 == _active_rules.end()) {
          --_next_rule_it2;
        }
        _confluence_known = false;
        if (rule->lhs()->size() < _min_length_lhs_rule) {
          // TODO(later) this is not valid when using non-length reducing
          // orderings (such as RECURSIVE)
          _min_length_lhs_rule = rule->lhs()->size();
        }
        if (!_contains_empty_string) {
          _contains_empty_string = rule->lhs()->empty() || rule->rhs()->empty();
        }
        LIBSEMIGROUPS_ASSERT(_set_rules.size() == _active_rules.size());
      }

      std::list<Rule const*>::iterator
      remove_rule(std::list<Rule const*>::iterator it) {
#ifdef LIBSEMIGROUPS_VERBOSE
        _unique_lhs_rules.erase(*((*it)->lhs()));
#endif
        Rule* rule = const_cast<Rule*>(*it);
        rule->deactivate();
        if (it != _next_rule_it1 && it != _next_rule_it2) {
          it = _active_rules.erase(it);
        } else if (it == _next_rule_it1 && it != _next_rule_it2) {
          _next_rule_it1 = _active_rules.erase(it);
          it             = _next_rule_it1;
        } else if (it != _next_rule_it1 && it == _next_rule_it2) {
          _next_rule_it2 = _active_rules.erase(it);
          it             = _next_rule_it2;
        } else {
          _next_rule_it1 = _active_rules.erase(it);
          _next_rule_it2 = _next_rule_it1;
          it             = _next_rule_it1;
        }
#ifdef LIBSEMIGROUPS_DEBUG
        LIBSEMIGROUPS_ASSERT(_set_rules.erase(RuleLookup(rule)));
#else
        _set_rules.erase(RuleLookup(rule));
#endif
        LIBSEMIGROUPS_ASSERT(_set_rules.size() == _active_rules.size());
        return it;
      }

     public:
      bool contains_empty_string() const noexcept {
        return _contains_empty_string;
      }

      //////////////////////////////////////////////////////////////////////////
      // KnuthBendixImpl - other methods - public
      //////////////////////////////////////////////////////////////////////////

      external_string_type* rewrite(external_string_type* w) const {
        external_to_internal_string(*w);
        internal_rewrite(w);
        internal_to_external_string(*w);
        return w;
      }

      bool equal_to(external_string_type const& u,
                    external_string_type const& v) {
        if (u == v) {
          return true;
        }
        external_string_type uu = _kb->rewrite(u);
        external_string_type vv = _kb->rewrite(v);
        if (uu == vv) {
          return true;
        }
        knuth_bendix();
        external_to_internal_string(uu);
        external_to_internal_string(vv);
        internal_rewrite(&uu);
        internal_rewrite(&vv);
        return uu == vv;
      }

      void set_overlap_policy(options::overlap p) {
        if (p == _kb->_settings._overlap_policy
            && _overlap_measure != nullptr) {
          return;
        }
        delete _overlap_measure;
        switch (p) {
          case options::overlap::ABC:
            _overlap_measure = new ABC();
            break;
          case options::overlap::AB_BC:
            _overlap_measure = new AB_BC();
            break;
          case options::overlap::MAX_AB_BC:
            _overlap_measure = new MAX_AB_BC();
            break;
          default:
            LIBSEMIGROUPS_ASSERT(false);
        }
      }

      void set_internal_alphabet(std::string const& lphbt = "") {
        _internal_is_same_as_external = true;
        for (size_t i = 0; i < lphbt.size(); ++i) {
          if (uint_to_internal_char(i) != lphbt[i]) {
            _internal_is_same_as_external = false;
            return;
          }
        }
      }

     private:
      //////////////////////////////////////////////////////////////////////////
      // KnuthBendixImpl - other methods - private
      //////////////////////////////////////////////////////////////////////////
      // REWRITE_FROM_LEFT from Sims, p67
      // Caution: this uses the assumption that rules are length reducing, if it
      // is not, then u might not have sufficient space!
      void internal_rewrite(internal_string_type* u) const {
        if (u->size() < _min_length_lhs_rule) {
          return;
        }
        internal_string_type::iterator const& v_begin = u->begin();
        internal_string_type::iterator        v_end
            = u->begin() + _min_length_lhs_rule - 1;
        internal_string_type::iterator        w_begin = v_end;
        internal_string_type::iterator const& w_end   = u->end();

        RuleLookup lookup;

        while (w_begin != w_end) {
          *v_end = *w_begin;
          ++v_end;
          ++w_begin;

          auto it = _set_rules.find(lookup(v_begin, v_end));
          if (it != _set_rules.end()) {
            Rule const* rule = (*it).rule();
            if (rule->lhs()->size() <= static_cast<size_t>(v_end - v_begin)) {
              LIBSEMIGROUPS_ASSERT(detail::is_suffix(
                  v_begin, v_end, rule->lhs()->cbegin(), rule->lhs()->cend()));
              v_end -= rule->lhs()->size();
              w_begin -= rule->rhs()->size();
              detail::string_replace(
                  w_begin, rule->rhs()->cbegin(), rule->rhs()->cend());
            }
          }
          while (w_begin != w_end
                 && _min_length_lhs_rule - 1
                        > static_cast<size_t>((v_end - v_begin))) {
            *v_end = *w_begin;
            ++v_end;
            ++w_begin;
          }
        }
        u->erase(v_end - u->cbegin());
      }

      // TEST_2 from Sims, p76
      void clear_stack() {
        while (!_stack.empty() && !_kb->stopped()) {
#ifdef LIBSEMIGROUPS_VERBOSE
          _max_stack_depth = std::max(_max_stack_depth, _stack.size());
#endif

          Rule* rule1 = _stack.top();
          _stack.pop();
          LIBSEMIGROUPS_ASSERT(!rule1->active());
          LIBSEMIGROUPS_ASSERT(*rule1->lhs() != *rule1->rhs());
          // Rewrite both sides and reorder if necessary . . .
          rule1->rewrite();

          if (*rule1->lhs() != *rule1->rhs()) {
            internal_string_type const* lhs = rule1->lhs();
            for (auto it = _active_rules.begin(); it != _active_rules.end();) {
              Rule* rule2 = const_cast<Rule*>(*it);
              if (rule2->lhs()->find(*lhs) != external_string_type::npos) {
                it = remove_rule(it);
                LIBSEMIGROUPS_ASSERT(*rule2->lhs() != *rule2->rhs());
                // rule2 is added to _inactive_rules by clear_stack
                _stack.emplace(rule2);
              } else {
                if (rule2->rhs()->find(*lhs) != external_string_type::npos) {
                  internal_rewrite(rule2->rhs());
                }
                ++it;
              }
            }
            add_rule(rule1);
            // rule1 is activated, we do this after removing rules that rule1
            // makes redundant to avoid failing to insert rule1 in _set_rules
          } else {
            _inactive_rules.push_back(rule1);
          }
          if (_kb->report()) {
            REPORT_DEFAULT(
                "active rules = %d, inactive rules = %d, rules defined = "
                "%d\n",
                _active_rules.size(),
                _inactive_rules.size(),
                _total_rules);
            REPORT_VERBOSE_DEFAULT("max stack depth = %d\n"
                                   "max word length = %d\n"
                                   "max active word length = %d\n"
                                   "max active rules = %d\n"
                                   "number of unique lhs = %d\n",
                                   _max_stack_depth,
                                   _max_word_length,
                                   max_active_word_length(),
                                   _max_active_rules,
                                   _unique_lhs_rules.size());
          }
        }
      }
      // FIXME(later) there is a possibly infinite loop here clear_stack ->
      // push_stack -> clear_stack and so on
      void push_stack(Rule* rule) {
        LIBSEMIGROUPS_ASSERT(!rule->active());
        if (*rule->lhs() != *rule->rhs()) {
          _stack.emplace(rule);
          clear_stack();
        } else {
          _inactive_rules.push_back(rule);
        }
      }

      // OVERLAP_2 from Sims, p77
      void overlap(Rule const* u, Rule const* v) {
        LIBSEMIGROUPS_ASSERT(u->active() && v->active());
        auto limit
            = u->lhs()->cend() - std::min(u->lhs()->size(), v->lhs()->size());
        int64_t u_id = u->id();
        int64_t v_id = v->id();
        for (auto it = u->lhs()->cend() - 1;
             it > limit && u_id == u->id() && v_id == v->id() && !_kb->stopped()
             && (_kb->_settings._max_overlap == POSITIVE_INFINITY
                 || (*_overlap_measure)(u, v, it)
                        <= _kb->_settings._max_overlap);
             --it) {
          // Check if B = [it, u->lhs()->cend()) is a prefix of v->lhs()
          if (detail::is_prefix(
                  v->lhs()->cbegin(), v->lhs()->cend(), it, u->lhs()->cend())) {
            // u = P_i = AB -> Q_i and v = P_j = BC -> Q_j
            // This version of new_rule does not reorder
            Rule* rule = new_rule(u->lhs()->cbegin(),
                                  it,
                                  u->rhs()->cbegin(),
                                  u->rhs()->cend());  // rule = A -> Q_i
            rule->_lhs->append(*v->rhs());            // rule = AQ_j -> Q_i
            rule->_rhs->append(v->lhs()->cbegin() + (u->lhs()->cend() - it),
                               v->lhs()->cend());  // rule = AQ_j -> Q_iC
            // rule is reordered during rewriting in clear_stack
            push_stack(rule);
            // It can be that the iterator `it` is invalidated by the call to
            // push_stack (i.e. if `u` is deactivated, then rewritten, actually
            // changed, and reactivated) and that is the reason for the checks
            // in the for-loop above. If this is the case, then we should stop
            // considering the overlaps of u and v here, and note that they will
            // be considered later, because when the rule `u` is reactivated it
            // is added to the end of the active rules list.
          }
        }
      }

     public:
      //////////////////////////////////////////////////////////////////////////
      // KnuthBendixImpl - main methods - public
      //////////////////////////////////////////////////////////////////////////

      bool confluent_known() const noexcept {
        return _confluence_known;
      }

      bool confluent() const {
        if (!_stack.empty()) {
          return false;
        }
        if (!_confluence_known && (!_kb->running() || !_kb->stopped())) {
          LIBSEMIGROUPS_ASSERT(_stack.empty());
          _confluent        = true;
          _confluence_known = true;
          internal_string_type word1;
          internal_string_type word2;
          size_t               seen = 0;

          for (auto it1 = _active_rules.cbegin();
               it1 != _active_rules.cend()
               && (!_kb->running() || !_kb->stopped());
               ++it1) {
            Rule const* rule1 = *it1;
            // Seems to be much faster to do this in reverse.
            for (auto it2 = _active_rules.crbegin();
                 it2 != _active_rules.crend()
                 && (!_kb->running() || !_kb->stopped());
                 ++it2) {
              seen++;
              Rule const* rule2 = *it2;
              for (auto it = rule1->lhs()->cend() - 1;
                   it >= rule1->lhs()->cbegin()
                   && (!_kb->running() || !_kb->stopped());
                   --it) {
                // Find longest common prefix of suffix B of rule1.lhs() defined
                // by it and R = rule2.lhs()
                auto prefix
                    = detail::maximum_common_prefix(it,
                                                    rule1->lhs()->cend(),
                                                    rule2->lhs()->cbegin(),
                                                    rule2->lhs()->cend());
                if (prefix.first == rule1->lhs()->cend()
                    || prefix.second == rule2->lhs()->cend()) {
                  word1.clear();
                  word1.append(rule1->lhs()->cbegin(), it);          // A
                  word1.append(*rule2->rhs());                       // S
                  word1.append(prefix.first, rule1->lhs()->cend());  // D

                  word2.clear();
                  word2.append(*rule1->rhs());                        // Q
                  word2.append(prefix.second, rule2->lhs()->cend());  // E

                  if (word1 != word2) {
                    internal_rewrite(&word1);
                    internal_rewrite(&word2);
                    if (word1 != word2) {
                      _confluent = false;
                      return _confluent;
                    }
                  }
                }
              }
            }
            if (_kb->report()) {
              REPORT_DEFAULT("checked %llu pairs of overlaps out of %llu\n",
                             uint64_t(seen),
                             uint64_t(_active_rules.size())
                                 * uint64_t(_active_rules.size()));
            }
          }
          if (_kb->running() && _kb->stopped()) {
            _confluence_known = false;
          }
        }
        return _confluent;
      }

      // KBS_2 from Sims, p77-78
      bool knuth_bendix() {
        detail::Timer timer;
        if (_stack.empty() && confluent() && !_kb->stopped()) {
          // _stack can be non-empty if non-reduced rules were used to define
          // the KnuthBendix.  If _stack is non-empty, then it means that the
          // rules in _active_rules might not define the system.
          REPORT_DEFAULT("the system is confluent already\n");
          return true;
        } else if (_active_rules.size() >= _kb->_settings._max_rules) {
          REPORT_DEFAULT("too many rules\n");
          return false;
        }
        // Reduce the rules
        _next_rule_it1 = _active_rules.begin();
        while (_next_rule_it1 != _active_rules.end() && !_kb->stopped()) {
          // Copy *_next_rule_it1 and push_stack so that it is not modified by
          // the call to clear_stack.
          LIBSEMIGROUPS_ASSERT((*_next_rule_it1)->lhs()
                               != (*_next_rule_it1)->rhs());
          push_stack(new_rule(*_next_rule_it1));
          ++_next_rule_it1;
        }
        _next_rule_it1 = _active_rules.begin();
        size_t nr      = 0;
        while (_next_rule_it1 != _active_rules.cend()
               && _active_rules.size() < _kb->_settings._max_rules
               && !_kb->stopped()) {
          Rule const* rule1 = *_next_rule_it1;
          _next_rule_it2    = _next_rule_it1;
          ++_next_rule_it1;
          overlap(rule1, rule1);
          while (_next_rule_it2 != _active_rules.begin() && rule1->active()) {
            --_next_rule_it2;
            Rule const* rule2 = *_next_rule_it2;
            overlap(rule1, rule2);
            ++nr;
            if (rule1->active() && rule2->active()) {
              ++nr;
              overlap(rule2, rule1);
            }
          }
          if (nr > _kb->_settings._check_confluence_interval) {
            if (confluent()) {
              break;
            }
            nr = 0;
          }
          if (_next_rule_it1 == _active_rules.cend()) {
            clear_stack();
          }
        }
        // LIBSEMIGROUPS_ASSERT(_stack.empty());
        // Seems that the stack can be non-empty here in KnuthBendix 12, 14, 16
        // and maybe more
        bool ret;
        if (_kb->_settings._max_overlap == POSITIVE_INFINITY
            && _kb->_settings._max_rules == POSITIVE_INFINITY
            && !_kb->stopped()) {
          _confluence_known = true;
          _confluent        = true;
          for (Rule* rule : _inactive_rules) {
            delete rule;
          }
          _inactive_rules.clear();
          ret = true;
        } else {
          ret = false;
        }

        REPORT_DEFAULT("stopping with active rules = %d, inactive rules = %d, "
                       "rules defined = %d\n",
                       _active_rules.size(),
                       _inactive_rules.size(),
                       _total_rules);
        REPORT_VERBOSE_DEFAULT("max stack depth = %d", _max_stack_depth);
        REPORT_TIME(timer);
        return ret;
      }

      void knuth_bendix_by_overlap_length() {
        detail::Timer timer;
        size_t        max_overlap = _kb->_settings._max_overlap;
        size_t        check_confluence_interval
            = _kb->_settings._check_confluence_interval;
        _kb->_settings._max_overlap               = 1;
        _kb->_settings._check_confluence_interval = POSITIVE_INFINITY;
        while (!_kb->stopped() && !confluent()) {
          knuth_bendix();
          _kb->_settings._max_overlap++;
        }
        _kb->_settings._max_overlap               = max_overlap;
        _kb->_settings._check_confluence_interval = check_confluence_interval;
        REPORT_TIME(timer);
      }

     private:
      ////////////////////////////////////////////////////////////////////////
      // KnuthBendixImpl - iterators - private
      ////////////////////////////////////////////////////////////////////////

      using external_rule_type
          = std::pair<external_string_type, external_string_type>;

      struct IteratorMethods {
        external_rule_type
        indirection(KnuthBendixImpl*                       kbi,
                    std::list<Rule const*>::const_iterator it) const {
          auto lhs = std::string(*(*it)->lhs());
          auto rhs = std::string(*(*it)->rhs());
          kbi->internal_to_external_string(lhs);
          kbi->internal_to_external_string(rhs);

          return std::make_pair(lhs, rhs);
        }

        // Not defined!
        external_rule_type const*
        addressof(KnuthBendixImpl*,
                  std::list<Rule const*>::const_iterator) const {
          return nullptr;
        }
      };

     public:
      ////////////////////////////////////////////////////////////////////////
      // KnuthBendixImpl - iterators - public
      ////////////////////////////////////////////////////////////////////////

      /*using const_iterator = detail::ConstIteratorStateful<
          KnuthBendixImpl const*,                  // state
          IteratorMethods,                        // methods
          std::list<Rule const*>::const_iterator,  // wrapped iterator
          external_rule_type,                      // external value type
          external_rule_type,                      // external const pointer
          external_rule_type&&                     // external const reference
          >;

      const_iterator cbegin_active_rules() const {
        return const_iterator(this, _active_rules.cbegin());
      }

      const_iterator cend_active_rules() const {
        return const_iterator(this, _active_rules.cend());
      }*/

     private:
      ////////////////////////////////////////////////////////////////////////
      // KnuthBendixImpl - data - private
      ////////////////////////////////////////////////////////////////////////

      std::list<Rule const*>           _active_rules;
      mutable std::atomic<bool>        _confluent;
      mutable std::atomic<bool>        _confluence_known;
      mutable std::list<Rule*>         _inactive_rules;
      bool                             _internal_is_same_as_external;
      bool                             _contains_empty_string;
      KnuthBendix*                     _kb;
      size_t                           _min_length_lhs_rule;
      std::list<Rule const*>::iterator _next_rule_it1;
      std::list<Rule const*>::iterator _next_rule_it2;
      OverlapMeasure*                  _overlap_measure;
      std::set<RuleLookup>             _set_rules;
      std::stack<Rule*>                _stack;
      internal_string_type*            _tmp_word1;
      internal_string_type*            _tmp_word2;
      mutable size_t                   _total_rules;

#ifdef LIBSEMIGROUPS_VERBOSE
      //////////////////////////////////////////////////////////////////////////
      // ./configure --enable-verbose functions
      //////////////////////////////////////////////////////////////////////////

      size_t max_active_word_length() {
        auto comp = [](Rule const* p, Rule const* q) -> bool {
          return p->lhs()->size() < q->lhs()->size();
        };
        auto max = std::max_element(
            _active_rules.cbegin(), _active_rules.cend(), comp);
        if (max != _active_rules.cend()) {
          _max_active_word_length
              = std::max(_max_active_word_length, (*max)->lhs()->size());
        }
        return _max_active_word_length;
      }
      size_t                                   _max_stack_depth;
      size_t                                   _max_word_length;
      size_t                                   _max_active_word_length;
      size_t                                   _max_active_rules;
      std::unordered_set<internal_string_type> _unique_lhs_rules;
#endif
    };  // struct KnuthBendixImpl
  }     // namespace fpsemigroup
}  // namespace libsemigroups
#endif  // LIBSEMIGROUPS_SRC_KNUTH_BENDIX_IMPL_HPP_

quality86%

¤ Dauer der Verarbeitung: 0.26 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.