libsemigroups
|
This class is used to represent a string rewriting system defining a finitely presented monoid or semigroup. More...
#include <rws.h>
Public Types | |
enum | overlap_measure { ABC = 0, AB_BC = 1, max_AB_BC = 2 } |
The values in this enum determine how a rewriting system measures the length \(d(AB, BC)\) of the overlap of two words \(AB\) and \(BC\): More... | |
typedef char | rws_letter_t |
Type for letters for rewriting systems. More... | |
Public Member Functions | |
RWS (ReductionOrdering *order, std::string alphabet=STANDARD_ALPHABET) | |
Constructs rewriting system with no rules and the reduction ordering order . More... | |
RWS () | |
Constructs a rewriting system with no rules, and the SHORTLEX reduction ordering. More... | |
RWS (std::string alphabet) | |
Constructs a rewriting system with no rules, and the SHORTLEX reduction ordering and using the alphabet specified by the parameter alphabet . More... | |
RWS (std::vector< relation_t > const &relations) | |
Constructs a rewriting system with rules derived from the parameter relations , and with the SHORTLEX reduction ordering. More... | |
RWS (ReductionOrdering *order, std::vector< relation_t > const &relations) | |
Constructs a rewriting system with rules derived from relations , and with the reduction ordering specified by order . More... | |
RWS (Congruence &cong) | |
Constructs a rewriting system from Congruence::relations and Congruence::extra applied to cong . More... | |
~RWS () | |
A default destructor. More... | |
void | add_rule (std::string const &p, std::string const &q) |
Add a rule to the rewriting system. More... | |
void | add_rules (std::vector< relation_t > const &relations) |
Adds rules derived from relations via RWS::word_to_rws_word to the rewriting system. More... | |
void | add_rules (Congruence &cong) |
Add rules derived from Congruence::relations and Congruence::extra applied to cong . More... | |
bool | confluent () const |
Returns true if the rewriting system is confluent and false if it is not. More... | |
void | knuth_bendix () |
Run the Knuth-Bendix algorithm on the rewriting system. More... | |
void | knuth_bendix (std::atomic< bool > &killed) |
Run the Knuth-Bendix algorithm on the rewriting system until it terminates or killed is set to true . More... | |
void | knuth_bendix_by_overlap_length () |
This method runs the Knuth-Bendix algorithm on the rewriting system by considering all overlaps of a given length \(n\) (according to the RWS::overlap_measure) before those overlaps of length \(n + 1\). More... | |
size_t | nr_rules () const |
Returns the current number of active rules in the rewriting system. More... | |
std::string * | rewrite (std::string *w) const |
Rewrites the word w in-place according to the current rules in the rewriting system. More... | |
std::string | rewrite (std::string w) const |
Rewrites a copy of the word w according to the current rules in the rewriting system. More... | |
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, i.e. if either \( p \to q\) or \( q \to p \) is a currently active rule of the system. More... | |
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 rewriting system. The first entry in every such pair is greater than the second according to the reduction ordering of the rewriting system. The rules are sorted according to the reduction ordering used by the rewriting system, on the first entry. More... | |
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. More... | |
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 that should be considered in RWS::knuth_bendix. More... | |
void | set_max_rules (size_t val) |
This method sets the (approximate) maximum number of rules that the system should contain. If this is number is exceeded in calls to RWS::knuth_bendix or RWS::knuth_bendix_by_overlap_length, then these methods will terminate and the system may not be confluent. More... | |
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 is meaasured. More... | |
void | set_report (bool val) const |
Turn reporting on or off. More... | |
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_overlap_length. This method can be used to determine the frequency with which this information is given, where a larger value means less frequently. More... | |
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_rws_word(q) , and false if not. More... | |
bool | test_equals (std::initializer_list< size_t > const &p, std::initializer_list< size_t > const &q) |
Returns true if the reduced form of RWS::word_to_rws_word(p) equal the reduced form of RWS::word_to_rws_word(q) , and false if not. More... | |
bool | test_equals (std::string const &p, std::string const &q) |
Returns true if RWS::rewrite(p) equals RWS::rewrite(q) , and false if not. More... | |
bool | test_equals (std::string *p, std::string *q) |
Returns true if RWS::rewrite(p) equals RWS::rewrite(q) , and false if not. More... | |
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::word_to_rws_word(q) , with respect to the reduction ordering of this , and false if not. More... | |
bool | test_less_than (std::string const &p, std::string const &q) |
Returns true if RWS::rewrite(p) is less than RWS::rewrite(q) , with respect to the reduction ordering of this , and false if not. More... | |
bool | test_less_than (std::string *p, std::string *q) |
Returns true if RWS::rewrite(p) is less than RWS::rewrite(q) , with respect to the reduction ordering of this , and false if not. More... | |
Static Public Member Functions | |
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. More... | |
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. More... | |
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 rewriting system. The second parameter ww is modified in-place to contain the string version of the vector of unsigned integers w . More... | |
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 rewriting system. More... | |
Static Public Attributes | |
static size_t const | UNBOUNDED = static_cast<size_t>(-2) |
The constant value represents an UNBOUNDED quantity. More... | |
Friends | |
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. More... | |
This class is used to represent a string rewriting system defining a finitely presented monoid or semigroup.
typedef char libsemigroups::RWS::rws_letter_t |
Type for letters for rewriting systems.
The values in this enum determine how a rewriting system measures the length \(d(AB, BC)\) of the overlap of two words \(AB\) and \(BC\):
|
inlineexplicit |
Constructs rewriting system with no rules and the reduction ordering order
.
This constructs a rewriting system with no rules, and with the reduction ordering ReductionOrdering specifed by the parameter order
.
|
inline |
Constructs a rewriting system with no rules, and the SHORTLEX reduction ordering.
|
inlineexplicit |
Constructs a rewriting system with no rules, and the SHORTLEX reduction ordering and using the alphabet specified by the parameter alphabet
.
|
inlineexplicit |
Constructs a rewriting system with rules derived from the parameter relations
, and with the SHORTLEX reduction ordering.
|
inline |
Constructs a rewriting system with rules derived from relations
, and with the reduction ordering specified by order
.
The RWS instance constructed here owns the parameter order
, and deletes it in its destructor.
|
inlineexplicit |
Constructs a rewriting system from Congruence::relations and Congruence::extra applied to cong
.
Constructs a rewriting system with rules corresponding to the relations used to define cong
, i.e. Congruence::relations and Congruence::extra, and with the SHORTLEX reduction ordering.
libsemigroups::RWS::~RWS | ( | ) |
A default destructor.
This deletes the reduction order used to construct the object, and the rules in the system.
void libsemigroups::RWS::add_rule | ( | std::string const & | p, |
std::string const & | q | ||
) |
Add a rule to the rewriting system.
The principal difference between this method and RWS::add_rule(std::string* p, std::string* q) is that the arguments are copied by this method.
void libsemigroups::RWS::add_rules | ( | std::vector< relation_t > const & | relations | ) |
Adds rules derived from relations
via RWS::word_to_rws_word to the rewriting system.
|
inline |
Add rules derived from Congruence::relations and Congruence::extra applied to cong
.
|
inline |
Returns true
if the rewriting system is confluent and false
if it is not.
|
inline |
Run the Knuth-Bendix algorithm on the rewriting system.
void libsemigroups::RWS::knuth_bendix | ( | std::atomic< bool > & | killed | ) |
Run the Knuth-Bendix algorithm on the rewriting system until it terminates or killed
is set to true
.
|
inline |
This method runs the Knuth-Bendix algorithm on the rewriting system by considering all overlaps of a given length \(n\) (according to the RWS::overlap_measure) before those overlaps of length \(n + 1\).
|
inline |
Returns the current number of active rules in the rewriting system.
|
inline |
Rewrites the word w
in-place according to the current rules in the rewriting system.
|
inline |
Rewrites a copy of the word w
according to the current rules in the rewriting system.
bool libsemigroups::RWS::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, i.e. if either \( p \to q\) or \( q \to p \) is a currently active rule of the system.
std::vector< std::pair< std::string, std::string > > libsemigroups::RWS::rules | ( | ) | const |
This method returns a vector consisting of the pairs of strings which represent the rules of the rewriting system. The first
entry in every such pair is greater than the second
according to the reduction ordering of the rewriting system. The rules are sorted according to the reduction ordering used by the rewriting system, on the first entry.
|
inlinestatic |
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.
|
inline |
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.
The default value is 4096, and should be set to RWS::UNBOUNDED if RWS::knuth_bendix should never check if the system is already confluent.
|
inline |
This method can be used to specify the maximum length of the overlap of two left hand sides of rules that should be considered in RWS::knuth_bendix.
If this value is less than the longest left hand side of a rule, then RWS::knuth_bendix can terminate without the system being confluent.
|
inline |
This method sets the (approximate) maximum number of rules that the system should contain. If this is number is exceeded in calls to RWS::knuth_bendix or RWS::knuth_bendix_by_overlap_length, then these methods will terminate and the system may not be confluent.
void libsemigroups::RWS::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 is meaasured.
|
inline |
Turn reporting on or off.
If val
is true, then some methods for a RWS object may report information about the progress of the computation.
|
inline |
Some information can be sent to std::cout during calls to RWS::knuth_bendix and RWS::knuth_bendix_by_overlap_length. This method can be used to determine the frequency with which this information is given, where a larger value means less frequently.
The default value is 1000.
Returns true
if the reduced form of RWS::word_to_rws_word(p)
equal the reduced form of RWS::word_to_rws_word(q)
, and false
if not.
bool libsemigroups::RWS::test_equals | ( | std::initializer_list< size_t > const & | p, |
std::initializer_list< size_t > const & | q | ||
) |
Returns true
if the reduced form of RWS::word_to_rws_word(p)
equal the reduced form of RWS::word_to_rws_word(q)
, and false
if not.
bool libsemigroups::RWS::test_equals | ( | std::string const & | p, |
std::string const & | q | ||
) |
Returns true
if RWS::rewrite(p)
equals RWS::rewrite(q)
, and false
if not.
bool libsemigroups::RWS::test_equals | ( | std::string * | p, |
std::string * | q | ||
) |
Returns true
if RWS::rewrite(p)
equals RWS::rewrite(q)
, and false
if not.
This method rewrites p
and q
in-place (unless they are already equal before rewriting). The caller responsible for deletion.
Returns true
if the reduced form of RWS::word_to_rws_word(p)
is less than the reduced form of RWS::word_to_rws_word(q)
, with respect to the reduction ordering of this
, and false
if not.
bool libsemigroups::RWS::test_less_than | ( | std::string const & | p, |
std::string const & | q | ||
) |
Returns true
if RWS::rewrite(p)
is less than RWS::rewrite(q)
, with respect to the reduction ordering of this
, and false
if not.
bool libsemigroups::RWS::test_less_than | ( | std::string * | p, |
std::string * | q | ||
) |
Returns true
if RWS::rewrite(p)
is less than RWS::rewrite(q)
, with respect to the reduction ordering of this
, and false
if not.
The parameters p
and q
are rewritten in-place, and the caller is responsible for their deletion.
|
inlinestatic |
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.
|
inlinestatic |
This method converts a vector of unsigned integers to a string which represents a word in the rewriting system. The second parameter ww
is modified in-place to contain the string version of the vector of unsigned integers w
.
This method returns its second parameter ww
.
|
inlinestatic |
This method converts a vector of unsigned integers to a string which represents a word in the rewriting system.
This method returns a pointer to a new string, and it is the responsibility of the caller to delete it.
|
friend |
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.
|
static |
The constant value represents an UNBOUNDED quantity.