Connect++ 0.6.0
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
Parameters.cpp
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#include "Parameters.hpp"
26
27//------------------------------------------------------------------
28// Cosmetic output options.
29//------------------------------------------------------------------
30uint8_t params::verbosity = 2;
31bool params::use_colours = true;
32uint8_t params::indent_size = 4;
33uint8_t params::output_width = 7;
34uint32_t params::output_frequency = 500000;
35bool params::output_terms_with_substitution = false;
36std::string params::problem_name = "Unknown";
37bool params::write_output_summary = false;
38std::string params::definitional_predicate_prefix = "def";
39std::string params::unique_var_prefix = "_u";
40std::string params::unique_skolem_prefix = "skolem";
41bool params::show_full_stats = true;
42bool params::first_parse = true;
43//------------------------------------------------------------------
44// CNF conversion.
45//------------------------------------------------------------------
46bool params::miniscope = true;
47bool params::all_definitional = false;
48bool params::no_definitional = false;
49//------------------------------------------------------------------
50// Equality axioms.
51 //------------------------------------------------------------------
52bool params::add_equality_axioms = true;
53bool params::equality_axioms_at_start = true;
54bool params::all_distinct_objects = false;
55bool params::no_distinct_objects = false;
56//------------------------------------------------------------------
57// Reordering
58//------------------------------------------------------------------
59unsigned params::random_seed = 0;
60uint32_t params::boost_random_seed = 0;
61bool params::deterministic_reorder = false;
62uint32_t params::number_of_reorders = 0;
63bool params::random_reorder = false;
64bool params::random_reorder_literals = false;
65//------------------------------------------------------------------
66// Timeout.
67//------------------------------------------------------------------
68bool params::timeout = false;
69uint32_t params::timeout_value = UINT32_MAX;
70//------------------------------------------------------------------
71// Use of schedule.
72//------------------------------------------------------------------
73bool params::use_schedule = false;
74//------------------------------------------------------------------
75// Positive/negative representation.
76//------------------------------------------------------------------
77bool params::positive_representation = false;
78//------------------------------------------------------------------
79// Deepening.
80//------------------------------------------------------------------
81uint32_t params::start_depth = 2;
82uint32_t params::depth_limit = UINT32_MAX;
83uint32_t params::depth_increment = 1;
84bool params::limit_by_tree_depth = false;
85bool params::depth_limit_all = false;
86//------------------------------------------------------------------
87// Start clauses.
88//------------------------------------------------------------------
89bool params::all_start = false;
90bool params::all_pos_neg_start = false;
91bool params::conjecture_start = false;
92bool params::restrict_start = false;
93//------------------------------------------------------------------
94// Use of regularity test.
95//------------------------------------------------------------------
96bool params::use_regularity_test = true;
97//------------------------------------------------------------------
98// Various basic limitations of search.
99//------------------------------------------------------------------
100bool params::use_lemmata = true;
101bool params::limit_lemmata = true;
102bool params::limit_reductions = true;
103bool params::limit_extensions = true;
104bool params::limit_bt_all = true;
105bool params::limit_bt_lemmas = true;
106bool params::limit_bt_reductions = true;
107bool params::limit_bt_extensions = true;
108bool params::limit_bt_extensions_left_tree = true;
109//------------------------------------------------------------------
110// Move to a complete search.
111//------------------------------------------------------------------
112uint32_t params::switch_to_complete = UINT32_MAX;
113//------------------------------------------------------------------
114// Type of unification to use.
115//------------------------------------------------------------------
116bool params::poly_unification = false;
117//------------------------------------------------------------------
118// Generation of proof for output.
119//------------------------------------------------------------------
120bool params::verify_proof_verbose = false;
121bool params::verify_proof = false;
122bool params::build_proof = false;
123bool params::generate_LaTeX_proof = false;
124bool params::sub_LaTeX_proof = false;
125int params::latex_truncation_length = 25;
126bool params::latex_tiny_proof = false;
127bool params::latex_include_matrix = true;
128bool params::generate_Prolog_proof = false;
129bool params::generate_tptp_proof = false;
130//------------------------------------------------------------------
131// Assorted file paths.
132//------------------------------------------------------------------
133std::filesystem::path params::LaTeX_proof_path = "latex_proof.tex";
134std::filesystem::path params::Prolog_matrix_path = "matrix.pl";
135std::filesystem::path params::Prolog_proof_path = "proof.pl";
136std::filesystem::path params::output_summary_path = "output_summary.txt";
137std::filesystem::path params::schedule_path = ".";
138std::filesystem::path params::tptp_path = ".";
139std::filesystem::path params::pwd_path = ".";
140std::filesystem::path params::connectpp_path = ".";
141std::filesystem::path params::full_problem_path;
142//------------------------------------------------------------------
143// Default schedule.
144//------------------------------------------------------------------
145std::string params::default_schedule;
146
147void params::set_default_schedule() {
148 default_schedule = "10 --complete 7 ;\n";
149 default_schedule += "15 --conjecture-start --all-definitional ;\n";
150 default_schedule += "15 --no-definitional --restrict-start ;\n";
151 default_schedule += "10 --restrict-start --all-backtrack ;\n";
152 default_schedule += "5 --all-definitional ;\n";
153 default_schedule += "4 --conjecture-start --no-definitional ;\n";
154 default_schedule += "2 --all-definitional --restrict-start ;\n";
155 default_schedule += "2 --restrict-start ;\n";
156 default_schedule += "1 --conjecture-start --all-definitional --all-backtrack ;\n";
157 default_schedule += "4 --random-reorder --random-reorder-literals --conjecture-start --no-definitional --restrict-start ;\n";
158 default_schedule += "4 --random-reorder --random-reorder-literals --all-definitional --restrict-start ;\n";
159 default_schedule += "2 --random-reorder --random-reorder-literals --all-definitional --restrict-start ;\n";
160 default_schedule += "2 --random-reorder --random-reorder-literals --all-definitional --restrict-start ;\n";
161 default_schedule += "2 --random-reorder --random-reorder-literals --no-definitional ;\n";
162 default_schedule += "2 --random-reorder --random-reorder-literals --conjecture-start --all-definitional ;\n";
163 default_schedule += "2 --random-reorder --random-reorder-literals --conjecture-start --all-definitional ;\n";
164 default_schedule += "1 --random-reorder --random-reorder-literals --conjecture-start --all-definitional ;\n";
165 default_schedule += "1 --random-reorder --random-reorder-literals --conjecture-start --all-definitional ;\n";
166 default_schedule += "1 --random-reorder --random-reorder-literals --conjecture-start --no-definitional --restrict-start ;\n";
167 default_schedule += "1 --random-reorder --random-reorder-literals --conjecture-start --no-definitional --restrict-start ;\n";
168 default_schedule += "1 --random-reorder --random-reorder-literals --conjecture-start --no-definitional --restrict-start ;\n";
169 default_schedule += "1 --random-reorder --random-reorder-literals --conjecture-start --no-definitional --restrict-start --all-backtrack ;\n";
170 default_schedule += "1 --random-reorder --random-reorder-literals --conjecture-start --no-definitional --restrict-start --all-backtrack ;\n";
171 default_schedule += "1 --random-reorder --random-reorder-literals --all-definitional --restrict-start --all-backtrack ;\n";
172 default_schedule += "1 --random-reorder --random-reorder-literals --all-definitional --restrict-start ;\n";
173 default_schedule += "1 --random-reorder --random-reorder-literals --all-definitional --restrict-start ;\n";
174 default_schedule += "1 --random-reorder --random-reorder-literals --no-definitional ;\n";
175 default_schedule += "1 --random-reorder --random-reorder-literals --no-definitional ;\n";
176 default_schedule += "1 --random-reorder --random-reorder-literals --no-definitional --restrict-start --all-backtrack ;\n";
177 default_schedule += "0 --all-definitional --all-backtrack ;\n";
178}
179//------------------------------------------------------------------------
180bool params::show_clauses = false;
181//------------------------------------------------------------------
182void params::set_default_schedule_parameters() {
183 all_definitional = false;
184 no_definitional = false;
185
186 deterministic_reorder = false;
187 number_of_reorders = 0;
188 random_reorder = false;
189 random_reorder_literals = false;
190
191 start_depth = 2;
192 depth_increment = 1;
193 limit_by_tree_depth = false;
194
195 all_start = false;
196 all_pos_neg_start = false;
197 conjecture_start = false;
198 restrict_start = false;
199
200 use_regularity_test = true;
201
202 use_lemmata = true;
203 limit_lemmata = true;
204 limit_reductions = true;
205 limit_extensions = true;
206 limit_bt_all = true;
207 limit_bt_lemmas = true;
208 limit_bt_reductions = true;
209 limit_bt_extensions = true;
210 limit_bt_extensions_left_tree = true;
211
212 switch_to_complete = UINT32_MAX;
213}
214//------------------------------------------------------------------------
215void params::set_complete_parameters() {
216 all_start = false;
217 all_pos_neg_start = true;
218 conjecture_start = false;
219 restrict_start = false;
220
221 limit_bt_all = false;
222 limit_bt_reductions = false;
223 limit_bt_extensions = false;
224 limit_bt_extensions_left_tree = false;
225}
226//------------------------------------------------------------------------
227bool params::search_is_complete() {
228 bool start_conditions_ok =
229 (all_pos_neg_start || all_start) && !restrict_start && !conjecture_start;
230
231 // You don't care about lemmas.
232 bool backtracking_ok =
233 !limit_bt_all && !limit_bt_reductions && !limit_bt_extensions &&
234 !limit_bt_extensions_left_tree;
235
236 return start_conditions_ok && backtracking_ok;
237}
238//------------------------------------------------------------------------
239void params::set_all_backtrack() {
240 limit_bt_all = false;
241 limit_bt_lemmas = false;
242 limit_bt_reductions = false;
243 limit_bt_extensions = false;
244 limit_bt_extensions_left_tree = false;
245}
246//------------------------------------------------------------------------
247bool params::no_start_options() {
248 return !all_start &&
249 !all_pos_neg_start &&
250 !conjecture_start &&
251 !restrict_start;
252}
253//------------------------------------------------------------------------
254void params::correct_missing_start_options() {
255 all_start = false;
256 all_pos_neg_start = true;
257 conjecture_start = false;
258 restrict_start = false;
259}
260//------------------------------------------------------------------------
261void params::set_all_start() {
262 all_start = true;
263 all_pos_neg_start = false;
264 conjecture_start = false;
265 restrict_start = false;
266}
267//------------------------------------------------------------------------
268void params::show_search_parameter_settings() {
269 cout << std::boolalpha
270 << "all_definitional: " << all_definitional << endl
271 << "no_definitional: " << no_definitional << endl
272 << "all_start: " << all_start << endl
273 << "all_pos_neg_start: " << all_pos_neg_start << endl
274 << "conjecture_start: " << conjecture_start << endl
275 << "restrict_start: " << restrict_start << endl
276 << "limit_bt_all: " << limit_bt_all << endl
277 << "switch_to_complete: " << switch_to_complete
278 << std::noboolalpha;
279}
params::set_default_schedule_parameters
static void set_default_schedule_parameters()
Self-explanatory.
Definition Parameters.cpp:182
params::set_all_backtrack
static void set_all_backtrack()
Self-explanatory.
Definition Parameters.cpp:239
params::set_all_start
static void set_all_start()
Self-explanatory.
Definition Parameters.cpp:261
params::set_complete_parameters
static void set_complete_parameters()
Change the parameters to make the search complete.
Definition Parameters.cpp:215
params::no_start_options
static bool no_start_options()
Self-explanatory.
Definition Parameters.cpp:247
params::correct_missing_start_options
static void correct_missing_start_options()
Self-explanatory.
Definition Parameters.cpp:254
params::search_is_complete
static bool search_is_complete()
Self-explanatory.
Definition Parameters.cpp:227
params::show_search_parameter_settings
static void show_search_parameter_settings()
Give a detailed indication of what the parameters affecting the search are currently set to.
Definition Parameters.cpp:268