vprover / vampire

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

Refactor ordering comparators #599

Closed mezpusz closed 2 months ago

mezpusz commented 2 months ago

This PR fixes some annoying things in OrderingComparator and subclasses:

quickbeam123 commented 2 months ago

TPTP performance (-i 2000) seems OK:

Sort by UNS 7341 ['problemsSTD_master8465_lpo_i2000.pkl'] 7344 ['problemsSTD_marton8471_lpo_i2000.pkl'] 7510 ['problemsSTD_master8465_i2000.pkl'] 7514 ['problemsSTD_marton8471_i2000.pkl']

(Of course, 4 problems are typically less than the variance of the used lrs, but is seems good enough.)

quickbeam123 commented 2 months ago

And here the dpc version of this:

Sort by UNS 7355 ['problemsSTD_master8465_lpo_dpc_i2000.pkl'] 7360 ['problemsSTD_marton8471_lpo_dpc_i2000.pkl'] 7509 ['problemsSTD_master8465_dpc_i2000.pkl'] 7511 ['problemsSTD_marton8471_dpc_i2000.pkl']