From: Kshitij Bansal Date: Sat, 19 Apr 2014 20:44:20 +0000 (-0400) Subject: Eh, what? X-Git-Tag: cvc5-1.0.0~6956^2~6 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e6b834f2976c736b6e9df1cc017bc2d72c00b27c;p=cvc5.git Eh, what? --- 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 #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 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 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 Options::suggestCommandLineOptions(const std::string& optionName) throw() { - std::vector 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 +#include +#include +#include +using namespace std; + +vector DidYouMean::getMatch(string input) { + /** Magic numbers */ + const int similarityThreshold = 7; + const unsigned numMatchesThreshold = 10; + + set< pair > scores; + vector 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 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 +#include +#include + +class DidYouMean { + typedef std::set Words; + Words d_words; + +public: + DidYouMean() {} + ~DidYouMean() {} + + DidYouMean(Words words) : d_words(words) {} + + void addWord(std::string word) { + d_words.insert(word); + } + + std::vector 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 +#include +using namespace std; + +set getDebugTags(); +set getOptionStrings(); + +int main() +{ + string a, b; + + cin >> a; + cout << "Matches with debug tags:" << endl; + vector 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 getDebugTags() +{ + set 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 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 ret; + while(cmdlineOptions[i] != NULL) { + ret.insert(cmdlineOptions[i]); + i++; + } + return ret; +}