[proofs] [alethe] Remove static call to options from post-processor (#8817)

diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
index c1b3805c6aebfad7ded05a94772e74aa181a47e0..86c2ef11575d4275ce937139a7023e7a4f8991aa 100644 (file)
--- 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 8ddf14b2f0bb45d655cb2bbcb29e897361cad258..62084612055826162c2c99b72bd727494cab3432 100644 (file)
--- 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 f400d6d6653aec989b3a489662601d113999fea2..19336df5aa385d0646112620264565ccaa4620f5 100644 (file)
--- 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);