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:

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 107 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 133 of file Schedule.hpp.

: schedule(), times(), schedule_step_number(0) {};

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 270 of file Schedule.cpp.

                                                                      {
    schedule_step step = item.first;
    unsigned int value = item.second;
    switch (step) {
        case schedule_step::all_definitional:
            if (params::no_definitional) {
                params::no_definitional = false;
                cerr << "Warning: --all-definitional cancels --no-definitional." << endl;
            }
            params::all_definitional = true;
            break;
        case schedule_step::no_definitional:
            if (params::all_definitional) {
                params::all_definitional = false;
                cerr << "Warning: --no-definitional cancels --all-definitional." << endl;
            }
            params::no_definitional = true;
            break;
        case schedule_step::reorder:
            params::deterministic_reorder = true;
            params::number_of_reorders = value;
            break;
        case schedule_step::rand_reorder:
            params::random_reorder = true;
            break;
        case schedule_step::rand_lits:
            params::random_reorder_literals = true;
            break;
        case schedule_step::all_start:
            params::set_all_start();
            break;
        case schedule_step::pos_neg_start:
            if (params::all_start) {
                cerr << "Warning: are you sure you want to mix --all-start with --pos-neg-start?" << endl;
            }
            params::all_pos_neg_start = true;
            break;
        case schedule_step::conjecture_start:
            if (params::all_start) {
                cerr << "Warning: are you sure you want to mix --all-start with --conjecture-start?" << endl;
            }
            params::conjecture_start = true;
            break;
        case schedule_step::restrict_start:
            if (params::all_start) {
                cerr << "Warning: are you sure you want to mix --all-start with --restrict-start?" << endl;
            }
            params::restrict_start = true;
            break;
        case schedule_step::no_regularity:
            params::use_regularity_test = false;
            break;
        case schedule_step::all_lemmata:
            params::limit_lemmata = false;
            break;
        case schedule_step::all_reductions:
            params::limit_reductions = false;
            break;
        case schedule_step::all_extensions:
            params::limit_extensions = false;
            break;
        case schedule_step::no_lemmata:
            params::use_lemmata = false;
            break;
        case schedule_step::all_backtrack:
            params::set_all_backtrack();
            break;
        case schedule_step::lemmata_backtrack:
            params::limit_bt_lemmas = false;
            break;
        case schedule_step::reduction_backtrack:
            params::limit_bt_reductions = false;
            break;
        case schedule_step::extension_backtrack:
            params::limit_bt_extensions = false;
            break;
        case schedule_step::explore_left_trees:
            params::limit_bt_extensions_left_tree = false;
            break;
        case schedule_step::complete:
            params::switch_to_complete = value;
            break;
        case schedule_step::start_depth:
            params::start_depth = value;
            break;
        case schedule_step::depth_inc:
            params::depth_increment = value;
            break;
        case schedule_step::limit_by_tree_depth:
            params::limit_by_tree_depth = true;
            break;
        default:
            break;
    }
}

read_schedule_from_file()

void schedule::Schedule::read_schedule_from_file

(

fs::path

path

)

Self-explanatory.

Produces an empty schedule if parsing fails.

Parameters

path	Path of file to read from.

Definition at line 226 of file Schedule.cpp.

                                                  {
    string file_contents;
    if (path == "default") {
        params::set_default_schedule();
        file_contents = params::default_schedule;
    }
    else {
        ifstream file;
        file.open(path);
        if (file.fail()) {
            throw (file_open_exception(path));
        }
        string current_line;
        std::getline(file, current_line);
        file_contents += current_line;
        while (file.good()) {
            std::getline(file, current_line);
            file_contents += current_line;
        }
        file.close();
    }
   
    Iter start = file_contents.begin();
    Iter end = file_contents.end();
 
    schedule_grammar<Iter> g;
    bool result = qi::phrase_parse(start, end, g, ascii::space);
 
    if (start != end || !result) {
        std::cerr << "Failed to parse schedule file." << endl;
        new_schedule.clear();
        new_times.clear();
    }
    schedule = new_schedule;
    times = new_times;
    if (times.back() != 0)
        std::cerr << "Warning: the last time entry in the schedule should be 0" << endl;
    unsigned int total = 0;
    for (unsigned int t : times) 
        total += t;
    if (total > 100) 
        std::cerr << "Warning: your time percentages add up to more than 100" << endl;
}   

reset_schedule()

void schedule::Schedule::reset_schedule ( )

inline

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

Definition at line 138 of file Schedule.hpp.

{ schedule_step_number = 0; }

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 366 of file Schedule.cpp.

                                                     {
    params::set_default_schedule_parameters();
    pair<bool,unsigned int> result(false,0);
    if (schedule_step_number == schedule.size())
        return result;
    for(size_t i = 0; i < schedule[schedule_step_number].size(); i++) {
        apply_item((schedule[schedule_step_number])[i]);
    }
    result.first = true;
    result.second = times[schedule_step_number];
    schedule_step_number++;
    /*
    * Make sure there is something specified as a start clause.
    */
    if (params::no_start_options()) {
        params::correct_missing_start_options();
    }
    return result;
 }

step_to_string()

string schedule::Schedule::step_to_string

(

size_t

n

)

const

Make a string representation of a line in the schedule.

Parameters

n	Line to convert.

Returns

String representation.

Definition at line 386 of file Schedule.cpp.

                                               {
    string result("Time: ");
    if (n < schedule.size()) {
        result += std::to_string(times[n]);
        for (size_t j = 0; j < schedule[n].size(); j++) {
            result += " (";
            result += to_string((schedule[n])[j].first);
            result += ", ";
            result += std::to_string((schedule[n])[j].second);
            result += ")";
        }
    }
    return result; 
 }

Friends And Related Symbol Documentation

operator<<

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

friend

Definition at line 401 of file Schedule.cpp.

                                                      {
    for (size_t i = 0; i < s.schedule.size(); i++) {
        out << s.step_to_string(i) << endl;
    }
    return out;
 }

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 115 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 123 of file Schedule.hpp.

times

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

private

Times for each member of a schedule.

Definition at line 119 of file Schedule.hpp.

---

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

• /Users/sbh11/Desktop/connection-prover/c++/connect++/source/Schedule.hpp
• /Users/sbh11/Desktop/connection-prover/c++/connect++/source/Schedule.cpp