Schedule.hpp

/*
 
Copyright © 2023-24 Sean Holden. All rights reserved.
 
*/
/*
 
This file is part of Connect++.
 
Connect++ is free software: you can redistribute it and/or modify it 
under the terms of the GNU General Public License as published by the 
Free Software Foundation, either version 3 of the License, or (at your 
option) any later version.
 
Connect++ is distributed in the hope that it will be useful, but WITHOUT 
ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or 
FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for 
more details.
 
You should have received a copy of the GNU General Public License along 
with Connect++. If not, see <https://www.gnu.org/licenses/>. 
 
*/
 
#ifndef SCHEDULE_HPP
#define SCHEDULE_HPP
 
#include<iostream>
#include<string>
#include<filesystem>
#include <fstream>
 
#include <boost/spirit/include/qi.hpp>
 
#include "Parameters.hpp"
#include "Exceptions.hpp"
 
using std::string;
using std::vector;
using std::ifstream;
using std::ostream;
using std::cout;
using std::cerr;
using std::endl;
using std::pair;
using namespace boost::spirit;
using Iter = string::const_iterator;
 
namespace fs = std::filesystem;
 
namespace schedule {
enum class schedule_step {
  all_definitional,
  no_definitional,
  reorder,
  rand_reorder,
  rand_lits,
  all_start,
  pos_neg_start,
  conjecture_start,
  restrict_start,
  no_regularity,
  all_lemmata,
  all_reductions,
  all_extensions,
  no_lemmata,
  all_backtrack,
  lemmata_backtrack,
  reduction_backtrack,
  extension_backtrack,
  explore_left_trees,
  complete,
  start_depth,
  depth_inc,
  limit_by_tree_depth
};
string to_string(const schedule_step&);
class Schedule {
private:
    vector<vector<pair<schedule_step,unsigned int>>> schedule;
    vector<unsigned int> times;
    size_t schedule_step_number;
    void apply_item(const pair<schedule_step,unsigned int>&);
public:
    Schedule() : schedule(), times(), schedule_step_number(0) {};
    void reset_schedule() { schedule_step_number = 0; }
    string step_to_string(size_t) const;
    void read_schedule_from_file(fs::path);
    pair<bool,unsigned int> set_next_schedule();
 
    friend ostream& operator<<(ostream&, const Schedule&);
};
struct add_time {
    void operator()(unsigned int, qi::unused_type, qi::unused_type) const;
};
struct set_value {
    void operator()(unsigned int, qi::unused_type, qi::unused_type) const;
};
struct set_step {
    void operator()(string, qi::unused_type, qi::unused_type) const;
};
struct add_step {
    void operator()(qi::unused_type, qi::unused_type) const;
};
struct next_settings {
    void operator()(qi::unused_type, qi::unused_type) const;
};
 
}
 
#endif