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 "expr/proof_rule.h" |
17 |
|
|
18 |
|
#include <iostream> |
19 |
|
|
20 |
|
namespace cvc5 { |
21 |
|
|
22 |
148490 |
const char* toString(PfRule id) |
23 |
|
{ |
24 |
148490 |
switch (id) |
25 |
|
{ |
26 |
|
//================================================= Core rules |
27 |
32826 |
case PfRule::ASSUME: return "ASSUME"; |
28 |
32826 |
case PfRule::SCOPE: return "SCOPE"; |
29 |
|
case PfRule::SUBS: return "SUBS"; |
30 |
|
case PfRule::REWRITE: return "REWRITE"; |
31 |
|
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 |
32823 |
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 |
1 |
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 |
|
//================================================= Boolean rules |
50 |
|
case PfRule::RESOLUTION: return "RESOLUTION"; |
51 |
1 |
case PfRule::CHAIN_RESOLUTION: return "CHAIN_RESOLUTION"; |
52 |
|
case PfRule::FACTORING: return "FACTORING"; |
53 |
1 |
case PfRule::REORDERING: return "REORDERING"; |
54 |
|
case PfRule::MACRO_RESOLUTION: return "MACRO_RESOLUTION"; |
55 |
|
case PfRule::SPLIT: return "SPLIT"; |
56 |
1 |
case PfRule::EQ_RESOLVE: return "EQ_RESOLVE"; |
57 |
|
case PfRule::MODUS_PONENS: return "MODUS_PONENS"; |
58 |
|
case PfRule::NOT_NOT_ELIM: return "NOT_NOT_ELIM"; |
59 |
|
case PfRule::CONTRA: return "CONTRA"; |
60 |
|
case PfRule::AND_ELIM: return "AND_ELIM"; |
61 |
1 |
case PfRule::AND_INTRO: return "AND_INTRO"; |
62 |
|
case PfRule::NOT_OR_ELIM: return "NOT_OR_ELIM"; |
63 |
|
case PfRule::IMPLIES_ELIM: return "IMPLIES_ELIM"; |
64 |
|
case PfRule::NOT_IMPLIES_ELIM1: return "NOT_IMPLIES_ELIM1"; |
65 |
|
case PfRule::NOT_IMPLIES_ELIM2: return "NOT_IMPLIES_ELIM2"; |
66 |
|
case PfRule::EQUIV_ELIM1: return "EQUIV_ELIM1"; |
67 |
|
case PfRule::EQUIV_ELIM2: return "EQUIV_ELIM2"; |
68 |
|
case PfRule::NOT_EQUIV_ELIM1: return "NOT_EQUIV_ELIM1"; |
69 |
|
case PfRule::NOT_EQUIV_ELIM2: return "NOT_EQUIV_ELIM2"; |
70 |
|
case PfRule::XOR_ELIM1: return "XOR_ELIM1"; |
71 |
|
case PfRule::XOR_ELIM2: return "XOR_ELIM2"; |
72 |
|
case PfRule::NOT_XOR_ELIM1: return "NOT_XOR_ELIM1"; |
73 |
|
case PfRule::NOT_XOR_ELIM2: return "NOT_XOR_ELIM2"; |
74 |
|
case PfRule::ITE_ELIM1: return "ITE_ELIM1"; |
75 |
|
case PfRule::ITE_ELIM2: return "ITE_ELIM2"; |
76 |
|
case PfRule::NOT_ITE_ELIM1: return "NOT_ITE_ELIM1"; |
77 |
|
case PfRule::NOT_ITE_ELIM2: return "NOT_ITE_ELIM2"; |
78 |
|
//================================================= De Morgan rules |
79 |
1 |
case PfRule::NOT_AND: return "NOT_AND"; |
80 |
|
//================================================= CNF rules |
81 |
|
case PfRule::CNF_AND_POS: return "CNF_AND_POS"; |
82 |
|
case PfRule::CNF_AND_NEG: return "CNF_AND_NEG"; |
83 |
|
case PfRule::CNF_OR_POS: return "CNF_OR_POS"; |
84 |
|
case PfRule::CNF_OR_NEG: return "CNF_OR_NEG"; |
85 |
|
case PfRule::CNF_IMPLIES_POS: return "CNF_IMPLIES_POS"; |
86 |
|
case PfRule::CNF_IMPLIES_NEG1: return "CNF_IMPLIES_NEG1"; |
87 |
|
case PfRule::CNF_IMPLIES_NEG2: return "CNF_IMPLIES_NEG2"; |
88 |
|
case PfRule::CNF_EQUIV_POS1: return "CNF_EQUIV_POS1"; |
89 |
|
case PfRule::CNF_EQUIV_POS2: return "CNF_EQUIV_POS2"; |
90 |
|
case PfRule::CNF_EQUIV_NEG1: return "CNF_EQUIV_NEG1"; |
91 |
|
case PfRule::CNF_EQUIV_NEG2: return "CNF_EQUIV_NEG2"; |
92 |
|
case PfRule::CNF_XOR_POS1: return "CNF_XOR_POS1"; |
93 |
|
case PfRule::CNF_XOR_POS2: return "CNF_XOR_POS2"; |
94 |
|
case PfRule::CNF_XOR_NEG1: return "CNF_XOR_NEG1"; |
95 |
|
case PfRule::CNF_XOR_NEG2: return "CNF_XOR_NEG2"; |
96 |
|
case PfRule::CNF_ITE_POS1: return "CNF_ITE_POS1"; |
97 |
|
case PfRule::CNF_ITE_POS2: return "CNF_ITE_POS2"; |
98 |
|
case PfRule::CNF_ITE_POS3: return "CNF_ITE_POS3"; |
99 |
|
case PfRule::CNF_ITE_NEG1: return "CNF_ITE_NEG1"; |
100 |
|
case PfRule::CNF_ITE_NEG2: return "CNF_ITE_NEG2"; |
101 |
|
case PfRule::CNF_ITE_NEG3: return "CNF_ITE_NEG3"; |
102 |
|
//================================================= Equality rules |
103 |
4 |
case PfRule::REFL: return "REFL"; |
104 |
5 |
case PfRule::SYMM: return "SYMM"; |
105 |
5 |
case PfRule::TRANS: return "TRANS"; |
106 |
5 |
case PfRule::CONG: return "CONG"; |
107 |
5 |
case PfRule::TRUE_INTRO: return "TRUE_INTRO"; |
108 |
1 |
case PfRule::TRUE_ELIM: return "TRUE_ELIM"; |
109 |
5 |
case PfRule::FALSE_INTRO: return "FALSE_INTRO"; |
110 |
4 |
case PfRule::FALSE_ELIM: return "FALSE_ELIM"; |
111 |
|
case PfRule::HO_APP_ENCODE: return "HO_APP_ENCODE"; |
112 |
|
case PfRule::HO_CONG: return "HO_CONG"; |
113 |
|
//================================================= Array rules |
114 |
|
case PfRule::ARRAYS_READ_OVER_WRITE: return "ARRAYS_READ_OVER_WRITE"; |
115 |
|
case PfRule::ARRAYS_READ_OVER_WRITE_CONTRA: |
116 |
|
return "ARRAYS_READ_OVER_WRITE_CONTRA"; |
117 |
|
case PfRule::ARRAYS_READ_OVER_WRITE_1: return "ARRAYS_READ_OVER_WRITE_1"; |
118 |
|
case PfRule::ARRAYS_EXT: return "ARRAYS_EXT"; |
119 |
|
case PfRule::ARRAYS_TRUST: return "ARRAYS_TRUST"; |
120 |
|
//================================================= Bit-Vector rules |
121 |
|
case PfRule::BV_BITBLAST: return "BV_BITBLAST"; |
122 |
|
case PfRule::BV_BITBLAST_CONST: return "BV_BITBLAST_CONST"; |
123 |
|
case PfRule::BV_BITBLAST_VAR: return "BV_BITBLAST_VAR"; |
124 |
|
case PfRule::BV_BITBLAST_EQUAL: return "BV_BITBLAST_EQUAL"; |
125 |
|
case PfRule::BV_BITBLAST_ULT: return "BV_BITBLAST_ULT"; |
126 |
|
case PfRule::BV_BITBLAST_ULE: return "BV_BITBLAST_ULE"; |
127 |
|
case PfRule::BV_BITBLAST_UGT: return "BV_BITBLAST_UGT"; |
128 |
|
case PfRule::BV_BITBLAST_UGE: return "BV_BITBLAST_UGE"; |
129 |
|
case PfRule::BV_BITBLAST_SLT: return "BV_BITBLAST_SLT"; |
130 |
|
case PfRule::BV_BITBLAST_SLE: return "BV_BITBLAST_SLE"; |
131 |
|
case PfRule::BV_BITBLAST_SGT: return "BV_BITBLAST_SGT"; |
132 |
|
case PfRule::BV_BITBLAST_SGE: return "BV_BITBLAST_SGE"; |
133 |
|
case PfRule::BV_BITBLAST_NOT: return "BV_BITBLAST_NOT"; |
134 |
|
case PfRule::BV_BITBLAST_CONCAT: return "BV_BITBLAST_CONCAT"; |
135 |
|
case PfRule::BV_BITBLAST_AND: return "BV_BITBLAST_AND"; |
136 |
|
case PfRule::BV_BITBLAST_OR: return "BV_BITBLAST_OR"; |
137 |
|
case PfRule::BV_BITBLAST_XOR: return "BV_BITBLAST_XOR"; |
138 |
|
case PfRule::BV_BITBLAST_XNOR: return "BV_BITBLAST_XNOR"; |
139 |
|
case PfRule::BV_BITBLAST_NAND: return "BV_BITBLAST_NAND"; |
140 |
|
case PfRule::BV_BITBLAST_NOR: return "BV_BITBLAST_NOR"; |
141 |
|
case PfRule::BV_BITBLAST_COMP: return "BV_BITBLAST_COMP"; |
142 |
|
case PfRule::BV_BITBLAST_MULT: return "BV_BITBLAST_MULT"; |
143 |
|
case PfRule::BV_BITBLAST_ADD: return "BV_BITBLAST_ADD"; |
144 |
|
case PfRule::BV_BITBLAST_SUB: return "BV_BITBLAST_SUB"; |
145 |
|
case PfRule::BV_BITBLAST_NEG: return "BV_BITBLAST_NEG"; |
146 |
|
case PfRule::BV_BITBLAST_UDIV: return "BV_BITBLAST_UDIV"; |
147 |
|
case PfRule::BV_BITBLAST_UREM: return "BV_BITBLAST_UREM"; |
148 |
|
case PfRule::BV_BITBLAST_SDIV: return "BV_BITBLAST_SDIV"; |
149 |
|
case PfRule::BV_BITBLAST_SREM: return "BV_BITBLAST_SREM"; |
150 |
|
case PfRule::BV_BITBLAST_SMOD: return "BV_BITBLAST_SMOD"; |
151 |
|
case PfRule::BV_BITBLAST_SHL: return "BV_BITBLAST_SHL"; |
152 |
|
case PfRule::BV_BITBLAST_LSHR: return "BV_BITBLAST_LSHR"; |
153 |
|
case PfRule::BV_BITBLAST_ASHR: return "BV_BITBLAST_ASHR"; |
154 |
|
case PfRule::BV_BITBLAST_ULTBV: return "BV_BITBLAST_ULTBV"; |
155 |
|
case PfRule::BV_BITBLAST_SLTBV: return "BV_BITBLAST_SLTBV"; |
156 |
|
case PfRule::BV_BITBLAST_ITE: return "BV_BITBLAST_ITE"; |
157 |
|
case PfRule::BV_BITBLAST_EXTRACT: return "BV_BITBLAST_EXTRACT"; |
158 |
|
case PfRule::BV_BITBLAST_REPEAT: return "BV_BITBLAST_REPEAT"; |
159 |
|
case PfRule::BV_BITBLAST_ZERO_EXTEND: return "BV_BITBLAST_ZERO_EXTEND"; |
160 |
|
case PfRule::BV_BITBLAST_SIGN_EXTEND: return "BV_BITBLAST_SIGN_EXTEND"; |
161 |
|
case PfRule::BV_BITBLAST_ROTATE_RIGHT: return "BV_BITBLAST_ROTATE_RIGHT"; |
162 |
|
case PfRule::BV_BITBLAST_ROTATE_LEFT: return "BV_BITBLAST_ROTATE_LEFT"; |
163 |
|
case PfRule::BV_EAGER_ATOM: return "BV_EAGER_ATOM"; |
164 |
|
//================================================= Datatype rules |
165 |
|
case PfRule::DT_UNIF: return "DT_UNIF"; |
166 |
|
case PfRule::DT_INST: return "DT_INST"; |
167 |
|
case PfRule::DT_COLLAPSE: return "DT_COLLAPSE"; |
168 |
|
case PfRule::DT_SPLIT: return "DT_SPLIT"; |
169 |
|
case PfRule::DT_CLASH: return "DT_CLASH"; |
170 |
|
case PfRule::DT_TRUST: return "DT_TRUST"; |
171 |
|
//================================================= Quantifiers rules |
172 |
|
case PfRule::SKOLEM_INTRO: return "SKOLEM_INTRO"; |
173 |
|
case PfRule::EXISTS_INTRO: return "EXISTS_INTRO"; |
174 |
|
case PfRule::SKOLEMIZE: return "SKOLEMIZE"; |
175 |
|
case PfRule::INSTANTIATE: return "INSTANTIATE"; |
176 |
|
//================================================= String rules |
177 |
|
case PfRule::CONCAT_EQ: return "CONCAT_EQ"; |
178 |
|
case PfRule::CONCAT_UNIFY: return "CONCAT_UNIFY"; |
179 |
|
case PfRule::CONCAT_CONFLICT: return "CONCAT_CONFLICT"; |
180 |
|
case PfRule::CONCAT_SPLIT: return "CONCAT_SPLIT"; |
181 |
|
case PfRule::CONCAT_CSPLIT: return "CONCAT_CSPLIT"; |
182 |
|
case PfRule::CONCAT_LPROP: return "CONCAT_LPROP"; |
183 |
|
case PfRule::CONCAT_CPROP: return "CONCAT_CPROP"; |
184 |
|
case PfRule::STRING_DECOMPOSE: return "STRING_DECOMPOSE"; |
185 |
|
case PfRule::STRING_LENGTH_POS: return "STRING_LENGTH_POS"; |
186 |
|
case PfRule::STRING_LENGTH_NON_EMPTY: return "STRING_LENGTH_NON_EMPTY"; |
187 |
|
case PfRule::STRING_REDUCTION: return "STRING_REDUCTION"; |
188 |
|
case PfRule::STRING_EAGER_REDUCTION: return "STRING_EAGER_REDUCTION"; |
189 |
|
case PfRule::RE_INTER: return "RE_INTER"; |
190 |
|
case PfRule::RE_UNFOLD_POS: return "RE_UNFOLD_POS"; |
191 |
|
case PfRule::RE_UNFOLD_NEG: return "RE_UNFOLD_NEG"; |
192 |
|
case PfRule::RE_UNFOLD_NEG_CONCAT_FIXED: |
193 |
|
return "RE_UNFOLD_NEG_CONCAT_FIXED"; |
194 |
|
case PfRule::RE_ELIM: return "RE_ELIM"; |
195 |
|
case PfRule::STRING_CODE_INJ: return "STRING_CODE_INJ"; |
196 |
|
case PfRule::STRING_SEQ_UNIT_INJ: return "STRING_SEQ_UNIT_INJ"; |
197 |
|
case PfRule::STRING_TRUST: return "STRING_TRUST"; |
198 |
|
//================================================= Arith rules |
199 |
32823 |
case PfRule::MACRO_ARITH_SCALE_SUM_UB: |
200 |
32823 |
return "ARITH_SCALE_SUM_UPPER_BOUNDS"; |
201 |
|
case PfRule::ARITH_SUM_UB: return "ARITH_SUM_UB"; |
202 |
1582 |
case PfRule::ARITH_TRICHOTOMY: return "ARITH_TRICHOTOMY"; |
203 |
273 |
case PfRule::INT_TIGHT_LB: return "INT_TIGHT_LB"; |
204 |
15297 |
case PfRule::INT_TIGHT_UB: return "INT_TIGHT_UB"; |
205 |
|
case PfRule::INT_TRUST: return "INT_TRUST"; |
206 |
|
case PfRule::ARITH_MULT_SIGN: return "ARITH_MULT_SIGN"; |
207 |
|
case PfRule::ARITH_MULT_POS: return "ARITH_MULT_POS"; |
208 |
|
case PfRule::ARITH_MULT_NEG: return "ARITH_MULT_NEG"; |
209 |
|
case PfRule::ARITH_MULT_TANGENT: return "ARITH_MULT_TANGENT"; |
210 |
|
case PfRule::ARITH_OP_ELIM_AXIOM: return "ARITH_OP_ELIM_AXIOM"; |
211 |
|
case PfRule::ARITH_TRANS_PI: return "ARITH_TRANS_PI"; |
212 |
|
case PfRule::ARITH_TRANS_EXP_NEG: return "ARITH_TRANS_EXP_NEG"; |
213 |
|
case PfRule::ARITH_TRANS_EXP_POSITIVITY: |
214 |
|
return "ARITH_TRANS_EXP_POSITIVITY"; |
215 |
|
case PfRule::ARITH_TRANS_EXP_SUPER_LIN: return "ARITH_TRANS_EXP_SUPER_LIN"; |
216 |
|
case PfRule::ARITH_TRANS_EXP_ZERO: return "ARITH_TRANS_EXP_ZERO"; |
217 |
|
case PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_NEG: |
218 |
|
return "ARITH_TRANS_EXP_APPROX_ABOVE_NEG"; |
219 |
|
case PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_POS: |
220 |
|
return "ARITH_TRANS_EXP_APPROX_ABOVE_POS"; |
221 |
|
case PfRule::ARITH_TRANS_EXP_APPROX_BELOW: |
222 |
|
return "ARITH_TRANS_EXP_APPROX_BELOW"; |
223 |
|
case PfRule::ARITH_TRANS_SINE_BOUNDS: return "ARITH_TRANS_SINE_BOUNDS"; |
224 |
|
case PfRule::ARITH_TRANS_SINE_SHIFT: return "ARITH_TRANS_SINE_SHIFT"; |
225 |
|
case PfRule::ARITH_TRANS_SINE_SYMMETRY: return "ARITH_TRANS_SINE_SYMMETRY"; |
226 |
|
case PfRule::ARITH_TRANS_SINE_TANGENT_ZERO: |
227 |
|
return "ARITH_TRANS_SINE_TANGENT_ZERO"; |
228 |
|
case PfRule::ARITH_TRANS_SINE_TANGENT_PI: |
229 |
|
return "ARITH_TRANS_SINE_TANGENT_PI"; |
230 |
|
case PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_NEG: |
231 |
|
return "ARITH_TRANS_SINE_APPROX_ABOVE_NEG"; |
232 |
|
case PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_POS: |
233 |
|
return "ARITH_TRANS_SINE_APPROX_ABOVE_POS"; |
234 |
|
case PfRule::ARITH_TRANS_SINE_APPROX_BELOW_NEG: |
235 |
|
return "ARITH_TRANS_SINE_APPROX_BELOW_NEG"; |
236 |
|
case PfRule::ARITH_TRANS_SINE_APPROX_BELOW_POS: |
237 |
|
return "ARITH_TRANS_SINE_APPROX_BELOW_POS"; |
238 |
|
case PfRule::ARITH_NL_CAD_DIRECT: return "ARITH_NL_CAD_DIRECT"; |
239 |
|
case PfRule::ARITH_NL_CAD_RECURSIVE: return "ARITH_NL_CAD_RECURSIVE"; |
240 |
|
//================================================= Unknown rule |
241 |
|
case PfRule::UNKNOWN: return "UNKNOWN"; |
242 |
|
default: return "?"; |
243 |
|
} |
244 |
|
} |
245 |
|
|
246 |
148490 |
std::ostream& operator<<(std::ostream& out, PfRule id) |
247 |
|
{ |
248 |
148490 |
out << toString(id); |
249 |
148490 |
return out; |
250 |
|
} |
251 |
|
|
252 |
2459870 |
size_t PfRuleHashFunction::operator()(PfRule id) const |
253 |
|
{ |
254 |
2459870 |
return static_cast<size_t>(id); |
255 |
|
} |
256 |
|
|
257 |
27735 |
} // namespace cvc5 |