First part of options refactoring (#6428)

This PR does a first round of refactoring and gets rid of a significant portion of generated code. In particular

- it removes options::optionName.wasSetByUser() (we still have Options::wasSetByUser())
- it removes options::optionName.set() (we still have Options::set())
- it removes options::optionName.getName() in favor of options::optionName.name
- it removes the specializations of Options::assign() and Options::assignBool() from the headers
- it eliminates runHandlerAndPredicates() and runBoolPredicates()

The removed methods are only used in few places with are changed to using Options::current().X() instead.

In the future, we also want to get rid of options::optionName() and use Options::operator[]() instead, and furthermore not use Options::current() but use the options from the Env object. This PR already adds Env::getOption() as a shorthand for Env::getOptions()[...] and uses it as a proof of concept within SmtEngine.

1 files changed, 23 insertions, 17 deletions

diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 19d14eb09..927fd1d13 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -127,25 +127,31 @@ void Printer::toStream(std::ostream& out, const SkolemList& sks) const
 
 Printer* Printer::getPrinter(OutputLanguage lang)
 {
-  if(lang == language::output::LANG_AUTO) {
-  // Infer the language to use for output.
-  //
-  // Options can be null in certain circumstances (e.g., when printing
-  // the singleton "null" expr.  So we guard against segfault
-  if(not Options::isCurrentNull()) {
-    if(options::outputLanguage.wasSetByUser()) {
-      lang = options::outputLanguage();
+  if (lang == language::output::LANG_AUTO)
+  {
+    // Infer the language to use for output.
+    //
+    // Options can be null in certain circumstances (e.g., when printing
+    // the singleton "null" expr.  So we guard against segfault
+    if (not Options::isCurrentNull())
+    {
+      if (Options::current().wasSetByUser(options::outputLanguage))
+      {
+        lang = options::outputLanguage();
+      }
+      if (lang == language::output::LANG_AUTO
+          && Options::current().wasSetByUser(options::inputLanguage))
+      {
+        lang = language::toOutputLanguage(options::inputLanguage());
+      }
+    }
+    if (lang == language::output::LANG_AUTO)
+    {
+      lang = language::output::LANG_SMTLIB_V2_6;  // default
     }
-    if(lang == language::output::LANG_AUTO && options::inputLanguage.wasSetByUser()) {
-      lang = language::toOutputLanguage(options::inputLanguage());
-     }
-   }
-   if (lang == language::output::LANG_AUTO)
-   {
-     lang = language::output::LANG_SMTLIB_V2_6;  // default
-   }
   }
-  if(d_printers[lang] == NULL) {
+  if (d_printers[lang] == nullptr)
+  {
     d_printers[lang] = makePrinter(lang);
   }
   return d_printers[lang].get();