GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/rewrites.cpp Lines: 1 195 0.5 %
Date: 2021-03-23 Branches: 2 191 1.0 %

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