Connect++ 0.6.0
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
Parameters.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 PARAMETERS_HPP
26#define PARAMETERS_HPP
27
28#include<iostream>
29#include <cstdint>
30#include <filesystem>
31
32using std::cout;
33using std::endl;
34
49struct params {
50 //------------------------------------------------------------------
51 // Cosmetic output options.
52 //------------------------------------------------------------------
53 static uint8_t verbosity;
54 static bool use_colours;
55 static uint8_t indent_size;
56 static uint8_t output_width;
57 static uint32_t output_frequency;
58 static bool output_terms_with_substitution; // Only applies to the use of
59 // operator<<
60 static std::string problem_name;
61 static bool write_output_summary;
62 static std::string definitional_predicate_prefix;
63 static std::string unique_var_prefix;
64 static std::string unique_skolem_prefix;
65 static bool show_full_stats;
66 static bool first_parse;
67 //------------------------------------------------------------------
68 // CNF conversion.
69 //------------------------------------------------------------------
70 static bool miniscope;
71 static bool all_definitional;
72 static bool no_definitional;
73 //------------------------------------------------------------------
74 // Equality axioms.
75 //------------------------------------------------------------------
76 static bool add_equality_axioms;
77 static bool equality_axioms_at_start;
78 static bool all_distinct_objects;
79 static bool no_distinct_objects;
80 //------------------------------------------------------------------
81 // Reordering
82 //------------------------------------------------------------------
83 static unsigned random_seed;
84 static uint32_t boost_random_seed;
85 static bool deterministic_reorder;
86 static uint32_t number_of_reorders;
87 static bool random_reorder;
88 static bool random_reorder_literals;
89 //------------------------------------------------------------------
90 // Timeout.
91 //------------------------------------------------------------------
92 static bool timeout;
93 static uint32_t timeout_value;
94 //------------------------------------------------------------------
95 // Use of schedule.
96 //------------------------------------------------------------------
97 static bool use_schedule;
98 //------------------------------------------------------------------
99 // Positive/negative representation.
100 //------------------------------------------------------------------
101 static bool positive_representation;
102 //------------------------------------------------------------------
103 // Deepening.
104 //------------------------------------------------------------------
105 static uint32_t start_depth;
106 static uint32_t depth_limit;
107 static uint32_t depth_increment;
108 static bool limit_by_tree_depth;
109 static bool depth_limit_all;
110 //------------------------------------------------------------------
111 // Start clauses.
112 //------------------------------------------------------------------
113 static bool all_start;
114 static bool all_pos_neg_start;
115 static bool conjecture_start;
116 static bool restrict_start;
117 //------------------------------------------------------------------
118 // Use of regularity test.
119 //------------------------------------------------------------------
120 static bool use_regularity_test;
121 //------------------------------------------------------------------
122 // Various basic limitations of search.
123 //------------------------------------------------------------------
124 static bool use_lemmata;
125 static bool limit_lemmata;
126 static bool limit_reductions;
127 static bool limit_extensions;
128 static bool limit_bt_all;
129 static bool limit_bt_lemmas;
130 static bool limit_bt_reductions;
131 static bool limit_bt_extensions;
132 static bool limit_bt_extensions_left_tree;
133 //------------------------------------------------------------------
134 // Move to a complete search.
135 //------------------------------------------------------------------
136 static uint32_t switch_to_complete;
137 //------------------------------------------------------------------
138 // Type of unification to use.
139 //------------------------------------------------------------------
140 static bool poly_unification;
141 //------------------------------------------------------------------
142 // Generation of proof for output.
143 //------------------------------------------------------------------
144 static bool verify_proof_verbose;
145 static bool verify_proof;
146 static bool build_proof;
147 static bool generate_LaTeX_proof;
148 static bool sub_LaTeX_proof;
149 static int latex_truncation_length;
150 static bool latex_tiny_proof;
151 static bool latex_include_matrix;
152 static bool generate_Prolog_proof;
153 static bool generate_tptp_proof;
154 //------------------------------------------------------------------
155 // Assorted file paths.
156 //------------------------------------------------------------------
157 static std::filesystem::path LaTeX_proof_path;
158 static std::filesystem::path Prolog_matrix_path;
159 static std::filesystem::path Prolog_proof_path;
160 static std::filesystem::path output_summary_path;
161 static std::filesystem::path schedule_path;
162 static std::filesystem::path tptp_path;
163 static std::filesystem::path pwd_path;
164 static std::filesystem::path connectpp_path;
165 static std::filesystem::path full_problem_path;
166 //------------------------------------------------------------------
167 // Default schedule.
168 //------------------------------------------------------------------
169 static std::string default_schedule;
170 static void set_default_schedule();
171 //------------------------------------------------------------------
172 // Other output options.
173 //------------------------------------------------------------------
174 static bool show_clauses;
182 static void set_default_schedule_parameters();
186 static void set_complete_parameters();
190 static bool search_is_complete();
194 static void set_all_backtrack();
198 static bool no_start_options();
202 static void correct_missing_start_options();
206 static void set_all_start();
211 static void show_search_parameter_settings();
212};
213
214#endif
params
Structure containing all the command line and other options.
Definition Parameters.hpp:49
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