Connect++ 0.7.0
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
Static Public Member Functions | Static Public Attributes | List of all members
params Struct Reference

Structure containing all the command line and other options. More...

#include <Parameters.hpp>

Collaboration diagram for params:
Collaboration graph
[legend]

Static Public Member Functions

static void set_default_schedule ()
 
static void set_default_schedule_parameters ()
 Self-explanatory.
 
static void set_complete_parameters ()
 Change the parameters to make the search complete.
 
static bool search_is_complete ()
 Self-explanatory.
 
static void set_all_backtrack ()
 Self-explanatory.
 
static bool no_start_options ()
 Self-explanatory.
 
static void correct_missing_start_options ()
 Self-explanatory.
 
static void set_all_start ()
 Self-explanatory.
 
static void show_search_parameter_settings ()
 Give a detailed indication of what the parameters affecting the search are currently set to.
 

Static Public Attributes

static uint8_t verbosity = 2
 
static bool use_colours = true
 
static uint8_t indent_size = 4
 
static uint8_t output_width = 7
 
static uint32_t output_frequency = 500000
 
static bool output_terms_with_substitution = false
 
static std::string problem_name = "Unknown"
 
static bool write_output_summary = false
 
static std::string definitional_predicate_prefix = "sP"
 
static std::string unique_var_prefix = "U_"
 
static std::string unique_skolem_prefix = "sK"
 
static bool show_full_stats = true
 
static bool first_parse = true
 
static bool miniscope = true
 
static bool all_definitional = false
 
static bool no_definitional = false
 
static bool add_equality_axioms = true
 
static bool equality_axioms_at_start = true
 
static bool all_distinct_objects = false
 
static bool no_distinct_objects = false
 
static unsigned random_seed = 0
 
static uint32_t boost_random_seed = 0
 
static bool deterministic_reorder = false
 
static uint32_t number_of_reorders = 0
 
static bool random_reorder = false
 
static bool random_reorder_literals = false
 
static bool timeout = false
 
static uint32_t timeout_value = UINT32_MAX
 
static std::chrono::steady_clock::time_point global_timeout
 
static bool use_schedule = false
 
static bool positive_representation = false
 
static uint32_t start_depth = 2
 
static uint32_t depth_limit = UINT32_MAX
 
static uint32_t depth_increment = 1
 
static bool all_start = false
 
static bool all_pos_neg_start = false
 
static bool conjecture_start = false
 
static bool restrict_start = false
 
static bool use_regularity_test = true
 
static bool use_lemmata = true
 
static bool limit_lemmata = true
 
static bool limit_reductions = true
 
static bool limit_extensions = true
 
static bool limit_bt_all = true
 
static bool limit_bt_lemmas = true
 
static bool limit_bt_reductions = true
 
static bool limit_bt_extensions = true
 
static bool limit_bt_extensions_left_tree = true
 
static uint32_t switch_to_complete = UINT32_MAX
 
static bool poly_unification = false
 
static size_t clause_copy_cache_start_size = 5
 
static size_t clause_copy_cache_increment = 1
 
static size_t stack_start_size = 5000
 
static size_t stack_increment = 0
 
static bool verify_proof_verbose = false
 
static bool verify_proof = false
 
static bool build_proof = false
 
static bool generate_LaTeX_proof = false
 
static bool generate_LaTeX_tableau_proof = false
 
static bool generate_graphviz_tableau_proof = false
 
static bool latex_tableau_subs = false
 
static bool graphviz_tableau_subs = false
 
static bool sub_LaTeX_proof = false
 
static bool sub_Graphviz_proof = false
 
static int latex_truncation_length = 25
 
static bool latex_tiny_proof = false
 
static bool latex_include_matrix = true
 
static string latex_height = "500mm"
 
static string latex_width = "500mm"
 
static float graphviz_height = 11.69
 
static float graphviz_width = 8.27
 
static bool latex_body_only = false
 
static bool generate_Prolog_proof = false
 
static bool generate_tptp_proof = false
 
static bool tptp_proof_to_file = false
 
static bool tptp_proof_no_subs = false
 
static bool tptp_proof_show_paths = false
 
static bool tptp_proof_show_subs = false
 
static bool all_tptp_records = false
 
static bool generate_sc_tptp_proof = false
 
static std::filesystem::path LaTeX_proof_path = "latex_proof.tex"
 
static std::filesystem::path LaTeX_tableau_proof_path = "latex_tableau_proof.tex"
 
static std::filesystem::path graphviz_tableau_proof_path = "graphviz_tableau_proof.dot"
 
static std::filesystem::path Prolog_matrix_path = "matrix.pl"
 
static std::filesystem::path Prolog_proof_path = "proof.pl"
 
static std::filesystem::path output_summary_path = "output_summary.txt"
 
static std::filesystem::path schedule_path = "."
 
static std::filesystem::path tptp_path = "."
 
static std::filesystem::path tptp_proof_path = "."
 
static std::filesystem::path pwd_path = "."
 
static std::filesystem::path connectpp_path = "."
 
static std::filesystem::path full_problem_path
 
static std::string default_schedule
 
static bool show_clauses = false
 

Detailed Description

Structure containing all the command line and other options.

Pretty much everything is static, because that makes sense.

There are also a small number of methods for setting defaults and testing for whether the configuration used leads to a complete search.

In most cases the name of the parameter should make it self-explanatory. So parameters are only explicitly documented where necessary.

Definition at line 51 of file Parameters.hpp.

Member Function Documentation

◆ correct_missing_start_options()

void params::correct_missing_start_options ( )
static

Self-explanatory.

Definition at line 278 of file Parameters.cpp.

278 {
279 all_start = false;
280 all_pos_neg_start = true;
281 conjecture_start = false;
282 restrict_start = false;
283}

◆ no_start_options()

bool params::no_start_options ( )
static

Self-explanatory.

Definition at line 271 of file Parameters.cpp.

271 {
272 return !all_start &&
273 !all_pos_neg_start &&
274 !conjecture_start &&
275 !restrict_start;
276}

◆ search_is_complete()

bool params::search_is_complete ( )
static

Self-explanatory.

Definition at line 251 of file Parameters.cpp.

251 {
252 bool start_conditions_ok =
253 (all_pos_neg_start || all_start) && !restrict_start && !conjecture_start;
254
255 // You don't care about lemmas.
256 bool backtracking_ok =
257 !limit_bt_all && !limit_bt_reductions && !limit_bt_extensions &&
258 !limit_bt_extensions_left_tree;
259
260 return start_conditions_ok && backtracking_ok;
261}

◆ set_all_backtrack()

void params::set_all_backtrack ( )
static

Self-explanatory.

Definition at line 263 of file Parameters.cpp.

263 {
264 limit_bt_all = false;
265 limit_bt_lemmas = false;
266 limit_bt_reductions = false;
267 limit_bt_extensions = false;
268 limit_bt_extensions_left_tree = false;
269}

◆ set_all_start()

void params::set_all_start ( )
static

Self-explanatory.

Definition at line 285 of file Parameters.cpp.

285 {
286 all_start = true;
287 all_pos_neg_start = false;
288 conjecture_start = false;
289 restrict_start = false;
290}

◆ set_complete_parameters()

void params::set_complete_parameters ( )
static

Change the parameters to make the search complete.

Definition at line 239 of file Parameters.cpp.

239 {
240 all_start = false;
241 all_pos_neg_start = true;
242 conjecture_start = false;
243 restrict_start = false;
244
245 limit_bt_all = false;
246 limit_bt_reductions = false;
247 limit_bt_extensions = false;
248 limit_bt_extensions_left_tree = false;
249}

◆ set_default_schedule()

void params::set_default_schedule ( )
static

Definition at line 172 of file Parameters.cpp.

172 {
173 default_schedule = "10 --complete 7 ;\n";
174 default_schedule += "15 --conjecture-start --all-definitional ;\n";
175 default_schedule += "15 --no-definitional --restrict-start ;\n";
176 default_schedule += "10 --restrict-start --all-backtrack ;\n";
177 default_schedule += "5 --all-definitional ;\n";
178 default_schedule += "4 --conjecture-start --no-definitional ;\n";
179 default_schedule += "2 --all-definitional --restrict-start ;\n";
180 default_schedule += "2 --restrict-start ;\n";
181 default_schedule += "1 --conjecture-start --all-definitional --all-backtrack ;\n";
182 default_schedule += "4 --random-reorder --random-reorder-literals --conjecture-start --no-definitional --restrict-start ;\n";
183 default_schedule += "4 --random-reorder --random-reorder-literals --all-definitional --restrict-start ;\n";
184 default_schedule += "2 --random-reorder --random-reorder-literals --all-definitional --restrict-start ;\n";
185 default_schedule += "2 --random-reorder --random-reorder-literals --all-definitional --restrict-start ;\n";
186 default_schedule += "2 --random-reorder --random-reorder-literals --no-definitional ;\n";
187 default_schedule += "2 --random-reorder --random-reorder-literals --conjecture-start --all-definitional ;\n";
188 default_schedule += "2 --random-reorder --random-reorder-literals --conjecture-start --all-definitional ;\n";
189 default_schedule += "1 --random-reorder --random-reorder-literals --conjecture-start --all-definitional ;\n";
190 default_schedule += "1 --random-reorder --random-reorder-literals --conjecture-start --all-definitional ;\n";
191 default_schedule += "1 --random-reorder --random-reorder-literals --conjecture-start --no-definitional --restrict-start ;\n";
192 default_schedule += "1 --random-reorder --random-reorder-literals --conjecture-start --no-definitional --restrict-start ;\n";
193 default_schedule += "1 --random-reorder --random-reorder-literals --conjecture-start --no-definitional --restrict-start ;\n";
194 default_schedule += "1 --random-reorder --random-reorder-literals --conjecture-start --no-definitional --restrict-start --all-backtrack ;\n";
195 default_schedule += "1 --random-reorder --random-reorder-literals --conjecture-start --no-definitional --restrict-start --all-backtrack ;\n";
196 default_schedule += "1 --random-reorder --random-reorder-literals --all-definitional --restrict-start --all-backtrack ;\n";
197 default_schedule += "1 --random-reorder --random-reorder-literals --all-definitional --restrict-start ;\n";
198 default_schedule += "1 --random-reorder --random-reorder-literals --all-definitional --restrict-start ;\n";
199 default_schedule += "1 --random-reorder --random-reorder-literals --no-definitional ;\n";
200 default_schedule += "1 --random-reorder --random-reorder-literals --no-definitional ;\n";
201 default_schedule += "1 --random-reorder --random-reorder-literals --no-definitional --restrict-start --all-backtrack ;\n";
202 default_schedule += "0 --all-definitional --all-backtrack ;\n";
203}

◆ set_default_schedule_parameters()

void params::set_default_schedule_parameters ( )
static

Self-explanatory.

IMPORTANT: these should match the values set in Parameters.cpp, as the assumption is that a schedule modifies them using commands mimicking the command line options.

Definition at line 207 of file Parameters.cpp.

207 {
208 all_definitional = false;
209 no_definitional = false;
210
211 deterministic_reorder = false;
212 number_of_reorders = 0;
213 random_reorder = false;
214 random_reorder_literals = false;
215
216 start_depth = 2;
217 depth_increment = 1;
218
219 all_start = false;
220 all_pos_neg_start = false;
221 conjecture_start = false;
222 restrict_start = false;
223
224 use_regularity_test = true;
225
226 use_lemmata = true;
227 limit_lemmata = true;
228 limit_reductions = true;
229 limit_extensions = true;
230 limit_bt_all = true;
231 limit_bt_lemmas = true;
232 limit_bt_reductions = true;
233 limit_bt_extensions = true;
234 limit_bt_extensions_left_tree = true;
235
236 switch_to_complete = UINT32_MAX;
237}

◆ show_search_parameter_settings()

void params::show_search_parameter_settings ( )
static

Give a detailed indication of what the parameters affecting the search are currently set to.

Definition at line 292 of file Parameters.cpp.

292 {
293 cout << std::boolalpha
294 << "all_definitional: " << all_definitional << endl
295 << "no_definitional: " << no_definitional << endl
296 << "all_start: " << all_start << endl
297 << "all_pos_neg_start: " << all_pos_neg_start << endl
298 << "conjecture_start: " << conjecture_start << endl
299 << "restrict_start: " << restrict_start << endl
300 << "limit_bt_all: " << limit_bt_all << endl
301 << "switch_to_complete: " << switch_to_complete
302 << std::noboolalpha;
303}

Member Data Documentation

◆ add_equality_axioms

bool params::add_equality_axioms = true
static

Definition at line 78 of file Parameters.hpp.

◆ all_definitional

bool params::all_definitional = false
static

Definition at line 73 of file Parameters.hpp.

◆ all_distinct_objects

bool params::all_distinct_objects = false
static

Definition at line 80 of file Parameters.hpp.

◆ all_pos_neg_start

bool params::all_pos_neg_start = false
static

Definition at line 115 of file Parameters.hpp.

◆ all_start

bool params::all_start = false
static

Definition at line 114 of file Parameters.hpp.

◆ all_tptp_records

bool params::all_tptp_records = false
static

Definition at line 176 of file Parameters.hpp.

◆ boost_random_seed

uint32_t params::boost_random_seed = 0
static

Definition at line 86 of file Parameters.hpp.

◆ build_proof

bool params::build_proof = false
static

Definition at line 154 of file Parameters.hpp.

◆ clause_copy_cache_increment

size_t params::clause_copy_cache_increment = 1
static

Definition at line 146 of file Parameters.hpp.

◆ clause_copy_cache_start_size

size_t params::clause_copy_cache_start_size = 5
static

Definition at line 145 of file Parameters.hpp.

◆ conjecture_start

bool params::conjecture_start = false
static

Definition at line 116 of file Parameters.hpp.

◆ connectpp_path

std::filesystem::path params::connectpp_path = "."
static

Definition at line 191 of file Parameters.hpp.

◆ default_schedule

std::string params::default_schedule
static

Definition at line 196 of file Parameters.hpp.

◆ definitional_predicate_prefix

std::string params::definitional_predicate_prefix = "sP"
static

Definition at line 64 of file Parameters.hpp.

◆ depth_increment

uint32_t params::depth_increment = 1
static

Definition at line 110 of file Parameters.hpp.

◆ depth_limit

uint32_t params::depth_limit = UINT32_MAX
static

Definition at line 109 of file Parameters.hpp.

◆ deterministic_reorder

bool params::deterministic_reorder = false
static

Definition at line 87 of file Parameters.hpp.

◆ equality_axioms_at_start

bool params::equality_axioms_at_start = true
static

Definition at line 79 of file Parameters.hpp.

◆ first_parse

bool params::first_parse = true
static

Definition at line 68 of file Parameters.hpp.

◆ full_problem_path

std::filesystem::path params::full_problem_path
static

Definition at line 192 of file Parameters.hpp.

◆ generate_graphviz_tableau_proof

bool params::generate_graphviz_tableau_proof = false
static

Definition at line 157 of file Parameters.hpp.

◆ generate_LaTeX_proof

bool params::generate_LaTeX_proof = false
static

Definition at line 155 of file Parameters.hpp.

◆ generate_LaTeX_tableau_proof

bool params::generate_LaTeX_tableau_proof = false
static

Definition at line 156 of file Parameters.hpp.

◆ generate_Prolog_proof

bool params::generate_Prolog_proof = false
static

Definition at line 170 of file Parameters.hpp.

◆ generate_sc_tptp_proof

bool params::generate_sc_tptp_proof = false
static

Definition at line 177 of file Parameters.hpp.

◆ generate_tptp_proof

bool params::generate_tptp_proof = false
static

Definition at line 171 of file Parameters.hpp.

◆ global_timeout

std::chrono::steady_clock::time_point params::global_timeout
static

Definition at line 96 of file Parameters.hpp.

◆ graphviz_height

float params::graphviz_height = 11.69
static

Definition at line 167 of file Parameters.hpp.

◆ graphviz_tableau_proof_path

std::filesystem::path params::graphviz_tableau_proof_path = "graphviz_tableau_proof.dot"
static

Definition at line 183 of file Parameters.hpp.

◆ graphviz_tableau_subs

bool params::graphviz_tableau_subs = false
static

Definition at line 159 of file Parameters.hpp.

◆ graphviz_width

float params::graphviz_width = 8.27
static

Definition at line 168 of file Parameters.hpp.

◆ indent_size

uint8_t params::indent_size = 4
static

Definition at line 57 of file Parameters.hpp.

◆ latex_body_only

bool params::latex_body_only = false
static

Definition at line 169 of file Parameters.hpp.

◆ latex_height

string params::latex_height = "500mm"
static

Definition at line 165 of file Parameters.hpp.

◆ latex_include_matrix

bool params::latex_include_matrix = true
static

Definition at line 164 of file Parameters.hpp.

◆ LaTeX_proof_path

std::filesystem::path params::LaTeX_proof_path = "latex_proof.tex"
static

Definition at line 181 of file Parameters.hpp.

◆ LaTeX_tableau_proof_path

std::filesystem::path params::LaTeX_tableau_proof_path = "latex_tableau_proof.tex"
static

Definition at line 182 of file Parameters.hpp.

◆ latex_tableau_subs

bool params::latex_tableau_subs = false
static

Definition at line 158 of file Parameters.hpp.

◆ latex_tiny_proof

bool params::latex_tiny_proof = false
static

Definition at line 163 of file Parameters.hpp.

◆ latex_truncation_length

int params::latex_truncation_length = 25
static

Definition at line 162 of file Parameters.hpp.

◆ latex_width

string params::latex_width = "500mm"
static

Definition at line 166 of file Parameters.hpp.

◆ limit_bt_all

bool params::limit_bt_all = true
static

Definition at line 129 of file Parameters.hpp.

◆ limit_bt_extensions

bool params::limit_bt_extensions = true
static

Definition at line 132 of file Parameters.hpp.

◆ limit_bt_extensions_left_tree

bool params::limit_bt_extensions_left_tree = true
static

Definition at line 133 of file Parameters.hpp.

◆ limit_bt_lemmas

bool params::limit_bt_lemmas = true
static

Definition at line 130 of file Parameters.hpp.

◆ limit_bt_reductions

bool params::limit_bt_reductions = true
static

Definition at line 131 of file Parameters.hpp.

◆ limit_extensions

bool params::limit_extensions = true
static

Definition at line 128 of file Parameters.hpp.

◆ limit_lemmata

bool params::limit_lemmata = true
static

Definition at line 126 of file Parameters.hpp.

◆ limit_reductions

bool params::limit_reductions = true
static

Definition at line 127 of file Parameters.hpp.

◆ miniscope

bool params::miniscope = true
static

Definition at line 72 of file Parameters.hpp.

◆ no_definitional

bool params::no_definitional = false
static

Definition at line 74 of file Parameters.hpp.

◆ no_distinct_objects

bool params::no_distinct_objects = false
static

Definition at line 81 of file Parameters.hpp.

◆ number_of_reorders

uint32_t params::number_of_reorders = 0
static

Definition at line 88 of file Parameters.hpp.

◆ output_frequency

uint32_t params::output_frequency = 500000
static

Definition at line 59 of file Parameters.hpp.

◆ output_summary_path

std::filesystem::path params::output_summary_path = "output_summary.txt"
static

Definition at line 186 of file Parameters.hpp.

◆ output_terms_with_substitution

bool params::output_terms_with_substitution = false
static

Definition at line 60 of file Parameters.hpp.

◆ output_width

uint8_t params::output_width = 7
static

Definition at line 58 of file Parameters.hpp.

◆ poly_unification

bool params::poly_unification = false
static

Definition at line 141 of file Parameters.hpp.

◆ positive_representation

bool params::positive_representation = false
static

Definition at line 104 of file Parameters.hpp.

◆ problem_name

std::string params::problem_name = "Unknown"
static

Definition at line 62 of file Parameters.hpp.

◆ Prolog_matrix_path

std::filesystem::path params::Prolog_matrix_path = "matrix.pl"
static

Definition at line 184 of file Parameters.hpp.

◆ Prolog_proof_path

std::filesystem::path params::Prolog_proof_path = "proof.pl"
static

Definition at line 185 of file Parameters.hpp.

◆ pwd_path

std::filesystem::path params::pwd_path = "."
static

Definition at line 190 of file Parameters.hpp.

◆ random_reorder

bool params::random_reorder = false
static

Definition at line 89 of file Parameters.hpp.

◆ random_reorder_literals

bool params::random_reorder_literals = false
static

Definition at line 90 of file Parameters.hpp.

◆ random_seed

unsigned params::random_seed = 0
static

Definition at line 85 of file Parameters.hpp.

◆ restrict_start

bool params::restrict_start = false
static

Definition at line 117 of file Parameters.hpp.

◆ schedule_path

std::filesystem::path params::schedule_path = "."
static

Definition at line 187 of file Parameters.hpp.

◆ show_clauses

bool params::show_clauses = false
static

Definition at line 201 of file Parameters.hpp.

◆ show_full_stats

bool params::show_full_stats = true
static

Definition at line 67 of file Parameters.hpp.

◆ stack_increment

size_t params::stack_increment = 0
static

Definition at line 148 of file Parameters.hpp.

◆ stack_start_size

size_t params::stack_start_size = 5000
static

Definition at line 147 of file Parameters.hpp.

◆ start_depth

uint32_t params::start_depth = 2
static

Definition at line 108 of file Parameters.hpp.

◆ sub_Graphviz_proof

bool params::sub_Graphviz_proof = false
static

Definition at line 161 of file Parameters.hpp.

◆ sub_LaTeX_proof

bool params::sub_LaTeX_proof = false
static

Definition at line 160 of file Parameters.hpp.

◆ switch_to_complete

uint32_t params::switch_to_complete = UINT32_MAX
static

Definition at line 137 of file Parameters.hpp.

◆ timeout

bool params::timeout = false
static

Definition at line 94 of file Parameters.hpp.

◆ timeout_value

uint32_t params::timeout_value = UINT32_MAX
static

Definition at line 95 of file Parameters.hpp.

◆ tptp_path

std::filesystem::path params::tptp_path = "."
static

Definition at line 188 of file Parameters.hpp.

◆ tptp_proof_no_subs

bool params::tptp_proof_no_subs = false
static

Definition at line 173 of file Parameters.hpp.

◆ tptp_proof_path

std::filesystem::path params::tptp_proof_path = "."
static

Definition at line 189 of file Parameters.hpp.

◆ tptp_proof_show_paths

bool params::tptp_proof_show_paths = false
static

Definition at line 174 of file Parameters.hpp.

◆ tptp_proof_show_subs

bool params::tptp_proof_show_subs = false
static

Definition at line 175 of file Parameters.hpp.

◆ tptp_proof_to_file

bool params::tptp_proof_to_file = false
static

Definition at line 172 of file Parameters.hpp.

◆ unique_skolem_prefix

std::string params::unique_skolem_prefix = "sK"
static

Definition at line 66 of file Parameters.hpp.

◆ unique_var_prefix

std::string params::unique_var_prefix = "U_"
static

Definition at line 65 of file Parameters.hpp.

◆ use_colours

bool params::use_colours = true
static

Definition at line 56 of file Parameters.hpp.

◆ use_lemmata

bool params::use_lemmata = true
static

Definition at line 125 of file Parameters.hpp.

◆ use_regularity_test

bool params::use_regularity_test = true
static

Definition at line 121 of file Parameters.hpp.

◆ use_schedule

bool params::use_schedule = false
static

Definition at line 100 of file Parameters.hpp.

◆ verbosity

uint8_t params::verbosity = 2
static

Definition at line 55 of file Parameters.hpp.

◆ verify_proof

bool params::verify_proof = false
static

Definition at line 153 of file Parameters.hpp.

◆ verify_proof_verbose

bool params::verify_proof_verbose = false
static

Definition at line 152 of file Parameters.hpp.

◆ write_output_summary

bool params::write_output_summary = false
static

Definition at line 63 of file Parameters.hpp.

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