Connect++ 0.1
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
Schedule.hpp
1/*
2
3Copyright © 2023 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#ifndef SCHEDULE_HPP
26#define SCHEDULE_HPP
27
28#include<iostream>
29#include<string>
30#include<filesystem>
31#include <fstream>
32
33#include <boost/spirit/include/qi.hpp>
34
35#include "Parameters.hpp"
36#include "Exceptions.hpp"
37
38using std::string;
39using std::vector;
40using std::ifstream;
41using std::ostream;
42using std::cout;
43using std::endl;
44using std::pair;
45using namespace boost::spirit;
46using Iter = string::const_iterator;
47
48namespace fs = std::filesystem;
49
58namespace schedule {
62enum class schedule_step {
63 reorder,
64 all_start,
65 pos_neg_start,
66 conjecture_start,
67 restrict_start,
68 no_regularity,
69 no_lemmata,
70 all_lemmata,
71 all_reductions,
72 all_extensions,
73 all_backtrack,
74 lemmata_backtrack,
75 reduction_backtrack,
76 extension_backtrack,
77 explore_left_trees,
78 hard_prune,
79 complete
80};
81string to_string(const schedule_step&);
100class Schedule {
101private:
108 vector<vector<pair<schedule_step,unsigned int>>> schedule;
112 vector<unsigned int> times;
116 size_t schedule_step_number;
120 void apply_item(const pair<schedule_step,unsigned int>&);
121public:
126 Schedule() : schedule(), times(), schedule_step_number(0) {};
131 void reset_schedule() { schedule_step_number = 0; }
138 string step_to_string(size_t) const;
153 pair<bool,unsigned int> set_next_schedule();
154
155 friend ostream& operator<<(ostream&, const Schedule&);
156};
160struct add_time {
161 void operator()(unsigned int, qi::unused_type, qi::unused_type) const;
162};
166struct set_value {
167 void operator()(unsigned int, qi::unused_type, qi::unused_type) const;
168};
172struct set_step {
173 void operator()(string, qi::unused_type, qi::unused_type) const;
174};
178struct add_step {
179 void operator()(qi::unused_type, qi::unused_type) const;
180};
184struct next_settings {
185 void operator()(qi::unused_type, qi::unused_type) const;
186};
187
188}
189
190#endif
Wrap up the parsing process and the operation of a schedule in a single class.
Definition Schedule-16-10-23.hpp:90
void read_schedule_from_file(fs::path)
Self-explanatory.
Schedule()
You only need this constructor because everything will be filled in by the parser.
Definition Schedule.hpp:126
void reset_schedule()
Go back to the beginning of the schedule but leave everything else intact.
Definition Schedule.hpp:131
string step_to_string(size_t) const
Make a string representation of a line in the schedule.
pair< bool, unsigned int > set_next_schedule()
Apply the settings for the next step in the schedule.
Hide all the global stuff in this namespace.
Definition Schedule-16-10-23.cpp:27
schedule_step
Possible kinds of schedule step.
Definition Schedule-16-10-23.hpp:62
Semantic action for parser.
Definition Schedule-16-10-23.hpp:150