search

vprover / vampire

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

Demodulation cosmetics #539

Closed quickbeam123 closed 5 months ago

quickbeam123 commented 5 months ago

1) getDemodulationLHSIterator does not need to be given the options object (we already know at the sites where we use it, whether we are doing FWD or BWD) 2) call SortHelper::getEqualityArgumentSort exactly once in withEqualitySort (and not potentially twice); but don't use on empty iterators

These are almost trivial changes. Just something I noticed before the breakfast...

quickbeam123 commented 5 months ago

Strictly better for discount10:

Sort by SAT
1006 ['problemsSTD_master7392_dis10_i10000.pkl']
1006 ['problemsSTD_mdc7396_dis10_i10000.pkl']

Sort by UNS
7763 ['problemsSTD_master7392_dis10_i10000.pkl']
7766 ['problemsSTD_mdc7396_dis10_i10000.pkl']

Total 1006 / 7766

Greedy cover (UNS):
# problemsSTD_mdc7396_dis10_i10000.pkl contributes 7766 total 7766
Total 7766