Branch data Line data Source code
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 Minisat_Options_h
21 : : #define Minisat_Options_h
22 : :
23 : : #include <stdlib.h>
24 : : #include <stdio.h>
25 : : #include <math.h>
26 : : #include <string.h>
27 : :
28 : : #include "prop/minisat/mtl/IntTypes.h"
29 : : #include "prop/minisat/mtl/Vec.h"
30 : : #include "prop/minisat/utils/ParseUtils.h"
31 : :
32 : : namespace cvc5::internal {
33 : : namespace Minisat {
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 [ + + ][ + - ]: 496400 : 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 : 496400 : Option(const char* name_,
69 : : const char* desc_,
70 : : const char* cate_,
71 : 496400 : const char* type_) :
72 : : name (name_)
73 : : , description(desc_)
74 : : , category (cate_)
75 : 496400 : , type_name (type_)
76 : : {
77 : 496400 : getOptionList().push(this);
78 : 496400 : }
79 : :
80 : : public:
81 : 496400 : 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 : 175200 : 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 : 204400 : 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 : 204400 : DoubleOption(const char* c, const char* n, const char* d, double def = double(), DoubleRange r = DoubleRange(-HUGE_VAL, false, HUGE_VAL, false))
130 : 204400 : : 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 : 204400 : }
133 : :
134 : : operator double (void) const { return value; }
135 : 356930 : operator double& (void) { return value; }
136 : : DoubleOption& operator=(double x) { value = x; return *this; }
137 : :
138 : 0 : bool parse(const char* str) override
139 : : {
140 : 0 : const char* span = str;
141 : :
142 [ - - ][ - - ]: 0 : if (!match(span, "-") || !match(span, name) || !match(span, "="))
[ - - ][ - - ]
143 : 0 : return false;
144 : :
145 : : char* end;
146 : 0 : double tmp = strtod(span, &end);
147 : :
148 [ - - ]: 0 : if (end == NULL)
149 : 0 : return false;
150 [ - - ][ - - ]: 0 : else if (tmp >= range.end && (!range.end_inclusive || tmp != range.end))
[ - - ]
151 : : {
152 : 0 : fprintf(stderr,
153 : : "ERROR! value <%s> is too large for option \"%s\".\n",
154 : : span,
155 : : name);
156 : 0 : exit(1);
157 : : }
158 [ - - ]: 0 : else if (tmp <= range.begin
159 [ - - ][ - - ]: 0 : && (!range.begin_inclusive || tmp != range.begin))
160 : : {
161 : 0 : fprintf(stderr,
162 : : "ERROR! value <%s> is too small for option \"%s\".\n",
163 : : span,
164 : : name);
165 : 0 : exit(1);
166 : : }
167 : :
168 : 0 : value = tmp;
169 : : // fprintf(stderr, "READ VALUE: %g\n", value);
170 : :
171 : 0 : return true;
172 : : }
173 : :
174 : 0 : void help(bool verbose = false) override
175 : : {
176 : 0 : fprintf(stderr,
177 : : " -%-12s = %-8s %c%4.2g .. %4.2g%c (default: %g)\n",
178 : : name,
179 : : type_name,
180 [ - - ]: 0 : range.begin_inclusive ? '[' : '(',
181 : : range.begin,
182 : : range.end,
183 [ - - ]: 0 : range.end_inclusive ? ']' : ')',
184 : : value);
185 [ - - ]: 0 : if (verbose)
186 : : {
187 : 0 : fprintf(stderr, "\n %s\n", description);
188 : 0 : fprintf(stderr, "\n");
189 : : }
190 : 0 : }
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 : 175200 : IntOption(const char* c, const char* n, const char* d, int32_t def = int32_t(), IntRange r = IntRange(INT32_MIN, INT32_MAX))
206 : 175200 : : Option(n, d, c, "<int32>"), range(r), value(def) {}
207 : :
208 : : operator int32_t (void) const { return value; }
209 : 305940 : operator int32_t& (void) { return value; }
210 : : IntOption& operator= (int32_t x) { value = x; return *this; }
211 : :
212 : 0 : bool parse(const char* str) override
213 : : {
214 : 0 : const char* span = str;
215 : :
216 [ - - ][ - - ]: 0 : if (!match(span, "-") || !match(span, name) || !match(span, "="))
[ - - ][ - - ]
217 : 0 : return false;
218 : :
219 : : char* end;
220 : 0 : int32_t tmp = strtol(span, &end, 10);
221 : :
222 [ - - ]: 0 : if (end == NULL)
223 : 0 : return false;
224 [ - - ]: 0 : else if (tmp > range.end)
225 : : {
226 : 0 : fprintf(stderr,
227 : : "ERROR! value <%s> is too large for option \"%s\".\n",
228 : : span,
229 : : name);
230 : 0 : exit(1);
231 : : }
232 [ - - ]: 0 : else if (tmp < range.begin)
233 : : {
234 : 0 : fprintf(stderr,
235 : : "ERROR! value <%s> is too small for option \"%s\".\n",
236 : : span,
237 : : name);
238 : 0 : exit(1);
239 : : }
240 : :
241 : 0 : value = tmp;
242 : :
243 : 0 : return true;
244 : : }
245 : :
246 : 0 : void help(bool verbose = false) override
247 : : {
248 : 0 : fprintf(stderr, " -%-12s = %-8s [", name, type_name);
249 [ - - ]: 0 : if (range.begin == INT32_MIN)
250 : 0 : fprintf(stderr, "imin");
251 : : else
252 : 0 : fprintf(stderr, "%4d", range.begin);
253 : :
254 : 0 : fprintf(stderr, " .. ");
255 [ - - ]: 0 : if (range.end == INT32_MAX)
256 : 0 : fprintf(stderr, "imax");
257 : : else
258 : 0 : fprintf(stderr, "%4d", range.end);
259 : :
260 : 0 : fprintf(stderr, "] (default: %d)\n", value);
261 [ - - ]: 0 : if (verbose)
262 : : {
263 : 0 : fprintf(stderr, "\n %s\n", description);
264 : 0 : fprintf(stderr, "\n");
265 : : }
266 : 0 : }
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 : 116800 : BoolOption(const char* c, const char* n, const char* d, bool v)
393 : 116800 : : Option(n, d, c, "<bool>"), value(v) {}
394 : :
395 : : operator bool (void) const { return value; }
396 : 203960 : operator bool& (void) { return value; }
397 : : BoolOption& operator=(bool b) { value = b; return *this; }
398 : :
399 : 0 : bool parse(const char* str) override
400 : : {
401 : 0 : const char* span = str;
402 : :
403 [ - - ]: 0 : if (match(span, "-"))
404 : : {
405 : 0 : bool b = !match(span, "no-");
406 : :
407 [ - - ]: 0 : if (strcmp(span, name) == 0)
408 : : {
409 : 0 : value = b;
410 : 0 : return true;
411 : : }
412 : : }
413 : :
414 : 0 : return false;
415 : : }
416 : :
417 : 0 : void help(bool verbose = false) override
418 : : {
419 : 0 : fprintf(stderr, " -%s, -no-%s", name, name);
420 : :
421 [ - - ]: 0 : for (uint32_t i = 0; i < 32 - strlen(name) * 2; i++) fprintf(stderr, " ");
422 : :
423 : 0 : fprintf(stderr, " ");
424 [ - - ]: 0 : fprintf(stderr, "(default: %s)\n", value ? "on" : "off");
425 [ - - ]: 0 : if (verbose)
426 : : {
427 : 0 : fprintf(stderr, "\n %s\n", description);
428 : 0 : fprintf(stderr, "\n");
429 : : }
430 : 0 : }
431 : : };
432 : :
433 : : //=================================================================================================
434 : : }
435 : : } // namespace cvc5::internal
436 : :
437 : : #endif
|
