CaDiCaL::Options Class Reference

#include <options.hpp>

Public Types
typedef Option *	iterator
typedef const Option *	const_iterator

Public Member Functions
	Options (Internal *)
OPTIONS int &	val (size_t idx)
bool	set (const char *name, int)
int	get (const char *name)
void	print ()
void	optimize (int val)
void	copy (Options &other) const

Static Public Member Functions
static Option *	has (const char *name)
static void	usage ()
static bool	is_preprocessing_option (const char *name)
static bool	parse_long_option (const char *, string &, int &)
static iterator	begin ()
static iterator	end ()

Static Public Attributes
static int	reportdefault

Friends
struct	Option

Detailed Description

Definition at line 315 of file options.hpp.

Member Typedef Documentation

const_iterator

typedef const Option* CaDiCaL::Options::const_iterator

Definition at line 404 of file options.hpp.

iterator

typedef Option* CaDiCaL::Options::iterator

Definition at line 403 of file options.hpp.

Constructor & Destructor Documentation

Options()

CaDiCaL::Options::Options

(

Internal *

s

)

Definition at line 108 of file cadical_options.cpp.

                             : internal (s) {
  CADICAL_assert (number_of_options == sizeof Options::table / sizeof (Option));
 
  // First initialize them according to defaults in 'options.hpp'.
  //
  const char *prev = "";
  size_t i = 0;
#define OPTION(N, V, L, H, O, P, R, D) \
  do { \
    if ((L) > (V)) \
      FATAL ("'" #N "' default '" #V "' " \
             "lower minimum '" #L "' in 'options.hpp'"); \
    if ((H) < (V)) \
      FATAL ("'" #N "' default '" #V "' " \
             "larger maximum '" #H "' in 'options.hpp'"); \
    if (strcmp (prev, #N) > 0) \
      FATAL ("'%s' ordered before '" #N "' in 'options.hpp'", prev); \
    N = (int) (V); \
    CADICAL_assert (&val (i) == &N); \
    /* The order of initializing static data is undefined and thus */ \
    /* it might be the case that the 'table' is not initialized yet. */ \
    /* Thus this construction just reinitializes the table too even */ \
    /* though it might not be necessary. */ \
    CADICAL_assert (!table[i].name || !strcmp (table[i].name, #N)); \
    table[i] = {#N,        (int) (V),  (int) (L), (int) (H), \
                (int) (O), (bool) (P), D}; \
    prev = #N; \
    i++; \
  } while (0);
  OPTIONS
#undef OPTION
 
  // Check consistency in debugging mode.
  //
#ifndef CADICAL_NDEBUG
  CADICAL_assert (i == number_of_options);
  CADICAL_assert (!has ("aaaaa"));
  CADICAL_assert (!has ("non-existing-option"));
  CADICAL_assert (!has ("zzzzz"));
#endif
 
  // Now overwrite default options with environment values.
  //
#define OPTION(N, V, L, H, O, P, R, D) \
  initialize_from_environment (N, #N, L, H);
  OPTIONS
#undef OPTION
}

Here is the call graph for this function:

Here is the caller graph for this function:

Member Function Documentation

begin()

static iterator CaDiCaL::Options::begin ( )

inlinestatic

Definition at line 406 of file options.hpp.

{ return table; }

copy()

void CaDiCaL::Options::copy

(

Options &

other

)

const

Definition at line 348 of file cadical_options.cpp.

                                        {
#ifdef LOGGING
  Internal *internal = other.internal;
#endif
#define OPTION(N, V, L, H, O, P, R, D) \
  if ((N) == (int) (V)) \
    LOG ("keeping non default option '--%s=%s'", #N, #V); \
  else if ((N) != (int) (V)) { \
    LOG ("overwriting default option by '--%s=%d'", #N, N); \
    other.N = N; \
  }
  OPTIONS
#undef OPTION
}

Here is the call graph for this function:

end()

static iterator CaDiCaL::Options::end ( )

inlinestatic

Definition at line 407 of file options.hpp.

{ return table + number_of_options; }

get()

int CaDiCaL::Options::get

(

const char *

name

)

Definition at line 191 of file cadical_options.cpp.

                                  {
  Option *o = has (name);
  return o ? o->val (this) : 0;
}

Here is the call graph for this function:

has()

Option * CaDiCaL::Options::has ( const char * name )

static

Definition at line 42 of file cadical_options.cpp.

                                      {
  size_t l = 0, r = number_of_options;
  while (l < r) {
    size_t m = l + (r - l) / 2;
    Option *res = &table[m];
    int tmp = strcmp (name, res->name);
    if (!tmp)
      return res;
    if (tmp < 0)
      r = m;
    if (tmp > 0)
      l = m + 1;
  }
  return 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

is_preprocessing_option()

bool CaDiCaL::Options::is_preprocessing_option ( const char * name )

static

Definition at line 319 of file cadical_options.cpp.

                                                       {
  Option *o = has (name);
  return o ? o->preprocessing : false;
}

Here is the call graph for this function:

Here is the caller graph for this function:

optimize()

void CaDiCaL::Options::optimize

(

int

val

)

Definition at line 250 of file cadical_options.cpp.

                               {
 
  if (val < 0) {
    LOG ("ignoring negative optimization mode '%d'", val);
    return;
  }
 
  const int max_val = 31;
  if (val > max_val) {
    LOG ("optimization argument '%d' reduced to '%d'", val, max_val);
    val = max_val;
  }
 
  int64_t factor2 = 1;
  for (int i = 0; i < val && factor2 <= INT_MAX; i++)
    factor2 *= 2;
 
  int64_t factor10 = 1;
  for (int i = 0; i < val && factor10 <= INT_MAX; i++)
    factor10 *= 10;
 
  unsigned increased = 0;
#define OPTION(N, V, L, H, O, P, R, D) \
  do { \
    if (!(O)) \
      break; \
    const int64_t factor1 = ((O) == 1 ? factor2 : factor10); \
    int64_t new_val = factor1 * (int64_t) (V); \
    if (new_val > (H)) \
      new_val = (H); \
    if (new_val == (int) (V)) \
      break; \
    LOG ("optimization mode '%d' for '%s' " \
         "gives '%" PRId64 "' instead of '%d", \
         val, #N, new_val, (int) (V)); \
    CADICAL_assert (new_val <= INT_MAX); \
    N = (int) new_val; \
    increased++; \
  } while (0);
  OPTIONS
#undef OPTION
  if (increased)
    MSG ("optimization mode '-O%d' increased %u limits", val, increased);
}

Here is the call graph for this function:

parse_long_option()

bool CaDiCaL::Options::parse_long_option ( const char * arg, string & name, int & val )

static

Definition at line 60 of file cadical_options.cpp.

                                                                        {
  if (arg[0] != '-' || arg[1] != '-')
    return false;
  const bool has_no_prefix =
      (arg[2] == 'n' && arg[3] == 'o' && arg[4] == '-');
  const size_t offset = has_no_prefix ? 5 : 2;
  name = arg + offset;
  const size_t pos = name.find_first_of ('=');
  if (pos != string::npos)
    name[pos] = 0;
  if (!Options::has (name.c_str ()))
    return false;
  if (pos == string::npos)
    val = !has_no_prefix;
  else {
    const char *val_str = name.c_str () + pos + 1;
    if (!parse_int_str (val_str, val))
      return false;
  }
  return true;
}

Here is the call graph for this function:

Here is the caller graph for this function:

print()

void CaDiCaL::Options::print

(

)

Definition at line 198 of file cadical_options.cpp.

                     {
  unsigned different = 0;
#ifdef CADICAL_QUIET
  const bool verbose = false;
#endif
  char buffer[256];
  // We prefer the macro iteration here since '[VLH]' might be '1e9' etc.
#define OPTION(N, V, L, H, O, P, R, D) \
  if (N != (V)) \
    different++; \
  if (verbose || N != (V)) { \
    if ((L) == 0 && (H) == 1) { \
      snprintf (buffer, sizeof buffer, "--" #N "=%s", \
                (N ? "true" : "false")); \
      MSG ("  %s%-30s%s (%s default %s'%s'%s)", \
           ((N == (V)) ? "" : tout.bright_yellow_code ()), buffer, \
           ((N == (V)) ? "" : tout.normal_code ()), \
           ((N == (V)) ? "same as" : "different from"), \
           ((N == (V)) ? tout.green_code () : tout.yellow_code ()), \
           (bool) (V) ? "true" : "false", tout.normal_code ()); \
    } else { \
      snprintf (buffer, sizeof buffer, "--" #N "=%d", N); \
      MSG ("  %s%-30s%s (%s default %s'" #V "'%s)", \
           ((N == (V)) ? "" : tout.bright_yellow_code ()), buffer, \
           ((N == (V)) ? "" : tout.normal_code ()), \
           ((N == (V)) ? "same as" : "different from"), \
           ((N == (V)) ? tout.green_code () : tout.yellow_code ()), \
           tout.normal_code ()); \
    } \
  }
  OPTIONS
#undef OPTION
  if (!different)
    MSG ("all options are set to their default value");
}

set()

bool CaDiCaL::Options::set	(	const char *	name,
		int	val )

Definition at line 183 of file cadical_options.cpp.

                                            {
  Option *o = has (name);
  if (!o)
    return false;
  set (o, val);
  return true;
}

Here is the call graph for this function:

usage()

void CaDiCaL::Options::usage ( )

static

Definition at line 236 of file cadical_options.cpp.

                     {
  // We prefer the macro iteration here since '[VLH]' might be '1e9' etc.
#define OPTION(N, V, L, H, O, P, R, D) \
  if ((L) == 0 && (H) == 1) \
    printf ("  %-26s " D " [%s]\n", "--" #N "=bool", \
            (bool) (V) ? "true" : "false"); \
  else \
    printf ("  %-26s " D " [" #V "]\n", "--" #N "=" #L ".." #H);
  OPTIONS
#undef OPTION
}

Here is the caller graph for this function:

val()

OPTIONS int & CaDiCaL::Options::val ( size_t idx )

inline

Definition at line 363 of file options.hpp.

                               {
    CADICAL_assert (idx < number_of_options);
    return (&__start_of_options__ + 1)[idx];
  }

Here is the caller graph for this function:

Friends And Related Symbol Documentation

Option

friend struct Option

friend

Definition at line 321 of file options.hpp.

Member Data Documentation

reportdefault

int CaDiCaL::Options::reportdefault

static

Definition at line 341 of file options.hpp.

---

The documentation for this class was generated from the following files:

• src/sat/cadical/options.hpp
• src/sat/cadical/cadical_options.cpp