From 422e6f9fb08c8fefd3ca9380f2d7ab9aceb7ddaf Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Wed, 25 May 2022 18:27:47 -0300
Subject: [PATCH] [proofs] [alethe] Remove static call to options from
 post-processor (#8817)

---
 src/proof/alethe/alethe_post_processor.cpp | 16 ++++++++--------
 src/proof/alethe/alethe_post_processor.h   |  9 +++++++--
 src/smt/proof_manager.cpp                  |  3 ++-
 3 files changed, 17 insertions(+), 11 deletions(-)

diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
index c1b3805c6..86c2ef115 100644
--- a/src/proof/alethe/alethe_post_processor.cpp
+++ b/src/proof/alethe/alethe_post_processor.cpp
@@ -31,8 +31,8 @@ namespace cvc5::internal {
 namespace proof {
 
 AletheProofPostprocessCallback::AletheProofPostprocessCallback(
-    ProofNodeManager* pnm, AletheNodeConverter& anc)
-    : d_pnm(pnm), d_anc(anc)
+    ProofNodeManager* pnm, AletheNodeConverter& anc, bool resPivots)
+    : d_pnm(pnm), d_anc(anc), d_resPivots(resPivots)
 {
   NodeManager* nm = NodeManager::currentNM();
   d_cl = nm->mkBoundVar("cl", nm->sExprType());
@@ -1512,9 +1512,8 @@ bool AletheProofPostprocessCallback::updatePost(
       }
       std::vector<Node> new_children = children;
       std::vector<Node> new_args =
-          options::proofAletheResPivots()
-              ? args
-              : std::vector<Node>(args.begin(), args.begin() + 3);
+          d_resPivots ? args
+                      : std::vector<Node>(args.begin(), args.begin() + 3);
       Node trueNode = nm->mkConst(true);
       Node falseNode = nm->mkConst(false);
       bool hasUpdated = false;
@@ -1612,7 +1611,7 @@ bool AletheProofPostprocessCallback::updatePost(
           }
         }
       }
-      if (hasUpdated || !options::proofAletheResPivots())
+      if (hasUpdated || !d_resPivots)
       {
         Trace("alethe-proof")
             << "... update alethe step in finalizer " << res << " "
@@ -1821,8 +1820,9 @@ bool AletheProofPostprocessCallback::addAletheStepFromOr(
 }
 
 AletheProofPostprocess::AletheProofPostprocess(ProofNodeManager* pnm,
-                                               AletheNodeConverter& anc)
-    : d_pnm(pnm), d_cb(d_pnm, anc)
+                                               AletheNodeConverter& anc,
+                                               bool resPivots)
+    : d_pnm(pnm), d_cb(d_pnm, anc, resPivots)
 {
 }
 
diff --git a/src/proof/alethe/alethe_post_processor.h b/src/proof/alethe/alethe_post_processor.h
index 8ddf14b2f..620846120 100644
--- a/src/proof/alethe/alethe_post_processor.h
+++ b/src/proof/alethe/alethe_post_processor.h
@@ -32,7 +32,8 @@ class AletheProofPostprocessCallback : public ProofNodeUpdaterCallback
 {
  public:
   AletheProofPostprocessCallback(ProofNodeManager* pnm,
-                                 AletheNodeConverter& anc);
+                                 AletheNodeConverter& anc,
+                                 bool resPivots);
   ~AletheProofPostprocessCallback() {}
   /** Should proof pn be updated? Only if its top-level proof rule is not an
    *  Alethe proof rule.
@@ -91,6 +92,8 @@ class AletheProofPostprocessCallback : public ProofNodeUpdaterCallback
   ProofNodeManager* d_pnm;
   /** The Alethe node converter */
   AletheNodeConverter& d_anc;
+  /** Whether to keep the pivots in the alguments of the resolution rule */
+  bool d_resPivots;
   /** The cl operator
    * For every step the conclusion is a clause. But since the or operator
    *requires at least two arguments it is extended by the cl operator. In case
@@ -145,7 +148,9 @@ class AletheProofPostprocessCallback : public ProofNodeUpdaterCallback
 class AletheProofPostprocess
 {
  public:
-  AletheProofPostprocess(ProofNodeManager* pnm, AletheNodeConverter& anc);
+  AletheProofPostprocess(ProofNodeManager* pnm,
+                         AletheNodeConverter& anc,
+                         bool resPivots);
   ~AletheProofPostprocess();
   /** post-process */
   void process(std::shared_ptr<ProofNode> pf);
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index f400d6d66..19336df5a 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -184,7 +184,8 @@ void PfManager::printProof(std::ostream& out,
   else if (options().proof.proofFormatMode == options::ProofFormatMode::ALETHE)
   {
     proof::AletheNodeConverter anc;
-    proof::AletheProofPostprocess vpfpp(d_pnm.get(), anc);
+    proof::AletheProofPostprocess vpfpp(
+        d_pnm.get(), anc, options().proof.proofAletheResPivots);
     vpfpp.process(fp);
     proof::AletheProofPrinter vpp;
     vpp.print(out, fp);
-- 
2.30.2