rws.h

//
// libsemigroups - C++ library for semigroups and monoids
// Copyright (C) 2017 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/>.
//

#ifndef LIBSEMIGROUPS_SRC_RWS_H_
#define LIBSEMIGROUPS_SRC_RWS_H_

#include <atomic>
#include <list>
#include <stack>
#include <string>
#include <utility>
#include <vector>

#include "cong.h"
#include "semigroups.h"

namespace libsemigroups {
  typedef char rws_letter_t;

  typedef std::string rws_word_t;

  class ReductionOrdering {
   public:
    explicit ReductionOrdering(
        std::function<bool(rws_word_t const*, rws_word_t const*)> func)
        : _func(func) {}

    size_t operator()(rws_word_t const* p, rws_word_t const* q) const {
      return _func(p, q);
    }

    size_t operator()(rws_word_t const& p, rws_word_t const& q) const {
      return _func(&p, &q);
    }

   private:
    std::function<bool(rws_word_t const*, rws_word_t const*)> _func;
  };

  class SHORTLEX : public ReductionOrdering {
   public:
    SHORTLEX()
        : ReductionOrdering([](rws_word_t const* p, rws_word_t const* q) {
            return (p->size() > q->size()
                    || (p->size() == q->size() && *p > *q));
          }) {}

    explicit SHORTLEX(std::function<bool(rws_letter_t const&,
                                         rws_letter_t const&)> letter_order)
        : ReductionOrdering([this](rws_word_t const* p, rws_word_t const* q) {
            // FIXME This is unsafe since we don't check that p and q consist of
            // the correct letters
            if (p->size() > q->size()) {
              return true;
            } else if (p->size() < q->size()) {
              return false;
            }
            auto itp = p->cbegin();
            auto itq = q->cbegin();
            while (itp < p->cend() && *itp == *itq) {
              itp++;
              itq++;
            }
            return (itp != p->cend() && this->_letter_order(*itp, *itq));
          }),
          _letter_order(letter_order) {}

   private:
    std::function<bool(rws_letter_t const&, rws_letter_t const&)> _letter_order;
  };

  // TODO add more reduction orderings


  class RWS {
   public:
    // Forward declaration of Rule
    class Rule;

    explicit RWS(ReductionOrdering* order)
        : _active_rules(),
          _confluence_known(false),
          _inactive_rules(),
          _is_confluent(),
          _order(order),
          _report_next(0),
          _report_interval(1000),
          _stack(),
          _total_rules(0) {
      _next_rule_it1 = _active_rules.end();  // null
      _next_rule_it2 = _active_rules.end();  // null
#ifdef LIBSEMIGROUPS_STATS
      _max_stack_depth        = 0;
      _max_word_length        = 0;
      _max_active_word_length = 0;
      _max_active_rules       = 0;
#endif
    }

    RWS() : RWS(new SHORTLEX()) {}

    explicit RWS(std::vector<relation_t> const& relations) : RWS() {
      add_rules(relations);
    }

    RWS(ReductionOrdering* order, std::vector<relation_t> const& relations)
        : RWS(order) {
      add_rules(relations);
    }

    explicit RWS(Congruence& cong) : RWS() {
      add_rules(cong);
    }

    ~RWS();

    bool is_confluent() const {
      std::atomic<bool> killed(false);
      return is_confluent(killed);
    }

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

    void rewrite(rws_word_t* w) const;

    rws_word_t rewrite(rws_word_t w) const {
      rewrite(&w);
      return w;
    }

    void knuth_bendix() {
      std::atomic<bool> killed(false);
      knuth_bendix(killed);
    }

    void knuth_bendix(std::atomic<bool>& killed);

    void set_confluent(bool val) {
      _is_confluent     = val;
      _confluence_known = true;
    }

    void add_rule(rws_word_t* p, rws_word_t* q);

    void add_rule(rws_word_t const& p, rws_word_t const& q);

    void add_rules(std::vector<relation_t> const& relations) {
      for (relation_t const& rel : relations) {
        if (rel.first != rel.second) {
          add_rule(word_to_rws_word(rel.first), word_to_rws_word(rel.second));
        }
      }
    }

    void add_rules(Congruence& cong) {
      add_rules(cong.relations());
      add_rules(cong.extra());
    }

    static rws_letter_t letter_to_rws_letter(letter_t const& a);

    static rws_word_t* letter_to_rws_word(letter_t const& a);

    static rws_word_t* word_to_rws_word(word_t const& w);

    static letter_t rws_letter_to_letter(rws_letter_t const& rws_letter);

    static word_t* rws_word_to_word(rws_word_t const* rws_word);

    void set_report(bool val) const {
      glob_reporter.set_report(val);
    }

    bool test_less_than(word_t const& p, word_t const& q);

    bool test_less_than(rws_word_t const& p, rws_word_t const& q);

    bool test_equals(word_t const& p, word_t const& q);

    bool test_equals(rws_word_t const& p, rws_word_t const& q);

    std::list<Rule const*>::const_iterator rules_cbegin() const {
      return _active_rules.cbegin();
    }

    std::list<Rule const*>::const_iterator rules_cend() const {
      return _active_rules.cend();
    }

   private:
    // internal only, rewrites in-place and deletes p and q.
    bool test(rws_word_t* p,
              rws_word_t* q,
              std::function<bool(rws_word_t* p, rws_word_t* q)> func) {
      knuth_bendix();
      rewrite(p);
      rewrite(q);
      bool out = func(q, p);
      delete p;
      delete q;
      return out;
    }

    void add_rule(Rule* rule);
    std::list<Rule const*>::iterator
    remove_rule(std::list<Rule const*>::iterator it);

    Rule* new_rule() const;
    Rule* new_rule(rws_word_t const* lhs, rws_word_t const* rhs) const;
    Rule* new_rule(Rule const* rule) const;
    Rule* new_rule(rws_word_t::const_iterator begin_lhs,
                   rws_word_t::const_iterator end_lhs,
                   rws_word_t::const_iterator begin_rhs,
                   rws_word_t::const_iterator end_rhs) const;

    bool is_confluent(std::atomic<bool>& killed) const;
    void clear_stack(std::atomic<bool>& killed);
    void overlap(Rule const* u, Rule const* v, std::atomic<bool>& killed);

    std::list<Rule const*>           _active_rules;
    mutable bool                     _confluence_known;
    mutable std::list<Rule*>         _inactive_rules;
    mutable bool                     _is_confluent;
    std::list<Rule const*>::iterator _next_rule_it1;
    std::list<Rule const*>::iterator _next_rule_it2;
    ReductionOrdering const*         _order;
    size_t                           _report_next;
    size_t                           _report_interval;
    std::stack<Rule*>                _stack;
    mutable size_t                   _total_rules;

#ifdef LIBSEMIGROUPS_STATS
    size_t                         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<rws_word_t> _unique_lhs_rules;
#endif
  };

  class RWS::Rule {
    friend RWS;

   public:
    rws_word_t const* lhs() const {
      return const_cast<rws_word_t const*>(_lhs);
    }

    rws_word_t const* rhs() const {
      return const_cast<rws_word_t const*>(_rhs);
    }

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

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

    // Construct from RWS, and pointers to libsemigroups::rws_word_t.
    //
    // A rule is guaranteed to have its left hand side greater than its right
    // hand side according to the reduction ordering of \p rws. The Rule
    // object constructed here takes ownership of \p p and \p q and deletes
    // them in its destructor.
    Rule(RWS const* rws, rws_word_t* p, rws_word_t* q)
        : _rws(rws), _lhs(p), _rhs(q), _active(false) {
      LIBSEMIGROUPS_ASSERT(*_lhs != *_rhs);
      reorder();
    }

    // Construct from RWS with new but empty rws_word_t's
    explicit Rule(RWS const* rws)
        : _rws(rws),
          _lhs(new rws_word_t()),
          _rhs(new rws_word_t()),
          _active(false) {}

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

    void rewrite() {
      _rws->rewrite(_lhs);
      _rws->rewrite(_rhs);
      reorder();
    }

    void rewrite_rhs() {
      _rws->rewrite(_rhs);
    }

    void clear() {
      _lhs->clear();
      _rhs->clear();
    }

    inline bool is_active() const {
      return _active;
    }

    void deactivate() {
      _active = false;
    }

    void activate() {
      _active = true;
    }

    void reorder() {
      if ((*(_rws->_order))(_rhs, _lhs)) {
        std::swap(_lhs, _rhs);
      }
    }

    RWS const*  _rws;
    rws_word_t* _lhs;
    rws_word_t* _rhs;
    bool        _active;
  };

}  // namespace libsemigroups
#endif  // LIBSEMIGROUPS_SRC_RWS_H_