Connect++ 0.3.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::reorder:
33 return string("--reorder");
34 break;
35 case schedule_step::all_start:
36 return string("--all-start");
37 break;
38 case schedule_step::pos_neg_start:
39 return string("--pos-neg-start");
40 break;
41 case schedule_step::conjecture_start:
42 return string("--conjecture-start");
43 break;
44 case schedule_step::restrict_start:
45 return string("--restrict-start");
46 break;
47 case schedule_step::no_regularity:
48 return string("--no-regularity");
49 break;
50 case schedule_step::no_lemmata:
51 return string("--no-lemmata");
52 break;
53 case schedule_step::all_lemmata:
54 return string("--all-lemmata");
55 break;
56 case schedule_step::all_reductions:
57 return string("--all-reductions");
58 break;
59 case schedule_step::all_extensions:
60 return string("--all-extensions");
61 break;
62 case schedule_step::all_backtrack:
63 return string("--all-backtrack");
64 break;
65 case schedule_step::lemmata_backtrack:
66 return string("--lemmata-backtrack");
67 break;
68 case schedule_step::reduction_backtrack:
69 return string("--reduction-backtrack");
70 break;
71 case schedule_step::extension_backtrack:
72 return string("--extension-backtrack");
73 break;
74 case schedule_step::explore_left_trees:
75 return string("--explore-left-trees");
76 break;
77 case schedule_step::hard_prune:
78 return string("--hard-prune");
79 break;
80 case schedule_step::complete:
81 return string("--complete");
82 break;
83 default:
84 break;
85 }
86 return string("");
87}
88//--------------------------------------------------------------
89// Basic material for parser semantic actions.
90//--------------------------------------------------------------
91unsigned int value = 0;
92unsigned int current_time = 0;
93string step;
94vector<pair<schedule_step, unsigned int>> current_settings;
95vector<vector<pair<schedule_step, unsigned int>>> new_schedule;
96vector<unsigned int> new_times;
97//--------------------------------------------------------------
98// Parser semantic actions.
99//--------------------------------------------------------------
100void add_time::operator()(unsigned int t, qi::unused_type,
101 qi::unused_type) const {
102 current_time = t;
103}
104void set_value::operator()(unsigned int v, qi::unused_type,
105 qi::unused_type) const {
106 value = v;
107}
108void set_step::operator()(string s, qi::unused_type,
109 qi::unused_type) const {
110 step = s;
111}
112void add_step::operator()(qi::unused_type, qi::unused_type) const {
113 schedule_step step2;
114 if (step == "--reorder") step2 = schedule_step::reorder;
115 if (step == "--all-start") step2 = schedule_step::all_start;
116 if (step == "--pos-neg-start") step2 = schedule_step::pos_neg_start;
117 if (step == "--conjecture-start") step2 = schedule_step::conjecture_start;
118 if (step == "--restrict-start") step2 = schedule_step::restrict_start;
119 if (step == "--no-regularity") step2 = schedule_step::no_regularity;
120 if (step == "--no-lemmata") step2 = schedule_step::no_lemmata;
121 if (step == "--all-lemmata") step2 = schedule_step::all_lemmata;
122 if (step == "--all-reductions") step2 = schedule_step::all_reductions;
123 if (step == "--all-extensions") step2 = schedule_step::all_extensions;
124 if (step == "--all-backtrack") step2 = schedule_step::all_backtrack;
125 if (step == "--lemmata-backtrack") step2 = schedule_step::lemmata_backtrack;
126 if (step == "--reduction-backtrack") step2 = schedule_step::reduction_backtrack;
127 if (step == "--extension-backtrack") step2 = schedule_step::extension_backtrack;
128 if (step == "--explore-left-trees") step2 = schedule_step::explore_left_trees;
129 if (step == "--hard-prune") step2 = schedule_step::hard_prune;
130 if (step == "--complete") step2 = schedule_step::complete;
131 current_settings.push_back(pair<schedule_step, unsigned int>(step2, value));
132 step = "";
133 value = 0;
134}
135void next_settings::operator()(qi::unused_type, qi::unused_type) const {
136 new_schedule.push_back(current_settings);
137 new_times.push_back(current_time);
138 current_time = 0;
139 current_settings.clear();
140}
141//--------------------------------------------------------------
142// Basic material for parser.
143//--------------------------------------------------------------
144qi::rule<Iter, string()> schedule_word =
145 ascii::string("--all-start")
146 | ascii::string("--pos-neg-start")
147 | ascii::string("--conjecture-start")
148 | ascii::string("--restrict-start")
149 | ascii::string("--no-regularity")
150 | ascii::string("--no-lemmata")
151 | ascii::string("--all-lemmata")
152 | ascii::string("--all-reductions")
153 | ascii::string("--all-extensions")
154 | ascii::string("--all-backtrack")
155 | ascii::string("--lemmata-backtrack")
156 | ascii::string("--reduction-backtrack")
157 | ascii::string("--extension-backtrack")
158 | ascii::string("--explore-left-trees")
159 | ascii::string("--hard-prune");
160
161qi::rule<Iter, string()> schedule_word_param =
162 ascii::string("--complete")
163 | ascii::string("--reorder");
164//--------------------------------------------------------------
165// Grammar for parser.
166//--------------------------------------------------------------
167template<typename It>
168 struct schedule_grammar
169 : qi::grammar<It, ascii::space_type>
170 {
171 schedule_grammar()
172 : schedule_grammar::base_type(schedule) {
173
174 schedule_item %=
175 ((schedule_word [set_step()])
176 | ((schedule_word_param [set_step()])
177 >> (qi::uint_) [set_value()]));
178
179 schedule_line %=
180 ((qi::uint_ [add_time()])
181 >> *(schedule_item [add_step()])
182 >> lit(';') [next_settings()]);
183
184 schedule %= *schedule_line;
185 }
186 qi::rule<Iter, ascii::space_type> schedule_item;
187 qi::rule<Iter, ascii::space_type> schedule_line;
188 qi::rule<Iter, ascii::space_type> schedule;
189 };
190//--------------------------------------------------------------
191// Implementation of Schedule.
192//--------------------------------------------------------------
193void Schedule::read_schedule_from_file(fs::path path) {
194 string file_contents;
195 if (path == "default") {
196 params::set_default_schedule();
197 file_contents = params::default_schedule;
198 }
199 else {
200 ifstream file;
201 file.open(path);
202 if (file.fail()) {
203 throw (file_open_exception(path));
204 }
205 string current_line;
206 std::getline(file, current_line);
207 file_contents += current_line;
208 while (file.good()) {
209 std::getline(file, current_line);
210 file_contents += current_line;
211 }
212 file.close();
213 }
214
215 Iter start = file_contents.begin();
216 Iter end = file_contents.end();
217
218 schedule_grammar<Iter> g;
219 bool result = qi::phrase_parse(start, end, g, ascii::space);
220
221 if (start != end || !result) {
222 std::cerr << "Failed to parse schedule file." << endl;
223 new_schedule.clear();
224 new_times.clear();
225 }
226 schedule = new_schedule;
227 times = new_times;
228 if (times.back() != 0)
229 std::cerr << "Warning: the last time entry in the schedule should be 0" << endl;
230 unsigned int total = 0;
231 for (unsigned int t : times)
232 total += t;
233 if (total > 100)
234 std::cerr << "Warning: your time percentages add up to more than 100" << endl;
235}
236//--------------------------------------------------------------
237void Schedule::apply_item(const pair<schedule_step,unsigned int>& item) {
238 schedule_step step = item.first;
239 unsigned int value = item.second;
240 switch (step) {
241 case schedule_step::reorder:
242 params::deterministic_reorder = true;
243 params::number_of_reorders = value;
244 break;
245 case schedule_step::all_start:
246 params::set_all_start();
247 break;
248 case schedule_step::pos_neg_start:
249 params::all_pos_neg_start = true;
250 break;
251 case schedule_step::conjecture_start:
252 params::conjecture_start = true;
253 break;
254 case schedule_step::restrict_start:
255 params::restrict_start = true;
256 break;
257 case schedule_step::no_regularity:
258 params::use_regularity_test = false;
259 break;
260 case schedule_step::no_lemmata:
261 params::use_lemmata = false;
262 break;
263 case schedule_step::all_lemmata:
264 params::limit_lemmata = false;
265 break;
266 case schedule_step::all_reductions:
267 params::limit_reductions = false;
268 break;
269 case schedule_step::all_extensions:
270 params::limit_extensions = false;
271 break;
272 case schedule_step::all_backtrack:
273 params::set_all_backtrack();
274 break;
275 case schedule_step::lemmata_backtrack:
276 params::limit_bt_lemmas = false;
277 break;
278 case schedule_step::reduction_backtrack:
279 params::limit_bt_reductions = false;
280 break;
281 case schedule_step::extension_backtrack:
282 params::limit_bt_extensions = false;
283 break;
284 case schedule_step::explore_left_trees:
285 params::limit_bt_extensions_left_tree = false;
286 break;
287 case schedule_step::hard_prune:
288 params::hard_prune = true;
289 break;
290 case schedule_step::complete:
291 params::switch_to_complete = value;
292 break;
293 default:
294 break;
295 }
296}
297//--------------------------------------------------------------
298 pair<bool,unsigned int> Schedule::set_next_schedule() {
299 params::set_default_schedule_parameters();
300 pair<bool,unsigned int> result(false,0);
301 if (schedule_step_number == schedule.size())
302 return result;
303 for(size_t i = 0; i < schedule[schedule_step_number].size(); i++) {
304 apply_item((schedule[schedule_step_number])[i]);
305 }
306 result.first = true;
307 result.second = times[schedule_step_number];
308 schedule_step_number++;
309 /*
310 * Make sure there is something specified as a start clause.
311 */
312 if (params::no_start_options()) {
313 params::correct_missing_start_options();
314 }
315 return result;
316 }
317 //--------------------------------------------------------------
318 string Schedule::step_to_string(size_t n) const {
319 string result("Time: ");
320 if (n < schedule.size()) {
321 result += std::to_string(times[n]);
322 for (size_t j = 0; j < schedule[n].size(); j++) {
323 result += " (";
324 result += to_string((schedule[n])[j].first);
325 result += ", ";
326 result += std::to_string((schedule[n])[j].second);
327 result += ")";
328 }
329 }
330 return result;
331 }
332 //--------------------------------------------------------------
333 ostream& operator<<(ostream& out, const Schedule& s) {
334 for (size_t i = 0; i < s.schedule.size(); i++) {
335 out << s.step_to_string(i) << endl;
336 }
337 return out;
338 }
339
340}
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:100
schedule::Schedule::schedule
vector< vector< pair< schedule_step, unsigned int > > > schedule
Representation of a schedule.
Definition Schedule.hpp:108
schedule::Schedule::read_schedule_from_file
void read_schedule_from_file(fs::path)
Self-explanatory.
Definition Schedule.cpp:193
schedule::Schedule::times
vector< unsigned int > times
Times for each member of a schedule.
Definition Schedule.hpp:112
schedule::Schedule::schedule_step_number
size_t schedule_step_number
Keep track of which step in the schedule we're on.
Definition Schedule.hpp:116
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:237
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:318
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:298
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:62
params::set_default_schedule_parameters
static void set_default_schedule_parameters()
Self-explanatory.
Definition Parameters.cpp:155
params::set_all_backtrack
static void set_all_backtrack()
Self-explanatory.
Definition Parameters.cpp:204
params::set_all_start
static void set_all_start()
Self-explanatory.
Definition Parameters.cpp:226
params::no_start_options
static bool no_start_options()
Self-explanatory.
Definition Parameters.cpp:212
params::correct_missing_start_options
static void correct_missing_start_options()
Self-explanatory.
Definition Parameters.cpp:219
schedule::add_step
Semantic action for parser.
Definition Schedule.hpp:178
schedule::add_time
Semantic action for parser.
Definition Schedule.hpp:160
schedule::next_settings
Semantic action for parser.
Definition Schedule.hpp:184
schedule::schedule_grammar
Definition Schedule.cpp:170
schedule::set_step
Semantic action for parser.
Definition Schedule.hpp:172
schedule::set_value
Semantic action for parser.
Definition Schedule.hpp:166
Generated by doxygen 1.9.7