Added CEGIS danger option for genetic only.

Author: pkesseli

src/cegis/danger/facade/danger_runner.cpp

@@ -107,28 +107,28 @@ int run_match(mstreamt &os, optionst &opt, const danger_programt &prog,
     typedef ga_learnt<selectt, mutatet, crosst, fitnesst, danger_fitness_configt> ga_learnt;
     ga_learnt ga_learn(opt, rnd, select, mutate, cross, fitness, converter);
 #ifndef _WIN32
-    concurrent_learnt<ga_learnt, symex_learnt> learn(ga_learn, symex_learn,
-        serialise, std::ref(deser), deserialise, symex_head_start);
-#else
-    // TODO: Remove once task_pool supports Windows.
-    ga_learnt &learn=ga_learn;
+    if (!opt.get_bool_option(CEGIS_GENETIC_ONLY))
+    {
+      concurrent_learnt<ga_learnt, symex_learnt> learn(ga_learn, symex_learn,
+          serialise, std::ref(deser), deserialise, symex_head_start);
+      return run_parallel(os, opt, prog, learn, preproc);
+    }
 #endif
-    return run_parallel(os, opt, prog, learn, preproc);
+    return run_parallel(os, opt, prog, ga_learn, preproc);
   }
   typedef tournament_selectt<program_populationt> selectt;
   selectt select(rounds);
-  typedef ga_learnt<selectt, random_mutatet, random_crosst, fitnesst,
-      danger_fitness_configt> ga_learnt;
+  typedef ga_learnt<selectt, mutatet, crosst, fitnesst, danger_fitness_configt> ga_learnt;
   ga_learnt ga_learn(opt, rnd, select, mutate, cross, fitness, converter);
 #ifndef _WIN32
-  concurrent_learnt<ga_learnt, symex_learnt> learn(ga_learn, symex_learn,
-      serialise, std::ref(deser), deserialise, symex_head_start);
-#else
-  // TODO: Remove once task_pool supports Windows.
-  ga_learnt &learn=ga_learn;
+  if (!opt.get_bool_option(CEGIS_GENETIC_ONLY))
+  {
+    concurrent_learnt<ga_learnt, symex_learnt> learn(ga_learn, symex_learn,
+        serialise, std::ref(deser), deserialise, symex_head_start);
+    return run_parallel(os, opt, prog, learn, preproc);
+  }
 #endif
-  return run_parallel(os, opt, prog, learn, preproc);
-  return 0;
+  return run_parallel(os, opt, prog, ga_learn, preproc);
 }
 
 template<class preproct>

src/cegis/options/parameters.h

@@ -11,6 +11,7 @@
 #define CEGIS_INVARIANT_PARAMETERS_H_
 
 #define CEGIS_GENETIC "cegis-genetic"
+#define CEGIS_GENETIC_ONLY "cegis-genetic-only"
 #define CEGIS_MAX_SIZE "cegis-max-size"
 #define CEGIS_SEED "cegis-seed"
 #define CEGIS_STATISTICS "cegis-statistics"

src/cegis/runner/cegis_parse_options.cpp

@@ -78,6 +78,7 @@ void cegis_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("cegis-match-select", !cmdline.isset("cegis-tournament-select"));
     options.set_option("cegis-statistics", cmdline.isset("cegis-statistics"));
     options.set_option(CEGIS_GENETIC, cmdline.isset(CEGIS_GENETIC));
+    options.set_option(CEGIS_GENETIC_ONLY, cmdline.isset(CEGIS_GENETIC_ONLY));
     set_integer_option(options, cmdline, "cegis-genetic-rounds", 10u);
     set_integer_option(options, cmdline, "cegis-seed", 747864937u);
     set_integer_option(options, cmdline, "cegis-genetic-popsize", 2000u);

src/cegis/runner/cegis_parse_options.h

@@ -15,7 +15,7 @@ Author: Daniel Kroening, [email protected]
   "(cegis)(cegis-seed):(cegis-root):(cegis-targets):" \
   "(cegis-min-prog-size):(cegis-max-prog-size):(cegis-skolem):(cegis-ranking):" \
   "(cegis-max-size):(cegis-statistics)(cegis-show-iterations)" \
-  "(cegis-keep-goto-programs)(cegis-genetic)(cegis-genetic-rounds):" \
+  "(cegis-keep-goto-programs)(cegis-genetic)(cegis-genetic-only)(cegis-genetic-rounds):" \
   "(cegis-genetic-popsize):(cegis-tournament-select)" \
   "(cegis-genetic-mutation-rate):(cegis-genetic-replace-rate):" \
   "(cegis-limit-wordsize)(cegis-parallel-verify)(cegis-symex-head-start):" \