[proof-new] Fixing SMT post-processor's handling of assumptions (#6277)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Wed, 7 Apr 2021 21:17:33 +0000 (18:17 -0300)
committerGitHub <noreply@github.com>
Wed, 7 Apr 2021 21:17:33 +0000 (21:17 +0000)
commit8d62f892ddc6ca1b38b3efb2134f12d5678d21ad
tree955f14b7b9f4769ae7363395b5051eb1ad0f04e8
parentc35aad2ce7ffe910200906d7758a41c0cf70dfe5
[proof-new] Fixing SMT post-processor's handling of assumptions (#6277)

Previously the SMT post-processor would update any assumption as long as it
had a proof for it. This can be a problem when one as assumption introduced in a
scope that should not be expanded. This commit fixes the issue by adding the
option of configuring a proof node updater to track scopes and the assumptions
they introduce, which can be used to determine the prood nodes which should be
updated. It also changes the SMT post-processor to only update assumptions that
have not been introduced in some scope.

This commit fixes an issue found by @Lachnitt during the integration of CVC4 and Isabelle.
src/expr/proof_node_updater.cpp
src/expr/proof_node_updater.h
src/options/proof_options.toml
src/prop/proof_post_processor.cpp
src/prop/proof_post_processor.h
src/smt/proof_manager.cpp
src/smt/proof_post_processor.cpp
src/smt/proof_post_processor.h
test/regress/CMakeLists.txt
test/regress/regress0/proofs/scope.smt2 [new file with mode: 0644]