From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 15 Dec 2021 15:15:26 +0000 (-0600)
Subject: Add trace to see inferences in final proof (#7813)
X-Git-Tag: cvc5-1.0.0~661
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5c82e1dd02c304dd34c72ffcc966840e8b3005ff;p=cvc5.git

Add trace to see inferences in final proof (#7813)

Adds -t im-pf to see which inferences occur in the final proof. Must be used with proofs and --proof-annotate.
---

diff --git a/src/smt/proof_final_callback.cpp b/src/smt/proof_final_callback.cpp
index 484f0dd73..4cf3a68f7 100644
--- a/src/smt/proof_final_callback.cpp
+++ b/src/smt/proof_final_callback.cpp
@@ -109,6 +109,12 @@ bool ProofFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
       if (getInferenceId(args[0], id))
       {
         d_annotationRuleIds << id;
+        // Use e.g. `--check-proofs --proof-annotate -t im-pf` to see a list of
+        // inference that appear in the final proof.
+        Trace("im-pf") << "(inference-pf " << id << " " << pn->getResult()
+                       << ")" << std::endl;
+        Trace("im-pf-assert")
+            << "(assert " << pn->getResult() << ") ; " << id << std::endl;
       }
     }
   }