Add incremental solver class
[satlib.git] / glucose-syrup / 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 Glucose_Options_h
21 #define Glucose_Options_h
22
23 #include <stdlib.h>
24 #include <stdio.h>
25 #include <math.h>
26 #include <string.h>
27
28 #include "mtl/IntTypes.h"
29 #include "mtl/Vec.h"
30 #include "utils/ParseUtils.h"
31
32 namespace Glucose {
33
34 //==================================================================================================
35 // Top-level option parse/help functions:
36
37
38 extern void parseOptions     (int& argc, char** argv, bool strict = false);
39 extern void printUsageAndExit(int  argc, char** argv, bool verbose = false);
40 extern void setUsageHelp     (const char* str);
41 extern void setHelpPrefixStr (const char* str);
42
43
44 //==================================================================================================
45 // Options is an abstract class that gives the interface for all types options:
46
47
48 class Option
49 {
50  protected:
51     const char* name;
52     const char* description;
53     const char* category;
54     const char* type_name;
55
56     static vec<Option*>& getOptionList () { static vec<Option*> options; return options; }
57     static const char*&  getUsageString() { static const char* usage_str; return usage_str; }
58     static const char*&  getHelpPrefixString() { static const char* help_prefix_str = ""; return help_prefix_str; }
59
60     struct OptionLt {
61         bool operator()(const Option* x, const Option* y) {
62             int test1 = strcmp(x->category, y->category);
63             return test1 < 0 || test1 == 0 && strcmp(x->type_name, y->type_name) < 0;
64         }
65     };
66
67     Option(const char* name_, 
68            const char* desc_,
69            const char* cate_,
70            const char* type_) : 
71       name       (name_)
72     , description(desc_)
73     , category   (cate_)
74     , type_name  (type_)
75     { 
76         getOptionList().push(this); 
77     }
78
79  public:
80     virtual ~Option() {}
81
82     virtual bool parse             (const char* str)      = 0;
83     virtual void help              (bool verbose = false) = 0;
84
85     friend  void parseOptions      (int& argc, char** argv, bool strict);
86     friend  void printUsageAndExit (int  argc, char** argv, bool verbose);
87     friend  void setUsageHelp      (const char* str);
88     friend  void setHelpPrefixStr  (const char* str);
89 };
90
91
92 //==================================================================================================
93 // Range classes with specialization for floating types:
94
95
96 struct IntRange {
97     int begin;
98     int end;
99     IntRange(int b, int e) : begin(b), end(e) {}
100 };
101
102 struct Int64Range {
103     int64_t begin;
104     int64_t end;
105     Int64Range(int64_t b, int64_t e) : begin(b), end(e) {}
106 };
107
108 struct DoubleRange {
109     double begin;
110     double end;
111     bool  begin_inclusive;
112     bool  end_inclusive;
113     DoubleRange(double b, bool binc, double e, bool einc) : begin(b), end(e), begin_inclusive(binc), end_inclusive(einc) {}
114 };
115
116
117 //==================================================================================================
118 // Double options:
119
120
121 class DoubleOption : public Option
122 {
123  protected:
124     DoubleRange range;
125     double      value;
126
127  public:
128     DoubleOption(const char* c, const char* n, const char* d, double def = double(), DoubleRange r = DoubleRange(-HUGE_VAL, false, HUGE_VAL, false))
129         : Option(n, d, c, "<double>"), range(r), value(def) {
130         // FIXME: set LC_NUMERIC to "C" to make sure that strtof/strtod parses decimal point correctly.
131     }
132
133     operator      double   (void) const { return value; }
134     operator      double&  (void)       { return value; }
135     DoubleOption& operator=(double x)   { value = x; return *this; }
136
137     virtual bool parse(const char* str){
138         const char* span = str; 
139
140         if (!match(span, "-") || !match(span, name) || !match(span, "="))
141             return false;
142
143         char*  end;
144         double tmp = strtod(span, &end);
145
146         if (end == NULL) 
147             return false;
148         else if (tmp >= range.end && (!range.end_inclusive || tmp != range.end)){
149             fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name);
150             exit(1);
151         }else if (tmp <= range.begin && (!range.begin_inclusive || tmp != range.begin)){
152             fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name);
153             exit(1); }
154
155         value = tmp;
156         // fprintf(stderr, "READ VALUE: %g\n", value);
157
158         return true;
159     }
160
161     virtual void help (bool verbose = false){
162         fprintf(stderr, "  -%-12s = %-8s %c%4.2g .. %4.2g%c (default: %g)\n", 
163                 name, type_name, 
164                 range.begin_inclusive ? '[' : '(', 
165                 range.begin,
166                 range.end,
167                 range.end_inclusive ? ']' : ')', 
168                 value);
169         if (verbose){
170             fprintf(stderr, "\n        %s\n", description);
171             fprintf(stderr, "\n");
172         }
173     }
174 };
175
176
177 //==================================================================================================
178 // Int options:
179
180
181 class IntOption : public Option
182 {
183  protected:
184     IntRange range;
185     int32_t  value;
186
187  public:
188     IntOption(const char* c, const char* n, const char* d, int32_t def = int32_t(), IntRange r = IntRange(INT32_MIN, INT32_MAX))
189         : Option(n, d, c, "<int32>"), range(r), value(def) {}
190  
191     operator   int32_t   (void) const { return value; }
192     operator   int32_t&  (void)       { return value; }
193     IntOption& operator= (int32_t x)  { value = x; return *this; }
194
195     virtual bool parse(const char* str){
196         const char* span = str; 
197
198         if (!match(span, "-") || !match(span, name) || !match(span, "="))
199             return false;
200
201         char*   end;
202         int32_t tmp = strtol(span, &end, 10);
203
204         if (end == NULL) 
205             return false;
206         else if (tmp > range.end){
207             fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name);
208             exit(1);
209         }else if (tmp < range.begin){
210             fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name);
211             exit(1); }
212
213         value = tmp;
214
215         return true;
216     }
217
218     virtual void help (bool verbose = false){
219         fprintf(stderr, "  -%-12s = %-8s [", name, type_name);
220         if (range.begin == INT32_MIN)
221             fprintf(stderr, "imin");
222         else
223             fprintf(stderr, "%4d", range.begin);
224
225         fprintf(stderr, " .. ");
226         if (range.end == INT32_MAX)
227             fprintf(stderr, "imax");
228         else
229             fprintf(stderr, "%4d", range.end);
230
231         fprintf(stderr, "] (default: %d)\n", value);
232         if (verbose){
233             fprintf(stderr, "\n        %s\n", description);
234             fprintf(stderr, "\n");
235         }
236     }
237 };
238
239
240 // Leave this out for visual C++ until Microsoft implements C99 and gets support for strtoll.
241 #ifndef _MSC_VER
242
243 class Int64Option : public Option
244 {
245  protected:
246     Int64Range range;
247     int64_t  value;
248
249  public:
250     Int64Option(const char* c, const char* n, const char* d, int64_t def = int64_t(), Int64Range r = Int64Range(INT64_MIN, INT64_MAX))
251         : Option(n, d, c, "<int64>"), range(r), value(def) {}
252  
253     operator     int64_t   (void) const { return value; }
254     operator     int64_t&  (void)       { return value; }
255     Int64Option& operator= (int64_t x)  { value = x; return *this; }
256
257     virtual bool parse(const char* str){
258         const char* span = str; 
259
260         if (!match(span, "-") || !match(span, name) || !match(span, "="))
261             return false;
262
263         char*   end;
264         int64_t tmp = strtoll(span, &end, 10);
265
266         if (end == NULL) 
267             return false;
268         else if (tmp > range.end){
269             fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name);
270             exit(1);
271         }else if (tmp < range.begin){
272             fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name);
273             exit(1); }
274
275         value = tmp;
276
277         return true;
278     }
279
280     virtual void help (bool verbose = false){
281         fprintf(stderr, "  -%-12s = %-8s [", name, type_name);
282         if (range.begin == INT64_MIN)
283             fprintf(stderr, "imin");
284         else
285             fprintf(stderr, "%4" PRIi64, range.begin);
286
287         fprintf(stderr, " .. ");
288         if (range.end == INT64_MAX)
289             fprintf(stderr, "imax");
290         else
291             fprintf(stderr, "%4" PRIi64, range.end);
292
293         fprintf(stderr, "] (default: %" PRIi64")\n", value);
294         if (verbose){
295             fprintf(stderr, "\n        %s\n", description);
296             fprintf(stderr, "\n");
297         }
298     }
299 };
300 #endif
301
302 //==================================================================================================
303 // String option:
304
305
306 class StringOption : public Option
307 {
308     const char* value;
309  public:
310     StringOption(const char* c, const char* n, const char* d, const char* def = NULL) 
311         : Option(n, d, c, "<string>"), value(def) {}
312
313     operator      const char*  (void) const     { return value; }
314     operator      const char*& (void)           { return value; }
315     StringOption& operator=    (const char* x)  { value = x; return *this; }
316
317     virtual bool parse(const char* str){
318         const char* span = str; 
319
320         if (!match(span, "-") || !match(span, name) || !match(span, "="))
321             return false;
322
323         value = span;
324         return true;
325     }
326
327     virtual void help (bool verbose = false){
328         fprintf(stderr, "  -%-10s = %8s\n", name, type_name);
329         if (verbose){
330             fprintf(stderr, "\n        %s\n", description);
331             fprintf(stderr, "\n");
332         }
333     }    
334 };
335
336
337 //==================================================================================================
338 // Bool option:
339
340
341 class BoolOption : public Option
342 {
343     bool value;
344
345  public:
346     BoolOption(const char* c, const char* n, const char* d, bool v) 
347         : Option(n, d, c, "<bool>"), value(v) {}
348
349     operator    bool     (void) const { return value; }
350     operator    bool&    (void)       { return value; }
351     BoolOption& operator=(bool b)     { value = b; return *this; }
352
353     virtual bool parse(const char* str){
354         const char* span = str; 
355         
356         if (match(span, "-")){
357             bool b = !match(span, "no-");
358
359             if (strcmp(span, name) == 0){
360                 value = b;
361                 return true; }
362         }
363
364         return false;
365     }
366
367     virtual void help (bool verbose = false){
368
369         fprintf(stderr, "  -%s, -no-%s", name, name);
370
371         for (uint32_t i = 0; i < 32 - strlen(name)*2; i++)
372             fprintf(stderr, " ");
373
374         fprintf(stderr, " ");
375         fprintf(stderr, "(default: %s)\n", value ? "on" : "off");
376         if (verbose){
377             fprintf(stderr, "\n        %s\n", description);
378             fprintf(stderr, "\n");
379         }
380     }
381 };
382
383 //=================================================================================================
384 }
385
386 #endif