From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Mon, 8 Nov 2021 16:52:59 +0000 (-0300)
Subject: [proofs] Method to convert node representation of Alethe rule (#7598)
X-Git-Tag: cvc5-1.0.0~866
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8e7b2778362ee10f5e4226b30efd1bc16e81bc6e;p=cvc5.git

[proofs] Method to convert node representation of Alethe rule (#7598)
---

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