From ffdc8a3676aad41d0fcef0290241aa9df2e5be1b Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 1 Nov 2021 03:52:55 -0700 Subject: [PATCH] Refactor DidYouMean (#7535) This refactors the `DidYouMean` class, which is used to make helpful suggestions for misspelled tags and options. It uses `std::vector` instead of `std::set`, moves it from `options` to `util` (so that we can keep using it in both libcvc5 and the driver) and generally modernizes the code a bit. Also, it replaces the stand-alone and never executed test by a regular unit test. --- src/CMakeLists.txt | 2 - src/main/options_template.cpp | 2 +- src/options/didyoumean_test.cpp | 763 --------------------------- src/options/options_handler.cpp | 2 +- src/util/CMakeLists.txt | 2 + src/{options => util}/didyoumean.cpp | 142 +++-- src/{options => util}/didyoumean.h | 17 +- test/unit/util/CMakeLists.txt | 1 + test/unit/util/didyoumean_black.cpp | 75 +++ 9 files changed, 149 insertions(+), 857 deletions(-) delete mode 100644 src/options/didyoumean_test.cpp rename src/{options => util}/didyoumean.cpp (55%) rename src/{options => util}/didyoumean.h (71%) create mode 100644 test/unit/util/didyoumean_black.cpp diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index d87d51559..721ccebe9 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -51,8 +51,6 @@ libcvc5_add_sources( omt/omt_optimizer.cpp omt/omt_optimizer.h options/decision_weight.h - options/didyoumean.cpp - options/didyoumean.h options/language.cpp options/language.h options/managed_streams.cpp diff --git a/src/main/options_template.cpp b/src/main/options_template.cpp index 138821c71..e0429c5f9 100644 --- a/src/main/options_template.cpp +++ b/src/main/options_template.cpp @@ -37,8 +37,8 @@ extern int optreset; #include "base/check.h" #include "base/output.h" -#include "options/didyoumean.h" #include "options/option_exception.h" +#include "util/didyoumean.h" #include #include diff --git a/src/options/didyoumean_test.cpp b/src/options/didyoumean_test.cpp deleted file mode 100644 index 9da20ce86..000000000 --- a/src/options/didyoumean_test.cpp +++ /dev/null @@ -1,763 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Kshitij Bansal, Tim King, Andrew Reynolds - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * [[ Add one-line brief description here ]] - * - * [[ Add lengthier description here ]] - * \todo document this file - */ - -// This is not built as a part of cvc5 and is not built by Makefile.am. -// Compile: g++ didyoumean_test.cpp didyoumean.cpp -// For debug compile with -DDIDYOUMEAN_DEBUG or -DDIDYOUMEAN_DEBUG1 or both - -#include "didyoumean.h" -#include - -using namespace std; -using namespace cvc5; - -set getDebugTags(); -set getOptionStrings(); - -int main() { - string a, b; - - cin >> a; - cout << "Matches with debug tags:" << endl; - for (const string& s : DidYouMean(getDebugTags()).getMatch(a)) { - cout << s << endl; - } - cout << "Matches with option strings:" << endl; - for (const string& s : DidYouMean(getOptionStrings()).getMatch(a)) { - 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("cegqi"); - a.insert("cegqi-debug"); - a.insert("cegqi-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("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-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", - "cegqi-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", - "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; -} diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 063145ea8..feeb172fb 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -32,7 +32,6 @@ #include "options/base_options.h" #include "options/bv_options.h" #include "options/decision_options.h" -#include "options/didyoumean.h" #include "options/language.h" #include "options/option_exception.h" #include "options/set_language.h" @@ -40,6 +39,7 @@ #include "options/theory_options.h" #include "smt/command.h" #include "smt/dump.h" +#include "util/didyoumean.h" namespace cvc5 { namespace options { diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index ad277cbb6..2ac529565 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -29,6 +29,8 @@ libcvc5_add_sources( cardinality_class.cpp cardinality_class.h dense_map.h + didyoumean.cpp + didyoumean.h divisible.cpp divisible.h floatingpoint.cpp diff --git a/src/options/didyoumean.cpp b/src/util/didyoumean.cpp similarity index 55% rename from src/options/didyoumean.cpp rename to src/util/didyoumean.cpp index 06abd51b8..0f95722fd 100644 --- a/src/options/didyoumean.cpp +++ b/src/util/didyoumean.cpp @@ -18,91 +18,52 @@ * There are no dependencies on cvc5 (except namespace). */ -#include "options/didyoumean.h" +#include "util/didyoumean.h" -#include -#include +#include +#include #include #include #include namespace cvc5 { -std::vector DidYouMean::getMatch(const std::string& input) -{ - /** Magic numbers */ - const int similarityThreshold = 7; - const unsigned numMatchesThreshold = 10; - - typedef std::set > ScoreSet; - ScoreSet scores; - std::vector ret; - for (Words::const_iterator it = d_words.begin(); it != d_words.end(); ++it) { - std::string s = (*it); - if (s == input) { - // if input matches AS-IS just return that - ret.push_back(s); - return ret; - } - int score; - if (s.compare(0, input.size(), input) == 0) { - score = 0; - } else { - score = editDistance(input, s) + 1; - } - scores.insert(make_pair(score, s)); - } - int min_score = scores.begin()->first; - for (ScoreSet::const_iterator 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; -} +namespace { -int DidYouMean::editDistance(const std::string& a, const std::string& b) { +uint64_t editDistance(const std::string& a, const std::string& b) { // input string: a // desired string: b - const size_t swapCost = 0; - const size_t substituteCost = 2; - const size_t addCost = 1; - const size_t deleteCost = 3; - const size_t switchCaseCost = 0; + constexpr uint64_t swapCost = 0; + constexpr uint64_t substituteCost = 2; + constexpr uint64_t addCost = 1; + constexpr uint64_t deleteCost = 3; + constexpr uint64_t switchCaseCost = 0; - size_t len1 = a.size(); - size_t len2 = b.size(); + uint64_t len1 = a.size(); + uint64_t len2 = b.size(); - size_t* C[3]; - size_t ii; - for (ii = 0; ii < 3; ++ii) { - C[ii] = new size_t[len2 + 1]; + std::array, 3> C; + for (auto& c: C) + { + c.resize(len2 + 1); } // int C[3][len2+1]; // cost - for (size_t j = 0; j <= len2; ++j) + for (uint64_t j = 0; j <= len2; ++j) { C[0][j] = j * addCost; } - for (size_t i = 1; i <= len1; ++i) + for (uint64_t i = 1; i <= len1; ++i) { - size_t cur = i % 3; - size_t prv = (i + 2) % 3; - size_t pr2 = (i + 1) % 3; + uint64_t cur = i % 3; + uint64_t prv = (i + 2) % 3; + uint64_t pr2 = (i + 1) % 3; C[cur][0] = i * deleteCost; - for (size_t j = 1; j <= len2; ++j) + for (uint64_t j = 1; j <= len2; ++j) { C[cur][j] = 100000000; // INF @@ -127,29 +88,59 @@ int DidYouMean::editDistance(const std::string& a, const std::string& b) { // delete C[cur][j] = std::min(C[cur][j], C[prv][j] + deleteCost); + } + } + return C[len1 % 3][len2]; +} + +} + +std::vector DidYouMean::getMatch(const std::string& input) +{ + { + std::sort(d_words.begin(), d_words.end()); + auto it = std::unique(d_words.begin(), d_words.end()); + d_words.erase(it, d_words.end()); + } + + /** Magic numbers */ + constexpr uint64_t similarityThreshold = 7; + constexpr uint64_t numMatchesThreshold = 10; -#ifdef DIDYOUMEAN_DEBUG1 - std::cout << "C[" << cur << "][" << 0 << "] = " << C[cur][0] << std::endl; -#endif + std::vector> scores; + std::vector ret; + for (const auto& s: d_words) { + if (s == input) { + // if input matches AS-IS just return that + ret.emplace_back(s); + return ret; } + uint64_t score = 0; + if (s.compare(0, input.size(), input) != 0) { + score = editDistance(input, s) + 1; + } + scores.emplace_back(std::make_pair(score, s)); } - int result = C[len1 % 3][len2]; - for (ii = 0; ii < 3; ++ii) { - delete[] C[ii]; + std::sort(scores.begin(), scores.end()); + const uint64_t min_score = scores.begin()->first; + for (const auto& score: scores) { + // from here on, matches are not similar enough + if (score.first > similarityThreshold) break; + // from here on, matches are way worse than the best one + if (score.first > min_score + 2) break; + // we already have enough matches + if (ret.size() >= numMatchesThreshold) break; + ret.push_back(score.second); } - return result; + return ret; } -std::string DidYouMean::getMatchAsString(const std::string& input, - uint64_t prefixNewLines, - uint64_t suffixNewLines) +std::string DidYouMean::getMatchAsString(const std::string& input) { std::vector matches = getMatch(input); std::ostringstream oss; if (matches.size() > 0) { - while (prefixNewLines-- > 0) { - oss << std::endl; - } + oss << std::endl << std::endl; if (matches.size() == 1) { oss << "Did you mean this?"; } else { @@ -159,9 +150,6 @@ std::string DidYouMean::getMatchAsString(const std::string& input, { oss << "\n " << matches[i]; } - while (suffixNewLines-- > 0) { - oss << std::endl; - } } return oss.str(); } diff --git a/src/options/didyoumean.h b/src/util/didyoumean.h similarity index 71% rename from src/options/didyoumean.h rename to src/util/didyoumean.h index 0118f1484..26de80f66 100644 --- a/src/options/didyoumean.h +++ b/src/util/didyoumean.h @@ -22,7 +22,6 @@ #include "cvc5_export.h" -#include #include #include @@ -30,15 +29,10 @@ namespace cvc5 { class CVC5_EXPORT DidYouMean { public: - using Words = std::set; - - DidYouMean() {} - ~DidYouMean() {} - - void addWord(std::string word) { d_words.insert(std::move(word)); } + void addWord(const std::string& word) { d_words.emplace_back(word); } void addWords(const std::vector& words) { - d_words.insert(words.begin(), words.end()); + d_words.insert(d_words.end(), words.begin(), words.end()); } std::vector getMatch(const std::string& input); @@ -47,13 +41,10 @@ class CVC5_EXPORT DidYouMean { * This is provided to make it easier to ensure consistency of * output. Returned string is empty if there are no matches. */ - std::string getMatchAsString(const std::string& input, - uint64_t prefixNewLines = 2, - uint64_t suffixNewLines = 0); + std::string getMatchAsString(const std::string& input); private: - int editDistance(const std::string& a, const std::string& b); - Words d_words; + std::vector d_words; }; } // namespace cvc5 diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt index c1630a203..03348f6e1 100644 --- a/test/unit/util/CMakeLists.txt +++ b/test/unit/util/CMakeLists.txt @@ -23,6 +23,7 @@ cvc5_add_unit_test_black(cardinality_black util) cvc5_add_unit_test_white(check_white util) cvc5_add_unit_test_black(configuration_black util) cvc5_add_unit_test_black(datatype_black util) +cvc5_add_unit_test_white(didyoumean_black util) cvc5_add_unit_test_black(exception_black util) cvc5_add_unit_test_black(floatingpoint_black util) cvc5_add_unit_test_black(integer_black util) diff --git a/test/unit/util/didyoumean_black.cpp b/test/unit/util/didyoumean_black.cpp new file mode 100644 index 000000000..cc2fdf878 --- /dev/null +++ b/test/unit/util/didyoumean_black.cpp @@ -0,0 +1,75 @@ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Andres Noetzli, Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Black box testing of cvc5::Stat and associated classes. + */ + +#include "test.h" + +#include "util/didyoumean.h" + +namespace cvc5::test { + +class TestUtilDidYouMean : public TestInternal +{ +}; + +TEST_F(TestUtilDidYouMean, getMatch) +{ + { + DidYouMean dym; + dym.addWords({"abfish", "cdfish", "whale"}); + { + auto expected = std::vector{"abfish"}; + EXPECT_EQ(dym.getMatch("abfish"), expected); + } + { + auto expected = std::vector{"whale"}; + EXPECT_EQ(dym.getMatch("wahl"), expected); + } + { + auto expected = std::vector{"abfish", "cdfish"}; + EXPECT_EQ(dym.getMatch("fish"), expected); + } + { + auto expected = std::vector{}; + EXPECT_EQ(dym.getMatch("elephant"), expected); + } + } +} + +TEST_F(TestUtilDidYouMean, getMatchAsString) +{ + DidYouMean dym; + dym.addWords({"abfish", "cdfish", "whale"}); + { + std::string expected = ""; + EXPECT_EQ(dym.getMatchAsString("elephant"), expected); + } + { + std::string expected = R"FOOBAR( + +Did you mean this? + whale)FOOBAR"; + EXPECT_EQ(dym.getMatchAsString("wahl"), expected); + } + { + std::string expected = R"FOOBAR( + +Did you mean any of these? + abfish + cdfish)FOOBAR"; + EXPECT_EQ(dym.getMatchAsString("fish"), expected); + } +} + +} // namespace cvc5::test -- 2.30.2