SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Options.h
Go to the documentation of this file.
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 "IntTypes.h"
29 #include "Vec.h"
30 
31 namespace Minisat
32 {
33  //==================================================================================================
34  // Top-level option help functions:
35 
36  extern void printUsageAndExit( int argc, char** argv, bool verbose = false );
37  extern void setUsageHelp( const char* str );
38  extern void setHelpPrefixStr( const char* str );
39 
40  //==================================================================================================
41  // Options is an abstract class that gives the interface for all types options:
42 
43  class Option
44  {
45  protected:
46  const char* name;
47  const char* description;
48  const char* category;
49  const char* type_name;
50 
52  {
53  static vec<Option*> options;
54  return options;
55  }
56 
57  static const char*& getUsageString()
58  {
59  static const char* usage_str;
60  return usage_str;
61  }
62 
63  static const char*& getHelpPrefixString()
64  {
65  static const char* help_prefix_str = "";
66  return help_prefix_str;
67  }
68 
69  struct OptionLt
70  {
71  bool operator ()( const Option* x, const Option* y )
72  {
73  int test1 = strcmp( x->category, y->category );
74  return (test1 < 0 || (test1 == 0 && strcmp( x->type_name, y->type_name ) < 0));
75  }
76  };
77 
78  Option( const char* name_, const char* desc_, const char* cate_, const char* type_ ):
79  name( name_ ),
80  description( desc_ ),
81  category( cate_ ),
82  type_name( type_ )
83  {
84  getOptionList().push( this );
85  }
86 
87  public:
88  virtual ~Option(){}
89 
90  virtual void help( bool verbose = false ) = 0;
91 
92  friend void printUsageAndExit( int argc, char** argv, bool verbose );
93  friend void setUsageHelp( const char* str );
94  friend void setHelpPrefixStr( const char* str );
95  };
96 
97  //==================================================================================================
98  // Range classes with specialization for floating types:
99 
100  struct IntRange
101  {
102  int begin;
103  int end;
104 
105  IntRange( int b, int e ):
106  begin( b ),
107  end( e )
108  {}
109  };
110 
111  struct Int64Range
112  {
113  int64_t begin;
114  int64_t end;
115 
116  Int64Range( int64_t b, int64_t e ):
117  begin( b ),
118  end( e )
119  {}
120  };
121 
122  struct DoubleRange
123  {
124  double begin;
125  double end;
128 
129  DoubleRange( double b, bool binc, double e, bool einc ):
130  begin( b ),
131  end( e ),
132  begin_inclusive( binc ),
133  end_inclusive( einc )
134  {}
135  };
136 
137  //==================================================================================================
138  // Double options:
139 
141  public Option
142  {
143  protected:
145  double value;
146 
147  public:
148  DoubleOption( const char* c,
149  const char* n,
150  const char* d,
151  double def = double(),
152  DoubleRange r = DoubleRange( -HUGE_VAL, false, HUGE_VAL, false ) ):
153  Option( n,
154  d,
155  c,
156  "<double>" ),
157  range( r ),
158  value( def )
159  {
160  // FIXME: set LC_NUMERIC to "C" to make sure that strtof/strtod parses decimal point correctly.
161  }
162 
163  operator double( void ) const
164  {
165  return value;
166  }
167 
169  {
170  value = x;
171  return *this;
172  }
173 
174  virtual void help( bool verbose = false )
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  // Int options:
195 
196  class IntOption:
197  public Option
198  {
199  protected:
201  int32_t value;
202 
203  public:
204  IntOption( const char* c, const char* n, const char* d, int32_t def = int32_t(), IntRange r = IntRange( INT_MIN, INT_MAX ) ):
205  Option( n, d, c, "<int32>" ),
206  range( r ),
207  value( def )
208  {}
209 
210  operator int32_t( void ) const
211  {
212  return value;
213  }
214 
215  IntOption& operator = ( int32_t x )
216  {
217  value = x;
218  return *this;
219  }
220 
221  virtual void help( bool verbose = false )
222  {
223  fprintf( stderr, " -%-12s = %-8s [", name, type_name );
224  if( range.begin == INT_MIN )
225  fprintf( stderr, "imin" );
226  else
227  fprintf( stderr, "%4d", range.begin );
228 
229  fprintf( stderr, " .. " );
230  if( range.end == INT_MAX )
231  fprintf( stderr, "imax" );
232  else
233  fprintf( stderr, "%4d", range.end );
234 
235  fprintf( stderr, "] (default: %d)\n", value );
236  if( verbose )
237  {
238  fprintf( stderr, "\n %s\n", description );
239  fprintf( stderr, "\n" );
240  }
241  }
242  };
243 
244  //==================================================================================================
245  // String option:
246 
248  public Option
249  {
250  const char* value;
251 
252  public:
253  StringOption( const char* c, const char* n, const char* d, const char* def = NULL ):
254  Option( n, d, c, "<string>" ),
255  value( def )
256  {}
257 
258  operator const char*( void ) const
259  {
260  return value;
261  }
262 
263  StringOption& operator = ( const char* x )
264  {
265  value = x;
266  return *this;
267  }
268 
269  virtual void help( bool verbose = false )
270  {
271  fprintf( stderr, " -%-10s = %8s\n", name, type_name );
272  if( verbose )
273  {
274  fprintf( stderr, "\n %s\n", description );
275  fprintf( stderr, "\n" );
276  }
277  }
278  };
279 
280  //==================================================================================================
281  // Bool option:
282 
283  class BoolOption:
284  public Option
285  {
286  bool value;
287 
288  public:
289  BoolOption( const char* c, const char* n, const char* d, bool v ):
290  Option( n, d, c, "<bool>" ),
291  value( v )
292  {}
293 
294  operator bool( void ) const
295  {
296  return value;
297  }
298 
300  {
301  value = b;
302  return *this;
303  }
304 
305  virtual void help( bool verbose = false )
306  {
307  fprintf( stderr, " -%s, -no-%s", name, name );
308 
309  for( uint32_t i = 0; i < 32 - strlen( name ) * 2; i++ )
310  fprintf( stderr, " " );
311 
312  fprintf( stderr, " " );
313  fprintf( stderr, "(default: %s)\n", value ? "on" : "off" );
314  if( verbose )
315  {
316  fprintf( stderr, "\n %s\n", description );
317  fprintf( stderr, "\n" );
318  }
319  }
320  };
321 
322  //=================================================================================================
323 }
324 
325 #endif
BoolOption(const char *c, const char *n, const char *d, bool v)
Definition: Options.h:289
virtual void help(bool verbose=false)
Definition: Options.h:305
BoolOption & operator=(bool b)
Definition: Options.h:299
DoubleRange range
Definition: Options.h:144
virtual void help(bool verbose=false)
Definition: Options.h:174
DoubleOption & operator=(double x)
Definition: Options.h:168
DoubleOption(const char *c, const char *n, const char *d, double def=double(), DoubleRange r=DoubleRange(-HUGE_VAL, false, HUGE_VAL, false))
Definition: Options.h:148
IntOption(const char *c, const char *n, const char *d, int32_t def=int32_t(), IntRange r=IntRange(INT_MIN, INT_MAX))
Definition: Options.h:204
IntOption & operator=(int32_t x)
Definition: Options.h:215
virtual void help(bool verbose=false)
Definition: Options.h:221
IntRange range
Definition: Options.h:200
static const char *& getHelpPrefixString()
Definition: Options.h:63
static vec< Option * > & getOptionList()
Definition: Options.h:51
const char * name
Definition: Options.h:46
virtual void help(bool verbose=false)=0
Option(const char *name_, const char *desc_, const char *cate_, const char *type_)
Definition: Options.h:78
const char * category
Definition: Options.h:48
friend void printUsageAndExit(int argc, char **argv, bool verbose)
const char * type_name
Definition: Options.h:49
static const char *& getUsageString()
Definition: Options.h:57
const char * description
Definition: Options.h:47
virtual ~Option()
Definition: Options.h:88
friend void setHelpPrefixStr(const char *str)
friend void setUsageHelp(const char *str)
const char * value
Definition: Options.h:250
StringOption & operator=(const char *x)
Definition: Options.h:263
virtual void help(bool verbose=false)
Definition: Options.h:269
StringOption(const char *c, const char *n, const char *d, const char *def=NULL)
Definition: Options.h:253
Definition: Alg.h:27
void setUsageHelp(const char *str)
Definition: Options.cpp:25
void printUsageAndExit(int argc, char **argv, bool verbose=false)
Definition: Options.cpp:35
void setHelpPrefixStr(const char *str)
Definition: Options.cpp:30
DoubleRange(double b, bool binc, double e, bool einc)
Definition: Options.h:129
Int64Range(int64_t b, int64_t e)
Definition: Options.h:116
IntRange(int b, int e)
Definition: Options.h:105
bool operator()(const Option *x, const Option *y)
Definition: Options.h:71