Connect++ 0.6.0
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
Schedule.cpp
1/*
2
3Copyright © 2023-24 Sean Holden. All rights reserved.
4
5*/
6/*
7
8This file is part of Connect++.
9
10Connect++ is free software: you can redistribute it and/or modify it
11under the terms of the GNU General Public License as published by the
12Free Software Foundation, either version 3 of the License, or (at your
13option) any later version.
14
15Connect++ is distributed in the hope that it will be useful, but WITHOUT
16ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
17FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for
18more details.
19
20You should have received a copy of the GNU General Public License along
21with Connect++. If not, see <https://www.gnu.org/licenses/>.
22
23*/
24
25#include "Schedule.hpp"
26
27namespace schedule {
28
29//--------------------------------------------------------------
30string to_string(const schedule_step& s) {
31 switch (s) {
32 case schedule_step::all_definitional:
33 return string("--all-definitional");
34 break;
35 case schedule_step::no_definitional:
36 return string("--no-definitional");
37 break;
38 case schedule_step::reorder:
39 return string("--reorder");
40 break;
41 case schedule_step::rand_reorder:
42 return string("--random-reorder");
43 break;
44 case schedule_step::rand_lits:
45 return string("--random-reorder-literals");
46 break;
47 case schedule_step::all_start:
48 return string("--all-start");
49 break;
50 case schedule_step::pos_neg_start:
51 return string("--pos-neg-start");
52 break;
53 case schedule_step::conjecture_start:
54 return string("--conjecture-start");
55 break;
56 case schedule_step::restrict_start:
57 return string("--restrict-start");
58 break;
59 case schedule_step::no_regularity:
60 return string("--no-regularity");
61 break;
62 case schedule_step::all_lemmata:
63 return string("--all-lemmata");
64 break;
65 case schedule_step::all_reductions:
66 return string("--all-reductions");
67 break;
68 case schedule_step::all_extensions:
69 return string("--all-extensions");
70 break;
71 case schedule_step::no_lemmata:
72 return string("--no-lemmata");
73 break;
74 case schedule_step::all_backtrack:
75 return string("--all-backtrack");
76 break;
77 case schedule_step::lemmata_backtrack:
78 return string("--lemmata-backtrack");
79 break;
80 case schedule_step::reduction_backtrack:
81 return string("--reduction-backtrack");
82 break;
83 case schedule_step::extension_backtrack:
84 return string("--extension-backtrack");
85 break;
86 case schedule_step::explore_left_trees:
87 return string("--explore-left-trees");
88 break;
89 case schedule_step::complete:
90 return string("--complete");
91 break;
92 case schedule_step::start_depth:
93 return string("--start-depth");
94 break;
95 case schedule_step::depth_inc:
96 return string("--depth-increment");
97 break;
98 case schedule_step::limit_by_tree_depth:
99 return string("--limit-by-tree-depth");
100 break;
101 default:
102 break;
103 }
104 return string("");
105}
106//--------------------------------------------------------------
107// Basic material for parser semantic actions.
108//--------------------------------------------------------------
109unsigned int value = 0;
110unsigned int current_time = 0;
111string step;
112vector<pair<schedule_step, unsigned int>> current_settings;
113vector<vector<pair<schedule_step, unsigned int>>> new_schedule;
114vector<unsigned int> new_times;
115//--------------------------------------------------------------
116// Parser semantic actions.
117//--------------------------------------------------------------
118void add_time::operator()(unsigned int t, qi::unused_type,
119 qi::unused_type) const {
120 current_time = t;
121}
122void set_value::operator()(unsigned int v, qi::unused_type,
123 qi::unused_type) const {
124 value = v;
125}
126void set_step::operator()(string s, qi::unused_type,
127 qi::unused_type) const {
128 step = s;
129}
130void add_step::operator()(qi::unused_type, qi::unused_type) const {
131 schedule_step step2;
132 if (step == "--all-definitional") step2 = schedule_step::all_definitional;
133 if (step == "--no-definitional") step2 = schedule_step::no_definitional;
134 if (step == "--reorder") step2 = schedule_step::reorder;
135 // Remember: you *do* need the extra space!
136 if (step == "--random-reorder ") step2 = schedule_step::rand_reorder;
137 if (step == "--random-reorder-literals") step2 = schedule_step::rand_lits;
138 if (step == "--all-start") step2 = schedule_step::all_start;
139 if (step == "--pos-neg-start") step2 = schedule_step::pos_neg_start;
140 if (step == "--conjecture-start") step2 = schedule_step::conjecture_start;
141 if (step == "--restrict-start") step2 = schedule_step::restrict_start;
142 if (step == "--no-regularity") step2 = schedule_step::no_regularity;
143 if (step == "--all-lemmata") step2 = schedule_step::all_lemmata;
144 if (step == "--all-reductions") step2 = schedule_step::all_reductions;
145 if (step == "--all-extensions") step2 = schedule_step::all_extensions;
146 if (step == "--no-lemmata") step2 = schedule_step::no_lemmata;
147 if (step == "--all-backtrack") step2 = schedule_step::all_backtrack;
148 if (step == "--lemmata-backtrack") step2 = schedule_step::lemmata_backtrack;
149 if (step == "--reduction-backtrack") step2 = schedule_step::reduction_backtrack;
150 if (step == "--extension-backtrack") step2 = schedule_step::extension_backtrack;
151 if (step == "--explore-left-trees") step2 = schedule_step::explore_left_trees;
152 if (step == "--complete") step2 = schedule_step::complete;
153 if (step == "--start-depth") step2 = schedule_step::start_depth;
154 if (step == "--depth-increment") step2 = schedule_step::depth_inc;
155 if (step == "--limit-by-tree-depth") step2 = schedule_step::limit_by_tree_depth;
156 current_settings.push_back(pair<schedule_step, unsigned int>(step2, value));
157 step = "";
158 value = 0;
159}
160void next_settings::operator()(qi::unused_type, qi::unused_type) const {
161 new_schedule.push_back(current_settings);
162 new_times.push_back(current_time);
163 current_time = 0;
164 current_settings.clear();
165}
166//--------------------------------------------------------------
167// Basic material for parser.
168//--------------------------------------------------------------
169qi::rule<Iter, string()> schedule_word =
170 ascii::string("--all-definitional")
171 | ascii::string("--no-definitional")
172 // Yes, you do need the extra space so that it doesn't get recognized
173 // instead of --random-reorder-literals!
174 | ascii::string("--random-reorder ")
175 | ascii::string("--random-reorder-literals")
176 | ascii::string("--all-start")
177 | ascii::string("--pos-neg-start")
178 | ascii::string("--conjecture-start")
179 | ascii::string("--restrict-start")
180 | ascii::string("--no-regularity")
181 | ascii::string("--all-lemmata")
182 | ascii::string("--all-reductions")
183 | ascii::string("--all-extensions")
184 | ascii::string("--no-lemmata")
185 | ascii::string("--all-backtrack")
186 | ascii::string("--lemmata-backtrack")
187 | ascii::string("--reduction-backtrack")
188 | ascii::string("--extension-backtrack")
189 | ascii::string("--explore-left-trees")
190 | ascii::string("--limit-by-tree-depth");
191
192qi::rule<Iter, string()> schedule_word_param =
193 ascii::string("--complete")
194 | ascii::string("--reorder")
195 | ascii::string("--start-depth")
196 | ascii::string("--depth-increment");
197//--------------------------------------------------------------
198// Grammar for parser.
199//--------------------------------------------------------------
200template<typename It>
201 struct schedule_grammar
202 : qi::grammar<It, ascii::space_type>
203 {
204 schedule_grammar()
205 : schedule_grammar::base_type(schedule) {
206
207 schedule_item %=
208 ((schedule_word [set_step()])
209 | ((schedule_word_param [set_step()])
210 >> (qi::uint_) [set_value()]));
211
212 schedule_line %=
213 ((qi::uint_ [add_time()])
214 >> *(schedule_item [add_step()])
215 >> lit(';') [next_settings()]);
216
217 schedule %= *schedule_line;
218 }
219 qi::rule<Iter, ascii::space_type> schedule_item;
220 qi::rule<Iter, ascii::space_type> schedule_line;
221 qi::rule<Iter, ascii::space_type> schedule;
222 };
223//--------------------------------------------------------------
224// Implementation of Schedule.
225//--------------------------------------------------------------
226void Schedule::read_schedule_from_file(fs::path path) {
227 string file_contents;
228 if (path == "default") {
229 params::set_default_schedule();
230 file_contents = params::default_schedule;
231 }
232 else {
233 ifstream file;
234 file.open(path);
235 if (file.fail()) {
236 throw (file_open_exception(path));
237 }
238 string current_line;
239 std::getline(file, current_line);
240 file_contents += current_line;
241 while (file.good()) {
242 std::getline(file, current_line);
243 file_contents += current_line;
244 }
245 file.close();
246 }
247
248 Iter start = file_contents.begin();
249 Iter end = file_contents.end();
250
251 schedule_grammar<Iter> g;
252 bool result = qi::phrase_parse(start, end, g, ascii::space);
253
254 if (start != end || !result) {
255 std::cerr << "Failed to parse schedule file." << endl;
256 new_schedule.clear();
257 new_times.clear();
258 }
259 schedule = new_schedule;
260 times = new_times;
261 if (times.back() != 0)
262 std::cerr << "Warning: the last time entry in the schedule should be 0" << endl;
263 unsigned int total = 0;
264 for (unsigned int t : times)
265 total += t;
266 if (total > 100)
267 std::cerr << "Warning: your time percentages add up to more than 100" << endl;
268}
269//--------------------------------------------------------------
270void Schedule::apply_item(const pair<schedule_step,unsigned int>& item) {
271 schedule_step step = item.first;
272 unsigned int value = item.second;
273 switch (step) {
274 case schedule_step::all_definitional:
275 if (params::no_definitional) {
276 params::no_definitional = false;
277 cerr << "Warning: --all-definitional cancels --no-definitional." << endl;
278 }
279 params::all_definitional = true;
280 break;
281 case schedule_step::no_definitional:
282 if (params::all_definitional) {
283 params::all_definitional = false;
284 cerr << "Warning: --no-definitional cancels --all-definitional." << endl;
285 }
286 params::no_definitional = true;
287 break;
288 case schedule_step::reorder:
289 params::deterministic_reorder = true;
290 params::number_of_reorders = value;
291 break;
292 case schedule_step::rand_reorder:
293 params::random_reorder = true;
294 break;
295 case schedule_step::rand_lits:
296 params::random_reorder_literals = true;
297 break;
298 case schedule_step::all_start:
299 params::set_all_start();
300 break;
301 case schedule_step::pos_neg_start:
302 if (params::all_start) {
303 cerr << "Warning: are you sure you want to mix --all-start with --pos-neg-start?" << endl;
304 }
305 params::all_pos_neg_start = true;
306 break;
307 case schedule_step::conjecture_start:
308 if (params::all_start) {
309 cerr << "Warning: are you sure you want to mix --all-start with --conjecture-start?" << endl;
310 }
311 params::conjecture_start = true;
312 break;
313 case schedule_step::restrict_start:
314 if (params::all_start) {
315 cerr << "Warning: are you sure you want to mix --all-start with --restrict-start?" << endl;
316 }
317 params::restrict_start = true;
318 break;
319 case schedule_step::no_regularity:
320 params::use_regularity_test = false;
321 break;
322 case schedule_step::all_lemmata:
323 params::limit_lemmata = false;
324 break;
325 case schedule_step::all_reductions:
326 params::limit_reductions = false;
327 break;
328 case schedule_step::all_extensions:
329 params::limit_extensions = false;
330 break;
331 case schedule_step::no_lemmata:
332 params::use_lemmata = false;
333 break;
334 case schedule_step::all_backtrack:
335 params::set_all_backtrack();
336 break;
337 case schedule_step::lemmata_backtrack:
338 params::limit_bt_lemmas = false;
339 break;
340 case schedule_step::reduction_backtrack:
341 params::limit_bt_reductions = false;
342 break;
343 case schedule_step::extension_backtrack:
344 params::limit_bt_extensions = false;
345 break;
346 case schedule_step::explore_left_trees:
347 params::limit_bt_extensions_left_tree = false;
348 break;
349 case schedule_step::complete:
350 params::switch_to_complete = value;
351 break;
352 case schedule_step::start_depth:
353 params::start_depth = value;
354 break;
355 case schedule_step::depth_inc:
356 params::depth_increment = value;
357 break;
358 case schedule_step::limit_by_tree_depth:
359 params::limit_by_tree_depth = true;
360 break;
361 default:
362 break;
363 }
364}
365//--------------------------------------------------------------
366 pair<bool,unsigned int> Schedule::set_next_schedule() {
367 params::set_default_schedule_parameters();
368 pair<bool,unsigned int> result(false,0);
369 if (schedule_step_number == schedule.size())
370 return result;
371 for(size_t i = 0; i < schedule[schedule_step_number].size(); i++) {
372 apply_item((schedule[schedule_step_number])[i]);
373 }
374 result.first = true;
375 result.second = times[schedule_step_number];
376 schedule_step_number++;
377 /*
378 * Make sure there is something specified as a start clause.
379 */
380 if (params::no_start_options()) {
381 params::correct_missing_start_options();
382 }
383 return result;
384 }
385 //--------------------------------------------------------------
386 string Schedule::step_to_string(size_t n) const {
387 string result("Time: ");
388 if (n < schedule.size()) {
389 result += std::to_string(times[n]);
390 for (size_t j = 0; j < schedule[n].size(); j++) {
391 result += " (";
392 result += to_string((schedule[n])[j].first);
393 result += ", ";
394 result += std::to_string((schedule[n])[j].second);
395 result += ")";
396 }
397 }
398 return result;
399 }
400 //--------------------------------------------------------------
401 ostream& operator<<(ostream& out, const Schedule& s) {
402 for (size_t i = 0; i < s.schedule.size(); i++) {
403 out << s.step_to_string(i) << endl;
404 }
405 return out;
406 }
407
408}
file_open_exception
Exception used by the application in main(...).
Definition Exceptions.hpp:36
schedule::Schedule
Wrap up the parsing process and the operation of a schedule in a single class.
Definition Schedule.hpp:107
schedule::Schedule::schedule
vector< vector< pair< schedule_step, unsigned int > > > schedule
Representation of a schedule.
Definition Schedule.hpp:115
schedule::Schedule::read_schedule_from_file
void read_schedule_from_file(fs::path)
Self-explanatory.
Definition Schedule.cpp:226
schedule::Schedule::times
vector< unsigned int > times
Times for each member of a schedule.
Definition Schedule.hpp:119
schedule::Schedule::schedule_step_number
size_t schedule_step_number
Keep track of which step in the schedule we're on.
Definition Schedule.hpp:123
schedule::Schedule::apply_item
void apply_item(const pair< schedule_step, unsigned int > &)
Apply the settings for a single step in a schedule.
Definition Schedule.cpp:270
schedule::Schedule::step_to_string
string step_to_string(size_t) const
Make a string representation of a line in the schedule.
Definition Schedule.cpp:386
schedule::Schedule::set_next_schedule
pair< bool, unsigned int > set_next_schedule()
Apply the settings for the next step in the schedule.
Definition Schedule.cpp:366
schedule
Hide all the global stuff in this namespace.
Definition Schedule.cpp:27
schedule::schedule_step
schedule_step
Possible kinds of schedule step.
Definition Schedule.hpp:63
params::set_default_schedule_parameters
static void set_default_schedule_parameters()
Self-explanatory.
Definition Parameters.cpp:182
params::set_all_backtrack
static void set_all_backtrack()
Self-explanatory.
Definition Parameters.cpp:239
params::set_all_start
static void set_all_start()
Self-explanatory.
Definition Parameters.cpp:261
params::no_start_options
static bool no_start_options()
Self-explanatory.
Definition Parameters.cpp:247
params::correct_missing_start_options
static void correct_missing_start_options()
Self-explanatory.
Definition Parameters.cpp:254
schedule::add_step
Semantic action for parser.
Definition Schedule.hpp:185
schedule::add_time
Semantic action for parser.
Definition Schedule.hpp:167
schedule::next_settings
Semantic action for parser.
Definition Schedule.hpp:191
schedule::schedule_grammar
Definition Schedule.cpp:203
schedule::set_step
Semantic action for parser.
Definition Schedule.hpp:179
schedule::set_value
Semantic action for parser.
Definition Schedule.hpp:173