[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 77d51297ad2594f451cd5248d0c77d7cb218ef30..aa3858969b09a0e58356b30ee3eb35b8f22aba37 100644 (file)
--- 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 127bb8161355c24b31d716b9e3ff57c599617190..026f69bd4e55d0447bd293cc4a0537e2c58b0f26 100644 (file)
--- 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