From 9dbe40db8a07ed8d66318d5e6f466fcf294707ce Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Fri, 10 Dec 2021 12:21:28 -0300 Subject: [PATCH] [proofs] Add option to prune inputs from final proof (#7789) This is useful for example to remove inputs corresponding to definition of symbols, which may be unexpected for some users, like when using named to wrap assertions and generate unsat cores. --- src/options/proof_options.toml | 8 ++++++++ src/smt/proof_manager.cpp | 6 ++++-- 2 files changed, 12 insertions(+), 2 deletions(-) diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml index 373e080a1..8eb2fd783 100644 --- a/src/options/proof_options.toml +++ b/src/options/proof_options.toml @@ -99,6 +99,14 @@ name = "Proof" default = "false" help = "add optional annotations to proofs, which enables statistics for inference ids for lemmas and conflicts appearing in final proof" +[[option]] + name = "proofPruneInput" + category = "regular" + long = "proof-prune-input" + type = "bool" + default = "false" + help = "Prune unused input assumptions from final scope" + [[option]] name = "proofAletheResPivots" category = "regular" diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index b8504112d..04f601680 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -151,8 +151,10 @@ void PfManager::setFinalProof(std::shared_ptr pfn, Assertions& as) Trace("smt-proof") << "SolverEngine::setFinalProof(): make scope...\n"; // Now make the final scope, which ensures that the only open leaves of the - // proof are the assertions. - d_finalProof = d_pnm->mkScope(pfn, assertions); + // proof are the assertions. If we are pruning the input, we will try to + // minimize the used assertions. + d_finalProof = + d_pnm->mkScope(pfn, assertions, true, options().proof.proofPruneInput); Trace("smt-proof") << "SolverEngine::setFinalProof(): finished.\n"; } -- 2.30.2