From: Lachnitt Date: Wed, 15 Sep 2021 14:01:33 +0000 (-0700) Subject: [proof] Added printer for proof rule names (#7185) X-Git-Tag: cvc5-1.0.0~1208 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=399c2b4fd86962a3cfb63be09d79855346d0d610;p=cvc5.git [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 index 000000000..77d51297a --- /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 + +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