[proof] Added printer for proof rule names (#7185)

Implementation file for Alethe proof rules.

diff --git a/src/proof/alethe/alethe_proof_rule.cpp b/src/proof/alethe/alethe_proof_rule.cpp
new file mode 100644 (file)
index 0000000..77d5129
--- /dev/null
+++ b/src/proof/alethe/alethe_proof_rule.cpp
@@ -0,0 +1,132 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Hanna Lachnitt
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Implementation of Alethe proof rules
+ */
+
+#include "proof/alethe/alethe_proof_rule.h"
+
+#include <iostream>
+
+namespace cvc5 {
+
+namespace proof {
+
+const char* aletheRuleToString(AletheRule id)
+{
+  switch (id)
+  {
+    case AletheRule::ASSUME: return "assume";
+    case AletheRule::ANCHOR_SUBPROOF: return "subproof";
+    case AletheRule::ANCHOR_BIND: return "bind";
+    case AletheRule::TRUE: return "true";
+    case AletheRule::FALSE: return "false";
+    case AletheRule::NOT_NOT: return "not_not";
+    case AletheRule::AND_POS: return "and_pos";
+    case AletheRule::AND_NEG: return "and_neg";
+    case AletheRule::OR_POS: return "or_pos";
+    case AletheRule::OR_NEG: return "or_neg";
+    case AletheRule::XOR_POS1: return "xor_pos1";
+    case AletheRule::XOR_POS2: return "xor_pos2";
+    case AletheRule::XOR_NEG1: return "xor_neg1";
+    case AletheRule::XOR_NEG2: return "xor_neg2";
+    case AletheRule::IMPLIES_POS: return "implies_pos";
+    case AletheRule::IMPLIES_NEG1: return "implies_neg1";
+    case AletheRule::IMPLIES_NEG2: return "implies_neg2";
+    case AletheRule::EQUIV_POS1: return "equiv_pos1";
+    case AletheRule::EQUIV_POS2: return "equiv_pos2";
+    case AletheRule::EQUIV_NEG1: return "equiv_neg1";
+    case AletheRule::EQUIV_NEG2: return "equiv_neg2";
+    case AletheRule::ITE_POS1: return "ite_pos1";
+    case AletheRule::ITE_POS2: return "ite_pos2";
+    case AletheRule::ITE_NEG1: return "ite_neg1";
+    case AletheRule::ITE_NEG2: return "ite_neg2";
+    case AletheRule::EQ_REFLEXIVE: return "eq_reflexive";
+    case AletheRule::EQ_TRANSITIVE: return "eq_transitive";
+    case AletheRule::EQ_CONGRUENT: return "eq_congruent";
+    case AletheRule::EQ_CONGRUENT_PRED: return "eq_congruent_pred";
+    case AletheRule::DISTINCT_ELIM: return "distinct_elim";
+    case AletheRule::LA_RW_EQ: return "la_rw_eq";
+    case AletheRule::LA_GENERIC: return "la_generic";
+    case AletheRule::LIA_GENERIC: return "lia_generic";
+    case AletheRule::LA_DISEQUALITY: return "la_disequality";
+    case AletheRule::LA_TOTALITY: return "la_totality";
+    case AletheRule::LA_TAUTOLOGY: return "la_tautology";
+    case AletheRule::FORALL_INST: return "forall_inst";
+    case AletheRule::QNT_JOIN: return "qnt_join";
+    case AletheRule::QNT_RM_UNUSED: return "qnt_rm_unused";
+    case AletheRule::TH_RESOLUTION: return "th_resolution";
+    case AletheRule::RESOLUTION: return "resolution";
+    case AletheRule::REFL: return "refl";
+    case AletheRule::TRANS: return "trans";
+    case AletheRule::CONG: return "cong";
+    case AletheRule::AND: return "and";
+    case AletheRule::TAUTOLOGIC_CLAUSE: return "tautologic_clause";
+    case AletheRule::NOT_OR: return "not_or";
+    case AletheRule::OR: return "or";
+    case AletheRule::NOT_AND: return "not_and";
+    case AletheRule::XOR1: return "xor1";
+    case AletheRule::XOR2: return "xor2";
+    case AletheRule::NOT_XOR1: return "not_xor1";
+    case AletheRule::NOT_XOR2: return "not_xor2";
+    case AletheRule::IMPLIES: return "implies";
+    case AletheRule::NOT_IMPLIES1: return "not_implies1";
+    case AletheRule::NOT_IMPLIES2: return "not_implies2";
+    case AletheRule::EQUIV1: return "equiv1";
+    case AletheRule::EQUIV2: return "equiv2";
+    case AletheRule::NOT_EQUIV1: return "not_equiv1";
+    case AletheRule::NOT_EQUIV2: return "not_equiv2";
+    case AletheRule::ITE1: return "ite1";
+    case AletheRule::ITE2: return "ite2";
+    case AletheRule::NOT_ITE1: return "not_ite1";
+    case AletheRule::NOT_ITE2: return "not_ite2";
+    case AletheRule::ITE_INTRO: return "ite_intro";
+    case AletheRule::DUPLICATED_LITERALS: return "duplicate_literals";
+    case AletheRule::CONNECTIVE_DEF: return "connective_def";
+    case AletheRule::ITE_SIMPLIFY: return "ite_simplify";
+    case AletheRule::EQ_SIMPLIFY: return "eq_simplify";
+    case AletheRule::AND_SIMPLIFY: return "and_simplify";
+    case AletheRule::OR_SIMPLIFY: return "or_simplify";
+    case AletheRule::NOT_SIMPLIFY: return "not_simplify";
+    case AletheRule::IMPLIES_SIMPLIFY: return "implies_simplify";
+    case AletheRule::EQUIV_SIMPLIFY: return "equiv_simplify";
+    case AletheRule::BOOL_SIMPLIFY: return "bool_simplify";
+    case AletheRule::QUANTIFIER_SIMPLIFY: return "qnt_simplify";
+    case AletheRule::DIV_SIMPLIFY: return "div_simplify";
+    case AletheRule::PROD_SIMPLIFY: return "prod_simplify";
+    case AletheRule::UNARY_MINUS_SIMPLIFY: return "unary_minus_simplify";
+    case AletheRule::MINUS_SIMPLIFY: return "minus_simplify";
+    case AletheRule::SUM_SIMPLIFY: return "sum_simplify";
+    case AletheRule::COMP_SIMPLIFY: return "comp_simplify";
+    case AletheRule::NARY_ELIM: return "nary_elim";
+    case AletheRule::LET: return "let";
+    case AletheRule::QNT_SIMPLIFY: return "qnt_simplify";
+    case AletheRule::SKO_EX: return "sko_ex";
+    case AletheRule::SKO_FORALL: return "sko_forall";
+    case AletheRule::SYMM: return "symm";
+    case AletheRule::NOT_SYMM: return "not_symm";
+    case AletheRule::REORDER: return "reorder";
+    //================================================= Undefined rule
+    case AletheRule::UNDEFINED: return "undefined";
+    default: return "?";
+  }
+}
+
+std::ostream& operator<<(std::ostream& out, AletheRule id)
+{
+  out << aletheRuleToString(id);
+  return out;
+}
+
+}  // namespace proof
+
+}  // namespace cvc5