From ef230f2fcd8556ff8b07fe570cc00e9e1c7d4025 Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 13 Jul 2017 18:16:59 -0700 Subject: [PATCH] Removing BOOST_FOREACH usage. --- src/options/didyoumean_test.cpp | 679 ++++++++++++------------ src/theory/sets/theory_sets_private.cpp | 9 +- 2 files changed, 342 insertions(+), 346 deletions(-) diff --git a/src/options/didyoumean_test.cpp b/src/options/didyoumean_test.cpp index ff5d7f7b5..76578b6c4 100644 --- a/src/options/didyoumean_test.cpp +++ b/src/options/didyoumean_test.cpp @@ -21,28 +21,28 @@ #include "didyoumean.h" #include -#include + using namespace std; using namespace CVC4; set getDebugTags(); set getOptionStrings(); -int main() -{ +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; + 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 getDebugTags() -{ +set getDebugTags() { set a; a.insert("CDInsertHashMap"); a.insert("CDTrailHashMap"); @@ -426,340 +426,339 @@ set getDebugTags() return a; } -set getOptionStrings() -{ +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 */ + "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) { + while (cmdlineOptions[i] != NULL) { ret.insert(cmdlineOptions[i]); i++; } diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index f70db9823..a2a56e137 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -17,8 +17,6 @@ #include #include "theory/sets/theory_sets_private.h" -#include - #include "expr/emptyset.h" #include "options/sets_options.h" #include "smt/smt_statistics_registry.h" @@ -56,7 +54,7 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, { d_rels = new TheorySetsRels(c, u, &d_equalityEngine, &d_conflict, external); - + d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); d_zero = NodeManager::currentNM()->mkConst( Rational(0) ); @@ -79,9 +77,8 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, TheorySetsPrivate::~TheorySetsPrivate(){ delete d_rels; - for(std::map< Node, EqcInfo* >::iterator i = d_eqc_info.begin(), iend = d_eqc_info.end(); i != iend; ++i){ - EqcInfo* current = (*i).second; - delete current; + for (std::pair& current_pair : d_eqc_info) { + delete current_pair.second; } }/* TheorySetsPrivate::~TheorySetsPrivate() */ -- 2.30.2