Runtime specialized unidirectional ordering checks for KBO and LPO

[mezpusz]

Implements runtime specialized KBO and LPO mainly to be used by forward demodulation, which is still very hot (in terms of runtime) when we try to demodulate with incomparable equations. A similar idea was published in this paper for KBO. As far as I know this is the first runtime specialized LPO.

The implementation is documented in the code, so I won't go into details here. The idea is that for a demodulator s = t, we precompile the comparison s > t so that when performing a comparison s\theta > t\theta under a substitution \theta, only variable-variable, variable-term or term-variable comparisons need to be performed (plus some simplified weight/variable checks for KBO).

I ran a cross-check using the original comparisons against the new ones with the entire TPTP using Otter and Discount, 20 seconds each, and there wasn't any difference between the two, so we get a fairly high confidence that the runtime specialized versions behave the same as the regular ones.

Note that this implementation is not final, just an initial one for CASC, I would like to iron out potential bottlenecks later. The results are promising, mostly improving for both KBO and LPO, although the latter is more dramatic (as the original LPO implementation is quadratic and we get a bigger boost by shaving off precomputable subcomparisons). But to avoid potential problems in the general option space, let's keep this feature behind a flag for now.

P.S. We could squash the branch commits as they contain some of the recent PRs' content as well.

[quickbeam123]

OK, so this again helps by a measurable bit! (A quick debug mode check under way...)

And let's say I don't want to read the code of the new Comparator classes, being happy that the improvement is hidden behind an option. How much, do you think, will this extension complicate the life of future modificators of the ordering code? Or can we at least say, "If we won't want to maintain this, we can easily disconnect it again."?

[MichaelRawson]

How much, do you think, will this extension complicate the life of future modificators of the ordering code?

I think this would be OK, the optimised version can be replaced with a call to the slower version.

[mezpusz]

How much, do you think, will this extension complicate the life of future modificators of the ordering code? Or can we at least say, "If we won't want to maintain this, we can easily disconnect it again."?

Yes, as @MichaelRawson said, we can just fall back to calling Ordering::compare or Ordering::isGreater directly. My (probably biased) opinion is that the code is not that complicated, so maintaining it wouldn't be a problem either for someone who also maintains KBO and LPO. And as the recent bug indicates, there is the benefit that we have a different implementation to cross-check with!