search

vprover / vampire

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

UPDR incorrect (deletes too much) in the presence of specially parsed function definitions from SMT #561

Closed quickbeam123 closed 3 months ago

quickbeam123 commented 3 months ago

On: 00082minimized.txt we have master with --decode ott+2_1:1_updr=on:foolp=on_2 giving saturation, while with --decode ott+2_1:1_updr=off:foolp=on_2 we find a proof.

@mezpusz is already after this one with https://github.com/vprover/vampire/compare/master...avoid-symbol-elimination-for-smtlib2-defined-symbols so, mostly, this issue tracks that we don't forget.

However, in addition to / instead of marking the relevant symbols as protected, it would be nice for the specially SMT-parsed function definitions to be turned back into normal formulas AT THE BEGINNING of the preprocessing pipeline under -fnrw off while their special treatment later on in the pipeline would only kick in for -fnrw on. Note that it might be necessary to mark both the actually parsed symbol as well as its "proxy" (named with the sFN /sPN prefix).

mezpusz commented 3 months ago

Thanks for creating the issue! I have a question though. So far I thought the udpr=off variant is the correct one, which means we are incomplete rather than unsound?

quickbeam123 commented 3 months ago

You are right. I changed the issue's title.

MichaelRawson commented 3 months ago

Does #564 fix this issue and the duplicate?

mezpusz commented 3 months ago

The problem is fixed on the examples provided in both issues, so I would consider this solved.