Connect++ 0.6.1
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
Schedule.cpp
1/*
2
3Copyright © 2023-25 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 default:
99 break;
100 }
101 return string("");
102}
103//--------------------------------------------------------------
104// Basic material for parser semantic actions.
105//--------------------------------------------------------------
106unsigned int value = 0;
107unsigned int current_time = 0;
108string step;
109vector<pair<schedule_step, unsigned int>> current_settings;
110vector<vector<pair<schedule_step, unsigned int>>> new_schedule;
111vector<unsigned int> new_times;
112//--------------------------------------------------------------
113// Parser semantic actions.
114//--------------------------------------------------------------
115void add_time::operator()(unsigned int t, qi::unused_type,
116 qi::unused_type) const {
117 current_time = t;
118}
119void set_value::operator()(unsigned int v, qi::unused_type,
120 qi::unused_type) const {
121 value = v;
122}
123void set_step::operator()(string s, qi::unused_type,
124 qi::unused_type) const {
125 step = s;
126}
127void add_step::operator()(qi::unused_type, qi::unused_type) const {
128 schedule_step step2;
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;
132 // Remember: you *do* need the extra space!
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));
153 step = "";
154 value = 0;
155}
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);
159 current_time = 0;
160 current_settings.clear();
161}
162//--------------------------------------------------------------
163// Basic material for parser.
164//--------------------------------------------------------------
165qi::rule<Iter, string()> schedule_word =
166 ascii::string("--all-definitional")
167 | ascii::string("--no-definitional")
168 // Yes, you do need the extra space so that it doesn't get recognized
169 // instead of --random-reorder-literals!
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");
187
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");
193//--------------------------------------------------------------
194// Grammar for parser.
195//--------------------------------------------------------------
196template<typename It>
198 : qi::grammar<It, ascii::space_type>
199 {
201 : schedule_grammar::base_type(schedule) {
202
203 schedule_item %=
204 ((schedule_word [set_step()])
205 | ((schedule_word_param [set_step()])
206 >> (qi::uint_) [set_value()]));
207
208 schedule_line %=
209 ((qi::uint_ [add_time()])
210 >> *(schedule_item [add_step()])
211 >> lit(';') [next_settings()]);
212
213 schedule %= *schedule_line;
214 }
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;
218 };
219//--------------------------------------------------------------
220// Implementation of Schedule.
221//--------------------------------------------------------------
223 string file_contents;
224 if (path == "default") {
225 params::set_default_schedule();
226 file_contents = params::default_schedule;
227 }
228 else {
229 ifstream file;
230 file.open(path);
231 if (file.fail()) {
232 throw (file_open_exception(path));
233 }
234 string current_line;
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;
240 }
241 file.close();
242 }
243
244 Iter start = file_contents.begin();
245 Iter end = file_contents.end();
246
248 bool result = qi::phrase_parse(start, end, g, ascii::space);
249
250 if (start != end || !result) {
251 std::cerr << "Failed to parse schedule file." << endl;
252 new_schedule.clear();
253 new_times.clear();
254 }
255 schedule = new_schedule;
256 times = new_times;
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)
261 total += t;
262 if (total > 100)
263 std::cerr << "Warning: your time percentages add up to more than 100" << endl;
264}
265//--------------------------------------------------------------
266void Schedule::apply_item(const pair<schedule_step,unsigned int>& item) {
267 schedule_step step = item.first;
268 unsigned int value = item.second;
269 switch (step) {
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;
274 }
275 params::all_definitional = true;
276 break;
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;
281 }
282 params::no_definitional = true;
283 break;
284 case schedule_step::reorder:
285 params::deterministic_reorder = true;
286 params::number_of_reorders = value;
287 break;
288 case schedule_step::rand_reorder:
289 params::random_reorder = true;
290 break;
291 case schedule_step::rand_lits:
292 params::random_reorder_literals = true;
293 break;
294 case schedule_step::all_start:
296 break;
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;
300 }
301 params::all_pos_neg_start = true;
302 break;
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;
306 }
307 params::conjecture_start = true;
308 break;
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;
312 }
313 params::restrict_start = true;
314 break;
315 case schedule_step::no_regularity:
316 params::use_regularity_test = false;
317 break;
318 case schedule_step::all_lemmata:
319 params::limit_lemmata = false;
320 break;
321 case schedule_step::all_reductions:
322 params::limit_reductions = false;
323 break;
324 case schedule_step::all_extensions:
325 params::limit_extensions = false;
326 break;
327 case schedule_step::no_lemmata:
328 params::use_lemmata = false;
329 break;
330 case schedule_step::all_backtrack:
332 break;
333 case schedule_step::lemmata_backtrack:
334 params::limit_bt_lemmas = false;
335 break;
336 case schedule_step::reduction_backtrack:
337 params::limit_bt_reductions = false;
338 break;
339 case schedule_step::extension_backtrack:
340 params::limit_bt_extensions = false;
341 break;
342 case schedule_step::explore_left_trees:
343 params::limit_bt_extensions_left_tree = false;
344 break;
345 case schedule_step::complete:
346 params::switch_to_complete = value;
347 break;
348 case schedule_step::start_depth:
349 params::start_depth = value;
350 break;
351 case schedule_step::depth_inc:
352 params::depth_increment = value;
353 break;
354 default:
355 break;
356 }
357}
358//--------------------------------------------------------------
359 pair<bool,unsigned int> Schedule::set_next_schedule() {
361 pair<bool,unsigned int> result(false,0);
362 if (schedule_step_number == schedule.size())
363 return result;
364 for(size_t i = 0; i < schedule[schedule_step_number].size(); i++) {
366 }
367 result.first = true;
368 result.second = times[schedule_step_number];
370 /*
371 * Make sure there is something specified as a start clause.
372 */
375 }
376 return result;
377 }
378 //--------------------------------------------------------------
379 string Schedule::step_to_string(size_t n) const {
380 string result("Time: ");
381 if (n < schedule.size()) {
382 result += std::to_string(times[n]);
383 for (size_t j = 0; j < schedule[n].size(); j++) {
384 result += " (";
385 result += to_string((schedule[n])[j].first);
386 result += ", ";
387 result += std::to_string((schedule[n])[j].second);
388 result += ")";
389 }
390 }
391 return result;
392 }
393 //--------------------------------------------------------------
394 ostream& operator<<(ostream& out, const Schedule& s) {
395 for (size_t i = 0; i < s.schedule.size(); i++) {
396 out << s.step_to_string(i) << endl;
397 }
398 return out;
399 }
400
401}
Exception used by the application in main(...).
Wrap up the parsing process and the operation of a schedule in a single class.
Definition Schedule.hpp:107
vector< vector< pair< schedule_step, unsigned int > > > schedule
Representation of a schedule.
Definition Schedule.hpp:115
void read_schedule_from_file(fs::path)
Self-explanatory.
Definition Schedule.cpp:222
vector< unsigned int > times
Times for each member of a schedule.
Definition Schedule.hpp:119
size_t schedule_step_number
Keep track of which step in the schedule we're on.
Definition Schedule.hpp:123
void apply_item(const pair< schedule_step, unsigned int > &)
Apply the settings for a single step in a schedule.
Definition Schedule.cpp:266
string step_to_string(size_t) const
Make a string representation of a line in the schedule.
Definition Schedule.cpp:379
pair< bool, unsigned int > set_next_schedule()
Apply the settings for the next step in the schedule.
Definition Schedule.cpp:359
Hide all the global stuff in this namespace.
Definition Schedule.cpp:27
schedule_step
Possible kinds of schedule step.
Definition Schedule.hpp:63
static void set_default_schedule_parameters()
Self-explanatory.
static void set_all_backtrack()
Self-explanatory.
static void set_all_start()
Self-explanatory.
static bool no_start_options()
Self-explanatory.
static void correct_missing_start_options()
Self-explanatory.
Semantic action for parser.
Definition Schedule.hpp:185
Semantic action for parser.
Definition Schedule.hpp:167
Semantic action for parser.
Definition Schedule.hpp:191
Semantic action for parser.
Definition Schedule.hpp:179
Semantic action for parser.
Definition Schedule.hpp:173