New version of the recursive options parsing strategy.

10 files changed, 492 insertions, 296 deletions

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index b83907bd3..f45f1d9f3 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -101,7 +101,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   progPath = argv[0];
 
   // Parse the options
-  vector<string> filenames = opts.parseOptions(argc, argv);
+  vector<string> filenames = Options::parseOptions(&opts, argc, argv);
 
 # ifndef PORTFOLIO_BUILD
   if( opts.wasSetByUserThreads() ||
diff --git a/src/main/portfolio_util.cpp b/src/main/portfolio_util.cpp
index e42787fea..60d591c28 100644
--- a/src/main/portfolio_util.cpp
+++ b/src/main/portfolio_util.cpp
@@ -92,7 +92,7 @@ void parseThreadSpecificOptions(OptionsList& threadOptions, const Options& opts)
       *vp++ = NULL;
       if(targc > 1) { // this is necessary in case you do e.g. --thread0="  "
         try {
-          tOpts.parseOptions(targc, targv);
+          Options::parseOptions(&tOpts, targc, targv);
         } catch(OptionException& e) {
           stringstream ss;
           ss << optid << ": " << e.getMessage();
diff --git a/src/options/Makefile.am b/src/options/Makefile.am
index 8a465c522..643932781 100644
--- a/src/options/Makefile.am
+++ b/src/options/Makefile.am
@@ -206,7 +206,8 @@ liboptions_la_SOURCES = \
 	arith_propagation_mode.h \
 	arith_unate_lemma_mode.cpp \
 	arith_unate_lemma_mode.h \
-	argument_extender.cpp \
+	argument_extender_implementation.cpp \
+	argument_extender_implementation.h \
 	argument_extender.h \
 	base_handlers.h \
 	boolean_term_conversion_mode.cpp \
diff --git a/src/options/argument_extender.cpp b/src/options/argument_extender.cpp
deleted file mode 100644
index d55610590..000000000
--- a/src/options/argument_extender.cpp
+++ /dev/null
@@ -1,74 +0,0 @@
-/*********************                                                        */
-/*! \file preempt_get_option.h
- ** \verbatim
- ** Original author: Tim King
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Utility function for parsing commandline options.
- **
- ** Utility function for parsing commandline options.
- **/
-
-#include "options/argument_extender.h"
-
-#include <cstdlib>
-#include <cstring>
-#include <vector>
-
-#include "base/cvc4_assert.h"
-#include "base/output.h"
-
-namespace CVC4 {
-namespace options {
-
-ArgumentExtender::ArgumentExtender(unsigned additional, size_t length)
-    : d_additional(additional)
-    , d_length(length)
-{
-  AlwaysAssert(d_additional >= 1);
-  AlwaysAssert(d_length >= 1);
-}
-
-ArgumentExtender::~ArgumentExtender(){}
-
-unsigned ArgumentExtender::getIncrease() const { return d_additional; }
-size_t ArgumentExtender::getLength() const { return d_length; }
-
-void ArgumentExtender::extend(int& argc, char**& argv, const char* opt,
-                                std::vector<char*>& allocated)
-{
-
-  Debug("preemptGetopt") << "preempting getopt() with " << opt << std::endl;
-
-  AlwaysAssert(opt != NULL && *opt != '\0');
-  AlwaysAssert(strlen(opt) <= getLength());
-
-  ++argc;
-  unsigned i = 1;
-  while(argv[i] != NULL && argv[i][0] != '\0') {
-    ++i;
-  }
-
-  if(argv[i] == NULL) {
-    unsigned newSize = i + getIncrease();
-    argv = (char**) realloc(argv, newSize * sizeof(char*));
-    for(unsigned j = i; j < newSize-1; ++j) {
-      char* newString = (char*) malloc(sizeof(char) * getLength());
-      newString[0] = '\0';
-      argv[j] = newString;
-      allocated.push_back(newString);
-    }
-    argv[newSize - 1] = NULL;
-  }
-
-  strncpy(argv[i], opt, getLength() - 1);
-  argv[i][getLength() - 1] = '\0'; // ensure NULL-termination even on overflow
-}
-
-}/* CVC4::options namespace */
-}/* CVC4 namespace */
diff --git a/src/options/argument_extender.h b/src/options/argument_extender.h
index 1f7e3c1dd..4c27317b4 100644
--- a/src/options/argument_extender.h
+++ b/src/options/argument_extender.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file preempt_get_option.h
+/*! \file argument_extender.h
  ** \verbatim
  ** Original author: Tim King
  ** Major contributors: none
@@ -9,71 +9,77 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Utility function for extending commandline options.
+ ** \brief Abstract utility class for extending commandline options.
  **
- ** Utility function for extending commandline options.
+ ** Abstract utility class for extending commandline options.
  **/
 
-#include "cvc4_private.h"
+#include "cvc4_public.h"
 
-#ifndef __CVC4__OPTIONS__PREMPT_GET_OPTION_H
-#define __CVC4__OPTIONS__PREMPT_GET_OPTION_H
+#ifndef __CVC4__OPTIONS__ARGUMENT_EXTENDER_H
+#define __CVC4__OPTIONS__ARGUMENT_EXTENDER_H
 
 #include <cstddef>
-#include <vector>
 
 namespace CVC4 {
 namespace options {
 
-
+/**
+ * Abstract utility class for implementing command line options
+ * parsing for the Options class. This allows for adding preemption
+ * arguments. A preemption is effectivly adding a new argument into
+ * the commandline arguments and must be processed immediately.
+ */
 class ArgumentExtender {
- public:
+public:
+  ArgumentExtender(){}
+  virtual ~ArgumentExtender(){}
+
   /**
+   * This creates a copy of the current arguments list as a new array.
+   * The new array is stored in argv.  The user of this function is
+   * expected to own the memory of the string array, but not the
+   * strings themselves.  The length of the new array is
+   * numArguments() and is stored in argc.
+   *
    * Preconditions:
-   *  additional >= 1
-   *  length >= 1
+   * - argc and argv are non-null.
    */
-  ArgumentExtender(unsigned additional, size_t length);
-  ~ArgumentExtender();
+  virtual void getArguments(int* argc, char*** argv) const = 0;
+
+  /** Returns the number of arguments that are . */
+  virtual size_t numArguments() const = 0;
 
   /**
-   * This purpose of this function is to massage argc and argv upon the event
-   * of parsing during Options::parseOptions of an option with the :link or
-   * :link-alternative attributes. The purpose of the function is to extend argv
-   * with another commandline argument.
-   *
-   * Preconditions:
-   *  opt is '\0' terminated, non-null and non-empty c-string.
-   *  strlen(opt) <= getLength()
-   *
-   * Let P be the first position in argv that is >= 1 and is either NULL or
-   * empty:
-   *   argv[P] == NULL || argv[P] == '\0'
-   *
-   * This has a very specific set of side effects:
-   * - argc is incremented by one.
-   * - If argv[P] == NULL, this reallocates argv to have (P+additional)
-   *   elements.
-   * - The 0 through P-1 elements of argv are the same.
-   * - The P element of argv is a copy of the first len-1 characters of opt.
-   *   This is a newly allocated '\0' terminated c string of length len.
-   * - The P+1 through (P+additional-2) elements of argv are newly allocated
-   *   empty '\0' terminated c strings of size len.
-   * - The last element at (P+additional-1) of argv is NULL.
-   * - All allocations are pushed back onto allocated.
+   * Inserts a copy of element into the front of the arguments list.
+   * Preconditions: element is non-null and 0 terminated.
+   */
+  virtual void pushFrontArgument(const char* element) = 0;
+
+  /**
+   * Inserts a copy of element into the back of the arguments list.
+   * Preconditions: element is non-null and 0 terminated.
+   */
+  virtual void pushBackArgument(const char* element) = 0;
+
+  /** Removes the front of the arguments list.*/
+  virtual void popFrontArgument() = 0;
+
+  /** Adds a new preemption to the arguments list. */
+  virtual void pushBackPreemption(const char* element) = 0;
+
+  /**
+   * Moves all of the preemptions into the front of the arguments
+   * list.
    */
-  void extend(int& argc, char**& argv, const char* opt,
-              std::vector<char*>& allocated);
+  virtual void movePreemptionsToArguments() = 0;
 
-  unsigned getIncrease() const;
-  size_t getLength() const;
+  /** Returns true iff there is a pending preemption.*/
+  virtual bool hasPreemptions() const = 0;
 
- private:
-  unsigned d_additional;
-  size_t d_length;
-};
+};/* class ArgumentExtender */
 
 }/* CVC4::options namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__OPTIONS__PREMPT_GET_OPTION_H */
+#endif /* __CVC4__OPTIONS__ARGUMENT_EXTENDER_H */
diff --git a/src/options/argument_extender_implementation.cpp b/src/options/argument_extender_implementation.cpp
new file mode 100644
index 000000000..c27c70dc2
--- /dev/null
+++ b/src/options/argument_extender_implementation.cpp
@@ -0,0 +1,114 @@
+/*********************                                                        */
+/*! \file argument_extender_implementation.cpp
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Utility class for parsing commandline options.
+ **
+ ** Utility class for parsing commandline options.
+ **/
+
+#include "options/argument_extender_implementation.h"
+
+#include <cstdlib>
+#include <cstring>
+#include <list>
+
+#include "base/cvc4_assert.h"
+#include "base/output.h"
+#include "options/argument_extender.h"
+
+namespace CVC4 {
+namespace options {
+
+ArgumentExtenderImplementation::ArgumentExtenderImplementation()
+  : d_allocated()
+  , d_preemptions()
+  , d_arguments()
+{
+}
+
+ArgumentExtenderImplementation::~ArgumentExtenderImplementation(){
+  for(CharPointerList::iterator i = d_allocated.begin(),
+        iend = d_allocated.end(); i != iend; ++i) {
+    char* current = *i;
+    Debug("options") << "~ArgumentExtenderImplementation " << current
+    << std::endl;
+    free(current);
+  }
+  d_allocated.clear();
+}
+
+size_t ArgumentExtenderImplementation::numArguments() const {
+  return d_arguments.size();
+}
+
+char* ArgumentExtenderImplementation::allocateCopy(const char* element) {
+  Assert(element != NULL);
+
+  char* duplicate = strdup(element);
+  Assert(duplicate != NULL);
+  d_allocated.push_back(duplicate);
+  return duplicate;
+}
+
+bool ArgumentExtenderImplementation::hasPreemptions() const {
+  return !d_preemptions.empty();
+}
+
+void ArgumentExtenderImplementation::pushBackPreemption(const char* element) {
+  d_preemptions.push_back(allocateCopy(element));
+}
+
+void ArgumentExtenderImplementation::movePreemptionsToArguments() {
+  d_arguments.splice(d_arguments.begin(), d_preemptions);
+}
+
+void ArgumentExtenderImplementation::popFrontArgument() {
+  Assert(!d_arguments.empty());
+  Debug("options") << "ArgumentExtenderImplementation::popFrontArgument "
+                   << d_arguments.front() << std::endl;
+  d_arguments.pop_front();
+}
+
+void ArgumentExtenderImplementation::pushFrontArgument(const char* element) {
+  d_arguments.push_front(allocateCopy(element));
+}
+
+void ArgumentExtenderImplementation::pushBackArgument(const char* element) {
+  d_arguments.push_back(allocateCopy(element));
+}
+
+void ArgumentExtenderImplementation::getArguments(int* argc, char*** argv)
+  const {
+  Assert(argc != NULL);
+  Assert(argv != NULL);
+
+  *argc = numArguments();
+  *argv = copyArguments();
+}
+
+char** ArgumentExtenderImplementation::copyArguments() const {
+  int size = numArguments();
+  Assert(size >= 0);
+
+  char** array = (char**) malloc( sizeof(char*) * size );
+  Assert(array != NULL);
+  int position = 0;
+  for(std::list< char* >::const_iterator i = d_arguments.begin(),
+        iend = d_arguments.end(); i != iend; ++i, ++position) {
+    char* at_position = *i;
+    array[position] = at_position;
+  }
+
+  return array;
+}
+
+}/* CVC4::options namespace */
+}/* CVC4 namespace */
diff --git a/src/options/argument_extender_implementation.h b/src/options/argument_extender_implementation.h
new file mode 100644
index 000000000..13ec71467
--- /dev/null
+++ b/src/options/argument_extender_implementation.h
@@ -0,0 +1,115 @@
+/*********************                                                        */
+/*! \file argument_extender_implementation.h
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Utility class for extending commandline options.
+ **
+ ** Utility class for extending commandline options.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__OPTIONS__ARGUMENT_EXTENDER_IMPLEMENTATION_H
+#define __CVC4__OPTIONS__ARGUMENT_EXTENDER_IMPLEMENTATION_H
+
+#include <cstddef>
+#include <list>
+
+#include "options/argument_extender.h"
+
+namespace CVC4 {
+namespace options {
+
+/**
+ * Utility class for implementing command line options parsing for the
+ * Options class. This allows for adding preemption arguments.
+ * Preemptions are processed immediately after the current argument.
+ */
+class ArgumentExtenderImplementation : public ArgumentExtender {
+ public:
+  /** Constructs a new empty ArgumentExtender.*/
+  ArgumentExtenderImplementation();
+
+  /** Destroys an ArgumentExtender and frees its associated memory.*/
+  ~ArgumentExtenderImplementation();
+
+  /**
+   * This creates a copy of the current arguments list as a new array.
+   * The new array is stored in argv.  The user of this function is
+   * expected to own the memory of the string array, but not the
+   * strings themselves.  The length of the new array is
+   * numArguments() and is stored in argc.
+   *
+   * Preconditions:
+   * - argc and argv are non-null.
+   */
+  void getArguments(int* argc, char*** argv) const;
+
+  /** Returns the number of arguments that are . */
+  size_t numArguments() const;
+
+  /**
+   * Inserts a copy of element into the front of the arguments list.
+   * Preconditions: element is non-null and 0 terminated.
+   */
+  void pushFrontArgument(const char* element);
+
+  /**
+   * Inserts a copy of element into the back of the arguments list.
+   * Preconditions: element is non-null and 0 terminated.
+   */
+  void pushBackArgument(const char* element);
+
+  /** Removes the front of the arguments list.*/
+  void popFrontArgument();
+
+  /** Adds a new preemption to the arguments list. */
+  void pushBackPreemption(const char* element);
+
+  /**
+   * Moves all of the preemptions into the front of the arguments
+   * list.
+   */
+  void movePreemptionsToArguments();
+
+  /** Returns true iff there is a pending preemption.*/
+  bool hasPreemptions() const;
+
+private:
+
+  typedef std::list< char* > CharPointerList;
+
+  /** Creates of copy of the arugments list.*/
+  char** copyArguments() const;
+
+  /** Allocates a copy and stores a copy in d_allocated.*/
+  char* allocateCopy(const char* element);
+
+  /** Contains a copy of the allocated strings.*/
+  CharPointerList d_allocated;
+
+  /**
+   * A list of all of the preempted arguments. All of these pointers
+   * in this list should be contained in d_allocated.
+   */
+  CharPointerList d_preemptions;
+
+  /**
+   * A list of all of the arguments. All of these pointers in this
+   * list should be contained in d_allocated.
+   */
+  CharPointerList d_arguments;
+
+};/* class ArgumentExtenderImplementation */
+
+}/* CVC4::options namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__OPTIONS__ARGUMENT_EXTENDER_IMPLEMENTATION_H */
diff --git a/src/options/mkoptions b/src/options/mkoptions
index ad8d7033f..dd5575644 100755
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -604,7 +604,7 @@ template <> bool Options::wasSetByUser(options::${internal}__option_t) const { r
     for link in $links; do
       run_links="$run_links
 #line $lineno \"$kf\"
-      argumentExtender.extend(extra_argc, extra_argv, \"$link\", allocated);"
+      extender->pushBackPreemption(\"$link\");"
     done
   fi
   if [ -n "$smt_links" ]; then
@@ -623,7 +623,7 @@ template <> bool Options::wasSetByUser(options::${internal}__option_t) const { r
     for link in $links_alternate; do
       run_links_alternate="$run_links_alternate
 #line $lineno \"$kf\"
-      argumentExtender.extend(extra_argc, extra_argv, \"$link\", allocated);"
+      extender->pushBackPreemption(\"$link\");"
     done
   fi
   if [ -n "$notifications" ]; then
@@ -657,7 +657,7 @@ template <> void runBoolPredicates(options::${internal}__option_t, std::string o
     if [ "$type" = bool ]; then
       all_modules_option_handlers="${all_modules_option_handlers}${cases}
 #line $lineno \"$kf\"
-      assignBool(options::$internal, option, true);$run_links
+      options->assignBool(options::$internal, option, true);$run_links
       break;
 "
     elif [ -n "$expect_arg" -a "$internal" != - ]; then
@@ -690,7 +690,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
 }"
       all_modules_option_handlers="${all_modules_option_handlers}${cases}
 #line $lineno \"$kf\"
-      assign(options::$internal, option, optionarg);$run_links
+      options->assign(options::$internal, option, optionarg);$run_links
       break;
 "
     elif [ -n "$expect_arg" ]; then
@@ -733,7 +733,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
     if [ "$type" = bool ]; then
       all_modules_option_handlers="${all_modules_option_handlers}${cases_alternate}
 #line $lineno \"$kf\"
-      assignBool(options::$internal, option, false);$run_links_alternate
+      options->assignBool(options::$internal, option, false);$run_links_alternate
       break;
 "
     else
@@ -1013,12 +1013,12 @@ function handle_alias {
     fi
     links="$links
 #line $lineno \"$kf\"
-      argumentExtender.extend(extra_argc, extra_argv, \"$linkopt\", allocated);"
+      extender->pushBackPreemption(\"$linkopt\");"
     if [ "$linkarg" ]; then
       # include also the arg
       links="$links
 #line $lineno \"$kf\"
-      argumentExtender.extend(extra_argc, extra_argv, optionarg.c_str(), allocated);"
+      extender->pushBackPreemption(optionarg.c_str());"
     fi
     shift
   done
diff --git a/src/options/options.h b/src/options/options.h
index 8fb52146f..6f0955bb9 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -27,6 +27,7 @@
 #include "base/listener.h"
 #include "base/modal_exception.h"
 #include "base/tls.h"
+#include "options/argument_extender.h"
 #include "options/language.h"
 #include "options/printer_modes.h"
 #include "options/option_exception.h"
@@ -314,12 +315,18 @@ public:
   static std::vector<std::string> suggestSmtOptions(const std::string& optionName) throw();
 
   /**
-   * Initialize the options based on the given command-line arguments.
-   * The return value is what's left of the command line (that is, the
-   * non-option arguments).
+   * 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.
+   *
+   * Preconditions: options and argv must be non-null.
    */
-  std::vector<std::string> parseOptions(int argc, char* argv[])
-      throw(OptionException);
+  static std::vector<std::string> parseOptions(Options* options,
+                                               int argc, char* argv[])
+    throw(OptionException);
 
   /**
    * Get the setting for all options.
@@ -528,6 +535,22 @@ public:
   /** Sends a std::flush to getOut(). */
   void flushOut();
 
+ private:
+
+  /**
+   * Internal procedure for implementing the parseOptions function.
+   * Initializes the options object based on the given command-line
+   * arguments. This uses an ArgumentExtender containing the
+   * command-line arguments. Nonoptions are stored into nonoptions.
+   *
+   * This is not thread safe.
+   *
+   * Preconditions: options, extender and nonoptions are non-null.
+   */
+  static void parseOptionsRecursive(Options* options,
+                                    options::ArgumentExtender* extender,
+                                    std::vector<std::string>* nonoptions)
+    throw(OptionException);
 };/* class Options */
 
 }/* CVC4 namespace */
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index 51b2bea5e..98db4951b 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -53,13 +53,14 @@ extern int optreset;
 #include "base/output.h"
 #include "base/tls.h"
 #include "options/argument_extender.h"
+#include "options/argument_extender_implementation.h"
 #include "options/didyoumean.h"
 #include "options/language.h"
 #include "options/options_handler.h"
 
 ${include_all_option_headers}
 
-#line 63 "${template}"
+#line 64 "${template}"
 
 #include "options/options_holder.h"
 #include "cvc4autoconfig.h"
@@ -67,7 +68,7 @@ ${include_all_option_headers}
 
 ${option_handler_includes}
 
-#line 71 "${template}"
+#line 72 "${template}"
 
 using namespace CVC4;
 using namespace CVC4::options;
@@ -389,7 +390,7 @@ Options::registerSetReplayLogFilename(
 
 ${all_custom_handlers}
 
-#line 393 "${template}"
+#line 394 "${template}"
 
 #ifdef CVC4_DEBUG
 #  define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true
@@ -407,18 +408,18 @@ options::OptionsHolder::OptionsHolder() : ${all_modules_defaults}
 {
 }
 
-#line 411 "${template}"
+#line 412 "${template}"
 
 static const std::string mostCommonOptionsDescription = "\
 Most commonly-used CVC4 options:${common_documentation}";
 
-#line 416 "${template}"
+#line 417 "${template}"
 
 static const std::string optionsDescription = mostCommonOptionsDescription + "\n\
 \n\
 Additional CVC4 options:${remaining_documentation}";
 
-#line 422 "${template}"
+#line 423 "${template}"
 
 static const std::string optionsFootnote = "\n\
 [*] Each of these options has a --no-OPTIONNAME variant, which reverses the\n\
@@ -431,7 +432,7 @@ Languages currently supported as arguments to the -L / --lang option:\n\
   cvc4 | presentation | pl       CVC4 presentation language\n\
   smt1 | smtlib1                 SMT-LIB format 1.2\n\
   smt | smtlib | smt2 |\n\
-    smt2.0 | smtlib2 | smtlib2.0 SMT-LIB format 2.0\n\
+  smt2.0 | smtlib2 | smtlib2.0   SMT-LIB format 2.0\n\
   smt2.5 | smtlib2.5             SMT-LIB format 2.5\n\
   tptp                           TPTP format (cnf and fof)\n\
   sygus                          SyGuS format\n\
@@ -442,7 +443,7 @@ Languages currently supported as arguments to the --output-lang option:\n\
   cvc3                           CVC3 presentation language\n\
   smt1 | smtlib1                 SMT-LIB format 1.2\n\
   smt | smtlib | smt2 |\n\
-    smt2.0 | smtlib2.0 | smtlib2   SMT-LIB format 2.0\n\
+  smt2.0 | smtlib2.0 | smtlib2   SMT-LIB format 2.0\n\
   smt2.5 | smtlib2.5             SMT-LIB format 2.5\n\
   tptp                           TPTP format\n\
   z3str                          SMT-LIB 2.0 with Z3-str string constraints\n\
@@ -497,7 +498,7 @@ static struct option cmdlineOptions[] = {${all_modules_long_options}
   { NULL, no_argument, NULL, '\0' }
 };/* cmdlineOptions */
 
-#line 501 "${template}"
+#line 502 "${template}"
 
 // static void preemptGetopt(int& argc, char**& argv, const char* opt) {
 
@@ -549,178 +550,196 @@ public:
  * The return value is what's left of the command line (that is, the
  * non-option arguments).
  */
-std::vector<std::string> Options::parseOptions(int argc, char* main_argv[]) throw(OptionException) {
-  options::OptionsGuard guard(&s_current, this);
+std::vector<std::string> Options::parseOptions(Options* options,
+                                               int argc, char* argv[])
+  throw(OptionException) {
 
-  // Having this synonym simplifies the generation code in mkoptions.
-  options::OptionsHandler* handler = d_handler;
+  Assert(options != NULL);
+  Assert(argv != NULL);
 
-  const char *progName = main_argv[0];
+  options::OptionsGuard guard(&s_current, options);
 
-  ArgumentExtender argumentExtender(s_preemptAdditional, s_maxoptlen);
-  std::vector<char*> allocated;
+  const char *progName = argv[0];
 
-  Debug("options") << "main_argv == " << main_argv << std::endl;
+  // 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");
 
-  // 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 */
+  Debug("options") << "Options::parseOptions == " << options << std::endl;
+  Debug("options") << "argv == " << argv << std::endl;
 
-  // find the base name of the program
+  // Find the base name of the program.
   const char *x = strrchr(progName, '/');
   if(x != NULL) {
     progName = x + 1;
   }
-  d_holder->binary_name = std::string(progName);
+  options->d_holder->binary_name = std::string(progName);
+
+  ArgumentExtender* argumentExtender = new ArgumentExtenderImplementation();
+  for(int position = 1; position < argc; position++) {
+    argumentExtender->pushBackArgument(argv[position]);
+  }
+
+  std::vector<std::string> nonoptions;
+  parseOptionsRecursive(options, argumentExtender, &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;
+    }
+  }
+
+  delete argumentExtender;
+  return nonoptions;
+}
+
+void Options::parseOptionsRecursive(Options* options,
+                                    ArgumentExtender* extender,
+                                    std::vector<std::string>* nonoptions)
+  throw(OptionException) {
+
+  int argc;
+  char** argv;
+
+  extender->movePreemptionsToArguments();
+  extender->pushFrontArgument("");
+  extender->getArguments(&argc, &argv);
+
+  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;
+    }
+  }
 
-  int extra_argc = 1;
-  char **extra_argv = (char**) malloc(2 * sizeof(char*));
-  extra_argv[0] = NULL;
-  extra_argv[1] = NULL;
+  // Having this synonym simplifies the generation code in mkoptions.
+  options::OptionsHandler* handler = options->d_handler;
+  options::OptionsHolder* holder = options->d_holder;
 
-  int extra_optind = 0, main_optind = 0;
+  // 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 */
+
+  
+  int main_optind = 0;
   int old_optind;
-  int *optind_ref = &main_optind;
 
-  char** argv = main_argv;
 
-  std::vector<std::string> nonOptions;
+  while(true) { // Repeat Forever
+
+    if(extender->hasPreemptions()){
+      // Stop this round of parsing. We now parse recursively
+      // to start on a new character array for argv.
+      parseOptionsRecursive(options, extender, nonoptions);
+      break;
+    }
 
-  for(;;) {
-    int c = -1;
     optopt = 0;
     std::string option, optionarg;
-    Debug("preemptGetopt") << "top of loop, extra_optind == " << extra_optind
-                           << ", extra_argc == " << extra_argc << std::endl;
-    if((extra_optind == 0 ? 1 : extra_optind) < extra_argc) {
-#if HAVE_DECL_OPTRESET
-      if(optind_ref != &extra_optind) {
-        optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this
-      }
-#endif /* HAVE_DECL_OPTRESET */
-      old_optind = optind = extra_optind;
-      optind_ref = &extra_optind;
-      argv = extra_argv;
-      Debug("preemptGetopt") << "in preempt code, next arg is "
-                             << extra_argv[optind == 0 ? 1 : optind]
-                             << std::endl;
-      if(extra_argv[extra_optind == 0 ? 1 : extra_optind][0] != '-') {
-        InternalError(
-            "preempted args cannot give non-options command-line args (found `%s')",
-            extra_argv[extra_optind == 0 ? 1 : extra_optind]);
-      }
-      c = getopt_long(extra_argc, extra_argv,
-                      "+:${all_modules_short_options}",
-                      cmdlineOptions, NULL);
-      Debug("preemptGetopt") << "in preempt code"
-                             << ", c == " << c << " (`" << char(c) << "')"
-                             << " optind == " << optind << std::endl;
-      if(optopt == 0 ||
-         ( optopt >= ${long_option_value_begin} && optopt <= ${long_option_value_end} )) {
-        // long option
-        option = argv[old_optind == 0 ? 1 : old_optind];
-        optionarg = (optarg == NULL) ? "" : optarg;
-      } else {
-        // short option
-        option = std::string("-") + char(optopt);
-        optionarg = (optarg == NULL) ? "" : optarg;
-      }
-      if(optind >= extra_argc) {
-        Debug("preemptGetopt") << "-- no more preempt args" << std::endl;
-        unsigned i = 1;
-        while(extra_argv[i] != NULL && extra_argv[i][0] != '\0') {
-          extra_argv[i][0] = '\0';
-          ++i;
-        }
-        extra_argc = 1;
-        extra_optind = 0;
-      } else {
-        Debug("preemptGetopt") << "-- more preempt args" << std::endl;
-        extra_optind = optind;
-      }
+
+    optind = main_optind;
+    old_optind = main_optind;
+    //optind_ref = &main_optind;
+    //argv = main_argv;
+
+    // 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;
+      extender->popFrontArgument();
+      continue;
     }
-    if(c == -1) {
-#if HAVE_DECL_OPTRESET
-      if(optind_ref != &main_optind) {
-        optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this
-      }
-#endif /* HAVE_DECL_OPTRESET */
-      old_optind = optind = main_optind;
-      optind_ref = &main_optind;
-      argv = main_argv;
-      if(main_optind < argc && main_argv[main_optind][0] != '-') {
-        do {
-          if(main_optind != 0) {
-            nonOptions.push_back(main_argv[main_optind]);
-          }
-          ++main_optind;
-        } while(main_optind < argc && main_argv[main_optind][0] != '-');
-        continue;
-      }
-      Debug("options") << "[ before, optind == " << optind << " ]" << std::endl;
-#if defined(__MINGW32__) || defined(__MINGW64__)
-      if(optreset == 1 && optind > 1) {
-        // on mingw, optreset will reset the optind, so we have to
-        // manually advance argc, argv
-        main_argv[optind - 1] = main_argv[0];
-        argv = main_argv += optind - 1;
-        argc -= optind - 1;
-        old_optind = optind = main_optind = 1;
-        if(argc > 0) {
-          Debug("options") << "looking at : " << argv[0] << std::endl;
-        }
-        /*c = getopt_long(argc, main_argv,
+
+
+    Debug("options") << "[ before, main_optind == " << main_optind << " ]"
+                     << std::endl;
+    Debug("options") << "[ before, optind == " << optind << " ]" << std::endl;
+    Debug("options") << "[ argc == " << argc << ", argv == " << argv << " ]"
+                     << std::endl;
+    int c = getopt_long(argc, argv,
                         "+:${all_modules_short_options}",
                         cmdlineOptions, NULL);
-        Debug("options") << "pre-emptory c is " << c << " (" << char(c) << ")" << std::endl;
-        Debug("options") << "optind was reset to " << optind << std::endl;
-        optind = main_optind;
-        Debug("options") << "I restored optind to " << optind << std::endl;*/
-      }
-#endif /* __MINGW32__ || __MINGW64__ */
-      Debug("options") << "[ argc == " << argc
-                       << ", main_argv == " << main_argv << " ]" << std::endl;
-      c = getopt_long(argc, main_argv,
-                      "+:${all_modules_short_options}",
-                      cmdlineOptions, NULL);
-      main_optind = optind;
-      Debug("options") << "[ got " << int(c) << " (" << char(c) << ") ]"
-                       << std::endl;
-      Debug("options") << "[ next option will be at pos: " << optind << " ]"
-                       << std::endl;
-      if(c == -1) {
+
+    while(main_optind < optind) {
+      main_optind++;
+      extender->popFrontArgument();
+    }
+
+    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.
+    //
+    // We have to reinitialize optind to 0 instead of 1 as we need to support
+    // changing the argv array passed to getopt.
+    // This is needed as are using GNU extensions.
+    // From: http://man7.org/linux/man-pages/man3/getopt.3.html
+    // A program that scans multiple argument vectors, or rescans the same
+    // vector more than once, and wants to make use of GNU extensions such
+    // as '+' and '-' at the start of optstring, or changes the value of
+    //  POSIXLY_CORRECT between scans, must reinitialize getopt() by
+    //  resetting optind to 0, rather than the traditional value of 1.
+    //  (Resetting to 0 forces the invocation of an internal initialization
+    //  routine that rechecks POSIXLY_CORRECT and checks for GNU extensions
+    //  in optstring.)
+    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;
-        break;
+        for(int index = optind; index < argc; ++index) {
+          Debug("options") << "remaining " << argv[index] << std::endl;
+        }
       }
-      option = argv[old_optind == 0 ? 1 : old_optind];
-      optionarg = (optarg == NULL) ? "" : optarg;
+      break;
     }
 
+    option = argv[old_optind == 0 ? 1 : old_optind];
+    optionarg = (optarg == NULL) ? "" : optarg;
+
     Debug("preemptGetopt") << "processing option " << c
                            << " (`" << char(c) << "'), " << option << std::endl;
 
     switch(c) {
 ${all_modules_option_handlers}
 
-#line 709 "${template}"
+#line 722 "${template}"
 
     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");
+      throw OptionException(std::string("option `") + option +
+                            "' missing its required argument");
 
     case '?':
     default:
-      if( ( optopt == 0 || ( optopt >= ${long_option_value_begin} && optopt <= ${long_option_value_end} ) ) &&
-          !strncmp(argv[optind - 1], "--thread", 8) &&
-          strlen(argv[optind - 1]) > 8 ) {
+      if( ( optopt == 0 ||
+            ( optopt >= ${long_option_value_begin} &&
+              optopt <= ${long_option_value_end} )
+          ) && !strncmp(argv[optind - 1], "--thread", 8) &&
+          strlen(argv[optind - 1]) > 8 )
+      {
         if(! isdigit(argv[optind - 1][8])) {
           throw OptionException(formatThreadOptionException(option));
         }
-        std::vector<std::string>& threadArgv = d_holder->threadArgv;
+        std::vector<std::string>& threadArgv = holder->threadArgv;
         char *end;
         long tnum = strtol(argv[optind - 1] + 8, &end, 10);
         if(tnum < 0 || (*end != '\0' && *end != '=')) {
@@ -734,23 +753,24 @@ ${all_modules_option_handlers}
         }
         if(*end == '\0') { // e.g., we have --thread0 "foo"
           if(argc <= optind) {
-            throw OptionException(std::string("option `") + option
-                                  + "' missing its required argument");
+            throw OptionException(std::string("option `") + option +
+                                  "' missing its required argument");
           }
           Debug("options") << "thread " << tnum << " gets option "
                            << argv[optind] << std::endl;
-          threadArgv[tnum] += argv[(*optind_ref)++];
+          threadArgv[tnum] += argv[main_optind];
+          main_optind++;
         } else { // e.g., we have --thread0="foo"
           if(end[1] == '\0') {
             throw OptionException(std::string("option `") + option +
                                   "' missing its required argument");
           }
-          Debug("options") << "thread " << tnum << " gets option " << (end + 1)
-                           << std::endl;
+          Debug("options") << "thread " << tnum << " gets option "
+                           << (end + 1) << std::endl;
           threadArgv[tnum] += end + 1;
         }
-        Debug("options") << "thread " << tnum << " now has " << threadArgv[tnum]
-                         << std::endl;
+        Debug("options") << "thread " << tnum << " now has "
+                         << threadArgv[tnum] << std::endl;
         break;
       }
 
@@ -759,19 +779,10 @@ ${all_modules_option_handlers}
     }
   }
 
-  Debug("options") << "returning " << nonOptions.size() << " non-option arguments." << std::endl;
-
-  free(extra_argv);
-  for(std::vector<char*>::iterator i = allocated.begin(), iend = allocated.end();
-      i != iend; ++i)
-  {
-    char* current = *i;
-    #warning "TODO: Unit tests fail if garbage collection is done here."
-    //free(current);
-  }
-  allocated.clear();
+  Debug("options") << "got " << nonoptions->size()
+                   << " non-option arguments." << std::endl;
 
-  return nonOptions;
+  free(argv);
 }
 
 std::string Options::suggestCommandLineOptions(const std::string& optionName) throw() {
@@ -787,7 +798,7 @@ std::string Options::suggestCommandLineOptions(const std::string& optionName) th
 
 static const char* smtOptions[] = {
   ${all_modules_smt_options},
-#line 790 "${template}"
+#line 800 "${template}"
   NULL
 };/* smtOptions[] */
 
@@ -809,7 +820,7 @@ std::vector< std::vector<std::string> > Options::getOptions() const throw() {
 
   ${all_modules_get_options}
 
-#line 813 "${template}"
+#line 762 "${template}"
 
   return opts;
 }