Skip to content

Commit 14374c8

Browse files
james-d-mitchellJoseph-Edwards
authored andcommitted
knuth-bendix: add support for RPO
1 parent 4e04a5d commit 14374c8

6 files changed

Lines changed: 227 additions & 19 deletions

File tree

docs/source/main-algorithms/knuth-bendix/to-knuth-bendix.rst

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,8 @@
55

66
The full license is in the file LICENSE, distributed with this software.
77

8+
.. TODO update
9+
810
.. currentmodule:: libsemigroups_pybind11
911

1012
Converting to a KnuthBendix

src/cong-common.cpp

Lines changed: 147 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,11 @@ namespace libsemigroups {
5454
using KnuthBendixWordLenLexTrie = KnuthBendix<word_type, LenLexTrie>;
5555
using KnuthBendixWordLenLexSet = KnuthBendix<word_type, LenLexSet>;
5656

57+
using KnuthBendixStringRPOTrie = KnuthBendix<std::string, RPOTrie>;
58+
using KnuthBendixStringRPOSet = KnuthBendix<std::string, RPOSet>;
59+
using KnuthBendixWordRPOTrie = KnuthBendix<word_type, RPOTrie>;
60+
using KnuthBendixWordRPOSet = KnuthBendix<word_type, RPOSet>;
61+
5762
////////////////////////////////////////////////////////////////////////
5863
// Implementation helpers
5964
////////////////////////////////////////////////////////////////////////
@@ -133,6 +138,11 @@ This function default constructs an uninitialised :any:`{name}` instance.
133138
DEF_CONSTRUCT_DEFAULT(detail::KnuthBendixImpl<LenLexSet>,
134139
detail::CongruenceCommon);
135140

141+
DEF_CONSTRUCT_DEFAULT(detail::KnuthBendixImpl<RPOTrie>,
142+
detail::CongruenceCommon);
143+
DEF_CONSTRUCT_DEFAULT(detail::KnuthBendixImpl<RPOSet>,
144+
detail::CongruenceCommon);
145+
136146
DEF_CONSTRUCT_DEFAULT(KnuthBendixStringLenLexTrie,
137147
detail::KnuthBendixImpl<LenLexTrie>);
138148
DEF_CONSTRUCT_DEFAULT(KnuthBendixStringLenLexSet,
@@ -142,6 +152,14 @@ This function default constructs an uninitialised :any:`{name}` instance.
142152
DEF_CONSTRUCT_DEFAULT(KnuthBendixWordLenLexSet,
143153
detail::KnuthBendixImpl<LenLexSet>);
144154

155+
DEF_CONSTRUCT_DEFAULT(KnuthBendixStringRPOTrie,
156+
detail::KnuthBendixImpl<RPOTrie>);
157+
DEF_CONSTRUCT_DEFAULT(KnuthBendixStringRPOSet,
158+
detail::KnuthBendixImpl<RPOSet>);
159+
DEF_CONSTRUCT_DEFAULT(KnuthBendixWordRPOTrie,
160+
detail::KnuthBendixImpl<RPOTrie>);
161+
DEF_CONSTRUCT_DEFAULT(KnuthBendixWordRPOSet, detail::KnuthBendixImpl<RPOSet>);
162+
145163
DEF_CONSTRUCT_DEFAULT(Congruence<word_type>, detail::CongruenceCommon);
146164
DEF_CONSTRUCT_DEFAULT(Congruence<std::string>, detail::CongruenceCommon);
147165

@@ -193,6 +211,9 @@ have been in if it had just been newly default constructed.
193211
DEF_INIT_DEFAULT(detail::KnuthBendixImpl<LenLexSet>,
194212
detail::CongruenceCommon);
195213

214+
DEF_INIT_DEFAULT(detail::KnuthBendixImpl<RPOTrie>, detail::CongruenceCommon);
215+
DEF_INIT_DEFAULT(detail::KnuthBendixImpl<RPOSet>, detail::CongruenceCommon);
216+
196217
DEF_INIT_DEFAULT(KnuthBendixStringLenLexTrie,
197218
detail::KnuthBendixImpl<LenLexTrie>);
198219
DEF_INIT_DEFAULT(KnuthBendixStringLenLexSet,
@@ -202,6 +223,11 @@ have been in if it had just been newly default constructed.
202223
DEF_INIT_DEFAULT(KnuthBendixWordLenLexSet,
203224
detail::KnuthBendixImpl<LenLexSet>);
204225

226+
DEF_INIT_DEFAULT(KnuthBendixStringRPOTrie, detail::KnuthBendixImpl<RPOTrie>);
227+
DEF_INIT_DEFAULT(KnuthBendixStringRPOSet, detail::KnuthBendixImpl<RPOSet>);
228+
DEF_INIT_DEFAULT(KnuthBendixWordRPOTrie, detail::KnuthBendixImpl<RPOTrie>);
229+
DEF_INIT_DEFAULT(KnuthBendixWordRPOSet, detail::KnuthBendixImpl<RPOSet>);
230+
205231
DEF_INIT_DEFAULT(Congruence<word_type>, detail::CongruenceCommon);
206232
DEF_INIT_DEFAULT(Congruence<std::string>, detail::CongruenceCommon);
207233

@@ -276,6 +302,20 @@ of kind *knd* over the semigroup or monoid defined by the presentation *p*.
276302
DEF_CONSTRUCT_KIND_PRESENTATION(KnuthBendixWordLenLexSet,
277303
detail::KnuthBendixImpl<LenLexSet>);
278304

305+
DEF_CONSTRUCT_KIND_PRESENTATION(detail::KnuthBendixImpl<RPOTrie>,
306+
detail::CongruenceCommon);
307+
DEF_CONSTRUCT_KIND_PRESENTATION(detail::KnuthBendixImpl<RPOSet>,
308+
detail::CongruenceCommon);
309+
310+
DEF_CONSTRUCT_KIND_PRESENTATION(KnuthBendixStringRPOTrie,
311+
detail::KnuthBendixImpl<RPOTrie>);
312+
DEF_CONSTRUCT_KIND_PRESENTATION(KnuthBendixStringRPOSet,
313+
detail::KnuthBendixImpl<RPOSet>);
314+
DEF_CONSTRUCT_KIND_PRESENTATION(KnuthBendixWordRPOTrie,
315+
detail::KnuthBendixImpl<RPOTrie>);
316+
DEF_CONSTRUCT_KIND_PRESENTATION(KnuthBendixWordRPOSet,
317+
detail::KnuthBendixImpl<RPOSet>);
318+
279319
DEF_CONSTRUCT_KIND_PRESENTATION(Congruence<word_type>,
280320
detail::CongruenceCommon);
281321
DEF_CONSTRUCT_KIND_PRESENTATION(Congruence<std::string>,
@@ -353,6 +393,20 @@ had been newly constructed from *knd* and *p*.
353393
DEF_INIT_KIND_PRESENTATION(KnuthBendixWordLenLexSet,
354394
detail::KnuthBendixImpl<LenLexSet>);
355395

396+
DEF_INIT_KIND_PRESENTATION(detail::KnuthBendixImpl<RPOTrie>,
397+
detail::CongruenceCommon);
398+
DEF_INIT_KIND_PRESENTATION(detail::KnuthBendixImpl<RPOSet>,
399+
detail::CongruenceCommon);
400+
401+
DEF_INIT_KIND_PRESENTATION(KnuthBendixStringRPOTrie,
402+
detail::KnuthBendixImpl<RPOTrie>);
403+
DEF_INIT_KIND_PRESENTATION(KnuthBendixStringRPOSet,
404+
detail::KnuthBendixImpl<RPOSet>);
405+
DEF_INIT_KIND_PRESENTATION(KnuthBendixWordRPOTrie,
406+
detail::KnuthBendixImpl<RPOTrie>);
407+
DEF_INIT_KIND_PRESENTATION(KnuthBendixWordRPOSet,
408+
detail::KnuthBendixImpl<RPOSet>);
409+
356410
DEF_INIT_KIND_PRESENTATION(Congruence<word_type>, detail::CongruenceCommon);
357411
DEF_INIT_KIND_PRESENTATION(Congruence<std::string>, detail::CongruenceCommon);
358412

@@ -404,6 +458,14 @@ Copy a :any:`{name}` object.
404458
DEF_COPY(KnuthBendixWordLenLexTrie, detail::KnuthBendixImpl<LenLexTrie>);
405459
DEF_COPY(KnuthBendixWordLenLexSet, detail::KnuthBendixImpl<LenLexSet>);
406460

461+
DEF_COPY(detail::KnuthBendixImpl<RPOTrie>, detail::CongruenceCommon);
462+
DEF_COPY(detail::KnuthBendixImpl<RPOSet>, detail::CongruenceCommon);
463+
464+
DEF_COPY(KnuthBendixStringRPOTrie, detail::KnuthBendixImpl<RPOTrie>);
465+
DEF_COPY(KnuthBendixStringRPOSet, detail::KnuthBendixImpl<RPOSet>);
466+
DEF_COPY(KnuthBendixWordRPOTrie, detail::KnuthBendixImpl<RPOTrie>);
467+
DEF_COPY(KnuthBendixWordRPOSet, detail::KnuthBendixImpl<RPOSet>);
468+
407469
DEF_COPY(Congruence<word_type>, detail::CongruenceCommon);
408470
DEF_COPY(Congruence<std::string>, detail::CongruenceCommon);
409471

@@ -460,6 +522,11 @@ number of classes in the congruence represented by a :any:`{name}` instance.
460522
DEF_NUMBER_OF_CLASSES(detail::KnuthBendixImpl<LenLexSet>,
461523
detail::CongruenceCommon);
462524

525+
DEF_NUMBER_OF_CLASSES(detail::KnuthBendixImpl<RPOTrie>,
526+
detail::CongruenceCommon);
527+
DEF_NUMBER_OF_CLASSES(detail::KnuthBendixImpl<RPOSet>,
528+
detail::CongruenceCommon);
529+
463530
DEF_NUMBER_OF_CLASSES(Congruence<word_type>, detail::CongruenceCommon);
464531
DEF_NUMBER_OF_CLASSES(Congruence<std::string>, detail::CongruenceCommon);
465532

@@ -543,6 +610,20 @@ This function adds a generating pair to the congruence represented by a
543610
DEF_ADD_GENERATING_PAIR(KnuthBendixWordLenLexSet,
544611
detail::KnuthBendixImpl<LenLexSet>);
545612

613+
DEF_ADD_GENERATING_PAIR(detail::KnuthBendixImpl<RPOTrie>,
614+
detail::CongruenceCommon);
615+
DEF_ADD_GENERATING_PAIR(detail::KnuthBendixImpl<RPOSet>,
616+
detail::CongruenceCommon);
617+
618+
DEF_ADD_GENERATING_PAIR(KnuthBendixStringRPOTrie,
619+
detail::KnuthBendixImpl<RPOTrie>);
620+
DEF_ADD_GENERATING_PAIR(KnuthBendixStringRPOSet,
621+
detail::KnuthBendixImpl<RPOSet>);
622+
DEF_ADD_GENERATING_PAIR(KnuthBendixWordRPOTrie,
623+
detail::KnuthBendixImpl<RPOTrie>);
624+
DEF_ADD_GENERATING_PAIR(KnuthBendixWordRPOSet,
625+
detail::KnuthBendixImpl<RPOSet>);
626+
546627
DEF_ADD_GENERATING_PAIR(Congruence<word_type>, detail::CongruenceCommon);
547628
DEF_ADD_GENERATING_PAIR(Congruence<std::string>, detail::CongruenceCommon);
548629

@@ -626,6 +707,20 @@ contained in the congruence, but that this is not currently known.
626707
DEF_CURRENTLY_CONTAINS(KnuthBendixWordLenLexSet,
627708
detail::KnuthBendixImpl<LenLexSet>);
628709

710+
DEF_CURRENTLY_CONTAINS(detail::KnuthBendixImpl<RPOTrie>,
711+
detail::CongruenceCommon);
712+
DEF_CURRENTLY_CONTAINS(detail::KnuthBendixImpl<RPOSet>,
713+
detail::CongruenceCommon);
714+
715+
DEF_CURRENTLY_CONTAINS(KnuthBendixStringRPOTrie,
716+
detail::KnuthBendixImpl<RPOTrie>);
717+
DEF_CURRENTLY_CONTAINS(KnuthBendixStringRPOSet,
718+
detail::KnuthBendixImpl<RPOSet>);
719+
DEF_CURRENTLY_CONTAINS(KnuthBendixWordRPOTrie,
720+
detail::KnuthBendixImpl<RPOTrie>);
721+
DEF_CURRENTLY_CONTAINS(KnuthBendixWordRPOSet,
722+
detail::KnuthBendixImpl<RPOSet>);
723+
629724
DEF_CURRENTLY_CONTAINS(Congruence<word_type>, detail::CongruenceCommon);
630725
DEF_CURRENTLY_CONTAINS(Congruence<std::string>, detail::CongruenceCommon);
631726

@@ -697,6 +792,14 @@ congruence represented by a :py:class:`{name}` instance.
697792
DEF_CONTAINS(KnuthBendixWordLenLexTrie, detail::KnuthBendixImpl<LenLexTrie>);
698793
DEF_CONTAINS(KnuthBendixWordLenLexSet, detail::KnuthBendixImpl<LenLexSet>);
699794

795+
DEF_CONTAINS(detail::KnuthBendixImpl<RPOTrie>, detail::CongruenceCommon);
796+
DEF_CONTAINS(detail::KnuthBendixImpl<RPOSet>, detail::CongruenceCommon);
797+
798+
DEF_CONTAINS(KnuthBendixStringRPOTrie, detail::KnuthBendixImpl<RPOTrie>);
799+
DEF_CONTAINS(KnuthBendixStringRPOSet, detail::KnuthBendixImpl<RPOSet>);
800+
DEF_CONTAINS(KnuthBendixWordRPOTrie, detail::KnuthBendixImpl<RPOTrie>);
801+
DEF_CONTAINS(KnuthBendixWordRPOSet, detail::KnuthBendixImpl<RPOSet>);
802+
700803
DEF_CONTAINS(Congruence<word_type>, detail::CongruenceCommon);
701804
DEF_CONTAINS(Congruence<std::string>, detail::CongruenceCommon);
702805

@@ -770,6 +873,14 @@ normal form for the input word *w*.
770873
DEF_REDUCE_NO_RUN(KnuthBendixWordLenLexSet,
771874
detail::KnuthBendixImpl<LenLexSet>);
772875

876+
DEF_REDUCE_NO_RUN(detail::KnuthBendixImpl<RPOTrie>, detail::CongruenceCommon);
877+
DEF_REDUCE_NO_RUN(detail::KnuthBendixImpl<RPOSet>, detail::CongruenceCommon);
878+
879+
DEF_REDUCE_NO_RUN(KnuthBendixStringRPOTrie, detail::KnuthBendixImpl<RPOTrie>);
880+
DEF_REDUCE_NO_RUN(KnuthBendixStringRPOSet, detail::KnuthBendixImpl<RPOSet>);
881+
DEF_REDUCE_NO_RUN(KnuthBendixWordRPOTrie, detail::KnuthBendixImpl<RPOTrie>);
882+
DEF_REDUCE_NO_RUN(KnuthBendixWordRPOSet, detail::KnuthBendixImpl<RPOSet>);
883+
773884
DEF_REDUCE_NO_RUN(Congruence<word_type>, detail::CongruenceCommon);
774885
DEF_REDUCE_NO_RUN(Congruence<std::string>, detail::CongruenceCommon);
775886

@@ -838,6 +949,14 @@ input word.
838949
DEF_REDUCE(KnuthBendixWordLenLexTrie, detail::KnuthBendixImpl<LenLexTrie>);
839950
DEF_REDUCE(KnuthBendixWordLenLexSet, detail::KnuthBendixImpl<LenLexSet>);
840951

952+
DEF_REDUCE(detail::KnuthBendixImpl<RPOTrie>, detail::CongruenceCommon);
953+
DEF_REDUCE(detail::KnuthBendixImpl<RPOSet>, detail::CongruenceCommon);
954+
955+
DEF_REDUCE(KnuthBendixStringRPOTrie, detail::KnuthBendixImpl<RPOTrie>);
956+
DEF_REDUCE(KnuthBendixStringRPOSet, detail::KnuthBendixImpl<RPOSet>);
957+
DEF_REDUCE(KnuthBendixWordRPOTrie, detail::KnuthBendixImpl<RPOTrie>);
958+
DEF_REDUCE(KnuthBendixWordRPOSet, detail::KnuthBendixImpl<RPOSet>);
959+
841960
DEF_REDUCE(Congruence<word_type>, detail::CongruenceCommon);
842961
DEF_REDUCE(Congruence<std::string>, detail::CongruenceCommon);
843962

@@ -896,6 +1015,14 @@ This function returns the generating pairs of the congruence as added via
8961015
DEF_GENERATING_PAIRS(KnuthBendixWordLenLexSet,
8971016
detail::KnuthBendixImpl<LenLexSet>);
8981017

1018+
DEF_GENERATING_PAIRS(KnuthBendixStringRPOTrie,
1019+
detail::KnuthBendixImpl<RPOTrie>);
1020+
DEF_GENERATING_PAIRS(KnuthBendixStringRPOSet,
1021+
detail::KnuthBendixImpl<RPOSet>);
1022+
DEF_GENERATING_PAIRS(KnuthBendixWordRPOTrie,
1023+
detail::KnuthBendixImpl<RPOTrie>);
1024+
DEF_GENERATING_PAIRS(KnuthBendixWordRPOSet, detail::KnuthBendixImpl<RPOSet>);
1025+
8991026
DEF_GENERATING_PAIRS(Congruence<word_type>, detail::CongruenceCommon);
9001027
DEF_GENERATING_PAIRS(Congruence<std::string>, detail::CongruenceCommon);
9011028

@@ -955,6 +1082,11 @@ presentation, then this presentation is returned by this function.
9551082
DEF_PRESENTATION(KnuthBendixWordLenLexSet,
9561083
detail::KnuthBendixImpl<LenLexSet>);
9571084

1085+
DEF_PRESENTATION(KnuthBendixStringRPOTrie, detail::KnuthBendixImpl<RPOTrie>);
1086+
DEF_PRESENTATION(KnuthBendixStringRPOSet, detail::KnuthBendixImpl<RPOSet>);
1087+
DEF_PRESENTATION(KnuthBendixWordRPOTrie, detail::KnuthBendixImpl<RPOTrie>);
1088+
DEF_PRESENTATION(KnuthBendixWordRPOSet, detail::KnuthBendixImpl<RPOSet>);
1089+
9581090
DEF_PRESENTATION(Congruence<word_type>, detail::CongruenceCommon);
9591091
DEF_PRESENTATION(Congruence<std::string>, detail::CongruenceCommon);
9601092

@@ -1023,6 +1155,11 @@ triggers a full enumeration of *{var}*.
10231155
DEF_PARTITION(KnuthBendixWordLenLexTrie);
10241156
DEF_PARTITION(KnuthBendixWordLenLexSet);
10251157

1158+
DEF_PARTITION(KnuthBendixStringRPOTrie);
1159+
DEF_PARTITION(KnuthBendixStringRPOSet);
1160+
DEF_PARTITION(KnuthBendixWordRPOTrie);
1161+
DEF_PARTITION(KnuthBendixWordRPOSet);
1162+
10261163
DEF_PARTITION(Congruence<word_type>);
10271164
DEF_PARTITION(Congruence<std::string>);
10281165

@@ -1090,6 +1227,11 @@ instance *{var}*.
10901227
DEF_NON_TRIVIAL_CLASSES(KnuthBendixWordLenLexTrie);
10911228
DEF_NON_TRIVIAL_CLASSES(KnuthBendixWordLenLexSet);
10921229

1230+
DEF_NON_TRIVIAL_CLASSES(KnuthBendixStringRPOTrie);
1231+
DEF_NON_TRIVIAL_CLASSES(KnuthBendixStringRPOSet);
1232+
DEF_NON_TRIVIAL_CLASSES(KnuthBendixWordRPOTrie);
1233+
DEF_NON_TRIVIAL_CLASSES(KnuthBendixWordRPOSet);
1234+
10931235
DEF_NON_TRIVIAL_CLASSES(Congruence<word_type>);
10941236
DEF_NON_TRIVIAL_CLASSES(Congruence<std::string>);
10951237

@@ -1153,6 +1295,11 @@ the congruence represented by an instance of :any:`{name}`.
11531295
DEF_NORMAL_FORMS(KnuthBendixWordLenLexTrie);
11541296
DEF_NORMAL_FORMS(KnuthBendixWordLenLexSet);
11551297

1298+
DEF_NORMAL_FORMS(KnuthBendixStringRPOTrie);
1299+
DEF_NORMAL_FORMS(KnuthBendixStringRPOSet);
1300+
DEF_NORMAL_FORMS(KnuthBendixWordRPOTrie);
1301+
DEF_NORMAL_FORMS(KnuthBendixWordRPOSet);
1302+
11561303
// TODO(1) uncomment when implemented in libsemigroups
11571304
// DEF_NORMAL_FORMS(Congruence<word_type>);
11581305
// DEF_NORMAL_FORMS(Congruence<std::string>);

src/knuth-bendix-impl.cpp

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -516,5 +516,8 @@ infinite; ``False`` is returned if it is not.
516516
m, "KnuthBendixImplLenLexSet");
517517
detail::bind_detail_knuth_bendix_impl<LenLexTrie>(
518518
m, "KnuthBendixImplLenLexTrie");
519+
520+
detail::bind_detail_knuth_bendix_impl<RPOSet>(m, "KnuthBendixImplRPOSet");
521+
detail::bind_detail_knuth_bendix_impl<RPOTrie>(m, "KnuthBendixImplRPOTrie");
519522
}
520523
} // namespace libsemigroups

src/knuth-bendix.cpp

Lines changed: 18 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -330,8 +330,10 @@ Check if all rules are reduced with respect to each other.
330330

331331
template <typename Word, typename Rewriter>
332332
void bind_normal_form_range(py::module& m, char const* name) {
333-
using NormalFormRange
334-
= detail::KnuthBendixNormalFormRange<Word, Rewriter, ShortLexCompare>;
333+
using NormalFormRange = detail::KnuthBendixNormalFormRange<
334+
Word,
335+
Rewriter,
336+
typename Rewriter::reduction_order>;
335337
py::class_<NormalFormRange> thing(m, name);
336338

337339
thing.def("__repr__", [](NormalFormRange const& nfr) {
@@ -459,6 +461,11 @@ redundant in this way, then ``None`` is returned.
459461
"KnuthBendixStringLenLexTrie");
460462
bind_knuth_bendix<std::string, LenLexSet>(m, "KnuthBendixStringLenLexSet");
461463

464+
bind_knuth_bendix<word_type, RPOTrie>(m, "KnuthBendixWordRPOTrie");
465+
bind_knuth_bendix<word_type, RPOSet>(m, "KnuthBendixWordRPOSet");
466+
bind_knuth_bendix<std::string, RPOTrie>(m, "KnuthBendixStringRPOTrie");
467+
bind_knuth_bendix<std::string, RPOSet>(m, "KnuthBendixStringRPOSet");
468+
462469
bind_normal_form_range<word_type, LenLexTrie>(
463470
m, "KnuthBendixNormalFormRangeWordLenLexTrie");
464471
bind_normal_form_range<word_type, LenLexSet>(
@@ -468,6 +475,15 @@ redundant in this way, then ``None`` is returned.
468475
bind_normal_form_range<std::string, LenLexSet>(
469476
m, "KnuthBendixNormalFormRangeStringLenLexSet");
470477

478+
bind_normal_form_range<word_type, RPOTrie>(
479+
m, "KnuthBendixNormalFormRangeWordRPOTrie");
480+
bind_normal_form_range<word_type, RPOSet>(
481+
m, "KnuthBendixNormalFormRangeWordRPOSet");
482+
bind_normal_form_range<std::string, RPOTrie>(
483+
m, "KnuthBendixNormalFormRangeStringRPOTrie");
484+
bind_normal_form_range<std::string, RPOSet>(
485+
m, "KnuthBendixNormalFormRangeStringRPOSet");
486+
471487
bind_redundant_rule<std::string>(m);
472488
bind_redundant_rule<word_type>(m);
473489
}

0 commit comments

Comments
 (0)