Refactor mkoptions (#1631)

This commit refactors code generation for options. It uses a new configuration format for defining options (*.toml) and a new Python script mkoptions.py to generate the source code and option documentation.

The option behavior did not change for most of the options, except that for bool --enable-/--disable- long options enable/disable was removed. E.g. --enable-miplib-trick and --disable-miplib-trick got changed to --miplib-trick and --no-miplib-trick.

This commit fixes also an issues with set-option/get-option via the SMT2 interface. Before long options were only accessible if the name included the =ARG part.

1 files changed, 41 insertions, 25 deletions

diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index 43d825488..917dae687 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file options_template.cpp
+/*! \file options.cpp
  ** \verbatim
  ** Top contributors (to current version):
  **   Tim King, Morgan Deters, Kshitij Bansal
@@ -58,17 +58,15 @@ extern int optreset;
 #include "options/language.h"
 #include "options/options_handler.h"
 
-${include_all_option_headers}
+${headers_module}$
 
-#line 64 "${template}"
 
 #include "options/options_holder.h"
 #include "cvc4autoconfig.h"
 #include "options/base_handlers.h"
 
-${option_handler_includes}
+${headers_handler}$
 
-#line 72 "${template}"
 
 using namespace CVC4;
 using namespace CVC4::options;
@@ -388,9 +386,8 @@ Options::registerSetReplayLogFilename(
   return registerAndNotify(d_setReplayFilenameListeners, listener, notify);
 }
 
-${all_custom_handlers}
+${custom_handlers}$
 
-#line 394 "${template}"
 
 #ifdef CVC4_DEBUG
 #  define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true
@@ -404,22 +401,22 @@ ${all_custom_handlers}
 #  define DO_SEMANTIC_CHECKS_BY_DEFAULT true
 #endif /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */
 
-options::OptionsHolder::OptionsHolder() : ${all_modules_defaults}
+options::OptionsHolder::OptionsHolder() :
+  ${module_defaults}$
 {
 }
 
-#line 412 "${template}"
 
 static const std::string mostCommonOptionsDescription = "\
-Most commonly-used CVC4 options:${common_documentation}";
+Most commonly-used CVC4 options:\n"
+${help_common}$;
 
-#line 417 "${template}"
 
 static const std::string optionsDescription = mostCommonOptionsDescription + "\n\
 \n\
-Additional CVC4 options:${remaining_documentation}";
+Additional CVC4 options:\n"
+${help_others}$;
 
-#line 423 "${template}"
 
 static const std::string optionsFootnote = "\n\
 [*] Each of these options has a --no-OPTIONNAME variant, which reverses the\n\
@@ -496,11 +493,11 @@ void Options::printLanguageHelp(std::ostream& out) {
  * If you add something that has a short option equivalent, you should
  * add it to the getopt_long() call in parseOptions().
  */
-static struct option cmdlineOptions[] = {${all_modules_long_options}
+static struct option cmdlineOptions[] = {
+  ${cmdline_options}$
   { NULL, no_argument, NULL, '\0' }
 };/* cmdlineOptions */
 
-#line 504 "${template}"
 
 // static void preemptGetopt(int& argc, char**& argv, const char* opt) {
 
@@ -671,7 +668,7 @@ void Options::parseOptionsRecursive(Options* options,
     Debug("options") << "[ argc == " << argc << ", argv == " << argv << " ]"
                      << std::endl;
     int c = getopt_long(argc, argv,
-                        "+:${all_modules_short_options}",
+                        "+:${options_short}$",
                         cmdlineOptions, NULL);
 
     while(main_optind < optind) {
@@ -721,9 +718,8 @@ void Options::parseOptionsRecursive(Options* options,
                            << " (`" << char(c) << "'), " << option << std::endl;
 
     switch(c) {
-${all_modules_option_handlers}
+${options_handler}$
 
-#line 726 "${template}"
 
     case ':':
       // This can be a long or short option, and the way to get at the
@@ -734,8 +730,8 @@ ${all_modules_option_handlers}
     case '?':
     default:
       if( ( optopt == 0 ||
-            ( optopt >= ${long_option_value_begin} &&
-              optopt <= ${long_option_value_end} )
+            ( optopt >= ${option_value_begin}$ &&
+              optopt <= ${option_value_end}$ )
           ) && !strncmp(argv[optind - 1], "--thread", 8) &&
           strlen(argv[optind - 1]) > 8 )
       {
@@ -801,8 +797,7 @@ std::string Options::suggestCommandLineOptions(const std::string& optionName)
 }
 
 static const char* smtOptions[] = {
-  ${all_modules_smt_options},
-#line 804 "${template}"
+  ${options_smt}$
   NULL
 };/* smtOptions[] */
 
@@ -825,15 +820,36 @@ std::vector<std::vector<std::string> > Options::getOptions() const
 {
   std::vector< std::vector<std::string> > opts;
 
-  ${all_modules_get_options}
+  ${options_getoptions}$
 
-#line 826 "${template}"
 
   return opts;
 }
 
+void Options::setOption(const std::string& key, const std::string& optionarg)
+{
+  options::OptionsHandler* handler = d_handler;
+  Options *options = Options::current();
+  Trace("options") << "SMT setOption(" << key << ", " << optionarg << ")"
+                   << std::endl;
+
+  ${setoption_handlers}$
+
+
+  throw UnrecognizedOptionException(key);
+}
+
+std::string Options::getOption(const std::string& key) const
+{
+  Trace("options") << "SMT getOption(" << key << ")" << std::endl;
+
+  ${getoption_handlers}$
+
+
+  throw UnrecognizedOptionException(key);
+}
 
 #undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT
 #undef DO_SEMANTIC_CHECKS_BY_DEFAULT
 
-}/* CVC4 namespace */
+}  // namespace CVC4