1 // 2 // libsemigroups - C++ library for semigroups and monoids 3 // Copyright (C) 2019 James D. Mitchell 4 // 5 // This program is free software: you can redistribute it and/or modify 6 // it under the terms of the GNU General Public License as published by 7 // the Free Software Foundation, either version 3 of the License, or 8 // (at your option) any later version. 9 // 10 // This program is distributed in the hope that it will be useful, 11 // but WITHOUT ANY WARRANTY; without even the implied warranty of 12 // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 13 // GNU General Public License for more details. 14 // 15 // You should have received a copy of the GNU General Public License 16 // along with this program. If not, see <http://www.gnu.org/licenses/>. 17 // 18 19 // This file contains an implementation of the Todd-Coxeter algorithm for 20 // semigroups. 21 22 #include "todd-coxeter.hpp" 23 24 #include <algorithm> // for reverse 25 #include <chrono> // for nanoseconds etc 26 #include <cstddef> // for size_t 27 #include <memory> // for shared_ptr 28 #include <numeric> // for iota 29 #include <random> // for mt19937 30 #include <string> // for operator+, basic_string 31 #include <utility> // for pair 32 33 #ifdef LIBSEMIGROUPS_DEBUG 34 #include <set> // for set 35 #endif 36 37 #include "cong-intf.hpp" // for CongruenceInterface 38 #include "coset.hpp" // for CosetManager 39 #include "froidure-pin-base.hpp" // for FroidurePinBase 40 #include "froidure-pin.hpp" // for FroidurePin 41 #include "knuth-bendix.hpp" // for fpsemigroup::KnuthBendix 42 #include "libsemigroups-config.hpp" // for LIBSEMIGROUPS_DEBUG 43 #include "libsemigroups-debug.hpp" // for LIBSEMIGROUPS_ASSERT 44 #include "libsemigroups-exception.hpp" // for LIBSEMIGROUPS_EXCEPTION 45 #include "obvinf.hpp" // for IsObviouslyInfinite 46 #include "report.hpp" // for REPORT 47 #include "stl.hpp" // for apply_permutation 48 #include "tce.hpp" // for TCE 49 #include "timer.hpp" // for detail::Timer 50 #include "types.hpp" // for letter_type 51 52 // TODO(later) 53 // 54 // 1. Explore whether row-filling is useful when performing HLT. I think the 55 // just means making sure that there are no undefined values in the row of 56 // the current coset, this is an option from ACE. 57 // 58 // 2. Allow there to be a limit to the number of deductions that are stacked. 59 // this is an option from ACE. There are 4 options as described: 60 // 61 // https://magma.maths.usyd.edu.au/magma/handbook/text/833 62 // 63 // 3. Explore whether deductions can be useful in HLT. 64 // 65 // 4. Make make_deductions_dfs non-recursive, this will likely only be an issue 66 // for presentations with extremely long relations. 67 // 68 // 5. Use path compression in _ident, or other techniques from union-find, see: 69 // 70 // https://www.boost.org/doc/libs/1_70_0/boost/pending/disjoint_sets.hpp 71 // 72 // 6. Wreath product standardize mem fn. 73 // 74 // 7. ACE stacks deductions when processing coincidences, we don't 75 76 //////////////////////////////////////////////////////////////////////////////// 77 // COSET TABLES: 78 // 79 // We use these three tables to store all a coset's images and preimages. 80 // _table[c][i] is coset c's image under generator i. 81 // _preim_init[c][i] is ONE of coset c's preimages under generator i. 82 // _preim_next[c][i] is a coset that has THE SAME IMAGE as coset c 83 // (under i) 84 // 85 // Hence to find all the preimages of c under i: 86 // - Let u = _preim_init[c][i] ONCE. 87 // - Let u = _preim_next[u][i] REPEATEDLY until it becomes UNDEFINED. 88 // Each u is one preimage. 89 // 90 // To add v, a new preimage of c under i: 91 // - Set _preim_next[v][i] to point to the current _preim_init[c][i]. 92 // - Then change _preim_init[c][i] to point to v. 93 // Now the new preimage and all the old preimages are stored. 94 //////////////////////////////////////////////////////////////////////////////// 95 96 //////////////////////////////////////////////////////////////////////// 97 // Reporting macros 98 //////////////////////////////////////////////////////////////////////// 99 100 #define TODD_COXETER_REPORT_COSETS() \ 101 REPORT_DEFAULT("%d defined, %d max, %d active, %d killed (%s)\n", \ 102 nr_cosets_defined(), \ 103 coset_capacity(), \ 104 nr_cosets_active(), \ 105 nr_cosets_killed(), \ 106 __func__); 107 108 #define TODD_COXETER_REPORT_SWITCH(t, r) \ 109 REPORT_VERBOSE_DEFAULT("switching %*d %s and %*d %s\n", \ 110 detail::to_string(nr_cosets_active()).length() \ 111 - detail::to_string(t).length() + 1, \ 112 t, \ 113 (is_active_coset(t) ? "(active)" : "(free) "), \ 114 detail::to_string(nr_cosets_active()).length() \ 115 - detail::to_string(r).length() + 1, \ 116 r, \ 117 (is_active_coset(r) ? "(active)" : "(free) ")); 118 119 #ifdef LIBSEMIGROUPS_DEBUG 120 #define TODD_COXETER_REPORT_OK() REPORT_DEBUG(" ok\n").flush_right().flush(); 121 #else 122 #define TODD_COXETER_REPORT_OK() 123 #endif 124 125 namespace libsemigroups { 126 namespace congruence { 127 //////////////////////////////////////////////////////////////////////// 128 // Aliases 129 //////////////////////////////////////////////////////////////////////// 130 131 using coset_type = congruence::ToddCoxeter::coset_type; 132 using Coincidence = std::pair<coset_type, coset_type>; 133 using Deduction = std::pair<coset_type, letter_type>; 134 135 //////////////////////////////////////////////////////////////////////// 136 // Helper structs 137 //////////////////////////////////////////////////////////////////////// 138 139 struct StackDeductions { operator ()libsemigroups::congruence::StackDeductions140 inline void operator()(std::stack<Deduction>& stck, 141 coset_type c, 142 letter_type a) const noexcept { 143 stck.emplace(c, a); 144 } 145 }; 146 147 struct DoNotStackDeductions { operator ()libsemigroups::congruence::DoNotStackDeductions148 inline void operator()(std::stack<Deduction>&, 149 coset_type, 150 letter_type) const noexcept {} 151 }; 152 153 struct ProcessCoincidences { 154 template <typename TStackDeductions> operator ()libsemigroups::congruence::ProcessCoincidences155 void operator()(congruence::ToddCoxeter* tc) const noexcept { 156 tc->process_coincidences<TStackDeductions>(); 157 } 158 }; 159 160 struct DoNotProcessCoincidences { 161 template <typename TStackDeductions> operator ()libsemigroups::congruence::DoNotProcessCoincidences162 void operator()(congruence::ToddCoxeter*) const noexcept {} 163 }; 164 165 //////////////////////////////////////////////////////////////////////// 166 // Helper free functions 167 //////////////////////////////////////////////////////////////////////// 168 ff(coset_type c,coset_type d,coset_type r)169 static inline coset_type ff(coset_type c, coset_type d, coset_type r) { 170 return (r == c ? d : (r == d ? c : r)); 171 } 172 173 //////////////////////////////////////////////////////////////////////// 174 // ToddCoxeter - inner classes - private 175 //////////////////////////////////////////////////////////////////////// 176 177 struct ToddCoxeter::Settings { Settingslibsemigroups::congruence::ToddCoxeter::Settings178 Settings() 179 : 180 #ifdef LIBSEMIGROUPS_DEBUG 181 enable_debug_verify_no_missing_deductions(true), 182 #endif 183 lookahead(policy::lookahead::partial), 184 lower_bound(UNDEFINED), 185 next_lookahead(5000000), 186 froidure_pin(policy::froidure_pin::none), 187 random_interval(200000000), 188 save(false), 189 standardize(false), 190 strategy(policy::strategy::hlt) { 191 } 192 193 Settings(Settings const& copy) = default; 194 195 #ifdef LIBSEMIGROUPS_DEBUG 196 bool enable_debug_verify_no_missing_deductions; 197 #endif 198 policy::lookahead lookahead; 199 size_t lower_bound; 200 size_t next_lookahead; 201 policy::froidure_pin froidure_pin; 202 std::chrono::nanoseconds random_interval; 203 bool save; 204 bool standardize; 205 policy::strategy strategy; 206 }; 207 208 class ToddCoxeter::FelschTree { 209 public: 210 using index_type = size_t; 211 using state_type = size_t; 212 using const_iterator = std::vector<index_type>::const_iterator; 213 static constexpr state_type initial_state = 0; 214 static constexpr state_type final_state = UNDEFINED; 215 FelschTree(ToddCoxeter const * tc)216 explicit FelschTree(ToddCoxeter const* tc) 217 : _automata(tc->nr_generators(), 1, final_state), 218 _index(1, std::vector<index_type>({})), 219 _parent(1, state_type(UNDEFINED)) {} 220 221 FelschTree(FelschTree const&) = default; 222 add_relations(std::vector<word_type> const & rels)223 void add_relations(std::vector<word_type> const& rels) { 224 size_t nr_words = 0; 225 LIBSEMIGROUPS_ASSERT(rels.size() % 2 == 0); 226 for (auto const& w : rels) { 227 // For every prefix [w.cbegin(), last) 228 for (auto last = w.cend(); last > w.cbegin(); --last) { 229 // For every suffix [first, last) of the prefix [w.cbegin(), last) 230 for (auto first = w.cbegin(); first < last; ++first) { 231 // Find the maximal suffix of [first, last) that corresponds to 232 // an existing state . . . 233 auto it = last - 1; 234 state_type s = initial_state; 235 while (_automata.get(s, *it) != final_state && it > first) { 236 s = _automata.get(s, *it); 237 --it; 238 } 239 if (_automata.get(s, *it) == final_state) { 240 // [it + 1, last) is the maximal suffix of [first, last) that 241 // corresponds to the existing state s 242 size_t nr_states = _automata.nr_rows(); 243 _automata.add_rows((it + 1) - first); 244 _index.resize(_index.size() + ((it + 1) - first), {}); 245 _parent.resize(_parent.size() + ((it + 1) - first), UNDEFINED); 246 while (it >= first) { 247 // Add [it, last) as a new state 248 _automata.set(s, *it, nr_states); 249 _parent[nr_states] = s; 250 s = nr_states; 251 nr_states++; 252 it--; 253 } 254 } 255 } 256 // Find the state corresponding to the prefix [w.cbegin(), last) 257 auto it = last - 1; 258 state_type s = initial_state; 259 while (it >= w.cbegin()) { 260 s = _automata.get(s, *it); 261 LIBSEMIGROUPS_ASSERT(s != final_state); 262 --it; 263 } 264 index_type m = ((nr_words % 2) == 0 ? nr_words : nr_words - 1); 265 if (!std::binary_search(_index[s].cbegin(), _index[s].cend(), m)) { 266 _index[s].push_back(m); 267 } 268 } 269 nr_words++; 270 } 271 } 272 push_back(letter_type x)273 void push_back(letter_type x) { 274 _current_state = _automata.get(initial_state, x); 275 } 276 push_front(letter_type x)277 bool push_front(letter_type x) { 278 LIBSEMIGROUPS_ASSERT(x < _automata.nr_cols()); 279 if (_automata.get(_current_state, x) != final_state) { 280 _current_state = _automata.get(_current_state, x); 281 return true; 282 } else { 283 return false; 284 } 285 } 286 pop_front()287 void pop_front() { 288 _current_state = _parent[_current_state]; 289 } 290 cbegin() const291 const_iterator cbegin() const { 292 LIBSEMIGROUPS_ASSERT(_current_state != final_state); 293 return _index[_current_state].cbegin(); 294 } 295 cend() const296 const_iterator cend() const { 297 LIBSEMIGROUPS_ASSERT(_current_state != final_state); 298 return _index[_current_state].cend(); 299 } 300 301 private: 302 using StateTable = detail::DynamicArray2<state_type>; 303 StateTable _automata; 304 state_type _current_state; 305 std::vector<std::vector<index_type>> _index; 306 std::vector<state_type> _parent; 307 }; 308 309 struct ToddCoxeter::TreeNode { TreeNodelibsemigroups::congruence::ToddCoxeter::TreeNode310 TreeNode() : parent(UNDEFINED), gen(UNDEFINED) {} TreeNodelibsemigroups::congruence::ToddCoxeter::TreeNode311 TreeNode(coset_type p, letter_type g) : parent(p), gen(g) {} 312 coset_type parent; 313 letter_type gen; 314 }; 315 316 //////////////////////////////////////////////////////////////////////// 317 // ToddCoxeter - constructors and destructor - public 318 //////////////////////////////////////////////////////////////////////// 319 ToddCoxeter(congruence_type type)320 ToddCoxeter::ToddCoxeter(congruence_type type) 321 : CongruenceInterface(type), 322 CosetManager(), 323 _coinc(), 324 _deduct(), 325 _extra(), 326 _felsch_tree(nullptr), 327 _nr_pairs_added_earlier(0), 328 _prefilled(false), 329 _preim_init(0, 0, UNDEFINED), 330 _preim_next(0, 0, UNDEFINED), 331 _relations(), 332 _settings(new Settings()), 333 _standardized(order::none), 334 _state(state::constructed), 335 _table(0, 0, UNDEFINED), 336 _tree(nullptr) {} 337 ToddCoxeter(ToddCoxeter const & copy)338 ToddCoxeter::ToddCoxeter(ToddCoxeter const& copy) 339 : CongruenceInterface(copy), 340 CosetManager(copy), 341 _coinc(copy._coinc), 342 _deduct(copy._deduct), 343 _extra(copy._extra), 344 _felsch_tree(nullptr), 345 _nr_pairs_added_earlier(copy._nr_pairs_added_earlier), 346 _prefilled(copy._prefilled), 347 _preim_init(copy._preim_init), 348 _preim_next(copy._preim_next), 349 _relations(copy._relations), 350 _settings(detail::make_unique<Settings>(*copy._settings)), 351 _standardized(copy._standardized), 352 _state(copy._state), 353 _table(copy._table), 354 _tree(nullptr) { 355 if (copy._felsch_tree != nullptr) { 356 _felsch_tree = detail::make_unique<FelschTree>(*copy._felsch_tree); 357 } 358 if (copy._tree != nullptr) { 359 _tree = detail::make_unique<Tree>(*copy._tree); 360 } 361 } 362 ToddCoxeter(congruence_type type,std::shared_ptr<FroidurePinBase> S,policy::froidure_pin p)363 ToddCoxeter::ToddCoxeter(congruence_type type, 364 std::shared_ptr<FroidurePinBase> S, 365 policy::froidure_pin p) 366 : ToddCoxeter(type) { 367 _settings->froidure_pin = p; 368 set_parent_froidure_pin(S); 369 set_nr_generators(S->nr_generators()); 370 } 371 372 // Construct a ToddCoxeter object representing a congruence over the 373 // semigroup defined by copy (the quotient that is). ToddCoxeter(congruence_type typ,ToddCoxeter & copy)374 ToddCoxeter::ToddCoxeter(congruence_type typ, ToddCoxeter& copy) 375 : ToddCoxeter(typ) { 376 if (copy.kind() != congruence_type::twosided && typ != copy.kind()) { 377 LIBSEMIGROUPS_EXCEPTION("incompatible types of congruence, found (" 378 + congruence_type_to_string(copy.kind()) + " / " 379 + congruence_type_to_string(typ) 380 + ") but only (left / left), (right / " 381 "right), (two-sided / *) are valid"); 382 } 383 copy_relations_for_quotient(copy); 384 } 385 ToddCoxeter(congruence_type typ,fpsemigroup::ToddCoxeter & copy)386 ToddCoxeter::ToddCoxeter(congruence_type typ, 387 fpsemigroup::ToddCoxeter& copy) 388 : ToddCoxeter(typ) { 389 set_parent_froidure_pin(copy); 390 if (copy.finished()) { 391 set_nr_generators(copy.froidure_pin()->nr_generators()); 392 _settings->froidure_pin = policy::froidure_pin::use_cayley_graph; 393 394 } else { 395 copy_relations_for_quotient(copy.congruence()); 396 _settings->froidure_pin = policy::froidure_pin::use_relations; 397 } 398 } 399 ToddCoxeter(congruence_type typ,fpsemigroup::KnuthBendix & kb)400 ToddCoxeter::ToddCoxeter(congruence_type typ, fpsemigroup::KnuthBendix& kb) 401 : ToddCoxeter(typ) { 402 set_nr_generators(kb.alphabet().size()); 403 // TODO(later) use active rules when available 404 for (auto it = kb.cbegin_rules(); it < kb.cend_rules(); ++it) { 405 add_pair(kb.string_to_word(it->first), kb.string_to_word(it->second)); 406 } 407 // FIXME something goes horribly wrong if the next line is above the for 408 // loop above. 409 set_parent_froidure_pin(kb); 410 if (kb.finished() && kb.is_obviously_finite()) { 411 LIBSEMIGROUPS_ASSERT(_settings->froidure_pin 412 == policy::froidure_pin::none); 413 _settings->froidure_pin = policy::froidure_pin::use_cayley_graph; 414 } 415 } 416 417 ToddCoxeter::~ToddCoxeter() = default; 418 419 //////////////////////////////////////////////////////////////////////// 420 // CongruenceInterface - non-pure virtual member functions - public 421 //////////////////////////////////////////////////////////////////////// 422 contains(word_type const & lhs,word_type const & rhs)423 bool ToddCoxeter::contains(word_type const& lhs, word_type const& rhs) { 424 validate_word(lhs); 425 validate_word(rhs); 426 init(); 427 if (!_prefilled && _relations.empty() && _extra.empty()) { 428 // This defines the free semigroup 429 return lhs == rhs; 430 } 431 return CongruenceInterface::contains(lhs, rhs); 432 } 433 434 //////////////////////////////////////////////////////////////////////// 435 // ToddCoxeter - member functions (init + settings) - public 436 //////////////////////////////////////////////////////////////////////// 437 438 // Init prefill(Table const & table)439 void ToddCoxeter::prefill(Table const& table) { 440 prefill_and_validate(table, true); 441 init_preimages_from_table(); 442 } 443 444 // Settings 445 ToddCoxeter& froidure_pin_policy(policy::froidure_pin x)446 ToddCoxeter::froidure_pin_policy(policy::froidure_pin x) noexcept { 447 _settings->froidure_pin = x; 448 return *this; 449 } 450 froidure_pin_policy() const451 ToddCoxeter::policy::froidure_pin ToddCoxeter::froidure_pin_policy() const 452 noexcept { 453 return _settings->froidure_pin; 454 } 455 lookahead(policy::lookahead x)456 ToddCoxeter& ToddCoxeter::lookahead(policy::lookahead x) noexcept { 457 _settings->lookahead = x; 458 return *this; 459 } 460 lower_bound(size_t n)461 ToddCoxeter& ToddCoxeter::lower_bound(size_t n) noexcept { 462 _settings->lower_bound = n; 463 return *this; 464 } 465 next_lookahead(size_t n)466 ToddCoxeter& ToddCoxeter::next_lookahead(size_t n) noexcept { 467 _settings->next_lookahead = n; 468 return *this; 469 } 470 standardize(bool x)471 ToddCoxeter& ToddCoxeter::standardize(bool x) noexcept { 472 _settings->standardize = x; 473 return *this; 474 } 475 save(bool x)476 ToddCoxeter& ToddCoxeter::save(bool x) { 477 if ((_prefilled 478 || (has_parent_froidure_pin() 479 && parent_froidure_pin()->is_finite() == tril::TRUE 480 && (_settings->froidure_pin == policy::froidure_pin::none 481 || _settings->froidure_pin 482 == policy::froidure_pin::use_cayley_graph))) 483 && x) { 484 LIBSEMIGROUPS_EXCEPTION("cannot use the save setting with a " 485 "prefilled ToddCoxeter instance"); 486 } 487 _settings->save = x; 488 return *this; 489 } 490 strategy(policy::strategy x)491 ToddCoxeter& ToddCoxeter::strategy(policy::strategy x) { 492 if ((_prefilled 493 || (has_parent_froidure_pin() 494 && parent_froidure_pin()->is_finite() == tril::TRUE 495 && (_settings->froidure_pin == policy::froidure_pin::none 496 || _settings->froidure_pin 497 == policy::froidure_pin::use_cayley_graph))) 498 && x == policy::strategy::felsch) { 499 LIBSEMIGROUPS_EXCEPTION("cannot use the Felsch strategy with a " 500 "prefilled ToddCoxeter instance"); 501 } 502 _settings->strategy = x; 503 return *this; 504 } 505 strategy() const506 ToddCoxeter::policy::strategy ToddCoxeter::strategy() const noexcept { 507 return _settings->strategy; 508 } 509 510 ToddCoxeter& random_interval(std::chrono::nanoseconds x)511 ToddCoxeter::random_interval(std::chrono::nanoseconds x) noexcept { 512 _settings->random_interval = x; 513 return *this; 514 } 515 516 //////////////////////////////////////////////////////////////////////// 517 // ToddCoxeter - member functions (container-like) - public 518 //////////////////////////////////////////////////////////////////////// 519 empty() const520 bool ToddCoxeter::empty() const { 521 return _relations.empty() && _extra.empty() && nr_cosets_active() == 1; 522 } 523 reserve(size_t n)524 void ToddCoxeter::reserve(size_t n) { 525 size_t m = coset_capacity(); 526 if (n > m) { 527 m = n - m; 528 _table.add_rows(m); 529 _preim_init.add_rows(m); 530 _preim_next.add_rows(m); 531 add_free_cosets(m); 532 } 533 } 534 shrink_to_fit()535 void ToddCoxeter::shrink_to_fit() { 536 if (!finished()) { 537 return; 538 } 539 if (!is_standardized()) { 540 standardize(order::shortlex); 541 } 542 543 _table.shrink_rows_to(nr_cosets_active()); 544 // Cannot delete _preim_init or _preim_next because they are required by 545 // standardize 546 _preim_init.shrink_rows_to(nr_cosets_active()); 547 _preim_next.shrink_rows_to(nr_cosets_active()); 548 _relations.clear(); 549 _relations.shrink_to_fit(); 550 _extra.clear(); 551 _extra.shrink_to_fit(); 552 erase_free_cosets(); 553 } 554 555 //////////////////////////////////////////////////////////////////////// 556 // ToddCoxeter - member functions (state) - public 557 //////////////////////////////////////////////////////////////////////// 558 complete() const559 bool ToddCoxeter::complete() const noexcept { 560 size_t const n = nr_generators(); 561 coset_type c = _id_coset; 562 while (c != first_free_coset()) { 563 for (size_t a = 0; a < n; ++a) { 564 if (_table.get(c, a) == UNDEFINED) { 565 return false; 566 } 567 } 568 c = next_active_coset(c); 569 } 570 return true; 571 } 572 compatible() const573 bool ToddCoxeter::compatible() const noexcept { 574 coset_type c = _id_coset; 575 while (c != first_free_coset()) { 576 for (auto it = _relations.cbegin(); it < _relations.cend(); it += 2) { 577 coset_type x = tau(c, (*it).cbegin(), (*it).cend()); 578 LIBSEMIGROUPS_ASSERT(is_active_coset(x) || x == UNDEFINED); 579 coset_type y = tau(c, (*(it + 1)).cbegin(), (*(it + 1)).cend()); 580 LIBSEMIGROUPS_ASSERT(is_active_coset(y) || y == UNDEFINED); 581 if (x != y) { 582 return false; 583 } 584 } 585 c = next_active_coset(c); 586 } 587 return true; 588 } 589 590 //////////////////////////////////////////////////////////////////////// 591 // ToddCoxeter - member functions (standardization) - public 592 //////////////////////////////////////////////////////////////////////// 593 is_standardized() const594 bool ToddCoxeter::is_standardized() const noexcept { 595 return _standardized != order::none; 596 } 597 standardize(order rdr)598 void ToddCoxeter::standardize(order rdr) { 599 if (_standardized == rdr || empty()) { 600 return; 601 } 602 switch (rdr) { 603 case order::shortlex: 604 init_standardize(); 605 shortlex_standardize(); 606 break; 607 case order::lex: 608 init_standardize(); 609 lex_standardize(); 610 break; 611 case order::recursive: 612 init_standardize(); 613 recursive_standardize(); 614 break; 615 case order::none: { 616 } 617 } 618 if (finished()) { 619 _standardized = rdr; 620 } 621 } 622 623 //////////////////////////////////////////////////////////////////////// 624 // CongruenceInterface - pure virtual member functions - private 625 //////////////////////////////////////////////////////////////////////// 626 class_index_to_word_impl(coset_type i)627 word_type ToddCoxeter::class_index_to_word_impl(coset_type i) { 628 run(); 629 if (!is_standardized()) { 630 standardize(order::shortlex); 631 } 632 LIBSEMIGROUPS_ASSERT(finished()); 633 word_type w; 634 TreeNode tn = (*_tree)[i + 1]; 635 while (tn.parent != UNDEFINED) { 636 w.push_back(tn.gen); 637 tn = (*_tree)[tn.parent]; 638 } 639 if (kind() != congruence_type::left) { 640 std::reverse(w.begin(), w.end()); 641 } 642 return w; 643 } 644 nr_classes_impl()645 size_t ToddCoxeter::nr_classes_impl() { 646 run(); 647 LIBSEMIGROUPS_ASSERT(finished()); 648 return nr_cosets_active() - 1; 649 } 650 quotient_impl()651 std::shared_ptr<FroidurePinBase> ToddCoxeter::quotient_impl() { 652 using detail::TCE; 653 run(); 654 LIBSEMIGROUPS_ASSERT(finished()); 655 if (!is_standardized()) { 656 standardize(order::shortlex); 657 } 658 659 // TODO(later) replace with 0-parameter constructor when available 660 std::vector<TCE> gens; 661 TCE x(this); 662 for (size_t i = 0; i < nr_generators(); ++i) { 663 // We use _table.get(0, i) instead of just i, because there might be 664 // more generators than cosets. 665 gens.emplace_back(x, _table.get(0, i)); 666 } 667 return std::make_shared<FroidurePin<TCE>>(gens); 668 } 669 run_impl()670 void ToddCoxeter::run_impl() { 671 if (is_quotient_obviously_infinite()) { 672 LIBSEMIGROUPS_EXCEPTION( 673 "there are infinitely many classes in the congruence and " 674 "Todd-Coxeter will never terminate"); 675 } 676 if (_settings->lower_bound != UNDEFINED) { 677 size_t const bound = _settings->lower_bound; 678 _settings->lower_bound = UNDEFINED; 679 run_until([this, &bound]() -> bool { 680 return (nr_cosets_active() == bound) && complete(); 681 }); 682 } else if (_settings->strategy == policy::strategy::felsch) { 683 felsch(); 684 } else if (_settings->strategy == policy::strategy::hlt) { 685 hlt(); 686 } else if (_settings->strategy == policy::strategy::random) { 687 sims(); 688 } 689 } 690 finished_impl() const691 bool ToddCoxeter::finished_impl() const { 692 return _state == state::finished; 693 } 694 word_to_class_index_impl(word_type const & w)695 coset_type ToddCoxeter::word_to_class_index_impl(word_type const& w) { 696 run(); 697 LIBSEMIGROUPS_ASSERT(finished()); 698 if (!is_standardized()) { 699 standardize(order::shortlex); 700 } 701 coset_type c = const_word_to_class_index(w); 702 // c is in the range 1, ..., nr_cosets_active() because 0 represents the 703 // identity coset, and does not correspond to an element. 704 return c; 705 } 706 707 //////////////////////////////////////////////////////////////////////// 708 // CongruenceInterface - non-pure virtual member functions - private 709 //////////////////////////////////////////////////////////////////////// 710 711 coset_type const_word_to_class_index(word_type const & w) const712 ToddCoxeter::const_word_to_class_index(word_type const& w) const { 713 validate_word(w); 714 coset_type c = _id_coset; 715 716 if (kind() == congruence_type::left) { 717 c = tau(c, w.crbegin(), w.crend()); 718 } else { 719 c = tau(c, w.cbegin(), w.cend()); 720 } 721 return (c == UNDEFINED ? c : c - 1); 722 } 723 is_quotient_obviously_finite_impl()724 bool ToddCoxeter::is_quotient_obviously_finite_impl() { 725 if (finished()) { 726 return true; 727 } 728 init(); 729 return _prefilled; 730 // _prefilled means that either we were created from a FroidurePinBase* 731 // with _settings->froidure_pin = use_cayley_graph and we successfully 732 // prefilled the table, or we manually prefilled the table. In this case 733 // the semigroup defined by _relations must be finite. 734 } 735 is_quotient_obviously_infinite_impl()736 bool ToddCoxeter::is_quotient_obviously_infinite_impl() { 737 if (finished()) { 738 return false; 739 } 740 init(); 741 if (_prefilled) { 742 return false; 743 } else if (nr_generators() > _relations.size() + _extra.size()) { 744 return true; 745 } 746 detail::IsObviouslyInfinite<letter_type, word_type> ioi(nr_generators()); 747 ioi.add_rules(_relations.cbegin(), _relations.cend()); 748 ioi.add_rules(_extra.cbegin(), _extra.cend()); 749 return ioi.result(); 750 } 751 set_nr_generators_impl(size_t n)752 void ToddCoxeter::set_nr_generators_impl(size_t n) { 753 // TODO(later) add columns to make it up to n? 754 _preim_init = Table(n, 1, UNDEFINED); 755 _preim_next = Table(n, 1, UNDEFINED); 756 _table = Table(n, 1, UNDEFINED); 757 } 758 759 //////////////////////////////////////////////////////////////////////// 760 // ToddCoxeter - member functions (validation) - private 761 //////////////////////////////////////////////////////////////////////// 762 validate_table(Table const & table,size_t const first,size_t const last) const763 void ToddCoxeter::validate_table(Table const& table, 764 size_t const first, 765 size_t const last) const { 766 REPORT_DEBUG_DEFAULT("validating coset table...\n"); 767 if (nr_generators() == UNDEFINED) { 768 LIBSEMIGROUPS_EXCEPTION("no generators have been defined"); 769 } else if (table.nr_cols() != nr_generators()) { 770 LIBSEMIGROUPS_EXCEPTION("invalid table, expected %d columns, found %d", 771 nr_generators(), 772 table.nr_cols()); 773 } 774 if (last - first <= 0) { 775 LIBSEMIGROUPS_EXCEPTION( 776 "invalid table, expected at least 1 rows, found %d", 777 table.nr_rows()); 778 } 779 for (size_t i = first; i < last; ++i) { 780 for (size_t j = 0; j < table.nr_cols(); ++j) { 781 coset_type c = table.get(i, j); 782 if (c < first || c >= last) { 783 LIBSEMIGROUPS_EXCEPTION( 784 "invalid table, expected entries in the range [%d, %d), found " 785 "%d in row %d, column %d", 786 i, 787 j, 788 first, 789 last, 790 c); 791 } 792 } 793 } 794 REPORT_DEBUG_DEFAULT("...coset table ok\n"); 795 } 796 797 //////////////////////////////////////////////////////////////////////// 798 // ToddCoxeter - member functions (initialisation) - private 799 //////////////////////////////////////////////////////////////////////// 800 801 //! Copy all _relations and _extra from copy into _relations of this copy_relations_for_quotient(ToddCoxeter & copy)802 void ToddCoxeter::copy_relations_for_quotient(ToddCoxeter& copy) { 803 REPORT_DEBUG_DEFAULT("copying relations for quotient...\n"); 804 LIBSEMIGROUPS_ASSERT(empty()); 805 copy.init(); 806 set_nr_generators(copy.nr_generators()); 807 _state = state::initialized; 808 _relations = copy._relations; 809 _relations.insert( 810 _relations.end(), copy._extra.cbegin(), copy._extra.cend()); 811 if (kind() == congruence_type::left 812 && copy.kind() != congruence_type::left) { 813 for (auto& w : _relations) { 814 std::reverse(w.begin(), w.end()); 815 } 816 } 817 _nr_pairs_added_earlier = 0; 818 } 819 init()820 void ToddCoxeter::init() { 821 if (_state == state::constructed) { 822 REPORT_DEBUG_DEFAULT("initializing...\n"); 823 // Add the relations/Cayley graph from parent() if any. 824 if (has_parent_froidure_pin() 825 && parent_froidure_pin()->is_finite() == tril::TRUE) { 826 if (_settings->froidure_pin == policy::froidure_pin::use_cayley_graph 827 || _settings->froidure_pin == policy::froidure_pin::none) { 828 REPORT_DEBUG_DEFAULT("using Cayley graph...\n"); 829 LIBSEMIGROUPS_ASSERT(_relations.empty()); 830 prefill(*parent_froidure_pin()); 831 #ifdef LIBSEMIGROUPS_DEBUG 832 // This is a check of program logic, since we use parent() to fill 833 // the table, so we only validate in debug mode. 834 validate_table(_table, 1, parent_froidure_pin()->size() + 1); 835 #endif 836 } else { 837 REPORT_DEBUG_DEFAULT("using presentation...\n"); 838 LIBSEMIGROUPS_ASSERT(_settings->froidure_pin 839 == policy::froidure_pin::use_relations); 840 auto sucker = [this](word_type const& w) -> void { 841 reverse_if_necessary_and_push_back(w, _relations); 842 }; 843 relations(*parent_froidure_pin(), sucker); 844 #ifdef LIBSEMIGROUPS_DEBUG 845 // This is a check of program logic, since we use parent() to 846 // obtain the relations, so we only validate in debug mode. 847 for (auto const& rel : _relations) { 848 validate_word(rel); 849 } 850 // We don't add anything to _extra here so no need to check. 851 #endif 852 } 853 } 854 _state = state::initialized; 855 } 856 857 // Get new generating pairs (if any) from CongruenceInterface (if any) 858 auto it = cbegin_generating_pairs() + _nr_pairs_added_earlier; 859 if (kind() != congruence_type::twosided) { 860 for (; it < cend_generating_pairs(); ++it) { 861 reverse_if_necessary_and_push_back(it->first, _extra); 862 reverse_if_necessary_and_push_back(it->second, _extra); 863 } 864 } else { 865 for (; it < cend_generating_pairs(); ++it) { 866 reverse_if_necessary_and_push_back(it->first, _relations); 867 reverse_if_necessary_and_push_back(it->second, _relations); 868 } 869 } 870 _nr_pairs_added_earlier 871 = cend_generating_pairs() - cbegin_generating_pairs(); 872 } 873 init_felsch_tree()874 void ToddCoxeter::init_felsch_tree() { 875 LIBSEMIGROUPS_ASSERT(_state >= state::initialized); 876 if (_felsch_tree == nullptr) { 877 REPORT_DEFAULT("initializing the Felsch tree...\n"); 878 detail::Timer tmr; 879 _felsch_tree = detail::make_unique<FelschTree>(this); 880 _felsch_tree->add_relations(_relations); 881 REPORT_TIME(tmr); 882 } 883 } 884 init_preimages_from_table()885 void ToddCoxeter::init_preimages_from_table() { 886 REPORT_DEBUG("initializing preimages...\n"); 887 LIBSEMIGROUPS_ASSERT(_table.nr_cols() == nr_generators()); 888 LIBSEMIGROUPS_ASSERT(_table.nr_rows() >= nr_cosets_active()); 889 LIBSEMIGROUPS_ASSERT(_prefilled); 890 LIBSEMIGROUPS_ASSERT(_state == state::constructed); 891 LIBSEMIGROUPS_ASSERT(_relations.empty()); 892 893 for (coset_type c = 0; c < nr_cosets_active(); c++) { 894 for (size_t i = 0; i < nr_generators(); i++) { 895 coset_type b = _table.get(c, i); 896 _preim_next.set(c, i, _preim_init.get(b, i)); 897 _preim_init.set(b, i, c); 898 } 899 } 900 } 901 prefill(FroidurePinBase & S)902 void ToddCoxeter::prefill(FroidurePinBase& S) { 903 REPORT_DEBUG_DEFAULT("prefilling the coset table from FroidurePin...\n"); 904 LIBSEMIGROUPS_ASSERT(_state == state::constructed); 905 LIBSEMIGROUPS_ASSERT( 906 _settings->froidure_pin == policy::froidure_pin::use_cayley_graph 907 || _settings->froidure_pin == policy::froidure_pin::none); 908 LIBSEMIGROUPS_ASSERT(S.nr_generators() == nr_generators()); 909 if (kind() == congruence_type::left) { 910 prefill_and_validate(S.left_cayley_graph(), false); 911 } else { 912 prefill_and_validate(S.right_cayley_graph(), false); 913 } 914 for (size_t i = 0; i < nr_generators(); i++) { 915 _table.set(0, i, S.letter_to_pos(i) + 1); 916 } 917 init_preimages_from_table(); 918 } 919 prefill_and_validate(Table const & table,bool validate)920 void ToddCoxeter::prefill_and_validate(Table const& table, bool validate) { 921 if (_settings->strategy == policy::strategy::felsch) { 922 LIBSEMIGROUPS_EXCEPTION( 923 "it is not possible to prefill when using the Felsch strategy"); 924 } 925 if (!empty()) { 926 LIBSEMIGROUPS_EXCEPTION("cannot prefill a non-empty instance") 927 } 928 if (validate) { 929 validate_table(table, 0, table.nr_rows()); 930 } 931 932 REPORT_DEBUG("prefilling the coset table...\n"); 933 _prefilled = true; 934 size_t m = table.nr_rows() + 1; 935 _table.add_rows(m - _table.nr_rows()); 936 for (size_t i = 0; i < _table.nr_cols(); i++) { 937 _table.set(0, i, i + 1); 938 } 939 for (size_t row = 0; row < _table.nr_rows() - 1; ++row) { 940 for (size_t col = 0; col < _table.nr_cols(); ++col) { 941 _table.set(row + 1, col, table.get(row, col) + 1); 942 } 943 } 944 add_active_cosets(m - nr_cosets_active()); 945 _preim_init.add_rows(m - _preim_init.nr_rows()); 946 _preim_next.add_rows(m - _preim_next.nr_rows()); 947 } 948 949 void reverse_if_necessary_and_push_back(word_type w,std::vector<word_type> & v)950 ToddCoxeter::reverse_if_necessary_and_push_back(word_type w, 951 std::vector<word_type>& v) { 952 if (kind() == congruence_type::left) { 953 std::reverse(w.begin(), w.end()); 954 } 955 v.push_back(std::move(w)); 956 } 957 958 //////////////////////////////////////////////////////////////////////// 959 // ToddCoxeter - member functions (cosets) - private 960 //////////////////////////////////////////////////////////////////////// 961 new_coset()962 coset_type ToddCoxeter::new_coset() { 963 if (!has_free_cosets()) { 964 reserve(2 * coset_capacity()); 965 return new_active_coset(); 966 } else { 967 coset_type const c = new_active_coset(); 968 // Clear the new coset's row in each table 969 for (letter_type i = 0; i < nr_generators(); i++) { 970 _table.set(c, i, UNDEFINED); 971 _preim_init.set(c, i, UNDEFINED); 972 } 973 return c; 974 } 975 } 976 remove_preimage(coset_type const cx,letter_type const x,coset_type const d)977 void ToddCoxeter::remove_preimage(coset_type const cx, 978 letter_type const x, 979 coset_type const d) { 980 LIBSEMIGROUPS_ASSERT(is_active_coset(cx)); 981 LIBSEMIGROUPS_ASSERT(is_valid_coset(d)); 982 coset_type e = _preim_init.get(cx, x); 983 if (e == d) { 984 _preim_init.set(cx, x, _preim_next.get(d, x)); 985 } else { 986 while (_preim_next.get(e, x) != d) { 987 e = _preim_next.get(e, x); 988 } 989 LIBSEMIGROUPS_ASSERT(_preim_next.get(e, x) == d); 990 _preim_next.set(e, x, _preim_next.get(d, x)); 991 } 992 } 993 994 // Perform a DFS in _felsch_tree make_deductions_dfs(coset_type const c)995 void ToddCoxeter::make_deductions_dfs(coset_type const c) { 996 for (auto it = _felsch_tree->cbegin(); it < _felsch_tree->cend(); ++it) { 997 push_definition_felsch<StackDeductions, DoNotProcessCoincidences>( 998 c, _relations[*it], _relations[*it + 1]); 999 } 1000 1001 size_t const n = nr_generators(); 1002 for (size_t x = 0; x < n; ++x) { 1003 if (_felsch_tree->push_front(x)) { 1004 coset_type e = _preim_init.get(c, x); 1005 while (e != UNDEFINED) { 1006 make_deductions_dfs(e); 1007 e = _preim_next.get(e, x); 1008 } 1009 _felsch_tree->pop_front(); 1010 } 1011 } 1012 } 1013 process_deductions()1014 void ToddCoxeter::process_deductions() { 1015 LIBSEMIGROUPS_ASSERT(!_prefilled); 1016 #ifdef LIBSEMIGROUPS_VERBOSE 1017 if (!_deduct.empty()) { 1018 REPORT_VERBOSE_DEFAULT("processing %llu deductions . . .\n", 1019 _deduct.size()); 1020 } 1021 #endif 1022 while (!_deduct.empty()) { 1023 auto d = _deduct.top(); 1024 _deduct.pop(); 1025 if (is_active_coset(d.first)) { 1026 _felsch_tree->push_back(d.second); 1027 make_deductions_dfs(d.first); 1028 process_coincidences<StackDeductions>(); 1029 } 1030 } 1031 process_coincidences<StackDeductions>(); 1032 if (!_deduct.empty()) { 1033 process_deductions(); 1034 } 1035 } 1036 1037 //////////////////////////////////////////////////////////////////////// 1038 // ToddCoxeter - member functions (main strategies) - private 1039 //////////////////////////////////////////////////////////////////////// 1040 felsch()1041 void ToddCoxeter::felsch() { 1042 REPORT_DEFAULT("performing Felsch %s standardization...\n", 1043 _settings->standardize ? "with" : "without"); 1044 detail::Timer tmr; 1045 init(); 1046 coset_type t = 0; 1047 size_t const n = nr_generators(); 1048 // Can only initialise _felsch_tree here because we require _relations 1049 // to be complete. 1050 init_felsch_tree(); 1051 if (_state == state::initialized) { 1052 LIBSEMIGROUPS_ASSERT(_settings->strategy == policy::strategy::felsch); 1053 for (auto it = _extra.cbegin(); it < _extra.cend(); it += 2) { 1054 push_definition_hlt<StackDeductions, ProcessCoincidences>( 1055 _id_coset, *it, *(it + 1)); 1056 } 1057 if (_settings->standardize) { 1058 for (letter_type x = 0; x < n; ++x) { 1059 standardize_immediate(_id_coset, t, x); 1060 } 1061 } 1062 if (!_prefilled) { 1063 if (_relations.empty()) { 1064 _felsch_tree->add_relations(_extra); 1065 _extra.swap(_relations); 1066 } 1067 process_deductions(); 1068 // process_deductions doesn't work if the table is prefilled 1069 } 1070 } else if (_state == state::hlt) { 1071 _current = _id_coset; 1072 } 1073 _state = state::felsch; 1074 while (_current != first_free_coset() && !stopped()) { 1075 for (letter_type a = 0; a < n; ++a) { 1076 if (_table.get(_current, a) == UNDEFINED) { 1077 define<StackDeductions>(_current, a, new_coset()); 1078 process_deductions(); 1079 #ifdef LIBSEMIGROUPS_DEBUG 1080 if (_settings->enable_debug_verify_no_missing_deductions) { 1081 debug_verify_no_missing_deductions(); 1082 } 1083 #endif 1084 } 1085 if (_settings->standardize) { 1086 standardize_immediate(_current, t, a); 1087 } 1088 } 1089 if (report()) { 1090 TODD_COXETER_REPORT_COSETS() 1091 } 1092 _current = next_active_coset(_current); 1093 } 1094 LIBSEMIGROUPS_ASSERT(_coinc.empty()); 1095 LIBSEMIGROUPS_ASSERT(_deduct.empty()); 1096 if (!stopped()) { 1097 LIBSEMIGROUPS_ASSERT(_current == first_free_coset()); 1098 _state = state::finished; 1099 } 1100 TODD_COXETER_REPORT_COSETS() 1101 REPORT_TIME(tmr); 1102 report_why_we_stopped(); 1103 } 1104 1105 // Walker's Strategy 1 = HLT = ACE style-R hlt()1106 void ToddCoxeter::hlt() { 1107 REPORT_DEFAULT("performing HLT %s standardization, %s lookahead, and%s" 1108 "deduction processing...\n", 1109 _settings->standardize ? "with" : "without", 1110 _settings->lookahead == policy::lookahead::partial 1111 ? "partial" 1112 : "full", 1113 _settings->save ? " " : " no "); 1114 detail::Timer tmr; 1115 init(); 1116 1117 coset_type t = 0; 1118 if (_state == state::initialized) { 1119 for (auto it = _extra.cbegin(); it < _extra.cend(); it += 2) { 1120 push_definition_hlt<DoNotStackDeductions, ProcessCoincidences>( 1121 _id_coset, *it, *(it + 1)); 1122 } 1123 if (_settings->standardize) { 1124 size_t const n = nr_generators(); 1125 for (letter_type x = 0; x < n; ++x) { 1126 standardize_immediate(_id_coset, t, x); 1127 } 1128 } 1129 if (!_prefilled) { 1130 if (_relations.empty()) { 1131 _extra.swap(_relations); 1132 } 1133 } 1134 } else if (_state == state::felsch) { 1135 _current = _id_coset; 1136 } 1137 _state = state::hlt; 1138 1139 if (_settings->save) { 1140 init_felsch_tree(); 1141 } 1142 // size_t const n = nr_generators(); 1143 while (_current != first_free_coset() && !stopped()) { 1144 if (!_settings->save) { 1145 for (auto it = _relations.cbegin(); it < _relations.cend(); it += 2) { 1146 push_definition_hlt<DoNotStackDeductions, ProcessCoincidences>( 1147 _current, *it, *(it + 1)); 1148 } 1149 // Row filling 1150 // for (letter_type x = 0; x < n; ++x) { 1151 // if (tau(_current, x) == UNDEFINED) { 1152 // define<DoNotStackDeductions>(_current, x, new_coset()); 1153 // } 1154 // } 1155 } else { 1156 for (auto it = _relations.cbegin(); it < _relations.cend(); it += 2) { 1157 push_definition_hlt<StackDeductions, DoNotProcessCoincidences>( 1158 _current, *it, *(it + 1)); 1159 process_deductions(); 1160 } 1161 // Row filling 1162 // for (letter_type x = 0; x < n; ++x) { 1163 // if (tau(_current, x) == UNDEFINED) { 1164 // define<StackDeductions>(_current, x, new_coset()); 1165 // } 1166 // } 1167 } 1168 if (nr_cosets_active() > _settings->next_lookahead) { 1169 perform_lookahead(); 1170 } 1171 if (_settings->standardize) { 1172 size_t const n = nr_generators(); 1173 for (letter_type x = 0; x < n; ++x) { 1174 standardize_immediate(_current, t, x); 1175 } 1176 } 1177 if (report()) { 1178 TODD_COXETER_REPORT_COSETS() 1179 } 1180 _current = next_active_coset(_current); 1181 } 1182 LIBSEMIGROUPS_ASSERT(_coinc.empty()); 1183 LIBSEMIGROUPS_ASSERT(_deduct.empty()); 1184 if (!stopped()) { 1185 LIBSEMIGROUPS_ASSERT(_current == first_free_coset()); 1186 _state = state::finished; 1187 } 1188 TODD_COXETER_REPORT_COSETS(); 1189 REPORT_TIME(tmr); 1190 report_why_we_stopped(); 1191 } 1192 1193 // This is not exactly Sim's TEN_CE, since all of the variants of 1194 // Todd-Coxeter represented in TEN_CE (that apply to semigroups/monoids) 1195 // are already accounted for in the above. sims()1196 void ToddCoxeter::sims() { 1197 REPORT_DEFAULT("performing random Sims' TEN_CE strategy...\n"); 1198 using int_dist_type 1199 = std::uniform_int_distribution<std::mt19937::result_type>; 1200 static int_dist_type dist(0, 9); 1201 static std::mt19937 mt; 1202 1203 static constexpr std::array<bool, 8> full 1204 = {true, true, true, true, false, false, false, false}; 1205 static constexpr std::array<bool, 10> stand 1206 = {true, true, false, false, true, true, false, false, true, false}; 1207 static constexpr std::array<bool, 8> save_it 1208 = {true, false, true, false, true, false, true, false}; 1209 1210 static const std::string line = std::string(79, '#') + '\n'; 1211 #ifdef LIBSEMIGROUPS_DEBUG 1212 // Don't check for missing deductions, because when changing from HLT to 1213 // Felsch and back repeatedly, there can be missing deductions after 1214 // deduction processing in Felsch (caused by not pushing all relations 1215 // through all cosets in HLT). 1216 _settings->enable_debug_verify_no_missing_deductions = false; 1217 #endif 1218 while (!finished()) { 1219 size_t m = dist(mt); 1220 if (m < 8) { 1221 strategy(policy::strategy::hlt); 1222 lookahead( 1223 (full[m] ? policy::lookahead::full : policy::lookahead::partial)); 1224 try { 1225 save(save_it[m]); 1226 } catch (...) { 1227 // It isn't always possible to use the save option (when this is 1228 // created from a Cayley table, for instance), and 1229 // ToddCoxeter::save throws if this is the case. 1230 } 1231 } else { 1232 try { 1233 strategy(policy::strategy::felsch); 1234 } catch (...) { 1235 // It isn't always possible to use the Felsch strategy (when this 1236 // is created from a Cayley table, for instance), and 1237 // ToddCoxeter::save throws if this is the case. 1238 } 1239 } 1240 standardize(stand[m]); 1241 1242 REPORT(line).prefix().color(fmt::color::dim_gray).flush(); 1243 // Second param, means don't lock, since we already locked in run_impl 1244 // above. 1245 run_for(_settings->random_interval); 1246 } 1247 LIBSEMIGROUPS_ASSERT(_coinc.empty()); 1248 LIBSEMIGROUPS_ASSERT(_deduct.empty()); 1249 // The next 2 lines are necessary because if we are changing from HLT to 1250 // Felsch repeatedly, we can be in the situation where the table is 1251 // complete but not compatible. Test [ToddCoxeter][048] is a good example 1252 // of this. 1253 lookahead(policy::lookahead::full); 1254 perform_lookahead(); 1255 } 1256 1257 // TODO(later) we could use deduction processing here instead of this, 1258 // where appropriate? perform_lookahead()1259 void ToddCoxeter::perform_lookahead() { 1260 state const old_state = _state; 1261 _state = state::lookahead; 1262 if (_settings->lookahead == policy::lookahead::partial) { 1263 REPORT_DEFAULT("performing partial lookahead...\n"); 1264 // Start lookahead from the coset after _current 1265 _current_la = next_active_coset(_current); 1266 } else { 1267 LIBSEMIGROUPS_ASSERT(_settings->lookahead == policy::lookahead::full); 1268 REPORT_DEFAULT("performing full lookahead...\n"); 1269 // Start from the first coset 1270 _current_la = _id_coset; 1271 } 1272 TODD_COXETER_REPORT_COSETS() 1273 1274 size_t nr_killed = nr_cosets_killed(); 1275 while (_current_la != first_free_coset() 1276 // when running the random sims method the state is finished at 1277 // this point, and so stopped() == true, but we anyway want to 1278 // perform a full lookahead, which is why "_state == 1279 // state::finished" is in the next line. 1280 && (old_state == state::finished || !stopped())) { 1281 for (auto it = _relations.cbegin(); it < _relations.cend(); it += 2) { 1282 push_definition_felsch<DoNotStackDeductions, ProcessCoincidences>( 1283 _current_la, *it, *(it + 1)); 1284 } 1285 _current_la = next_active_coset(_current_la); 1286 if (report()) { 1287 TODD_COXETER_REPORT_COSETS() 1288 } 1289 } 1290 nr_killed = nr_cosets_killed() - nr_killed; 1291 if (nr_cosets_active() > _settings->next_lookahead 1292 || nr_killed < (nr_cosets_active() / 4)) { 1293 _settings->next_lookahead *= 2; 1294 } 1295 REPORT_DEFAULT("%2d cosets killed\n", nr_killed); 1296 _state = old_state; 1297 } 1298 1299 //////////////////////////////////////////////////////////////////////// 1300 // ToddCoxeter - member functions (standardize) - private 1301 //////////////////////////////////////////////////////////////////////// 1302 init_standardize()1303 void ToddCoxeter::init_standardize() { 1304 if (_tree == nullptr) { 1305 _tree = detail::make_unique<std::vector<TreeNode>>(nr_cosets_active(), 1306 TreeNode()); 1307 } else { 1308 _tree->resize(nr_cosets_active()); 1309 } 1310 LIBSEMIGROUPS_ASSERT(_coinc.empty()); 1311 } 1312 1313 // Returns true if t is incremented (i.e. it's the first time we are 1314 // seeing and t as a coset in a standardization) and false otherwise. standardize_immediate(coset_type const s,coset_type & t,letter_type const x)1315 bool ToddCoxeter::standardize_immediate(coset_type const s, 1316 coset_type& t, 1317 letter_type const x) { 1318 LIBSEMIGROUPS_ASSERT(!finished()); 1319 coset_type const r = _table.get(s, x); 1320 if (r != UNDEFINED) { 1321 if (r > t) { 1322 t++; 1323 if (r > t) { 1324 swap(t, r); 1325 } 1326 return true; 1327 } 1328 } 1329 return false; 1330 } 1331 standardize_deferred(std::vector<coset_type> & p,std::vector<coset_type> & q,coset_type const s,coset_type & t,letter_type const x)1332 bool ToddCoxeter::standardize_deferred(std::vector<coset_type>& p, 1333 std::vector<coset_type>& q, 1334 coset_type const s, 1335 coset_type& t, 1336 letter_type const x) { 1337 // p : new -> old and q : old -> new 1338 coset_type r = _table.get(p[s], x); 1339 if (r != UNDEFINED) { 1340 r = q[r]; // new 1341 if (r > t) { 1342 t++; 1343 if (r > t) { 1344 TODD_COXETER_REPORT_SWITCH(r, t); 1345 std::swap(p[t], p[r]); 1346 std::swap(q[p[t]], q[p[r]]); 1347 } 1348 (*_tree)[t].parent = (s == t ? r : s); 1349 (*_tree)[t].gen = x; 1350 return true; 1351 } 1352 } 1353 return false; 1354 } 1355 lex_standardize()1356 void ToddCoxeter::lex_standardize() { 1357 REPORT_DEFAULT("standardizing (lex)... "); 1358 detail::Timer tmr; 1359 1360 coset_type s = 0; 1361 coset_type t = 0; 1362 letter_type x = 0; 1363 size_t const n = nr_generators(); 1364 std::vector<coset_type> p(coset_capacity(), 0); 1365 std::iota(p.begin(), p.end(), 0); 1366 std::vector<coset_type> q(coset_capacity(), 0); 1367 std::iota(q.begin(), q.end(), 0); 1368 1369 // Perform a DFS through the _table 1370 while (s <= t) { 1371 if (standardize_deferred(p, q, s, t, x)) { 1372 s = t; 1373 x = 0; 1374 continue; 1375 } 1376 x++; 1377 if (x == n) { // backtrack 1378 x = (*_tree)[s].gen; 1379 s = (*_tree)[s].parent; 1380 } 1381 } 1382 apply_permutation(p, q); 1383 1384 REPORT("%d\n", tmr).prefix().flush_right().flush(); 1385 #ifdef LIBSEMIGROUPS_DEBUG 1386 debug_validate_forwd_bckwd(); 1387 debug_validate_table(); 1388 // debug_validate_preimages(); 1389 #endif 1390 } 1391 shortlex_standardize()1392 void ToddCoxeter::shortlex_standardize() { 1393 REPORT_DEFAULT("standardizing (shortlex)... "); 1394 detail::Timer tmr; 1395 coset_type t = 0; 1396 size_t const n = nr_generators(); 1397 std::vector<coset_type> p(coset_capacity(), 0); 1398 std::iota(p.begin(), p.end(), 0); 1399 std::vector<coset_type> q(coset_capacity(), 0); 1400 std::iota(q.begin(), q.end(), 0); 1401 1402 for (coset_type s = 0; s <= t; ++s) { 1403 for (letter_type x = 0; x < n; ++x) { 1404 standardize_deferred(p, q, s, t, x); 1405 } 1406 } 1407 apply_permutation(p, q); 1408 REPORT("%d\n", tmr).prefix().flush_right().flush(); 1409 #ifdef LIBSEMIGROUPS_DEBUG 1410 debug_validate_forwd_bckwd(); 1411 debug_validate_table(); 1412 // debug_validate_preimages(); 1413 #endif 1414 } 1415 1416 // This is how the recursive words up to a given length M, and on an 1417 // arbitrary finite alphabet are generated. On a single letter alphabet, 1418 // this order is just increasing powers of the only generator: 1419 // 1420 // a < aa < aaa < aaaa < ... < aa...a (M times) 1421 // 1422 // With an n-letter alphabet A = {a_1, a_2, ..., a_n}, suppose we have 1423 // already obtained all of the words W_{n - 1} containing {a_1, ..., a_{n - 1424 // 1}}. Every word in W_{n - 1} is less than any word containing a_n, and 1425 // the least word greater than every word in W_{n - 1} is a_n. Words greater 1426 // than a_n are obtain in the follow way, where: 1427 // 1428 // x: is the maximum word in W_{n - 1}, this is constant, in the description 1429 // that follows. 1430 // u: the first word obtained in point (1), the first time it is applied 1431 // after (2) has been applied, starting with u = a_{n - 1}. 1432 // v: a word with one fewer letters than u, starting with the empty word. 1433 // w: a word such that w < u, also starting with the empty word. 1434 // 1435 // 1. If v < x, then v is replaced by the next word in the order. If |uv| <= 1436 // M, then the next word is uv. Otherwise, goto 1. 1437 // 1438 // 2. If v = x, then and there exists a word w' in the set of words obtained 1439 // so far such that w' > w and |w'| <= M - 1, then replace w with w', 1440 // replace u by wa_n, replace v by the empty word, and the next word is 1441 // wa_n. 1442 // 1443 // If no such word w' exists, then we have enumerated all the required 1444 // words, and we can stop. 1445 // 1446 // For example, if A = {a, b} and M = 4, then the initial elements in the 1447 // order are: 1448 // 1449 // e < a < aa < aaa < aaaa (e is the empty word) 1450 // 1451 // Set b > aaaa. At this point, x = aaaa, u = b, v = e, w = e, and so 1452 // (1) applies, v <- a, and since |uv| = ba <= 4 = M, the next word is 1453 // ba. Repeatedly applying (1), until it fails to hold, we obtain the 1454 // following: 1455 // 1456 // aaaa < b < ba < baa < baaa 1457 // 1458 // After defining baa < baaa, x = aaaa, u = b, v = aaaa, and w = e. Hence v 1459 // = x, and so (2) applies. The next w' in the set of words so far 1460 // enumerated is a, and |a| = 1 <= 3 = M - 1, and so w <- a, u <- ab, v <- 1461 // e, and the next word is ab. We repeatedly apply (1), until it fails, to 1462 // obtain 1463 // 1464 // baaa < ab < aba < abaa 1465 // 1466 // At which point u = b, v = aaaa = x, and w = a. Hence (2) applies, w <- 1467 // aa, v <- e, u <- aab, and the next word is: aab. And so on ... 1468 1469 // TODO(later): improve this, it is currently very slow. recursive_standardize()1470 void ToddCoxeter::recursive_standardize() { 1471 REPORT_DEFAULT("standardizing (recursive)... "); 1472 detail::Timer tmr; 1473 std::vector<word_type> out; 1474 size_t const n = nr_generators(); 1475 letter_type a = 0; 1476 coset_type s = 0; 1477 coset_type t = 0; 1478 1479 std::vector<coset_type> p(coset_capacity(), 0); 1480 std::iota(p.begin(), p.end(), 0); 1481 std::vector<coset_type> q(coset_capacity(), 0); 1482 std::iota(q.begin(), q.end(), 0); 1483 1484 while (s <= t) { 1485 if (standardize_deferred(p, q, s, t, 0)) { 1486 out.push_back(word_type(t, a)); 1487 } 1488 s++; 1489 } 1490 a++; 1491 bool new_generator = true; 1492 int x, u, w; 1493 while (a < n && t < nr_cosets_active() - 1) { 1494 if (new_generator) { 1495 w = -1; // -1 is the empty word 1496 if (standardize_deferred(p, q, 0, t, a)) { 1497 out.push_back({a}); 1498 } 1499 x = out.size() - 1; 1500 u = out.size() - 1; 1501 new_generator = false; 1502 } 1503 1504 coset_type const uu = tau(0, out[u].begin(), out[u].end()); 1505 if (uu != UNDEFINED) { 1506 for (int v = 0; v < x; v++) { 1507 coset_type const uuv = tau(uu, out[v].begin(), out[v].end() - 1); 1508 if (uuv != UNDEFINED) { 1509 s = q[uuv]; 1510 if (standardize_deferred(p, q, s, t, out[v].back())) { 1511 word_type nxt = out[u]; 1512 nxt.insert(nxt.end(), out[v].begin(), out[v].end()); 1513 out.push_back(std::move(nxt)); 1514 } 1515 } 1516 } 1517 } 1518 w++; 1519 if (static_cast<size_t>(w) < out.size()) { 1520 coset_type const ww = tau(0, out[w].begin(), out[w].end()); 1521 if (ww != UNDEFINED) { 1522 s = q[ww]; 1523 if (standardize_deferred(p, q, s, t, a)) { 1524 u = out.size(); 1525 word_type nxt = out[w]; 1526 nxt.push_back(a); 1527 out.push_back(std::move(nxt)); 1528 } 1529 } 1530 } else { 1531 a++; 1532 new_generator = true; 1533 } 1534 } 1535 apply_permutation(p, q); 1536 REPORT("%d\n", tmr).prefix().flush_right().flush(); 1537 #ifdef LIBSEMIGROUPS_DEBUG 1538 debug_validate_forwd_bckwd(); 1539 debug_validate_table(); 1540 debug_validate_preimages(); 1541 #endif 1542 } 1543 1544 // The permutation q must map the active cosets to the [0, .. 1545 // , nr_cosets_active()) apply_permutation(std::vector<coset_type> & p,std::vector<coset_type> & q)1546 void ToddCoxeter::apply_permutation(std::vector<coset_type>& p, 1547 std::vector<coset_type>& q) { 1548 // p : new -> old, q = p ^ -1 1549 #ifdef LIBSEMIGROUPS_DEBUG 1550 for (size_t c = 0; c < q.size(); ++c) { 1551 LIBSEMIGROUPS_ASSERT( 1552 (is_active_coset(c) && q[c] < nr_cosets_active()) 1553 || (!is_active_coset(c) && q[c] >= nr_cosets_active())); 1554 LIBSEMIGROUPS_ASSERT(p[q[c]] == c); 1555 LIBSEMIGROUPS_ASSERT(q[p[c]] == c); 1556 } 1557 #endif 1558 { 1559 coset_type c = _id_coset; 1560 size_t const n = nr_generators(); 1561 // Permute all the values in the _table, and pre-images, that relate 1562 // to active cosets 1563 while (c < nr_cosets_active()) { 1564 for (letter_type x = 0; x < n; ++x) { 1565 coset_type i = _table.get(p[c], x); 1566 _table.set(p[c], x, (i == UNDEFINED ? i : q[i])); 1567 i = _preim_init.get(p[c], x); 1568 _preim_init.set(p[c], x, (i == UNDEFINED ? i : q[i])); 1569 i = _preim_next.get(p[c], x); 1570 _preim_next.set(p[c], x, (i == UNDEFINED ? i : q[i])); 1571 } 1572 c++; 1573 } 1574 // Permute the rows themselves 1575 _table.apply_row_permutation(p); 1576 _preim_init.apply_row_permutation(p); 1577 _preim_next.apply_row_permutation(p); 1578 } 1579 { 1580 // Permute the cosets in the CosetManager using p . . . 1581 size_t const n = p.size(); 1582 for (coset_type i = 0; i < n; ++i) { 1583 coset_type current = i; 1584 while (i != p[current]) { 1585 size_t next = p[current]; 1586 switch_cosets(current, next); 1587 p[current] = current; 1588 current = next; 1589 } 1590 p[current] = current; 1591 } 1592 } 1593 } 1594 1595 // Based on the procedure SWITCH in Sims' book, p193 1596 // Swaps an active coset and another coset in the table. swap(coset_type const c,coset_type const d)1597 void ToddCoxeter::swap(coset_type const c, coset_type const d) { 1598 TODD_COXETER_REPORT_SWITCH(c, d) 1599 1600 LIBSEMIGROUPS_ASSERT(_coinc.empty()); 1601 LIBSEMIGROUPS_ASSERT(c != _id_coset); 1602 LIBSEMIGROUPS_ASSERT(d != _id_coset); 1603 LIBSEMIGROUPS_ASSERT(c != d); 1604 LIBSEMIGROUPS_ASSERT(is_valid_coset(c)); 1605 LIBSEMIGROUPS_ASSERT(is_valid_coset(d)); 1606 LIBSEMIGROUPS_ASSERT(is_active_coset(c) || is_active_coset(d)); 1607 1608 size_t const n = nr_generators(); 1609 for (letter_type x = 0; x < n; ++x) { 1610 coset_type cx = _table.get(c, x); 1611 coset_type dx = _table.get(d, x); 1612 1613 if (is_active_coset(c)) { 1614 // Replace c <-- d in the coset table _table 1615 coset_type e = _preim_init.get(c, x); 1616 while (e != UNDEFINED) { 1617 LIBSEMIGROUPS_ASSERT(_table.get(e, x) == c); 1618 _table.set(e, x, d); 1619 e = _preim_next.get(e, x); 1620 } 1621 _table.set(c, x, ff(c, d, cx)); 1622 } 1623 if (is_active_coset(d)) { 1624 // Replace d <-- c in the coset table _table 1625 coset_type e = _preim_init.get(d, x); 1626 while (e != UNDEFINED) { 1627 _table.set(e, x, c); 1628 e = _preim_next.get(e, x); 1629 } 1630 _table.set(d, x, ff(c, d, dx)); 1631 } 1632 if (is_active_coset(c) && is_active_coset(d) && cx == dx 1633 && cx != UNDEFINED) { 1634 // Swap c <--> d in preimages of cx = dx 1635 size_t found = 0; 1636 coset_type e = _preim_init.get(cx, x); 1637 if (e == c) { 1638 _preim_init.set(cx, x, d); 1639 found++; 1640 } else if (e == d) { 1641 _preim_init.set(cx, x, c); 1642 found++; 1643 } 1644 while (e != UNDEFINED && found < 2) { 1645 LIBSEMIGROUPS_ASSERT(ff(c, d, _table.get(e, x)) == cx); 1646 coset_type f = _preim_next.get(e, x); 1647 if (f == c) { 1648 _preim_next.set(e, x, d); 1649 found++; 1650 } else if (f == d) { 1651 _preim_next.set(e, x, c); 1652 found++; 1653 } 1654 e = f; 1655 } 1656 } else { 1657 if (is_active_coset(c) && cx != UNDEFINED) { 1658 // Replace c <-- d in preimages of cx, and d is not a preimage of 1659 // cx under x 1660 coset_type e = _preim_init.get(cx, x); 1661 if (e == c) { 1662 _preim_init.set(cx, x, d); 1663 e = UNDEFINED; // To prevent going into the next loop 1664 } 1665 while (e != UNDEFINED) { 1666 LIBSEMIGROUPS_ASSERT(ff(c, d, _table.get(e, x)) == cx); 1667 coset_type f = _preim_next.get(e, x); 1668 if (f == c) { 1669 _preim_next.set(e, x, d); 1670 break; 1671 } 1672 e = f; 1673 } 1674 } 1675 if (is_active_coset(d) && dx != UNDEFINED) { 1676 // Replace d <-- c in preimages of dx, and c is not a preimage of 1677 // dx under x 1678 coset_type e = _preim_init.get(dx, x); 1679 if (e == d) { 1680 _preim_init.set(dx, x, c); 1681 e = UNDEFINED; // To prevent going into the next loop 1682 } 1683 while (e != UNDEFINED) { 1684 LIBSEMIGROUPS_ASSERT(ff(c, d, _table.get(e, x)) == dx); 1685 coset_type f = _preim_next.get(e, x); 1686 if (f == d) { 1687 _preim_next.set(e, x, c); 1688 break; 1689 } 1690 e = f; 1691 } 1692 } 1693 } 1694 _table.swap(c, x, d, x); 1695 _preim_init.swap(c, x, d, x); 1696 _preim_next.swap(c, x, d, x); 1697 } 1698 switch_cosets(c, d); 1699 } 1700 1701 //////////////////////////////////////////////////////////////////////// 1702 // ToddCoxeter - member functions (debug) - private 1703 //////////////////////////////////////////////////////////////////////// 1704 1705 #ifdef LIBSEMIGROUPS_DEBUG 1706 // Validates the coset table. debug_validate_table() const1707 void ToddCoxeter::debug_validate_table() const { 1708 REPORT_DEBUG_DEFAULT("validating the coset table... "); 1709 size_t const n = nr_generators(); 1710 coset_type c = _id_coset; 1711 while (c != first_free_coset()) { 1712 if (!is_active_coset(c)) { 1713 LIBSEMIGROUPS_EXCEPTION( 1714 "invalid table, coset %d is both free and active!", c); 1715 } 1716 for (letter_type x = 0; x < n; ++x) { 1717 if (_table.get(c, x) != UNDEFINED 1718 && !is_active_coset(_table.get(c, x))) { 1719 LIBSEMIGROUPS_EXCEPTION("invalid table, _table.get(%d, %d) = %d" 1720 " is not an active coset or UNDEFINED!", 1721 c, 1722 x, 1723 _table.get(c, x)); 1724 } 1725 } 1726 c = next_active_coset(c); 1727 } 1728 TODD_COXETER_REPORT_OK(); 1729 } 1730 1731 // Validates the preimages, this is very expensive. debug_validate_preimages() const1732 void ToddCoxeter::debug_validate_preimages() const { 1733 REPORT_DEBUG_DEFAULT("validating preimages... "); 1734 size_t const n = nr_generators(); 1735 coset_type c = _id_coset; 1736 while (c != first_free_coset()) { 1737 for (letter_type x = 0; x < n; ++x) { 1738 coset_type e = _preim_init.get(c, x); 1739 std::set<coset_type> stored_preimages; 1740 while (e != UNDEFINED) { 1741 if (!is_active_coset(e)) { 1742 LIBSEMIGROUPS_EXCEPTION("invalid preimage e = %d of c = %d, e = " 1743 "%d is not an active coset or UNDEFINED!", 1744 e, 1745 c, 1746 e); 1747 } 1748 if (!stored_preimages.insert(e).second) { 1749 LIBSEMIGROUPS_EXCEPTION( 1750 "duplicate preimage e = %d of c = %d under x = %d!", e, c, x); 1751 } 1752 if (_table.get(e, x) != c) { 1753 LIBSEMIGROUPS_EXCEPTION( 1754 "invalid preimage, _table.get(%d, %d) != %d but found e = %d " 1755 "in the preimages of %d under x = %d", 1756 e, 1757 x, 1758 c, 1759 e, 1760 c, 1761 x); 1762 } 1763 e = _preim_next.get(e, x); 1764 } 1765 // Check there are no missing preimages! 1766 coset_type d = 0; 1767 while (d != first_free_coset()) { 1768 if (d != c && _table.get(d, x) == c 1769 && stored_preimages.insert(d).second) { 1770 LIBSEMIGROUPS_EXCEPTION( 1771 "missing preimage, _table.get(%d, %d) == %d but d = %d " 1772 "wasn't found in the stored preimages", 1773 d, 1774 x, 1775 c, 1776 d); 1777 } 1778 d = next_active_coset(d); 1779 } 1780 } 1781 c = next_active_coset(c); 1782 } 1783 TODD_COXETER_REPORT_OK(); 1784 } 1785 debug_verify_no_missing_deductions() const1786 void ToddCoxeter::debug_verify_no_missing_deductions() const { 1787 REPORT_DEBUG_DEFAULT("verifying no missing deductions or " 1788 "coincidences..."); 1789 if (!_deduct.empty()) { 1790 LIBSEMIGROUPS_EXCEPTION("the deduction stack is not empty"); 1791 } 1792 if (!_coinc.empty()) { 1793 LIBSEMIGROUPS_EXCEPTION("the coincidence stack is not empty"); 1794 } 1795 for (coset_type c = _id_coset; c != first_free_coset(); 1796 c = next_active_coset(c)) { 1797 for (auto it = _relations.cbegin(); it < _relations.cend(); it += 2) { 1798 word_type const& u = *it; 1799 word_type const& v = *(it + 1); 1800 LIBSEMIGROUPS_ASSERT(is_valid_coset(c)); 1801 LIBSEMIGROUPS_ASSERT(!u.empty()); 1802 LIBSEMIGROUPS_ASSERT(!v.empty()); 1803 coset_type x = tau(c, u.cbegin(), u.cend() - 1); 1804 if (x == UNDEFINED) { 1805 goto end; 1806 } 1807 LIBSEMIGROUPS_ASSERT(is_valid_coset(x)); 1808 coset_type y = tau(c, v.cbegin(), v.cend() - 1); 1809 if (y == UNDEFINED) { 1810 goto end; 1811 } 1812 LIBSEMIGROUPS_ASSERT(is_valid_coset(y)); 1813 letter_type a = u.back(); 1814 letter_type b = v.back(); 1815 coset_type xx = _table.get(x, a); 1816 coset_type yy = _table.get(y, b); 1817 if (xx == UNDEFINED && yy != UNDEFINED) { 1818 LIBSEMIGROUPS_EXCEPTION("missing deduction tau(%d, %d) = %d when " 1819 "pushing coset %d through %s = %s", 1820 x, 1821 a, 1822 yy, 1823 c, 1824 detail::to_string(u), 1825 detail::to_string(v)); 1826 } else if (xx != UNDEFINED && yy == UNDEFINED) { 1827 // tau(y, b) <- xx 1828 LIBSEMIGROUPS_EXCEPTION("missing deduction tau(%d, %d) = %d when " 1829 "pushing coset %d through %s = %s", 1830 y, 1831 b, 1832 xx, 1833 c, 1834 detail::to_string(u), 1835 detail::to_string(v)); 1836 } else if (xx != UNDEFINED && yy != UNDEFINED) { 1837 // tau(x, a) and tau(y, b) are defined 1838 if (xx != yy) { 1839 LIBSEMIGROUPS_EXCEPTION("missing coincidence %d = %d when " 1840 "pushing coset %d through %s = %s", 1841 xx, 1842 yy, 1843 c, 1844 detail::to_string(u), 1845 detail::to_string(v)); 1846 } 1847 } 1848 } 1849 } 1850 end: 1851 TODD_COXETER_REPORT_OK(); 1852 } 1853 1854 #endif 1855 } // namespace congruence 1856 } // namespace libsemigroups 1857