src/prop/bvminisat/utils/Options.h

   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     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     Option(const char* name_,
  69            const char* desc_,
  70            const char* cate_,
  71            const char* type_) :
  72       name       (name_)
  73     , description(desc_)
  74     , category   (cate_)
  75     , type_name  (type_)
  76     {
  77         getOptionList().push(this);
  78     }
  79
  80  public:
  81     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     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     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 class DoubleOption : public Option
 123 {
 124  protected:
 125     DoubleRange range;
 126     double      value;
 127
 128  public:
 129     DoubleOption(const char* c, const char* n, const char* d, double def = double(), DoubleRange r = DoubleRange(-HUGE_VAL, false, HUGE_VAL, false))
 130         : 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     }
 133
 134     operator      double   (void) const { return value; }
 135     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 class IntOption : public Option
 199 {
 200  protected:
 201     IntRange range;
 202     int32_t  value;
 203
 204  public:
 205     IntOption(const char* c, const char* n, const char* d, int32_t def = int32_t(), IntRange r = IntRange(INT32_MIN, INT32_MAX))
 206         : Option(n, d, c, "<int32>"), range(r), value(def) {}
 207
 208     operator   int32_t   (void) const { return value; }
 209     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 class BoolOption : public Option
 388 {
 389     bool value;
 390
 391  public:
 392     BoolOption(const char* c, const char* n, const char* d, bool v)
 393         : Option(n, d, c, "<bool>"), value(v) {}
 394
 395     operator    bool     (void) const { return value; }
 396     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