#include "didyoumean.h"
#include <iostream>
-#include <boost/foreach.hpp>
+
using namespace std;
using namespace CVC4;
set<string> getDebugTags();
set<string> getOptionStrings();
-int main()
-{
+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;
+ for (const string& s : DidYouMean(getDebugTags()).getMatch(a)) {
+ cout << s << endl;
+ }
cout << "Matches with option strings:" << endl;
- ret = DidYouMean(getOptionStrings()).getMatch(a);
- BOOST_FOREACH(string s, ret) cout << s << endl;
+ for (const string& s : DidYouMean(getOptionStrings()).getMatch(a)) {
+ cout << s << endl;
+ }
}
-set<string> getDebugTags()
-{
+set<string> getDebugTags() {
set<string> a;
a.insert("CDInsertHashMap");
a.insert("CDTrailHashMap");
return a;
}
-set<string> getOptionStrings()
-{
+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 */
+ "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) {
+ while (cmdlineOptions[i] != NULL) {
ret.insert(cmdlineOptions[i]);
i++;
}