Connect++ 0.5.0
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
Classes | Enumerations | Functions | Variables
schedule Namespace Reference

Hide all the global stuff in this namespace. More...

Classes

struct  add_step
 Semantic action for parser. More...
 
struct  add_time
 Semantic action for parser. More...
 
struct  next_settings
 Semantic action for parser. More...
 
class  Schedule
 Wrap up the parsing process and the operation of a schedule in a single class. More...
 
struct  schedule_grammar
 
struct  set_step
 Semantic action for parser. More...
 
struct  set_value
 Semantic action for parser. More...
 

Enumerations

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
}
 Possible kinds of schedule step. More...
 

Functions

string to_string (const schedule_step &s)
 
ostream & operator<< (ostream &out, const Schedule &s)
 

Variables

unsigned int value = 0
 
unsigned int current_time = 0
 
string step
 
vector< pair< schedule_step, unsigned int > > current_settings
 
vector< vector< pair< schedule_step, unsigned int > > > new_schedule
 
vector< unsigned int > new_times
 
qi::rule< Iter, string()> schedule_word
 
qi::rule< Iter, string()> schedule_word_param
 

Detailed Description

Hide all the global stuff in this namespace.

It's easiest to implement a parser using the relevant boost libraries if you use globals to store things as you parse. Hiding them in a namespace makes the use of globals a bit less reprehensible.

Enumeration Type Documentation

◆ schedule_step

enum class schedule::schedule_step
strong

Possible kinds of schedule step.

Definition at line 63 of file Schedule.hpp.

63 {
64 all_definitional,
65 no_definitional,
66 reorder,
67 rand_reorder,
68 rand_lits,
69 all_start,
70 pos_neg_start,
71 conjecture_start,
72 restrict_start,
73 no_regularity,
74 all_lemmata,
75 all_reductions,
76 all_extensions,
77 no_lemmata,
78 all_backtrack,
79 lemmata_backtrack,
80 reduction_backtrack,
81 extension_backtrack,
82 explore_left_trees,
83 complete,
84 start_depth,
85 depth_inc,
86 limit_by_tree_depth
87};

Function Documentation

◆ operator<<()

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

Definition at line 401 of file Schedule.cpp.

401 {
402 for (size_t i = 0; i < s.schedule.size(); i++) {
403 out << s.step_to_string(i) << endl;
404 }
405 return out;
406 }
schedule::Schedule::schedule
vector< vector< pair< schedule_step, unsigned int > > > schedule
Representation of a schedule.
Definition Schedule.hpp:118
schedule::Schedule::step_to_string
string step_to_string(size_t) const
Make a string representation of a line in the schedule.
Definition Schedule.cpp:386

◆ to_string()

string schedule::to_string ( const schedule_step & s)

Definition at line 30 of file Schedule.cpp.

30 {
31 switch (s) {
32 case schedule_step::all_definitional:
33 return string("--all-definitional");
34 break;
35 case schedule_step::no_definitional:
36 return string("--no-definitional");
37 break;
38 case schedule_step::reorder:
39 return string("--reorder");
40 break;
41 case schedule_step::rand_reorder:
42 return string("--random-reorder");
43 break;
44 case schedule_step::rand_lits:
45 return string("--random-reorder-literals");
46 break;
47 case schedule_step::all_start:
48 return string("--all-start");
49 break;
50 case schedule_step::pos_neg_start:
51 return string("--pos-neg-start");
52 break;
53 case schedule_step::conjecture_start:
54 return string("--conjecture-start");
55 break;
56 case schedule_step::restrict_start:
57 return string("--restrict-start");
58 break;
59 case schedule_step::no_regularity:
60 return string("--no-regularity");
61 break;
62 case schedule_step::all_lemmata:
63 return string("--all-lemmata");
64 break;
65 case schedule_step::all_reductions:
66 return string("--all-reductions");
67 break;
68 case schedule_step::all_extensions:
69 return string("--all-extensions");
70 break;
71 case schedule_step::no_lemmata:
72 return string("--no-lemmata");
73 break;
74 case schedule_step::all_backtrack:
75 return string("--all-backtrack");
76 break;
77 case schedule_step::lemmata_backtrack:
78 return string("--lemmata-backtrack");
79 break;
80 case schedule_step::reduction_backtrack:
81 return string("--reduction-backtrack");
82 break;
83 case schedule_step::extension_backtrack:
84 return string("--extension-backtrack");
85 break;
86 case schedule_step::explore_left_trees:
87 return string("--explore-left-trees");
88 break;
89 case schedule_step::complete:
90 return string("--complete");
91 break;
92 case schedule_step::start_depth:
93 return string("--start-depth");
94 break;
95 case schedule_step::depth_inc:
96 return string("--depth-increment");
97 break;
98 case schedule_step::limit_by_tree_depth:
99 return string("--limit-by-tree-depth");
100 break;
101 default:
102 break;
103 }
104 return string("");
105}

Variable Documentation

◆ current_settings

vector<pair<schedule_step, unsigned int> > schedule::current_settings

Definition at line 112 of file Schedule.cpp.

◆ current_time

unsigned int schedule::current_time = 0

Definition at line 110 of file Schedule.cpp.

◆ new_schedule

vector<vector<pair<schedule_step, unsigned int> > > schedule::new_schedule

Definition at line 113 of file Schedule.cpp.

◆ new_times

vector<unsigned int> schedule::new_times

Definition at line 114 of file Schedule.cpp.

◆ schedule_word

qi::rule<Iter, string()> schedule::schedule_word
Initial value:
=
ascii::string("--all-definitional")
| ascii::string("--no-definitional")
| ascii::string("--random-reorder ")
| ascii::string("--random-reorder-literals")
| ascii::string("--all-start")
| ascii::string("--pos-neg-start")
| ascii::string("--conjecture-start")
| ascii::string("--restrict-start")
| ascii::string("--no-regularity")
| ascii::string("--all-lemmata")
| ascii::string("--all-reductions")
| ascii::string("--all-extensions")
| ascii::string("--no-lemmata")
| ascii::string("--all-backtrack")
| ascii::string("--lemmata-backtrack")
| ascii::string("--reduction-backtrack")
| ascii::string("--extension-backtrack")
| ascii::string("--explore-left-trees")
| ascii::string("--limit-by-tree-depth")

Definition at line 169 of file Schedule.cpp.

◆ schedule_word_param

qi::rule<Iter, string()> schedule::schedule_word_param
Initial value:
=
ascii::string("--complete")
| ascii::string("--reorder")
| ascii::string("--start-depth")
| ascii::string("--depth-increment")

Definition at line 192 of file Schedule.cpp.

◆ step

string schedule::step

Definition at line 111 of file Schedule.cpp.

◆ value

unsigned int schedule::value = 0

Definition at line 109 of file Schedule.cpp.