Improve knuth bendix 2 squash

[Joseph-Edwards]

This PR makes sort_pending_rules a function template that accepts arbitrary orderings. When the pending rules are sorted with respect to the reduction order of the rewriting system, bad test case [932] now completes in about 20 seconds on my machine. Further changes that prevent the use of a new rule trie speed this up even further, but I didn't want to commit those changes.

It is worth noting that, presently, this makes some of the other tests fail. The failures seem to be related to active rules having their letters permuted. Some of the quick tests are also slower with this change. As a result, I'm not sure whether this PR should actually be merged, but it's good for experimentation.

[james-d-mitchell]

This PR makes sort_pending_rules a function template that accepts arbitrary orderings. When the pending rules are sorted with respect to the reduction order of the rewriting system, bad test case [932] now completes in about 20 seconds on my machine. Further changes that prevent the use of a new rule trie speed this up even further, but I didn't want to commit those changes.

It is worth noting that, presently, this makes some of the other tests fail. The failures seem to be related to active rules having their letters permuted. Some of the quick tests are also slower with this change. As a result, I'm not sure whether this PR should actually be merged, but it's good for experimentation.

When you say "letters permuted" do you mean "rules permuted" o/w this ought not to be possible.

[Joseph-Edwards]

When you say "letters permuted" do you mean "rules permuted" o/w this ought not to be possible.
Things like this:

  { {  }, { 1 }, { 1, 0 }, { 0 }, { 0, 1 } }
  ==
  { {  }, { 0 }, { 0, 1 }, { 1 }, { 1, 0 } }

I suppose that's also rules permuted.