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;
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;
64 static bool miniscope;
65 static bool all_definitional;
66 static bool no_definitional;
70 static bool add_equality_axioms;
71 static bool equality_axioms_at_start;
72 static bool all_distinct_objects;
73 static bool no_distinct_objects;
77 static unsigned random_seed;
78 static uint32_t boost_random_seed;
79 static bool deterministic_reorder;
80 static uint32_t number_of_reorders;
81 static bool random_reorder;
86 static uint32_t timeout_value;
92 static bool positive_representation;
94 static bool use_schedule;
98 static uint32_t start_depth;
99 static uint32_t depth_limit;
100 static uint32_t depth_increment;
101 static bool limit_by_tree_depth;
105 static bool all_start;
106 static bool all_pos_neg_start;
107 static bool conjecture_start;
108 static bool restrict_start;
112 static bool use_regularity_test;
116 static bool use_lemmata;
117 static bool limit_lemmata;
118 static bool limit_reductions;
119 static bool limit_extensions;
120 static bool limit_bt_all;
121 static bool limit_bt_lemmas;
122 static bool limit_bt_reductions;
123 static bool limit_bt_extensions;
124 static bool limit_bt_extensions_left_tree;
125 static bool hard_prune;
129 static uint32_t switch_to_complete;
133 static bool verify_proof_verbose;
134 static bool verify_proof;
135 static bool build_proof;
136 static bool generate_LaTeX_proof;
137 static bool sub_LaTeX_proof;
138 static int latex_truncation_length;
139 static bool latex_tiny_proof;
140 static bool latex_include_matrix;
141 static bool generate_Prolog_proof;
142 static bool generate_tptp_proof;
143 static std::string tptp_conversion_string;
147 static std::filesystem::path LaTeX_proof_path;
148 static std::filesystem::path Prolog_matrix_path;
149 static std::filesystem::path Prolog_proof_path;
150 static std::filesystem::path output_summary_path;
151 static std::filesystem::path schedule_path;
152 static std::filesystem::path tptp_path;
153 static std::filesystem::path pwd_path;
154 static std::filesystem::path connectpp_path;
155 static std::filesystem::path full_problem_path;
159 static std::string default_schedule;
160 static void set_default_schedule();
164 static bool show_clauses;
Structure containing all the command line and other options.
static void set_default_schedule_parameters()
Self-explanatory.
static void set_all_backtrack()
Self-explanatory.
static void set_all_start()
Self-explanatory.
static void set_complete_parameters()
Change the parameters to make the search complete.
static bool no_start_options()
Self-explanatory.
static void correct_missing_start_options()
Self-explanatory.
static bool search_is_complete()
Self-explanatory.