Remove argument extender (#4223)

This was a utility class for dynamically changing argc/argv.

7 files changed, 10 insertions, 384 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 5284aa12c..9ad790398 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -924,7 +924,6 @@ install(FILES
         DESTINATION
           ${INCLUDE_INSTALL_DIR}/cvc4/expr)
 install(FILES
-          options/argument_extender.h
           options/language.h
           options/option_exception.h
           options/options.h
diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt
index 4909d7d43..46bd17172 100644
--- a/src/options/CMakeLists.txt
+++ b/src/options/CMakeLists.txt
@@ -13,9 +13,6 @@ if(RET_TOML)
 endif()
 
 libcvc4_add_sources(
-  argument_extender.h
-  argument_extender_implementation.cpp
-  argument_extender_implementation.h
   base_handlers.h
   decision_weight.h
   didyoumean.cpp
diff --git a/src/options/argument_extender.h b/src/options/argument_extender.h
deleted file mode 100644
index e3cec3c25..000000000
--- a/src/options/argument_extender.h
+++ /dev/null
@@ -1,85 +0,0 @@
-/*********************                                                        */
-/*! \file argument_extender.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Paul Meng, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 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.\endverbatim
- **
- ** \brief Abstract utility class for extending commandline options.
- **
- ** Abstract utility class for extending commandline options.
- **/
-
-#include "cvc4_public.h"
-
-#ifndef CVC4__OPTIONS__ARGUMENT_EXTENDER_H
-#define CVC4__OPTIONS__ARGUMENT_EXTENDER_H
-
-#include <cstddef>
-
-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:
-  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:
-   * - argc and argv are non-null.
-   */
-  virtual void getArguments(int* argc, char*** argv) const = 0;
-
-  /** Returns the number of arguments that are . */
-  virtual size_t numArguments() const = 0;
-
-  /**
-   * 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.
-   */
-  virtual void movePreemptionsToArguments() = 0;
-
-  /** Returns true iff there is a pending preemption.*/
-  virtual bool hasPreemptions() const = 0;
-
-};/* class ArgumentExtender */
-
-}/* CVC4::options namespace */
-}/* CVC4 namespace */
-
-#endif /* CVC4__OPTIONS__ARGUMENT_EXTENDER_H */
diff --git a/src/options/argument_extender_implementation.cpp b/src/options/argument_extender_implementation.cpp
deleted file mode 100644
index 1073521ca..000000000
--- a/src/options/argument_extender_implementation.cpp
+++ /dev/null
@@ -1,114 +0,0 @@
-/*********************                                                        */
-/*! \file argument_extender_implementation.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Paul Meng
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 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.\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/check.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
deleted file mode 100644
index 9906bb420..000000000
--- a/src/options/argument_extender_implementation.h
+++ /dev/null
@@ -1,115 +0,0 @@
-/*********************                                                        */
-/*! \file argument_extender_implementation.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Paul Meng, Mathias Preiner
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 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.\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 override;
-
-  /** Returns the number of arguments that are . */
-  size_t numArguments() const override;
-
-  /**
-   * 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) override;
-
-  /**
-   * 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) override;
-
-  /** Removes the front of the arguments list.*/
-  void popFrontArgument() override;
-
-  /** Adds a new preemption to the arguments list. */
-  void pushBackPreemption(const char* element) override;
-
-  /**
-   * Moves all of the preemptions into the front of the arguments
-   * list.
-   */
-  void movePreemptionsToArguments() override;
-
-  /** Returns true iff there is a pending preemption.*/
-  bool hasPreemptions() const override;
-
- 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/options.h b/src/options/options.h
index 3d1e67aba..c63af1c64 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -26,7 +26,6 @@
 
 #include "base/listener.h"
 #include "base/modal_exception.h"
-#include "options/argument_extender.h"
 #include "options/language.h"
 #include "options/option_exception.h"
 #include "options/printer_modes.h"
@@ -479,8 +478,8 @@ public:
   /**
    * 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.
+   * arguments. The command line arguments are stored in argc/argv.
+   * Nonoptions are stored into nonoptions.
    *
    * This is not thread safe.
    *
@@ -489,7 +488,8 @@ public:
    * Preconditions: options, extender and nonoptions are non-null.
    */
   static void parseOptionsRecursive(Options* options,
-                                    options::ArgumentExtender* extender,
+                                    int argc,
+                                    char* argv[],
                                     std::vector<std::string>* nonoptions);
 };/* class Options */
 
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index 48b6a66dd..faaa446ce 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -51,8 +51,6 @@ extern int optreset;
 #include "base/check.h"
 #include "base/exception.h"
 #include "base/output.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"
@@ -74,8 +72,6 @@ namespace CVC4 {
 
 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,
@@ -488,33 +484,6 @@ static struct option cmdlineOptions[] = {
   { NULL, no_argument, NULL, '\0' }
 };/* cmdlineOptions */
 
-
-// static void preemptGetopt(int& argc, char**& argv, const char* opt) {
-
-//   Debug("preemptGetopt") << "preempting getopt() with " << opt << std::endl;
-
-//   AlwaysAssert(opt != NULL && *opt != '\0');
-//   AlwaysAssert(strlen(opt) <= maxoptlen);
-
-//   ++argc;
-//   unsigned i = 1;
-//   while(argv[i] != NULL && argv[i][0] != '\0') {
-//     ++i;
-//   }
-
-//   if(argv[i] == NULL) {
-//     argv = (char**) realloc(argv, (i + 6) * sizeof(char*));
-//     for(unsigned j = i; j < i + 5; ++j) {
-//       argv[j] = (char*) malloc(sizeof(char) * maxoptlen);
-//       argv[j][0] = '\0';
-//     }
-//     argv[i + 5] = NULL;
-//   }
-
-//   strncpy(argv[i], opt, maxoptlen - 1);
-//   argv[i][maxoptlen - 1] = '\0'; // ensure NUL-termination even on overflow
-// }
-
 namespace options {
 
 /** Set a given Options* as "current" just for a particular scope. */
@@ -567,13 +536,9 @@ std::vector<std::string> Options::parseOptions(Options* options,
   }
   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);
+  parseOptionsRecursive(options, argc, argv, &nonoptions);
   if(Debug.isOn("options")){
     for(std::vector<std::string>::const_iterator i = nonoptions.begin(),
           iend = nonoptions.end(); i != iend; ++i){
@@ -581,20 +546,14 @@ std::vector<std::string> Options::parseOptions(Options* options,
     }
   }
 
-  delete argumentExtender;
   return nonoptions;
 }
 
 void Options::parseOptionsRecursive(Options* options,
-                                    ArgumentExtender* extender,
+                                    int argc,
+                                    char* argv[],
                                     std::vector<std::string>* nonoptions)
 {
-  int argc;
-  char** argv;
-
-  extender->movePreemptionsToArguments();
-  extender->pushFrontArgument("");
-  extender->getArguments(&argc, &argv);
 
   if(Debug.isOn("options")) {
     Debug("options") << "starting a new parseOptionsRecursive with "
@@ -615,27 +574,18 @@ void Options::parseOptionsRecursive(Options* options,
   optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this
 #endif /* HAVE_DECL_OPTRESET */
 
-  
-  int main_optind = 0;
+  // start with position after the binary name
+  int main_optind = 1;
   int old_optind;
 
 
   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;
-    }
-
     optopt = 0;
     std::string option, optionarg;
 
     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
@@ -646,7 +596,6 @@ void Options::parseOptionsRecursive(Options* options,
                        << " as a non-option." << std::endl;
       nonoptions->push_back(argv[main_optind]);
       ++main_optind;
-      extender->popFrontArgument();
       continue;
     }
 
@@ -660,10 +609,7 @@ void Options::parseOptionsRecursive(Options* options,
                         "+:${options_short}$",
                         cmdlineOptions, NULL);
 
-    while(main_optind < optind) {
-      main_optind++;
-      extender->popFrontArgument();
-    }
+    main_optind = optind;
 
     Debug("options") << "[ got " << int(c) << " (" << char(c) << ") ]"
                      << "[ next option will be at pos: " << optind << " ]"
@@ -725,8 +671,6 @@ ${options_handler}$
 
   Debug("options") << "got " << nonoptions->size()
                    << " non-option arguments." << std::endl;
-
-  free(argv);
 }
 
 std::string Options::suggestCommandLineOptions(const std::string& optionName)