19 #ifndef LIBSEMIGROUPS_SRC_RWS_H_ 20 #define LIBSEMIGROUPS_SRC_RWS_H_ 31 #include "semigroups.h" 52 std::function<
bool(std::string
const*, std::string
const*)> func)
57 size_t operator()(std::string
const* p, std::string
const* q)
const {
63 size_t operator()(std::string
const& p, std::string
const& q)
const {
68 std::function<bool(std::string const*, std::string const*)> _func;
79 return (p->size() > q->size()
80 || (p->size() == q->size() && *p > *q));
139 struct OverlapMeasure;
147 typedef std::string rws_word_t;
166 std::string alphabet = STANDARD_ALPHABET)
169 _check_confluence_interval(4096),
171 _confluence_known(false),
176 _min_length_lhs_rule(std::numeric_limits<size_t>::max()),
178 _overlap_measure(nullptr),
180 _report_interval(1000),
182 _tmp_word1(new rws_word_t()),
183 _tmp_word2(new rws_word_t()),
185 _next_rule_it1 = _active_rules.end();
186 _next_rule_it2 = _active_rules.end();
188 if (_alphabet != STANDARD_ALPHABET) {
189 if (std::is_sorted(_alphabet.cbegin(), _alphabet.cend())) {
190 _alphabet = STANDARD_ALPHABET;
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)));
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;
221 explicit RWS(std::vector<relation_t>
const& relations) :
RWS() {
254 friend std::ostream&
operator<<(std::ostream& os,
RWS const& rws);
260 std::atomic<bool> killed(
false);
266 return _active_rules.size();
272 string_to_rws_word(*w);
274 rws_word_to_string(*w);
292 std::atomic<bool> killed(
false);
318 size_t max_overlap = _max_overlap;
319 size_t check_confluence_interval = _check_confluence_interval;
322 std::atomic<bool> killed(
false);
327 _max_overlap = max_overlap;
328 _check_confluence_interval = check_confluence_interval;
329 REPORT(
"elapsed time = " << timer);
339 void add_rule(std::string
const& p, std::string
const& q);
345 void add_rules(std::vector<relation_t>
const& relations);
358 bool rule(std::string p, std::string q)
const;
366 std::vector<std::pair<std::string, std::string>>
rules()
const;
373 glob_reporter.set_report(val);
383 _report_interval = interval;
401 _check_confluence_interval = interval;
492 bool test_equals(std::initializer_list<size_t>
const& p,
493 std::initializer_list<size_t>
const& q);
502 bool test_equals(std::string
const& p, std::string
const& q);
520 static size_t const UNBOUNDED =
static_cast<size_t>(-2);
526 return new rws_word_t(1, uint_to_rws_letter(a));
533 w->reserve(rws_word->size());
535 w->push_back(rws_letter_to_uint(rws_letter));
548 for (
size_t const& a : w) {
549 (*ww) += uint_to_rws_letter(a);
560 rws_word_t* ww =
new rws_word_t();
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);
569 return static_cast<size_t>(rws_letter - 1);
573 static inline rws_letter_t uint_to_rws_letter(
size_t const& a) {
574 #ifdef LIBSEMIGROUPS_DEBUG 582 LIBSEMIGROUPS_ASSERT(_alphabet != STANDARD_ALPHABET);
583 LIBSEMIGROUPS_ASSERT(_alphabet_map.find(a) != _alphabet_map.end());
584 return (*_alphabet_map.find(a)).second;
588 LIBSEMIGROUPS_ASSERT(_alphabet != STANDARD_ALPHABET);
589 LIBSEMIGROUPS_ASSERT(rws_letter_to_uint(a) < _alphabet.size());
590 return _alphabet[rws_letter_to_uint(a)];
593 inline void string_to_rws_word(std::string& w)
const {
594 if (_alphabet == STANDARD_ALPHABET) {
598 a = char_to_rws_letter(a);
602 inline void rws_word_to_string(rws_word_t& w)
const {
603 if (_alphabet == STANDARD_ALPHABET) {
607 a = rws_letter_to_char(a);
611 static std::string
const STANDARD_ALPHABET;
614 std::list<Rule const*>::iterator
615 remove_rule(std::list<Rule const*>::iterator it);
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;
627 void internal_rewrite(rws_word_t* w)
const;
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;
639 mutable std::atomic<bool> _confluence_known;
640 mutable std::list<Rule*> _inactive_rules;
641 mutable std::atomic<bool> _confluent;
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;
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;
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;
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());
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);
686 rws_word_t
const* lhs()
const {
687 return const_cast<rws_word_t const*
>(_lhs);
693 rws_word_t
const* rhs()
const {
694 return const_cast<rws_word_t const*
>(_rhs);
699 Rule& operator=(Rule
const& copy) =
delete;
703 Rule(Rule
const& copy) =
delete;
706 explicit Rule(
RWS const* rws, int64_t
id)
708 _lhs(new rws_word_t()),
709 _rhs(new rws_word_t()),
711 LIBSEMIGROUPS_ASSERT(_id < 0);
721 LIBSEMIGROUPS_ASSERT(_id != 0);
722 _rws->internal_rewrite(_lhs);
723 _rws->internal_rewrite(_rhs);
728 LIBSEMIGROUPS_ASSERT(_id != 0);
729 _rws->internal_rewrite(_rhs);
733 LIBSEMIGROUPS_ASSERT(_id != 0);
738 inline bool active()
const {
739 LIBSEMIGROUPS_ASSERT(_id != 0);
744 LIBSEMIGROUPS_ASSERT(_id != 0);
751 LIBSEMIGROUPS_ASSERT(_id != 0);
757 void set_id(int64_t
id) {
758 LIBSEMIGROUPS_ASSERT(
id > 0);
759 LIBSEMIGROUPS_ASSERT(!active());
764 LIBSEMIGROUPS_ASSERT(_id != 0);
769 if ((*(_rws->_order))(_rhs, _lhs)) {
770 std::swap(_lhs, _rhs);
781 class RWS::RuleLookup {
783 RuleLookup() : _rule(nullptr) {}
785 explicit RuleLookup(RWS::Rule*
rule)
786 : _first(
rule->lhs()->cbegin()),
787 _last(
rule->lhs()->cend()),
790 RuleLookup& operator()(rws_word_t::iterator
const& first,
791 rws_word_t::iterator
const& last) {
797 Rule
const*
rule()
const {
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) {
813 return *it_this < *it_that;
817 rws_word_t::const_iterator _first;
818 rws_word_t::const_iterator _last;
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, the integer 0 is converted to the word with single letter which is the 1st ASCII character.
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. This method can be used to set how frequently this happens, it is the number of new overlaps that should be considered before checking confluence. Setting this value too low can adversely affect the performance of RWS::knuth_bendix.
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. The currently active rules of the system are represented in the output.
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. This method is the inverse of RWS::uint_to_rws_word.
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