Eh, what?

7 files changed, 988 insertions, 30 deletions

diff --git a/src/options/base_options_handlers.h b/src/options/base_options_handlers.h
index 2298f5880..3779f75c1 100644
--- a/src/options/base_options_handlers.h
+++ b/src/options/base_options_handlers.h
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Kshitij Bansal
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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
  **
@@ -25,6 +25,7 @@
 #include <sstream>
 
 #include "expr/command.h"
+#include "util/didyoumean.h"
 #include "util/language.h"
 
 namespace CVC4 {
@@ -99,11 +100,24 @@ inline InputLanguage stringToInputLanguage(std::string option, std::string optar
   Unreachable();
 }
 
+inline std::string suggestTags(char const* const* validTags, std::string inputTag)
+{
+  DidYouMean didYouMean;
+
+  const char* opt;
+  for(size_t i = 0; (opt = validTags[i]) != NULL; ++i) {
+    didYouMean.addWord(validTags[i]);
+  }
+
+  return  didYouMean.getMatchAsString(inputTag);
+}
+
 inline void addTraceTag(std::string option, std::string optarg, SmtEngine* smt) {
   if(Configuration::isTracingBuild()) {
     if(!Configuration::isTraceTag(optarg.c_str()))
       throw OptionException(std::string("trace tag ") + optarg +
-                            std::string(" not available"));
+                            std::string(" not available.") +
+                            suggestTags(Configuration::getTraceTags(), optarg) );
   } else {
     throw OptionException("trace tags not available in non-tracing builds");
   }
@@ -115,7 +129,8 @@ inline void addDebugTag(std::string option, std::string optarg, SmtEngine* smt)
     if(!Configuration::isDebugTag(optarg.c_str()) &&
        !Configuration::isTraceTag(optarg.c_str())) {
       throw OptionException(std::string("debug tag ") + optarg +
-                            std::string(" not available"));
+                            std::string(" not available.") +
+                            suggestTags(Configuration::getDebugTags(), optarg) );
     }
   } else if(! Configuration::isDebugBuild()) {
     throw OptionException("debug tags not available in non-debug builds");
diff --git a/src/options/options.h b/src/options/options.h
index eaafade93..b41c9a66e 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Kshitij Bansal
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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
  **
@@ -119,12 +119,11 @@ public:
   static void printLanguageHelp(std::ostream& out);
 
   /**
-   * Look up long command-line option names that bear some similarity to
-   * the given name.  Don't include the initial "--".  This might be
-   * useful in case of typos.  Can return an empty vector if there are
-   * no suggestions.
+   * Look up long command-line option names that bear some similarity
+   * to the given name.  Returns an empty string if there are no
+   * suggestions.
    */
-  static std::vector<std::string> suggestCommandLineOptions(const std::string& optionName) throw();
+  static std::string suggestCommandLineOptions(const std::string& optionName) throw();
 
   /**
    * Look up SMT option names that bear some similarity to
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index 02bfc6ca0..fc8b31d49 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Kshitij Bansal
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
@@ -47,13 +47,14 @@ extern int optreset;
 
 #include "expr/expr.h"
 #include "util/configuration.h"
+#include "util/didyoumean.h"
 #include "util/exception.h"
 #include "util/language.h"
 #include "util/tls.h"
 
 ${include_all_option_headers}
 
-#line 57 "${template}"
+#line 58 "${template}"
 
 #include "util/output.h"
 #include "options/options_holder.h"
@@ -62,7 +63,7 @@ ${include_all_option_headers}
 
 ${option_handler_includes}
 
-#line 66 "${template}"
+#line 67 "${template}"
 
 using namespace CVC4;
 using namespace CVC4::options;
@@ -199,7 +200,7 @@ void runBoolPredicates(T, std::string option, bool b, SmtEngine* smt) {
 
 ${all_custom_handlers}
 
-#line 203 "${template}"
+#line 204 "${template}"
 
 #ifdef CVC4_DEBUG
 #  define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true
@@ -229,18 +230,18 @@ options::OptionsHolder::OptionsHolder() : ${all_modules_defaults}
 {
 }
 
-#line 233 "${template}"
+#line 234 "${template}"
 
 static const std::string mostCommonOptionsDescription = "\
 Most commonly-used CVC4 options:${common_documentation}";
 
-#line 238 "${template}"
+#line 239 "${template}"
 
 static const std::string optionsDescription = mostCommonOptionsDescription + "\n\
 \n\
 Additional CVC4 options:${remaining_documentation}";
 
-#line 244 "${template}"
+#line 245 "${template}"
 
 static const std::string optionsFootnote = "\n\
 [*] Each of these options has a --no-OPTIONNAME variant, which reverses the\n\
@@ -312,7 +313,7 @@ static struct option cmdlineOptions[] = {${all_modules_long_options}
   { NULL, no_argument, NULL, '\0' }
 };/* cmdlineOptions */
 
-#line 316 "${template}"
+#line 317 "${template}"
 
 static void preemptGetopt(int& argc, char**& argv, const char* opt) {
   const size_t maxoptlen = 128;
@@ -505,7 +506,7 @@ std::vector<std::string> Options::parseOptions(int argc, char* main_argv[]) thro
     switch(c) {
 ${all_modules_option_handlers}
 
-#line 509 "${template}"
+#line 510 "${template}"
 
     case ':':
       // This can be a long or short option, and the way to get at the
@@ -549,7 +550,8 @@ ${all_modules_option_handlers}
         break;
       }
 
-      throw OptionException(std::string("can't understand option `") + option + "'");
+      throw OptionException(std::string("can't understand option `") + option + "'"
+                            + suggestCommandLineOptions(option));
     }
   }
 
@@ -558,22 +560,20 @@ ${all_modules_option_handlers}
   return nonOptions;
 }
 
-std::vector<std::string> Options::suggestCommandLineOptions(const std::string& optionName) throw() {
-  std::vector<std::string> suggestions;
+std::string Options::suggestCommandLineOptions(const std::string& optionName) throw() {
+  DidYouMean didYouMean;
 
   const char* opt;
   for(size_t i = 0; (opt = cmdlineOptions[i].name) != NULL; ++i) {
-    if(std::strstr(opt, optionName.c_str()) != NULL) {
-      suggestions.push_back(opt);
-    }
+    didYouMean.addWord(std::string("--") + cmdlineOptions[i].name);
   }
 
-  return suggestions;
+  return didYouMean.getMatchAsString(optionName);
 }
 
 static const char* smtOptions[] = {
   ${all_modules_smt_options},
-#line 577 "${template}"
+#line 589 "${template}"
   NULL
 };/* smtOptions[] */
 
@@ -595,7 +595,7 @@ SExpr Options::getOptions() const throw() {
 
   ${all_modules_get_options}
 
-#line 599 "${template}"
+#line 611 "${template}"
 
   return SExpr(opts);
 }
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 1cfd5cd5c..bf3f1a873 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -94,7 +94,9 @@ libutil_la_SOURCES = \
 	sort_inference.h \
 	sort_inference.cpp \
 	regexp.h \
-	regexp.cpp
+	regexp.cpp \
+	didyoumean.h \
+	didyoumean.cpp
 
 libstatistics_la_SOURCES = \
 	statistics_registry.h \
diff --git a/src/util/didyoumean.cpp b/src/util/didyoumean.cpp
new file mode 100644
index 000000000..d64435ce7
--- /dev/null
+++ b/src/util/didyoumean.cpp
@@ -0,0 +1,145 @@
+/*********************                                                        */
+/*! \file didyoumean.cpp
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** 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 did-you-mean style suggestions
+ **
+ ** ``What do you mean? I don't understand.'' An attempt to be more
+ ** helpful than that. Similar to one in git.
+ **
+ ** There are no dependencies on CVC4, intentionally.
+ **/
+
+#include "didyoumean.h"
+#include <iostream>
+#include <sstream>
+#include <boost/foreach.hpp>
+#include <boost/algorithm/string/predicate.hpp>
+using namespace std;
+
+vector<string> DidYouMean::getMatch(string input) {
+  /** Magic numbers */
+  const int similarityThreshold = 7;
+  const unsigned numMatchesThreshold = 10;
+
+  set< pair<int, string> > scores;
+  vector<string> ret;
+  BOOST_FOREACH(string s, d_words ) {
+    if( s == input ) {
+      // if input matches AS-IS just return that
+      ret.push_back(s);
+      return ret;
+    }
+    int score;
+    if(boost::starts_with(s, input)) {
+      score = 0;
+    } else {
+      score = editDistance(input, s) + 1;
+    }
+    scores.insert( make_pair(score, s) );
+  }
+  int min_score = scores.begin()->first;
+  for(typeof(scores.begin()) i = scores.begin();
+      i != scores.end(); ++i) {
+
+    // add if score is overall not too big, and also not much close to
+    // the score of the best suggestion
+    if(i->first < similarityThreshold && i->first <= min_score + 1) {
+      ret.push_back(i->second);
+#ifdef DIDYOUMEAN_DEBUG
+      cout << i->second << ": " << i->first << std::endl;
+#endif
+    }
+  }
+  if(ret.size() > numMatchesThreshold ) ret.resize(numMatchesThreshold);;
+  return ret;
+}
+
+
+int DidYouMean::editDistance(const std::string& a, const std::string& b)
+{
+  // input string: a
+  // desired string: b
+  
+  const int swapCost = 0;
+  const int substituteCost = 2;
+  const int addCost = 1;
+  const int deleteCost = 3;
+  const int switchCaseCost = 0;
+
+  int len1 = a.size();
+  int len2 = b.size();
+
+  int C[3][len2+1];             // cost
+
+  for(int j = 0; j <= len2; ++j) {
+    C[0][j] = j * addCost;
+  }
+
+  for(int i = 1; i <= len1; ++i) {
+
+    int cur = i%3;
+    int prv = (i+2)%3;
+    int pr2 = (i+1)%3;
+
+    C[cur][0] = i * deleteCost;
+
+    for(int j = 1; j <= len2; ++j) {
+
+      C[cur][j] = 100000000;      // INF
+
+      if(a[i-1] == b[j-1]) {
+        // match
+        C[cur][j] = std::min(C[cur][j], C[prv][j-1]);
+      } else if(tolower(a[i-1]) == tolower(b[j-1])){
+        // switch case
+        C[cur][j] = std::min(C[cur][j], C[prv][j-1] + switchCaseCost);
+      } else {
+        // substitute
+        C[cur][j] = std::min(C[cur][j], C[prv][j-1] + substituteCost);
+      }
+
+      // swap
+      if(i >= 2 && j >= 2 && a[i-1] == b[j-2] && a[i-2] == b[j-1]) {
+        C[cur][j] = std::min(C[cur][j], C[pr2][j-2] + swapCost);
+      }
+
+      // add
+      C[cur][j] = std::min(C[cur][j], C[cur][j-1] + addCost);
+
+      // delete
+      C[cur][j] = std::min(C[cur][j], C[prv][j] + deleteCost);
+      
+#ifdef DIDYOUMEAN_DEBUG1
+      std::cout << "C[" << cur << "][" << 0 << "] = " << C[cur][0] << std::endl;
+#endif
+    }
+
+  }
+  return C[len1%3][len2];
+}
+
+string DidYouMean::getMatchAsString(string input, int prefixNewLines, int suffixNewLines) {
+  vector<string> matches = getMatch(input);
+  ostringstream oss;
+  if(matches.size() > 0) {
+    while(prefixNewLines --> 0) { oss << endl; }
+    if(matches.size() == 1) {
+      oss << "Did you mean this?";
+    } else {
+      oss << "Did you mean any of these?";
+    }
+    for(unsigned i = 0; i < matches.size(); ++i) {
+      oss << "\n        " << matches[i];
+    }
+    while(suffixNewLines --> 0) { oss << endl; }
+  }
+  return oss.str();
+}
diff --git a/src/util/didyoumean.h b/src/util/didyoumean.h
new file mode 100644
index 000000000..2907fcece
--- /dev/null
+++ b/src/util/didyoumean.h
@@ -0,0 +1,49 @@
+/*********************                                                        */
+/*! \file didyoumean.h
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** 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 did-you-mean style suggestions.
+ **
+ ** ``What do you mean? I don't understand.'' An attempt to be more
+ ** helpful than that. Similar to one in git.
+ **
+ ** There are no dependencies on CVC4, intentionally.
+ **/
+
+#pragma once
+
+#include <vector>
+#include <set>
+#include <string>
+
+class DidYouMean {
+  typedef std::set<std::string> Words;
+  Words d_words;
+
+public:
+  DidYouMean() {}
+  ~DidYouMean() {}
+
+  DidYouMean(Words words) : d_words(words) {}
+  
+  void addWord(std::string word) {
+    d_words.insert(word);
+  }
+  
+  std::vector<std::string> getMatch(std::string input);
+
+  /**
+   * This is provided to make it easier to ensure consistency of
+   * output. Returned string is empty if there are no matches.
+   */
+  std::string getMatchAsString(std::string input, int prefixNewLines = 2, int suffixNewLines = 0);
+private:
+  int editDistance(const std::string& a, const std::string& b);
+};
diff --git a/src/util/didyoumean_test.cpp b/src/util/didyoumean_test.cpp
new file mode 100644
index 000000000..5aa7cc105
--- /dev/null
+++ b/src/util/didyoumean_test.cpp
@@ -0,0 +1,748 @@
+// Compile: g++ didyoumean_test.cpp didyoumean.cpp
+// For debug compile with -DDIDYOUMEAN_DEBUG or -DDIDYOUMEAN_DEBUG1 or both
+
+#include "didyoumean.h"
+#include <iostream>
+#include <boost/foreach.hpp>
+using namespace std;
+
+set<string> getDebugTags();
+set<string> getOptionStrings();
+
+int main()
+{
+  string a, b;
+
+  cin >> a;
+  cout << "Matches with debug tags:" << endl;
+  vector<string> ret = DidYouMean(getDebugTags()).getMatch(a);
+  BOOST_FOREACH(string s, ret) cout << s << endl;
+  cout << "Matches with option strings:" << endl;
+  ret = DidYouMean(getOptionStrings()).getMatch(a);
+  BOOST_FOREACH(string s, ret) cout << s << endl;
+}
+
+set<string> getDebugTags()
+{
+  set<string> a;
+  a.insert("CDInsertHashMap");
+  a.insert("CDTrailHashMap");
+  a.insert("TrailHashMap");
+  a.insert("approx");
+  a.insert("approx::");
+  a.insert("approx::branch");
+  a.insert("approx::checkCutOnPad");
+  a.insert("approx::constraint");
+  a.insert("approx::gmi");
+  a.insert("approx::gmiCut");
+  a.insert("approx::guessIsConstructable");
+  a.insert("approx::lemmas");
+  a.insert("approx::mir");
+  a.insert("approx::mirCut");
+  a.insert("approx::nodelog");
+  a.insert("approx::replayAssert");
+  a.insert("approx::replayLogRec");
+  a.insert("approx::soi");
+  a.insert("approx::solveMIP");
+  a.insert("approx::sumConstraints");
+  a.insert("approx::vars");
+  a.insert("arith");
+  a.insert("arith::addSharedTerm");
+  a.insert("arith::approx::cuts");
+  a.insert("arith::arithvar");
+  a.insert("arith::asVectors");
+  a.insert("arith::bt");
+  a.insert("arith::collectModelInfo");
+  a.insert("arith::conflict");
+  a.insert("arith::congruenceManager");
+  a.insert("arith::congruences");
+  a.insert("arith::consistency");
+  a.insert("arith::consistency::comitonconflict");
+  a.insert("arith::consistency::final");
+  a.insert("arith::consistency::initial");
+  a.insert("arith::constraint");
+  a.insert("arith::dio");
+  a.insert("arith::dio::ex");
+  a.insert("arith::dio::max");
+  a.insert("arith::div");
+  a.insert("arith::dual");
+  a.insert("arith::ems");
+  a.insert("arith::eq");
+  a.insert("arith::error::mem");
+  a.insert("arith::explain");
+  a.insert("arith::explainNonbasics");
+  a.insert("arith::findModel");
+  a.insert("arith::focus");
+  a.insert("arith::hasIntegerModel");
+  a.insert("arith::importSolution");
+  a.insert("arith::ite");
+  a.insert("arith::ite::red");
+  a.insert("arith::learned");
+  a.insert("arith::lemma");
+  a.insert("arith::nf");
+  a.insert("arith::oldprop");
+  a.insert("arith::pivot");
+  a.insert("arith::preprocess");
+  a.insert("arith::preregister");
+  a.insert("arith::presolve");
+  a.insert("arith::print_assertions");
+  a.insert("arith::print_model");
+  a.insert("arith::prop");
+  a.insert("arith::resolveOutPropagated");
+  a.insert("arith::restart");
+  a.insert("arith::rewriter");
+  a.insert("arith::selectPrimalUpdate");
+  a.insert("arith::simplex:row");
+  a.insert("arith::solveInteger");
+  a.insert("arith::static");
+  a.insert("arith::subsumption");
+  a.insert("arith::tracking");
+  a.insert("arith::tracking::mid");
+  a.insert("arith::tracking::post");
+  a.insert("arith::tracking::pre");
+  a.insert("arith::unate");
+  a.insert("arith::unate::conf");
+  a.insert("arith::update");
+  a.insert("arith::update::select");
+  a.insert("arith::value");
+  a.insert("array-pf");
+  a.insert("array-types");
+  a.insert("arrays");
+  a.insert("arrays-model-based");
+  a.insert("arrays::propagate");
+  a.insert("arrays::sharing");
+  a.insert("attrgc");
+  a.insert("basicsAtBounds");
+  a.insert("bitvector");
+  a.insert("bitvector-bb");
+  a.insert("bitvector-bitblast");
+  a.insert("bitvector-expandDefinition");
+  a.insert("bitvector-model");
+  a.insert("bitvector-preregister");
+  a.insert("bitvector-rewrite");
+  a.insert("bitvector::bitblaster");
+  a.insert("bitvector::core");
+  a.insert("bitvector::explain");
+  a.insert("bitvector::propagate");
+  a.insert("bitvector::sharing");
+  a.insert("bool-flatten");
+  a.insert("bool-ite");
+  a.insert("boolean-terms");
+  a.insert("bt");
+  a.insert("builder");
+  a.insert("bv-bitblast");
+  a.insert("bv-core");
+  a.insert("bv-core-model");
+  a.insert("bv-inequality");
+  a.insert("bv-inequality-explain");
+  a.insert("bv-inequality-internal");
+  a.insert("bv-rewrite");
+  a.insert("bv-slicer");
+  a.insert("bv-slicer-eq");
+  a.insert("bv-slicer-uf");
+  a.insert("bv-subtheory-inequality");
+  a.insert("bv-to-bool");
+  a.insert("bva");
+  a.insert("bvminisat");
+  a.insert("bvminisat::explain");
+  a.insert("bvminisat::search");
+  a.insert("cbqi");
+  a.insert("cbqi-debug");
+  a.insert("cbqi-prop-as-dec");
+  a.insert("cd_set_collection");
+  a.insert("cdlist");
+  a.insert("cdlist:cmm");
+  a.insert("cdqueue");
+  a.insert("check-inst");
+  a.insert("check-model::rep-checking");
+  a.insert("circuit-prop");
+  a.insert("cnf");
+  a.insert("constructInfeasiblityFunction");
+  a.insert("context");
+  a.insert("current");
+  a.insert("datatypes");
+  a.insert("datatypes-cycle-check");
+  a.insert("datatypes-cycles");
+  a.insert("datatypes-cycles-find");
+  a.insert("datatypes-debug");
+  a.insert("datatypes-explain");
+  a.insert("datatypes-gt");
+  a.insert("datatypes-inst");
+  a.insert("datatypes-labels");
+  a.insert("datatypes-output");
+  a.insert("datatypes-parametric");
+  a.insert("datatypes-prereg");
+  a.insert("datatypes-split");
+  a.insert("decision");
+  a.insert("decision::jh");
+  a.insert("determineArithVar");
+  a.insert("diamonds");
+  a.insert("dio::push");
+  a.insert("dt");
+  a.insert("dt-enum");
+  a.insert("dt-warn");
+  a.insert("dt::propagate");
+  a.insert("dualLike");
+  a.insert("effortlevel");
+  a.insert("ensureLiteral");
+  a.insert("eq");
+  a.insert("equality");
+  a.insert("equality::backtrack");
+  a.insert("equality::disequality");
+  a.insert("equality::evaluation");
+  a.insert("equality::graph");
+  a.insert("equality::internal");
+  a.insert("equality::trigger");
+  a.insert("equalsConstant");
+  a.insert("error");
+  a.insert("estimateWithCFE");
+  a.insert("expand");
+  a.insert("export");
+  a.insert("flipdec");
+  a.insert("fmc-entry-trie");
+  a.insert("fmc-interval-model-debug");
+  a.insert("fmf-card-debug");
+  a.insert("fmf-eval-debug");
+  a.insert("fmf-eval-debug2");
+  a.insert("fmf-exit");
+  a.insert("fmf-index-order");
+  a.insert("fmf-model-complete");
+  a.insert("fmf-model-cons");
+  a.insert("fmf-model-cons-debug");
+  a.insert("fmf-model-eval");
+  a.insert("fmf-model-prefs");
+  a.insert("fmf-model-req");
+  a.insert("focusDownToJust");
+  a.insert("focusDownToLastHalf");
+  a.insert("foo");
+  a.insert("gaussianElimConstructTableRow");
+  a.insert("gc");
+  a.insert("gc:leaks");
+  a.insert("getBestImpliedBound");
+  a.insert("getCeiling");
+  a.insert("getNewDomainValue");
+  a.insert("getPropagatedLiterals");
+  a.insert("getType");
+  a.insert("glpk::loadVB");
+  a.insert("guessCoefficientsConstructTableRow");
+  a.insert("guessIsConstructable");
+  a.insert("handleBorders");
+  a.insert("includeBoundUpdate");
+  a.insert("inst");
+  a.insert("inst-engine");
+  a.insert("inst-engine-ctrl");
+  a.insert("inst-engine-debug");
+  a.insert("inst-engine-phase-req");
+  a.insert("inst-engine-stuck");
+  a.insert("inst-fmf-ei");
+  a.insert("inst-match-gen");
+  a.insert("inst-trigger");
+  a.insert("integers");
+  a.insert("interactive");
+  a.insert("intersectConstantIte");
+  a.insert("isConst");
+  a.insert("ite");
+  a.insert("ite::atom");
+  a.insert("ite::constantIteEqualsConstant");
+  a.insert("ite::print-success");
+  a.insert("ite::simpite");
+  a.insert("lemma-ites");
+  a.insert("lemmaInputChannel");
+  a.insert("literal-matching");
+  a.insert("logPivot");
+  a.insert("matrix");
+  a.insert("minisat");
+  a.insert("minisat::lemmas");
+  a.insert("minisat::pop");
+  a.insert("minisat::remove-clause");
+  a.insert("minisat::search");
+  a.insert("miplib");
+  a.insert("model");
+  a.insert("model-getvalue");
+  a.insert("nf::tmp");
+  a.insert("nm");
+  a.insert("normal-form");
+  a.insert("options");
+  a.insert("paranoid:check_tableau");
+  a.insert("parser");
+  a.insert("parser-extra");
+  a.insert("parser-idt");
+  a.insert("parser-param");
+  a.insert("partial_model");
+  a.insert("pb");
+  a.insert("pickle");
+  a.insert("pickler");
+  a.insert("pipe");
+  a.insert("portfolio::outputmode");
+  a.insert("prec");
+  a.insert("preemptGetopt");
+  a.insert("proof:sat");
+  a.insert("proof:sat:detailed");
+  a.insert("prop");
+  a.insert("prop-explain");
+  a.insert("prop-value");
+  a.insert("prop::lemmas");
+  a.insert("propagateAsDecision");
+  a.insert("properConflict");
+  a.insert("qcf-ccbe");
+  a.insert("qcf-check-inst");
+  a.insert("qcf-eval");
+  a.insert("qcf-match");
+  a.insert("qcf-match-debug");
+  a.insert("qcf-nground");
+  a.insert("qint-check-debug2");
+  a.insert("qint-debug");
+  a.insert("qint-error");
+  a.insert("qint-model-debug");
+  a.insert("qint-model-debug2");
+  a.insert("qint-var-order-debug2");
+  a.insert("quant-arith");
+  a.insert("quant-arith-debug");
+  a.insert("quant-arith-simplex");
+  a.insert("quant-datatypes");
+  a.insert("quant-datatypes-debug");
+  a.insert("quant-req-phase");
+  a.insert("quant-uf-strategy");
+  a.insert("quantifiers");
+  a.insert("quantifiers-assert");
+  a.insert("quantifiers-check");
+  a.insert("quantifiers-dec");
+  a.insert("quantifiers-engine");
+  a.insert("quantifiers-flip");
+  a.insert("quantifiers-other");
+  a.insert("quantifiers-prereg");
+  a.insert("quantifiers-presolve");
+  a.insert("quantifiers-relevance");
+  a.insert("quantifiers-sat");
+  a.insert("quantifiers-substitute-debug");
+  a.insert("quantifiers::collectModelInfo");
+  a.insert("queueConditions");
+  a.insert("rationalToCfe");
+  a.insert("recentlyViolated");
+  a.insert("register");
+  a.insert("register::internal");
+  a.insert("relevant-trigger");
+  a.insert("removeFixed");
+  a.insert("rl");
+  a.insert("sat::minisat");
+  a.insert("selectFocusImproving");
+  a.insert("set_collection");
+  a.insert("sets");
+  a.insert("sets-assert");
+  a.insert("sets-checkmodel-ignore");
+  a.insert("sets-eq");
+  a.insert("sets-learn");
+  a.insert("sets-lemma");
+  a.insert("sets-model");
+  a.insert("sets-model-details");
+  a.insert("sets-parent");
+  a.insert("sets-pending");
+  a.insert("sets-prop");
+  a.insert("sets-prop-details");
+  a.insert("sets-scrutinize");
+  a.insert("sets-terminfo");
+  a.insert("shared");
+  a.insert("shared-terms-database");
+  a.insert("shared-terms-database::assert");
+  a.insert("sharing");
+  a.insert("simple-trigger");
+  a.insert("simplify");
+  a.insert("smart-multi-trigger");
+  a.insert("smt");
+  a.insert("soi::findModel");
+  a.insert("soi::selectPrimalUpdate");
+  a.insert("solveRealRelaxation");
+  a.insert("sort");
+  a.insert("speculativeUpdate");
+  a.insert("strings");
+  a.insert("strings-explain");
+  a.insert("strings-explain-debug");
+  a.insert("strings-prereg");
+  a.insert("strings-propagate");
+  a.insert("substitution");
+  a.insert("substitution::internal");
+  a.insert("tableau");
+  a.insert("te");
+  a.insert("term-db-cong");
+  a.insert("theory");
+  a.insert("theory::assertions");
+  a.insert("theory::atoms");
+  a.insert("theory::bv::rewrite");
+  a.insert("theory::conflict");
+  a.insert("theory::explain");
+  a.insert("theory::idl");
+  a.insert("theory::idl::model");
+  a.insert("theory::internal");
+  a.insert("theory::propagate");
+  a.insert("trans-closure");
+  a.insert("treat-unknown-error");
+  a.insert("tuprec");
+  a.insert("typecheck-idt");
+  a.insert("typecheck-q");
+  a.insert("typecheck-r");
+  a.insert("uf");
+  a.insert("uf-ss");
+  a.insert("uf-ss-check-region");
+  a.insert("uf-ss-cliques");
+  a.insert("uf-ss-debug");
+  a.insert("uf-ss-disequal");
+  a.insert("uf-ss-na");
+  a.insert("uf-ss-region");
+  a.insert("uf-ss-region-debug");
+  a.insert("uf-ss-register");
+  a.insert("uf-ss-sat");
+  a.insert("uf::propagate");
+  a.insert("uf::sharing");
+  a.insert("ufgc");
+  a.insert("ufsymm");
+  a.insert("ufsymm:clauses");
+  a.insert("ufsymm:eq");
+  a.insert("ufsymm:match");
+  a.insert("ufsymm:norm");
+  a.insert("ufsymm:p");
+  a.insert("update");
+  a.insert("updateAndSignal");
+  a.insert("weak");
+  a.insert("whytheoryenginewhy");
+  return a;
+}
+
+set<string> getOptionStrings()
+{
+  const char* cmdlineOptions[] = {
+    "lang",
+    "output-lang",
+    "language",
+    "output-language",
+    "verbose",
+    "quiet",
+    "stats",
+    "no-stats",
+    "statistics",
+    "no-statistics",
+    "stats-every-query",
+    "no-stats-every-query",
+    "statistics-every-query",
+    "no-statistics-every-query",
+    "parse-only",
+    "no-parse-only",
+    "preprocess-only",
+    "no-preprocess-only",
+    "trace",
+    "debug",
+    "print-success",
+    "no-print-success",
+    "smtlib-strict",
+    "default-expr-depth",
+    "default-dag-thresh",
+    "print-expr-types",
+    "eager-type-checking",
+    "lazy-type-checking",
+    "no-type-checking",
+    "biased-ites",
+    "no-biased-ites",
+    "boolean-term-conversion-mode",
+    "theoryof-mode",
+    "use-theory",
+    "bitblast-eager",
+    "no-bitblast-eager",
+    "bitblast-share-lemmas",
+    "no-bitblast-share-lemmas",
+    "bitblast-eager-fullcheck",
+    "no-bitblast-eager-fullcheck",
+    "bv-inequality-solver",
+    "no-bv-inequality-solver",
+    "bv-core-solver",
+    "no-bv-core-solver",
+    "bv-to-bool",
+    "no-bv-to-bool",
+    "bv-propagate",
+    "no-bv-propagate",
+    "bv-eq",
+    "no-bv-eq",
+    "dt-rewrite-error-sel",
+    "no-dt-rewrite-error-sel",
+    "dt-force-assignment",
+    "unate-lemmas",
+    "arith-prop",
+    "heuristic-pivots",
+    "standard-effort-variable-order-pivots",
+    "error-selection-rule",
+    "simplex-check-period",
+    "pivot-threshold",
+    "prop-row-length",
+    "disable-dio-solver",
+    "enable-arith-rewrite-equalities",
+    "disable-arith-rewrite-equalities",
+    "enable-miplib-trick",
+    "disable-miplib-trick",
+    "miplib-trick-subs",
+    "cut-all-bounded",
+    "no-cut-all-bounded",
+    "maxCutsInContext",
+    "revert-arith-models-on-unsat",
+    "no-revert-arith-models-on-unsat",
+    "fc-penalties",
+    "no-fc-penalties",
+    "use-fcsimplex",
+    "no-use-fcsimplex",
+    "use-soi",
+    "no-use-soi",
+    "restrict-pivots",
+    "no-restrict-pivots",
+    "collect-pivot-stats",
+    "no-collect-pivot-stats",
+    "use-approx",
+    "no-use-approx",
+    "approx-branch-depth",
+    "dio-decomps",
+    "no-dio-decomps",
+    "new-prop",
+    "no-new-prop",
+    "arith-prop-clauses",
+    "soi-qe",
+    "no-soi-qe",
+    "rewrite-divk",
+    "no-rewrite-divk",
+    "se-solve-int",
+    "no-se-solve-int",
+    "lemmas-on-replay-failure",
+    "no-lemmas-on-replay-failure",
+    "dio-turns",
+    "rr-turns",
+    "dio-repeat",
+    "no-dio-repeat",
+    "replay-early-close-depth",
+    "replay-failure-penalty",
+    "replay-num-err-penalty",
+    "replay-reject-cut",
+    "replay-lemma-reject-cut",
+    "replay-soi-major-threshold",
+    "replay-soi-major-threshold-pen",
+    "replay-soi-minor-threshold",
+    "replay-soi-minor-threshold-pen",
+    "symmetry-breaker",
+    "no-symmetry-breaker",
+    "condense-function-values",
+    "no-condense-function-values",
+    "disable-uf-ss-regions",
+    "uf-ss-eager-split",
+    "no-uf-ss-eager-split",
+    "uf-ss-totality",
+    "no-uf-ss-totality",
+    "uf-ss-totality-limited",
+    "uf-ss-totality-sym-break",
+    "no-uf-ss-totality-sym-break",
+    "uf-ss-abort-card",
+    "uf-ss-explained-cliques",
+    "no-uf-ss-explained-cliques",
+    "uf-ss-simple-cliques",
+    "no-uf-ss-simple-cliques",
+    "uf-ss-deq-prop",
+    "no-uf-ss-deq-prop",
+    "disable-uf-ss-min-model",
+    "uf-ss-clique-splits",
+    "no-uf-ss-clique-splits",
+    "uf-ss-sym-break",
+    "no-uf-ss-sym-break",
+    "uf-ss-fair",
+    "no-uf-ss-fair",
+    "arrays-optimize-linear",
+    "no-arrays-optimize-linear",
+    "arrays-lazy-rintro1",
+    "no-arrays-lazy-rintro1",
+    "arrays-model-based",
+    "no-arrays-model-based",
+    "arrays-eager-index",
+    "no-arrays-eager-index",
+    "arrays-eager-lemmas",
+    "no-arrays-eager-lemmas",
+    "disable-miniscope-quant",
+    "disable-miniscope-quant-fv",
+    "disable-prenex-quant",
+    "disable-var-elim-quant",
+    "disable-ite-lift-quant",
+    "cnf-quant",
+    "no-cnf-quant",
+    "clause-split",
+    "no-clause-split",
+    "pre-skolem-quant",
+    "no-pre-skolem-quant",
+    "ag-miniscope-quant",
+    "no-ag-miniscope-quant",
+    "macros-quant",
+    "no-macros-quant",
+    "fo-prop-quant",
+    "no-fo-prop-quant",
+    "disable-smart-triggers",
+    "relevant-triggers",
+    "no-relevant-triggers",
+    "relational-triggers",
+    "no-relational-triggers",
+    "register-quant-body-terms",
+    "no-register-quant-body-terms",
+    "inst-when",
+    "eager-inst-quant",
+    "no-eager-inst-quant",
+    "full-saturate-quant",
+    "no-full-saturate-quant",
+    "literal-matching",
+    "enable-cbqi",
+    "no-enable-cbqi",
+    "cbqi-recurse",
+    "no-cbqi-recurse",
+    "user-pat",
+    "flip-decision",
+    "disable-quant-internal-reps",
+    "finite-model-find",
+    "no-finite-model-find",
+    "mbqi",
+    "mbqi-one-inst-per-round",
+    "no-mbqi-one-inst-per-round",
+    "mbqi-one-quant-per-round",
+    "no-mbqi-one-quant-per-round",
+    "fmf-inst-engine",
+    "no-fmf-inst-engine",
+    "disable-fmf-inst-gen",
+    "fmf-inst-gen-one-quant-per-round",
+    "no-fmf-inst-gen-one-quant-per-round",
+    "fmf-fresh-dc",
+    "no-fmf-fresh-dc",
+    "disable-fmf-fmc-simple",
+    "fmf-bound-int",
+    "no-fmf-bound-int",
+    "axiom-inst",
+    "quant-cf",
+    "no-quant-cf",
+    "quant-cf-mode",
+    "quant-cf-when",
+    "rewrite-rules",
+    "no-rewrite-rules",
+    "rr-one-inst-per-round",
+    "no-rr-one-inst-per-round",
+    "strings-exp",
+    "no-strings-exp",
+    "strings-lb",
+    "strings-fmf",
+    "no-strings-fmf",
+    "strings-eit",
+    "no-strings-eit",
+    "strings-alphabet-card",
+    "show-sat-solvers",
+    "random-freq",
+    "random-seed",
+    "restart-int-base",
+    "restart-int-inc",
+    "refine-conflicts",
+    "no-refine-conflicts",
+    "minisat-elimination",
+    "no-minisat-elimination",
+    "minisat-dump-dimacs",
+    "no-minisat-dump-dimacs",
+    "model-format",
+    "dump",
+    "dump-to",
+    "force-logic",
+    "simplification",
+    "no-simplification",
+    "static-learning",
+    "no-static-learning",
+    "produce-models",
+    "no-produce-models",
+    "check-models",
+    "no-check-models",
+    "dump-models",
+    "no-dump-models",
+    "proof",
+    "no-proof",
+    "check-proofs",
+    "no-check-proofs",
+    "dump-proofs",
+    "no-dump-proofs",
+    "produce-unsat-cores",
+    "no-produce-unsat-cores",
+    "produce-assignments",
+    "no-produce-assignments",
+    "interactive",
+    "no-interactive",
+    "ite-simp",
+    "no-ite-simp",
+    "on-repeat-ite-simp",
+    "no-on-repeat-ite-simp",
+    "simp-with-care",
+    "no-simp-with-care",
+    "simp-ite-compress",
+    "no-simp-ite-compress",
+    "unconstrained-simp",
+    "no-unconstrained-simp",
+    "repeat-simp",
+    "no-repeat-simp",
+    "simp-ite-hunt-zombies",
+    "sort-inference",
+    "no-sort-inference",
+    "incremental",
+    "no-incremental",
+    "abstract-values",
+    "no-abstract-values",
+    "model-u-dt-enum",
+    "no-model-u-dt-enum",
+    "tlimit",
+    "tlimit-per",
+    "rlimit",
+    "rlimit-per",
+    "rewrite-apply-to-const",
+    "no-rewrite-apply-to-const",
+    "replay",
+    "replay-log",
+    "decision",
+    "decision-threshold",
+    "decision-use-weight",
+    "no-decision-use-weight",
+    "decision-random-weight",
+    "decision-weight-internal",
+    "version",
+    "license",
+    "help",
+    "show-config",
+    "show-debug-tags",
+    "show-trace-tags",
+    "early-exit",
+    "no-early-exit",
+    "threads",
+    "threadN",
+    "filter-lemma-length",
+    "fallback-sequential",
+    "no-fallback-sequential",
+    "incremental-parallel",
+    "no-incremental-parallel",
+    "no-interactive-prompt",
+    "continued-execution",
+    "immediate-exit",
+    "segv-spin",
+    "no-segv-spin",
+    "segv-nospin",
+    "wait-to-join",
+    "no-wait-to-join",
+    "strict-parsing",
+    "no-strict-parsing",
+    "mmap",
+    "no-mmap",
+    "no-checking",
+    "no-filesystem-access",
+    "no-include-file",
+    "enable-idl-rewrite-equalities",
+    "disable-idl-rewrite-equalities",
+    "sets-propagate",
+    "no-sets-propagate",
+    "sets-eager-lemmas",
+    "no-sets-eager-lemmas",
+    NULL,
+  };/* cmdlineOptions */
+  int i = 0;
+  set<string> ret;
+  while(cmdlineOptions[i] != NULL) {
+    ret.insert(cmdlineOptions[i]);
+    i++;
+  }
+  return ret;
+}