Skip to content

Commit e5bf74b

Browse files
pkesselipkesseli
committed
Extracted rational CEGIS control solution config.
Transformed control_symex_learn to accept a template defining the type of solution to use, as well how to insert these types of solutions into the respective GOTO programs.
1 parent 7bcc403 commit e5bf74b

8 files changed

+148
-134
lines changed

‎src/cegis/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -46,10 +46,10 @@ SRC = danger/meta/meta_variable_names.cpp danger/facade/danger_runner.cpp danger
4646
jsa/genetic/jsa_source_provider.cpp jsa/genetic/dynamic_jsa_test_runner.cpp jsa/genetic/random_jsa_mutate.cpp \
4747
jsa/genetic/random_jsa_cross.cpp jsa/genetic/jsa_genetic_convert.cpp jsa/genetic/jsa_random.cpp \
4848
jsa/genetic/solution_helper.cpp jsa/genetic/jsa_serialiser.cpp jsa/genetic/jsa_paragon_wrapper.cpp \
49-
control/facade/control_runner.cpp control/facade/rational_solution_configuration.cpp \
49+
control/facade/control_runner.cpp control/learn/rational_solution_configuration.cpp \
5050
control/preprocessing/control_preprocessing.cpp control/preprocessing/propagate_controller_sizes.cpp \
5151
control/options/control_program.cpp \
52-
control/learn/control_symex_learn.cpp control/learn/nondet_solution.cpp \
52+
control/learn/nondet_solution.cpp \
5353
control/simplify/remove_unused_elements.cpp \
5454
control/verify/control_symex_verify.cpp control/verify/insert_solution.cpp \
5555
control/value/float_helper.cpp control/value/control_types.cpp \

‎src/cegis/control/facade/control_runner.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@
88
#include <cegis/control/preprocessing/control_preprocessing.h>
99
#include <cegis/control/preprocessing/propagate_controller_sizes.h>
1010
#include <cegis/control/learn/control_symex_learn.h>
11+
#include <cegis/control/learn/rational_solution_configuration.h>
1112
#include <cegis/control/verify/control_symex_verify.h>
1213
#include <cegis/control/facade/control_runner.h>
1314

@@ -16,7 +17,8 @@ int run_control(optionst &o, messaget::mstreamt &result,
1617
{
1718
control_preprocessingt prep(st, gf);
1819
const control_programt &program=prep.get_program();
19-
control_symex_learnt lcfg(program);
20+
typedef control_symex_learnt<rational_solution_configurationt> control_learnt;
21+
control_learnt lcfg(program);
2022
const std::function<void(control_solutiont &)> default_solution=
2123
[&st](control_solutiont &solution)
2224
{ if (!solution.a.operands().empty()) return;
@@ -29,7 +31,7 @@ int run_control(optionst &o, messaget::mstreamt &result,
2931
solution.a=get_a_controller_comp(ns, zero_struct);
3032
solution.b=get_b_controller_comp(ns, zero_struct);
3133
};
32-
cegis_symex_learnt<control_preprocessingt, control_symex_learnt> learn(o,
34+
cegis_symex_learnt<control_preprocessingt, control_learnt> learn(o,
3335
prep, lcfg, default_solution);
3436
control_symex_verifyt vcfg(program);
3537
cegis_symex_verifyt<control_symex_verifyt> oracle(o, vcfg);

‎src/cegis/control/facade/rational_solution_configuration.cpp

Lines changed: 0 additions & 36 deletions
This file was deleted.

‎src/cegis/control/facade/rational_solution_configuration.h

Lines changed: 0 additions & 54 deletions
This file was deleted.

‎src/cegis/control/learn/control_symex_learn.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@
2121
*
2222
* @details
2323
*/
24+
template<class solution_configt>
2425
class control_symex_learnt
2526
{
2627
const control_programt &original_program;
@@ -104,4 +105,6 @@ class control_symex_learnt
104105
const candidatet &candidate) const;
105106
};
106107

108+
#include "control_symex_learn.inc"
109+
107110
#endif // CPROVER_CEGIS_CONTROL_LEARN_CONTROL_SYMEX_LEARN_H

‎src/cegis/control/learn/control_symex_learn.inc

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
#include <cegis/learn/constraint_helper.h>
2+
#include <cegis/learn/insert_counterexample.h>
3+
4+
template<class solution_configt>
5+
control_symex_learnt<solution_configt>::control_symex_learnt(
6+
const control_programt &original_program) :
7+
original_program(original_program)
8+
{
9+
}
10+
11+
template<class solution_configt>
12+
void control_symex_learnt<solution_configt>::process(
13+
const counterexamplest &counterexamples, const size_t max_solution_size)
14+
{
15+
current_program=original_program;
16+
symbol_tablet &st=current_program.st;
17+
goto_functionst &gf=current_program.gf;
18+
solution_configt::nondeterminise_solution_configuration(st, gf);
19+
transform_asserts_to_assumes(gf);
20+
const goto_programt::targetst &ce_locs=
21+
current_program.counterexample_locations;
22+
insert_counterexamples(st, gf, counterexamples, ce_locs);
23+
gf.update();
24+
}
25+
26+
template<class solution_configt>
27+
const symbol_tablet &control_symex_learnt<solution_configt>::get_symbol_table() const
28+
{
29+
return current_program.st;
30+
}
31+
32+
template<class solution_configt>
33+
const goto_functionst &control_symex_learnt<solution_configt>::get_goto_functions() const
34+
{
35+
return current_program.gf;
36+
}
37+
38+
template<class solution_configt>
39+
void control_symex_learnt<solution_configt>::set_word_width(
40+
const size_t word_width_in_bits) const
41+
{
42+
}
43+
44+
template<class solution_configt>
45+
void control_symex_learnt<solution_configt>::convert(
46+
candidatet &current_candidate, const goto_tracet &trace,
47+
const size_t max_solution_size) const
48+
{
49+
solution_configt::convert(current_candidate, trace, current_program.st);
50+
}
51+
52+
template<class solution_configt>
53+
void control_symex_learnt<solution_configt>::show_candidate(
54+
messaget::mstreamt &os, const candidatet &candidate) const
55+
{
56+
solution_configt::show_candidate(os, candidate, current_program.st);
57+
}

‎src/cegis/control/learn/control_symex_learn.cpp renamed to ‎src/cegis/control/learn/rational_solution_configuration.cpp

Lines changed: 11 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -1,46 +1,16 @@
11
#include <ansi-c/expr2c.h>
22
#include <goto-programs/goto_trace.h>
33

4-
#include <cegis/cegis-util/program_helper.h>
5-
#include <cegis/learn/constraint_helper.h>
6-
#include <cegis/learn/insert_counterexample.h>
74
#include <cegis/control/value/control_vars.h>
5+
#include <cegis/control/value/control_solution.h>
86
#include <cegis/control/preprocessing/propagate_controller_sizes.h>
97
#include <cegis/control/learn/nondet_solution.h>
10-
#include <cegis/control/learn/control_symex_learn.h>
8+
#include <cegis/control/learn/rational_solution_configuration.h>
119

12-
control_symex_learnt::control_symex_learnt(
13-
const control_programt &original_program) :
14-
original_program(original_program)
10+
void rational_solution_configurationt::nondeterminise_solution_configuration(
11+
symbol_tablet &st, goto_functionst &gf)
1512
{
16-
}
17-
18-
void control_symex_learnt::process(const counterexamplest &counterexamples,
19-
const size_t max_solution_size)
20-
{
21-
current_program=original_program;
22-
symbol_tablet &st=current_program.st;
23-
goto_functionst &gf=current_program.gf;
2413
nondet_control_solution(st, gf);
25-
transform_asserts_to_assumes(gf);
26-
const goto_programt::targetst &ce_locs=
27-
current_program.counterexample_locations;
28-
insert_counterexamples(st, gf, counterexamples, ce_locs);
29-
gf.update();
30-
}
31-
32-
const symbol_tablet &control_symex_learnt::get_symbol_table() const
33-
{
34-
return current_program.st;
35-
}
36-
37-
const goto_functionst &control_symex_learnt::get_goto_functions() const
38-
{
39-
return current_program.gf;
40-
}
41-
42-
void control_symex_learnt::set_word_width(const size_t word_width_in_bits) const
43-
{
4414
}
4515

4616
namespace
@@ -59,11 +29,12 @@ const struct_exprt &find_solution(const goto_tracet &trace)
5929
}
6030
}
6131

62-
void control_symex_learnt::convert(candidatet &current_candidate,
63-
const goto_tracet &trace, const size_t max_solution_size) const
32+
void rational_solution_configurationt::convert(
33+
control_solutiont &current_candidate, const goto_tracet &trace,
34+
const symbol_tablet &st)
6435
{
6536
const struct_exprt &solution=find_solution(trace);
66-
const namespacet ns(current_program.st);
37+
const namespacet ns(st);
6738
current_candidate.a=get_a_controller_comp(ns, solution);
6839
current_candidate.b=get_b_controller_comp(ns, solution);
6940
}
@@ -84,10 +55,10 @@ void print_array(messaget::mstreamt &os, const array_exprt &array,
8455
}
8556
}
8657

87-
void control_symex_learnt::show_candidate(messaget::mstreamt &os,
88-
const candidatet &candidate) const
58+
59+
void rational_solution_configurationt::show_candidate(messaget::mstreamt &os,
60+
const control_solutiont &candidate, const symbol_tablet &st)
8961
{
90-
const symbol_tablet &st=current_program.st;
9162
print_array(os, candidate.a, "a", st);
9263
print_array(os, candidate.b, "b", st);
9364
}

‎src/cegis/control/learn/rational_solution_configuration.h

Lines changed: 71 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,71 @@
1+
/*******************************************************************
2+
3+
Module: Counterexample-Guided Inductive Synthesis
4+
5+
Author: Daniel Kroening, [email protected]
6+
Pascal Kesseli, [email protected]
7+
8+
\*******************************************************************/
9+
10+
#ifndef CEGIS_CONTROL_LEARN_RATIONAL_SOLUTION_CONFIGURATION_H_
11+
#define CEGIS_CONTROL_LEARN_RATIONAL_SOLUTION_CONFIGURATION_H_
12+
13+
#include <util/message.h>
14+
15+
/**
16+
* @brief
17+
*
18+
* @details
19+
*/
20+
class rational_solution_configurationt
21+
{
22+
public:
23+
/**
24+
* @brief
25+
*
26+
* @details
27+
*/
28+
typedef class control_solutiont solutiont;
29+
30+
/**
31+
* @brief
32+
*
33+
* @details
34+
*
35+
* @param st
36+
* @param gf
37+
*/
38+
static void nondeterminise_solution_configuration(
39+
class symbol_tablet &st,
40+
class goto_functionst &gf);
41+
42+
/**
43+
* @brief
44+
*
45+
* @details
46+
*
47+
* @param current_candidate
48+
* @param trace
49+
* @param st
50+
*/
51+
static void convert(
52+
class control_solutiont &current_candidate,
53+
const class goto_tracet &trace,
54+
const symbol_tablet &st);
55+
56+
/**
57+
* @brief
58+
*
59+
* @details
60+
*
61+
* @param os
62+
* @param candidate
63+
* @param st
64+
*/
65+
static void show_candidate(
66+
messaget::mstreamt &os,
67+
const control_solutiont &candidate,
68+
const symbol_tablet &st);
69+
};
70+
71+
#endif /* CEGIS_CONTROL_LEARN_RATIONAL_SOLUTION_CONFIGURATION_H_ */

0 commit comments

Comments
 (0)