[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.

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
@@ -100,6 +100,14 @@ name   = "Proof"
   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"
   long       = "proof-alethe-res-pivots"
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<ProofNode> 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";
 }