Modules
=======

  Each options module starts with the following required attributes:

    id     ... (string) ID of the module (e.g., "ARITH")
    name   ... (string) name of the module (e.g., "Arithmetic Theory")
    header ... (string) name of the options header to generated (e.g., "options/arith_options.h")

  A module defines 0 or more options.

  In general, each attribute/value pair is required to be in one line.
  Comments start with # and are not allowed in attribute/value lines.


Options
=======

  Options can be defined with the [[option]] tag, the required attributes for
  an option are:

    category ... (string) common | expert | regular | undocumented
    type     ... (string) C++ type of the option value

  Optional attributes are:

    name       ... (string) option name that is used to access via
                            options::<name>()
    smt_name   ... (string) alternative name to access option via
                            set-option/get-option commands
    short      ... (string) short option name consisting of one character
                            (no '-' prefix required)
    long       ... (string) long option name (required if short is specified,
                            no '--' prefix required).
                            long option names may have a suffix '=XXX' where
                            'XXX' can be used to indicate the type of the
                            option value, e.g., '=MODE', '=LANG', '=N', ...
    default    ... (string) default value of type 'type'
    handler    ... (string) handler for parsing option values before setting
                            option
    predicates ... (list)   functions that check whether given option value is
                            valid
    includes   ... (list)   header files required by handler/predicates
    read_only  ... (bool)   true: option should not provide a ::set method,
                            false (default): option should provide a ::set
                            method to set the option value
    alternate  ... (bool)   true (default): add --no-<long> alternative option
                            false: omit --no-<long> alternative option
    help       ... (string) documentation (required if category is not
                            undocumented)

  Note that if an option defines a long option name with type 'bool',
  mkoptions.py automatically generates a --no-<long> option to set the option
  to false.
  This behaviour can be explicitely disabled for options with attribute
  alternate = false.
  More information on how to use handler and predicates can be found
  at the end of the README.


  Example:

    [[option]]
      name       = "outputLanguage"
      smt_name   = "output-language"
      category   = "common"
      short      = ""
      long       = "output-lang=LANG"
      type       = "OutputLanguage"
      default    = "language::output::LANG_AUTO"
      handler    = "stringToOutputLanguage"
      predicates = []
      includes   = ["options/language.h"]
      read_only  = false
      help       = "force output language (default is \"auto\"; see --output-lang help)"


Further information (the old option package)
============================================

  The options/ package supports a wide range of operations for responding to
  an option being set. Roughly the three major concepts are:

   - handler to parse an option before setting its value.
   - predicates to reject bad values for the option.

  More details on each class of custom handlers.

   - handler = ""

    Handlers provide support for parsing custom option types.
    The signature for a handler call is:

       T custom-option-handler(std::string option, std::string optarg,
                               OptionsHandler* handler);

    where T is the type of the option. The suggested implementation is to
    implement custom-handler as a dispatch into a function on handler with the
    signature:

       T OptionsHandler::custom-option-handler(std::string option,
                                               std::string optarg);

    The handlers are run before predicates.
    Having multiple handlers is considered bad practice and is unsupported.
    Handlers may have arbitrary side effects, but should call no code
    inaccessible to liboptions. For side effects that are not required in order
    to parse the option, using :predicate is recommended. Memory
    management done by a handler needs to either be encapsulated by the type
    and the destructor for the type or should *always* be owned by handler.
    More elaborate memory management schemes are not currently supported.

   - predicates = [...]

    Predicates provide support for checking whether or not the value of an
    option is acceptable. Predicates are run after handlers.
    The signature for a predicate call is:

      void custom-predicate(std::string option, T value,
                            OptionsHandler* handler);

    where T is the type of the option. The suggested implementation is to
    implement custom-predicate as a dispatch into a function on handler with
    the signature:

      void OptionsHandler::custom-predicate(std::string option, T value);

    The predicates are run after handlers. Multiple
    predicates may be defined for the same option, but the order they are run
    is not guaranteed. Predicates may have arbitrary side effects, but should
    call no code inaccessible to liboptions.