(proof-new) Fixes and improvements for smt proof postprocessor (#5197)

This includes several subtle issues encountered in the past month based on our regressions.

It also improves the expansion forms of MACRO_ rules to use EQ_RESOLVE instead of a TRUE_INTRO/TRUE_ELIM scheme. This is both more compact and avoids cyclic proofs for some corner cases of proofs with Boolean constant equalites.

1 files changed, 12 insertions, 3 deletions

diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h
index b65519c6d..d7186ea74 100644
--- a/src/smt/proof_post_processor.h
+++ b/src/smt/proof_post_processor.h
@@ -198,14 +198,23 @@ class ProofPostproccess
   void process(std::shared_ptr<ProofNode> pf);
   /** set eliminate rule */
   void setEliminateRule(PfRule rule);
-
  private:
+  /** The proof node manager */
+  ProofNodeManager* d_pnm;
   /** The post process callback */
   ProofPostprocessCallback d_cb;
+  /**
+   * The updater, which is responsible for expanding macros in the final proof
+   * and connecting preprocessed assumptions to input assumptions.
+   */
+  ProofNodeUpdater d_updater;
   /** The post process callback for finalization */
   ProofPostprocessFinalCallback d_finalCb;
-  /** The proof node manager */
-  ProofNodeManager* d_pnm;
+  /**
+   * The finalizer, which is responsible for taking stats and checking for
+   * (lazy) pedantic failures.
+   */
+  ProofNodeUpdater d_finalizer;
 };
 
 }  // namespace smt