vprover / vampire

The Vampire Theorem Prover
https://vprover.github.io/
Other
282 stars 49 forks source link

Avoid demodulator renormalization #549

Closed mezpusz closed 4 months ago

mezpusz commented 4 months ago

Another small optimization for forward demodulation.

Code trees index terms normalized to increase the number of shared instructions. Hence, the substitution we get from matching is for the normalized term and not the original indexed term, hence we need to renormalize to get a substitution for the original term.

If done during each query, this renormalization can consume up to a third (!) of the runtime in cases when demodulation fails a lot (mainly due to the later ordering checks).

Instead, we can normalize the term to be indexed before indexing it and tell the code tree that no renormalization is needed. I added a new leaf data DemodulatorData where we can cache all kinds of relevant bits for a particular orientation of a demodulator; and I left the code for the original leaf data intact so this shouldn't cause problems for application where code trees are used for different purposes.

There are a couple of discussion points: