From: Lachnitt <lachnitt@stanford.edu>
Date: Fri, 3 Dec 2021 23:39:38 +0000 (-0800)
Subject: [proofs] Alethe: Implementation of Process Function (#7745)
X-Git-Tag: cvc5-1.0.0~726
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c2e17604dda0f221a2232daa89ee580da2877315;p=cvc5.git

[proofs] Alethe: Implementation of Process Function (#7745)

Add call to updater and finalizer to process function of the AlethePostProcessor.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
---

diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
index 2254c025f..46ec3f25e 100644
--- a/src/proof/alethe/alethe_post_processor.cpp
+++ b/src/proof/alethe/alethe_post_processor.cpp
@@ -20,6 +20,7 @@
 #include "proof/proof.h"
 #include "proof/proof_checker.h"
 #include "proof/proof_node_algorithm.h"
+#include "proof/proof_node_manager.h"
 #include "theory/builtin/proof_checker.h"
 #include "util/rational.h"
 
@@ -1712,7 +1713,37 @@ AletheProofPostprocess::AletheProofPostprocess(ProofNodeManager* pnm,
 
 AletheProofPostprocess::~AletheProofPostprocess() {}
 
-void AletheProofPostprocess::process(std::shared_ptr<ProofNode> pf) {}
+void AletheProofPostprocess::process(std::shared_ptr<ProofNode> pf) {
+  // Translate proof node
+  ProofNodeUpdater updater(d_pnm, d_cb,true,false);
+  updater.process(pf->getChildren()[0]);
+
+  // In the Alethe proof format the final step has to be (cl). However, after
+  // the translation it might be (cl false). In that case additional steps are
+  // required.
+  // The function has the additional purpose of sanitizing the attributes of the
+  // first SCOPE
+  CDProof cpf(d_pnm, nullptr, "ProofNodeUpdater::CDProof", true);
+  const std::vector<std::shared_ptr<ProofNode>>& cc = pf->getChildren();
+  std::vector<Node> ccn;
+  for (const std::shared_ptr<ProofNode>& cp : cc)
+  {
+    Node cpres = cp->getResult();
+    ccn.push_back(cpres);
+    // store in the proof
+    cpf.addProof(cp);
+  }
+  if (d_cb.finalStep(
+          pf->getResult(), pf->getRule(), ccn, pf->getArguments(), &cpf))
+  {
+    std::shared_ptr<ProofNode> npn = cpf.getProofFor(pf->getResult());
+
+    // then, update the original proof node based on this one
+    Trace("pf-process-debug") << "Update node..." << std::endl;
+    d_pnm->updateNode(pf.get(), npn.get());
+    Trace("pf-process-debug") << "...update node finished." << std::endl;
+  }
+}
 
 }  // namespace proof