GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/bvminisat/utils/Options.h Lines: 22 92 23.9 %
Date: 2021-09-29 Branches: 4 72 5.6 %

Line Exec Source
1
/***************************************************************************************[Options.h]
2
Copyright (c) 2008-2010, Niklas Sorensson
3
4
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
5
associated documentation files (the "Software"), to deal in the Software without restriction,
6
including without limitation the rights to use, copy, modify, merge, publish, distribute,
7
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
8
furnished to do so, subject to the following conditions:
9
10
The above copyright notice and this permission notice shall be included in all copies or
11
substantial portions of the Software.
12
13
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
14
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
15
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
16
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
17
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
18
**************************************************************************************************/
19
20
#ifndef BVMinisat_Options_h
21
#define BVMinisat_Options_h
22
23
#include <stdlib.h>
24
#include <stdio.h>
25
#include <math.h>
26
#include <string.h>
27
28
#include "prop/bvminisat/mtl/IntTypes.h"
29
#include "prop/bvminisat/mtl/Vec.h"
30
#include "prop/bvminisat/utils/ParseUtils.h"
31
32
namespace cvc5 {
33
namespace BVMinisat {
34
35
//==================================================================================================
36
// Top-level option parse/help functions:
37
38
39
extern void parseOptions     (int& argc, char** argv, bool strict = false);
40
extern void printUsageAndExit(int  argc, char** argv, bool verbose = false);
41
extern void setUsageHelp     (const char* str);
42
extern void setHelpPrefixStr (const char* str);
43
44
45
//==================================================================================================
46
// Options is an abstract class that gives the interface for all types options:
47
48
49
class Option
50
{
51
 protected:
52
    const char* name;
53
    const char* description;
54
    const char* category;
55
    const char* type_name;
56
57
136476
    static vec<Option*>& getOptionList () { static vec<Option*> options; return options; }
58
    static const char*&  getUsageString() { static const char* usage_str; return usage_str; }
59
    static const char*&  getHelpPrefixString() { static const char* help_prefix_str = ""; return help_prefix_str; }
60
61
    struct OptionLt {
62
        bool operator()(const Option* x, const Option* y) {
63
            int test1 = strcmp(x->category, y->category);
64
            return test1 < 0 || (test1 == 0 && strcmp(x->type_name, y->type_name) < 0);
65
        }
66
    };
67
68
136476
    Option(const char* name_,
69
           const char* desc_,
70
           const char* cate_,
71
136476
           const char* type_) :
72
      name       (name_)
73
    , description(desc_)
74
    , category   (cate_)
75
136476
    , type_name  (type_)
76
    {
77
136476
        getOptionList().push(this);
78
136476
    }
79
80
 public:
81
136476
    virtual ~Option() {}
82
83
    virtual bool parse             (const char* str)      = 0;
84
    virtual void help              (bool verbose = false) = 0;
85
86
    friend  void parseOptions      (int& argc, char** argv, bool strict);
87
    friend  void printUsageAndExit (int  argc, char** argv, bool verbose);
88
    friend  void setUsageHelp      (const char* str);
89
    friend  void setHelpPrefixStr  (const char* str);
90
};
91
92
93
//==================================================================================================
94
// Range classes with specialization for floating types:
95
96
97
struct IntRange {
98
    int begin;
99
    int end;
100
45492
    IntRange(int b, int e) : begin(b), end(e) {}
101
};
102
103
struct Int64Range {
104
    int64_t begin;
105
    int64_t end;
106
    Int64Range(int64_t b, int64_t e) : begin(b), end(e) {}
107
};
108
109
struct DoubleRange {
110
    double begin;
111
    double end;
112
    bool  begin_inclusive;
113
    bool  end_inclusive;
114
53074
    DoubleRange(double b, bool binc, double e, bool einc) : begin(b), end(e), begin_inclusive(binc), end_inclusive(einc) {}
115
};
116
117
118
//==================================================================================================
119
// Double options:
120
121
122
53074
class DoubleOption : public Option
123
{
124
 protected:
125
    DoubleRange range;
126
    double      value;
127
128
 public:
129
53074
    DoubleOption(const char* c, const char* n, const char* d, double def = double(), DoubleRange r = DoubleRange(-HUGE_VAL, false, HUGE_VAL, false))
130
53074
        : Option(n, d, c, "<double>"), range(r), value(def) {
131
        // FIXME: set LC_NUMERIC to "C" to make sure that strtof/strtod parses decimal point correctly.
132
53074
    }
133
134
    operator      double   (void) const { return value; }
135
21
    operator      double&  (void)       { return value; }
136
    DoubleOption& operator=(double x)   { value = x; return *this; }
137
138
    bool parse(const char* str) override
139
    {
140
      const char* span = str;
141
142
      if (!match(span, "-") || !match(span, name) || !match(span, "="))
143
        return false;
144
145
      char* end;
146
      double tmp = strtod(span, &end);
147
148
      if (end == NULL)
149
        return false;
150
      else if (tmp >= range.end && (!range.end_inclusive || tmp != range.end))
151
      {
152
        fprintf(stderr,
153
                "ERROR! value <%s> is too large for option \"%s\".\n",
154
                span,
155
                name);
156
        exit(1);
157
      }
158
      else if (tmp <= range.begin
159
               && (!range.begin_inclusive || tmp != range.begin))
160
      {
161
        fprintf(stderr,
162
                "ERROR! value <%s> is too small for option \"%s\".\n",
163
                span,
164
                name);
165
        exit(1);
166
      }
167
168
      value = tmp;
169
      // fprintf(stderr, "READ VALUE: %g\n", value);
170
171
      return true;
172
    }
173
174
    void help(bool verbose = false) override
175
    {
176
      fprintf(stderr,
177
              "  -%-12s = %-8s %c%4.2g .. %4.2g%c (default: %g)\n",
178
              name,
179
              type_name,
180
              range.begin_inclusive ? '[' : '(',
181
              range.begin,
182
              range.end,
183
              range.end_inclusive ? ']' : ')',
184
              value);
185
      if (verbose)
186
      {
187
        fprintf(stderr, "\n        %s\n", description);
188
        fprintf(stderr, "\n");
189
      }
190
    }
191
};
192
193
194
//==================================================================================================
195
// Int options:
196
197
198
45492
class IntOption : public Option
199
{
200
 protected:
201
    IntRange range;
202
    int32_t  value;
203
204
 public:
205
45492
    IntOption(const char* c, const char* n, const char* d, int32_t def = int32_t(), IntRange r = IntRange(INT32_MIN, INT32_MAX))
206
45492
        : Option(n, d, c, "<int32>"), range(r), value(def) {}
207
208
    operator   int32_t   (void) const { return value; }
209
18
    operator   int32_t&  (void)       { return value; }
210
    IntOption& operator= (int32_t x)  { value = x; return *this; }
211
212
    bool parse(const char* str) override
213
    {
214
      const char* span = str;
215
216
      if (!match(span, "-") || !match(span, name) || !match(span, "="))
217
        return false;
218
219
      char* end;
220
      int32_t tmp = strtol(span, &end, 10);
221
222
      if (end == NULL)
223
        return false;
224
      else if (tmp > range.end)
225
      {
226
        fprintf(stderr,
227
                "ERROR! value <%s> is too large for option \"%s\".\n",
228
                span,
229
                name);
230
        exit(1);
231
      }
232
      else if (tmp < range.begin)
233
      {
234
        fprintf(stderr,
235
                "ERROR! value <%s> is too small for option \"%s\".\n",
236
                span,
237
                name);
238
        exit(1);
239
      }
240
241
      value = tmp;
242
243
      return true;
244
    }
245
246
    void help(bool verbose = false) override
247
    {
248
      fprintf(stderr, "  -%-12s = %-8s [", name, type_name);
249
      if (range.begin == INT32_MIN)
250
        fprintf(stderr, "imin");
251
      else
252
        fprintf(stderr, "%4d", range.begin);
253
254
      fprintf(stderr, " .. ");
255
      if (range.end == INT32_MAX)
256
        fprintf(stderr, "imax");
257
      else
258
        fprintf(stderr, "%4d", range.end);
259
260
      fprintf(stderr, "] (default: %d)\n", value);
261
      if (verbose)
262
      {
263
        fprintf(stderr, "\n        %s\n", description);
264
        fprintf(stderr, "\n");
265
      }
266
    }
267
};
268
269
270
// Leave this out for visual C++ until Microsoft implements C99 and gets support for strtoll.
271
#ifndef _MSC_VER
272
273
class Int64Option : public Option
274
{
275
 protected:
276
    Int64Range range;
277
    int64_t  value;
278
279
 public:
280
    Int64Option(const char* c, const char* n, const char* d, int64_t def = int64_t(), Int64Range r = Int64Range(INT64_MIN, INT64_MAX))
281
        : Option(n, d, c, "<int64>"), range(r), value(def) {}
282
283
    operator     int64_t   (void) const { return value; }
284
    operator     int64_t&  (void)       { return value; }
285
    Int64Option& operator= (int64_t x)  { value = x; return *this; }
286
287
    bool parse(const char* str) override
288
    {
289
      const char* span = str;
290
291
      if (!match(span, "-") || !match(span, name) || !match(span, "="))
292
        return false;
293
294
      char* end;
295
      int64_t tmp = strtoll(span, &end, 10);
296
297
      if (end == NULL)
298
        return false;
299
      else if (tmp > range.end)
300
      {
301
        fprintf(stderr,
302
                "ERROR! value <%s> is too large for option \"%s\".\n",
303
                span,
304
                name);
305
        exit(1);
306
      }
307
      else if (tmp < range.begin)
308
      {
309
        fprintf(stderr,
310
                "ERROR! value <%s> is too small for option \"%s\".\n",
311
                span,
312
                name);
313
        exit(1);
314
      }
315
316
      value = tmp;
317
318
      return true;
319
    }
320
321
    void help(bool verbose = false) override
322
    {
323
      fprintf(stderr, "  -%-12s = %-8s [", name, type_name);
324
      if (range.begin == INT64_MIN)
325
        fprintf(stderr, "imin");
326
      else
327
        fprintf(stderr, "%4" PRIi64, range.begin);
328
329
      fprintf(stderr, " .. ");
330
      if (range.end == INT64_MAX)
331
        fprintf(stderr, "imax");
332
      else
333
        fprintf(stderr, "%4" PRIi64, range.end);
334
335
      fprintf(stderr, "] (default: %" PRIi64 ")\n", value);
336
      if (verbose)
337
      {
338
        fprintf(stderr, "\n        %s\n", description);
339
        fprintf(stderr, "\n");
340
      }
341
    }
342
};
343
#endif
344
345
//==================================================================================================
346
// String option:
347
348
349
class StringOption : public Option
350
{
351
    const char* value;
352
 public:
353
    StringOption(const char* c, const char* n, const char* d, const char* def = NULL)
354
        : Option(n, d, c, "<string>"), value(def) {}
355
356
    operator      const char*  (void) const     { return value; }
357
    operator      const char*& (void)           { return value; }
358
    StringOption& operator=    (const char* x)  { value = x; return *this; }
359
360
    bool parse(const char* str) override
361
    {
362
      const char* span = str;
363
364
      if (!match(span, "-") || !match(span, name) || !match(span, "="))
365
        return false;
366
367
      value = span;
368
      return true;
369
    }
370
371
    void help(bool verbose = false) override
372
    {
373
      fprintf(stderr, "  -%-10s = %8s\n", name, type_name);
374
      if (verbose)
375
      {
376
        fprintf(stderr, "\n        %s\n", description);
377
        fprintf(stderr, "\n");
378
      }
379
    }
380
};
381
382
383
//==================================================================================================
384
// Bool option:
385
386
387
37910
class BoolOption : public Option
388
{
389
    bool value;
390
391
 public:
392
37910
    BoolOption(const char* c, const char* n, const char* d, bool v)
393
37910
        : Option(n, d, c, "<bool>"), value(v) {}
394
395
    operator    bool     (void) const { return value; }
396
15
    operator    bool&    (void)       { return value; }
397
    BoolOption& operator=(bool b)     { value = b; return *this; }
398
399
    bool parse(const char* str) override
400
    {
401
      const char* span = str;
402
403
      if (match(span, "-"))
404
      {
405
        bool b = !match(span, "no-");
406
407
        if (strcmp(span, name) == 0)
408
        {
409
          value = b;
410
          return true;
411
        }
412
      }
413
414
      return false;
415
    }
416
417
    void help(bool verbose = false) override
418
    {
419
      fprintf(stderr, "  -%s, -no-%s", name, name);
420
421
      for (uint32_t i = 0; i < 32 - strlen(name) * 2; i++) fprintf(stderr, " ");
422
423
      fprintf(stderr, " ");
424
      fprintf(stderr, "(default: %s)\n", value ? "on" : "off");
425
      if (verbose)
426
      {
427
        fprintf(stderr, "\n        %s\n", description);
428
        fprintf(stderr, "\n");
429
      }
430
    }
431
};
432
433
//=================================================================================================
434
}  // namespace BVMinisat
435
}  // namespace cvc5
436
437
#endif