Fix proof equality engine for "no-explain" premises (#7079)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 30 Aug 2021 20:44:32 +0000 (15:44 -0500)
committerGitHub <noreply@github.com>
Mon, 30 Aug 2021 20:44:32 +0000 (20:44 +0000)
commit007e93702d91c02954180cd601741aa19bf2a127
tree2d2a02f3a5ab70e590f36256b67f492e50e62596
parentbe403c18c6291e1cf15cdbe46489e65d9323e1b6
Fix proof equality engine for "no-explain" premises (#7079)

There was an inconsistency between when the equality engine would explain a literal and when we would provide a proof for it. This led to rare cases where we over zealously provided a proof for a fact that should have been an assumption in the theory lemma proof.

This corrects the issue by ensuring that no-explain premises are explicitly marked via a new helper proof generator "AssumptionProofGenerator" which always supplies (ASSUME f) as the proof for f.

This corrects some proof checking errors on string benchmarks.
src/CMakeLists.txt
src/proof/assumption_proof_generator.cpp [new file with mode: 0644]
src/proof/assumption_proof_generator.h [new file with mode: 0644]
src/theory/uf/proof_equality_engine.cpp
src/theory/uf/proof_equality_engine.h
test/regress/CMakeLists.txt
test/regress/regress1/strings/instance3303-delta.smt2 [new file with mode: 0644]
test/regress/regress1/strings/instance7075-delta.smt2 [new file with mode: 0644]