search

vprover / vampire

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

Demodulation redundancy check cannot be turned off #580

Closed mezpusz closed 4 months ago

mezpusz commented 4 months ago

During the latest refactor, I forgot to actually use the flag which checks drc=off.

I wonder what effects this had on our CASC schedules.

quickbeam123 commented 4 months ago

The CASC FOF schedules were using strategies developed with a previous version in which drc=off still worked, but I reevaluated them with the then current vampire, so the schedule construction "knew" drc=off does not matter. These schedules will now be slightly off.

On the other hand, the UEQ strategies were discovered with the buggy vampire and I so if you look, they never try to set drc=off as it is a non-default value and had been observed not to make a difference. So the UEQ strategies will not be affected at all.

mezpusz commented 4 months ago

Provided we think drc=off is still useful, I'm happy.

https://github.com/vprover/vampire/pull/497 Maybe something relevant. I tried to convince Martin that either drc=on or drc=off has to go, but they seem to have a better "coverage" together than encompassment plus one or the other.