Connect++ 0.3.0
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
Public Member Functions | Private Member Functions | Private Attributes | Friends | List of all members
schedule::Schedule Class Reference

Wrap up the parsing process and the operation of a schedule in a single class. More...

#include <Schedule.hpp>

Collaboration diagram for schedule::Schedule:
Collaboration graph
[legend]

Public Member Functions

 Schedule ()
 You only need this constructor because everything will be filled in by the parser.
 
void reset_schedule ()
 Go back to the beginning of the schedule but leave everything else intact.
 
string step_to_string (size_t) const
 Make a string representation of a line in the schedule.
 
void read_schedule_from_file (fs::path)
 Self-explanatory.
 
pair< bool, unsigned int > set_next_schedule ()
 Apply the settings for the next step in the schedule.
 

Private Member Functions

void apply_item (const pair< schedule_step, unsigned int > &)
 Apply the settings for a single step in a schedule.
 

Private Attributes

vector< vector< pair< schedule_step, unsigned int > > > schedule
 Representation of a schedule.
 
vector< unsigned int > times
 Times for each member of a schedule.
 
size_t schedule_step_number
 Keep track of which step in the schedule we're on.
 

Friends

ostream & operator<< (ostream &, const Schedule &)
 

Detailed Description

Wrap up the parsing process and the operation of a schedule in a single class.

This covers parsing, and also the sequencing, including manipulation of parameters for each step, of a schedule stored in a file.

The main elements of a file exactly mimic the command line options, so a single step in a schedule acts exactly as though the relevant options had been supplied to a single call from the command line.

Aside from that, a line ends with a semicolon, and there is a number at the start of the line specifying a percentage of the timeout. The last line should start with 0, specifying "all remaining".

Definition at line 100 of file Schedule.hpp.

Constructor & Destructor Documentation

◆ Schedule()

schedule::Schedule::Schedule ( )
inline

You only need this constructor because everything will be filled in by the parser.

Definition at line 126 of file Schedule.hpp.

vector< vector< pair< schedule_step, unsigned int > > > schedule
Representation of a schedule.
Definition Schedule.hpp:108
vector< unsigned int > times
Times for each member of a schedule.
Definition Schedule.hpp:112
size_t schedule_step_number
Keep track of which step in the schedule we're on.
Definition Schedule.hpp:116

Member Function Documentation

◆ apply_item()

void schedule::Schedule::apply_item ( const pair< schedule_step, unsigned int > &  item)
private

Apply the settings for a single step in a schedule.

Definition at line 237 of file Schedule.cpp.

237 {
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:
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:
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}
schedule_step
Possible kinds of schedule step.
Definition Schedule.hpp:62
static void set_all_backtrack()
Self-explanatory.
static void set_all_start()
Self-explanatory.

◆ read_schedule_from_file()

void schedule::Schedule::read_schedule_from_file ( fs::path  path)

Self-explanatory.

Produces an empty schedule if parsing fails.

Parameters
pathPath of file to read from.

Definition at line 193 of file Schedule.cpp.

193 {
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}
Exception used by the application in main(...).
Hide all the global stuff in this namespace.
Definition Schedule.cpp:27

◆ reset_schedule()

void schedule::Schedule::reset_schedule ( )
inline

Go back to the beginning of the schedule but leave everything else intact.

Definition at line 131 of file Schedule.hpp.

◆ set_next_schedule()

pair< bool, unsigned int > schedule::Schedule::set_next_schedule ( )

Apply the settings for the next step in the schedule.

Returns
True and the percentage of time to run for if successful, false and 0 otherwise.

Definition at line 298 of file Schedule.cpp.

298 {
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++) {
305 }
306 result.first = true;
307 result.second = times[schedule_step_number];
309 /*
310 * Make sure there is something specified as a start clause.
311 */
314 }
315 return result;
316 }
void apply_item(const pair< schedule_step, unsigned int > &)
Apply the settings for a single step in a schedule.
Definition Schedule.cpp:237
static void set_default_schedule_parameters()
Self-explanatory.
static bool no_start_options()
Self-explanatory.
static void correct_missing_start_options()
Self-explanatory.

◆ step_to_string()

string schedule::Schedule::step_to_string ( size_t  n) const

Make a string representation of a line in the schedule.

Parameters
nLine to convert.
Returns
String representation.

Definition at line 318 of file Schedule.cpp.

318 {
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 }

Friends And Related Symbol Documentation

◆ operator<<

ostream & operator<< ( ostream &  out,
const Schedule s 
)
friend

Definition at line 333 of file Schedule.cpp.

333 {
334 for (size_t i = 0; i < s.schedule.size(); i++) {
335 out << s.step_to_string(i) << endl;
336 }
337 return out;
338 }

Member Data Documentation

◆ schedule

vector<vector<pair<schedule_step,unsigned int> > > schedule::Schedule::schedule
private

Representation of a schedule.

Each element is a vector of pairs. Each pair is an identifier for a step, and an integer. Times are dealt with elsewhere.

Definition at line 108 of file Schedule.hpp.

◆ schedule_step_number

size_t schedule::Schedule::schedule_step_number
private

Keep track of which step in the schedule we're on.

Definition at line 116 of file Schedule.hpp.

◆ times

vector<unsigned int> schedule::Schedule::times
private

Times for each member of a schedule.

Definition at line 112 of file Schedule.hpp.


The documentation for this class was generated from the following files: