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

diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml
index 373e080a1e720e377e6d8fa009aa978e56b5416e..8eb2fd783e613f3f82602c61ad3f05df339ef5d7 100644 (file)
--- 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 b8504112db346f4b2d216699218b80fe83a3a5b4..04f6016808556b1e9ce5e06cff8a265173e091e0 100644 (file)
--- 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";
 }