1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Hanna Lachnitt |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Implementation of Alethe proof rules |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "proof/alethe/alethe_proof_rule.h" |
17 |
|
|
18 |
|
#include <iostream> |
19 |
|
|
20 |
|
namespace cvc5 { |
21 |
|
|
22 |
|
namespace proof { |
23 |
|
|
24 |
|
const char* aletheRuleToString(AletheRule id) |
25 |
|
{ |
26 |
|
switch (id) |
27 |
|
{ |
28 |
|
case AletheRule::ASSUME: return "assume"; |
29 |
|
case AletheRule::ANCHOR_SUBPROOF: return "subproof"; |
30 |
|
case AletheRule::ANCHOR_BIND: return "bind"; |
31 |
|
case AletheRule::TRUE: return "true"; |
32 |
|
case AletheRule::FALSE: return "false"; |
33 |
|
case AletheRule::NOT_NOT: return "not_not"; |
34 |
|
case AletheRule::AND_POS: return "and_pos"; |
35 |
|
case AletheRule::AND_NEG: return "and_neg"; |
36 |
|
case AletheRule::OR_POS: return "or_pos"; |
37 |
|
case AletheRule::OR_NEG: return "or_neg"; |
38 |
|
case AletheRule::XOR_POS1: return "xor_pos1"; |
39 |
|
case AletheRule::XOR_POS2: return "xor_pos2"; |
40 |
|
case AletheRule::XOR_NEG1: return "xor_neg1"; |
41 |
|
case AletheRule::XOR_NEG2: return "xor_neg2"; |
42 |
|
case AletheRule::IMPLIES_POS: return "implies_pos"; |
43 |
|
case AletheRule::IMPLIES_NEG1: return "implies_neg1"; |
44 |
|
case AletheRule::IMPLIES_NEG2: return "implies_neg2"; |
45 |
|
case AletheRule::EQUIV_POS1: return "equiv_pos1"; |
46 |
|
case AletheRule::EQUIV_POS2: return "equiv_pos2"; |
47 |
|
case AletheRule::EQUIV_NEG1: return "equiv_neg1"; |
48 |
|
case AletheRule::EQUIV_NEG2: return "equiv_neg2"; |
49 |
|
case AletheRule::ITE_POS1: return "ite_pos1"; |
50 |
|
case AletheRule::ITE_POS2: return "ite_pos2"; |
51 |
|
case AletheRule::ITE_NEG1: return "ite_neg1"; |
52 |
|
case AletheRule::ITE_NEG2: return "ite_neg2"; |
53 |
|
case AletheRule::EQ_REFLEXIVE: return "eq_reflexive"; |
54 |
|
case AletheRule::EQ_TRANSITIVE: return "eq_transitive"; |
55 |
|
case AletheRule::EQ_CONGRUENT: return "eq_congruent"; |
56 |
|
case AletheRule::EQ_CONGRUENT_PRED: return "eq_congruent_pred"; |
57 |
|
case AletheRule::DISTINCT_ELIM: return "distinct_elim"; |
58 |
|
case AletheRule::LA_RW_EQ: return "la_rw_eq"; |
59 |
|
case AletheRule::LA_GENERIC: return "la_generic"; |
60 |
|
case AletheRule::LIA_GENERIC: return "lia_generic"; |
61 |
|
case AletheRule::LA_DISEQUALITY: return "la_disequality"; |
62 |
|
case AletheRule::LA_TOTALITY: return "la_totality"; |
63 |
|
case AletheRule::LA_TAUTOLOGY: return "la_tautology"; |
64 |
|
case AletheRule::FORALL_INST: return "forall_inst"; |
65 |
|
case AletheRule::QNT_JOIN: return "qnt_join"; |
66 |
|
case AletheRule::QNT_RM_UNUSED: return "qnt_rm_unused"; |
67 |
|
case AletheRule::TH_RESOLUTION: return "th_resolution"; |
68 |
|
case AletheRule::RESOLUTION: return "resolution"; |
69 |
|
case AletheRule::REFL: return "refl"; |
70 |
|
case AletheRule::TRANS: return "trans"; |
71 |
|
case AletheRule::CONG: return "cong"; |
72 |
|
case AletheRule::AND: return "and"; |
73 |
|
case AletheRule::TAUTOLOGIC_CLAUSE: return "tautologic_clause"; |
74 |
|
case AletheRule::NOT_OR: return "not_or"; |
75 |
|
case AletheRule::OR: return "or"; |
76 |
|
case AletheRule::NOT_AND: return "not_and"; |
77 |
|
case AletheRule::XOR1: return "xor1"; |
78 |
|
case AletheRule::XOR2: return "xor2"; |
79 |
|
case AletheRule::NOT_XOR1: return "not_xor1"; |
80 |
|
case AletheRule::NOT_XOR2: return "not_xor2"; |
81 |
|
case AletheRule::IMPLIES: return "implies"; |
82 |
|
case AletheRule::NOT_IMPLIES1: return "not_implies1"; |
83 |
|
case AletheRule::NOT_IMPLIES2: return "not_implies2"; |
84 |
|
case AletheRule::EQUIV1: return "equiv1"; |
85 |
|
case AletheRule::EQUIV2: return "equiv2"; |
86 |
|
case AletheRule::NOT_EQUIV1: return "not_equiv1"; |
87 |
|
case AletheRule::NOT_EQUIV2: return "not_equiv2"; |
88 |
|
case AletheRule::ITE1: return "ite1"; |
89 |
|
case AletheRule::ITE2: return "ite2"; |
90 |
|
case AletheRule::NOT_ITE1: return "not_ite1"; |
91 |
|
case AletheRule::NOT_ITE2: return "not_ite2"; |
92 |
|
case AletheRule::ITE_INTRO: return "ite_intro"; |
93 |
|
case AletheRule::DUPLICATED_LITERALS: return "duplicate_literals"; |
94 |
|
case AletheRule::CONNECTIVE_DEF: return "connective_def"; |
95 |
|
case AletheRule::ITE_SIMPLIFY: return "ite_simplify"; |
96 |
|
case AletheRule::EQ_SIMPLIFY: return "eq_simplify"; |
97 |
|
case AletheRule::AND_SIMPLIFY: return "and_simplify"; |
98 |
|
case AletheRule::OR_SIMPLIFY: return "or_simplify"; |
99 |
|
case AletheRule::NOT_SIMPLIFY: return "not_simplify"; |
100 |
|
case AletheRule::IMPLIES_SIMPLIFY: return "implies_simplify"; |
101 |
|
case AletheRule::EQUIV_SIMPLIFY: return "equiv_simplify"; |
102 |
|
case AletheRule::BOOL_SIMPLIFY: return "bool_simplify"; |
103 |
|
case AletheRule::QUANTIFIER_SIMPLIFY: return "qnt_simplify"; |
104 |
|
case AletheRule::DIV_SIMPLIFY: return "div_simplify"; |
105 |
|
case AletheRule::PROD_SIMPLIFY: return "prod_simplify"; |
106 |
|
case AletheRule::UNARY_MINUS_SIMPLIFY: return "unary_minus_simplify"; |
107 |
|
case AletheRule::MINUS_SIMPLIFY: return "minus_simplify"; |
108 |
|
case AletheRule::SUM_SIMPLIFY: return "sum_simplify"; |
109 |
|
case AletheRule::COMP_SIMPLIFY: return "comp_simplify"; |
110 |
|
case AletheRule::NARY_ELIM: return "nary_elim"; |
111 |
|
case AletheRule::LET: return "let"; |
112 |
|
case AletheRule::QNT_SIMPLIFY: return "qnt_simplify"; |
113 |
|
case AletheRule::SKO_EX: return "sko_ex"; |
114 |
|
case AletheRule::SKO_FORALL: return "sko_forall"; |
115 |
|
case AletheRule::SYMM: return "symm"; |
116 |
|
case AletheRule::NOT_SYMM: return "not_symm"; |
117 |
|
case AletheRule::REORDER: return "reorder"; |
118 |
|
//================================================= Undefined rule |
119 |
|
case AletheRule::UNDEFINED: return "undefined"; |
120 |
|
default: return "?"; |
121 |
|
} |
122 |
|
} |
123 |
|
|
124 |
|
std::ostream& operator<<(std::ostream& out, AletheRule id) |
125 |
|
{ |
126 |
|
out << aletheRuleToString(id); |
127 |
|
return out; |
128 |
|
} |
129 |
|
|
130 |
|
} // namespace proof |
131 |
|
|
132 |
22746 |
} // namespace cvc5 |