GCC Code Coverage Report
Directory: . Exec Total Coverage
File: build-coverage/src/options/strings_options.cpp Lines: 48 179 26.8 %
Date: 2021-03-22 Branches: 2 61 3.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file module_template.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mathias Preiner
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 Option template for option modules.
13
 **
14
 ** For each <module>_options.toml configuration file, mkoptions.py
15
 ** expands this template and generates a <module>_options.cpp file.
16
 **/
17
18
#include "options/options_holder.h"
19
#include "base/check.h"
20
21
namespace CVC4 {
22
23
template <> void Options::set(
24
    options::regExpElim__option_t,
25
    const options::regExpElim__option_t::type& x)
26
{
27
  d_holder->regExpElim = x;
28
}
29
87874
template <> const options::regExpElim__option_t::type& Options::operator[](
30
    options::regExpElim__option_t) const
31
{
32
87874
  return d_holder->regExpElim;
33
}
34
template <> bool Options::wasSetByUser(options::regExpElim__option_t) const
35
{
36
  return d_holder->regExpElim__setByUser__;
37
}
38
template <> void Options::set(
39
    options::regExpElimAgg__option_t,
40
    const options::regExpElimAgg__option_t::type& x)
41
{
42
  d_holder->regExpElimAgg = x;
43
}
44
8995
template <> const options::regExpElimAgg__option_t::type& Options::operator[](
45
    options::regExpElimAgg__option_t) const
46
{
47
8995
  return d_holder->regExpElimAgg;
48
}
49
template <> bool Options::wasSetByUser(options::regExpElimAgg__option_t) const
50
{
51
  return d_holder->regExpElimAgg__setByUser__;
52
}
53
template <> void Options::set(
54
    options::stringRegExpInterMode__option_t,
55
    const options::stringRegExpInterMode__option_t::type& x)
56
{
57
  d_holder->stringRegExpInterMode = x;
58
}
59
1229
template <> const options::stringRegExpInterMode__option_t::type& Options::operator[](
60
    options::stringRegExpInterMode__option_t) const
61
{
62
1229
  return d_holder->stringRegExpInterMode;
63
}
64
template <> bool Options::wasSetByUser(options::stringRegExpInterMode__option_t) const
65
{
66
  return d_holder->stringRegExpInterMode__setByUser__;
67
}
68
2747
template <> const options::stringCheckEntailLen__option_t::type& Options::operator[](
69
    options::stringCheckEntailLen__option_t) const
70
{
71
2747
  return d_holder->stringCheckEntailLen;
72
}
73
template <> bool Options::wasSetByUser(options::stringCheckEntailLen__option_t) const
74
{
75
  return d_holder->stringCheckEntailLen__setByUser__;
76
}
77
17184
template <> const options::stringEager__option_t::type& Options::operator[](
78
    options::stringEager__option_t) const
79
{
80
17184
  return d_holder->stringEager;
81
}
82
template <> bool Options::wasSetByUser(options::stringEager__option_t) const
83
{
84
  return d_holder->stringEager__setByUser__;
85
}
86
template <> void Options::set(
87
    options::stringEagerEval__option_t,
88
    const options::stringEagerEval__option_t::type& x)
89
{
90
  d_holder->stringEagerEval = x;
91
}
92
8995
template <> const options::stringEagerEval__option_t::type& Options::operator[](
93
    options::stringEagerEval__option_t) const
94
{
95
8995
  return d_holder->stringEagerEval;
96
}
97
template <> bool Options::wasSetByUser(options::stringEagerEval__option_t) const
98
{
99
  return d_holder->stringEagerEval__setByUser__;
100
}
101
44778
template <> const options::stringEagerLen__option_t::type& Options::operator[](
102
    options::stringEagerLen__option_t) const
103
{
104
44778
  return d_holder->stringEagerLen;
105
}
106
template <> bool Options::wasSetByUser(options::stringEagerLen__option_t) const
107
{
108
  return d_holder->stringEagerLen__setByUser__;
109
}
110
template <> void Options::set(
111
    options::stringExp__option_t,
112
    const options::stringExp__option_t::type& x)
113
{
114
  d_holder->stringExp = x;
115
}
116
130621
template <> const options::stringExp__option_t::type& Options::operator[](
117
    options::stringExp__option_t) const
118
{
119
130621
  return d_holder->stringExp;
120
}
121
template <> bool Options::wasSetByUser(options::stringExp__option_t) const
122
{
123
  return d_holder->stringExp__setByUser__;
124
}
125
8592
template <> const options::stringFlatForms__option_t::type& Options::operator[](
126
    options::stringFlatForms__option_t) const
127
{
128
8592
  return d_holder->stringFlatForms;
129
}
130
template <> bool Options::wasSetByUser(options::stringFlatForms__option_t) const
131
{
132
  return d_holder->stringFlatForms__setByUser__;
133
}
134
template <> void Options::set(
135
    options::stringFMF__option_t,
136
    const options::stringFMF__option_t::type& x)
137
{
138
  d_holder->stringFMF = x;
139
}
140
97071
template <> const options::stringFMF__option_t::type& Options::operator[](
141
    options::stringFMF__option_t) const
142
{
143
97071
  return d_holder->stringFMF;
144
}
145
template <> bool Options::wasSetByUser(options::stringFMF__option_t) const
146
{
147
  return d_holder->stringFMF__setByUser__;
148
}
149
7074
template <> const options::stringGuessModel__option_t::type& Options::operator[](
150
    options::stringGuessModel__option_t) const
151
{
152
7074
  return d_holder->stringGuessModel;
153
}
154
template <> bool Options::wasSetByUser(options::stringGuessModel__option_t) const
155
{
156
  return d_holder->stringGuessModel__setByUser__;
157
}
158
15311
template <> const options::stringInferAsLemmas__option_t::type& Options::operator[](
159
    options::stringInferAsLemmas__option_t) const
160
{
161
15311
  return d_holder->stringInferAsLemmas;
162
}
163
template <> bool Options::wasSetByUser(options::stringInferAsLemmas__option_t) const
164
{
165
  return d_holder->stringInferAsLemmas__setByUser__;
166
}
167
83064
template <> const options::stringInferSym__option_t::type& Options::operator[](
168
    options::stringInferSym__option_t) const
169
{
170
83064
  return d_holder->stringInferSym;
171
}
172
template <> bool Options::wasSetByUser(options::stringInferSym__option_t) const
173
{
174
  return d_holder->stringInferSym__setByUser__;
175
}
176
310
template <> const options::stringIgnNegMembership__option_t::type& Options::operator[](
177
    options::stringIgnNegMembership__option_t) const
178
{
179
310
  return d_holder->stringIgnNegMembership;
180
}
181
template <> bool Options::wasSetByUser(options::stringIgnNegMembership__option_t) const
182
{
183
  return d_holder->stringIgnNegMembership__setByUser__;
184
}
185
19794
template <> const options::stringLazyPreproc__option_t::type& Options::operator[](
186
    options::stringLazyPreproc__option_t) const
187
{
188
19794
  return d_holder->stringLazyPreproc;
189
}
190
template <> bool Options::wasSetByUser(options::stringLazyPreproc__option_t) const
191
{
192
  return d_holder->stringLazyPreproc__setByUser__;
193
}
194
8592
template <> const options::stringLenNorm__option_t::type& Options::operator[](
195
    options::stringLenNorm__option_t) const
196
{
197
8592
  return d_holder->stringLenNorm;
198
}
199
template <> bool Options::wasSetByUser(options::stringLenNorm__option_t) const
200
{
201
  return d_holder->stringLenNorm__setByUser__;
202
}
203
template <> const options::stringLenPropCsp__option_t::type& Options::operator[](
204
    options::stringLenPropCsp__option_t) const
205
{
206
  return d_holder->stringLenPropCsp;
207
}
208
template <> bool Options::wasSetByUser(options::stringLenPropCsp__option_t) const
209
{
210
  return d_holder->stringLenPropCsp__setByUser__;
211
}
212
21054
template <> const options::stringMinPrefixExplain__option_t::type& Options::operator[](
213
    options::stringMinPrefixExplain__option_t) const
214
{
215
21054
  return d_holder->stringMinPrefixExplain;
216
}
217
template <> bool Options::wasSetByUser(options::stringMinPrefixExplain__option_t) const
218
{
219
  return d_holder->stringMinPrefixExplain__setByUser__;
220
}
221
39075
template <> const options::stdPrintASCII__option_t::type& Options::operator[](
222
    options::stdPrintASCII__option_t) const
223
{
224
39075
  return d_holder->stdPrintASCII;
225
}
226
template <> bool Options::wasSetByUser(options::stdPrintASCII__option_t) const
227
{
228
  return d_holder->stdPrintASCII__setByUser__;
229
}
230
40
template <> void Options::set(
231
    options::stringProcessLoopMode__option_t,
232
    const options::stringProcessLoopMode__option_t::type& x)
233
{
234
40
  d_holder->stringProcessLoopMode = x;
235
40
}
236
1580
template <> const options::stringProcessLoopMode__option_t::type& Options::operator[](
237
    options::stringProcessLoopMode__option_t) const
238
{
239
1580
  return d_holder->stringProcessLoopMode;
240
}
241
40
template <> bool Options::wasSetByUser(options::stringProcessLoopMode__option_t) const
242
{
243
40
  return d_holder->stringProcessLoopMode__setByUser__;
244
}
245
14846
template <> const options::stringRExplainLemmas__option_t::type& Options::operator[](
246
    options::stringRExplainLemmas__option_t) const
247
{
248
14846
  return d_holder->stringRExplainLemmas;
249
}
250
template <> bool Options::wasSetByUser(options::stringRExplainLemmas__option_t) const
251
{
252
  return d_holder->stringRExplainLemmas__setByUser__;
253
}
254
5534
template <> const options::stringUnifiedVSpt__option_t::type& Options::operator[](
255
    options::stringUnifiedVSpt__option_t) const
256
{
257
5534
  return d_holder->stringUnifiedVSpt;
258
}
259
template <> bool Options::wasSetByUser(options::stringUnifiedVSpt__option_t) const
260
{
261
  return d_holder->stringUnifiedVSpt__setByUser__;
262
}
263
264
265
namespace options {
266
267
thread_local struct regExpElim__option_t regExpElim;
268
thread_local struct regExpElimAgg__option_t regExpElimAgg;
269
thread_local struct stringRegExpInterMode__option_t stringRegExpInterMode;
270
thread_local struct stringCheckEntailLen__option_t stringCheckEntailLen;
271
thread_local struct stringEager__option_t stringEager;
272
thread_local struct stringEagerEval__option_t stringEagerEval;
273
thread_local struct stringEagerLen__option_t stringEagerLen;
274
thread_local struct stringExp__option_t stringExp;
275
thread_local struct stringFlatForms__option_t stringFlatForms;
276
thread_local struct stringFMF__option_t stringFMF;
277
thread_local struct stringGuessModel__option_t stringGuessModel;
278
thread_local struct stringInferAsLemmas__option_t stringInferAsLemmas;
279
thread_local struct stringInferSym__option_t stringInferSym;
280
thread_local struct stringIgnNegMembership__option_t stringIgnNegMembership;
281
thread_local struct stringLazyPreproc__option_t stringLazyPreproc;
282
thread_local struct stringLenNorm__option_t stringLenNorm;
283
thread_local struct stringLenPropCsp__option_t stringLenPropCsp;
284
thread_local struct stringMinPrefixExplain__option_t stringMinPrefixExplain;
285
thread_local struct stdPrintASCII__option_t stdPrintASCII;
286
thread_local struct stringProcessLoopMode__option_t stringProcessLoopMode;
287
thread_local struct stringRExplainLemmas__option_t stringRExplainLemmas;
288
thread_local struct stringUnifiedVSpt__option_t stringUnifiedVSpt;
289
290
291
std::ostream&
292
operator<<(std::ostream& os, RegExpInterMode mode)
293
{
294
  os << "RegExpInterMode::";
295
  switch(mode) {
296
    case RegExpInterMode::CONSTANT:
297
      os << "CONSTANT";
298
      break;
299
    case RegExpInterMode::NONE:
300
      os << "NONE";
301
      break;
302
    case RegExpInterMode::ALL:
303
      os << "ALL";
304
      break;
305
    case RegExpInterMode::ONE_CONSTANT:
306
      os << "ONE_CONSTANT";
307
      break;
308
    default:
309
        Unreachable();
310
  }
311
  return os;
312
}
313
314
RegExpInterMode
315
stringToRegExpInterMode(const std::string& option, const std::string& optarg)
316
{
317
  if (optarg == "constant")
318
  {
319
    return RegExpInterMode::CONSTANT;
320
  }
321
  else if (optarg == "none")
322
  {
323
    return RegExpInterMode::NONE;
324
  }
325
  else if (optarg == "all")
326
  {
327
    return RegExpInterMode::ALL;
328
  }
329
  else if (optarg == "one-constant")
330
  {
331
    return RegExpInterMode::ONE_CONSTANT;
332
  }
333
  else if (optarg == "help")
334
  {
335
    puts("Regular expression intersection modes.\n"
336
         "Available modes for --re-inter-mode are:\n"
337
         "+ constant (default)\n"
338
         "  Compute intersections only between regular expressions that do not contain\n"
339
         "  re.allchar or re.range.\n"
340
         "+ none\n"
341
         "  Do not compute intersections for regular expressions.\n"
342
         "+ all\n"
343
         "  Compute intersections for all regular expressions.\n"
344
         "+ one-constant\n"
345
         "  Compute intersections only between regular expressions such that at least one\n"
346
         "  side does not contain re.allchar or re.range.\n");
347
    exit(1);
348
  }
349
  else
350
  {
351
    throw OptionException(std::string("unknown option for --re-inter-mode: `") +
352
                          optarg + "'.  Try --re-inter-mode=help.");
353
  }
354
}
355
356
std::ostream&
357
operator<<(std::ostream& os, ProcessLoopMode mode)
358
{
359
  os << "ProcessLoopMode::";
360
  switch(mode) {
361
    case ProcessLoopMode::NONE:
362
      os << "NONE";
363
      break;
364
    case ProcessLoopMode::SIMPLE:
365
      os << "SIMPLE";
366
      break;
367
    case ProcessLoopMode::FULL:
368
      os << "FULL";
369
      break;
370
    case ProcessLoopMode::ABORT:
371
      os << "ABORT";
372
      break;
373
    case ProcessLoopMode::SIMPLE_ABORT:
374
      os << "SIMPLE_ABORT";
375
      break;
376
    default:
377
        Unreachable();
378
  }
379
  return os;
380
}
381
382
ProcessLoopMode
383
stringToProcessLoopMode(const std::string& option, const std::string& optarg)
384
{
385
  if (optarg == "none")
386
  {
387
    return ProcessLoopMode::NONE;
388
  }
389
  else if (optarg == "simple")
390
  {
391
    return ProcessLoopMode::SIMPLE;
392
  }
393
  else if (optarg == "full")
394
  {
395
    return ProcessLoopMode::FULL;
396
  }
397
  else if (optarg == "abort")
398
  {
399
    return ProcessLoopMode::ABORT;
400
  }
401
  else if (optarg == "simple-abort")
402
  {
403
    return ProcessLoopMode::SIMPLE_ABORT;
404
  }
405
  else if (optarg == "help")
406
  {
407
    puts("Loop processing modes.\n"
408
         "Available modes for --strings-process-loop-mode are:\n"
409
         "+ none\n"
410
         "  Omit loop processing.\n"
411
         "+ simple\n"
412
         "  Omit normal loop breaking (default with --strings-fmf).\n"
413
         "+ full (default)\n"
414
         "  Perform full processing of looping word equations.\n"
415
         "+ abort\n"
416
         "  Abort if looping word equations are encountered.\n"
417
         "+ simple-abort\n"
418
         "  Abort when normal loop breaking is required.\n");
419
    exit(1);
420
  }
421
  else
422
  {
423
    throw OptionException(std::string("unknown option for --strings-process-loop-mode: `") +
424
                          optarg + "'.  Try --strings-process-loop-mode=help.");
425
  }
426
}
427
428
429
}  // namespace options
430
26676
}  // namespace CVC4