Connect++ 0.3.0
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
Schedule.hpp
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#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;
120 void apply_item(const pair<schedule_step,unsigned int>&);
121public:
138 string step_to_string(size_t) const;
146 void read_schedule_from_file(fs::path);
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};
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.hpp:100
vector< vector< pair< schedule_step, unsigned int > > > schedule
Representation of a schedule.
Definition Schedule.hpp:108
void read_schedule_from_file(fs::path)
Self-explanatory.
Definition Schedule.cpp:193
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
void apply_item(const pair< schedule_step, unsigned int > &)
Apply the settings for a single step in a schedule.
Definition Schedule.cpp:237
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.
Definition Schedule.cpp:318
pair< bool, unsigned int > set_next_schedule()
Apply the settings for the next step in the schedule.
Definition Schedule.cpp:298
Hide all the global stuff in this namespace.
Definition Schedule.cpp:27
schedule_step
Possible kinds of schedule step.
Definition Schedule.hpp:62
Semantic action for parser.
Definition Schedule.hpp:178
Semantic action for parser.
Definition Schedule.hpp:160
Semantic action for parser.
Definition Schedule.hpp:184
Semantic action for parser.
Definition Schedule.hpp:172
Semantic action for parser.
Definition Schedule.hpp:166