Removing BOOST_FOREACH usage.

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 <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");
@@ -426,340 +426,339 @@ set<string> getDebugTags()
   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++;
   }
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 <algorithm>
 #include "theory/sets/theory_sets_private.h"
 
-#include <boost/foreach.hpp>
-
 #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<const Node, EqcInfo*>& current_pair : d_eqc_info) {
+    delete current_pair.second;
   }
 }/* TheorySetsPrivate::~TheorySetsPrivate() */