Move public options functions to separate file (#6671)

This PR moves the remaining special purpose functions out of the Options class. This set of functions is only used to implement API functions in the smt engine (getting and setting options by string), and by the main driver for parsing and printing usage information.

9 files changed, 683 insertions, 763 deletions

diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt
index 926693185..a548717f3 100644
--- a/src/options/CMakeLists.txt
+++ b/src/options/CMakeLists.txt
@@ -29,7 +29,6 @@ libcvc5_add_sources(
   options_handler.cpp
   options_handler.h
   options_listener.h
-  options_public.cpp
   options_public.h
   outputc.cpp
   outputc.h
@@ -67,7 +66,7 @@ set(options_toml_files
 string(REPLACE "toml" "cpp;" options_gen_cpp_files ${options_toml_files})
 string(REPLACE "toml" "h;"   options_gen_h_files ${options_toml_files})
 
-libcvc5_add_sources(GENERATED options.h options.cpp ${options_gen_cpp_files})
+libcvc5_add_sources(GENERATED options.h options.cpp options_public.cpp ${options_gen_cpp_files})
 
 list_prepend(options_toml_files "${CMAKE_CURRENT_LIST_DIR}/" abs_toml_files)
 
@@ -82,7 +81,7 @@ endif()
 
 add_custom_command(
     OUTPUT
-      options.h options.cpp
+      options.h options.cpp options_public.cpp
       ${options_gen_cpp_files} ${options_gen_h_files}
       ${options_gen_doc_files}
     COMMAND
@@ -97,6 +96,7 @@ add_custom_command(
       ${options_toml_files}
       module_template.h
       module_template.cpp
+      options_public_template.cpp
       options_template.h
       options_template.cpp
 )
@@ -105,6 +105,7 @@ add_custom_target(gen-options
   DEPENDS
     options.h
     options.cpp
+    options_public.cpp
     ${options_gen_cpp_files}
     ${options_gen_h_files}
 )
diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index 2223664d1..a766dce67 100644
--- a/src/options/base_options.toml
+++ b/src/options/base_options.toml
@@ -7,21 +7,21 @@ public = true
   category   = "undocumented"
   type       = "std::istream*"
   default    = "&std::cin"
-  includes   = ["<iosfwd>"]
+  includes   = ["<iostream>"]
 
 [[option]]
   name       = "out"
   category   = "undocumented"
   type       = "std::ostream*"
   default    = "&std::cout"
-  includes   = ["<iosfwd>"]
+  includes   = ["<iostream>"]
 
 [[option]]
   name       = "err"
   category   = "undocumented"
   type       = "std::ostream*"
   default    = "&std::cerr"
-  includes   = ["<iosfwd>"]
+  includes   = ["<iostream>"]
 
 [[option]]
   name       = "inputLanguage"
diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index 45b1db4d6..aeff832b5 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -27,6 +27,7 @@
 
     Directory <tpl-src> must contain:
         - options_template.cpp
+        - options_public_template.cpp
         - module_template.cpp
         - module_template.h
 
@@ -183,6 +184,11 @@ def concat_format(s, objs):
     return '\n'.join([s.format(**o.__dict__) for o in objs])
 
 
+def get_module_headers(modules):
+    """Render includes for module headers"""
+    return concat_format('#include "{header}"', modules)
+
+
 def get_holder_fwd_decls(modules):
     """Render forward declaration of holder structs"""
     return concat_format('  struct Holder{id_cap};', modules)
@@ -237,6 +243,19 @@ def get_predicates(option):
     return ['opts.handler().{}("{}", option, value);'.format(x, optname)
             for x in option.predicates]
 
+
+def get_getall(module, option):
+    """Render snippet to add option to result of getAll()"""
+    if option.type == 'bool':
+        return 'res.push_back({{"{}", opts.{}.{} ? "true" : "false"}});'.format(
+            option.long_name, module.id, option.name)
+    elif is_numeric_cpp_type(option.type):
+        return 'res.push_back({{"{}", std::to_string(opts.{}.{})}});'.format(
+            option.long_name, module.id, option.name)
+    else:
+        return '{{ std::stringstream ss; ss << opts.{}.{}; res.push_back({{"{}", ss.str()}}); }}'.format(
+            module.id, option.name, option.long_name)
+
 class Module(object):
     """Options module.
 
@@ -705,25 +724,26 @@ def add_getopt_long(long_name, argument_req, getopt_long):
             'required' if argument_req else 'no', value))
 
 
-def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_cpp):
+def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h,
+                        tpl_options_cpp, tpl_options_public):
     """
-    Generate code for all option modules (options.cpp, options_holder.h).
+    Generate code for all option modules (options.cpp).
     """
 
     headers_module = []      # generated *_options.h header includes
     headers_handler = set()  # option includes (for handlers, predicates, ...)
     getopt_short = []        # short options for getopt_long
     getopt_long = []         # long options for getopt_long
-    options_smt = []         # all options names accessible via {set,get}-option
+    options_getall = []      # options for options::getAll()
     options_getoptions = []  # options for Options::getOptions()
     options_handler = []     # option handler calls
-    defaults = []            # default values
-    custom_handlers = []     # custom handler implementations assign/assignBool
     help_common = []         # help text for all common options
     help_others = []         # help text for all non-common options
     setoption_handlers = []  # handlers for set-option command
     getoption_handlers = []  # handlers for get-option command
 
+    assign_impls = []
+
     sphinxgen = SphinxGenerator()
 
     for module in modules:
@@ -809,7 +829,7 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_
                 cond = ' || '.join(
                     ['key == "{}"'.format(x) for x in sorted(keys)])
 
-                setoption_handlers.append('if({}) {{'.format(cond))
+                setoption_handlers.append('  if ({}) {{'.format(cond))
                 if option.type == 'bool':
                     setoption_handlers.append(
                         TPL_CALL_ASSIGN_BOOL.format(
@@ -824,15 +844,15 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_
                             name=option.name,
                             option='key'))
                 elif option.handler:
-                    h = 'handler->{handler}("{smtname}", key'
+                    h = '    opts.handler().{handler}("{smtname}", key'
                     if argument_req:
                         h += ', optionarg'
                     h += ');'
                     setoption_handlers.append(
                         h.format(handler=option.handler, smtname=option.long_name))
 
-                setoption_handlers.append('return;')
-                setoption_handlers.append('}')
+                setoption_handlers.append('    return;')
+                setoption_handlers.append('  }')
 
                 if option.name:
                     getoption_handlers.append(
@@ -880,80 +900,51 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_
                 cases.append('  break;')
                 options_handler.extend(cases)
 
-            optname = option.long
-            # collect options available to the SMT-frontend
-            if optname:
-                options_smt.append('"{}",'.format(optname))
-
             if option.name:
                 # Build options for options::getOptions()
-                if optname:
-                    # collect SMT option names
-                    options_smt.append('"{}",'.format(optname))
-
-                    if option.type == 'bool':
-                        s = 'opts.push_back({{"{}", {}.{} ? "true" : "false"}});'.format(
-                            optname, module.id, option.name)
-                    elif is_numeric_cpp_type(option.type):
-                        s = 'opts.push_back({{"{}", std::to_string({}.{})}});'.format(
-                            optname, module.id, option.name)
-                    else:
-                        s = '{{ std::stringstream ss; ss << {}.{}; opts.push_back({{"{}", ss.str()}}); }}'.format(
-                            module.id, option.name, optname)
-                    options_getoptions.append(s)
+                if option.long_name:
+                    options_getall.append(get_getall(module, option))
 
 
                 # Define handler assign/assignBool
                 if not mode_handler:
                     if option.type == 'bool':
-                        custom_handlers.append(TPL_ASSIGN_BOOL.format(
+                        assign_impls.append(TPL_ASSIGN_BOOL.format(
                             module=module.id,
                             name=option.name,
                             handler=handler,
                             predicates='\n'.join(predicates)
                         ))
                     elif option.short or option.long:
-                        custom_handlers.append(TPL_ASSIGN.format(
+                        assign_impls.append(TPL_ASSIGN.format(
                             module=module.id,
                             name=option.name,
                             handler=handler,
                             predicates='\n'.join(predicates)
                         ))
 
-                # Default option values
-                default = option.default if option.default else ''
-                # Prepend enum name
-                if option.mode and option.type not in default:
-                    default = '{}::{}'.format(option.type, default)
-                defaults.append('{}({})'.format(option.name, default))
-                defaults.append('{}WasSetByUser(false)'.format(option.name))
-
-    write_file(dst_dir, 'options.h', tpl_options_h.format(
-        holder_fwd_decls=get_holder_fwd_decls(modules),
-        holder_mem_decls=get_holder_mem_decls(modules),
-        holder_ref_decls=get_holder_ref_decls(modules),
-    ))
-
-    write_file(dst_dir, 'options.cpp', tpl_options_cpp.format(
-        headers_module='\n'.join(headers_module),
-        headers_handler='\n'.join(sorted(list(headers_handler))),
-        holder_mem_copy=get_holder_mem_copy(modules),
-        holder_mem_inits=get_holder_mem_inits(modules),
-        holder_ref_inits=get_holder_ref_inits(modules),
-        custom_handlers='\n'.join(custom_handlers),
-        module_defaults=',\n  '.join(defaults),
-        help_common='\n'.join(help_common),
-        help_others='\n'.join(help_others),
-        cmdline_options='\n  '.join(getopt_long),
-        options_short=''.join(getopt_short),
-        options_handler='\n    '.join(options_handler),
-        option_value_begin=g_getopt_long_start,
-        option_value_end=g_getopt_long_start + len(getopt_long),
-        options_smt='\n  '.join(options_smt),
-        options_getoptions='\n  '.join(options_getoptions),
-        setoption_handlers='\n'.join(setoption_handlers),
-        getoption_handlers='\n'.join(getoption_handlers)
-    ))
+    data = {
+        'holder_fwd_decls': get_holder_fwd_decls(modules),
+        'holder_mem_decls': get_holder_mem_decls(modules),
+        'holder_ref_decls': get_holder_ref_decls(modules),
+        'headers_module': get_module_headers(modules),
+        'headers_handler': '\n'.join(sorted(list(headers_handler))),
+        'holder_mem_inits': get_holder_mem_inits(modules),
+        'holder_ref_inits': get_holder_ref_inits(modules),
+        'holder_mem_copy': get_holder_mem_copy(modules),
+        'cmdline_options': '\n  '.join(getopt_long),
+        'help_common': '\n'.join(help_common),
+        'help_others': '\n'.join(help_others),
+        'options_handler': '\n    '.join(options_handler),
+        'options_short': ''.join(getopt_short),
+        'assigns': '\n'.join(assign_impls),
+        'options_getall': '\n  '.join(options_getall),
+        'getoption_handlers': '\n'.join(getoption_handlers),
+        'setoption_handlers': '\n'.join(setoption_handlers),
+    }
+    write_file(dst_dir, 'options.h', tpl_options_h.format(**data))
+    write_file(dst_dir, 'options.cpp', tpl_options_cpp.format(**data))
+    write_file(dst_dir, 'options_public.cpp', tpl_options_public.format(**data))
 
     if os.path.isdir('{}/docs/'.format(build_dir)):
         sphinxgen.render('{}/docs/'.format(build_dir), 'options_generated.rst')
@@ -1093,6 +1084,7 @@ def mkoptions_main():
     # Read source code template files from source directory.
     tpl_module_h = read_tpl(src_dir, 'module_template.h')
     tpl_module_cpp = read_tpl(src_dir, 'module_template.cpp')
+    tpl_options_public = read_tpl(src_dir, 'options_public_template.cpp')
     tpl_options_h = read_tpl(src_dir, 'options_template.h')
     tpl_options_cpp = read_tpl(src_dir, 'options_template.cpp')
 
@@ -1113,8 +1105,7 @@ def mkoptions_main():
         codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp)
 
     # Create options.cpp in destination directory
-    codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_cpp)
-
+    codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_cpp, tpl_options_public)
 
 
 if __name__ == "__main__":
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index e423dc149..7a80c4d7a 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -155,11 +155,11 @@ void OptionsHandler::checkBvSatSolver(const std::string& option,
     throw OptionException(ss.str());
   }
 
-  if (options::bvSolver() != options::BVSolver::BITBLAST
+  if (d_options->bv.bvSolver != options::BVSolver::BITBLAST
       && (m == SatSolverMode::CRYPTOMINISAT || m == SatSolverMode::CADICAL
           || m == SatSolverMode::KISSAT))
   {
-    if (options::bitblastMode() == options::BitblastMode::LAZY
+    if (d_options->bv.bitblastMode == options::BitblastMode::LAZY
         && d_options->bv.bitblastModeWasSetByUser)
     {
       throwLazyBBUnsupported(m);
@@ -178,9 +178,9 @@ void OptionsHandler::checkBitblastMode(const std::string& option,
     options::bv::setDefaultBitvectorEqualitySolver(*d_options, true);
     options::bv::setDefaultBitvectorInequalitySolver(*d_options, true);
     options::bv::setDefaultBitvectorAlgebraicSolver(*d_options, true);
-    if (options::bvSatSolver() != options::SatSolverMode::MINISAT)
+    if (d_options->bv.bvSatSolver != options::SatSolverMode::MINISAT)
     {
-      throwLazyBBUnsupported(options::bvSatSolver());
+      throwLazyBBUnsupported(d_options->bv.bvSatSolver);
     }
   }
   else if (m == BitblastMode::EAGER)
@@ -195,7 +195,7 @@ void OptionsHandler::setBitblastAig(const std::string& option,
 {
   if(arg) {
     if (d_options->bv.bitblastModeWasSetByUser) {
-      if (options::bitblastMode() != options::BitblastMode::EAGER)
+      if (d_options->bv.bitblastMode != options::BitblastMode::EAGER)
       {
         throw OptionException("bitblast-aig must be used with eager bitblaster");
       }
diff --git a/src/options/options_public.cpp b/src/options/options_public.cpp
deleted file mode 100644
index 552058312..000000000
--- a/src/options/options_public.cpp
+++ /dev/null
@@ -1,26 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Tim King, Gereon Kremer, Andrew Reynolds
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved.  See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * Definitions of public facing interface functions for Options.
- *
- * These are all one line wrappers for accessing the internal option data.
- */
-
-#include "options_public.h"
-
-#include "options/uf_options.h"
-
-namespace cvc5::options {
-
-bool getUfHo(const Options& opts) { return opts.uf.ufHo; }
-
-}  // namespace cvc5::options
diff --git a/src/options/options_public.h b/src/options/options_public.h
index 60929c96c..03d7ec41a 100644
--- a/src/options/options_public.h
+++ b/src/options/options_public.h
@@ -10,12 +10,7 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * Public facing functions for options that need to be accessed from the
- * outside.
- *
- * These are all one line wrappers for accessing the internal option data so
- * that external code (including parser/ and main/) does not need to include
- * the option modules (*_options.h).
+ * Global (command-line, set-option, ...) parameters for SMT.
  */
 
 #include "cvc5_public.h"
@@ -23,12 +18,77 @@
 #ifndef CVC5__OPTIONS__OPTIONS_PUBLIC_H
 #define CVC5__OPTIONS__OPTIONS_PUBLIC_H
 
+#include <iosfwd>
+#include <string>
+#include <vector>
+
+#include "cvc5_export.h"
 #include "options/options.h"
 
 namespace cvc5::options {
 
 bool getUfHo(const Options& opts) CVC5_EXPORT;
 
+/**
+ * Get a description of the command-line flags accepted by
+ * parse.  The returned string will be escaped so that it is
+ * suitable as an argument to printf. */
+const std::string& getDescription() CVC5_EXPORT;
+
+/**
+ * Print overall command-line option usage message, prefixed by
+ * "msg"---which could be an error message causing the usage
+ * output in the first place, e.g. "no such option --foo"
+ */
+void printUsage(const std::string& msg, std::ostream& os) CVC5_EXPORT;
+
+/**
+ * Print command-line option usage message for only the most-commonly
+ * used options.  The message is prefixed by "msg"---which could be
+ * an error message causing the usage output in the first place, e.g.
+ * "no such option --foo"
+ */
+void printShortUsage(const std::string& msg, std::ostream& os) CVC5_EXPORT;
+
+/** Print help for the --lang command line option */
+void printLanguageHelp(std::ostream& os) CVC5_EXPORT;
+
+/**
+ * Initialize the Options object options based on the given
+ * command-line arguments given in argc and argv.  The return value
+ * is what's left of the command line (that is, the non-option
+ * arguments).
+ *
+ * This function uses getopt_long() and is not thread safe.
+ *
+ * Throws OptionException on failures.
+ *
+ * Preconditions: options and argv must be non-null.
+ */
+std::vector<std::string> parse(Options& opts,
+                               int argc,
+                               char* argv[],
+                               std::string& binaryName) CVC5_EXPORT;
+
+/**
+ * Retrieve an option value by name (as given in key) from the Options object
+ * opts as a string.
+ */
+std::string get(const Options& opts, const std::string& key) CVC5_EXPORT;
+
+/**
+ * Update the Options object opts, set the value of the option specified by key
+ * to the value parsed from optionarg.
+ */
+void set(Options& opts,
+         const std::string& key,
+         const std::string& optionarg) CVC5_EXPORT;
+
+/**
+ * Get the setting for all options.
+ */
+std::vector<std::vector<std::string> > getAll(const Options& opts) CVC5_EXPORT;
+
 }  // namespace cvc5::options
 
 #endif
diff --git a/src/options/options_public_template.cpp b/src/options/options_public_template.cpp
new file mode 100644
index 000000000..70c6f420a
--- /dev/null
+++ b/src/options/options_public_template.cpp
@@ -0,0 +1,496 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Tim King, Gereon Kremer, Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Global (command-line, set-option, ...) parameters for SMT.
+ */
+
+#include "options/options_public.h"
+
+#if !defined(_BSD_SOURCE) && defined(__MINGW32__) && !defined(__MINGW64__)
+// force use of optreset; mingw32 croaks on argv-switching otherwise
+#include "base/cvc5config.h"
+#define _BSD_SOURCE
+#undef HAVE_DECL_OPTRESET
+#define HAVE_DECL_OPTRESET 1
+#define CVC5_IS_NOT_REALLY_BSD
+#endif /* !_BSD_SOURCE && __MINGW32__ && !__MINGW64__ */
+
+#ifdef __MINGW64__
+extern int optreset;
+#endif /* __MINGW64__ */
+
+#include <getopt.h>
+
+// clean up
+#ifdef CVC5_IS_NOT_REALLY_BSD
+#  undef _BSD_SOURCE
+#endif /* CVC5_IS_NOT_REALLY_BSD */
+
+#include "base/check.h"
+#include "base/output.h"
+#include "options/didyoumean.h"
+#include "options/options_handler.h"
+#include "options/options_listener.h"
+#include "options/options.h"
+#include "options/uf_options.h"
+${headers_module}$
+${headers_handler}$
+
+#include <cstring>
+#include <iostream>
+#include <limits>
+
+namespace cvc5::options {
+
+bool getUfHo(const Options& opts) { return opts.uf.ufHo; }
+
+// clang-format off
+static const std::string mostCommonOptionsDescription =
+    "\
+Most commonly-used cvc5 options:\n"
+${help_common}$
+    ;
+
+static const std::string optionsDescription =
+    mostCommonOptionsDescription + "\n\nAdditional cvc5 options:\n"
+${help_others}$;
+
+static const std::string optionsFootnote = "\n\
+[*] Each of these options has a --no-OPTIONNAME variant, which reverses the\n\
+    sense of the option.\n\
+";
+
+static const std::string languageDescription =
+    "\
+Languages currently supported as arguments to the -L / --lang option:\n\
+  auto                           attempt to automatically determine language\n\
+  cvc | presentation | pl        CVC presentation language\n\
+  smt | smtlib | smt2 |\n\
+  smt2.6 | smtlib2.6             SMT-LIB format 2.6 with support for the strings standard\n\
+  tptp                           TPTP format (cnf, fof and tff)\n\
+  sygus | sygus2                 SyGuS version 2.0\n\
+\n\
+Languages currently supported as arguments to the --output-lang option:\n\
+  auto                           match output language to input language\n\
+  cvc | presentation | pl        CVC presentation language\n\
+  smt | smtlib | smt2 |\n\
+  smt2.6 | smtlib2.6             SMT-LIB format 2.6 with support for the strings standard\n\
+  tptp                           TPTP format\n\
+  ast                            internal format (simple syntax trees)\n\
+";
+// clang-format on
+
+const std::string& getDescription()
+{
+  return optionsDescription;
+}
+
+void printUsage(const std::string& msg, std::ostream& os) {
+  os << msg << optionsDescription << std::endl
+      << optionsFootnote << std::endl << std::flush;
+}
+
+void printShortUsage(const std::string& msg, std::ostream& os) {
+  os << msg << mostCommonOptionsDescription << std::endl
+      << optionsFootnote << std::endl
+      << "For full usage, please use --help."
+      << std::endl << std::endl << std::flush;
+}
+
+void printLanguageHelp(std::ostream& os) {
+  os << languageDescription << std::flush;
+}
+
+/** Set a given Options* as "current" just for a particular scope. */
+class OptionsGuard {
+  Options** d_field;
+  Options* d_old;
+public:
+  OptionsGuard(Options** field, Options* opts) :
+    d_field(field),
+    d_old(*field) {
+    *field = opts;
+  }
+  ~OptionsGuard() {
+    *d_field = d_old;
+  }
+};/* class OptionsGuard */
+
+/**
+ * This is a table of long options.  By policy, each short option
+ * should have an equivalent long option (but the reverse isn't the
+ * case), so this table should thus contain all command-line options.
+ *
+ * Each option in this array has four elements:
+ *
+ * 1. the long option string
+ * 2. argument behavior for the option:
+ *    no_argument - no argument permitted
+ *    required_argument - an argument is expected
+ *    optional_argument - an argument is permitted but not required
+ * 3. this is a pointer to an int which is set to the 4th entry of the
+ *    array if the option is present; or NULL, in which case
+ *    getopt_long() returns the 4th entry
+ * 4. the return value for getopt_long() when this long option (or the
+ *    value to set the 3rd entry to; see #3)
+ *
+ * If you add something here, you should add it in src/main/usage.h
+ * also, to document it.
+ *
+ * If you add something that has a short option equivalent, you should
+ * add it to the getopt_long() call in parse().
+ */
+// clang-format off
+static struct option cmdlineOptions[] = {
+  ${cmdline_options}$
+  {nullptr, no_argument, nullptr, '\0'}};
+// clang-format on
+
+std::string suggestCommandLineOptions(const std::string& optionName)
+{
+  DidYouMean didYouMean;
+
+  const char* opt;
+  for(size_t i = 0; (opt = cmdlineOptions[i].name) != nullptr; ++i) {
+    didYouMean.addWord(std::string("--") + cmdlineOptions[i].name);
+  }
+
+  return didYouMean.getMatchAsString(optionName.substr(0, optionName.find('=')));
+}
+
+/**
+ * This is a default handler for options of built-in C++ type.  This
+ * template is really just a helper for the handleOption() template,
+ * below.  Variants of this template handle numeric and non-numeric,
+ * integral and non-integral, signed and unsigned C++ types.
+ * handleOption() makes sure to instantiate the right one.
+ *
+ * This implements default behavior when e.g. an option is
+ * unsigned but the user specifies a negative argument; etc.
+ */
+template <class T, bool is_numeric, bool is_integer>
+struct OptionHandler {
+  static T handle(const std::string& option, const std::string& flag, const std::string& optionarg);
+};/* struct OptionHandler<> */
+
+/** Variant for integral C++ types */
+template <class T>
+struct OptionHandler<T, true, true> {
+  static bool stringToInt(T& t, const std::string& str) {
+    std::istringstream ss(str);
+    ss >> t;
+    char tmp;
+    return !(ss.fail() || ss.get(tmp));
+  }
+
+  static bool containsMinus(const std::string& str) {
+    return str.find('-') != std::string::npos;
+  }
+
+  static T handle(const std::string& option, const std::string& flag, const std::string& optionarg) {
+    try {
+      T i;
+      bool success = stringToInt(i, optionarg);
+
+      if(!success){
+        throw OptionException(flag + ": failed to parse "+ optionarg +
+                              " as an integer of the appropriate type.");
+      }
+
+      // Depending in the platform unsigned numbers with '-' signs may parse.
+      // Reject these by looking for any minus if it is not signed.
+      if( (! std::numeric_limits<T>::is_signed) && containsMinus(optionarg) ) {
+        // unsigned type but user gave negative argument
+        throw OptionException(flag + " requires a nonnegative argument");
+      } else if(i < std::numeric_limits<T>::min()) {
+        // negative overflow for type
+        std::stringstream ss;
+        ss << flag << " requires an argument >= "
+           << std::numeric_limits<T>::min();
+        throw OptionException(ss.str());
+      } else if(i > std::numeric_limits<T>::max()) {
+        // positive overflow for type
+        std::stringstream ss;
+        ss << flag << " requires an argument <= "
+           << std::numeric_limits<T>::max();
+        throw OptionException(ss.str());
+      }
+
+      return i;
+
+      // if(std::numeric_limits<T>::is_signed) {
+      //   return T(i.getLong());
+      // } else {
+      //   return T(i.getUnsignedLong());
+      // }
+    } catch(std::invalid_argument&) {
+      // user gave something other than an integer
+      throw OptionException(flag + " requires an integer argument");
+    }
+  }
+};/* struct OptionHandler<T, true, true> */
+
+/** Variant for numeric but non-integral C++ types */
+template <class T>
+struct OptionHandler<T, true, false> {
+  static T handle(const std::string& option, const std::string& flag, const std::string& optionarg) {
+    std::stringstream inss(optionarg);
+    long double r;
+    inss >> r;
+    if(! inss.eof()) {
+      // we didn't consume the whole string (junk at end)
+      throw OptionException(flag + " requires a numeric argument");
+    }
+
+    if(! std::numeric_limits<T>::is_signed && r < 0.0) {
+      // unsigned type but user gave negative value
+      throw OptionException(flag + " requires a nonnegative argument");
+    } else if(r < -std::numeric_limits<T>::max()) {
+      // negative overflow for type
+      std::stringstream ss;
+      ss << flag << " requires an argument >= "
+         << -std::numeric_limits<T>::max();
+      throw OptionException(ss.str());
+    } else if(r > std::numeric_limits<T>::max()) {
+      // positive overflow for type
+      std::stringstream ss;
+      ss << flag << " requires an argument <= "
+         << std::numeric_limits<T>::max();
+      throw OptionException(ss.str());
+    }
+
+    return T(r);
+  }
+};/* struct OptionHandler<T, true, false> */
+
+/** Variant for non-numeric C++ types */
+template <class T>
+struct OptionHandler<T, false, false> {
+  static T handle(const std::string& option, const std::string& flag, const std::string& optionarg) {
+    T::unsupported_handleOption_call___please_write_me;
+    // The above line causes a compiler error if this version of the template
+    // is ever instantiated (meaning that a specialization is missing).  So
+    // don't worry about the segfault in the next line, the "return" is only
+    // there to keep the compiler from giving additional, distracting errors
+    // and warnings.
+    return *(T*)0;
+  }
+};/* struct OptionHandler<T, false, false> */
+
+/** Handle an option of type T in the default way. */
+template <class T>
+T handleOption(const std::string& option, const std::string& flag, const std::string& optionarg) {
+  return OptionHandler<T, std::numeric_limits<T>::is_specialized, std::numeric_limits<T>::is_integer>::handle(option, flag, optionarg);
+}
+
+/** Handle an option of type std::string in the default way. */
+template <>
+std::string handleOption<std::string>(const std::string& option, const std::string& flag, const std::string& optionarg) {
+  return optionarg;
+}
+
+// clang-format off
+${assigns}$
+// clang-format off
+
+void parseInternal(Options& opts, int argc,
+                                    char* argv[],
+                                    std::vector<std::string>& nonoptions)
+{
+  Assert(argv != nullptr);
+  if(Debug.isOn("options")) {
+    Debug("options") << "starting a new parseInternal with "
+                     << argc << " arguments" << std::endl;
+    for( int i = 0; i < argc ; i++ ){
+      Assert(argv[i] != NULL);
+      Debug("options") << "  argv[" << i << "] = " << argv[i] << std::endl;
+    }
+  }
+
+  // Reset getopt(), in the case of multiple calls to parse().
+  // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0.
+  optind = 0;
+#if HAVE_DECL_OPTRESET
+  optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this
+#endif /* HAVE_DECL_OPTRESET */
+
+  // We must parse the binary name, which is manually ignored below. Setting
+  // this to 1 leads to incorrect behavior on some platforms.
+  int main_optind = 0;
+  int old_optind;
+
+
+  while(true) { // Repeat Forever
+
+    optopt = 0;
+    std::string option, optionarg;
+
+    optind = main_optind;
+    old_optind = main_optind;
+
+    // If we encounter an element that is not at zero and does not start
+    // with a "-", this is a non-option. We consume this element as a
+    // non-option.
+    if (main_optind > 0 && main_optind < argc &&
+        argv[main_optind][0] != '-') {
+      Debug("options") << "enqueueing " << argv[main_optind]
+                       << " as a non-option." << std::endl;
+      nonoptions.push_back(argv[main_optind]);
+      ++main_optind;
+      continue;
+    }
+
+
+    Debug("options") << "[ before, main_optind == " << main_optind << " ]"
+                     << std::endl;
+    Debug("options") << "[ before, optind == " << optind << " ]" << std::endl;
+    Debug("options") << "[ argc == " << argc << ", argv == " << argv << " ]"
+                     << std::endl;
+    // clang-format off
+    int c = getopt_long(argc, argv,
+                        "+:${options_short}$",
+                        cmdlineOptions, NULL);
+    // clang-format on
+
+    main_optind = optind;
+
+    Debug("options") << "[ got " << int(c) << " (" << char(c) << ") ]"
+                     << "[ next option will be at pos: " << optind << " ]"
+                     << std::endl;
+
+    // The initial getopt_long call should always determine that argv[0]
+    // is not an option and returns -1. We always manually advance beyond
+    // this element.
+    if ( old_optind == 0  && c == -1 ) {
+      Assert(main_optind > 0);
+      continue;
+    }
+
+    if ( c == -1 ) {
+      if(Debug.isOn("options")) {
+        Debug("options") << "done with option parsing" << std::endl;
+        for(int index = optind; index < argc; ++index) {
+          Debug("options") << "remaining " << argv[index] << std::endl;
+        }
+      }
+      break;
+    }
+
+    option = argv[old_optind == 0 ? 1 : old_optind];
+    optionarg = (optarg == NULL) ? "" : optarg;
+
+    Debug("preemptGetopt") << "processing option " << c
+                           << " (`" << char(c) << "'), " << option << std::endl;
+
+    // clang-format off
+    switch(c)
+    {
+${options_handler}$
+
+      case ':' :
+      // This can be a long or short option, and the way to get at the
+      // name of it is different.
+      throw OptionException(std::string("option `") + option
+                            + "' missing its required argument");
+
+      case '?':
+      default:
+        throw OptionException(std::string("can't understand option `") + option
+                              + "'" + suggestCommandLineOptions(option));
+    }
+  }
+  // clang-format on
+
+  Debug("options") << "got " << nonoptions.size()
+                   << " non-option arguments." << std::endl;
+}
+
+/**
+ * Parse argc/argv and put the result into a cvc5::Options.
+ * The return value is what's left of the command line (that is, the
+ * non-option arguments).
+ *
+ * Throws OptionException on failures.
+ */
+std::vector<std::string> parse(
+    Options & opts, int argc, char* argv[], std::string& binaryName)
+{
+  Assert(argv != nullptr);
+
+  Options* cur = &Options::current();
+  OptionsGuard guard(&cur, &opts);
+
+  const char *progName = argv[0];
+
+  // To debug options parsing, you may prefer to simply uncomment this
+  // and recompile. Debug flags have not been parsed yet so these have
+  // not been set.
+  //DebugChannel.on("options");
+
+  Debug("options") << "options::parse == " << &opts << std::endl;
+  Debug("options") << "argv == " << argv << std::endl;
+
+  // Find the base name of the program.
+  const char *x = strrchr(progName, '/');
+  if(x != nullptr) {
+    progName = x + 1;
+  }
+  binaryName = std::string(progName);
+
+  std::vector<std::string> nonoptions;
+  parseInternal(opts, argc, argv, nonoptions);
+  if (Debug.isOn("options")){
+    for(std::vector<std::string>::const_iterator i = nonoptions.begin(),
+          iend = nonoptions.end(); i != iend; ++i){
+      Debug("options") << "nonoptions " << *i << std::endl;
+    }
+  }
+
+  return nonoptions;
+}
+
+std::string get(const Options& options, const std::string& key)
+{
+  Trace("options") << "Options::getOption(" << key << ")" << std::endl;
+  ${getoption_handlers}$
+
+  throw UnrecognizedOptionException(key);
+}
+
+void setInternal(Options& opts, const std::string& key,
+                                const std::string& optionarg)
+                                {
+  ${setoption_handlers}$
+  throw UnrecognizedOptionException(key);
+}
+
+void set(Options& opts, const std::string& key, const std::string& optionarg)
+{
+
+  Trace("options") << "setOption(" << key << ", " << optionarg << ")"
+                   << std::endl;
+  // first update this object
+  setInternal(opts, key, optionarg);
+  // then, notify the provided listener
+  opts.notifyListener(key);
+}
+
+std::vector<std::vector<std::string> > getAll(const Options& opts)
+{
+  std::vector<std::vector<std::string>> res;
+
+${options_getall}$
+
+  return res;
+}
+
+}  // namespace cvc5::options
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index 2c22065c2..db58c3a4a 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -13,43 +13,11 @@
  * Contains code for handling command-line options.
  */
 
-#if !defined(_BSD_SOURCE) && defined(__MINGW32__) && !defined(__MINGW64__)
-// force use of optreset; mingw32 croaks on argv-switching otherwise
-#include "base/cvc5config.h"
-#define _BSD_SOURCE
-#undef HAVE_DECL_OPTRESET
-#define HAVE_DECL_OPTRESET 1
-#define CVC5_IS_NOT_REALLY_BSD
-#endif /* !_BSD_SOURCE && __MINGW32__ && !__MINGW64__ */
-
-#ifdef __MINGW64__
-extern int optreset;
-#endif /* __MINGW64__ */
-
-#include <getopt.h>
-
-// clean up
-#ifdef CVC5_IS_NOT_REALLY_BSD
-#  undef _BSD_SOURCE
-#endif /* CVC5_IS_NOT_REALLY_BSD */
-
-#include <unistd.h>
-#include <string.h>
-#include <time.h>
-
-#include <cstdio>
-#include <cstdlib>
-#include <cstring>
-#include <iomanip>
-#include <new>
-#include <string>
-#include <sstream>
-#include <limits>
+#include "options/options.h"
 
 #include "base/check.h"
 #include "base/exception.h"
 #include "base/output.h"
-#include "options/didyoumean.h"
 #include "options/language.h"
 #include "options/options_handler.h"
 #include "options/options_listener.h"
@@ -65,175 +33,22 @@ using namespace cvc5;
 using namespace cvc5::options;
 // clang-format on
 
-namespace cvc5 {
-
-thread_local Options* Options::s_current = NULL;
-
-/**
- * This is a default handler for options of built-in C++ type.  This
- * template is really just a helper for the handleOption() template,
- * below.  Variants of this template handle numeric and non-numeric,
- * integral and non-integral, signed and unsigned C++ types.
- * handleOption() makes sure to instantiate the right one.
- *
- * This implements default behavior when e.g. an option is
- * unsigned but the user specifies a negative argument; etc.
- */
-template <class T, bool is_numeric, bool is_integer>
-struct OptionHandler {
-  static T handle(const std::string& option,
-                  const std::string& flag,
-                  const std::string& optionarg);
-};/* struct OptionHandler<> */
-
-/** Variant for integral C++ types */
-template <class T>
-struct OptionHandler<T, true, true> {
-  static bool stringToInt(T& t, const std::string& str) {
-    std::istringstream ss(str);
-    ss >> t;
-    char tmp;
-    return !(ss.fail() || ss.get(tmp));
-  }
-
-  static bool containsMinus(const std::string& str) {
-    return str.find('-') != std::string::npos;
-  }
-
-  static T handle(const std::string& option,
-                  const std::string& flag,
-                  const std::string& optionarg)
-  {
-    try {
-      T i;
-      bool success = stringToInt(i, optionarg);
-
-      if(!success){
-        throw OptionException(flag + ": failed to parse " + optionarg
-                              + " as an integer of the appropriate type.");
-      }
-
-      // Depending in the platform unsigned numbers with '-' signs may parse.
-      // Reject these by looking for any minus if it is not signed.
-      if( (! std::numeric_limits<T>::is_signed) && containsMinus(optionarg) ) {
-        // unsigned type but user gave negative argument
-        throw OptionException(flag + " requires a nonnegative argument");
-      } else if(i < std::numeric_limits<T>::min()) {
-        // negative overflow for type
-        std::stringstream ss;
-        ss << flag
-           << " requires an argument >= " << std::numeric_limits<T>::min();
-        throw OptionException(ss.str());
-      } else if(i > std::numeric_limits<T>::max()) {
-        // positive overflow for type
-        std::stringstream ss;
-        ss << flag
-           << " requires an argument <= " << std::numeric_limits<T>::max();
-        throw OptionException(ss.str());
-      }
-
-      return i;
-
-      // if(std::numeric_limits<T>::is_signed) {
-      //   return T(i.getLong());
-      // } else {
-      //   return T(i.getUnsignedLong());
-      // }
-    } catch(std::invalid_argument&) {
-      // user gave something other than an integer
-      throw OptionException(flag + " requires an integer argument");
-    }
-  }
-};/* struct OptionHandler<T, true, true> */
-
-/** Variant for numeric but non-integral C++ types */
-template <class T>
-struct OptionHandler<T, true, false> {
-  static T handle(const std::string& option,
-                  const std::string& flag,
-                  const std::string& optionarg)
-  {
-    std::stringstream inss(optionarg);
-    long double r;
-    inss >> r;
-    if (!inss.eof())
-    {
-      // we didn't consume the whole string (junk at end)
-      throw OptionException(flag + " requires a numeric argument");
-    }
-
-    if(! std::numeric_limits<T>::is_signed && r < 0.0) {
-      // unsigned type but user gave negative value
-      throw OptionException(flag + " requires a nonnegative argument");
-    } else if(r < -std::numeric_limits<T>::max()) {
-      // negative overflow for type
-      std::stringstream ss;
-      ss << flag
-         << " requires an argument >= " << -std::numeric_limits<T>::max();
-      throw OptionException(ss.str());
-    } else if(r > std::numeric_limits<T>::max()) {
-      // positive overflow for type
-      std::stringstream ss;
-      ss << flag
-         << " requires an argument <= " << std::numeric_limits<T>::max();
-      throw OptionException(ss.str());
-    }
-
-    return T(r);
-  }
-};/* struct OptionHandler<T, true, false> */
-
-/** Variant for non-numeric C++ types */
-template <class T>
-struct OptionHandler<T, false, false> {
-  static T handle(const std::string& option,
-                  const std::string& flag,
-                  const std::string& optionarg)
-  {
-    T::unsupported_handleOption_call___please_write_me;
-    // The above line causes a compiler error if this version of the template
-    // is ever instantiated (meaning that a specialization is missing).  So
-    // don't worry about the segfault in the next line, the "return" is only
-    // there to keep the compiler from giving additional, distracting errors
-    // and warnings.
-    return *(T*)0;
-  }
-};/* struct OptionHandler<T, false, false> */
-
-/** Handle an option of type T in the default way. */
-template <class T>
-T handleOption(const std::string& option,
-               const std::string& flag,
-               const std::string& optionarg)
-{
-  return OptionHandler<T,
-                       std::numeric_limits<T>::is_specialized,
-                       std::numeric_limits<T>::is_integer>::handle(option,
-                                                                   flag,
-                                                                   optionarg);
-}
-
-/** Handle an option of type std::string in the default way. */
-template <>
-std::string handleOption<std::string>(const std::string& option,
-                                      const std::string& flag,
-                                      const std::string& optionarg)
+namespace cvc5
 {
-  return optionarg;
-}
+  thread_local Options* Options::s_current = nullptr;
 
-Options::Options(OptionsListener* ol)
-    : d_handler(new options::OptionsHandler(this)),
+  Options::Options(OptionsListener * ol)
+      :
+        d_olisten(ol),
 // clang-format off
 ${holder_mem_inits}$
 ${holder_ref_inits}$
 // clang-format on
-      d_olisten(ol)
-{}
+        d_handler(std::make_unique<options::OptionsHandler>(this))
+  {
+  }
 
-Options::~Options() {
-  delete d_handler;
-}
+  Options::~Options() {}
 
 void Options::copyValues(const Options& options){
   if(this != &options) {
@@ -244,333 +59,14 @@ ${holder_mem_copy}$
 }
 
 void Options::setListener(OptionsListener* ol) { d_olisten = ol; }
-
-// clang-format off
-${custom_handlers}$
-// clang-format on
-
-static const std::string mostCommonOptionsDescription =
-    "\
-Most commonly-used cvc5 options:\n"
-    // clang-format off
-${help_common}$
-    // clang-format on
-    ;
-
-// clang-format off
-static const std::string optionsDescription =
-    mostCommonOptionsDescription + "\n\nAdditional cvc5 options:\n"
-${help_others}$;
-// clang-format on
-
-static const std::string optionsFootnote = "\n\
-[*] Each of these options has a --no-OPTIONNAME variant, which reverses the\n\
-    sense of the option.\n\
-";
-
-static const std::string languageDescription =
-    "\
-Languages currently supported as arguments to the -L / --lang option:\n\
-  auto                           attempt to automatically determine language\n\
-  cvc | presentation | pl        CVC presentation language\n\
-  smt | smtlib | smt2 |\n\
-  smt2.6 | smtlib2.6             SMT-LIB format 2.6 with support for the strings standard\n\
-  tptp                           TPTP format (cnf, fof and tff)\n\
-  sygus | sygus2                 SyGuS version 2.0\n\
-\n\
-Languages currently supported as arguments to the --output-lang option:\n\
-  auto                           match output language to input language\n\
-  cvc | presentation | pl        CVC presentation language\n\
-  smt | smtlib | smt2 |\n\
-  smt2.6 | smtlib2.6             SMT-LIB format 2.6 with support for the strings standard\n\
-  tptp                           TPTP format\n\
-  ast                            internal format (simple syntax trees)\n\
-";
-
-std::string Options::getDescription() const {
-  return optionsDescription;
-}
-
-void Options::printUsage(const std::string msg, std::ostream& out) {
-  out << msg << optionsDescription << std::endl
-      << optionsFootnote << std::endl << std::flush;
-}
-
-void Options::printShortUsage(const std::string msg, std::ostream& out) {
-  out << msg << mostCommonOptionsDescription << std::endl
-      << optionsFootnote << std::endl
-      << "For full usage, please use --help."
-      << std::endl << std::endl << std::flush;
-}
-
-void Options::printLanguageHelp(std::ostream& out) {
-  out << languageDescription << std::flush;
-}
-
-/**
- * This is a table of long options.  By policy, each short option
- * should have an equivalent long option (but the reverse isn't the
- * case), so this table should thus contain all command-line options.
- *
- * Each option in this array has four elements:
- *
- * 1. the long option string
- * 2. argument behavior for the option:
- *    no_argument - no argument permitted
- *    required_argument - an argument is expected
- *    optional_argument - an argument is permitted but not required
- * 3. this is a pointer to an int which is set to the 4th entry of the
- *    array if the option is present; or NULL, in which case
- *    getopt_long() returns the 4th entry
- * 4. the return value for getopt_long() when this long option (or the
- *    value to set the 3rd entry to; see #3)
- *
- * If you add something here, you should add it in src/main/usage.h
- * also, to document it.
- *
- * If you add something that has a short option equivalent, you should
- * add it to the getopt_long() call in parseOptions().
- */
-// clang-format off
-static struct option cmdlineOptions[] = {
-  ${cmdline_options}$
-  {nullptr, no_argument, nullptr, '\0'}};
-// clang-format on
-
-namespace options {
-
-/** Set a given Options* as "current" just for a particular scope. */
-class OptionsGuard {
-  Options** d_field;
-  Options* d_old;
-public:
-  OptionsGuard(Options** field, Options* opts) :
-    d_field(field),
-    d_old(*field) {
-    *field = opts;
-  }
-  ~OptionsGuard() {
-    *d_field = d_old;
-  }
-};/* class OptionsGuard */
-
-}  // namespace options
-
-/**
- * Parse argc/argv and put the result into a cvc5::Options.
- * The return value is what's left of the command line (that is, the
- * non-option arguments).
- *
- * Throws OptionException on failures.
- */
-std::vector<std::string> Options::parseOptions(Options* options,
-                                               int argc,
-                                               char* argv[],
-                                               std::string& binaryName)
-{
-  Assert(options != NULL);
-  Assert(argv != NULL);
-
-  options::OptionsGuard guard(&s_current, options);
-
-  const char *progName = argv[0];
-
-  // To debug options parsing, you may prefer to simply uncomment this
-  // and recompile. Debug flags have not been parsed yet so these have
-  // not been set.
-  //DebugChannel.on("options");
-
-  Debug("options") << "Options::parseOptions == " << options << std::endl;
-  Debug("options") << "argv == " << argv << std::endl;
-
-  // Find the base name of the program.
-  const char *x = strrchr(progName, '/');
-  if(x != NULL) {
-    progName = x + 1;
-  }
-  binaryName = std::string(progName);
-
-  std::vector<std::string> nonoptions;
-  options->parseOptionsRecursive(argc, argv, &nonoptions);
-  if(Debug.isOn("options")){
-    for(std::vector<std::string>::const_iterator i = nonoptions.begin(),
-          iend = nonoptions.end(); i != iend; ++i){
-      Debug("options") << "nonoptions " << *i << std::endl;
-    }
-  }
-
-  return nonoptions;
-}
-
-std::string suggestCommandLineOptions(const std::string& optionName)
-{
-  DidYouMean didYouMean;
-
-  const char* opt;
-  for(size_t i = 0; (opt = cmdlineOptions[i].name) != nullptr; ++i) {
-    didYouMean.addWord(std::string("--") + cmdlineOptions[i].name);
-  }
-
-  return didYouMean.getMatchAsString(optionName.substr(0, optionName.find('=')));
-}
-
-void Options::parseOptionsRecursive(int argc,
-                                    char* argv[],
-                                    std::vector<std::string>* nonoptions)
-{
-  Options& opts = *this;
-  if(Debug.isOn("options")) {
-    Debug("options") << "starting a new parseOptionsRecursive with "
-                     << argc << " arguments" << std::endl;
-    for( int i = 0; i < argc ; i++ ){
-      Assert(argv[i] != NULL);
-      Debug("options") << "  argv[" << i << "] = " << argv[i] << std::endl;
-    }
-  }
-
-  // Reset getopt(), in the case of multiple calls to parseOptions().
-  // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0.
-  optind = 0;
-#if HAVE_DECL_OPTRESET
-  optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this
-#endif /* HAVE_DECL_OPTRESET */
-
-  // We must parse the binary name, which is manually ignored below. Setting
-  // this to 1 leads to incorrect behavior on some platforms.
-  int main_optind = 0;
-  int old_optind;
-
-
-  while(true) { // Repeat Forever
-
-    optopt = 0;
-    std::string option, optionarg;
-
-    optind = main_optind;
-    old_optind = main_optind;
-
-    // If we encounter an element that is not at zero and does not start
-    // with a "-", this is a non-option. We consume this element as a
-    // non-option.
-    if (main_optind > 0 && main_optind < argc &&
-        argv[main_optind][0] != '-') {
-      Debug("options") << "enqueueing " << argv[main_optind]
-                       << " as a non-option." << std::endl;
-      nonoptions->push_back(argv[main_optind]);
-      ++main_optind;
-      continue;
-    }
-
-
-    Debug("options") << "[ before, main_optind == " << main_optind << " ]"
-                     << std::endl;
-    Debug("options") << "[ before, optind == " << optind << " ]" << std::endl;
-    Debug("options") << "[ argc == " << argc << ", argv == " << argv << " ]"
-                     << std::endl;
-    // clang-format off
-    int c = getopt_long(argc, argv,
-                        "+:${options_short}$",
-                        cmdlineOptions, NULL);
-    // clang-format on
-
-    main_optind = optind;
-
-    Debug("options") << "[ got " << int(c) << " (" << char(c) << ") ]"
-                     << "[ next option will be at pos: " << optind << " ]"
-                     << std::endl;
-
-    // The initial getopt_long call should always determine that argv[0]
-    // is not an option and returns -1. We always manually advance beyond
-    // this element.
-    if ( old_optind == 0  && c == -1 ) {
-      Assert(main_optind > 0);
-      continue;
-    }
-
-    if ( c == -1 ) {
-      if(Debug.isOn("options")) {
-        Debug("options") << "done with option parsing" << std::endl;
-        for(int index = optind; index < argc; ++index) {
-          Debug("options") << "remaining " << argv[index] << std::endl;
-        }
-      }
-      break;
-    }
-
-    option = argv[old_optind == 0 ? 1 : old_optind];
-    optionarg = (optarg == NULL) ? "" : optarg;
-
-    Debug("preemptGetopt") << "processing option " << c
-                           << " (`" << char(c) << "'), " << option << std::endl;
-
-    // clang-format off
-    switch(c)
+  
+void Options::notifyListener(const std::string& key)
+  {
+    if (d_olisten != nullptr)
     {
-${options_handler}$
-
-      case ':' :
-      // This can be a long or short option, and the way to get at the
-      // name of it is different.
-      throw OptionException(std::string("option `") + option
-                            + "' missing its required argument");
-
-      case '?':
-      default:
-        throw OptionException(std::string("can't understand option `") + option
-                              + "'" + suggestCommandLineOptions(option));
+      d_olisten->notifySetOption(key);
     }
   }
-  // clang-format on
-
-  Debug("options") << "got " << nonoptions->size()
-                   << " non-option arguments." << std::endl;
-}
-
-// clang-format off
-std::vector<std::vector<std::string> > Options::getOptions() const
-{
-  std::vector< std::vector<std::string> > opts;
-
-  ${options_getoptions}$
-
-  return opts;
-}
-// clang-format on
-
-void Options::setOption(const std::string& key, const std::string& optionarg)
-{
-  Trace("options") << "setOption(" << key << ", " << optionarg << ")"
-                   << std::endl;
-  // first update this object
-  setOptionInternal(key, optionarg);
-  // then, notify the provided listener
-  if (d_olisten != nullptr)
-  {
-    d_olisten->notifySetOption(key);
-  }
-}
-
-// clang-format off
-void Options::setOptionInternal(const std::string& key,
-                                const std::string& optionarg)
-{
-  options::OptionsHandler* handler = d_handler;
-  Options& opts = *this;
-  ${setoption_handlers}$
-  throw UnrecognizedOptionException(key);
-}
-// clang-format on
-
-// clang-format off
-std::string Options::getOption(const std::string& key) const
-{
-  Trace("options") << "Options::getOption(" << key << ")" << std::endl;
-  const Options& options = *this;
-  ${getoption_handlers}$
-
-  throw UnrecognizedOptionException(key);
-}
-// clang-format on
 
 }  // namespace cvc5
 
diff --git a/src/options/options_template.h b/src/options/options_template.h
index e9a4a6999..a4e595f0d 100644
--- a/src/options/options_template.h
+++ b/src/options/options_template.h
@@ -25,46 +25,20 @@
 
 #include "base/listener.h"
 #include "cvc5_export.h"
-#include "options/language.h"
-#include "options/printer_modes.h"
 
 namespace cvc5 {
-
-namespace api {
-class Solver;
-}
 namespace options {
-  struct OptionsHolder;
   class OptionsHandler;
 // clang-format off
 ${holder_fwd_decls}$
 // clang-format on
-  }  // namespace options
+}  // namespace options
 
 class OptionsListener;
 
 class CVC5_EXPORT Options
 {
-  friend api::Solver;
-
-  /** The handler for the options of the theory. */
-  options::OptionsHandler* d_handler;
-
-// clang-format off
-${holder_mem_decls}$
-// clang-format on
- public:
-// clang-format off
-${holder_ref_decls}$
-// clang-format on
-  
- private:
-
-  /** The current Options in effect */
-  static thread_local Options* s_current;
-
-  friend class options::OptionsHandler;
-
+  public:
   /**
    * Options cannot be copied as they are given an explicit list of
    * Listeners to respond to.
@@ -77,25 +51,25 @@ ${holder_ref_decls}$
    */
   Options& operator=(const Options& options) = delete;
 
-public:
- class OptionsScope
- {
-  private:
-    Options* d_oldOptions;
-  public:
-    OptionsScope(Options* newOptions) :
-        d_oldOptions(Options::s_current)
-    {
-      Options::s_current = newOptions;
-    }
-    ~OptionsScope(){
-      Options::s_current = d_oldOptions;
-    }
- };
+  class OptionsScope
+  {
+   private:
+     Options* d_oldOptions;
+   public:
+     OptionsScope(Options* newOptions) :
+         d_oldOptions(Options::s_current)
+     {
+       Options::s_current = newOptions;
+     }
+     ~OptionsScope(){
+       Options::s_current = d_oldOptions;
+     }
+  };
+  friend class OptionsScope;
 
   /** Return true if current Options are null */
   static inline bool isCurrentNull() {
-    return s_current == NULL;
+    return s_current == nullptr;
   }
 
   /** Get the current Options in effect */
@@ -117,103 +91,31 @@ public:
    */
   void copyValues(const Options& options);
 
-  /**
-   * Set the value of the given option by key.
-   *
-   * Throws OptionException or ModalException on failures.
-   */
-  void setOption(const std::string& key, const std::string& optionarg);
-
-  /**
-   * Gets the value of the given option by key and returns value as a string.
-   *
-   * Throws OptionException on failures, such as key not being the name of an
-   * option.
-   */
-  std::string getOption(const std::string& key) const;
-
-  // Static accessor functions.
-  // TODO: Document these.
-  static std::ostream* currentGetOut();
-
-  /**
-   * Get a description of the command-line flags accepted by
-   * parseOptions.  The returned string will be escaped so that it is
-   * suitable as an argument to printf. */
-  std::string getDescription() const;
-
-  /**
-   * Print overall command-line option usage message, prefixed by
-   * "msg"---which could be an error message causing the usage
-   * output in the first place, e.g. "no such option --foo"
-   */
-  static void printUsage(const std::string msg, std::ostream& out);
-
-  /**
-   * Print command-line option usage message for only the most-commonly
-   * used options.  The message is prefixed by "msg"---which could be
-   * an error message causing the usage output in the first place, e.g.
-   * "no such option --foo"
-   */
-  static void printShortUsage(const std::string msg, std::ostream& out);
-
-  /** Print help for the --lang command line option */
-  static void printLanguageHelp(std::ostream& out);
-
-  /**
-   * Initialize the Options object options based on the given
-   * command-line arguments given in argc and argv.  The return value
-   * is what's left of the command line (that is, the non-option
-   * arguments).
-   *
-   * This function uses getopt_long() and is not thread safe.
-   *
-   * Throws OptionException on failures.
-   *
-   * Preconditions: options and argv must be non-null.
-   */
-  static std::vector<std::string> parseOptions(Options* options,
-                                               int argc,
-                                               char* argv[],
-                                               std::string& binaryName);
-
-  /**
-   * Get the setting for all options.
-   */
-  std::vector<std::vector<std::string> > getOptions() const;
-
   /** Set the generic listener associated with this class to ol */
   void setListener(OptionsListener* ol);
 
-  /** Sends a std::flush to getErr(). */
-  void flushErr();
-
-  /** Sends a std::flush to getOut(). */
-  void flushOut();
+  void notifyListener(const std::string& key);
 
  private:
   /** Pointer to the options listener, if one exists */
-  OptionsListener* d_olisten;
-  /**
-   * Helper method for setOption, updates this object for setting the given
-   * option.
-   */
-  void setOptionInternal(const std::string& key, const std::string& optionarg);
-  /**
-   * Internal procedure for implementing the parseOptions function.
-   * Initializes the options object based on the given command-line
-   * arguments. The command line arguments are stored in argc/argv.
-   * Nonoptions are stored into nonoptions.
-   *
-   * This is not thread safe.
-   *
-   * Throws OptionException on failures.
-   *
-   * Preconditions: options, extender and nonoptions are non-null.
-   */
-  void parseOptionsRecursive(int argc,
-                                    char* argv[],
-                                    std::vector<std::string>* nonoptions);
+  OptionsListener* d_olisten = nullptr;
+
+// clang-format off
+${holder_mem_decls}$
+// clang-format on
+ public:
+// clang-format off
+${holder_ref_decls}$
+// clang-format on
+  
+ private:
+  /** The handler for the options of the theory. */
+  std::unique_ptr<options::OptionsHandler> d_handler;
+
+  /** The current Options in effect */
+  static thread_local Options* s_current;
+
+
 }; /* class Options */
 
 }  // namespace cvc5