1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Haniel Barbosa, Gereon Kremer |
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 proof rule. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "proof/proof_rule.h" |
17 |
|
|
18 |
|
#include <iostream> |
19 |
|
|
20 |
|
namespace cvc5 { |
21 |
|
|
22 |
192050 |
const char* toString(PfRule id) |
23 |
|
{ |
24 |
192050 |
switch (id) |
25 |
|
{ |
26 |
|
//================================================= Core rules |
27 |
42409 |
case PfRule::ASSUME: return "ASSUME"; |
28 |
42409 |
case PfRule::SCOPE: return "SCOPE"; |
29 |
|
case PfRule::SUBS: return "SUBS"; |
30 |
|
case PfRule::REWRITE: return "REWRITE"; |
31 |
4 |
case PfRule::EVALUATE: return "EVALUATE"; |
32 |
|
case PfRule::MACRO_SR_EQ_INTRO: return "MACRO_SR_EQ_INTRO"; |
33 |
|
case PfRule::MACRO_SR_PRED_INTRO: return "MACRO_SR_PRED_INTRO"; |
34 |
|
case PfRule::MACRO_SR_PRED_ELIM: return "MACRO_SR_PRED_ELIM"; |
35 |
42402 |
case PfRule::MACRO_SR_PRED_TRANSFORM: return "MACRO_SR_PRED_TRANSFORM"; |
36 |
|
case PfRule::REMOVE_TERM_FORMULA_AXIOM: return "REMOVE_TERM_FORMULA_AXIOM"; |
37 |
|
//================================================= Trusted rules |
38 |
|
case PfRule::THEORY_LEMMA: return "THEORY_LEMMA"; |
39 |
5 |
case PfRule::THEORY_REWRITE: return "THEORY_REWRITE"; |
40 |
|
case PfRule::PREPROCESS: return "PREPROCESS"; |
41 |
|
case PfRule::PREPROCESS_LEMMA: return "PREPROCESS_LEMMA"; |
42 |
|
case PfRule::THEORY_PREPROCESS: return "THEORY_PREPROCESS"; |
43 |
|
case PfRule::THEORY_PREPROCESS_LEMMA: return "THEORY_PREPROCESS_LEMMA"; |
44 |
|
case PfRule::THEORY_EXPAND_DEF: return "THEORY_EXPAND_DEF"; |
45 |
|
case PfRule::WITNESS_AXIOM: return "WITNESS_AXIOM"; |
46 |
|
case PfRule::TRUST_REWRITE: return "TRUST_REWRITE"; |
47 |
|
case PfRule::TRUST_SUBS: return "TRUST_SUBS"; |
48 |
|
case PfRule::TRUST_SUBS_MAP: return "TRUST_SUBS_MAP"; |
49 |
|
case PfRule::TRUST_SUBS_EQ: return "TRUST_SUBS_EQ"; |
50 |
|
case PfRule::THEORY_INFERENCE: return "THEORY_INFERENCE"; |
51 |
|
case PfRule::SAT_REFUTATION: return "SAT_REFUTATION"; |
52 |
|
//================================================= Boolean rules |
53 |
|
case PfRule::RESOLUTION: return "RESOLUTION"; |
54 |
5 |
case PfRule::CHAIN_RESOLUTION: return "CHAIN_RESOLUTION"; |
55 |
|
case PfRule::FACTORING: return "FACTORING"; |
56 |
1 |
case PfRule::REORDERING: return "REORDERING"; |
57 |
|
case PfRule::MACRO_RESOLUTION: return "MACRO_RESOLUTION"; |
58 |
|
case PfRule::MACRO_RESOLUTION_TRUST: return "MACRO_RESOLUTION_TRUST"; |
59 |
|
case PfRule::SPLIT: return "SPLIT"; |
60 |
5 |
case PfRule::EQ_RESOLVE: return "EQ_RESOLVE"; |
61 |
4 |
case PfRule::MODUS_PONENS: return "MODUS_PONENS"; |
62 |
|
case PfRule::NOT_NOT_ELIM: return "NOT_NOT_ELIM"; |
63 |
4 |
case PfRule::CONTRA: return "CONTRA"; |
64 |
|
case PfRule::AND_ELIM: return "AND_ELIM"; |
65 |
5 |
case PfRule::AND_INTRO: return "AND_INTRO"; |
66 |
|
case PfRule::NOT_OR_ELIM: return "NOT_OR_ELIM"; |
67 |
|
case PfRule::IMPLIES_ELIM: return "IMPLIES_ELIM"; |
68 |
|
case PfRule::NOT_IMPLIES_ELIM1: return "NOT_IMPLIES_ELIM1"; |
69 |
|
case PfRule::NOT_IMPLIES_ELIM2: return "NOT_IMPLIES_ELIM2"; |
70 |
|
case PfRule::EQUIV_ELIM1: return "EQUIV_ELIM1"; |
71 |
|
case PfRule::EQUIV_ELIM2: return "EQUIV_ELIM2"; |
72 |
|
case PfRule::NOT_EQUIV_ELIM1: return "NOT_EQUIV_ELIM1"; |
73 |
|
case PfRule::NOT_EQUIV_ELIM2: return "NOT_EQUIV_ELIM2"; |
74 |
|
case PfRule::XOR_ELIM1: return "XOR_ELIM1"; |
75 |
|
case PfRule::XOR_ELIM2: return "XOR_ELIM2"; |
76 |
|
case PfRule::NOT_XOR_ELIM1: return "NOT_XOR_ELIM1"; |
77 |
|
case PfRule::NOT_XOR_ELIM2: return "NOT_XOR_ELIM2"; |
78 |
|
case PfRule::ITE_ELIM1: return "ITE_ELIM1"; |
79 |
|
case PfRule::ITE_ELIM2: return "ITE_ELIM2"; |
80 |
|
case PfRule::NOT_ITE_ELIM1: return "NOT_ITE_ELIM1"; |
81 |
|
case PfRule::NOT_ITE_ELIM2: return "NOT_ITE_ELIM2"; |
82 |
5 |
case PfRule::NOT_AND: return "NOT_AND"; |
83 |
|
//================================================= CNF rules |
84 |
|
case PfRule::CNF_AND_POS: return "CNF_AND_POS"; |
85 |
|
case PfRule::CNF_AND_NEG: return "CNF_AND_NEG"; |
86 |
|
case PfRule::CNF_OR_POS: return "CNF_OR_POS"; |
87 |
|
case PfRule::CNF_OR_NEG: return "CNF_OR_NEG"; |
88 |
|
case PfRule::CNF_IMPLIES_POS: return "CNF_IMPLIES_POS"; |
89 |
|
case PfRule::CNF_IMPLIES_NEG1: return "CNF_IMPLIES_NEG1"; |
90 |
|
case PfRule::CNF_IMPLIES_NEG2: return "CNF_IMPLIES_NEG2"; |
91 |
|
case PfRule::CNF_EQUIV_POS1: return "CNF_EQUIV_POS1"; |
92 |
|
case PfRule::CNF_EQUIV_POS2: return "CNF_EQUIV_POS2"; |
93 |
|
case PfRule::CNF_EQUIV_NEG1: return "CNF_EQUIV_NEG1"; |
94 |
|
case PfRule::CNF_EQUIV_NEG2: return "CNF_EQUIV_NEG2"; |
95 |
|
case PfRule::CNF_XOR_POS1: return "CNF_XOR_POS1"; |
96 |
|
case PfRule::CNF_XOR_POS2: return "CNF_XOR_POS2"; |
97 |
|
case PfRule::CNF_XOR_NEG1: return "CNF_XOR_NEG1"; |
98 |
|
case PfRule::CNF_XOR_NEG2: return "CNF_XOR_NEG2"; |
99 |
|
case PfRule::CNF_ITE_POS1: return "CNF_ITE_POS1"; |
100 |
|
case PfRule::CNF_ITE_POS2: return "CNF_ITE_POS2"; |
101 |
|
case PfRule::CNF_ITE_POS3: return "CNF_ITE_POS3"; |
102 |
|
case PfRule::CNF_ITE_NEG1: return "CNF_ITE_NEG1"; |
103 |
|
case PfRule::CNF_ITE_NEG2: return "CNF_ITE_NEG2"; |
104 |
|
case PfRule::CNF_ITE_NEG3: return "CNF_ITE_NEG3"; |
105 |
|
//================================================= Equality rules |
106 |
13 |
case PfRule::REFL: return "REFL"; |
107 |
24 |
case PfRule::SYMM: return "SYMM"; |
108 |
24 |
case PfRule::TRANS: return "TRANS"; |
109 |
24 |
case PfRule::CONG: return "CONG"; |
110 |
20 |
case PfRule::TRUE_INTRO: return "TRUE_INTRO"; |
111 |
5 |
case PfRule::TRUE_ELIM: return "TRUE_ELIM"; |
112 |
20 |
case PfRule::FALSE_INTRO: return "FALSE_INTRO"; |
113 |
19 |
case PfRule::FALSE_ELIM: return "FALSE_ELIM"; |
114 |
|
case PfRule::HO_APP_ENCODE: return "HO_APP_ENCODE"; |
115 |
|
case PfRule::HO_CONG: return "HO_CONG"; |
116 |
|
//================================================= Array rules |
117 |
|
case PfRule::ARRAYS_READ_OVER_WRITE: return "ARRAYS_READ_OVER_WRITE"; |
118 |
|
case PfRule::ARRAYS_READ_OVER_WRITE_CONTRA: |
119 |
|
return "ARRAYS_READ_OVER_WRITE_CONTRA"; |
120 |
|
case PfRule::ARRAYS_READ_OVER_WRITE_1: return "ARRAYS_READ_OVER_WRITE_1"; |
121 |
|
case PfRule::ARRAYS_EXT: return "ARRAYS_EXT"; |
122 |
|
case PfRule::ARRAYS_EQ_RANGE_EXPAND: return "ARRAYS_EQ_RANGE_EXPAND"; |
123 |
|
//================================================= Bit-Vector rules |
124 |
|
case PfRule::BV_BITBLAST: return "BV_BITBLAST"; |
125 |
|
case PfRule::BV_BITBLAST_STEP: return "BV_BITBLAST_STEP"; |
126 |
|
case PfRule::BV_EAGER_ATOM: return "BV_EAGER_ATOM"; |
127 |
|
//================================================= Datatype rules |
128 |
|
case PfRule::DT_UNIF: return "DT_UNIF"; |
129 |
|
case PfRule::DT_INST: return "DT_INST"; |
130 |
|
case PfRule::DT_COLLAPSE: return "DT_COLLAPSE"; |
131 |
|
case PfRule::DT_SPLIT: return "DT_SPLIT"; |
132 |
|
case PfRule::DT_CLASH: return "DT_CLASH"; |
133 |
|
//================================================= Quantifiers rules |
134 |
|
case PfRule::SKOLEM_INTRO: return "SKOLEM_INTRO"; |
135 |
|
case PfRule::EXISTS_INTRO: return "EXISTS_INTRO"; |
136 |
|
case PfRule::SKOLEMIZE: return "SKOLEMIZE"; |
137 |
|
case PfRule::INSTANTIATE: return "INSTANTIATE"; |
138 |
|
case PfRule::QUANTIFIERS_PREPROCESS: return "QUANTIFIERS_PREPROCESS"; |
139 |
|
//================================================= String rules |
140 |
|
case PfRule::CONCAT_EQ: return "CONCAT_EQ"; |
141 |
|
case PfRule::CONCAT_UNIFY: return "CONCAT_UNIFY"; |
142 |
|
case PfRule::CONCAT_CONFLICT: return "CONCAT_CONFLICT"; |
143 |
|
case PfRule::CONCAT_SPLIT: return "CONCAT_SPLIT"; |
144 |
|
case PfRule::CONCAT_CSPLIT: return "CONCAT_CSPLIT"; |
145 |
|
case PfRule::CONCAT_LPROP: return "CONCAT_LPROP"; |
146 |
|
case PfRule::CONCAT_CPROP: return "CONCAT_CPROP"; |
147 |
|
case PfRule::STRING_DECOMPOSE: return "STRING_DECOMPOSE"; |
148 |
|
case PfRule::STRING_LENGTH_POS: return "STRING_LENGTH_POS"; |
149 |
|
case PfRule::STRING_LENGTH_NON_EMPTY: return "STRING_LENGTH_NON_EMPTY"; |
150 |
|
case PfRule::STRING_REDUCTION: return "STRING_REDUCTION"; |
151 |
|
case PfRule::STRING_EAGER_REDUCTION: return "STRING_EAGER_REDUCTION"; |
152 |
|
case PfRule::RE_INTER: return "RE_INTER"; |
153 |
|
case PfRule::RE_UNFOLD_POS: return "RE_UNFOLD_POS"; |
154 |
|
case PfRule::RE_UNFOLD_NEG: return "RE_UNFOLD_NEG"; |
155 |
|
case PfRule::RE_UNFOLD_NEG_CONCAT_FIXED: |
156 |
|
return "RE_UNFOLD_NEG_CONCAT_FIXED"; |
157 |
|
case PfRule::RE_ELIM: return "RE_ELIM"; |
158 |
|
case PfRule::STRING_CODE_INJ: return "STRING_CODE_INJ"; |
159 |
|
case PfRule::STRING_SEQ_UNIT_INJ: return "STRING_SEQ_UNIT_INJ"; |
160 |
|
case PfRule::STRING_INFERENCE: return "STRING_INFERENCE"; |
161 |
|
//================================================= Arith rules |
162 |
42402 |
case PfRule::MACRO_ARITH_SCALE_SUM_UB: |
163 |
42402 |
return "ARITH_SCALE_SUM_UPPER_BOUNDS"; |
164 |
4 |
case PfRule::ARITH_SUM_UB: return "ARITH_SUM_UB"; |
165 |
3179 |
case PfRule::ARITH_TRICHOTOMY: return "ARITH_TRICHOTOMY"; |
166 |
407 |
case PfRule::INT_TIGHT_LB: return "INT_TIGHT_LB"; |
167 |
18643 |
case PfRule::INT_TIGHT_UB: return "INT_TIGHT_UB"; |
168 |
|
case PfRule::ARITH_MULT_SIGN: return "ARITH_MULT_SIGN"; |
169 |
4 |
case PfRule::ARITH_MULT_POS: return "ARITH_MULT_POS"; |
170 |
4 |
case PfRule::ARITH_MULT_NEG: return "ARITH_MULT_NEG"; |
171 |
|
case PfRule::ARITH_MULT_TANGENT: return "ARITH_MULT_TANGENT"; |
172 |
|
case PfRule::ARITH_OP_ELIM_AXIOM: return "ARITH_OP_ELIM_AXIOM"; |
173 |
|
case PfRule::ARITH_TRANS_PI: return "ARITH_TRANS_PI"; |
174 |
|
case PfRule::ARITH_TRANS_EXP_NEG: return "ARITH_TRANS_EXP_NEG"; |
175 |
|
case PfRule::ARITH_TRANS_EXP_POSITIVITY: |
176 |
|
return "ARITH_TRANS_EXP_POSITIVITY"; |
177 |
|
case PfRule::ARITH_TRANS_EXP_SUPER_LIN: return "ARITH_TRANS_EXP_SUPER_LIN"; |
178 |
|
case PfRule::ARITH_TRANS_EXP_ZERO: return "ARITH_TRANS_EXP_ZERO"; |
179 |
|
case PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_NEG: |
180 |
|
return "ARITH_TRANS_EXP_APPROX_ABOVE_NEG"; |
181 |
|
case PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_POS: |
182 |
|
return "ARITH_TRANS_EXP_APPROX_ABOVE_POS"; |
183 |
|
case PfRule::ARITH_TRANS_EXP_APPROX_BELOW: |
184 |
|
return "ARITH_TRANS_EXP_APPROX_BELOW"; |
185 |
|
case PfRule::ARITH_TRANS_SINE_BOUNDS: return "ARITH_TRANS_SINE_BOUNDS"; |
186 |
|
case PfRule::ARITH_TRANS_SINE_SHIFT: return "ARITH_TRANS_SINE_SHIFT"; |
187 |
|
case PfRule::ARITH_TRANS_SINE_SYMMETRY: return "ARITH_TRANS_SINE_SYMMETRY"; |
188 |
|
case PfRule::ARITH_TRANS_SINE_TANGENT_ZERO: |
189 |
|
return "ARITH_TRANS_SINE_TANGENT_ZERO"; |
190 |
|
case PfRule::ARITH_TRANS_SINE_TANGENT_PI: |
191 |
|
return "ARITH_TRANS_SINE_TANGENT_PI"; |
192 |
|
case PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_NEG: |
193 |
|
return "ARITH_TRANS_SINE_APPROX_ABOVE_NEG"; |
194 |
|
case PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_POS: |
195 |
|
return "ARITH_TRANS_SINE_APPROX_ABOVE_POS"; |
196 |
|
case PfRule::ARITH_TRANS_SINE_APPROX_BELOW_NEG: |
197 |
|
return "ARITH_TRANS_SINE_APPROX_BELOW_NEG"; |
198 |
|
case PfRule::ARITH_TRANS_SINE_APPROX_BELOW_POS: |
199 |
|
return "ARITH_TRANS_SINE_APPROX_BELOW_POS"; |
200 |
|
case PfRule::ARITH_NL_CAD_DIRECT: return "ARITH_NL_CAD_DIRECT"; |
201 |
|
case PfRule::ARITH_NL_CAD_RECURSIVE: return "ARITH_NL_CAD_RECURSIVE"; |
202 |
|
//================================================= External rules |
203 |
|
case PfRule::LFSC_RULE: return "LFSC_RULE"; |
204 |
|
//================================================= Unknown rule |
205 |
|
case PfRule::UNKNOWN: return "UNKNOWN"; |
206 |
|
default: return "?"; |
207 |
|
} |
208 |
|
} |
209 |
|
|
210 |
192050 |
std::ostream& operator<<(std::ostream& out, PfRule id) |
211 |
|
{ |
212 |
192050 |
out << toString(id); |
213 |
192050 |
return out; |
214 |
|
} |
215 |
|
|
216 |
2767918 |
size_t PfRuleHashFunction::operator()(PfRule id) const |
217 |
|
{ |
218 |
2767918 |
return static_cast<size_t>(id); |
219 |
|
} |
220 |
|
|
221 |
29502 |
} // namespace cvc5 |