Connect++ 0.7.0
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
Parameters.hpp
1/*
2
3Copyright © 2023-26 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 PARAMETERS_HPP
26#define PARAMETERS_HPP
27
28#include<iostream>
29#include <cstdint>
30#include <filesystem>
31#include <chrono>
32
33using std::cout;
34using std::endl;
35using std::string;
36
51struct params {
52 //------------------------------------------------------------------
53 // Cosmetic output options.
54 //------------------------------------------------------------------
55 static uint8_t verbosity;
56 static bool use_colours;
57 static uint8_t indent_size;
58 static uint8_t output_width;
59 static uint32_t output_frequency;
60 static bool output_terms_with_substitution; // Only applies to the use of
61 // operator<<
62 static std::string problem_name;
63 static bool write_output_summary;
64 static std::string definitional_predicate_prefix;
65 static std::string unique_var_prefix;
66 static std::string unique_skolem_prefix;
67 static bool show_full_stats;
68 static bool first_parse;
69 //------------------------------------------------------------------
70 // CNF conversion.
71 //------------------------------------------------------------------
72 static bool miniscope;
73 static bool all_definitional;
74 static bool no_definitional;
75 //------------------------------------------------------------------
76 // Equality axioms.
77 //------------------------------------------------------------------
78 static bool add_equality_axioms;
79 static bool equality_axioms_at_start;
80 static bool all_distinct_objects;
81 static bool no_distinct_objects;
82 //------------------------------------------------------------------
83 // Reordering
84 //------------------------------------------------------------------
85 static unsigned random_seed;
86 static uint32_t boost_random_seed;
87 static bool deterministic_reorder;
88 static uint32_t number_of_reorders;
89 static bool random_reorder;
90 static bool random_reorder_literals;
91 //------------------------------------------------------------------
92 // Timeout.
93 //------------------------------------------------------------------
94 static bool timeout;
95 static uint32_t timeout_value;
96 static std::chrono::steady_clock::time_point global_timeout;
97 //------------------------------------------------------------------
98 // Use of schedule.
99 //------------------------------------------------------------------
100 static bool use_schedule;
101 //------------------------------------------------------------------
102 // Positive/negative representation.
103 //------------------------------------------------------------------
104 static bool positive_representation;
105 //------------------------------------------------------------------
106 // Deepening.
107 //------------------------------------------------------------------
108 static uint32_t start_depth;
109 static uint32_t depth_limit;
110 static uint32_t depth_increment;
111 //------------------------------------------------------------------
112 // Start clauses.
113 //------------------------------------------------------------------
114 static bool all_start;
115 static bool all_pos_neg_start;
116 static bool conjecture_start;
117 static bool restrict_start;
118 //------------------------------------------------------------------
119 // Use of regularity test.
120 //------------------------------------------------------------------
121 static bool use_regularity_test;
122 //------------------------------------------------------------------
123 // Various basic limitations of search.
124 //------------------------------------------------------------------
125 static bool use_lemmata;
126 static bool limit_lemmata;
127 static bool limit_reductions;
128 static bool limit_extensions;
129 static bool limit_bt_all;
130 static bool limit_bt_lemmas;
131 static bool limit_bt_reductions;
132 static bool limit_bt_extensions;
133 static bool limit_bt_extensions_left_tree;
134 //------------------------------------------------------------------
135 // Move to a complete search.
136 //------------------------------------------------------------------
137 static uint32_t switch_to_complete;
138 //------------------------------------------------------------------
139 // Type of unification to use.
140 //------------------------------------------------------------------
141 static bool poly_unification;
142 //------------------------------------------------------------------
143 // Start and increment sizes for clause cache and stacks.
144 //------------------------------------------------------------------
145 static size_t clause_copy_cache_start_size;
146 static size_t clause_copy_cache_increment;
147 static size_t stack_start_size;
148 static size_t stack_increment;
149 //------------------------------------------------------------------
150 // Generation of proof for output.
151 //------------------------------------------------------------------
152 static bool verify_proof_verbose;
153 static bool verify_proof;
154 static bool build_proof;
155 static bool generate_LaTeX_proof;
156 static bool generate_LaTeX_tableau_proof;
157 static bool generate_graphviz_tableau_proof;
158 static bool latex_tableau_subs;
159 static bool graphviz_tableau_subs;
160 static bool sub_LaTeX_proof;
161 static bool sub_Graphviz_proof;
162 static int latex_truncation_length;
163 static bool latex_tiny_proof;
164 static bool latex_include_matrix;
165 static string latex_height;
166 static string latex_width;
167 static float graphviz_height;
168 static float graphviz_width;
169 static bool latex_body_only;
170 static bool generate_Prolog_proof;
171 static bool generate_tptp_proof;
172 static bool tptp_proof_to_file;
173 static bool tptp_proof_no_subs;
174 static bool tptp_proof_show_paths;
175 static bool tptp_proof_show_subs;
176 static bool all_tptp_records;
177 static bool generate_sc_tptp_proof;
178 //------------------------------------------------------------------
179 // Assorted file paths.
180 //------------------------------------------------------------------
181 static std::filesystem::path LaTeX_proof_path;
182 static std::filesystem::path LaTeX_tableau_proof_path;
183 static std::filesystem::path graphviz_tableau_proof_path;
184 static std::filesystem::path Prolog_matrix_path;
185 static std::filesystem::path Prolog_proof_path;
186 static std::filesystem::path output_summary_path;
187 static std::filesystem::path schedule_path;
188 static std::filesystem::path tptp_path;
189 static std::filesystem::path tptp_proof_path;
190 static std::filesystem::path pwd_path;
191 static std::filesystem::path connectpp_path;
192 static std::filesystem::path full_problem_path;
193 //------------------------------------------------------------------
194 // Default schedule.
195 //------------------------------------------------------------------
196 static std::string default_schedule;
197 static void set_default_schedule();
198 //------------------------------------------------------------------
199 // Other output options.
200 //------------------------------------------------------------------
201 static bool show_clauses;
209 static void set_default_schedule_parameters();
213 static void set_complete_parameters();
217 static bool search_is_complete();
221 static void set_all_backtrack();
225 static bool no_start_options();
229 static void correct_missing_start_options();
233 static void set_all_start();
238 static void show_search_parameter_settings();
239};
240
241#endif
params
Structure containing all the command line and other options.
Definition Parameters.hpp:51
params::set_default_schedule_parameters
static void set_default_schedule_parameters()
Self-explanatory.
Definition Parameters.cpp:207
params::set_all_backtrack
static void set_all_backtrack()
Self-explanatory.
Definition Parameters.cpp:263
params::set_all_start
static void set_all_start()
Self-explanatory.
Definition Parameters.cpp:285
params::set_complete_parameters
static void set_complete_parameters()
Change the parameters to make the search complete.
Definition Parameters.cpp:239
params::no_start_options
static bool no_start_options()
Self-explanatory.
Definition Parameters.cpp:271
params::correct_missing_start_options
static void correct_missing_start_options()
Self-explanatory.
Definition Parameters.cpp:278
params::search_is_complete
static bool search_is_complete()
Self-explanatory.
Definition Parameters.cpp:251
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:292