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 575 return static_cast<rws_letter_t>(a + 97);
577 return static_cast<rws_letter_t>(a + 1);
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,...
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