diff --git a/Project.toml b/Project.toml
index f02831d..b7dec13 100644
--- a/Project.toml
+++ b/Project.toml
@@ -12,6 +12,7 @@ libsemigroups_jll = "99c76e05-e2a6-5e47-b69a-d74ec2f0d12c"
[compat]
AbstractAlgebra = "0.43, 0.48"
CxxWrap = "0.17"
+libsemigroups_jll = "=3.5.5"
julia = "1.9"
[extras]
diff --git a/deps/src/CMakeLists.txt b/deps/src/CMakeLists.txt
index 37a9edd..da75f48 100644
--- a/deps/src/CMakeLists.txt
+++ b/deps/src/CMakeLists.txt
@@ -45,6 +45,7 @@ message(STATUS "libsemigroups libraries: ${LIBSEMIGROUPS_LIBRARIES}")
add_library(libsemigroups_julia SHARED
libsemigroups_julia.cpp
bmat8.cpp
+ cong-common.cpp
constants.cpp
froidure-pin-base.cpp
froidure-pin.cpp
@@ -56,6 +57,7 @@ add_library(libsemigroups_julia SHARED
word-range.cpp
presentation.cpp
presentation-examples.cpp
+ knuth-bendix.cpp
)
# Include directories
diff --git a/deps/src/cong-common.cpp b/deps/src/cong-common.cpp
new file mode 100644
index 0000000..2352da4
--- /dev/null
+++ b/deps/src/cong-common.cpp
@@ -0,0 +1,166 @@
+//
+// Copyright (c) 2026 James W. Swent
+//
+// This program is free software: you can redistribute it and/or modify
+// it under the terms of the GNU General Public License as published by
+// the Free Software Foundation, either version 3 of the License, or
+// (at your option) any later version.
+//
+// This program is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+// GNU General Public License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program. If not, see .
+//
+
+// CRITICAL: libsemigroups_julia.hpp MUST be included first (fmt consteval fix)
+#include "libsemigroups_julia.hpp"
+
+#include
+#include
+#include
+#include
+#include
+
+#include
+
+#include
+#include
+#include
+#include
+
+namespace jlcxx {
+ template <>
+ struct IsMirroredType
+ : std::false_type {};
+
+ template <>
+ struct SuperType {
+ using type = libsemigroups::Runner;
+ };
+} // namespace jlcxx
+
+namespace libsemigroups_julia {
+
+ namespace {
+ template
+ void define_cong_common_word_helpers(jl::Module& m) {
+ using Word = typename Thing::native_word_type;
+
+ // reduce (triggers full enumeration)
+ m.method("cong_common_reduce",
+ [](Thing& self, jlcxx::ArrayRef w) -> Word {
+ Word input(w.begin(), w.end());
+ return libsemigroups::congruence_common::reduce(self, input);
+ });
+
+ // reduce_no_run (no enumeration)
+ m.method("cong_common_reduce_no_run",
+ [](Thing const& self, jlcxx::ArrayRef w) -> Word {
+ Word input(w.begin(), w.end());
+ return libsemigroups::congruence_common::reduce_no_run(self,
+ input);
+ });
+
+ // contains (triggers full enumeration)
+ m.method("cong_common_contains",
+ [](Thing& self,
+ jlcxx::ArrayRef u,
+ jlcxx::ArrayRef v) -> bool {
+ Word uw(u.begin(), u.end());
+ Word vw(v.begin(), v.end());
+ return libsemigroups::congruence_common::contains(
+ self, uw, vw);
+ });
+
+ // currently_contains (no enumeration, returns tril)
+ m.method("cong_common_currently_contains",
+ [](Thing const& self,
+ jlcxx::ArrayRef u,
+ jlcxx::ArrayRef v) -> libsemigroups::tril {
+ Word uw(u.begin(), u.end());
+ Word vw(v.begin(), v.end());
+ return libsemigroups::congruence_common::currently_contains(
+ self, uw, vw);
+ });
+
+ // add_generating_pair!
+ m.method("cong_common_add_generating_pair!",
+ [](Thing& self,
+ jlcxx::ArrayRef u,
+ jlcxx::ArrayRef v) {
+ Word uw(u.begin(), u.end());
+ Word vw(v.begin(), v.end());
+ libsemigroups::congruence_common::add_generating_pair(
+ self, uw, vw);
+ });
+
+ m.method("cong_common_partition",
+ [](Thing& self, jlcxx::ArrayRef words)
+ -> std::vector> {
+ std::vector input;
+ input.reserve(words.size());
+ for (jl_value_t* word_value : words) {
+ auto word = jlcxx::ArrayRef(
+ reinterpret_cast(word_value));
+ input.emplace_back(word.begin(), word.end());
+ }
+ return libsemigroups::congruence_common::partition(
+ self, input.begin(), input.end());
+ });
+ }
+
+ template
+ void define_cong_common_normal_forms(jl::Module& m) {
+ using Word = typename Thing::native_word_type;
+
+ // normal_forms() returns an rx-style range; use
+ // .at_end()/.get()/.next().
+ m.method(
+ "cong_common_normal_forms", [](Thing& self) -> std::vector {
+ std::vector result;
+ auto range = libsemigroups::congruence_common::normal_forms(self);
+ while (!range.at_end()) {
+ result.push_back(range.get());
+ range.next();
+ }
+ return result;
+ });
+ }
+
+ template
+ void define_cong_common_non_trivial_classes(jl::Module& m) {
+ using Word = typename Thing::native_word_type;
+
+ m.method("cong_common_non_trivial_classes",
+ [](Thing& x, Thing& y) -> std::vector> {
+ return libsemigroups::congruence_common::non_trivial_classes(
+ x, y);
+ });
+ }
+ } // namespace
+
+ void define_cong_common(jl::Module& m) {
+ using libsemigroups::Runner;
+ using CongruenceCommon = libsemigroups::detail::CongruenceCommon;
+
+ // No constructors: CongruenceCommon is a shared implementation base.
+ // Derived algorithms register their concrete methods on their own types.
+ m.add_type("CongruenceCommon",
+ jlcxx::julia_base_type());
+ }
+
+ void define_knuth_bendix_cong_common_helpers(jl::Module& m) {
+ using libsemigroups::word_type;
+ using KB = libsemigroups::KnuthBendix;
+
+ define_cong_common_word_helpers(m);
+ define_cong_common_normal_forms(m);
+ define_cong_common_non_trivial_classes(m);
+ }
+
+} // namespace libsemigroups_julia
diff --git a/deps/src/constants.cpp b/deps/src/constants.cpp
index d8b064d..99b73fe 100644
--- a/deps/src/constants.cpp
+++ b/deps/src/constants.cpp
@@ -57,6 +57,14 @@ namespace libsemigroups_julia {
m.method("NEGATIVE_INFINITY_Int64",
[]() -> int64_t { return libsemigroups::NEGATIVE_INFINITY; });
+ // congruence_kind enum for sided-ness of a congruence
+ m.add_bits("congruence_kind",
+ jl::julia_type("CppEnum"));
+ m.set_const("congruence_kind_onesided",
+ libsemigroups::congruence_kind::onesided);
+ m.set_const("congruence_kind_twosided",
+ libsemigroups::congruence_kind::twosided);
+
// tril enum for three-valued logic (true, false, unknown)
m.add_bits("tril", jl::julia_type("CppEnum"));
m.set_const("tril_FALSE", libsemigroups::tril::FALSE);
diff --git a/deps/src/knuth-bendix.cpp b/deps/src/knuth-bendix.cpp
new file mode 100644
index 0000000..fbe6da3
--- /dev/null
+++ b/deps/src/knuth-bendix.cpp
@@ -0,0 +1,261 @@
+//
+// Semigroups.jl
+// Copyright (C) 2026, James W. Swent
+//
+// This program is free software: you can redistribute it and/or modify
+// it under the terms of the GNU General Public License as published by
+// the Free Software Foundation, either version 3 of the License, or
+// (at your option) any later version.
+//
+// This program is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+// GNU General Public License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program. If not, see .
+//
+
+// CRITICAL: libsemigroups_julia.hpp MUST be included first (fmt consteval fix)
+#include "libsemigroups_julia.hpp"
+
+#include
+#include
+#include
+#include
+
+#include
+#include
+#include
+#include
+#include
+#include
+#include
+#include
+
+namespace jlcxx {
+ template <>
+ struct IsMirroredType<
+ libsemigroups::detail::KnuthBendixImpl>
+ : std::false_type {};
+
+ template <>
+ struct IsMirroredType<
+ libsemigroups::KnuthBendix>
+ : std::false_type {};
+
+ template <>
+ struct SuperType<
+ libsemigroups::detail::KnuthBendixImpl> {
+ using type = libsemigroups::detail::CongruenceCommon;
+ };
+
+ template <>
+ struct SuperType<
+ libsemigroups::KnuthBendix> {
+ using type = libsemigroups::detail::KnuthBendixImpl<
+ libsemigroups::detail::RewriteTrie,
+ libsemigroups::ShortLexCompare>;
+ };
+} // namespace jlcxx
+
+namespace libsemigroups_julia {
+
+ void define_knuth_bendix(jl::Module& m) {
+ using libsemigroups::congruence_kind;
+ using libsemigroups::Presentation;
+ using libsemigroups::word_type;
+
+ using CongruenceCommon = libsemigroups::detail::CongruenceCommon;
+ using KBImpl = libsemigroups::detail::KnuthBendixImpl<
+ libsemigroups::detail::RewriteTrie,
+ libsemigroups::ShortLexCompare>;
+ using KB = libsemigroups::KnuthBendix;
+
+ ////////////////////////////////////////////////////////////////////////
+ // overlap enum
+ ////////////////////////////////////////////////////////////////////////
+
+ m.add_bits("overlap", jl::julia_type("CppEnum"));
+ m.set_const("overlap_ABC", KB::options::overlap::ABC);
+ m.set_const("overlap_AB_BC", KB::options::overlap::AB_BC);
+ m.set_const("overlap_MAX_AB_BC", KB::options::overlap::MAX_AB_BC);
+
+ ////////////////////////////////////////////////////////////////////////
+ // Type registration
+ ////////////////////////////////////////////////////////////////////////
+
+ m.add_type("KnuthBendixImplRewriteTrie",
+ jlcxx::julia_base_type());
+ auto type = m.add_type("KnuthBendixRewriteTrie",
+ jlcxx::julia_base_type());
+
+ ////////////////////////////////////////////////////////////////////////
+ // Constructors
+ ////////////////////////////////////////////////////////////////////////
+
+ type.constructor const&>();
+ type.constructor(); // copy ctor
+ type.method("init!", [](KB& self) -> KB& { return self.init(); });
+ type.method("init!",
+ [](KB& self,
+ congruence_kind knd,
+ Presentation const& p) -> KB& {
+ return self.init(knd, p);
+ });
+
+ ////////////////////////////////////////////////////////////////////////
+ // Settings (getter / setter with DISTINCT names)
+ ////////////////////////////////////////////////////////////////////////
+
+ // max_pending_rules
+ type.method("max_pending_rules", [](KB const& self) -> size_t {
+ return self.max_pending_rules();
+ });
+ type.method("set_max_pending_rules!",
+ [](KB& self, size_t val) { self.max_pending_rules(val); });
+
+ // check_confluence_interval
+ type.method("check_confluence_interval", [](KB const& self) -> size_t {
+ return self.check_confluence_interval();
+ });
+ type.method("set_check_confluence_interval!", [](KB& self, size_t val) {
+ self.check_confluence_interval(val);
+ });
+
+ // max_overlap
+ type.method("max_overlap",
+ [](KB const& self) -> size_t { return self.max_overlap(); });
+ type.method("set_max_overlap!",
+ [](KB& self, size_t val) { self.max_overlap(val); });
+
+ // max_rules
+ type.method("max_rules",
+ [](KB const& self) -> size_t { return self.max_rules(); });
+ type.method("set_max_rules!",
+ [](KB& self, size_t val) { self.max_rules(val); });
+
+ // overlap_policy
+ type.method("overlap_policy", [](KB const& self) -> KB::options::overlap {
+ return self.overlap_policy();
+ });
+ type.method("set_overlap_policy!", [](KB& self, KB::options::overlap val) {
+ self.overlap_policy(val);
+ });
+
+ ////////////////////////////////////////////////////////////////////////
+ // Query methods
+ ////////////////////////////////////////////////////////////////////////
+
+ type.method("number_of_active_rules", [](KB const& self) -> size_t {
+ return self.number_of_active_rules();
+ });
+ type.method("number_of_inactive_rules", [](KB const& self) -> size_t {
+ return self.number_of_inactive_rules();
+ });
+ type.method("number_of_pending_rules", [](KB const& self) -> size_t {
+ return self.number_of_pending_rules();
+ });
+ type.method("total_rules",
+ [](KB const& self) -> size_t { return self.total_rules(); });
+
+ type.method("confluent", [](KB& self) -> bool { return self.confluent(); });
+ type.method("confluent_known",
+ [](KB const& self) -> bool { return self.confluent_known(); });
+
+ type.method("number_of_classes",
+ [](KB& self) -> uint64_t { return self.number_of_classes(); });
+
+ type.method("kind",
+ [](KB const& self) -> congruence_kind { return self.kind(); });
+ type.method("number_of_generating_pairs", [](KB const& self) -> size_t {
+ return self.number_of_generating_pairs();
+ });
+ type.method("generating_pairs",
+ [](KB const& self) -> std::vector {
+ auto const& pairs = self.generating_pairs();
+ return std::vector(pairs.begin(), pairs.end());
+ });
+
+ // presentation — return by copy
+ type.method("presentation", [](KB const& self) -> Presentation {
+ return self.presentation();
+ });
+
+ ////////////////////////////////////////////////////////////////////////
+ // Rules access
+ ////////////////////////////////////////////////////////////////////////
+
+ // active_rules — collect the range to a flat vector
+ // (even indices = lhs, odd indices = rhs)
+ // active_rules() returns an rx range — use .at_end()/.get()/.next()
+ m.method("kb_active_rules", [](KB& self) -> std::vector {
+ std::vector result;
+ auto range = self.active_rules();
+ while (!range.at_end()) {
+ auto const& pair = range.get();
+ result.push_back(pair.first);
+ result.push_back(pair.second);
+ range.next();
+ }
+ return result;
+ });
+
+ ////////////////////////////////////////////////////////////////////////
+ // Graph access
+ ////////////////////////////////////////////////////////////////////////
+
+ // gilman_graph — return by const reference (large stable data)
+ type.method("gilman_graph",
+ [](KB& self) -> libsemigroups::WordGraph const& {
+ return self.gilman_graph();
+ });
+
+ // gilman_graph_node_labels — collect to vector of vectors by copy
+ type.method("gilman_graph_node_labels",
+ [](KB& self) -> std::vector {
+ return self.gilman_graph_node_labels();
+ });
+
+ ////////////////////////////////////////////////////////////////////////
+ // Display
+ ////////////////////////////////////////////////////////////////////////
+
+ type.method("to_human_readable_repr", [](KB& self) -> std::string {
+ return libsemigroups::to_human_readable_repr(self);
+ });
+
+ ////////////////////////////////////////////////////////////////////////
+ // Free functions (knuth_bendix:: namespace)
+ ////////////////////////////////////////////////////////////////////////
+
+ // by_overlap_length! (mutating)
+ m.method("kb_by_overlap_length!", [](KB& self) {
+ libsemigroups::knuth_bendix::by_overlap_length(self);
+ });
+
+ // is_reduced
+ m.method("kb_is_reduced", [](KB& self) -> bool {
+ return libsemigroups::knuth_bendix::is_reduced(self);
+ });
+
+ // redundant_rule — takes Presentation and a timeout in
+ // nanoseconds (int64_t), returns an index into p.rules (0-based).
+ // Returns p.rules.size() if no redundant rule was found.
+ m.method("kb_redundant_rule",
+ [](Presentation const& p, int64_t ns) -> size_t {
+ auto it = libsemigroups::knuth_bendix::redundant_rule(
+ p, std::chrono::nanoseconds(ns));
+ return static_cast(std::distance(p.rules.cbegin(), it));
+ });
+ }
+
+} // namespace libsemigroups_julia
diff --git a/deps/src/libsemigroups_julia.cpp b/deps/src/libsemigroups_julia.cpp
index 0cd8b6e..863ed05 100644
--- a/deps/src/libsemigroups_julia.cpp
+++ b/deps/src/libsemigroups_julia.cpp
@@ -32,6 +32,7 @@ namespace libsemigroups_julia {
// Define base types (must be registered before derived types)
define_runner(mod);
+ define_cong_common(mod);
// Define element types
define_transf(mod);
@@ -44,6 +45,8 @@ namespace libsemigroups_julia {
define_froidure_pin(mod);
define_presentation(mod);
define_presentation_examples(mod);
+ define_knuth_bendix(mod);
+ define_knuth_bendix_cong_common_helpers(mod);
}
} // namespace libsemigroups_julia
diff --git a/deps/src/libsemigroups_julia.hpp b/deps/src/libsemigroups_julia.hpp
index 3af5852..be064db 100644
--- a/deps/src/libsemigroups_julia.hpp
+++ b/deps/src/libsemigroups_julia.hpp
@@ -57,6 +57,7 @@ namespace libsemigroups_julia {
void define_constants(jl::Module& mod);
void define_report(jl::Module& mod);
void define_runner(jl::Module& mod);
+ void define_cong_common(jl::Module& mod);
void define_transf(jl::Module& mod);
void define_bmat8(jl::Module& mod);
void define_order(jl::Module& mod);
@@ -66,6 +67,8 @@ namespace libsemigroups_julia {
void define_froidure_pin(jl::Module& mod);
void define_presentation(jl::Module& mod);
void define_presentation_examples(jl::Module& mod);
+ void define_knuth_bendix(jl::Module& mod);
+ void define_knuth_bendix_cong_common_helpers(jl::Module& mod);
} // namespace libsemigroups_julia
diff --git a/docs/Project.toml b/docs/Project.toml
index 1b1e5cd..d71de71 100644
--- a/docs/Project.toml
+++ b/docs/Project.toml
@@ -1,11 +1,8 @@
[deps]
Documenter = "e30172f5-a6a5-5a46-863b-614d45cd2de4"
LiveServer = "16fef848-5104-11e9-1b77-fb7a48bbb589"
-Revise = "295af30f-e4ad-537b-8983-00126c2a3abe"
+Revise = "295af30f-e4ad-537b-8983-00126c2a3abe"
Semigroups = "f8a5e1c0-7b2d-4a3e-9c6f-1d2e3f4a5b6c"
[sources]
Semigroups = {path = ".."}
-
-[compat]
-Documenter = "1"
diff --git a/docs/make.jl b/docs/make.jl
index f0def1e..c66eead 100644
--- a/docs/make.jl
+++ b/docs/make.jl
@@ -66,11 +66,17 @@ makedocs(;
"main-algorithms/core-classes/index.md",
"main-algorithms/core-classes/runner.md",
],
+ "Common congruence helpers" => "main-algorithms/cong-common-helpers.md",
"Froidure-Pin" => [
"Overview" => "main-algorithms/froidure-pin/index.md",
"The FroidurePin type" => "main-algorithms/froidure-pin/froidure-pin.md",
"Helper functions" => "main-algorithms/froidure-pin/helpers.md",
],
+ "Knuth-Bendix" => [
+ "Overview" => "main-algorithms/knuth-bendix/index.md",
+ "The KnuthBendix type" => "main-algorithms/knuth-bendix/knuth-bendix.md",
+ "Helper functions" => "main-algorithms/knuth-bendix/helpers.md",
+ ],
],
],
warnonly = [:missing_docs, :linkcheck, :cross_references],
diff --git a/docs/src/main-algorithms/cong-common-helpers.md b/docs/src/main-algorithms/cong-common-helpers.md
new file mode 100644
index 0000000..10cf0fb
--- /dev/null
+++ b/docs/src/main-algorithms/cong-common-helpers.md
@@ -0,0 +1,122 @@
+# Common congruence helpers
+
+This page documents the helper functions that are shared by every
+congruence-style algorithm in Semigroups.jl. They mirror the
+`libsemigroups::congruence_common::*` namespace and are dispatched on
+[`CongruenceCommon`](@ref Semigroups.CongruenceCommon), so the same
+function names work uniformly across [`KnuthBendix`](@ref
+Semigroups.KnuthBendix) (and, in later phases, `ToddCoxeter`,
+`Kambites`, and `Congruence`).
+
+Words are accepted and returned as 1-based `Vector{Int}` letter indices
+throughout.
+
+!!! warning "v1 limitation"
+ [`KnuthBendix`](@ref Semigroups.KnuthBendix) is the only concrete
+ subtype of [`CongruenceCommon`](@ref Semigroups.CongruenceCommon)
+ bound in v1. The same helpers will apply to `ToddCoxeter`,
+ `Kambites`, and `Congruence` once those types land.
+
+!!! note
+ `Semigroups.reduce` and `Semigroups.contains` are not exported, to
+ avoid shadowing `Base.reduce` and `Base.contains`. Call them with
+ the module-qualified form: `Semigroups.reduce(cong, w)`,
+ `Semigroups.contains(cong, u, v)`.
+
+## Table of contents
+
+| Section | Description |
+| ------- | ----------- |
+| [Add generating pairs](@ref) | Extend a congruence with extra generating pairs. |
+| [Containment](@ref) | Test whether two words are equivalent under a congruence. |
+| [Reduce a word](@ref) | Reduce a word to a normal form (or a current-rules form). |
+| [Normal forms](@ref) | Enumerate one normal form per congruence class. |
+| [Partitioning](@ref) | Partition input words into congruence classes. |
+
+```@docs
+Semigroups.CongruenceCommon
+```
+
+## Add generating pairs
+
+### Contents
+
+| Function | Description |
+| -------- | ----------- |
+| [`add_generating_pair!`](@ref Semigroups.add_generating_pair!(::CongruenceCommon, ::AbstractVector{<:Integer}, ::AbstractVector{<:Integer})) | Add an extra generating pair `(u, v)` to a congruence. |
+
+### Full API
+
+```@docs
+Semigroups.add_generating_pair!(::CongruenceCommon, ::AbstractVector{<:Integer}, ::AbstractVector{<:Integer})
+```
+
+## Containment
+
+These functions test whether two words are equivalent under a
+congruence. The `currently_*` variant performs no enumeration and may
+return [`tril_unknown`](@ref Semigroups.tril_unknown).
+
+### Contents
+
+| Function | Description |
+| -------- | ----------- |
+| [`Semigroups.contains`](@ref Semigroups.contains(::CongruenceCommon, ::AbstractVector{<:Integer}, ::AbstractVector{<:Integer})) | Test equivalence; triggers a full run. |
+| [`currently_contains`](@ref Semigroups.currently_contains(::CongruenceCommon, ::AbstractVector{<:Integer}, ::AbstractVector{<:Integer})) | Test equivalence using current rules; returns [`tril`](@ref Semigroups.tril). |
+
+### Full API
+
+```@docs
+Semigroups.contains(::CongruenceCommon, ::AbstractVector{<:Integer}, ::AbstractVector{<:Integer})
+Semigroups.currently_contains(::CongruenceCommon, ::AbstractVector{<:Integer}, ::AbstractVector{<:Integer})
+```
+
+## Reduce a word
+
+These functions return a word equivalent to the input under the
+congruence. The `_no_run` variant uses only the current rules and does
+not trigger an enumeration.
+
+### Contents
+
+| Function | Description |
+| -------- | ----------- |
+| [`Semigroups.reduce`](@ref Semigroups.reduce(::CongruenceCommon, ::AbstractVector{<:Integer})) | Reduce to a normal form; triggers a full run. |
+| [`reduce_no_run`](@ref Semigroups.reduce_no_run(::CongruenceCommon, ::AbstractVector{<:Integer})) | Reduce using current rules; no run. |
+
+### Full API
+
+```@docs
+Semigroups.reduce(::CongruenceCommon, ::AbstractVector{<:Integer})
+Semigroups.reduce_no_run(::CongruenceCommon, ::AbstractVector{<:Integer})
+```
+
+## Normal forms
+
+### Contents
+
+| Function | Description |
+| -------- | ----------- |
+| [`normal_forms`](@ref Semigroups.normal_forms(::CongruenceCommon)) | One normal form per congruence class. |
+
+### Full API
+
+```@docs
+Semigroups.normal_forms(::CongruenceCommon)
+```
+
+## Partitioning
+
+### Contents
+
+| Function | Description |
+| -------- | ----------- |
+| [`partition`](@ref Semigroups.partition(::CongruenceCommon, ::AbstractVector{<:AbstractVector{<:Integer}})) | Partition a list of words into congruence classes. |
+| [`non_trivial_classes`](@ref Semigroups.non_trivial_classes(::CongruenceCommon, ::CongruenceCommon)) | Classes of size ≥ 2 in the partition of the normal forms of one congruence by another. |
+
+### Full API
+
+```@docs
+Semigroups.partition(::CongruenceCommon, ::AbstractVector{<:AbstractVector{<:Integer}})
+Semigroups.non_trivial_classes(::CongruenceCommon, ::CongruenceCommon)
+```
diff --git a/docs/src/main-algorithms/knuth-bendix/helpers.md b/docs/src/main-algorithms/knuth-bendix/helpers.md
new file mode 100644
index 0000000..ff35f75
--- /dev/null
+++ b/docs/src/main-algorithms/knuth-bendix/helpers.md
@@ -0,0 +1,54 @@
+# Knuth-Bendix helper functions
+
+This page collects the free functions that are specific to the
+[`KnuthBendix`](@ref Semigroups.KnuthBendix) type. They mirror the
+`libsemigroups::knuth_bendix::*` namespace.
+
+The shared helpers re-exported by `knuth_bendix::` (`reduce`, `contains`,
+`currently_contains`, `add_generating_pair!`, `normal_forms`, `partition`,
+and `non_trivial_classes`) are documented on the
+[Common congruence helpers](../cong-common-helpers.md) page; they apply to
+every congruence type, including `KnuthBendix`.
+
+## Table of contents
+
+| Section | Description |
+| ------- | ----------- |
+| [Running variants](@ref) | Alternate entry points for the Knuth-Bendix algorithm. |
+| [Rule utilities](@ref) | Checking reducedness and finding redundant rules. |
+
+## Running variants
+
+These run the Knuth-Bendix algorithm with a different scheduling
+discipline from the inherited [`run!`](@ref Semigroups.run!).
+
+### Contents
+
+| Function | Description |
+| -------- | ----------- |
+| [`by_overlap_length!`](@ref Semigroups.by_overlap_length!(::KnuthBendix)) | Run the algorithm ordered by overlap length. |
+
+### Full API
+
+```@docs
+Semigroups.by_overlap_length!(::KnuthBendix)
+```
+
+## Rule utilities
+
+Helpers for inspecting and reasoning about the rules of a rewriting
+system.
+
+### Contents
+
+| Function | Description |
+| -------- | ----------- |
+| [`is_reduced`](@ref Semigroups.is_reduced(::KnuthBendix)) | Check whether all rules are reduced with respect to each other. |
+| [`redundant_rule`](@ref Semigroups.redundant_rule(::Presentation, ::TimePeriod)) | Find a rule of a presentation that follows from the others. |
+
+### Full API
+
+```@docs
+Semigroups.is_reduced(::KnuthBendix)
+Semigroups.redundant_rule(::Presentation, ::TimePeriod)
+```
diff --git a/docs/src/main-algorithms/knuth-bendix/index.md b/docs/src/main-algorithms/knuth-bendix/index.md
new file mode 100644
index 0000000..96b9169
--- /dev/null
+++ b/docs/src/main-algorithms/knuth-bendix/index.md
@@ -0,0 +1,26 @@
+# Knuth-Bendix
+
+This section contains documentation related to the implementation of the
+Knuth-Bendix completion algorithm in Semigroups.jl.
+
+The Knuth-Bendix algorithm takes a finitely presented semigroup or monoid and
+attempts to compute a confluent rewriting system — a finite set of rules that
+reduces every word to a unique normal form. When the algorithm terminates, the
+congruence is decidable and normal forms enumerate the elements of the
+semigroup.
+
+!!! warning "v1 limitation"
+ Semigroups.jl v1 binds `KnuthBendix{word_type, RewriteTrie}` only.
+ Letter indices are 1-based `Int` values throughout the Julia API.
+
+## Contents
+
+| Page | Description |
+| ---- | ----------- |
+| [The KnuthBendix type](knuth-bendix.md) | The main [`KnuthBendix`](@ref Semigroups.KnuthBendix) type: construction, settings, queries, and graph access. |
+| [Helper functions](helpers.md) | KnuthBendix-specific free functions: running by overlap length, checking reducedness, and finding redundant rules. |
+
+The shared word-operation and class-enumeration helpers (`reduce`,
+`contains`, `currently_contains`, `add_generating_pair!`, `normal_forms`,
+`partition`, `non_trivial_classes`) are documented on the
+[Common congruence helpers](../cong-common-helpers.md) page.
diff --git a/docs/src/main-algorithms/knuth-bendix/knuth-bendix.md b/docs/src/main-algorithms/knuth-bendix/knuth-bendix.md
new file mode 100644
index 0000000..7529293
--- /dev/null
+++ b/docs/src/main-algorithms/knuth-bendix/knuth-bendix.md
@@ -0,0 +1,148 @@
+# The KnuthBendix type
+
+This page documents the [`KnuthBendix`](@ref Semigroups.KnuthBendix) type,
+which implements the Knuth-Bendix completion algorithm for finitely presented
+semigroups and monoids.
+
+`KnuthBendix` is a subtype of [`Runner`](@ref Semigroups.Runner), so all
+runner methods ([`run!`](@ref), [`run_for!`](@ref), [`finished`](@ref), etc.)
+are available.
+
+## Table of contents
+
+| Section | Description |
+| ------- | ----------- |
+| [Construction and re-initialization](@ref) | Constructors and `init!`. |
+| [Settings](@ref) | Overlap policy, rule limits, confluence-check interval. |
+| [Queries](@ref) | Confluence state, rule counts, class count. |
+| [Presentation and generating pairs](@ref) | Access the underlying presentation and extra generating pairs. |
+| [Word operations](@ref) | Reduce words, test containment, add generating pairs. |
+| [Rules access](@ref) | Enumerate active rules. |
+| [Graph access](@ref) | Gilman WordGraph and its node labels. |
+| [Display and copy](@ref) | `show`, `copy`, `length`. |
+
+```@docs
+Semigroups.KnuthBendix
+```
+
+## Construction and re-initialization
+
+| Function | Description |
+| -------- | ----------- |
+| `KnuthBendix(kind, p)` | Construct from a [`congruence_kind`](@ref Semigroups.congruence_kind) and a [`Presentation`](@ref Semigroups.Presentation). |
+| `KnuthBendix(other)` | Copy an existing `KnuthBendix`. |
+| [`init!(kb)`](@ref Semigroups.init!(::KnuthBendix)) | Reset to default-constructed state or reinitialize from a new kind and presentation. |
+
+```@docs
+Semigroups.init!(::KnuthBendix)
+```
+
+## Settings
+
+| Function | Description |
+| -------- | ----------- |
+| [`max_pending_rules(kb)`](@ref Semigroups.max_pending_rules(::KnuthBendix)) | Get the pending-rule batch size (default: `128`). |
+| [`max_pending_rules!(kb, n)`](@ref Semigroups.max_pending_rules!(::KnuthBendix, ::Integer)) | Set the pending-rule batch size. |
+| [`check_confluence_interval(kb)`](@ref Semigroups.check_confluence_interval(::KnuthBendix)) | Get the confluence-check interval (default: `4096`). |
+| [`check_confluence_interval!(kb, n)`](@ref Semigroups.check_confluence_interval!(::KnuthBendix, ::Integer)) | Set the confluence-check interval. |
+| [`max_overlap(kb)`](@ref Semigroups.max_overlap(::KnuthBendix)) | Get the maximum overlap length. |
+| [`max_overlap!(kb, n)`](@ref Semigroups.max_overlap!(::KnuthBendix, ::Integer)) | Set the maximum overlap length. |
+| [`max_rules(kb)`](@ref Semigroups.max_rules(::KnuthBendix)) | Get the approximate maximum number of rules (default: `POSITIVE_INFINITY`). |
+| [`max_rules!(kb, n)`](@ref Semigroups.max_rules!(::KnuthBendix, ::Integer)) | Set the approximate maximum number of rules. |
+| [`overlap_policy(kb)`](@ref Semigroups.overlap_policy(::KnuthBendix)) | Get the overlap measurement policy. |
+| [`overlap_policy!(kb, val)`](@ref Semigroups.overlap_policy!(::KnuthBendix, ::Any)) | Set the overlap measurement policy. |
+
+```@docs
+Semigroups.overlap_ABC
+Semigroups.overlap_AB_BC
+Semigroups.overlap_MAX_AB_BC
+Semigroups.max_pending_rules(::KnuthBendix)
+Semigroups.max_pending_rules!(::KnuthBendix, ::Integer)
+Semigroups.check_confluence_interval(::KnuthBendix)
+Semigroups.check_confluence_interval!(::KnuthBendix, ::Integer)
+Semigroups.max_overlap(::KnuthBendix)
+Semigroups.max_overlap!(::KnuthBendix, ::Integer)
+Semigroups.max_rules(::KnuthBendix)
+Semigroups.max_rules!(::KnuthBendix, ::Integer)
+Semigroups.overlap_policy(::KnuthBendix)
+Semigroups.overlap_policy!(::KnuthBendix, ::Any)
+```
+
+## Queries
+
+| Function | Description |
+| -------- | ----------- |
+| [`confluent(kb)`](@ref Semigroups.confluent(::KnuthBendix)) | Check if the system is confluent. |
+| [`confluent_known(kb)`](@ref Semigroups.confluent_known(::KnuthBendix)) | Check if confluence status is already known. |
+| [`number_of_classes(kb)`](@ref Semigroups.number_of_classes(::KnuthBendix)) | Number of congruence classes (triggers full run). |
+| [`number_of_active_rules(kb)`](@ref Semigroups.number_of_active_rules(::KnuthBendix)) | Current number of active rules. |
+| [`number_of_inactive_rules(kb)`](@ref Semigroups.number_of_inactive_rules(::KnuthBendix)) | Current number of inactive rules. |
+| [`number_of_pending_rules(kb)`](@ref Semigroups.number_of_pending_rules(::KnuthBendix)) | Number of pending (unprocessed) rules. |
+| [`total_rules(kb)`](@ref Semigroups.total_rules(::KnuthBendix)) | Total rule instances ever created. |
+
+```@docs
+Semigroups.confluent(::KnuthBendix)
+Semigroups.confluent_known(::KnuthBendix)
+Semigroups.number_of_classes(::KnuthBendix)
+Semigroups.number_of_active_rules(::KnuthBendix)
+Semigroups.number_of_inactive_rules(::KnuthBendix)
+Semigroups.number_of_pending_rules(::KnuthBendix)
+Semigroups.total_rules(::KnuthBendix)
+```
+
+## Presentation and generating pairs
+
+| Function | Description |
+| -------- | ----------- |
+| [`kind(kb)`](@ref Semigroups.kind(::KnuthBendix)) | Congruence kind (`twosided` or `onesided`). |
+| [`presentation(kb)`](@ref Semigroups.presentation(::KnuthBendix)) | Copy of the underlying presentation. |
+| [`number_of_generating_pairs(kb)`](@ref Semigroups.number_of_generating_pairs(::KnuthBendix)) | Number of extra generating pairs. |
+| [`generating_pairs(kb)`](@ref Semigroups.generating_pairs(::KnuthBendix)) | Extra generating pairs as 1-based word tuples. |
+
+```@docs
+Semigroups.kind(::KnuthBendix)
+Semigroups.presentation(::KnuthBendix)
+Semigroups.number_of_generating_pairs(::KnuthBendix)
+Semigroups.generating_pairs(::KnuthBendix)
+```
+
+## Word operations
+
+These functions are defined on
+[`CongruenceCommon`](@ref Semigroups.CongruenceCommon) and work on all
+congruence types, including `KnuthBendix`. Words are given and returned as
+1-based `Vector{Int}` letter indices.
+
+!!! note
+ `Semigroups.reduce` and `Semigroups.contains` are not exported to avoid
+ shadowing `Base.reduce`. Use the module-qualified form:
+ `Semigroups.reduce(kb, w)`, `Semigroups.contains(kb, u, v)`.
+
+| Function | Description |
+| -------- | ----------- |
+| `Semigroups.reduce(kb, w)` | Reduce a word to normal form (triggers full run). |
+| `reduce_no_run(kb, w)` | Reduce using current rules only (no run). |
+| `Semigroups.contains(kb, u, v)` | Test if two words are congruent (triggers full run). |
+| `currently_contains(kb, u, v)` | Test containment using current rules (no run); returns [`tril`](@ref Semigroups.tril). |
+| `add_generating_pair!(kb, u, v)` | Add an extra generating pair. |
+
+## Rules access
+
+```@docs
+Semigroups.active_rules(::KnuthBendix)
+```
+
+## Graph access
+
+```@docs
+Semigroups.gilman_graph(::KnuthBendix)
+Semigroups.gilman_graph_node_labels(::KnuthBendix)
+```
+
+## Display and copy
+
+```@docs
+Base.length(::KnuthBendix)
+Base.show(::IO, ::KnuthBendix)
+Base.copy(::KnuthBendix)
+```
diff --git a/src/Semigroups.jl b/src/Semigroups.jl
index f8f88e1..23ac534 100644
--- a/src/Semigroups.jl
+++ b/src/Semigroups.jl
@@ -70,6 +70,8 @@ include("word-range.jl")
include("word-graph.jl")
include("presentation.jl")
include("presentation-examples.jl")
+include("cong-common.jl")
+include("knuth-bendix.jl")
# High-level element types
include("bmat8.jl")
@@ -91,6 +93,7 @@ end
export enable_debug, is_debug, LibsemigroupsError, ReportGuard
export UNDEFINED, POSITIVE_INFINITY, NEGATIVE_INFINITY, LIMIT_MAX
export Runner, RunnerState
+export CongruenceCommon
export STATE_NEVER_RUN, STATE_RUNNING_TO_FINISH, STATE_RUNNING_FOR
export STATE_RUNNING_UNTIL, STATE_TIMED_OUT, STATE_STOPPED_BY_PREDICATE
export STATE_NOT_RUNNING, STATE_DEAD
@@ -99,6 +102,7 @@ export finished, started, running, timed_out, stopped, dead
export stopped_by_predicate, running_for, running_until
export current_state, running_for_how_long
export report_why_we_stopped, string_why_we_stopped
+export congruence_kind, onesided, twosided
export tril, tril_FALSE, tril_TRUE, tril_unknown, tril_to_bool
export is_undefined, is_positive_infinity, is_negative_infinity, is_limit_max
@@ -158,6 +162,23 @@ export sigma_plactic_monoid
export renner_type_B_monoid, renner_type_D_monoid
export not_renner_type_B_monoid, not_renner_type_D_monoid
+# KnuthBendix
+export KnuthBendix
+export overlap_ABC, overlap_AB_BC, overlap_MAX_AB_BC
+export max_pending_rules, max_pending_rules!
+export check_confluence_interval, check_confluence_interval!
+export max_overlap, max_overlap!, max_rules, max_rules!
+export overlap_policy, overlap_policy!
+export number_of_active_rules, number_of_inactive_rules
+export number_of_pending_rules, total_rules
+export confluent, confluent_known, number_of_classes
+export kind, number_of_generating_pairs, generating_pairs, presentation
+export reduce_no_run, currently_contains
+export add_generating_pair!
+export active_rules, gilman_graph, gilman_graph_node_labels
+export by_overlap_length!, is_reduced, redundant_rule
+export normal_forms, partition, non_trivial_classes
+
# Transformation types and functions
export Transf, PPerm, Perm
export degree, rank, image, domain, inverse
diff --git a/src/cong-common.jl b/src/cong-common.jl
new file mode 100644
index 0000000..182ec3d
--- /dev/null
+++ b/src/cong-common.jl
@@ -0,0 +1,352 @@
+# Copyright (c) 2026, James W. Swent
+#
+# Distributed under the terms of the GPL license version 3.
+
+"""
+cong-common.jl - shared CongruenceCommon helper wrappers
+"""
+
+"""
+ CongruenceCommon
+
+Abstract supertype shared by every congruence-style algorithm in
+Semigroups.jl. The helpers documented on the
+[Common congruence helpers](../cong-common-helpers.md) page are defined
+on this supertype and dispatch to whichever concrete subtype is passed
+in.
+
+`CongruenceCommon` is itself a subtype of [`Runner`](@ref
+Semigroups.Runner), so all runner methods (`run!`, `run_for!`,
+`finished`, `timed_out`, `current_state`, etc.) work on every congruence
+algorithm.
+"""
+const CongruenceCommon = LibSemigroups.CongruenceCommon
+
+_words_to_cpp(words::AbstractVector{<:AbstractVector{<:Integer}}) =
+ Any[_word_to_cpp(word) for word in words]
+
+"""
+ add_generating_pair!(cong::CongruenceCommon, u::AbstractVector{<:Integer}, v::AbstractVector{<:Integer}) -> CongruenceCommon
+
+Add a generating pair `(u, v)` to `cong`.
+
+# Arguments
+
+- `cong::CongruenceCommon`: the congruence to add a generating pair to.
+- `u::AbstractVector{<:Integer}`: the left-hand side of the pair, as a
+ 1-based `Vector{Int}` of letter indices.
+- `v::AbstractVector{<:Integer}`: the right-hand side of the pair, as a
+ 1-based `Vector{Int}` of letter indices.
+
+Returns `cong` for chaining.
+
+# Throws
+
+- `LibsemigroupsError` if any letter in `u` or `v` is not in the
+ alphabet of the underlying presentation.
+"""
+function add_generating_pair!(
+ cong::CongruenceCommon,
+ u::AbstractVector{<:Integer},
+ v::AbstractVector{<:Integer},
+)
+ cpp_u = _word_to_cpp(u)
+ cpp_v = _word_to_cpp(v)
+ @wrap_libsemigroups_call LibSemigroups.cong_common_add_generating_pair!(
+ cong,
+ cpp_u,
+ cpp_v,
+ )
+ return cong
+end
+
+"""
+ currently_contains(cong::CongruenceCommon, u::AbstractVector{<:Integer}, v::AbstractVector{<:Integer}) -> tril
+
+Check whether the words `u` and `v` are already known to be equivalent
+under `cong`, without triggering a run.
+
+This function performs no enumeration of `cong`, so it is possible for
+`u` and `v` to be equivalent in the congruence but for that not yet to
+be known.
+
+# Arguments
+
+- `cong::CongruenceCommon`: the congruence to check containment in.
+- `u::AbstractVector{<:Integer}`: the first word, as a 1-based
+ `Vector{Int}` of letter indices.
+- `v::AbstractVector{<:Integer}`: the second word, as a 1-based
+ `Vector{Int}` of letter indices.
+
+# Returns
+
+A [`tril`](@ref Semigroups.tril) value:
+
+- `tril_TRUE` if the words are known to belong to the congruence;
+- `tril_FALSE` if the words are known not to belong to the congruence;
+- `tril_unknown` otherwise.
+
+# Throws
+
+- `LibsemigroupsError` if any letter in `u` or `v` is not in the
+ alphabet of the underlying presentation.
+
+# See also
+
+[`contains`](@ref Semigroups.contains(::CongruenceCommon, ::AbstractVector{<:Integer}, ::AbstractVector{<:Integer}))
+"""
+function currently_contains(
+ cong::CongruenceCommon,
+ u::AbstractVector{<:Integer},
+ v::AbstractVector{<:Integer},
+)
+ cpp_u = _word_to_cpp(u)
+ cpp_v = _word_to_cpp(v)
+ return @wrap_libsemigroups_call LibSemigroups.cong_common_currently_contains(
+ cong,
+ cpp_u,
+ cpp_v,
+ )
+end
+
+"""
+ contains(cong::CongruenceCommon, u::AbstractVector{<:Integer}, v::AbstractVector{<:Integer}) -> Bool
+
+Check whether the words `u` and `v` are equivalent under `cong`.
+
+This function triggers a full enumeration of `cong`, which may never
+terminate.
+
+# Arguments
+
+- `cong::CongruenceCommon`: the congruence to check containment in.
+- `u::AbstractVector{<:Integer}`: the first word, as a 1-based
+ `Vector{Int}` of letter indices.
+- `v::AbstractVector{<:Integer}`: the second word, as a 1-based
+ `Vector{Int}` of letter indices.
+
+# Returns
+
+`true` if `u` and `v` are equivalent under `cong`, `false` otherwise.
+
+# Throws
+
+- `LibsemigroupsError` if any letter in `u` or `v` is not in the
+ alphabet of the underlying presentation.
+
+!!! warning
+ The Knuth-Bendix algorithm (and several other congruence algorithms)
+ may never terminate for an undecidable input.
+
+# See also
+
+[`currently_contains`](@ref Semigroups.currently_contains(::CongruenceCommon, ::AbstractVector{<:Integer}, ::AbstractVector{<:Integer}))
+"""
+function contains(
+ cong::CongruenceCommon,
+ u::AbstractVector{<:Integer},
+ v::AbstractVector{<:Integer},
+)
+ cpp_u = _word_to_cpp(u)
+ cpp_v = _word_to_cpp(v)
+ return @wrap_libsemigroups_call LibSemigroups.cong_common_contains(cong, cpp_u, cpp_v)
+end
+
+"""
+ reduce_no_run(cong::CongruenceCommon, w::AbstractVector{<:Integer}) -> Vector{Int}
+
+Reduce the word `w` using the current state of `cong`, without
+triggering an enumeration.
+
+The output word is equivalent to `w` in the congruence represented by
+`cong`. If `cong` is [`finished`](@ref Semigroups.finished), the output
+is a normal form for `w`. Otherwise, equivalent input words may produce
+different output words.
+
+# Arguments
+
+- `cong::CongruenceCommon`: the congruence to reduce in.
+- `w::AbstractVector{<:Integer}`: the word to reduce, as a 1-based
+ `Vector{Int}` of letter indices.
+
+# Returns
+
+A 1-based `Vector{Int}` representing a word equivalent to `w` under the
+current rules of `cong`.
+
+# Throws
+
+- `LibsemigroupsError` if any letter in `w` is not in the alphabet of
+ the underlying presentation.
+
+# See also
+
+[`reduce`](@ref Semigroups.reduce(::CongruenceCommon, ::AbstractVector{<:Integer}))
+"""
+function reduce_no_run(cong::CongruenceCommon, w::AbstractVector{<:Integer})
+ cpp_w = _word_to_cpp(w)
+ result = @wrap_libsemigroups_call LibSemigroups.cong_common_reduce_no_run(cong, cpp_w)
+ return _word_from_cpp(result)
+end
+
+"""
+ reduce(cong::CongruenceCommon, w::AbstractVector{<:Integer}) -> Vector{Int}
+
+Reduce the word `w` to a normal form under `cong`.
+
+This function triggers a full enumeration of `cong`. The output word is
+a normal form for `w` in the congruence.
+
+# Arguments
+
+- `cong::CongruenceCommon`: the congruence to reduce in.
+- `w::AbstractVector{<:Integer}`: the word to reduce, as a 1-based
+ `Vector{Int}` of letter indices.
+
+# Returns
+
+A 1-based `Vector{Int}` representing a normal form of `w` in `cong`.
+
+# Throws
+
+- `LibsemigroupsError` if any letter in `w` is not in the alphabet of
+ the underlying presentation.
+
+!!! warning
+ The Knuth-Bendix algorithm (and several other congruence algorithms)
+ may never terminate for an undecidable input.
+
+!!! note
+ `Semigroups.reduce` is **not** exported, since exporting it would
+ shadow `Base.reduce`. Use the module-qualified form
+ `Semigroups.reduce(cong, w)`.
+
+# See also
+
+[`reduce_no_run`](@ref Semigroups.reduce_no_run(::CongruenceCommon, ::AbstractVector{<:Integer}))
+"""
+function reduce(cong::CongruenceCommon, w::AbstractVector{<:Integer})
+ cpp_w = _word_to_cpp(w)
+ result = @wrap_libsemigroups_call LibSemigroups.cong_common_reduce(cong, cpp_w)
+ return _word_from_cpp(result)
+end
+
+"""
+ normal_forms(cong::CongruenceCommon) -> Vector{Vector{Int}}
+
+Return the normal forms of every congruence class of `cong`.
+
+The order of the classes, and the normal form chosen for each class,
+are determined by the reduction order of `cong`. This function triggers
+a full enumeration of `cong`.
+
+# Returns
+
+A `Vector` of 1-based `Vector{Int}` words, one per congruence class.
+
+!!! warning
+ The Knuth-Bendix algorithm (and several other congruence algorithms)
+ may never terminate for an undecidable input. If the congruence has
+ infinitely many classes, this function does not return.
+
+# See also
+
+[`partition`](@ref Semigroups.partition(::CongruenceCommon, ::AbstractVector{<:AbstractVector{<:Integer}})),
+[`non_trivial_classes`](@ref Semigroups.non_trivial_classes(::CongruenceCommon, ::CongruenceCommon))
+"""
+function normal_forms(cong::CongruenceCommon)
+ nf = @wrap_libsemigroups_call LibSemigroups.cong_common_normal_forms(cong)
+ return [_word_from_cpp(w) for w in nf]
+end
+
+"""
+ partition(cong::CongruenceCommon, words::AbstractVector{<:AbstractVector{<:Integer}}) -> Vector{Vector{Vector{Int}}}
+
+Partition `words` into congruence classes induced by `cong`.
+
+Each returned class is a list of the input words that belong to the
+same congruence class. This function triggers a full enumeration of
+`cong`.
+
+# Arguments
+
+- `cong::CongruenceCommon`: the congruence used to partition the words.
+- `words::AbstractVector{<:AbstractVector{<:Integer}}`: the input words,
+ each a 1-based `Vector{Int}` of letter indices.
+
+# Returns
+
+A `Vector` of classes; each class is a `Vector` of 1-based `Vector{Int}`
+words.
+
+# Throws
+
+- `LibsemigroupsError` if `cong` has infinitely many classes (the
+ partition would not be finite).
+
+# See also
+
+[`non_trivial_classes`](@ref Semigroups.non_trivial_classes(::CongruenceCommon, ::CongruenceCommon)),
+[`normal_forms`](@ref Semigroups.normal_forms(::CongruenceCommon))
+"""
+function partition(
+ cong::CongruenceCommon,
+ words::AbstractVector{<:AbstractVector{<:Integer}},
+)
+ classes = @wrap_libsemigroups_call LibSemigroups.cong_common_partition(
+ cong,
+ _words_to_cpp(words),
+ )
+ return [[_word_from_cpp(word) for word in cls] for cls in classes]
+end
+
+"""
+ non_trivial_classes(cong1::CongruenceCommon, cong2::CongruenceCommon) -> Vector{Vector{Vector{Int}}}
+
+Return the classes of size at least 2 in the partition of the normal
+forms of `cong2` induced by `cong1`.
+
+Here `cong1` must represent a coarser congruence than `cong2` (i.e. one
+with fewer classes). This function triggers a full enumeration of both
+arguments.
+
+This function does **not** compute the normal forms of `cong2`,
+partition them by `cong1`, and filter; it can therefore return the
+non-trivial classes even when one of `cong1` or `cong2` has infinitely
+many classes, provided there are only finitely many finite non-trivial
+classes.
+
+# Arguments
+
+- `cong1::CongruenceCommon`: the coarser congruence.
+- `cong2::CongruenceCommon`: the finer congruence.
+
+# Returns
+
+A `Vector` of non-trivial classes; each class is a `Vector` of 1-based
+`Vector{Int}` words.
+
+# Throws
+
+- `LibsemigroupsError` if `cong1` has infinitely many classes and
+ `cong2` has finitely many classes (so that there is at least one
+ infinite non-trivial class).
+- `LibsemigroupsError` if the alphabets of the underlying presentations
+ of `cong1` and `cong2` are not equal.
+- `LibsemigroupsError` if [`gilman_graph`](@ref Semigroups.gilman_graph)
+ of `cong1` has fewer nodes than that of `cong2` (Knuth-Bendix only).
+
+!!! warning
+ The Knuth-Bendix algorithm (and several other congruence algorithms)
+ may never terminate for an undecidable input.
+
+# See also
+
+[`partition`](@ref Semigroups.partition(::CongruenceCommon, ::AbstractVector{<:AbstractVector{<:Integer}})),
+[`normal_forms`](@ref Semigroups.normal_forms(::CongruenceCommon))
+"""
+function non_trivial_classes(cong1::CongruenceCommon, cong2::CongruenceCommon)
+ classes =
+ @wrap_libsemigroups_call LibSemigroups.cong_common_non_trivial_classes(cong1, cong2)
+ return [[_word_from_cpp(w) for w in cls] for cls in classes]
+end
diff --git a/src/constants.jl b/src/constants.jl
index ad3fd5a..2732d38 100644
--- a/src/constants.jl
+++ b/src/constants.jl
@@ -199,6 +199,30 @@ Base.show(io::IO, ::PositiveInfinityType) = print(io, "POSITIVE_INFINITY")
Base.show(io::IO, ::NegativeInfinityType) = print(io, "NEGATIVE_INFINITY")
Base.show(io::IO, ::LimitMaxType) = print(io, "LIMIT_MAX")
+# congruence_kind enum re-exports from LibSemigroups
+
+"""
+ congruence_kind
+
+Enum indicating the sided-ness of a congruence. Use `twosided` or `onesided`
+for the possible values.
+"""
+const congruence_kind = LibSemigroups.congruence_kind
+
+"""
+ onesided
+
+Value of [`congruence_kind`](@ref) representing a one-sided congruence.
+"""
+const onesided = LibSemigroups.congruence_kind_onesided
+
+"""
+ twosided
+
+Value of [`congruence_kind`](@ref) representing a two-sided congruence.
+"""
+const twosided = LibSemigroups.congruence_kind_twosided
+
# tril enum re-exports from LibSemigroups
"""
diff --git a/src/knuth-bendix.jl b/src/knuth-bendix.jl
new file mode 100644
index 0000000..5f57f2e
--- /dev/null
+++ b/src/knuth-bendix.jl
@@ -0,0 +1,669 @@
+# Copyright (c) 2026, James W. Swent
+#
+# Distributed under the terms of the GPL license version 3.
+
+"""
+knuth-bendix.jl - KnuthBendix wrapper (Layer 2 + 3)
+"""
+
+# ============================================================================
+# Type alias and constants
+# ============================================================================
+
+"""
+ KnuthBendix
+
+Type implementing the Knuth-Bendix completion algorithm for semigroups and
+monoids.
+
+A `KnuthBendix` object represents a [string rewriting
+system](https://w.wiki/9Re) defining a 1- or 2-sided congruence on a finitely
+presented semigroup or monoid. It is constructed from a
+[`congruence_kind`](@ref Semigroups.congruence_kind) and a
+[`Presentation`](@ref Semigroups.Presentation), and runs the Knuth-Bendix
+algorithm to find a confluent rewriting system.
+
+`KnuthBendix` is a subtype of [`Runner`](@ref Semigroups.Runner), so all
+runner methods (`run!`, `run_for!`, `run_until!`, `finished`, `timed_out`,
+`current_state`, etc.) work on `KnuthBendix` objects.
+
+# Constructors
+
+ KnuthBendix(kind::congruence_kind, p::Presentation) -> KnuthBendix
+ KnuthBendix(other::KnuthBendix) -> KnuthBendix
+
+The first form constructs a `KnuthBendix` from a congruence kind and a
+presentation. The second form copies an existing `KnuthBendix`.
+
+# Throws
+
+- `LibsemigroupsError` if `p` is not valid.
+- `LibsemigroupsError` if `p` has more than 256 letters in its alphabet
+ (the internal rewriting trie uses 1-byte letter indices).
+
+!!! warning "v1 limitation"
+ v1 of Semigroups.jl binds `KnuthBendix{word_type, RewriteTrie}` only.
+
+# Example
+
+The example below mirrors the [libsemigroups `KnuthBendix`
+example](https://libsemigroups.github.io/libsemigroups/group__knuth__bendix__class__group.html)
+for the free group on two generators with relations ``ab = ba^{-1}`` and
+``cd = dc^{-1}``. Letters `1, 2, 3, 4` correspond to ``a, b, c, d``.
+
+```julia
+using Semigroups
+
+p = Presentation()
+set_contains_empty_word!(p, true)
+set_alphabet!(p, 4) # letters 1, 2, 3, 4 <-> a, b, c, d
+add_rule_no_checks!(p, [1, 2], Int[]) # ab = ε
+add_rule_no_checks!(p, [2, 1], Int[]) # ba = ε
+add_rule_no_checks!(p, [3, 4], Int[]) # cd = ε
+add_rule_no_checks!(p, [4, 3], Int[]) # dc = ε
+
+kb = KnuthBendix(twosided, p)
+
+number_of_active_rules(kb) # 0
+number_of_pending_rules(kb) # 4
+run!(kb)
+number_of_active_rules(kb) # 4
+number_of_pending_rules(kb) # 0
+confluent(kb) # true
+number_of_classes(kb) # POSITIVE_INFINITY
+```
+"""
+const KnuthBendix = LibSemigroups.KnuthBendixRewriteTrie
+
+"""
+ overlap_ABC
+
+Overlap policy: measure ``d(AB, BC) = |A| + |B| + |C|``.
+
+The overlap of words ``AB`` and ``BC`` is measured as the sum of the lengths
+of the three constituent parts. See [`overlap_policy!`](@ref
+Semigroups.overlap_policy!) for how to apply this policy to a
+[`KnuthBendix`](@ref Semigroups.KnuthBendix) instance.
+"""
+const overlap_ABC = LibSemigroups.overlap_ABC
+
+"""
+ overlap_AB_BC
+
+Overlap policy: measure ``d(AB, BC) = |AB| + |BC|``.
+
+The overlap of words ``AB`` and ``BC`` is measured as the sum of the lengths
+of the two overlapping words. See [`overlap_policy!`](@ref
+Semigroups.overlap_policy!) for how to apply this policy.
+"""
+const overlap_AB_BC = LibSemigroups.overlap_AB_BC
+
+"""
+ overlap_MAX_AB_BC
+
+Overlap policy: measure ``d(AB, BC) = \\max(|AB|, |BC|)``.
+
+The overlap of words ``AB`` and ``BC`` is measured as the maximum of the
+lengths of the two overlapping words. See [`overlap_policy!`](@ref
+Semigroups.overlap_policy!) for how to apply this policy.
+"""
+const overlap_MAX_AB_BC = LibSemigroups.overlap_MAX_AB_BC
+
+# ============================================================================
+# Initialization
+# ============================================================================
+
+"""
+ init!(kb::KnuthBendix) -> KnuthBendix
+ init!(kb::KnuthBendix, kind::congruence_kind, p::Presentation) -> KnuthBendix
+
+Re-initialize `kb`.
+
+The one-argument form clears the rewriter, presentation, settings, and
+statistics from `kb`, putting it back into the same state as a newly
+default-constructed [`KnuthBendix`](@ref Semigroups.KnuthBendix).
+
+The three-argument form reinitializes `kb` as if it had just been constructed
+from `kind` and `p`.
+
+# Throws
+
+- `LibsemigroupsError` if `p` is not valid (three-argument form).
+- `LibsemigroupsError` if `p` has more than 256 letters in its alphabet
+ (three-argument form).
+
+!!! warning
+ At present it is only possible to create `KnuthBendix` objects from
+ presentations with at most 256 letters in the alphabet.
+"""
+function init!(kb::KnuthBendix)
+ @wrap_libsemigroups_call LibSemigroups.init!(kb)
+ return kb
+end
+
+function init!(kb::KnuthBendix, kind::congruence_kind, p::Presentation)
+ @wrap_libsemigroups_call LibSemigroups.init!(kb, kind, p)
+ return kb
+end
+
+# ============================================================================
+# Settings — getter / setter pairs
+# ============================================================================
+
+"""
+ max_pending_rules(kb::KnuthBendix) -> Int
+
+Return the current maximum number of pending rules before processing.
+
+Pending rules accumulate until there are `max_pending_rules(kb)` of them, at
+which point they are reduced, processed, and added to the active system. The
+default value is `128`. Set to `1` to process each rule immediately.
+
+# See also
+
+[`max_pending_rules!`](@ref Semigroups.max_pending_rules!)
+"""
+max_pending_rules(kb::KnuthBendix) = Int(LibSemigroups.max_pending_rules(kb))
+
+"""
+ max_pending_rules!(kb::KnuthBendix, n::Integer) -> KnuthBendix
+
+Set the maximum number of pending rules to `n`. Returns `kb` for chaining.
+
+Pending rules accumulate until there are `n` of them, at which point they are
+reduced, processed, and added to the active system. The default is `128`. Set
+to `1` to process each new rule immediately as it is created.
+
+# See also
+
+[`max_pending_rules`](@ref Semigroups.max_pending_rules)
+"""
+function max_pending_rules!(kb::KnuthBendix, n::Integer)
+ LibSemigroups.set_max_pending_rules!(kb, UInt(n))
+ return kb
+end
+
+"""
+ check_confluence_interval(kb::KnuthBendix) -> Int
+
+Return the current interval at which confluence is checked during `run!`.
+
+This is the number of new overlaps considered between confluence checks.
+The default value is `4096`. Returns `LIMIT_MAX` if confluence is never
+checked mid-run.
+
+# See also
+
+[`check_confluence_interval!`](@ref Semigroups.check_confluence_interval!),
+[`run!`](@ref Semigroups.run!)
+"""
+check_confluence_interval(kb::KnuthBendix) =
+ Int(LibSemigroups.check_confluence_interval(kb))
+
+"""
+ check_confluence_interval!(kb::KnuthBendix, n::Integer) -> KnuthBendix
+
+Set the confluence-check interval to `n`. Returns `kb` for chaining.
+
+[`run!`](@ref Semigroups.run!) periodically checks whether the system is
+already confluent; `n` is the number of new overlaps to consider between
+consecutive checks. Setting `n` too low can adversely affect performance. The
+default is `4096`. Set to `LIMIT_MAX` to disable mid-run confluence checks.
+
+# See also
+
+[`check_confluence_interval`](@ref Semigroups.check_confluence_interval),
+[`run!`](@ref Semigroups.run!)
+"""
+function check_confluence_interval!(kb::KnuthBendix, n::Integer)
+ LibSemigroups.set_check_confluence_interval!(kb, UInt(n))
+ return kb
+end
+
+"""
+ max_overlap(kb::KnuthBendix) -> Int
+
+Return the maximum overlap length currently set.
+
+This is the maximum length of the overlap of two left-hand sides of rules
+considered during [`run!`](@ref Semigroups.run!). If set to a value less than
+the longest left-hand side of any rule, `run!` may terminate without the
+system being confluent.
+
+# See also
+
+[`max_overlap!`](@ref Semigroups.max_overlap!)
+"""
+max_overlap(kb::KnuthBendix) = Int(LibSemigroups.max_overlap(kb))
+
+"""
+ max_overlap!(kb::KnuthBendix, n::Integer) -> KnuthBendix
+
+Set the maximum overlap length to `n`. Returns `kb` for chaining.
+
+Overlaps of length greater than `n` are not considered during [`run!`](@ref
+Semigroups.run!). If `n` is smaller than the longest left-hand side of any
+rule, `run!` may terminate without producing a confluent system.
+
+# See also
+
+[`max_overlap`](@ref Semigroups.max_overlap), [`run!`](@ref Semigroups.run!)
+"""
+function max_overlap!(kb::KnuthBendix, n::Integer)
+ LibSemigroups.set_max_overlap!(kb, UInt(n))
+ return kb
+end
+
+"""
+ max_rules(kb::KnuthBendix) -> Int
+
+Return the approximate maximum number of rules currently set.
+
+If the number of rules exceeds this value during [`run!`](@ref
+Semigroups.run!) or [`by_overlap_length!`](@ref Semigroups.by_overlap_length!),
+those functions terminate early and the system may not be confluent. The
+default is `POSITIVE_INFINITY`.
+
+# See also
+
+[`max_rules!`](@ref Semigroups.max_rules!)
+"""
+max_rules(kb::KnuthBendix) = Int(LibSemigroups.max_rules(kb))
+
+"""
+ max_rules!(kb::KnuthBendix, n::Integer) -> KnuthBendix
+
+Set the approximate maximum number of rules to `n`. Returns `kb` for chaining.
+
+If the number of rules exceeds `n` during [`run!`](@ref Semigroups.run!) or
+[`by_overlap_length!`](@ref Semigroups.by_overlap_length!), those functions
+terminate early and the system may not be confluent. The default is
+`POSITIVE_INFINITY`.
+
+# See also
+
+[`max_rules`](@ref Semigroups.max_rules), [`run!`](@ref Semigroups.run!)
+"""
+function max_rules!(kb::KnuthBendix, n::Integer)
+ LibSemigroups.set_max_rules!(kb, UInt(n))
+ return kb
+end
+
+"""
+ overlap_policy(kb::KnuthBendix)
+
+Return the current overlap policy.
+
+The overlap policy determines how the length ``d(AB, BC)`` of an overlap of
+two words ``AB`` and ``BC`` is measured. See [`overlap_ABC`](@ref
+Semigroups.overlap_ABC), [`overlap_AB_BC`](@ref Semigroups.overlap_AB_BC), and
+[`overlap_MAX_AB_BC`](@ref Semigroups.overlap_MAX_AB_BC).
+
+# See also
+
+[`overlap_policy!`](@ref Semigroups.overlap_policy!)
+"""
+overlap_policy(kb::KnuthBendix) = LibSemigroups.overlap_policy(kb)
+
+"""
+ overlap_policy!(kb::KnuthBendix, val) -> KnuthBendix
+
+Set the overlap policy. Returns `kb` for chaining.
+
+The overlap policy controls how the length of an overlap of two words is
+measured during the algorithm. `val` must be one of [`overlap_ABC`](@ref
+Semigroups.overlap_ABC), [`overlap_AB_BC`](@ref Semigroups.overlap_AB_BC), or
+[`overlap_MAX_AB_BC`](@ref Semigroups.overlap_MAX_AB_BC).
+
+# See also
+
+[`overlap_policy`](@ref Semigroups.overlap_policy)
+"""
+function overlap_policy!(kb::KnuthBendix, val)
+ LibSemigroups.set_overlap_policy!(kb, val)
+ return kb
+end
+
+# ============================================================================
+# Query methods
+# ============================================================================
+
+"""
+ number_of_active_rules(kb::KnuthBendix) -> Int
+
+Return the current number of active rules in the rewriting system.
+
+Active rules are used to perform rewriting. This count changes as the
+Knuth-Bendix algorithm runs.
+
+# Complexity
+
+Constant.
+"""
+number_of_active_rules(kb::KnuthBendix) = Int(LibSemigroups.number_of_active_rules(kb))
+
+"""
+ number_of_inactive_rules(kb::KnuthBendix) -> Int
+
+Return the current number of inactive rules in the rewriting system.
+
+Inactive rules have been superseded during the algorithm and are no longer
+used for rewriting.
+
+# Complexity
+
+Constant.
+"""
+number_of_inactive_rules(kb::KnuthBendix) = Int(LibSemigroups.number_of_inactive_rules(kb))
+
+"""
+ number_of_pending_rules(kb::KnuthBendix) -> Int
+
+Return the number of pending rules.
+
+All rules in the system are either active or pending. Active rules are used
+for rewriting; pending rules are not until they have been processed and
+promoted to active status. Rules from the presentation are initially pending
+when a `KnuthBendix` is constructed.
+
+# Complexity
+
+Constant.
+"""
+number_of_pending_rules(kb::KnuthBendix) = Int(LibSemigroups.number_of_pending_rules(kb))
+
+"""
+ total_rules(kb::KnuthBendix) -> Int
+
+Return the total number of rule instances created during the algorithm.
+
+This is the total count of `Rule` objects ever created while Knuth-Bendix has
+been running. It is **not** simply
+[`number_of_active_rules`](@ref Semigroups.number_of_active_rules) plus
+[`number_of_inactive_rules`](@ref Semigroups.number_of_inactive_rules),
+because rules are re-initialized and reused where possible.
+
+# Complexity
+
+Constant.
+"""
+total_rules(kb::KnuthBendix) = Int(LibSemigroups.total_rules(kb))
+
+"""
+ confluent(kb::KnuthBendix) -> Bool
+
+Check if the current rewriting system is [confluent](https://w.wiki/9DA).
+
+Returns `true` if the current rules are confluent, `false` otherwise. This
+function does not trigger a run; call [`run!`](@ref Semigroups.run!) first to
+ensure the system has been fully processed.
+"""
+confluent(kb::KnuthBendix) = LibSemigroups.confluent(kb)
+
+"""
+ confluent_known(kb::KnuthBendix) -> Bool
+
+Return `true` if the confluence status of the current rules is already known.
+
+Reports whether [`confluent`](@ref Semigroups.confluent) would return a
+definitive answer without running further. Does not trigger a run.
+"""
+confluent_known(kb::KnuthBendix) = LibSemigroups.confluent_known(kb)
+
+"""
+ number_of_classes(kb::KnuthBendix) -> UInt64
+
+Compute the number of congruence classes, triggering a full run if needed.
+
+Returns `POSITIVE_INFINITY` if the semigroup has infinitely many elements.
+
+If `kb` has already been run to completion, this function determines the
+number of classes via the [`gilman_graph`](@ref Semigroups.gilman_graph) in
+``O(mn)`` time, where ``m`` is the size of the alphabet and ``n`` is the
+number of nodes in the Gilman graph.
+
+!!! warning
+ This function may not terminate if the congruence has infinitely many
+ classes and Knuth-Bendix cannot detect this.
+
+# See also
+
+[`gilman_graph`](@ref Semigroups.gilman_graph),
+[`normal_forms`](@ref Semigroups.normal_forms)
+"""
+number_of_classes(kb::KnuthBendix) = LibSemigroups.number_of_classes(kb)
+
+"""
+ kind(kb::KnuthBendix) -> congruence_kind
+
+Return the kind of the congruence represented by `kb`.
+
+Returns `twosided` or `onesided`. See [`congruence_kind`](@ref
+Semigroups.congruence_kind) for details.
+
+# Complexity
+
+Constant.
+"""
+kind(kb::KnuthBendix) = LibSemigroups.kind(kb)
+
+"""
+ number_of_generating_pairs(kb::KnuthBendix) -> Int
+
+Return the number of generating pairs added to `kb`.
+
+This equals the length of [`generating_pairs`](@ref
+Semigroups.generating_pairs) divided by 2.
+
+# Complexity
+
+Constant.
+"""
+number_of_generating_pairs(kb::KnuthBendix) =
+ Int(LibSemigroups.number_of_generating_pairs(kb))
+
+"""
+ generating_pairs(kb::KnuthBendix) -> Vector{Tuple{Vector{Int}, Vector{Int}}}
+
+Return the generating pairs of `kb` as 1-based word pairs.
+
+These are the pairs added via [`add_generating_pair!`](@ref
+Semigroups.add_generating_pair!). Words are returned as 1-based `Vector{Int}`
+letter indices.
+
+!!! warning
+ If `kb` represents a one-sided congruence ([`kind`](@ref Semigroups.kind)
+ is `onesided`) and generating pairs have been added, the presentation's
+ alphabet contains one extra letter required by the algorithm. This extra
+ letter may appear in the returned words.
+"""
+function generating_pairs(kb::KnuthBendix)
+ flat = LibSemigroups.generating_pairs(kb)
+ result = Tuple{Vector{Int},Vector{Int}}[]
+ for i = 1:2:length(flat)
+ push!(result, (_word_from_cpp(flat[i]), _word_from_cpp(flat[i+1])))
+ end
+ return result
+end
+
+"""
+ presentation(kb::KnuthBendix) -> Presentation
+
+Return a copy of the presentation used by `kb`.
+
+!!! warning
+ If `kb` represents a one-sided congruence ([`kind`](@ref Semigroups.kind)
+ is `onesided`) and generating pairs have been added
+ ([`number_of_generating_pairs`](@ref Semigroups.number_of_generating_pairs)
+ `> 0`), the returned presentation's alphabet contains one extra letter
+ required by the algorithm. This extra letter also appears in the output of
+ [`active_rules`](@ref Semigroups.active_rules).
+"""
+presentation(kb::KnuthBendix) = LibSemigroups.presentation(kb)
+
+# ============================================================================
+# Rules access
+# ============================================================================
+
+"""
+ active_rules(kb::KnuthBendix) -> Vector{Tuple{Vector{Int}, Vector{Int}}}
+
+Return all active rules as a vector of `(lhs, rhs)` tuples.
+
+Words are returned as 1-based `Vector{Int}` letter indices.
+"""
+function active_rules(kb::KnuthBendix)
+ flat = @wrap_libsemigroups_call LibSemigroups.kb_active_rules(kb)
+ result = Tuple{Vector{Int},Vector{Int}}[]
+ for i = 1:2:length(flat)
+ push!(result, (_word_from_cpp(flat[i]), _word_from_cpp(flat[i+1])))
+ end
+ return result
+end
+
+# ============================================================================
+# Graph access
+# ============================================================================
+
+"""
+ gilman_graph(kb::KnuthBendix) -> WordGraph
+
+Return the Gilman [`WordGraph`](@ref Semigroups.WordGraph) of the rewriting
+system.
+
+The Gilman WordGraph is a directed graph where paths from the initial node
+(corresponding to the empty word) spell out the shortlex normal forms of the
+semigroup elements. The semigroup is finite if and only if the graph is
+acyclic.
+
+!!! warning
+ This function will not return until `kb` is both reduced and confluent,
+ which may never happen.
+
+# See also
+
+[`number_of_classes`](@ref Semigroups.number_of_classes),
+[`normal_forms`](@ref Semigroups.normal_forms)
+"""
+@cxxdereference gilman_graph(kb::KnuthBendix) = LibSemigroups.gilman_graph(kb)
+
+"""
+ gilman_graph_node_labels(kb::KnuthBendix) -> Vector{Vector{Int}}
+
+Return the node labels of the Gilman graph as 1-based words.
+
+Each label corresponds to a unique prefix of the left-hand sides of the rules
+in the rewriting system. Words are returned as 1-based `Vector{Int}` letter
+indices.
+
+# See also
+
+[`gilman_graph`](@ref Semigroups.gilman_graph)
+"""
+@cxxdereference function gilman_graph_node_labels(kb::KnuthBendix)
+ labels = LibSemigroups.gilman_graph_node_labels(kb)
+ return [_word_from_cpp(w) for w in labels]
+end
+
+# ============================================================================
+# Base.* overloads
+# ============================================================================
+
+"""
+ Base.length(kb::KnuthBendix) -> UInt64
+
+Return the number of congruence classes. Equivalent to
+[`number_of_classes`](@ref Semigroups.number_of_classes).
+"""
+Base.length(kb::KnuthBendix) = number_of_classes(kb)
+
+"""
+ Base.show(io::IO, kb::KnuthBendix)
+
+Print a human-readable representation of `kb`.
+"""
+function Base.show(io::IO, kb::KnuthBendix)
+ print(io, LibSemigroups.to_human_readable_repr(kb))
+end
+
+"""
+ Base.copy(kb::KnuthBendix) -> KnuthBendix
+
+Create an independent copy of `kb`.
+"""
+Base.copy(kb::KnuthBendix) = LibSemigroups.KnuthBendixRewriteTrie(kb)
+
+Base.deepcopy_internal(kb::KnuthBendix, ::IdDict) = LibSemigroups.KnuthBendixRewriteTrie(kb)
+
+# ============================================================================
+# Free functions
+# ============================================================================
+
+"""
+ by_overlap_length!(kb::KnuthBendix) -> KnuthBendix
+
+Run the Knuth-Bendix algorithm ordered by overlap length.
+
+This function runs the Knuth-Bendix algorithm by considering all overlaps of
+length ``n`` (as measured by the current [`overlap_policy`](@ref
+Semigroups.overlap_policy)) before those of length ``n + 1``. Returns `kb`.
+
+!!! warning
+ This function will not terminate until `kb` is confluent, which may never
+ happen.
+
+# See also
+
+[`run!`](@ref Semigroups.run!),
+[`overlap_policy!`](@ref Semigroups.overlap_policy!)
+"""
+function by_overlap_length!(kb::KnuthBendix)
+ @wrap_libsemigroups_call LibSemigroups.kb_by_overlap_length!(kb)
+ return kb
+end
+
+"""
+ is_reduced(kb::KnuthBendix) -> Bool
+
+Check if all rules in the system are reduced with respect to each other.
+
+Returns `true` if for each pair of rules ``(A, B)`` and ``(C, D)`` in `kb`,
+the word ``C`` is neither a subword of ``A`` nor of ``B``. Returns `false`
+otherwise.
+"""
+is_reduced(kb::KnuthBendix) = @wrap_libsemigroups_call LibSemigroups.kb_is_reduced(kb)
+
+"""
+ redundant_rule(p::Presentation, timeout::TimePeriod) -> Union{Int, Nothing}
+
+Find a redundant rule in `p` using Knuth-Bendix, with the given timeout.
+
+Starting with the last rule in `p`, this function attempts to run
+Knuth-Bendix on the rules of `p` with each rule omitted in turn. For each
+omitted rule, Knuth-Bendix is run for at most `timeout`, then it checks
+whether the omitted rule follows from the remaining rules. Returns the
+1-based rule-pair index of the first redundant rule found, or `nothing` if
+no redundant rule is identified within the timeout.
+
+!!! warning
+ This function is non-deterministic: results may differ between calls
+ with identical parameters.
+
+# Arguments
+
+- `p`: the presentation to search.
+- `timeout`: maximum time per omitted rule (e.g. `Millisecond(100)`,
+ `Second(5)`).
+"""
+function redundant_rule(p::Presentation, timeout::TimePeriod)
+ ns = convert(Nanosecond, timeout)
+ idx =
+ @wrap_libsemigroups_call LibSemigroups.kb_redundant_rule(p, Int64(Dates.value(ns)))
+ n_flat = 2 * number_of_rules(p)
+ # If idx == n_flat, no redundant rule was found
+ if idx >= n_flat
+ return nothing
+ end
+ # Convert from 0-based flat index to 1-based rule-pair index
+ return div(Int(idx), 2) + 1
+end
diff --git a/test/runtests.jl b/test/runtests.jl
index 214bd89..02dcb3c 100644
--- a/test/runtests.jl
+++ b/test/runtests.jl
@@ -23,4 +23,6 @@ using Semigroups
include("test_presentation_examples.jl")
include("test_word_range.jl")
include("test_froidure_pin_transf.jl")
+ include("test_knuth_bendix_1.jl")
+ include("test_knuth_bendix_6.jl")
end
diff --git a/test/test_knuth_bendix_1.jl b/test/test_knuth_bendix_1.jl
new file mode 100644
index 0000000..51bf61c
--- /dev/null
+++ b/test/test_knuth_bendix_1.jl
@@ -0,0 +1,1320 @@
+# Copyright (c) 2026, James W. Swent
+#
+# Distributed under the terms of the GPL license version 3.
+#
+# The full license is in the file LICENSE, distributed with this software.
+
+"""
+test_knuth_bendix_1.jl - Ports of libsemigroups test-knuth-bendix-1.cpp
+
+The upstream file mostly tests `KnuthBendix`. Semigroups.jl
+currently exposes the `word_type`/`RewriteTrie` instantiation, so these tests
+translate each C++ string alphabet to 1-based Julia word vectors while keeping
+the C++ test numbering.
+"""
+
+using Test
+using Semigroups
+using Dates
+
+function _kb1_word(alphabet::AbstractString, s::AbstractString)
+ letters = collect(alphabet)
+ return [something(findfirst(==(c), letters)) for c in s]
+end
+
+function _kb1_words(alphabet::AbstractString, strings)
+ return [_kb1_word(alphabet, s) for s in strings]
+end
+
+function _kb1_add_rule!(p::Presentation, alphabet::AbstractString, lhs, rhs)
+ add_rule_no_checks!(p, _kb1_word(alphabet, lhs), _kb1_word(alphabet, rhs))
+ return p
+end
+
+_kb1_cword(xs::Integer...) = [Int(x) + 1 for x in xs]
+_kb1_cword(xs::AbstractVector{<:Integer}) = [Int(x) + 1 for x in xs]
+
+function _kb1_add_cpp_rule!(p::Presentation, lhs, rhs)
+ add_rule_no_checks!(p, _kb1_cword(lhs), _kb1_cword(rhs))
+ return p
+end
+
+function _kb1_presentation(alphabet::AbstractString, rules; empty_word::Bool = false)
+ p = Presentation()
+ empty_word && set_contains_empty_word!(p, true)
+ set_alphabet!(p, length(collect(alphabet)))
+ for (lhs, rhs) in rules
+ _kb1_add_rule!(p, alphabet, lhs, rhs)
+ end
+ return p
+end
+
+function _kb1_words_of_length(n::Integer, len::Integer)
+ len == 0 && return [Int[]]
+ prev = _kb1_words_of_length(n, len - 1)
+ return [[word; a] for word in prev for a = 1:n]
+end
+
+function _kb1_normal_forms_between(
+ kb::KnuthBendix,
+ alphabet_size::Integer,
+ min_len::Integer,
+ max_len::Integer,
+)
+ result = Vector{Int}[]
+ for len = min_len:max_len
+ for w in _kb1_words_of_length(alphabet_size, len)
+ Semigroups.reduce(kb, w) == w && push!(result, w)
+ end
+ end
+ return result
+end
+
+function _kb1_expect_normal_forms(
+ kb::KnuthBendix,
+ alphabet::AbstractString,
+ min_len::Integer,
+ max_len::Integer,
+ expected,
+)
+ @test _kb1_normal_forms_between(kb, length(collect(alphabet)), min_len, max_len) ==
+ _kb1_words(alphabet, expected)
+end
+
+function _kb1_same_presentation(p::Presentation, q::Presentation)
+ return contains_empty_word(p) == contains_empty_word(q) &&
+ Semigroups.alphabet(p) == Semigroups.alphabet(q) &&
+ rules(p) == rules(q)
+end
+
+function _kb1_number_of_edges(g)
+ count = 0
+ for source = 1:number_of_nodes(g), label = 1:out_degree(g)
+ is_undefined(target(g, source, label)) || (count += 1)
+ end
+ return count
+end
+
+function _kb1_is_acyclic(g)
+ state = zeros(Int, number_of_nodes(g))
+
+ function visit(v)
+ state[v] == 1 && return false
+ state[v] == 2 && return true
+ state[v] = 1
+ for label = 1:out_degree(g)
+ t = target(g, v, label)
+ if !is_undefined(t) && !visit(t)
+ return false
+ end
+ end
+ state[v] = 2
+ return true
+ end
+
+ return all(v -> state[v] == 2 || visit(v), 1:number_of_nodes(g))
+end
+
+function _kb1_path_count(g, min_len::Integer, max_len::Integer; source::Integer = 1)
+ counts = zeros(BigInt, number_of_nodes(g))
+ counts[source] = 1
+ total = min_len == 0 ? big(1) : big(0)
+
+ for len = 1:max_len
+ next_counts = zeros(BigInt, number_of_nodes(g))
+ for v = 1:number_of_nodes(g)
+ iszero(counts[v]) && continue
+ for label = 1:out_degree(g)
+ t = target(g, v, label)
+ is_undefined(t) || (next_counts[t] += counts[v])
+ end
+ end
+ len >= min_len && (total += sum(next_counts))
+ counts = next_counts
+ end
+
+ return total
+end
+
+function _kb1_paths_take_from_successors(
+ successors,
+ n::Integer;
+ source::Integer = 1,
+ skip_empty::Bool = true,
+)
+ nodes = [source]
+ words = [Int[]]
+ result = Vector{Int}[]
+ head = 1
+
+ while length(result) < n
+ head <= length(nodes) || error("not enough paths in graph")
+ v = nodes[head]
+ w = words[head]
+ head += 1
+
+ if !(skip_empty && isempty(w))
+ push!(result, w)
+ length(result) == n && break
+ end
+
+ for (label, t) in successors(v)
+ push!(nodes, t)
+ push!(words, [w; label])
+ end
+ end
+
+ return result
+end
+
+function _kb1_paths_take(g, n::Integer; source::Integer = 1, skip_empty::Bool = true)
+ return _kb1_paths_take_from_successors(n; source, skip_empty) do v
+ edges = Tuple{Int,Int}[]
+ for label = 1:out_degree(g)
+ t = target(g, v, label)
+ is_undefined(t) || push!(edges, (label, Int(t)))
+ end
+ return edges
+ end
+end
+
+function _kb1_paths_take_rows(
+ rows,
+ n::Integer;
+ source::Integer = 1,
+ skip_empty::Bool = true,
+)
+ degree = maximum(length, rows)
+ return _kb1_paths_take_from_successors(n; source, skip_empty) do v
+ row = rows[v]
+ edges = Tuple{Int,Int}[]
+ for label = 1:degree
+ if label <= length(row)
+ t = row[label]
+ t === nothing || push!(edges, (label, Int(t) + 1))
+ end
+ end
+ return edges
+ end
+end
+
+@testset verbose = true "KnuthBendix test-knuth-bendix-1.cpp" begin
+ ReportGuard(false)
+
+ @testset "000: confluent fp semigroup 1 (infinite)" begin
+ alphabet = "abc"
+ p = _kb1_presentation(
+ alphabet,
+ [
+ ("ab", "ba"),
+ ("ac", "ca"),
+ ("aa", "a"),
+ ("ac", "a"),
+ ("ca", "a"),
+ ("bb", "bb"),
+ ("bc", "cb"),
+ ("bbb", "b"),
+ ("bc", "b"),
+ ("cb", "b"),
+ ("a", "b"),
+ ],
+ )
+
+ kb = KnuthBendix(twosided, p)
+
+ @test number_of_active_rules(kb) == 0
+ @test number_of_pending_rules(kb) == 10
+ @test confluent(kb)
+ @test Semigroups.reduce(kb, _kb1_word(alphabet, "ca")) == _kb1_word(alphabet, "a")
+ @test Semigroups.reduce(kb, _kb1_word(alphabet, "ac")) == _kb1_word(alphabet, "a")
+ @test Semigroups.contains(kb, _kb1_word(alphabet, "ca"), _kb1_word(alphabet, "a"))
+ @test Semigroups.contains(kb, _kb1_word(alphabet, "ac"), _kb1_word(alphabet, "a"))
+ @test number_of_classes(kb) == POSITIVE_INFINITY
+ _kb1_expect_normal_forms(kb, alphabet, 1, 4, ["a", "c", "cc", "ccc", "cccc"])
+ end
+
+ @testset "001: confluent fp semigroup 2 (infinite)" begin
+ alphabet = "abc"
+ p = _kb1_presentation(
+ alphabet,
+ [
+ ("ac", "ca"),
+ ("aa", "a"),
+ ("ac", "a"),
+ ("ca", "a"),
+ ("bb", "bb"),
+ ("bc", "cb"),
+ ("bbb", "b"),
+ ("bc", "b"),
+ ("cb", "b"),
+ ("a", "b"),
+ ],
+ )
+
+ kb = KnuthBendix(twosided, p)
+
+ @test confluent(kb)
+ @test number_of_active_rules(kb) == 4
+ _kb1_expect_normal_forms(kb, alphabet, 1, 4, ["a", "c", "cc", "ccc", "cccc"])
+ @test number_of_classes(kb) == POSITIVE_INFINITY
+ end
+
+ @testset "002: confluent fp semigroup 3 (infinite)" begin
+ alphabet = "012"
+ p = _kb1_presentation(
+ alphabet,
+ [
+ ("01", "10"),
+ ("02", "20"),
+ ("00", "0"),
+ ("02", "0"),
+ ("20", "0"),
+ ("11", "11"),
+ ("12", "21"),
+ ("111", "1"),
+ ("12", "1"),
+ ("21", "1"),
+ ("0", "1"),
+ ],
+ )
+
+ kb = KnuthBendix(twosided, p)
+
+ @test number_of_active_rules(kb) == 0
+ @test number_of_pending_rules(kb) == 10
+ @test confluent(kb)
+ @test number_of_active_rules(kb) == 4
+ @test number_of_classes(kb) == POSITIVE_INFINITY
+ _kb1_expect_normal_forms(kb, alphabet, 1, 1, ["0", "2"])
+ _kb1_expect_normal_forms(
+ kb,
+ alphabet,
+ 1,
+ 11,
+ [
+ "0",
+ "2",
+ "22",
+ "222",
+ "2222",
+ "22222",
+ "222222",
+ "2222222",
+ "22222222",
+ "222222222",
+ "2222222222",
+ "22222222222",
+ ],
+ )
+ end
+
+ @testset "003: non-confluent example wikipedia" begin
+ alphabet = "01"
+ p = _kb1_presentation(
+ alphabet,
+ [("000", ""), ("111", ""), ("010101", "")],
+ empty_word = true,
+ )
+
+ kb = KnuthBendix(twosided, p)
+
+ @test Semigroups.alphabet(presentation(kb)) == [1, 2]
+ @test !confluent(kb)
+ run!(kb)
+ @test active_rules(kb) == [
+ (_kb1_word(alphabet, "000"), Int[]),
+ (_kb1_word(alphabet, "111"), Int[]),
+ (_kb1_word(alphabet, "1010"), _kb1_word(alphabet, "0011")),
+ (_kb1_word(alphabet, "1100"), _kb1_word(alphabet, "0101")),
+ ]
+ @test confluent(kb)
+ @test number_of_classes(kb) == POSITIVE_INFINITY
+ _kb1_expect_normal_forms(
+ kb,
+ alphabet,
+ 0,
+ 4,
+ [
+ "",
+ "0",
+ "1",
+ "00",
+ "01",
+ "10",
+ "11",
+ "001",
+ "010",
+ "011",
+ "100",
+ "101",
+ "110",
+ "0010",
+ "0011",
+ "0100",
+ "0101",
+ "0110",
+ "1001",
+ "1011",
+ "1101",
+ ],
+ )
+ nfs = _kb1_normal_forms_between(kb, length(alphabet), 0, 10)
+ @test all(w -> Semigroups.reduce(kb, w) == w, nfs)
+ end
+
+ @testset "004: Example 5.1 in Sims (infinite)" begin
+ alphabet = "abcd"
+ p = _kb1_presentation(
+ alphabet,
+ [("ab", ""), ("ba", ""), ("cd", ""), ("dc", ""), ("ca", "ac")],
+ empty_word = true,
+ )
+
+ kb = KnuthBendix(twosided, p)
+
+ @test !confluent(kb)
+ run!(kb)
+ @test number_of_active_rules(kb) == 8
+ @test confluent(kb)
+ @test number_of_classes(kb) == POSITIVE_INFINITY
+ _kb1_expect_normal_forms(
+ kb,
+ alphabet,
+ 0,
+ 4,
+ [
+ "",
+ "a",
+ "b",
+ "c",
+ "d",
+ "aa",
+ "ac",
+ "ad",
+ "bb",
+ "bc",
+ "bd",
+ "cc",
+ "dd",
+ "aaa",
+ "aac",
+ "aad",
+ "acc",
+ "add",
+ "bbb",
+ "bbc",
+ "bbd",
+ "bcc",
+ "bdd",
+ "ccc",
+ "ddd",
+ "aaaa",
+ "aaac",
+ "aaad",
+ "aacc",
+ "aadd",
+ "accc",
+ "addd",
+ "bbbb",
+ "bbbc",
+ "bbbd",
+ "bbcc",
+ "bbdd",
+ "bccc",
+ "bddd",
+ "cccc",
+ "dddd",
+ ],
+ )
+ nfs = _kb1_normal_forms_between(kb, length(alphabet), 0, 6)
+ @test all(w -> Semigroups.reduce(kb, w) == w, nfs)
+ end
+
+ @testset "005: Example 5.1 in Sims (infinite) x 2" begin
+ alphabet = "aAbB"
+ p = Presentation()
+ set_contains_empty_word!(p, true)
+ set_alphabet!(p, length(alphabet))
+ add_inverse_rules!(p, _kb1_word(alphabet, "AaBb"))
+ _kb1_add_rule!(p, alphabet, "ba", "ab")
+
+ kb = KnuthBendix(twosided, p)
+
+ @test !confluent(kb)
+ run!(kb)
+ @test number_of_active_rules(kb) == 8
+ @test confluent(kb)
+ @test number_of_classes(kb) == POSITIVE_INFINITY
+ _kb1_expect_normal_forms(
+ kb,
+ alphabet,
+ 0,
+ 4,
+ [
+ "",
+ "a",
+ "A",
+ "b",
+ "B",
+ "aa",
+ "ab",
+ "aB",
+ "AA",
+ "Ab",
+ "AB",
+ "bb",
+ "BB",
+ "aaa",
+ "aab",
+ "aaB",
+ "abb",
+ "aBB",
+ "AAA",
+ "AAb",
+ "AAB",
+ "Abb",
+ "ABB",
+ "bbb",
+ "BBB",
+ "aaaa",
+ "aaab",
+ "aaaB",
+ "aabb",
+ "aaBB",
+ "abbb",
+ "aBBB",
+ "AAAA",
+ "AAAb",
+ "AAAB",
+ "AAbb",
+ "AABB",
+ "Abbb",
+ "ABBB",
+ "bbbb",
+ "BBBB",
+ ],
+ )
+ nfs = _kb1_normal_forms_between(kb, length(alphabet), 0, 6)
+ @test all(w -> Semigroups.reduce(kb, w) == w, nfs)
+ end
+
+ @testset "006: Example 5.3 in Sims" begin
+ alphabet = "ab"
+ p = _kb1_presentation(
+ alphabet,
+ [("aa", ""), ("bbb", ""), ("ababab", "")],
+ empty_word = true,
+ )
+
+ kb = KnuthBendix(twosided, p)
+
+ @test !confluent(kb)
+ run!(kb)
+ @test number_of_active_rules(kb) == 6
+ @test confluent(kb)
+ @test number_of_classes(kb) == 12
+ @test length(normal_forms(kb)) == 12
+ @test normal_forms(kb) == _kb1_words(
+ alphabet,
+ ["", "a", "b", "ab", "ba", "bb", "aba", "abb", "bab", "bba", "babb", "bbab"],
+ )
+ nfs = _kb1_normal_forms_between(kb, length(alphabet), 0, 6)
+ @test all(w -> Semigroups.reduce(kb, w) == w, nfs)
+ end
+
+ @testset "007: Example 5.4 in Sims" begin
+ alphabet = "Bab"
+ p = _kb1_presentation(
+ alphabet,
+ [("aa", ""), ("bB", ""), ("bbb", ""), ("ababab", "")],
+ empty_word = true,
+ )
+
+ kb = KnuthBendix(twosided, p)
+
+ @test !confluent(kb)
+ run!(kb)
+ @test number_of_active_rules(kb) == 11
+ @test confluent(kb)
+ @test number_of_classes(kb) == 12
+ nf = _kb1_normal_forms_between(kb, length(alphabet), 1, 5)
+ @test length(nf) == 11
+ @test nf == _kb1_words(
+ alphabet,
+ ["B", "a", "b", "Ba", "aB", "ab", "ba", "BaB", "Bab", "aBa", "baB"],
+ )
+ end
+
+ @testset "008: Example 6.4 in Sims" begin
+ alphabet = "abc"
+ p = _kb1_presentation(
+ alphabet,
+ [
+ ("aa", ""),
+ ("bc", ""),
+ ("bbb", ""),
+ ("ababababababab", ""),
+ ("abacabacabacabac", ""),
+ ],
+ empty_word = true,
+ )
+
+ kb = KnuthBendix(twosided, p)
+
+ @test !confluent(kb)
+ run!(kb)
+ @test number_of_active_rules(kb) == 40
+ @test confluent(kb)
+ @test Semigroups.reduce(kb, _kb1_word(alphabet, "cc")) == _kb1_word(alphabet, "b")
+ @test Semigroups.reduce(kb, _kb1_word(alphabet, "ccc")) == Int[]
+ @test number_of_classes(kb) == 168
+ _kb1_expect_normal_forms(
+ kb,
+ alphabet,
+ 1,
+ 4,
+ [
+ "a",
+ "b",
+ "c",
+ "ab",
+ "ac",
+ "ba",
+ "ca",
+ "aba",
+ "aca",
+ "bab",
+ "bac",
+ "cab",
+ "cac",
+ "abab",
+ "abac",
+ "acab",
+ "acac",
+ "baba",
+ "baca",
+ "caba",
+ "caca",
+ ],
+ )
+ end
+
+ @testset "009: random example" begin
+ alphabet = "012"
+ p = _kb1_presentation(alphabet, [("000", "2"), ("111", "2"), ("010101", "2")])
+ add_identity_rules!(p, _kb1_word(alphabet, "2")[1])
+
+ kb = KnuthBendix(twosided, p)
+
+ @test !confluent(kb)
+ run!(kb)
+ @test number_of_active_rules(kb) == 9
+ @test confluent(kb)
+
+ wg = gilman_graph(kb)
+ @test number_of_nodes(wg) == 9
+ @test _kb1_number_of_edges(wg) == 13
+ @test !_kb1_is_acyclic(wg)
+ _kb1_expect_normal_forms(
+ kb,
+ alphabet,
+ 1,
+ 4,
+ [
+ "0",
+ "1",
+ "2",
+ "00",
+ "01",
+ "10",
+ "11",
+ "001",
+ "010",
+ "011",
+ "100",
+ "101",
+ "110",
+ "0010",
+ "0011",
+ "0100",
+ "0101",
+ "0110",
+ "1001",
+ "1011",
+ "1101",
+ ],
+ )
+ end
+
+ @testset "010: SL(2, 7) from Chap. 3, Prop. 1.5 in NR" begin
+ alphabet = "abAB"
+ p = _kb1_presentation(
+ alphabet,
+ [
+ ("aaaaaaa", ""),
+ ("bb", "ababab"),
+ ("bb", "aaaabaaaabaaaabaaaab"),
+ ("aA", ""),
+ ("Aa", ""),
+ ("bB", ""),
+ ("Bb", ""),
+ ],
+ empty_word = true,
+ )
+
+ kb = KnuthBendix(twosided, p)
+
+ @test !confluent(kb)
+ run!(kb)
+ @test number_of_active_rules(kb) == 152
+ @test confluent(kb)
+ @test number_of_classes(kb) == 336
+
+ wg = gilman_graph(kb)
+ @test number_of_nodes(wg) == 232
+ @test _kb1_number_of_edges(wg) == 265
+ @test _kb1_is_acyclic(wg)
+ @test _kb1_path_count(wg, 0, 13) == 336
+ end
+
+ @testset "011: F(2, 5) - Chap. 9, Sec. 1 in NR" begin
+ alphabet = "abcde"
+ p = _kb1_presentation(
+ alphabet,
+ [("ab", "c"), ("bc", "d"), ("cd", "e"), ("de", "a"), ("ea", "b")],
+ )
+
+ kb = KnuthBendix(twosided, p)
+
+ @test !confluent(kb)
+ run!(kb)
+ @test number_of_active_rules(kb) == 24
+ @test confluent(kb)
+ @test number_of_classes(kb) == 11
+
+ wg = gilman_graph(kb)
+ @test number_of_nodes(wg) == 8
+ @test _kb1_number_of_edges(wg) == 11
+ @test _kb1_is_acyclic(wg)
+ @test _kb1_path_count(wg, 0, 5) == 12
+ end
+
+ @testset "012: Reinis example 1" begin
+ alphabet = "abc"
+ p = _kb1_presentation(alphabet, [("a", "abb"), ("b", "baa")])
+
+ kb = KnuthBendix(twosided, p)
+
+ @test !confluent(kb)
+ run!(kb)
+ @test number_of_active_rules(kb) == 4
+
+ wg = gilman_graph(kb)
+ @test number_of_nodes(wg) == 7
+ @test _kb1_number_of_edges(wg) == 17
+ @test !_kb1_is_acyclic(wg)
+ @test _kb1_path_count(wg, 0, 9) == 13_044
+ end
+
+ @testset "013: redundant_rule (string adaptation)" begin
+ alphabet = "abc"
+ p = _kb1_presentation(
+ alphabet,
+ [("a", "abb"), ("b", "baa"), ("c", "abbabababaaababababab")],
+ )
+
+ @test redundant_rule(p, Millisecond(100)) === nothing
+
+ _kb1_add_rule!(p, alphabet, "b", "baa")
+ idx = redundant_rule(p, Millisecond(100))
+ @test idx !== nothing
+ @test rule_lhs(p, idx) == _kb1_word(alphabet, "b")
+ @test rule_rhs(p, idx) == _kb1_word(alphabet, "baa")
+ end
+
+ @testset "014: redundant_rule (word_type)" begin
+ p = Presentation()
+ set_alphabet!(p, 3)
+ add_rule!(p, [1], [1, 2, 2])
+ add_rule!(p, [2], [2, 1, 1])
+ add_rule!(p, [3], [1, 2, 2, 1, 2, 1, 2, 1, 1, 1, 1, 2, 1, 2, 1, 2, 1, 2, 1, 2, 1])
+
+ @test redundant_rule(p, Millisecond(10)) === nothing
+
+ add_rule!(p, [2], [2, 1, 1])
+ idx = redundant_rule(p, Millisecond(10))
+ @test idx !== nothing
+ @test rule_lhs(p, idx) == [2]
+ @test rule_rhs(p, idx) == [2, 1, 1]
+ end
+
+ @testset "015: constructors/init for finished" begin
+ alphabet1 = "abcd"
+ p1 = _kb1_presentation(
+ alphabet1,
+ [("ab", ""), ("ba", ""), ("cd", ""), ("dc", ""), ("ca", "ac")],
+ empty_word = true,
+ )
+
+ alphabet2 = "01"
+ p2 = _kb1_presentation(
+ alphabet2,
+ [("000", ""), ("111", ""), ("010101", "")],
+ empty_word = true,
+ )
+
+ kb1 = KnuthBendix(twosided, p1)
+ @test !confluent(kb1)
+ @test !finished(kb1)
+ run!(kb1)
+ @test confluent(kb1)
+ @test Semigroups.reduce(kb1, _kb1_word(alphabet1, "abababbdbcbdbabdbdb")) ==
+ _kb1_word(alphabet1, "bbbbbbddd")
+
+ init!(kb1, twosided, p2)
+ @test !confluent(kb1)
+ @test !finished(kb1)
+ @test _kb1_same_presentation(presentation(kb1), p2)
+ run!(kb1)
+ @test finished(kb1)
+ @test confluent(kb1)
+ @test confluent_known(kb1)
+
+ init!(kb1, twosided, p1)
+ @test !confluent(kb1)
+ @test !finished(kb1)
+ @test _kb1_same_presentation(presentation(kb1), p1)
+ run!(kb1)
+ @test finished(kb1)
+ @test confluent(kb1)
+ @test confluent_known(kb1)
+ @test Semigroups.reduce(kb1, _kb1_word(alphabet1, "abababbdbcbdbabdbdb")) ==
+ _kb1_word(alphabet1, "bbbbbbddd")
+
+ kb2 = copy(kb1)
+ @test confluent(kb2)
+ @test confluent_known(kb2)
+ @test finished(kb2)
+ @test Semigroups.reduce(kb2, _kb1_word(alphabet1, "abababbdbcbdbabdbdb")) ==
+ _kb1_word(alphabet1, "bbbbbbddd")
+
+ kb1 = copy(kb2)
+ @test confluent(kb1)
+ @test confluent_known(kb1)
+ @test finished(kb1)
+ @test Semigroups.reduce(kb1, _kb1_word(alphabet1, "abababbdbcbdbabdbdb")) ==
+ _kb1_word(alphabet1, "bbbbbbddd")
+
+ init!(kb1, twosided, p1)
+ @test !confluent(kb1)
+ @test !finished(kb1)
+ run!(kb1)
+ @test finished(kb1)
+ @test confluent(kb1)
+ @test confluent_known(kb1)
+ @test Semigroups.reduce(kb1, _kb1_word(alphabet1, "abababbdbcbdbabdbdb")) ==
+ _kb1_word(alphabet1, "bbbbbbddd")
+ end
+
+ @testset "016: constructors/init for partially run" begin
+ alphabet = "abc"
+ p = _kb1_presentation(
+ alphabet,
+ [
+ ("aa", ""),
+ ("bc", ""),
+ ("bbb", ""),
+ ("ababababababab", ""),
+ ("abacabacabacabacabacabacabacabac", ""),
+ ],
+ empty_word = true,
+ )
+
+ kb1 = KnuthBendix(twosided, p)
+ @test !confluent(kb1)
+ @test !finished(kb1)
+ run_for!(kb1, Millisecond(10))
+ @test !confluent(kb1)
+ @test !finished(kb1)
+
+ init!(kb1, twosided, p)
+ @test !confluent(kb1)
+ @test !finished(kb1)
+ @test _kb1_same_presentation(presentation(kb1), p)
+ run_for!(kb1, Millisecond(10))
+ @test !confluent(kb1)
+ @test !finished(kb1)
+
+ kb2 = copy(kb1)
+ @test !confluent(kb2)
+ @test !finished(kb2)
+ @test _kb1_same_presentation(presentation(kb2), p)
+ @test number_of_active_rules(kb1) == number_of_active_rules(kb2)
+ run_for!(kb2, Millisecond(10))
+ @test !confluent(kb2)
+ @test !finished(kb2)
+
+ active = number_of_active_rules(kb2)
+ kb1 = copy(kb2)
+ @test number_of_active_rules(kb1) == active
+ @test !finished(kb1)
+
+ init!(kb1, twosided, p)
+ add_generating_pair!(kb1, _kb1_word(alphabet, "ab"), _kb1_word(alphabet, "ba"))
+ @test number_of_generating_pairs(kb1) == 1
+ @test generating_pairs(kb1) ==
+ [(_kb1_word(alphabet, "ab"), _kb1_word(alphabet, "ba"))]
+
+ init!(kb1, twosided, p)
+ @test number_of_generating_pairs(kb1) == 0
+ @test isempty(generating_pairs(kb1))
+
+ add_generating_pair!(kb1, _kb1_word(alphabet, "ab"), _kb1_word(alphabet, "ba"))
+ @test number_of_generating_pairs(kb1) == 1
+ @test length(generating_pairs(kb1)) == 1
+
+ init!(kb1)
+ @test number_of_generating_pairs(kb1) == 0
+ @test isempty(generating_pairs(kb1))
+ end
+
+ @testset "017: non-trivial classes" begin
+ alphabet = "abc"
+ p = _kb1_presentation(
+ alphabet,
+ [
+ ("ab", "ba"),
+ ("ac", "ca"),
+ ("aa", "a"),
+ ("ac", "a"),
+ ("ca", "a"),
+ ("bc", "cb"),
+ ("bbb", "b"),
+ ("bc", "b"),
+ ("cb", "b"),
+ ],
+ )
+
+ kb1 = KnuthBendix(twosided, p)
+ _kb1_add_rule!(p, alphabet, "a", "b")
+ kb2 = KnuthBendix(twosided, p)
+
+ @test Semigroups.contains(kb2, _kb1_word(alphabet, "a"), _kb1_word(alphabet, "b"))
+ @test Semigroups.contains(kb2, _kb1_word(alphabet, "a"), _kb1_word(alphabet, "ba"))
+ @test Semigroups.contains(kb2, _kb1_word(alphabet, "a"), _kb1_word(alphabet, "bb"))
+ @test Semigroups.contains(kb2, _kb1_word(alphabet, "a"), _kb1_word(alphabet, "bab"))
+ @test non_trivial_classes(kb1, kb2) ==
+ [_kb1_words(alphabet, ["b", "ab", "bb", "abb", "a"])]
+ end
+
+ @testset "018: non-trivial classes x 2" begin
+ alphabet = "abc"
+ p = _kb1_presentation(
+ alphabet,
+ [
+ ("ab", "ba"),
+ ("ac", "ca"),
+ ("aa", "a"),
+ ("ac", "a"),
+ ("ca", "a"),
+ ("bc", "cb"),
+ ("bbb", "b"),
+ ("bc", "b"),
+ ("cb", "b"),
+ ],
+ )
+
+ kb1 = KnuthBendix(twosided, p)
+ @test number_of_classes(kb1) == POSITIVE_INFINITY
+
+ _kb1_add_rule!(p, alphabet, "b", "c")
+ kb2 = KnuthBendix(twosided, p)
+ @test number_of_classes(kb2) == 2
+ @test_throws LibsemigroupsError non_trivial_classes(kb1, kb2)
+ end
+
+ @testset "019: non-trivial classes x 3" begin
+ alphabet = "abc"
+ p = _kb1_presentation(
+ alphabet,
+ [
+ ("ab", "ba"),
+ ("ac", "ca"),
+ ("aa", "a"),
+ ("ac", "a"),
+ ("ca", "a"),
+ ("bc", "cb"),
+ ("bbb", "b"),
+ ("bc", "b"),
+ ("cb", "b"),
+ ],
+ )
+
+ kb1 = KnuthBendix(twosided, p)
+ _kb1_add_rule!(p, alphabet, "bb", "a")
+ kb2 = KnuthBendix(twosided, p)
+
+ @test non_trivial_classes(kb1, kb2) ==
+ [_kb1_words(alphabet, ["ab", "b"]), _kb1_words(alphabet, ["bb", "abb", "a"])]
+ end
+
+ @testset "020: non-trivial classes x 4" begin
+ p = Presentation()
+ set_alphabet!(p, 4)
+ add_rule_no_checks!(p, [1, 2], [2, 1])
+ add_rule_no_checks!(p, [1, 3], [3, 1])
+ add_rule_no_checks!(p, [1, 1], [1])
+ add_rule_no_checks!(p, [1, 3], [1])
+ add_rule_no_checks!(p, [3, 1], [1])
+ add_rule_no_checks!(p, [2, 3], [3, 2])
+ add_rule_no_checks!(p, [2, 2, 2], [2])
+ add_rule_no_checks!(p, [2, 3], [2])
+ add_rule_no_checks!(p, [3, 2], [2])
+ add_rule_no_checks!(p, [1, 4], [1])
+ add_rule_no_checks!(p, [4, 1], [1])
+ add_rule_no_checks!(p, [2, 4], [2])
+ add_rule_no_checks!(p, [4, 2], [2])
+ add_rule_no_checks!(p, [3, 4], [3])
+ add_rule_no_checks!(p, [4, 3], [3])
+
+ kb1 = KnuthBendix(twosided, p)
+ add_rule_no_checks!(p, [1], [2])
+ kb2 = KnuthBendix(twosided, p)
+
+ @test non_trivial_classes(kb1, kb2) == [[[2], [1, 2], [2, 2], [1, 2, 2], [1]]]
+ end
+
+ @testset "021: non-trivial congruence on infinite fp semigroup" begin
+ p = Presentation()
+ set_alphabet!(p, 5)
+ for (lhs, rhs) in [
+ ([0, 1], [0]),
+ ([1, 0], [0]),
+ ([0, 2], [0]),
+ ([2, 0], [0]),
+ ([0, 3], [0]),
+ ([3, 0], [0]),
+ ([0, 0], [0]),
+ ([1, 1], [0]),
+ ([2, 2], [0]),
+ ([3, 3], [0]),
+ ([1, 2], [0]),
+ ([2, 1], [0]),
+ ([1, 3], [0]),
+ ([3, 1], [0]),
+ ([2, 3], [0]),
+ ([3, 2], [0]),
+ ([4, 0], [0]),
+ ([4, 1], [1]),
+ ([4, 2], [2]),
+ ([4, 3], [3]),
+ ([0, 4], [0]),
+ ([1, 4], [1]),
+ ([2, 4], [2]),
+ ([3, 4], [3]),
+ ]
+ _kb1_add_cpp_rule!(p, lhs, rhs)
+ end
+
+ kb1 = KnuthBendix(twosided, p)
+ rows1 = [[1, 2, 3, 4, 5], [], [], [], [], [nothing, nothing, nothing, nothing, 5]]
+ @test number_of_classes(kb1) == POSITIVE_INFINITY
+ @test _kb1_paths_take(gilman_graph(kb1), 1000) == _kb1_paths_take_rows(rows1, 1000)
+
+ _kb1_add_cpp_rule!(p, [1], [2])
+ kb2 = KnuthBendix(twosided, p)
+ rows2 = [[1, 2, nothing, 3, 4], [], [], [], [nothing, nothing, nothing, nothing, 4]]
+
+ @test number_of_classes(kb1) == POSITIVE_INFINITY
+ @test _kb1_paths_take(gilman_graph(kb2), 1000) == _kb1_paths_take_rows(rows2, 1000)
+ @test Semigroups.contains(kb2, [2], [3])
+
+ ntc = non_trivial_classes(kb1, kb2)
+ @test length(ntc) == 1
+ @test length(ntc[1]) == 2
+ @test ntc == [[[3], [2]]]
+ end
+
+ @testset "022: non-trivial congruence on infinite fp semigroup x 2" begin
+ p = Presentation()
+ set_alphabet!(p, 5)
+ for (lhs, rhs) in [
+ ([0, 1], [0]),
+ ([1, 0], [0]),
+ ([0, 2], [0]),
+ ([2, 0], [0]),
+ ([0, 3], [0]),
+ ([3, 0], [0]),
+ ([0, 0], [0]),
+ ([1, 1], [0]),
+ ([2, 2], [0]),
+ ([3, 3], [0]),
+ ([1, 2], [0]),
+ ([2, 1], [0]),
+ ([1, 3], [0]),
+ ([3, 1], [0]),
+ ([2, 3], [0]),
+ ([3, 2], [0]),
+ ([4, 0], [0]),
+ ([4, 1], [2]),
+ ([4, 2], [3]),
+ ([4, 3], [1]),
+ ([0, 4], [0]),
+ ([1, 4], [2]),
+ ([2, 4], [3]),
+ ([3, 4], [1]),
+ ]
+ _kb1_add_cpp_rule!(p, lhs, rhs)
+ end
+
+ kb1 = KnuthBendix(twosided, p)
+ _kb1_add_cpp_rule!(p, [2], [3])
+ kb2 = KnuthBendix(twosided, p)
+
+ ntc = non_trivial_classes(kb1, kb2)
+ @test length(ntc) == 1
+ @test length(ntc[1]) == 3
+ @test ntc == [[[3], [4], [2]]]
+ end
+
+ @testset "023: trivial congruence on finite fp semigroup" begin
+ p = Presentation()
+ set_alphabet!(p, 2)
+ for (lhs, rhs) in [
+ ([0, 0, 1], [0, 0]),
+ ([0, 0, 0, 0], [0, 0]),
+ ([0, 1, 1, 0], [0, 0]),
+ ([0, 1, 1, 1], [0, 0, 0]),
+ ([1, 1, 1, 0], [1, 1, 0]),
+ ([1, 1, 1, 1], [1, 1, 1]),
+ ([0, 1, 0, 0, 0], [0, 1, 0, 1]),
+ ([0, 1, 0, 1, 0], [0, 1, 0, 0]),
+ ([0, 1, 0, 1, 1], [0, 1, 0, 1]),
+ ]
+ _kb1_add_cpp_rule!(p, lhs, rhs)
+ end
+
+ kb1 = KnuthBendix(twosided, p)
+ kb2 = KnuthBendix(twosided, p)
+
+ @test !contains_empty_word(p)
+ @test number_of_classes(kb1) == 27
+ @test number_of_classes(kb2) == 27
+ @test isempty(non_trivial_classes(kb1, kb2))
+ end
+
+ @testset "024: universal congruence on finite fp semigroup" begin
+ p = Presentation()
+ set_alphabet!(p, 2)
+ for (lhs, rhs) in [
+ ([0, 0, 1], [0, 0]),
+ ([0, 0, 0, 0], [0, 0]),
+ ([0, 1, 1, 0], [0, 0]),
+ ([0, 1, 1, 1], [0, 0, 0]),
+ ([1, 1, 1, 0], [1, 1, 0]),
+ ([1, 1, 1, 1], [1, 1, 1]),
+ ([0, 1, 0, 0, 0], [0, 1, 0, 1]),
+ ([0, 1, 0, 1, 0], [0, 1, 0, 0]),
+ ([0, 1, 0, 1, 1], [0, 1, 0, 1]),
+ ]
+ _kb1_add_cpp_rule!(p, lhs, rhs)
+ end
+
+ kb1 = KnuthBendix(twosided, p)
+
+ _kb1_add_cpp_rule!(p, [0], [1])
+ _kb1_add_cpp_rule!(p, [0, 0], [0])
+ kb2 = KnuthBendix(twosided, p)
+
+ @test number_of_classes(kb2) == 1
+ ntc = non_trivial_classes(kb1, kb2)
+ @test length(ntc) == 1
+ @test length(ntc[1]) == 27
+
+ expected = _kb1_cword.([
+ [0],
+ [1],
+ [0, 0],
+ [0, 1],
+ [1, 0],
+ [1, 1],
+ [0, 0, 0],
+ [1, 0, 0],
+ [0, 1, 0],
+ [1, 0, 1],
+ [0, 1, 1],
+ [1, 1, 0],
+ [1, 1, 1],
+ [1, 0, 0, 0],
+ [0, 1, 0, 0],
+ [1, 1, 0, 0],
+ [1, 0, 1, 0],
+ [0, 1, 0, 1],
+ [1, 1, 0, 1],
+ [1, 0, 1, 1],
+ [1, 1, 0, 0, 0],
+ [1, 0, 1, 0, 0],
+ [1, 1, 0, 1, 0],
+ [1, 0, 1, 0, 1],
+ [1, 1, 0, 1, 1],
+ [1, 1, 0, 1, 0, 0],
+ [1, 1, 0, 1, 0, 1],
+ ])
+ @test sort(repr.(ntc[1])) == sort(repr.(expected))
+ end
+
+ @testset "025: finite fp semigroup, size 16" begin
+ p = Presentation()
+ set_alphabet!(p, 11)
+ for (lhs, rhs) in [
+ ([2], [1]),
+ ([4], [3]),
+ ([5], [0]),
+ ([6], [3]),
+ ([7], [1]),
+ ([8], [3]),
+ ([9], [3]),
+ ([10], [0]),
+ ([0, 2], [0, 1]),
+ ([0, 4], [0, 3]),
+ ([0, 5], [0, 0]),
+ ([0, 6], [0, 3]),
+ ([0, 7], [0, 1]),
+ ([0, 8], [0, 3]),
+ ([0, 9], [0, 3]),
+ ([0, 10], [0, 0]),
+ ([1, 1], [1]),
+ ([1, 2], [1]),
+ ([1, 4], [1, 3]),
+ ([1, 5], [1, 0]),
+ ([1, 6], [1, 3]),
+ ([1, 7], [1]),
+ ([1, 8], [1, 3]),
+ ([1, 9], [1, 3]),
+ ([1, 10], [1, 0]),
+ ([3, 1], [3]),
+ ([3, 2], [3]),
+ ([3, 3], [3]),
+ ([3, 4], [3]),
+ ([3, 5], [3, 0]),
+ ([3, 6], [3]),
+ ([3, 7], [3]),
+ ([3, 8], [3]),
+ ([3, 9], [3]),
+ ([3, 10], [3, 0]),
+ ([0, 0, 0], [0]),
+ ([0, 0, 1], [1]),
+ ([0, 0, 3], [3]),
+ ([0, 1, 3], [1, 3]),
+ ([1, 0, 0], [1]),
+ ([1, 0, 3], [0, 3]),
+ ([3, 0, 0], [3]),
+ ([0, 1, 0, 1], [1, 0, 1]),
+ ([0, 3, 0, 3], [3, 0, 3]),
+ ([1, 0, 1, 0], [1, 0, 1]),
+ ([1, 3, 0, 1], [1, 0, 1]),
+ ([1, 3, 0, 3], [3, 0, 3]),
+ ([3, 0, 1, 0], [3, 0, 1]),
+ ([3, 0, 3, 0], [3, 0, 3]),
+ ]
+ _kb1_add_cpp_rule!(p, lhs, rhs)
+ end
+
+ kb1 = KnuthBendix(twosided, p)
+ @test number_of_nodes(gilman_graph(kb1)) == 16
+
+ rows1 = [
+ [
+ 3,
+ 1,
+ nothing,
+ 2,
+ nothing,
+ nothing,
+ nothing,
+ nothing,
+ nothing,
+ nothing,
+ nothing,
+ ],
+ [6, nothing, nothing, 12],
+ [7, nothing],
+ [4, 5, nothing, 9],
+ [],
+ [8],
+ [nothing, 11],
+ [nothing, 14, nothing, 15],
+ [],
+ [10],
+ [nothing, 14],
+ [],
+ [13],
+ [nothing],
+ [],
+ [],
+ ]
+ @test _kb1_paths_take(gilman_graph(kb1), 16) == _kb1_paths_take_rows(rows1, 16)
+
+ _kb1_add_cpp_rule!(p, [1], [3])
+ kb2 = KnuthBendix(twosided, p)
+ rows2 = [
+ [
+ 2,
+ 1,
+ nothing,
+ nothing,
+ nothing,
+ nothing,
+ nothing,
+ nothing,
+ nothing,
+ nothing,
+ nothing,
+ ],
+ [],
+ [3],
+ [],
+ ]
+ @test _kb1_paths_take(gilman_graph(kb2), 3) == _kb1_paths_take_rows(rows2, 3)
+
+ ntc = non_trivial_classes(kb1, kb2)
+ expected = _kb1_cword.([
+ [1],
+ [3],
+ [0, 1],
+ [0, 3],
+ [1, 0],
+ [3, 0],
+ [1, 3],
+ [0, 1, 0],
+ [0, 3, 0],
+ [1, 0, 1],
+ [3, 0, 1],
+ [3, 0, 3],
+ [1, 3, 0],
+ [0, 3, 0, 1],
+ ])
+ @test sort(repr.(ntc[1])) == sort(repr.(expected))
+ end
+
+ @testset "026: non_trivial_classes exceptions" begin
+ p = Presentation()
+ set_alphabet!(p, 1)
+ kbp = KnuthBendix(twosided, p)
+
+ q = Presentation()
+ set_alphabet!(q, 2)
+ kbq = KnuthBendix(twosided, q)
+ @test_throws LibsemigroupsError non_trivial_classes(kbp, kbq)
+ @test number_of_inactive_rules(kbq) == 0
+
+ add_rule_no_checks!(p, [1, 1, 1, 1], [1, 1])
+ init!(kbp, twosided, p)
+
+ q = Presentation()
+ set_alphabet!(q, 1)
+ add_rule_no_checks!(q, [1, 1], [1])
+ kbq = KnuthBendix(twosided, q)
+ @test_throws LibsemigroupsError non_trivial_classes(kbq, kbp)
+ end
+end
diff --git a/test/test_knuth_bendix_6.jl b/test/test_knuth_bendix_6.jl
new file mode 100644
index 0000000..8aa7e2d
--- /dev/null
+++ b/test/test_knuth_bendix_6.jl
@@ -0,0 +1,404 @@
+# Copyright (c) 2026, James W. Swent
+#
+# Distributed under the terms of the GPL license version 3.
+#
+# The full license is in the file LICENSE, distributed with this software.
+
+"""
+test_knuth_bendix_6.jl - Ports of libsemigroups test-knuth-bendix-6.cpp
+
+The upstream file is already based on `Presentation`, so these
+tests translate C++ 0-based word literals to Semigroups.jl's 1-based public
+word API and avoid direct `LibSemigroups` calls.
+"""
+
+using Test
+using Semigroups
+
+_kb6_cword(xs::Integer...) = [Int(x) + 1 for x in xs]
+_kb6_cword(xs::AbstractVector{<:Integer}) = [Int(x) + 1 for x in xs]
+
+function _kb6_add_cpp_rule!(p::Presentation, lhs, rhs)
+ add_rule!(p, _kb6_cword(lhs), _kb6_cword(rhs))
+ return p
+end
+
+function _kb6_add_cpp_rule_no_checks!(p::Presentation, lhs, rhs)
+ add_rule_no_checks!(p, _kb6_cword(lhs), _kb6_cword(rhs))
+ return p
+end
+
+function _kb6_presentation(n::Integer, rules; checks::Bool = true)
+ p = Presentation()
+ set_alphabet!(p, n)
+ add = checks ? _kb6_add_cpp_rule! : _kb6_add_cpp_rule_no_checks!
+ for (lhs, rhs) in rules
+ add(p, lhs, rhs)
+ end
+ return p
+end
+
+function _kb6_words_of_length(n::Integer, len::Integer)
+ len == 0 && return [Int[]]
+ prev = _kb6_words_of_length(n, len - 1)
+ return [[word; a] for word in prev for a = 1:n]
+end
+
+function _kb6_normal_forms_count(
+ kb::KnuthBendix,
+ alphabet_size::Integer,
+ min_len::Integer,
+ max_len::Integer,
+)
+ count = 0
+ for len = min_len:max_len
+ for w in _kb6_words_of_length(alphabet_size, len)
+ Semigroups.reduce(kb, w) == w && (count += 1)
+ end
+ end
+ return count
+end
+
+@testset verbose = true "KnuthBendix test-knuth-bendix-6.cpp" begin
+ ReportGuard(false)
+
+ @testset "129: Presentation{word_type}" begin
+ p = _kb6_presentation(2, [([0, 0, 0], [0]), ([0], [1, 1])])
+ kb = KnuthBendix(twosided, p)
+
+ @test !finished(kb)
+ @test number_of_classes(kb) == 5
+ @test finished(kb)
+ @test Semigroups.reduce(kb, _kb6_cword(0, 0, 1)) == _kb6_cword(0, 0, 1)
+ @test Semigroups.reduce(kb, _kb6_cword(0, 0, 0, 0, 1)) == _kb6_cword(0, 0, 1)
+ @test Semigroups.reduce(kb, _kb6_cword(0, 1, 1, 0, 0, 1)) == _kb6_cword(0, 0, 1)
+ @test !Semigroups.contains(kb, _kb6_cword(0, 0, 0), _kb6_cword(1))
+ @test !Semigroups.contains(kb, _kb6_cword(0, 0, 0, 0), _kb6_cword(0, 0, 0))
+ end
+
+ @testset "130: free semigroup congruence (6 classes)" begin
+ p = _kb6_presentation(
+ 5,
+ [
+ ([0, 0], [0]),
+ ([0, 1], [1]),
+ ([1, 0], [1]),
+ ([0, 2], [2]),
+ ([2, 0], [2]),
+ ([0, 3], [3]),
+ ([3, 0], [3]),
+ ([0, 4], [4]),
+ ([4, 0], [4]),
+ ([1, 2], [0]),
+ ([2, 1], [0]),
+ ([3, 4], [0]),
+ ([4, 3], [0]),
+ ([2, 2], [0]),
+ ([1, 4, 2, 3, 3], [0]),
+ ([4, 4, 4], [0]),
+ ],
+ )
+
+ kb = KnuthBendix(twosided, p)
+
+ @test number_of_classes(kb) == 6
+ @test Semigroups.contains(kb, _kb6_cword(1), _kb6_cword(2))
+ end
+
+ @testset "131: free semigroup congruence (16 classes)" begin
+ p = _kb6_presentation(
+ 4,
+ [
+ ([3], [2]),
+ ([0, 3], [0, 2]),
+ ([1, 1], [1]),
+ ([1, 3], [1, 2]),
+ ([2, 1], [2]),
+ ([2, 2], [2]),
+ ([2, 3], [2]),
+ ([0, 0, 0], [0]),
+ ([0, 0, 1], [1]),
+ ([0, 0, 2], [2]),
+ ([0, 1, 2], [1, 2]),
+ ([1, 0, 0], [1]),
+ ([1, 0, 2], [0, 2]),
+ ([2, 0, 0], [2]),
+ ([0, 1, 0, 1], [1, 0, 1]),
+ ([0, 2, 0, 2], [2, 0, 2]),
+ ([1, 0, 1, 0], [1, 0, 1]),
+ ([1, 2, 0, 1], [1, 0, 1]),
+ ([1, 2, 0, 2], [2, 0, 2]),
+ ([2, 0, 1, 0], [2, 0, 1]),
+ ([2, 0, 2, 0], [2, 0, 2]),
+ ],
+ )
+
+ kb = KnuthBendix(twosided, p)
+
+ @test number_of_classes(kb) == 16
+ @test number_of_active_rules(kb) == 18
+ @test Semigroups.contains(kb, _kb6_cword(2), _kb6_cword(3))
+ end
+
+ @testset "132: free semigroup congruence x 2" begin
+ p = _kb6_presentation(
+ 11,
+ [
+ ([2], [1]),
+ ([4], [3]),
+ ([5], [0]),
+ ([6], [3]),
+ ([7], [1]),
+ ([8], [3]),
+ ([9], [3]),
+ ([10], [0]),
+ ([0, 2], [0, 1]),
+ ([0, 4], [0, 3]),
+ ([0, 5], [0, 0]),
+ ([0, 6], [0, 3]),
+ ([0, 7], [0, 1]),
+ ([0, 8], [0, 3]),
+ ([0, 9], [0, 3]),
+ ([0, 10], [0, 0]),
+ ([1, 1], [1]),
+ ([1, 2], [1]),
+ ([1, 4], [1, 3]),
+ ([1, 5], [1, 0]),
+ ([1, 6], [1, 3]),
+ ([1, 7], [1]),
+ ([1, 8], [1, 3]),
+ ([1, 9], [1, 3]),
+ ([1, 10], [1, 0]),
+ ([3, 1], [3]),
+ ([3, 2], [3]),
+ ([3, 3], [3]),
+ ([3, 4], [3]),
+ ([3, 5], [3, 0]),
+ ([3, 6], [3]),
+ ([3, 7], [3]),
+ ([3, 8], [3]),
+ ([3, 9], [3]),
+ ([3, 10], [3, 0]),
+ ([0, 0, 0], [0]),
+ ([0, 0, 1], [1]),
+ ([0, 0, 3], [3]),
+ ([0, 1, 3], [1, 3]),
+ ([1, 0, 0], [1]),
+ ([1, 0, 3], [0, 3]),
+ ([3, 0, 0], [3]),
+ ([0, 1, 0, 1], [1, 0, 1]),
+ ([0, 3, 0, 3], [3, 0, 3]),
+ ([1, 0, 1, 0], [1, 0, 1]),
+ ([1, 3, 0, 1], [1, 0, 1]),
+ ([1, 3, 0, 3], [3, 0, 3]),
+ ([3, 0, 1, 0], [3, 0, 1]),
+ ([3, 0, 3, 0], [3, 0, 3]),
+ ],
+ checks = false,
+ )
+
+ kb = KnuthBendix(twosided, p)
+ @test number_of_classes(kb) == 16
+ @test Semigroups.contains(kb, _kb6_cword(0), _kb6_cword(5))
+ @test Semigroups.contains(kb, _kb6_cword(0), _kb6_cword(5))
+ @test Semigroups.contains(kb, _kb6_cword(0), _kb6_cword(10))
+ @test Semigroups.contains(kb, _kb6_cword(1), _kb6_cword(2))
+ @test Semigroups.contains(kb, _kb6_cword(1), _kb6_cword(7))
+ @test Semigroups.contains(kb, _kb6_cword(3), _kb6_cword(4))
+ @test Semigroups.contains(kb, _kb6_cword(3), _kb6_cword(6))
+ @test Semigroups.contains(kb, _kb6_cword(3), _kb6_cword(8))
+ @test Semigroups.contains(kb, _kb6_cword(3), _kb6_cword(9))
+ end
+
+ @testset "133: free semigroup congruence (240 classes)" begin
+ p = _kb6_presentation(
+ 2,
+ [
+ ([0, 0, 0], [0]),
+ ([1, 1, 1, 1], [1]),
+ ([0, 1, 1, 1, 0], [0, 0]),
+ ([1, 0, 0, 1], [1, 1]),
+ ([0, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0], [0, 0]),
+ ],
+ )
+
+ kb = KnuthBendix(twosided, p)
+ @test number_of_classes(kb) == 240
+ end
+
+ @testset "134: free semigroup congruence x 2 (FroidurePin conversion deferred)" begin
+ p = _kb6_presentation(
+ 2,
+ [
+ ([0, 0, 0], [0]),
+ ([1, 1, 1, 1], [1]),
+ ([0, 1, 1, 1, 0], [0, 0]),
+ ([1, 0, 0, 1], [1, 1]),
+ ([0, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0], [0, 0]),
+ ],
+ )
+
+ kb = KnuthBendix(twosided, p)
+ @test number_of_classes(kb) == 240
+ end
+
+ @testset "135: constructors" begin
+ p = _kb6_presentation(
+ 2,
+ [
+ ([0, 0, 0], [0]),
+ ([1, 1, 1, 1, 1, 1, 1, 1, 1], [1]),
+ ([0, 1, 1, 1, 1, 1, 0, 1, 1], [1, 1, 0]),
+ ],
+ )
+
+ kb = KnuthBendix(twosided, p)
+ @test number_of_classes(kb) == 746
+
+ kb_copy = copy(kb)
+ @test number_of_classes(kb_copy) == 746
+ @test length(Semigroups.alphabet(presentation(kb_copy))) == 2
+ @test number_of_active_rules(kb_copy) == 105
+ end
+
+ @testset "136: number of classes when obviously infinite" begin
+ p = _kb6_presentation(
+ 3,
+ [
+ ([0, 1], [1, 0]),
+ ([0, 2], [2, 0]),
+ ([0, 0], [0]),
+ ([0, 2], [0]),
+ ([2, 0], [0]),
+ ([1, 1], [1, 1]),
+ ([1, 2], [2, 1]),
+ ([1, 1, 1], [1]),
+ ([1, 2], [1]),
+ ([2, 1], [1]),
+ ([0], [1]),
+ ],
+ )
+
+ kb = KnuthBendix(twosided, p)
+ @test number_of_classes(kb) == POSITIVE_INFINITY
+ end
+
+ @testset "137: Chinese monoid x 2" begin
+ p = chinese_monoid(3)
+ kb = KnuthBendix(twosided, p)
+
+ @test number_of_classes(kb) == POSITIVE_INFINITY
+ @test number_of_rules(presentation(kb)) == 8
+ @test _kb6_normal_forms_count(kb, 3, 1, 9) == 1_175
+ end
+
+ @testset "138: partial_transformation_monoid(4)" begin
+ p = partial_transformation_monoid(4)
+ kb = KnuthBendix(twosided, p)
+
+ @test number_of_classes(kb) == 625
+ @test number_of_active_rules(kb) == 362
+ repr = sprint(show, kb)
+ @test occursin("confluent 2-sided KnuthBendix", repr)
+ @test occursin("362 active rules", repr)
+ end
+
+ @testset "139: partial_transformation_monoid5" begin
+ @test_skip "upstream [extreme] test; takes about 1 minute"
+ end
+
+ @testset "140: full_transformation_monoid Iwahori" begin
+ @test_skip "upstream [extreme] test; intentionally not run in the Julia quick suite"
+ end
+
+ @testset "141: constructors/init for finished x 2" begin
+ p1 = Presentation()
+ set_contains_empty_word!(p1, true)
+ set_alphabet!(p1, 4)
+ add_rule!(p1, _kb6_cword(0, 1), Int[])
+ add_rule!(p1, _kb6_cword(1, 0), Int[])
+ add_rule!(p1, _kb6_cword(2, 3), Int[])
+ add_rule!(p1, _kb6_cword(3, 2), Int[])
+ add_rule!(p1, _kb6_cword(2, 0), _kb6_cword(0, 2))
+
+ p2 = Presentation()
+ set_contains_empty_word!(p2, true)
+ set_alphabet!(p2, 2)
+ add_rule!(p2, _kb6_cword(0, 0, 0), Int[])
+ add_rule!(p2, _kb6_cword(1, 1, 1), Int[])
+ add_rule!(p2, _kb6_cword(0, 1, 0, 1, 0, 1), Int[])
+
+ kb1 = KnuthBendix(twosided, p1)
+ @test !confluent(kb1)
+ @test !finished(kb1)
+ run!(kb1)
+ @test confluent(kb1)
+ @test number_of_active_rules(kb1) == 8
+
+ init!(kb1, twosided, p2)
+ @test !confluent(kb1)
+ @test !finished(kb1)
+ run!(kb1)
+ @test finished(kb1)
+ @test confluent(kb1)
+ @test confluent_known(kb1)
+ @test number_of_active_rules(kb1) == 4
+
+ init!(kb1, twosided, p1)
+ @test !confluent(kb1)
+ @test !finished(kb1)
+ run!(kb1)
+ @test finished(kb1)
+ @test confluent(kb1)
+ @test confluent_known(kb1)
+ @test number_of_active_rules(kb1) == 8
+
+ kb2 = copy(kb1)
+ @test confluent(kb2)
+ @test confluent_known(kb2)
+ @test finished(kb2)
+ @test number_of_active_rules(kb2) == 8
+
+ kb1 = copy(kb2)
+ @test confluent(kb1)
+ @test confluent_known(kb1)
+ @test finished(kb1)
+ @test number_of_active_rules(kb1) == 8
+
+ init!(kb1, twosided, p1)
+ @test !confluent(kb1)
+ @test !finished(kb1)
+ run!(kb1)
+ @test finished(kb1)
+ @test confluent(kb1)
+ @test confluent_known(kb1)
+ @test number_of_active_rules(kb1) == 8
+
+ kb3 = KnuthBendix(twosided, p2)
+ @test !confluent(kb3)
+ @test !finished(kb3)
+ run!(kb3)
+ @test finished(kb3)
+ @test confluent(kb3)
+ @test confluent_known(kb3)
+ @test number_of_active_rules(kb3) == 4
+ end
+
+ @testset "142: close to or greater than 255 letters" begin
+ p = Presentation()
+ set_alphabet!(p, 257)
+ @test_throws Exception KnuthBendix(twosided, p)
+ end
+
+ @testset "118: process pending rules x1" begin
+ @test_skip "process_pending_rules is not exposed by the high-level Julia API"
+ end
+
+ @testset "143: process pending rules x2" begin
+ @test_skip "process_pending_rules is not exposed by the high-level Julia API"
+ end
+
+ @testset "144: process pending rules x3" begin
+ @test_skip "upstream [extreme] test and process_pending_rules is not exposed"
+ end
+end