search

vprover / vampire

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

Fix conditional redundancy handler literal constraints with encompassment demodulation incompleteness issue #600

Closed mezpusz closed 2 months ago

mezpusz commented 2 months ago

We assume in DemodulationHelper that the rewriting clause is unit, which resulted in false redundancies inside ConditionalRedundancyHandler where this assumption is not true with crlc=on.

Instead of overcomplicating original code and potentially slowing down demodulation, I duplicated the relevant part in ConditionalRedundancyHandler.

Tests indicate no further incompleteness so far, efficiency is comparable to previous version.