1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Andres Noetzli, Yoni Zohar |
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 inference information utility. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/strings/rewrites.h" |
17 |
|
|
18 |
|
#include <iostream> |
19 |
|
|
20 |
|
namespace cvc5 { |
21 |
|
namespace theory { |
22 |
|
namespace strings { |
23 |
|
|
24 |
|
const char* toString(Rewrite r) |
25 |
|
{ |
26 |
|
switch (r) |
27 |
|
{ |
28 |
|
case Rewrite::CTN_COMPONENT: return "CTN_COMPONENT"; |
29 |
|
case Rewrite::CTN_CONCAT_CHAR: return "CTN_CONCAT_CHAR"; |
30 |
|
case Rewrite::CTN_CONST: return "CTN_CONST"; |
31 |
|
case Rewrite::CTN_EQ: return "CTN_EQ"; |
32 |
|
case Rewrite::CTN_LEN_INEQ: return "CTN_LEN_INEQ"; |
33 |
|
case Rewrite::CTN_LEN_INEQ_NSTRICT: return "CTN_LEN_INEQ_NSTRICT"; |
34 |
|
case Rewrite::CTN_LHS_EMPTYSTR: return "CTN_LHS_EMPTYSTR"; |
35 |
|
case Rewrite::CTN_MSET_NSS: return "CTN_MSET_NSS"; |
36 |
|
case Rewrite::CTN_NCONST_CTN_CONCAT: return "CTN_NCONST_CTN_CONCAT"; |
37 |
|
case Rewrite::CTN_REPL: return "CTN_REPL"; |
38 |
|
case Rewrite::CTN_REPL_CHAR: return "CTN_REPL_CHAR"; |
39 |
|
case Rewrite::CTN_REPL_CNSTS_TO_CTN: return "CTN_REPL_CNSTS_TO_CTN"; |
40 |
|
case Rewrite::CTN_REPL_EMPTY: return "CTN_REPL_EMPTY"; |
41 |
|
case Rewrite::CTN_REPL_LEN_ONE_TO_CTN: return "CTN_REPL_LEN_ONE_TO_CTN"; |
42 |
|
case Rewrite::CTN_REPL_SELF: return "CTN_REPL_SELF"; |
43 |
|
case Rewrite::CTN_REPL_SIMP_REPL: return "CTN_REPL_SIMP_REPL"; |
44 |
|
case Rewrite::CTN_REPL_TO_CTN: return "CTN_REPL_TO_CTN"; |
45 |
|
case Rewrite::CTN_REPL_TO_CTN_DISJ: return "CTN_REPL_TO_CTN_DISJ"; |
46 |
|
case Rewrite::CTN_RHS_EMPTYSTR: return "CTN_RHS_EMPTYSTR"; |
47 |
|
case Rewrite::CTN_RPL_NON_CTN: return "CTN_RPL_NON_CTN"; |
48 |
|
case Rewrite::CTN_SPLIT: return "CTN_SPLIT"; |
49 |
|
case Rewrite::CTN_SPLIT_ONES: return "CTN_SPLIT_ONES"; |
50 |
|
case Rewrite::CTN_STRIP_ENDPT: return "CTN_STRIP_ENDPT"; |
51 |
|
case Rewrite::CTN_SUBSTR: return "CTN_SUBSTR"; |
52 |
|
case Rewrite::EQ_LEN_DEQ: return "EQ_LEN_DEQ"; |
53 |
|
case Rewrite::EQ_NCTN: return "EQ_NCTN"; |
54 |
|
case Rewrite::EQ_NFIX: return "EQ_NFIX"; |
55 |
|
case Rewrite::FROM_CODE_EVAL: return "FROM_CODE_EVAL"; |
56 |
|
case Rewrite::IDOF_DEF_CTN: return "IDOF_DEF_CTN"; |
57 |
|
case Rewrite::IDOF_EMP_IDOF: return "IDOF_EMP_IDOF"; |
58 |
|
case Rewrite::IDOF_EQ_CST_START: return "IDOF_EQ_CST_START"; |
59 |
|
case Rewrite::IDOF_EQ_NORM: return "IDOF_EQ_NORM"; |
60 |
|
case Rewrite::IDOF_EQ_NSTART: return "IDOF_EQ_NSTART"; |
61 |
|
case Rewrite::IDOF_FIND: return "IDOF_FIND"; |
62 |
|
case Rewrite::IDOF_LEN: return "IDOF_LEN"; |
63 |
|
case Rewrite::IDOF_MAX: return "IDOF_MAX"; |
64 |
|
case Rewrite::IDOF_NCTN: return "IDOF_NCTN"; |
65 |
|
case Rewrite::IDOF_NEG: return "IDOF_NEG"; |
66 |
|
case Rewrite::IDOF_NFIND: return "IDOF_NFIND"; |
67 |
|
case Rewrite::IDOF_NORM_PREFIX: return "IDOF_NORM_PREFIX"; |
68 |
|
case Rewrite::IDOF_PULL_ENDPT: return "IDOF_PULL_ENDPT"; |
69 |
|
case Rewrite::IDOF_STRIP_CNST_ENDPTS: return "IDOF_STRIP_CNST_ENDPTS"; |
70 |
|
case Rewrite::IDOF_STRIP_SYM_LEN: return "IDOF_STRIP_SYM_LEN"; |
71 |
|
case Rewrite::INDEXOF_RE_EMP_RE: return "INDEXOF_RE_EMP_RE"; |
72 |
|
case Rewrite::INDEXOF_RE_EVAL: return "INDEXOF_RE_EVAL"; |
73 |
|
case Rewrite::INDEXOF_RE_INVALID_INDEX: return "INDEXOF_RE_INVALID_INDEX"; |
74 |
|
case Rewrite::INDEXOF_RE_MAX_INDEX: return "INDEXOF_RE_MAX_INDEX"; |
75 |
|
case Rewrite::ITOS_EVAL: return "ITOS_EVAL"; |
76 |
|
case Rewrite::RE_AND_EMPTY: return "RE_AND_EMPTY"; |
77 |
|
case Rewrite::RE_ANDOR_FLATTEN: return "RE_ANDOR_FLATTEN"; |
78 |
|
case Rewrite::RE_ANDOR_INC_CONFLICT: return "RE_ANDOR_INC_CONFLICT"; |
79 |
|
case Rewrite::RE_CHAR_IN_STR_STAR: return "RE_CHAR_IN_STR_STAR"; |
80 |
|
case Rewrite::RE_CONCAT: return "RE_CONCAT"; |
81 |
|
case Rewrite::RE_CONCAT_FLATTEN: return "RE_CONCAT_FLATTEN"; |
82 |
|
case Rewrite::RE_CONCAT_OPT: return "RE_CONCAT_OPT"; |
83 |
|
case Rewrite::RE_CONCAT_PURE_ALLCHAR: return "RE_CONCAT_PURE_ALLCHAR"; |
84 |
|
case Rewrite::RE_CONCAT_TO_CONTAINS: return "RE_CONCAT_TO_CONTAINS"; |
85 |
|
case Rewrite::RE_EMPTY_IN_STR_STAR: return "RE_EMPTY_IN_STR_STAR"; |
86 |
|
case Rewrite::RE_IN_DIST_CHAR_STAR: return "RE_IN_DIST_CHAR_STAR"; |
87 |
|
case Rewrite::RE_IN_SIGMA_STAR: return "RE_IN_SIGMA_STAR"; |
88 |
|
case Rewrite::RE_LOOP: return "RE_LOOP"; |
89 |
|
case Rewrite::RE_LOOP_STAR: return "RE_LOOP_STAR"; |
90 |
|
case Rewrite::RE_OR_ALL: return "RE_OR_ALL"; |
91 |
|
case Rewrite::RE_SIMPLE_CONSUME: return "RE_SIMPLE_CONSUME"; |
92 |
|
case Rewrite::RE_STAR_EMPTY: return "RE_STAR_EMPTY"; |
93 |
|
case Rewrite::RE_STAR_EMPTY_STRING: return "RE_STAR_EMPTY_STRING"; |
94 |
|
case Rewrite::RE_STAR_NESTED_STAR: return "RE_STAR_NESTED_STAR"; |
95 |
|
case Rewrite::RE_STAR_UNION: return "RE_STAR_UNION"; |
96 |
|
case Rewrite::REPL_CHAR_NCONTRIB_FIND: return "REPL_CHAR_NCONTRIB_FIND"; |
97 |
|
case Rewrite::REPL_DUAL_REPL_ITE: return "REPL_DUAL_REPL_ITE"; |
98 |
|
case Rewrite::REPL_REPL_SHORT_CIRCUIT: return "REPL_REPL_SHORT_CIRCUIT"; |
99 |
|
case Rewrite::REPL_REPL2_INV: return "REPL_REPL2_INV"; |
100 |
|
case Rewrite::REPL_REPL2_INV_ID: return "REPL_REPL2_INV_ID"; |
101 |
|
case Rewrite::REPL_REPL3_INV: return "REPL_REPL3_INV"; |
102 |
|
case Rewrite::REPL_REPL3_INV_ID: return "REPL_REPL3_INV_ID"; |
103 |
|
case Rewrite::REPL_SUBST_IDX: return "REPL_SUBST_IDX"; |
104 |
|
case Rewrite::REPLALL_CONST: return "REPLALL_CONST"; |
105 |
|
case Rewrite::REPLALL_EMPTY_FIND: return "REPLALL_EMPTY_FIND"; |
106 |
|
case Rewrite::RPL_CCTN: return "RPL_CCTN"; |
107 |
|
case Rewrite::RPL_CCTN_RPL: return "RPL_CCTN_RPL"; |
108 |
|
case Rewrite::RPL_CNTS_SUBSTS: return "RPL_CNTS_SUBSTS"; |
109 |
|
case Rewrite::RPL_CONST_FIND: return "RPL_CONST_FIND"; |
110 |
|
case Rewrite::RPL_CONST_NFIND: return "RPL_CONST_NFIND"; |
111 |
|
case Rewrite::RPL_EMP_CNTS_SUBSTS: return "RPL_EMP_CNTS_SUBSTS"; |
112 |
|
case Rewrite::RPL_ID: return "RPL_ID"; |
113 |
|
case Rewrite::RPL_NCTN: return "RPL_NCTN"; |
114 |
|
case Rewrite::RPL_PULL_ENDPT: return "RPL_PULL_ENDPT"; |
115 |
|
case Rewrite::RPL_REPLACE: return "RPL_REPLACE"; |
116 |
|
case Rewrite::RPL_RPL_EMPTY: return "RPL_RPL_EMPTY"; |
117 |
|
case Rewrite::RPL_RPL_LEN_ID: return "RPL_RPL_LEN_ID"; |
118 |
|
case Rewrite::RPL_X_Y_X_SIMP: return "RPL_X_Y_X_SIMP"; |
119 |
|
case Rewrite::REPLACE_RE_EVAL: return "REPLACE_RE_EVAL"; |
120 |
|
case Rewrite::REPLACE_RE_ALL_EVAL: return "REPLACE_RE_ALL_EVAL"; |
121 |
|
case Rewrite::REPLACE_RE_EMP_RE: return "REPLACE_RE_EMP_RE"; |
122 |
|
case Rewrite::SPLIT_EQ: return "SPLIT_EQ"; |
123 |
|
case Rewrite::SPLIT_EQ_STRIP_L: return "SPLIT_EQ_STRIP_L"; |
124 |
|
case Rewrite::SPLIT_EQ_STRIP_R: return "SPLIT_EQ_STRIP_R"; |
125 |
|
case Rewrite::SS_COMBINE: return "SS_COMBINE"; |
126 |
|
case Rewrite::SS_CONST_END_OOB: return "SS_CONST_END_OOB"; |
127 |
|
case Rewrite::SS_CONST_LEN_MAX_OOB: return "SS_CONST_LEN_MAX_OOB"; |
128 |
|
case Rewrite::SS_CONST_LEN_NON_POS: return "SS_CONST_LEN_NON_POS"; |
129 |
|
case Rewrite::SS_CONST_SS: return "SS_CONST_SS"; |
130 |
|
case Rewrite::SS_CONST_START_MAX_OOB: return "SS_CONST_START_MAX_OOB"; |
131 |
|
case Rewrite::SS_CONST_START_NEG: return "SS_CONST_START_NEG"; |
132 |
|
case Rewrite::SS_CONST_START_OOB: return "SS_CONST_START_OOB"; |
133 |
|
case Rewrite::SS_EMPTYSTR: return "SS_EMPTYSTR"; |
134 |
|
case Rewrite::SS_END_PT_NORM: return "SS_END_PT_NORM"; |
135 |
|
case Rewrite::SS_GEQ_ZERO_START_ENTAILS_EMP_S: |
136 |
|
return "SS_GEQ_ZERO_START_ENTAILS_EMP_S"; |
137 |
|
case Rewrite::SS_LEN_INCLUDE: return "SS_LEN_INCLUDE"; |
138 |
|
case Rewrite::SS_LEN_NON_POS: return "SS_LEN_NON_POS"; |
139 |
|
case Rewrite::SS_LEN_ONE_Z_Z: return "SS_LEN_ONE_Z_Z"; |
140 |
|
case Rewrite::SS_NON_ZERO_LEN_ENTAILS_OOB: |
141 |
|
return "SS_NON_ZERO_LEN_ENTAILS_OOB"; |
142 |
|
case Rewrite::SS_START_ENTAILS_ZERO_LEN: return "SS_START_ENTAILS_ZERO_LEN"; |
143 |
|
case Rewrite::SS_START_GEQ_LEN: return "SS_START_GEQ_LEN"; |
144 |
|
case Rewrite::SS_START_NEG: return "SS_START_NEG"; |
145 |
|
case Rewrite::SS_STRIP_END_PT: return "SS_STRIP_END_PT"; |
146 |
|
case Rewrite::SS_STRIP_START_PT: return "SS_STRIP_START_PT"; |
147 |
|
case Rewrite::UPD_EVAL: return "UPD_EVAL"; |
148 |
|
case Rewrite::UPD_EMPTYSTR: return "UPD_EMPTYSTR"; |
149 |
|
case Rewrite::UPD_CONST_INDEX_MAX_OOB: return "UPD_CONST_INDEX_MAX_OOB"; |
150 |
|
case Rewrite::UPD_CONST_INDEX_NEG: return "UPD_CONST_INDEX_NEG"; |
151 |
|
case Rewrite::UPD_CONST_INDEX_OOB: return "UPD_CONST_INDEX_OOB"; |
152 |
|
case Rewrite::STOI_CONCAT_NONNUM: return "STOI_CONCAT_NONNUM"; |
153 |
|
case Rewrite::STOI_EVAL: return "STOI_EVAL"; |
154 |
|
case Rewrite::STR_CONV_CONST: return "STR_CONV_CONST"; |
155 |
|
case Rewrite::STR_CONV_IDEM: return "STR_CONV_IDEM"; |
156 |
|
case Rewrite::STR_CONV_ITOS: return "STR_CONV_ITOS"; |
157 |
|
case Rewrite::STR_CONV_MINSCOPE_CONCAT: return "STR_CONV_MINSCOPE_CONCAT"; |
158 |
|
case Rewrite::STR_EMP_REPL_EMP: return "STR_EMP_REPL_EMP"; |
159 |
|
case Rewrite::STR_EMP_REPL_EMP_R: return "STR_EMP_REPL_EMP_R"; |
160 |
|
case Rewrite::STR_EMP_REPL_X_Y_X: return "STR_EMP_REPL_X_Y_X"; |
161 |
|
case Rewrite::STR_EMP_SUBSTR_ELIM: return "STR_EMP_SUBSTR_ELIM"; |
162 |
|
case Rewrite::STR_EMP_SUBSTR_LEQ_LEN: return "STR_EMP_SUBSTR_LEQ_LEN"; |
163 |
|
case Rewrite::STR_EMP_SUBSTR_LEQ_Z: return "STR_EMP_SUBSTR_LEQ_Z"; |
164 |
|
case Rewrite::STR_EQ_CONJ_LEN_ENTAIL: return "STR_EQ_CONJ_LEN_ENTAIL"; |
165 |
|
case Rewrite::STR_EQ_CONST_NHOMOG: return "STR_EQ_CONST_NHOMOG"; |
166 |
|
case Rewrite::STR_EQ_HOMOG_CONST: return "STR_EQ_HOMOG_CONST"; |
167 |
|
case Rewrite::STR_EQ_REPL_EMP: return "STR_EQ_REPL_EMP"; |
168 |
|
case Rewrite::STR_EQ_REPL_NOT_CTN: return "STR_EQ_REPL_NOT_CTN"; |
169 |
|
case Rewrite::STR_EQ_REPL_TO_DIS: return "STR_EQ_REPL_TO_DIS"; |
170 |
|
case Rewrite::STR_EQ_REPL_TO_EQ: return "STR_EQ_REPL_TO_EQ"; |
171 |
|
case Rewrite::STR_EQ_UNIFY: return "STR_EQ_UNIFY"; |
172 |
|
case Rewrite::STR_LEQ_CPREFIX: return "STR_LEQ_CPREFIX"; |
173 |
|
case Rewrite::STR_LEQ_EMPTY: return "STR_LEQ_EMPTY"; |
174 |
|
case Rewrite::STR_LEQ_EVAL: return "STR_LEQ_EVAL"; |
175 |
|
case Rewrite::STR_LEQ_ID: return "STR_LEQ_ID"; |
176 |
|
case Rewrite::STR_REV_CONST: return "STR_REV_CONST"; |
177 |
|
case Rewrite::STR_REV_IDEM: return "STR_REV_IDEM"; |
178 |
|
case Rewrite::STR_REV_MINSCOPE_CONCAT: return "STR_REV_MINSCOPE_CONCAT"; |
179 |
|
case Rewrite::SUBSTR_REPL_SWAP: return "SUBSTR_REPL_SWAP"; |
180 |
|
case Rewrite::SUF_PREFIX_CONST: return "SUF_PREFIX_CONST"; |
181 |
|
case Rewrite::SUF_PREFIX_CTN: return "SUF_PREFIX_CTN"; |
182 |
|
case Rewrite::SUF_PREFIX_EMPTY: return "SUF_PREFIX_EMPTY"; |
183 |
|
case Rewrite::SUF_PREFIX_EMPTY_CONST: return "SUF_PREFIX_EMPTY_CONST"; |
184 |
|
case Rewrite::SUF_PREFIX_EQ: return "SUF_PREFIX_EQ"; |
185 |
|
case Rewrite::SUF_PREFIX_TO_EQS: return "SUF_PREFIX_TO_EQS"; |
186 |
|
case Rewrite::TO_CODE_EVAL: return "TO_CODE_EVAL"; |
187 |
|
case Rewrite::EQ_REFL: return "EQ_REFL"; |
188 |
|
case Rewrite::EQ_CONST_FALSE: return "EQ_CONST_FALSE"; |
189 |
|
case Rewrite::EQ_SYM: return "EQ_SYM"; |
190 |
|
case Rewrite::CONCAT_NORM: return "CONCAT_NORM"; |
191 |
|
case Rewrite::IS_DIGIT_ELIM: return "IS_DIGIT_ELIM"; |
192 |
|
case Rewrite::RE_CONCAT_EMPTY: return "RE_CONCAT_EMPTY"; |
193 |
|
case Rewrite::RE_CONSUME_CCONF: return "RE_CONSUME_CCONF"; |
194 |
|
case Rewrite::RE_CONSUME_S: return "RE_CONSUME_S"; |
195 |
|
case Rewrite::RE_CONSUME_S_CCONF: return "RE_CONSUME_S_CCONF"; |
196 |
|
case Rewrite::RE_CONSUME_S_FULL: return "RE_CONSUME_S_FULL"; |
197 |
|
case Rewrite::RE_IN_EMPTY: return "RE_IN_EMPTY"; |
198 |
|
case Rewrite::RE_IN_SIGMA: return "RE_IN_SIGMA"; |
199 |
|
case Rewrite::RE_IN_EVAL: return "RE_IN_EVAL"; |
200 |
|
case Rewrite::RE_IN_COMPLEMENT: return "RE_IN_COMPLEMENT"; |
201 |
|
case Rewrite::RE_IN_RANGE: return "RE_IN_RANGE"; |
202 |
|
case Rewrite::RE_IN_CSTRING: return "RE_IN_CSTRING"; |
203 |
|
case Rewrite::RE_IN_ANDOR: return "RE_IN_ANDOR"; |
204 |
|
case Rewrite::RE_REPEAT_ELIM: return "RE_REPEAT_ELIM"; |
205 |
|
case Rewrite::SUF_PREFIX_ELIM: return "SUF_PREFIX_ELIM"; |
206 |
|
case Rewrite::STR_LT_ELIM: return "STR_LT_ELIM"; |
207 |
|
case Rewrite::RE_RANGE_SINGLE: return "RE_RANGE_SINGLE"; |
208 |
|
case Rewrite::RE_RANGE_EMPTY: return "RE_RANGE_EMPTY"; |
209 |
|
case Rewrite::RE_OPT_ELIM: return "RE_OPT_ELIM"; |
210 |
|
case Rewrite::RE_PLUS_ELIM: return "RE_PLUS_ELIM"; |
211 |
|
case Rewrite::RE_DIFF_ELIM: return "RE_DIFF_ELIM"; |
212 |
|
case Rewrite::LEN_EVAL: return "LEN_EVAL"; |
213 |
|
case Rewrite::LEN_CONCAT: return "LEN_CONCAT"; |
214 |
|
case Rewrite::LEN_REPL_INV: return "LEN_REPL_INV"; |
215 |
|
case Rewrite::LEN_CONV_INV: return "LEN_CONV_INV"; |
216 |
|
case Rewrite::LEN_SEQ_UNIT: return "LEN_SEQ_UNIT"; |
217 |
|
case Rewrite::CHARAT_ELIM: return "CHARAT_ELIM"; |
218 |
|
case Rewrite::SEQ_UNIT_EVAL: return "SEQ_UNIT_EVAL"; |
219 |
|
case Rewrite::SEQ_NTH_EVAL: return "SEQ_NTH_EVAL"; |
220 |
|
case Rewrite::SEQ_NTH_TOTAL_OOB: return "SEQ_NTH_TOTAL_OOB"; |
221 |
|
default: return "?"; |
222 |
|
} |
223 |
|
} |
224 |
|
|
225 |
|
std::ostream& operator<<(std::ostream& out, Rewrite r) |
226 |
|
{ |
227 |
|
out << toString(r); |
228 |
|
return out; |
229 |
|
} |
230 |
|
|
231 |
|
} // namespace strings |
232 |
|
} // namespace theory |
233 |
29577 |
} // namespace cvc5 |