Skip to content

Commit 7250494

Browse files
author
pkesseli
committed
Added genetic only option to CEGIS safety.
1 parent 5dfda05 commit 7250494

File tree

2 files changed

+17
-15
lines changed

2 files changed

+17
-15
lines changed

src/cegis/refactor/learn/refactor_candidate_printer.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@ void print_instr(messaget::mstreamt &os, const namespacet &ns,
3434
[opcode](const goto_programt::instructiont &instr)
3535
{ return matches_opcode(instr, opcode);}));
3636
const goto_programt::const_targett last=std::find_if(first, end,
37-
std::mem_fun_ref(goto_programt::instructiont::is_goto));
37+
std::mem_fun_ref(&goto_programt::instructiont::is_goto));
3838
for (; first != last; ++first)
3939
body.output_instruction(ns, func_name, oss, first);
4040
std::string result(oss.str());

src/cegis/safety/facade/safety_runner.cpp

Lines changed: 16 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -96,14 +96,15 @@ int configure_backend(mstreamt &os, const optionst &o,
9696
safety_goto_cet>, safety_fitness_configt> ga_learnt;
9797
ga_learnt ga_learn(o, rnd, select, mutate, cross, fit, safety_fitness_config);
9898
#ifndef _WIN32
99-
const individual_to_safety_solution_deserialisert deser(prog, info_fac);
100-
concurrent_learnt<ga_learnt, symex_learnt> learner(ga_learn, learn,
101-
serialise, deser, deserialise, symex_head_start);
102-
#else
103-
// TODO: Remove once task_pool supports Windows.
104-
ga_learnt &learner=ga_learn;
99+
if (!o.get_bool_option(CEGIS_GENETIC_ONLY))
100+
{
101+
const individual_to_safety_solution_deserialisert deser(prog, info_fac);
102+
concurrent_learnt<ga_learnt, symex_learnt> learner(ga_learn, learn,
103+
serialise, deser, deserialise, symex_head_start);
104+
return configure_ui_and_run(os, o, learner, verify, pre);
105+
}
105106
#endif
106-
return configure_ui_and_run(os, o, learner, verify, pre);
107+
return configure_ui_and_run(os, o, ga_learn, verify, pre);
107108
}
108109
typedef tournament_selectt<program_populationt> selectt;
109110
selectt select(rounds);
@@ -112,14 +113,15 @@ int configure_backend(mstreamt &os, const optionst &o,
112113
safety_goto_cet>, safety_fitness_configt> ga_learnt;
113114
ga_learnt ga_learn(o, rnd, select, mutate, cross, fit, safety_fitness_config);
114115
#ifndef _WIN32
115-
const individual_to_safety_solution_deserialisert deser(prog, info_fac);
116-
concurrent_learnt<ga_learnt, symex_learnt> learner(ga_learn, learn, serialise,
117-
std::ref(deser), deserialise, symex_head_start);
118-
#else
119-
// TODO: Remove once task_pool supports Windows.
120-
ga_learnt &learner=ga_learn;
116+
if (!o.get_bool_option(CEGIS_GENETIC_ONLY))
117+
{
118+
const individual_to_safety_solution_deserialisert deser(prog, info_fac);
119+
concurrent_learnt<ga_learnt, symex_learnt> learner(ga_learn, learn,
120+
serialise, std::ref(deser), deserialise, symex_head_start);
121+
return configure_ui_and_run(os, o, learner, verify, pre);
122+
}
121123
#endif
122-
return configure_ui_and_run(os, o, learner, verify, pre);
124+
return configure_ui_and_run(os, o, ga_learn, verify, pre);
123125
}
124126

125127
constant_strategyt get_constant_strategy(const optionst &opt)

0 commit comments

Comments
 (0)