32 case schedule_step::all_definitional:
33 return string(
"--all-definitional");
35 case schedule_step::no_definitional:
36 return string(
"--no-definitional");
38 case schedule_step::reorder:
39 return string(
"--reorder");
41 case schedule_step::rand_reorder:
42 return string(
"--random-reorder");
44 case schedule_step::rand_lits:
45 return string(
"--random-reorder-literals");
47 case schedule_step::all_start:
48 return string(
"--all-start");
50 case schedule_step::pos_neg_start:
51 return string(
"--pos-neg-start");
53 case schedule_step::conjecture_start:
54 return string(
"--conjecture-start");
56 case schedule_step::restrict_start:
57 return string(
"--restrict-start");
59 case schedule_step::no_regularity:
60 return string(
"--no-regularity");
62 case schedule_step::all_lemmata:
63 return string(
"--all-lemmata");
65 case schedule_step::all_reductions:
66 return string(
"--all-reductions");
68 case schedule_step::all_extensions:
69 return string(
"--all-extensions");
71 case schedule_step::no_lemmata:
72 return string(
"--no-lemmata");
74 case schedule_step::all_backtrack:
75 return string(
"--all-backtrack");
77 case schedule_step::lemmata_backtrack:
78 return string(
"--lemmata-backtrack");
80 case schedule_step::reduction_backtrack:
81 return string(
"--reduction-backtrack");
83 case schedule_step::extension_backtrack:
84 return string(
"--extension-backtrack");
86 case schedule_step::explore_left_trees:
87 return string(
"--explore-left-trees");
89 case schedule_step::complete:
90 return string(
"--complete");
92 case schedule_step::start_depth:
93 return string(
"--start-depth");
95 case schedule_step::depth_inc:
96 return string(
"--depth-increment");
106unsigned int value = 0;
107unsigned int current_time = 0;
109vector<pair<schedule_step, unsigned int>> current_settings;
110vector<vector<pair<schedule_step, unsigned int>>> new_schedule;
111vector<unsigned int> new_times;
115void add_time::operator()(
unsigned int t, qi::unused_type,
116 qi::unused_type)
const {
119void set_value::operator()(
unsigned int v, qi::unused_type,
120 qi::unused_type)
const {
123void set_step::operator()(
string s, qi::unused_type,
124 qi::unused_type)
const {
127void add_step::operator()(qi::unused_type, qi::unused_type)
const {
129 if (step ==
"--all-definitional") step2 = schedule_step::all_definitional;
130 if (step ==
"--no-definitional") step2 = schedule_step::no_definitional;
131 if (step ==
"--reorder") step2 = schedule_step::reorder;
133 if (step ==
"--random-reorder ") step2 = schedule_step::rand_reorder;
134 if (step ==
"--random-reorder-literals") step2 = schedule_step::rand_lits;
135 if (step ==
"--all-start") step2 = schedule_step::all_start;
136 if (step ==
"--pos-neg-start") step2 = schedule_step::pos_neg_start;
137 if (step ==
"--conjecture-start") step2 = schedule_step::conjecture_start;
138 if (step ==
"--restrict-start") step2 = schedule_step::restrict_start;
139 if (step ==
"--no-regularity") step2 = schedule_step::no_regularity;
140 if (step ==
"--all-lemmata") step2 = schedule_step::all_lemmata;
141 if (step ==
"--all-reductions") step2 = schedule_step::all_reductions;
142 if (step ==
"--all-extensions") step2 = schedule_step::all_extensions;
143 if (step ==
"--no-lemmata") step2 = schedule_step::no_lemmata;
144 if (step ==
"--all-backtrack") step2 = schedule_step::all_backtrack;
145 if (step ==
"--lemmata-backtrack") step2 = schedule_step::lemmata_backtrack;
146 if (step ==
"--reduction-backtrack") step2 = schedule_step::reduction_backtrack;
147 if (step ==
"--extension-backtrack") step2 = schedule_step::extension_backtrack;
148 if (step ==
"--explore-left-trees") step2 = schedule_step::explore_left_trees;
149 if (step ==
"--complete") step2 = schedule_step::complete;
150 if (step ==
"--start-depth") step2 = schedule_step::start_depth;
151 if (step ==
"--depth-increment") step2 = schedule_step::depth_inc;
152 current_settings.push_back(pair<schedule_step, unsigned int>(step2, value));
156void next_settings::operator()(qi::unused_type, qi::unused_type)
const {
157 new_schedule.push_back(current_settings);
158 new_times.push_back(current_time);
160 current_settings.clear();
165qi::rule<Iter, string()> schedule_word =
166 ascii::string(
"--all-definitional")
167 | ascii::string(
"--no-definitional")
170 | ascii::string(
"--random-reorder ")
171 | ascii::string(
"--random-reorder-literals")
172 | ascii::string(
"--all-start")
173 | ascii::string(
"--pos-neg-start")
174 | ascii::string(
"--conjecture-start")
175 | ascii::string(
"--restrict-start")
176 | ascii::string(
"--no-regularity")
177 | ascii::string(
"--all-lemmata")
178 | ascii::string(
"--all-reductions")
179 | ascii::string(
"--all-extensions")
180 | ascii::string(
"--no-lemmata")
181 | ascii::string(
"--all-backtrack")
182 | ascii::string(
"--lemmata-backtrack")
183 | ascii::string(
"--reduction-backtrack")
184 | ascii::string(
"--extension-backtrack")
185 | ascii::string(
"--explore-left-trees")
186 | ascii::string(
"--limit-by-tree-depth");
188qi::rule<Iter, string()> schedule_word_param =
189 ascii::string(
"--complete")
190 | ascii::string(
"--reorder")
191 | ascii::string(
"--start-depth")
192 | ascii::string(
"--depth-increment");
198 : qi::grammar<It, ascii::space_type>
201 : schedule_grammar::base_type(
schedule) {
205 | ((schedule_word_param [
set_step()])
215 qi::rule<Iter, ascii::space_type> schedule_item;
216 qi::rule<Iter, ascii::space_type> schedule_line;
217 qi::rule<Iter, ascii::space_type>
schedule;
223 string file_contents;
224 if (path ==
"default") {
225 params::set_default_schedule();
226 file_contents = params::default_schedule;
235 std::getline(file, current_line);
236 file_contents += current_line;
237 while (file.good()) {
238 std::getline(file, current_line);
239 file_contents += current_line;
244 Iter start = file_contents.begin();
245 Iter end = file_contents.end();
248 bool result = qi::phrase_parse(start, end, g, ascii::space);
250 if (start != end || !result) {
251 std::cerr <<
"Failed to parse schedule file." << endl;
252 new_schedule.clear();
257 if (
times.back() != 0)
258 std::cerr <<
"Warning: the last time entry in the schedule should be 0" << endl;
259 unsigned int total = 0;
260 for (
unsigned int t :
times)
263 std::cerr <<
"Warning: your time percentages add up to more than 100" << endl;
268 unsigned int value = item.second;
270 case schedule_step::all_definitional:
271 if (params::no_definitional) {
272 params::no_definitional =
false;
273 cerr <<
"Warning: --all-definitional cancels --no-definitional." << endl;
275 params::all_definitional =
true;
277 case schedule_step::no_definitional:
278 if (params::all_definitional) {
279 params::all_definitional =
false;
280 cerr <<
"Warning: --no-definitional cancels --all-definitional." << endl;
282 params::no_definitional =
true;
284 case schedule_step::reorder:
285 params::deterministic_reorder =
true;
286 params::number_of_reorders = value;
288 case schedule_step::rand_reorder:
289 params::random_reorder =
true;
291 case schedule_step::rand_lits:
292 params::random_reorder_literals =
true;
294 case schedule_step::all_start:
297 case schedule_step::pos_neg_start:
298 if (params::all_start) {
299 cerr <<
"Warning: are you sure you want to mix --all-start with --pos-neg-start?" << endl;
301 params::all_pos_neg_start =
true;
303 case schedule_step::conjecture_start:
304 if (params::all_start) {
305 cerr <<
"Warning: are you sure you want to mix --all-start with --conjecture-start?" << endl;
307 params::conjecture_start =
true;
309 case schedule_step::restrict_start:
310 if (params::all_start) {
311 cerr <<
"Warning: are you sure you want to mix --all-start with --restrict-start?" << endl;
313 params::restrict_start =
true;
315 case schedule_step::no_regularity:
316 params::use_regularity_test =
false;
318 case schedule_step::all_lemmata:
319 params::limit_lemmata =
false;
321 case schedule_step::all_reductions:
322 params::limit_reductions =
false;
324 case schedule_step::all_extensions:
325 params::limit_extensions =
false;
327 case schedule_step::no_lemmata:
328 params::use_lemmata =
false;
330 case schedule_step::all_backtrack:
333 case schedule_step::lemmata_backtrack:
334 params::limit_bt_lemmas =
false;
336 case schedule_step::reduction_backtrack:
337 params::limit_bt_reductions =
false;
339 case schedule_step::extension_backtrack:
340 params::limit_bt_extensions =
false;
342 case schedule_step::explore_left_trees:
343 params::limit_bt_extensions_left_tree =
false;
345 case schedule_step::complete:
346 params::switch_to_complete = value;
348 case schedule_step::start_depth:
349 params::start_depth = value;
351 case schedule_step::depth_inc:
352 params::depth_increment = value;
361 pair<bool,unsigned int> result(
false,0);
380 string result(
"Time: ");
382 result += std::to_string(
times[n]);
383 for (
size_t j = 0; j <
schedule[n].size(); j++) {
385 result += to_string((
schedule[n])[j].first);
387 result += std::to_string((
schedule[n])[j].second);
394 ostream& operator<<(ostream& out,
const Schedule& s) {
395 for (
size_t i = 0; i < s.
schedule.size(); i++) {