libsemigroups
rws.h
1 //
2 // libsemigroups - C++ library for semigroups and monoids
3 // Copyright (C) 2017 James D. Mitchell
4 //
5 // This program is free software: you can redistribute it and/or modify
6 // it under the terms of the GNU General Public License as published by
7 // the Free Software Foundation, either version 3 of the License, or
8 // (at your option) any later version.
9 //
10 // This program is distributed in the hope that it will be useful,
11 // but WITHOUT ANY WARRANTY; without even the implied warranty of
12 // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 // GNU General Public License for more details.
14 //
15 // You should have received a copy of the GNU General Public License
16 // along with this program. If not, see <http://www.gnu.org/licenses/>.
17 //
18 
19 #ifndef LIBSEMIGROUPS_SRC_RWS_H_
20 #define LIBSEMIGROUPS_SRC_RWS_H_
21 
22 #include <atomic>
23 #include <list>
24 #include <set>
25 #include <stack>
26 #include <string>
27 #include <utility>
28 #include <vector>
29 
30 #include "cong.h"
31 #include "semigroups.h"
32 
33 namespace libsemigroups {
34 
44  public:
52  std::function<bool(std::string const*, std::string const*)> func)
53  : _func(func) {}
54 
57  size_t operator()(std::string const* p, std::string const* q) const {
58  return _func(p, q);
59  }
60 
63  size_t operator()(std::string const& p, std::string const& q) const {
64  return _func(&p, &q);
65  }
66 
67  private:
68  std::function<bool(std::string const*, std::string const*)> _func;
69  };
70 
73  class SHORTLEX : public ReductionOrdering {
74  public:
78  : ReductionOrdering([](std::string const* p, std::string const* q) {
79  return (p->size() > q->size()
80  || (p->size() == q->size() && *p > *q));
81  }) {}
82  };
83 
84  // The ordering used here is recursive path ordering (based on
85  // that described in the book "Confluent String Rewriting" by Matthias
86  // Jantzen, Defn 1.2.14, page 24).
87  //
88  // The ordering is as follows:
89  // let u, v be elements of X* u >= v iff one of the following conditions is
90  // fulfilled;
91  // 1) u = v
92  // OR
93  // u = u'a, v = v'b for some a,b elements of X, u',v' elements of X* and then:
94  // 2) a = b and u' >= v'
95  // OR
96  // 3) a > b and u > v'
97  // OR
98  // 4) b > a and u'> v
99  //
100  // 1 or 0 = false
101  // 2 = true
102  /*class RECURSIVE : public ReductionOrdering {
103  public:
104  RECURSIVE()
105  : ReductionOrdering([](std::string const* Q, std::string const* P) {
106  bool lastmoved = false;
107  auto it_P = P->crbegin();
108  auto it_Q = Q->crbegin();
109  while (true) {
110  if (it_P == P->crend()) {
111  return (it_Q == Q->crend() ? lastmoved : true);
112  } else if (it_Q == Q->crend()) {
113  return false;
114  }
115  if (*it_P == *it_Q) {
116  ++it_P;
117  ++it_Q;
118  } else if (*it_P < *it_Q) {
119  ++it_P;
120  lastmoved = false;
121  } else {
122  ++it_Q;
123  lastmoved = true;
124  }
125  }
126  }) {}
127  };*/
128 
129  // TODO add more reduction orderings
130 
134 
135  class RWS {
136  // Forward declarations
137  struct Rule;
138  class RuleLookup;
139  struct OverlapMeasure;
140  friend Rule;
141 
142  public:
144  typedef char rws_letter_t;
145 
147  typedef std::string rws_word_t;
148 
157  enum overlap_measure { ABC = 0, AB_BC = 1, max_AB_BC = 2 };
158 
165  explicit RWS(ReductionOrdering* order,
166  std::string alphabet = STANDARD_ALPHABET)
167  : _active_rules(),
168  _alphabet(alphabet),
169  _check_confluence_interval(4096),
170  // _clear_stack_interval(0),
171  _confluence_known(false),
172  _inactive_rules(),
173  _confluent(false),
174  _max_overlap(UNBOUNDED),
175  _max_rules(UNBOUNDED),
176  _min_length_lhs_rule(std::numeric_limits<size_t>::max()),
177  _order(order),
178  _overlap_measure(nullptr),
179  _report_next(0),
180  _report_interval(1000),
181  _stack(),
182  _tmp_word1(new rws_word_t()),
183  _tmp_word2(new rws_word_t()),
184  _total_rules(0) {
185  _next_rule_it1 = _active_rules.end(); // null
186  _next_rule_it2 = _active_rules.end(); // null
187  set_overlap_measure(overlap_measure::ABC);
188  if (_alphabet != STANDARD_ALPHABET) {
189  if (std::is_sorted(_alphabet.cbegin(), _alphabet.cend())) {
190  _alphabet = STANDARD_ALPHABET;
191  } else {
192  for (size_t i = 0; i < _alphabet.size(); ++i) {
193  _alphabet_map.emplace(
194  std::make_pair(_alphabet[i], uint_to_rws_letter(i)));
195  }
196  }
197  }
198 #ifdef LIBSEMIGROUPS_STATS
199  _max_stack_depth = 0;
200  _max_word_length = 0;
201  _max_active_word_length = 0;
202  _max_active_rules = 0;
203 #endif
204  }
205 
208  RWS() : RWS(new SHORTLEX(), STANDARD_ALPHABET) {}
209 
213  // Apparently old versions of GCC (4.8.2) don't like explicit constructors
214  // with single default parameters:
215  // https://gcc.gnu.org/bugzilla/show_bug.cgi?id=60367
216  // and so we have two constructors instead.
217  explicit RWS(std::string alphabet) : RWS(new SHORTLEX(), alphabet) {}
218 
221  explicit RWS(std::vector<relation_t> const& relations) : RWS() {
222  add_rules(relations);
223  }
224 
230  RWS(ReductionOrdering* order, std::vector<relation_t> const& relations)
231  : RWS(order) {
232  add_rules(relations);
233  }
234 
241  explicit RWS(Congruence& cong) : RWS() {
242  add_rules(cong);
243  }
244 
249  ~RWS();
250 
254  friend std::ostream& operator<<(std::ostream& os, RWS const& rws);
255 
259  bool confluent() const {
260  std::atomic<bool> killed(false);
261  return confluent(killed);
262  }
263 
265  size_t nr_rules() const { // FIXME should this be nrrules?
266  return _active_rules.size();
267  }
268 
271  std::string* rewrite(std::string* w) const {
272  string_to_rws_word(*w);
273  internal_rewrite(w);
274  rws_word_to_string(*w);
275  return w;
276  }
277 
280  std::string rewrite(std::string w) const {
281  rewrite(&w);
282  return w;
283  }
284 
291  void knuth_bendix() {
292  std::atomic<bool> killed(false);
293  knuth_bendix(killed);
294  }
295 
305  void knuth_bendix(std::atomic<bool>& killed);
306 
315  // TODO a version that also accepts killed.
317  Timer timer;
318  size_t max_overlap = _max_overlap;
319  size_t check_confluence_interval = _check_confluence_interval;
320  _max_overlap = 1;
321  _check_confluence_interval = UNBOUNDED;
322  std::atomic<bool> killed(false);
323  while (!confluent()) {
324  knuth_bendix(killed);
325  _max_overlap++;
326  }
327  _max_overlap = max_overlap;
328  _check_confluence_interval = check_confluence_interval;
329  REPORT("elapsed time = " << timer);
330  }
331 
339  void add_rule(std::string const& p, std::string const& q);
340 
345  void add_rules(std::vector<relation_t> const& relations);
346 
349  void add_rules(Congruence& cong) {
350  add_rules(cong.relations());
351  add_rules(cong.extra());
352  }
353 
357  // TODO remove this
358  bool rule(std::string p, std::string q) const;
359 
366  std::vector<std::pair<std::string, std::string>> rules() const;
367 
372  void set_report(bool val) const {
373  glob_reporter.set_report(val);
374  }
375 
382  void set_report_interval(size_t interval) {
383  _report_interval = interval;
384  }
385 
397  void set_check_confluence_interval(size_t interval) {
398  if (interval > UNBOUNDED) {
399  interval = UNBOUNDED;
400  }
401  _check_confluence_interval = interval;
402  }
403 
404  // This is temporarily disabled, and may be deleted altogether in the
405  // future.
406  // void set_clear_stack_interval(size_t interval) {
407  // _clear_stack_interval = interval;
408  // }
409 
418  void set_max_overlap(size_t val) {
419  if (val > UNBOUNDED) {
420  val = UNBOUNDED;
421  }
422  _max_overlap = val;
423  }
424 
431  void set_max_rules(size_t val) {
432  _max_rules = val;
433  }
434 
439  void set_overlap_measure(overlap_measure measure);
440 
449  bool test_less_than(word_t const& p, word_t const& q);
450 
459  bool test_less_than(std::string const& p, std::string const& q);
460 
472  bool test_less_than(std::string* p, std::string* q);
473 
482  bool test_equals(word_t const& p, word_t const& q);
483 
492  bool test_equals(std::initializer_list<size_t> const& p,
493  std::initializer_list<size_t> const& q);
494 
502  bool test_equals(std::string const& p, std::string const& q);
503 
514  bool test_equals(std::string* p, std::string* q);
515 
520  static size_t const UNBOUNDED = static_cast<size_t>(-2);
521 
525  static inline rws_word_t* uint_to_rws_word(size_t const& a) {
526  return new rws_word_t(1, uint_to_rws_letter(a));
527  }
528 
531  static word_t* rws_word_to_word(rws_word_t const* rws_word) {
532  word_t* w = new word_t();
533  w->reserve(rws_word->size());
534  for (rws_letter_t const& rws_letter : *rws_word) {
535  w->push_back(rws_letter_to_uint(rws_letter));
536  }
537  return w;
538  }
539 
546  static rws_word_t* word_to_rws_word(word_t const& w, rws_word_t* ww) {
547  ww->clear();
548  for (size_t const& a : w) {
549  (*ww) += uint_to_rws_letter(a);
550  }
551  return ww;
552  }
553 
559  static inline rws_word_t* word_to_rws_word(word_t const& w) {
560  rws_word_t* ww = new rws_word_t();
561  return word_to_rws_word(w, ww);
562  }
563 
564  private:
565  static inline size_t rws_letter_to_uint(rws_letter_t const& rws_letter) {
566 #ifdef LIBSEMIGROUPS_DEBUG
567  return static_cast<size_t>(rws_letter - 97);
568 #else
569  return static_cast<size_t>(rws_letter - 1);
570 #endif
571  }
572 
573  static inline rws_letter_t uint_to_rws_letter(size_t const& a) {
574 #ifdef LIBSEMIGROUPS_DEBUG
575  return static_cast<rws_letter_t>(a + 97);
576 #else
577  return static_cast<rws_letter_t>(a + 1);
578 #endif
579  }
580 
581  inline rws_letter_t char_to_rws_letter(char a) const {
582  LIBSEMIGROUPS_ASSERT(_alphabet != STANDARD_ALPHABET);
583  LIBSEMIGROUPS_ASSERT(_alphabet_map.find(a) != _alphabet_map.end());
584  return (*_alphabet_map.find(a)).second;
585  }
586 
587  inline char rws_letter_to_char(rws_letter_t a) const {
588  LIBSEMIGROUPS_ASSERT(_alphabet != STANDARD_ALPHABET);
589  LIBSEMIGROUPS_ASSERT(rws_letter_to_uint(a) < _alphabet.size());
590  return _alphabet[rws_letter_to_uint(a)];
591  }
592 
593  inline void string_to_rws_word(std::string& w) const {
594  if (_alphabet == STANDARD_ALPHABET) {
595  return;
596  }
597  for (auto& a : w) {
598  a = char_to_rws_letter(a);
599  }
600  }
601 
602  inline void rws_word_to_string(rws_word_t& w) const {
603  if (_alphabet == STANDARD_ALPHABET) {
604  return;
605  }
606  for (auto& a : w) {
607  a = rws_letter_to_char(a);
608  }
609  }
610 
611  static std::string const STANDARD_ALPHABET;
612 
613  void add_rule(Rule* rule);
614  std::list<Rule const*>::iterator
615  remove_rule(std::list<Rule const*>::iterator it);
616 
617  Rule* new_rule() const;
618  Rule* new_rule(rws_word_t* lhs, rws_word_t* rhs) const;
619  Rule* new_rule(Rule const* rule) const;
620  Rule* new_rule(rws_word_t::const_iterator begin_lhs,
621  rws_word_t::const_iterator end_lhs,
622  rws_word_t::const_iterator begin_rhs,
623  rws_word_t::const_iterator end_rhs) const;
624 
625  // Rewrites the word pointed to by \p w in-place according to the current
626  // rules in the rewriting system.
627  void internal_rewrite(rws_word_t* w) const;
628 
629  bool confluent(std::atomic<bool>& killed) const;
630  void clear_stack(std::atomic<bool>& killed);
631  void push_stack(Rule* rule);
632  void push_stack(Rule* rule, std::atomic<bool>& killed);
633  void overlap(Rule const* u, Rule const* v, std::atomic<bool>& killed);
634  std::list<Rule const*> _active_rules;
635  std::string _alphabet;
636  std::unordered_map<char, rws_letter_t> _alphabet_map;
637  size_t _check_confluence_interval;
638  // size_t _clear_stack_interval;
639  mutable std::atomic<bool> _confluence_known;
640  mutable std::list<Rule*> _inactive_rules;
641  mutable std::atomic<bool> _confluent;
642  size_t _max_overlap;
643  size_t _max_rules;
644  size_t _min_length_lhs_rule;
645  std::list<Rule const*>::iterator _next_rule_it1;
646  std::list<Rule const*>::iterator _next_rule_it2;
647  ReductionOrdering const* _order;
648  OverlapMeasure* _overlap_measure;
649  size_t _report_next;
650  size_t _report_interval;
651  std::set<RuleLookup> _set_rules;
652  std::stack<Rule*> _stack;
653  rws_word_t* _tmp_word1;
654  rws_word_t* _tmp_word2;
655  mutable size_t _total_rules;
656 
657 #ifdef LIBSEMIGROUPS_STATS
658  size_t max_active_word_length();
659  size_t _max_stack_depth;
660  size_t _max_word_length;
661  size_t _max_active_word_length;
662  size_t _max_active_rules;
663  std::unordered_set<rws_word_t> _unique_lhs_rules;
664 #endif
665  };
666 
667  // Class for rules in rewriting systems, which supports only two methods,
668  // Rule::lhs and Rule::rhs, which return the left and right hand sides of
669  // the rule.
670  struct RWS::Rule {
671  friend std::ostream& operator<<(std::ostream& os, Rule const& rule) {
672  os << rule.rws_word_to_string(rule.lhs()) << " -> "
673  << rule.rws_word_to_string(rule.rhs());
674  return os;
675  }
676 
677  std::string rws_word_to_string(rws_word_t const* word) const {
678  std::string str(*word);
679  _rws->rws_word_to_string(str);
680  return str;
681  }
682 
683  // Returns the left hand side of the rule, which is guaranteed to be
684  // greater than its right hand side according to the reduction ordering of
685  // the RWS used to construct this.
686  rws_word_t const* lhs() const {
687  return const_cast<rws_word_t const*>(_lhs);
688  }
689 
690  // Returns the right hand side of the rule, which is guaranteed to be
691  // less than its left hand side according to the reduction ordering of
692  // the RWS used to construct this.
693  rws_word_t const* rhs() const {
694  return const_cast<rws_word_t const*>(_rhs);
695  }
696 
697  // The Rule class does not support an assignment contructor to avoid
698  // accidental copying.
699  Rule& operator=(Rule const& copy) = delete;
700 
701  // The Rule class does not support a copy contructor to avoid
702  // accidental copying.
703  Rule(Rule const& copy) = delete;
704 
705  // Construct from RWS with new but empty rws_word_t's
706  explicit Rule(RWS const* rws, int64_t id)
707  : _rws(rws),
708  _lhs(new rws_word_t()),
709  _rhs(new rws_word_t()),
710  _id(-1 * id) {
711  LIBSEMIGROUPS_ASSERT(_id < 0);
712  }
713 
714  // Destructor, deletes pointers used to create the rule.
715  ~Rule() {
716  delete _lhs;
717  delete _rhs;
718  }
719 
720  void rewrite() {
721  LIBSEMIGROUPS_ASSERT(_id != 0);
722  _rws->internal_rewrite(_lhs);
723  _rws->internal_rewrite(_rhs);
724  reorder();
725  }
726 
727  void rewrite_rhs() {
728  LIBSEMIGROUPS_ASSERT(_id != 0);
729  _rws->internal_rewrite(_rhs);
730  }
731 
732  void clear() {
733  LIBSEMIGROUPS_ASSERT(_id != 0);
734  _lhs->clear();
735  _rhs->clear();
736  }
737 
738  inline bool active() const {
739  LIBSEMIGROUPS_ASSERT(_id != 0);
740  return (_id > 0);
741  }
742 
743  void deactivate() {
744  LIBSEMIGROUPS_ASSERT(_id != 0);
745  if (active()) {
746  _id *= -1;
747  }
748  }
749 
750  void activate() {
751  LIBSEMIGROUPS_ASSERT(_id != 0);
752  if (!active()) {
753  _id *= -1;
754  }
755  }
756 
757  void set_id(int64_t id) {
758  LIBSEMIGROUPS_ASSERT(id > 0);
759  LIBSEMIGROUPS_ASSERT(!active());
760  _id = -1 * id;
761  }
762 
763  int64_t id() const {
764  LIBSEMIGROUPS_ASSERT(_id != 0);
765  return _id;
766  }
767 
768  void reorder() {
769  if ((*(_rws->_order))(_rhs, _lhs)) {
770  std::swap(_lhs, _rhs);
771  }
772  }
773 
774  RWS const* _rws;
775  rws_word_t* _lhs;
776  rws_word_t* _rhs;
777  int64_t _id;
778  };
779 
780  // Simple class wrapping a two iterators to an rws_word_t and a Rule const*
781  class RWS::RuleLookup {
782  public:
783  RuleLookup() : _rule(nullptr) {}
784 
785  explicit RuleLookup(RWS::Rule* rule)
786  : _first(rule->lhs()->cbegin()),
787  _last(rule->lhs()->cend()),
788  _rule(rule) {}
789 
790  RuleLookup& operator()(rws_word_t::iterator const& first,
791  rws_word_t::iterator const& last) {
792  _first = first;
793  _last = last;
794  return *this;
795  }
796 
797  Rule const* rule() const {
798  return _rule;
799  }
800 
801  // This implements reverse lex comparison of this and that, which satisfies
802  // the requirement of std::set that equivalent items be incomparable, so,
803  // for example bcbc and abcbc are considered equivalent, but abcba and bcbc
804  // are not.
805  bool operator<(RuleLookup const& that) const {
806  auto it_this = _last - 1;
807  auto it_that = that._last - 1;
808  while (it_this > _first && it_that > that._first
809  && *it_this == *it_that) {
810  --it_that;
811  --it_this;
812  }
813  return *it_this < *it_that;
814  }
815 
816  private:
817  rws_word_t::const_iterator _first;
818  rws_word_t::const_iterator _last;
819  Rule const* _rule;
820  };
821 } // namespace libsemigroups
822 #endif // LIBSEMIGROUPS_SRC_RWS_H_
std::string * rewrite(std::string *w) const
Rewrites the word w in-place according to the current rules in the rewriting system.
Definition: rws.h:271
RWS(ReductionOrdering *order, std::string alphabet=STANDARD_ALPHABET)
Constructs rewriting system with no rules and the reduction ordering order.
Definition: rws.h:165
bool test_equals(word_t const &p, word_t const &q)
Returns true if the reduced form of RWS::word_to_rws_word(p) equal the reduced form of RWS::word_to_r...
Definition: rws.cc:672
RWS(Congruence &cong)
Constructs a rewriting system from Congruence::relations and Congruence::extra applied to cong.
Definition: rws.h:241
This class implements the shortlex reduction ordering derived from an ordering on libsemigroups::rws_...
Definition: rws.h:73
void set_overlap_measure(overlap_measure measure)
This method can be used to determine the way that the length of an overlap of two words in the system...
Definition: rws.cc:171
RWS(std::string alphabet)
Constructs a rewriting system with no rules, and the SHORTLEX reduction ordering and using the alphab...
Definition: rws.h:217
overlap_measure
The values in this enum determine how a rewriting system measures the length of the overlap of two w...
Definition: rws.h:157
void set_report_interval(size_t interval)
Some information can be sent to std::cout during calls to RWS::knuth_bendix and RWS::knuth_bendix_by_...
Definition: rws.h:382
std::vector< std::pair< std::string, std::string > > rules() const
This method returns a vector consisting of the pairs of strings which represent the rules of the rewr...
Definition: rws.cc:343
ReductionOrdering(std::function< bool(std::string const *, std::string const *)> func)
A constructor.
Definition: rws.h:51
void add_rule(std::string const &p, std::string const &q)
Add a rule to the rewriting system.
Definition: rws.cc:228
static rws_word_t * uint_to_rws_word(size_t const &a)
This method converts an unsigned integer to the corresponding rws_word_t. For example,...
Definition: rws.h:525
std::vector< letter_t > word_t
Type for a word over the generators of a semigroup.
Definition: semigroups.h:55
void set_max_rules(size_t val)
This method sets the (approximate) maximum number of rules that the system should contain....
Definition: rws.h:431
bool rule(std::string p, std::string q) const
This method returns true if the strings p and q represent an active rule of the rewriting system,...
Definition: rws.cc:364
static size_t const UNBOUNDED
The constant value represents an UNBOUNDED quantity.
Definition: rws.h:520
void set_max_overlap(size_t val)
This method can be used to specify the maximum length of the overlap of two left hand sides of rules ...
Definition: rws.h:418
size_t operator()(std::string const *p, std::string const *q) const
Returns true if the word pointed to by p is greater than the word pointed to by q in the reduction or...
Definition: rws.h:57
RWS(std::vector< relation_t > const &relations)
Constructs a rewriting system with rules derived from the parameter relations, and with the SHORTLEX ...
Definition: rws.h:221
std::vector< relation_t > const & relations()
Returns the vector of relations used to define the semigroup over which the congruence is defined.
Definition: cong.h:271
size_t nr_rules() const
Returns the current number of active rules in the rewriting system.
Definition: rws.h:265
SHORTLEX()
Constructs a short-lex reduction ordering object derived from the order of on libsemigroups::rws_lett...
Definition: rws.h:77
std::vector< relation_t > const & extra() const
Returns the vector of extra relations (or equivalently, generating pairs) used to define the congruen...
Definition: cong.h:278
RWS()
Constructs a rewriting system with no rules, and the SHORTLEX reduction ordering.
Definition: rws.h:208
void knuth_bendix()
Run the Knuth-Bendix algorithm on the rewriting system.
Definition: rws.h:291
bool test_less_than(word_t const &p, word_t const &q)
Returns true if the reduced form of RWS::word_to_rws_word(p) is less than the reduced form of RWS::wo...
Definition: rws.cc:705
static rws_word_t * word_to_rws_word(word_t const &w, rws_word_t *ww)
This method converts a vector of unsigned integers to a string which represents a word in the rewriti...
Definition: rws.h:546
bool confluent() const
Returns true if the rewriting system is confluent and false if it is not.
Definition: rws.h:259
Class for congruence on a semigroup or fintely presented semigroup.
Definition: cong.h:54
~RWS()
A default destructor.
Definition: rws.cc:190
char rws_letter_t
Type for letters for rewriting systems.
Definition: rws.h:144
void set_check_confluence_interval(size_t interval)
The method RWS::knuth_bendix periodically checks if the system is already confluent....
Definition: rws.h:397
Namespace for everything in the libsemigroups library.
Definition: blocks.cc:32
void set_report(bool val) const
Turn reporting on or off.
Definition: rws.h:372
RWS(ReductionOrdering *order, std::vector< relation_t > const &relations)
Constructs a rewriting system with rules derived from relations, and with the reduction ordering spec...
Definition: rws.h:230
This class is used to represent a string rewriting system defining a finitely presented monoid or sem...
Definition: rws.h:135
void add_rules(Congruence &cong)
Add rules derived from Congruence::relations and Congruence::extra applied to cong.
Definition: rws.h:349
void knuth_bendix_by_overlap_length()
This method runs the Knuth-Bendix algorithm on the rewriting system by considering all overlaps of a ...
Definition: rws.h:316
friend std::ostream & operator<<(std::ostream &os, RWS const &rws)
This method allows a RWS object to be left shifted into a std::ostream, such as std::cout....
Definition: rws.cc:211
std::string rewrite(std::string w) const
Rewrites a copy of the word w according to the current rules in the rewriting system.
Definition: rws.h:280
void add_rules(std::vector< relation_t > const &relations)
Adds rules derived from relations via RWS::word_to_rws_word to the rewriting system.
Definition: rws.cc:219
static word_t * rws_word_to_word(rws_word_t const *rws_word)
This method converts a string in the rewriting system into a vector of unsigned integers....
Definition: rws.h:531
static rws_word_t * word_to_rws_word(word_t const &w)
This method converts a vector of unsigned integers to a string which represents a word in the rewriti...
Definition: rws.h:559
size_t operator()(std::string const &p, std::string const &q) const
Returns true if the word p is greater than the word q in the reduction ordering.
Definition: rws.h:63
This class provides a call operator which can be used to compare libsemigroups::rws_word_t.
Definition: rws.h:43