From 8e7b2778362ee10f5e4226b30efd1bc16e81bc6e Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Mon, 8 Nov 2021 13:52:59 -0300
Subject: [PATCH] [proofs] Method to convert node representation of Alethe rule
 (#7598)

---
 src/proof/alethe/alethe_proof_rule.cpp | 12 ++++++++++++
 src/proof/alethe/alethe_proof_rule.h   |  7 ++++++-
 2 files changed, 18 insertions(+), 1 deletion(-)

diff --git a/src/proof/alethe/alethe_proof_rule.cpp b/src/proof/alethe/alethe_proof_rule.cpp
index 77d51297a..aa3858969 100644
--- a/src/proof/alethe/alethe_proof_rule.cpp
+++ b/src/proof/alethe/alethe_proof_rule.cpp
@@ -17,6 +17,8 @@
 
 #include <iostream>
 
+#include "proof/proof_checker.h"
+
 namespace cvc5 {
 
 namespace proof {
@@ -127,6 +129,16 @@ std::ostream& operator<<(std::ostream& out, AletheRule id)
   return out;
 }
 
+AletheRule getAletheRule(Node n)
+{
+  uint32_t id;
+  if (ProofRuleChecker::getUInt32(n, id))
+  {
+    return static_cast<AletheRule>(id);
+  }
+  return AletheRule::UNDEFINED;
+}
+
 }  // namespace proof
 
 }  // namespace cvc5
diff --git a/src/proof/alethe/alethe_proof_rule.h b/src/proof/alethe/alethe_proof_rule.h
index 127bb8161..026f69bd4 100644
--- a/src/proof/alethe/alethe_proof_rule.h
+++ b/src/proof/alethe/alethe_proof_rule.h
@@ -18,7 +18,9 @@
 #ifndef CVC4__PROOF__ALETHE_PROOF_RULE_H
 #define CVC4__PROOF__ALETHE_PROOF_RULE_H
 
-#include <memory>
+#include <iostream>
+
+#include "expr/node.h"
 
 namespace cvc5 {
 
@@ -420,6 +422,9 @@ const char* aletheRuleToString(AletheRule id);
  */
 std::ostream& operator<<(std::ostream& out, AletheRule id);
 
+/** Convert a node holding an id to the corresponding AletheRule */
+AletheRule getAletheRule(Node n);
+
 }  // namespace proof
 
 }  // namespace cvc5
-- 
2.30.2