This class is used to represent a string rewriting system defining a finitely presented monoid or semigroup. More...

#include <rws.h>

Classes
class	Rule
	Class for rules in rewriting systems, which supports only two methods, Rule::lhs and Rule::rhs, which return the left and right hand sides of the rule. More...

Public Member Functions
	RWS (ReductionOrdering *order)
	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::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 (rws_word_t p, rws_word_t q)
	Add a rule to the rewriting system. More...

void	add_rule (rws_word_t const &p, rws_word_t 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	is_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...

size_t	nr_rules () const
	Returns the current number of active rules in the rewriting system. More...

void	rewrite (rws_word_t *w) const
	Rewrites the word pointed to by `w` in-place according to the current rules in the rewriting system. More...

rws_word_t	rewrite (rws_word_t w) const
	Rewrites a copy of the word `w` according to the current rules in the rewriting system. More...

std::list< Rule const * >::const_iterator	rules_cbegin () const
	Returns an iterator pointing at the first Rule of `this`. More...

std::list< Rule const * >::const_iterator	rules_cend () const
	Returns an iterator pointing past the last Rule of `this`. More...

void	set_confluent (bool val)
	If you somehow magically know that the rewriting system is confluent, or not, then you can set this using this method. More...

void	set_report (bool val) const
	Turn reporting on or off. 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 (rws_word_t const &p, rws_word_t const &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 (rws_word_t const &p, rws_word_t 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...

Static Public Member Functions
static rws_letter_t	letter_to_rws_letter (letter_t const &a)
	Helper function for converting a libsemigroups::letter_t to a libsemigroups::rws_letter_t. More...

static rws_word_t *	letter_to_rws_word (letter_t const &a)
	Helper function for converting a libsemigroups::letter_t to a libsemigroups::rws_word_t. More...

static letter_t	rws_letter_to_letter (rws_letter_t const &rws_letter)
	Helper function for converting a libsemigroups::rws_letter_t to a libsemigroups::letter_t. More...

static word_t *	rws_word_to_word (rws_word_t const *rws_word)
	Helper function for converting a libsemigroups::rws_word_t to a libsemigroups::word_t. More...

static rws_word_t *	word_to_rws_word (word_t const &w)
	Helper function for converting a libsemigroups::word_t to a libsemigroups::rws_word_t. More...

Detailed Description

This class is used to represent a string rewriting system defining a finitely presented monoid or semigroup.

Constructor & Destructor Documentation

◆ RWS() [1/5]

libsemigroups::RWS::RWS ( ReductionOrdering * order )

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.

◆ RWS() [2/5]

libsemigroups::RWS::RWS ( )

inline

Constructs a rewriting system with no rules, and the SHORTLEX reduction ordering.

◆ RWS() [3/5]

libsemigroups::RWS::RWS ( std::vector< relation_t > const & relations )

inlineexplicit

Constructs a rewriting system with rules derived from the parameter relations, and with the SHORTLEX reduction ordering.

◆ RWS() [4/5]

libsemigroups::RWS::RWS	(	ReductionOrdering *	order,
		std::vector< relation_t > const &	relations
	)

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.

◆ RWS() [5/5]

libsemigroups::RWS::RWS ( Congruence & cong )

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.

◆ ~RWS()

libsemigroups::RWS::~RWS ( )

A default destructor.

This deletes the reduction order used to construct the object, and the rules in the system.

Member Function Documentation

◆ add_rule() [1/2]

void libsemigroups::RWS::add_rule	(	rws_word_t *	p,
		rws_word_t *	q
	)

Add a rule to the rewriting system.

The parameters p and q correspond to the rule being added.

If p and q are not equal, then this method adds a rule to the rewriting system, where the left-hand side of the rule is strictly greater than the right-hand side in the reduction ordering used to defined this. If p and q are equal, then the rewriting system is unchanged and p and q are deleted.

The parameters p and q are not copied and will be deleted by the this.

◆ add_rule() [2/2]

void libsemigroups::RWS::add_rule	(	rws_word_t const &	p,
		rws_word_t const &	q
	)

Add a rule to the rewriting system.

The principal difference between this method and RWS::add_rule(rws_word_t* p, rws_word_t* q) is that the arguments are copied by this method.

See also: RWS::add_rule.

◆ add_rules() [1/2]

void libsemigroups::RWS::add_rules ( std::vector< relation_t > const & relations )

inline

Adds rules derived from relations via RWS::word_to_rws_word to the rewriting system.

See also: RWS::add_rule.

◆ add_rules() [2/2]

void libsemigroups::RWS::add_rules ( Congruence & cong )

inline

Add rules derived from Congruence::relations and Congruence::extra applied to cong.

◆ is_confluent()

bool libsemigroups::RWS::is_confluent ( ) const

inline

Returns true if the rewriting system is confluent and false if it is not.

◆ knuth_bendix() [1/2]

void libsemigroups::RWS::knuth_bendix ( )

inline

Run the Knuth-Bendix algorithm on the rewriting system.

Warning: This will terminate when the rewriting system is confluent, which might be never.

◆ knuth_bendix() [2/2]

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.

Warning: This will terminate when the rewriting system is confluent, which might be never.

◆ letter_to_rws_letter()

rws_letter_t libsemigroups::RWS::letter_to_rws_letter ( letter_t const & a )

static

Helper function for converting a libsemigroups::letter_t to a libsemigroups::rws_letter_t.

See also: RWS::rws_letter_to_letter.

◆ letter_to_rws_word()

rws_word_t * libsemigroups::RWS::letter_to_rws_word ( letter_t const & a )

static

Helper function for converting a libsemigroups::letter_t to a libsemigroups::rws_word_t.

◆ nr_rules()

size_t libsemigroups::RWS::nr_rules ( ) const

inline

Returns the current number of active rules in the rewriting system.

◆ rewrite() [1/2]

void libsemigroups::RWS::rewrite ( rws_word_t * w ) const

Rewrites the word pointed to by w in-place according to the current rules in the rewriting system.

◆ rewrite() [2/2]

rws_word_t libsemigroups::RWS::rewrite ( rws_word_t w ) const

inline

Rewrites a copy of the word w according to the current rules in the rewriting system.

◆ rules_cbegin()

std::list<Rule const*>::const_iterator libsemigroups::RWS::rules_cbegin ( ) const

inline

Returns an iterator pointing at the first Rule of this.

◆ rules_cend()

std::list<Rule const*>::const_iterator libsemigroups::RWS::rules_cend ( ) const

inline

Returns an iterator pointing past the last Rule of this.

◆ rws_letter_to_letter()

letter_t libsemigroups::RWS::rws_letter_to_letter ( rws_letter_t const & rws_letter )

static

Helper function for converting a libsemigroups::rws_letter_t to a libsemigroups::letter_t.

See also: RWS::letter_to_rws_letter.

◆ rws_word_to_word()

word_t * libsemigroups::RWS::rws_word_to_word ( rws_word_t const * rws_word )

static

Helper function for converting a libsemigroups::rws_word_t to a libsemigroups::word_t.

See also: RWS::word_to_rws_word.

◆ set_confluent()

void libsemigroups::RWS::set_confluent ( bool val )

inline

If you somehow magically know that the rewriting system is confluent, or not, then you can set this using this method.

◆ set_report()

void libsemigroups::RWS::set_report ( bool val ) const

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.

◆ test_equals() [1/2]

bool libsemigroups::RWS::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.

Warning: This method calls RWS::knuth_bendix and so it may never terminate.

See also: RWS::test_equals(rws_word_t const& p, rws_word_t const& q)

◆ test_equals() [2/2]

bool libsemigroups::RWS::test_equals	(	rws_word_t const &	p,
		rws_word_t const &	q
	)

Returns true if RWS::rewrite(p) equals RWS::rewrite(q), and false if not.

Warning: This method calls RWS::knuth_bendix and so it may never terminate.

See also: RWS::test_equals(word_t const& p, word_t const& q)

◆ test_less_than() [1/2]

bool libsemigroups::RWS::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.

Warning: This method calls RWS::knuth_bendix and so it may never terminate.

See also: RWS::test_less_than(rws_word_t const& p, rws_word_t const& q)

◆ test_less_than() [2/2]

bool libsemigroups::RWS::test_less_than	(	rws_word_t const &	p,
		rws_word_t 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.

Warning: This method calls RWS::knuth_bendix and so it may never terminate.

See also: RWS::test_less_than(word_t const& p, word_t const& q)

◆ word_to_rws_word()

rws_word_t * libsemigroups::RWS::word_to_rws_word ( word_t const & w )

static

Helper function for converting a libsemigroups::word_t to a libsemigroups::rws_word_t.

See also: RWS::rws_word_to_word.

The documentation for this class was generated from the following files:

src/rws.h
src/rws.cc

Classes

Public Member Functions

Static Public Member Functions

Detailed Description

Constructor & Destructor Documentation

◆ RWS() [1/5]

◆ RWS() [2/5]

◆ RWS() [3/5]

◆ RWS() [4/5]

◆ RWS() [5/5]

◆ ~RWS()

Member Function Documentation

◆ add_rule() [1/2]

◆ add_rule() [2/2]

◆ add_rules() [1/2]

◆ add_rules() [2/2]

◆ is_confluent()

◆ knuth_bendix() [1/2]

◆ knuth_bendix() [2/2]

◆ letter_to_rws_letter()

◆ letter_to_rws_word()

◆ nr_rules()

◆ rewrite() [1/2]

◆ rewrite() [2/2]

◆ rules_cbegin()

◆ rules_cend()

◆ rws_letter_to_letter()

◆ rws_word_to_word()

◆ set_confluent()

◆ set_report()

◆ test_equals() [1/2]

◆ test_equals() [2/2]

◆ test_less_than() [1/2]

◆ test_less_than() [2/2]

◆ word_to_rws_word()