Connect++ 0.4.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 <cstdint>
29#include <filesystem>
30
45struct params {
46 //------------------------------------------------------------------
47 // Cosmetic output options.
48 //------------------------------------------------------------------
49 static uint8_t verbosity;
50 static bool use_colours;
51 static uint8_t indent_size;
52 static uint8_t output_width;
53 static uint32_t output_frequency;
54 static bool output_terms_with_substitution; // Only applies to the use of
55 // operator<<
56 static std::string problem_name;
57 static bool write_output_summary;
58 static std::string definitional_predicate_prefix;
59 static std::string unique_var_prefix;
60 static std::string unique_skolem_prefix;
61 static bool first_parse;
62 //------------------------------------------------------------------
63 // CNF conversion.
64 //------------------------------------------------------------------
65 static bool miniscope;
66 static bool all_definitional;
67 static bool no_definitional;
68 //------------------------------------------------------------------
69 // Equality axioms.
70 //------------------------------------------------------------------
71 static bool add_equality_axioms;
72 static bool equality_axioms_at_start;
73 static bool all_distinct_objects;
74 static bool no_distinct_objects;
75 //------------------------------------------------------------------
76 // Reordering
77 //------------------------------------------------------------------
78 static unsigned random_seed;
79 static uint32_t boost_random_seed;
80 static bool deterministic_reorder;
81 static uint32_t number_of_reorders;
82 static bool random_reorder;
83 static bool random_reorder_literals;
84 //------------------------------------------------------------------
85 // Timeout.
86 //------------------------------------------------------------------
87 static bool timeout;
88 static uint32_t timeout_value;
89 //------------------------------------------------------------------
90 // Use of schedule.
91 //------------------------------------------------------------------
92 static bool use_schedule;
93 //------------------------------------------------------------------
94 // Positive/negative representation.
95 //------------------------------------------------------------------
96 static bool positive_representation;
97 //------------------------------------------------------------------
98 // Deepening.
99 //------------------------------------------------------------------
100 static uint32_t start_depth;
101 static uint32_t depth_limit;
102 static uint32_t depth_increment;
103 static bool limit_by_tree_depth;
104 static bool depth_limit_all;
105 //------------------------------------------------------------------
106 // Start clauses.
107 //------------------------------------------------------------------
108 static bool all_start;
109 static bool all_pos_neg_start;
110 static bool conjecture_start;
111 static bool restrict_start;
112 //------------------------------------------------------------------
113 // Use of regularity test.
114 //------------------------------------------------------------------
115 static bool use_regularity_test;
116 //------------------------------------------------------------------
117 // Various basic limitations of search.
118 //------------------------------------------------------------------
119 static bool use_lemmata;
120 static bool limit_lemmata;
121 static bool limit_reductions;
122 static bool limit_extensions;
123 static bool limit_bt_all;
124 static bool limit_bt_lemmas;
125 static bool limit_bt_reductions;
126 static bool limit_bt_extensions;
127 static bool limit_bt_extensions_left_tree;
128 //------------------------------------------------------------------
129 // Move to a complete search.
130 //------------------------------------------------------------------
131 static uint32_t switch_to_complete;
132 //------------------------------------------------------------------
133 // Generation of proof for output.
134 //------------------------------------------------------------------
135 static bool verify_proof_verbose;
136 static bool verify_proof;
137 static bool build_proof;
138 static bool generate_LaTeX_proof;
139 static bool sub_LaTeX_proof;
140 static int latex_truncation_length;
141 static bool latex_tiny_proof;
142 static bool latex_include_matrix;
143 static bool generate_Prolog_proof;
144 static bool generate_tptp_proof;
145 //------------------------------------------------------------------
146 // Assorted file paths.
147 //------------------------------------------------------------------
148 static std::filesystem::path LaTeX_proof_path;
149 static std::filesystem::path Prolog_matrix_path;
150 static std::filesystem::path Prolog_proof_path;
151 static std::filesystem::path output_summary_path;
152 static std::filesystem::path schedule_path;
153 static std::filesystem::path tptp_path;
154 static std::filesystem::path pwd_path;
155 static std::filesystem::path connectpp_path;
156 static std::filesystem::path full_problem_path;
157 //------------------------------------------------------------------
158 // Default schedule.
159 //------------------------------------------------------------------
160 static std::string default_schedule;
161 static void set_default_schedule();
162 //------------------------------------------------------------------
163 // Other output options.
164 //------------------------------------------------------------------
165 static bool show_clauses;
173 static void set_default_schedule_parameters();
177 static void set_complete_parameters();
181 static bool search_is_complete();
185 static void set_all_backtrack();
189 static bool no_start_options();
193 static void correct_missing_start_options();
197 static void set_all_start();
198};
199
200#endif
params
Structure containing all the command line and other options.
Definition Parameters.hpp:45
params::set_default_schedule_parameters
static void set_default_schedule_parameters()
Self-explanatory.
Definition Parameters.cpp:177
params::set_all_backtrack
static void set_all_backtrack()
Self-explanatory.
Definition Parameters.cpp:234
params::set_all_start
static void set_all_start()
Self-explanatory.
Definition Parameters.cpp:256
params::set_complete_parameters
static void set_complete_parameters()
Change the parameters to make the search complete.
Definition Parameters.cpp:210
params::no_start_options
static bool no_start_options()
Self-explanatory.
Definition Parameters.cpp:242
params::correct_missing_start_options
static void correct_missing_start_options()
Self-explanatory.
Definition Parameters.cpp:249
params::search_is_complete
static bool search_is_complete()
Self-explanatory.
Definition Parameters.cpp:222