33#include <boost/program_options.hpp>
35#include "connect++-version.hpp"
37#include "StackProver.hpp"
38#include "Schedule.hpp"
39#include "ProofChecker.hpp"
45namespace fs = std::filesystem;
46namespace chrono = std::chrono;
47namespace po = boost::program_options;
49using namespace verbose_print;
50using namespace boost::spirit;
55void SIGINT_handler(
int p) {
56 cout << endl <<
"% SZS status Error for "
57 << params::problem_name
58 <<
" : terminated by SIGINT." << endl;
61void SIGXCPU_handler(
int p) {
62 cout << endl <<
"% SZS status Timeout for "
63 << params::problem_name
64 <<
" : terminated by SIGXCPU." << endl;
67void SIGALRM_handler(
int p) {
68 cout << endl <<
"% SZS status Timeout for "
69 << params::problem_name
70 <<
" : terminated by SIGALRM." << endl;
74int main(
int argc,
char** argv) {
78 chrono::steady_clock::time_point startTime;
79 startTime = chrono::steady_clock::now();
83 std::signal(SIGINT, SIGINT_handler);
84 std::signal(SIGXCPU, SIGXCPU_handler);
85 std::signal(SIGALRM, SIGALRM_handler);
91 char* tptp_env = getenv(
"TPTP");
92 if (tptp_env !=
nullptr) {
93 params::tptp_path = fs::path(tptp_env);
95 char* pwd_env = getenv(
"PWD");
96 if (pwd_env !=
nullptr) {
97 params::pwd_path = fs::path(pwd_env);
99 char* path_env = getenv(
"CONNECTPP_PATH");
100 if (path_env !=
nullptr) {
101 params::connectpp_path = fs::path(path_env);
104 params::connectpp_path = params::pwd_path;
110 po::options_description main_options(
"Basic options");
111 main_options.add_options()
113 "Show this message.")
115 "Show version number.")
116 (
"input,i", po::value<string>(),
118 (
"output,o", po::value<string>(),
119 "Write a short output summary (file, status, outcome, time etc) to the specified file. Using \"default\" places it in \"./output_summary.txt\"" )
121 "Don't add equality axioms. (For example, if they were added elsewhere.) NOTE: also inhibits adding of distinct object axioms.")
123 "Place equality axioms at the end of the matrix, not the beginning")
124 (
"all-distinct-objects",
125 "By default Connect++ follows the TPTP convention of considering \"foobar\" to be a distinct object. This option makes *all* constants distinct.")
126 (
"no-distinct-objects",
127 "By default Connect++ follows the TPTP convention of considering \"foobar\" to be a distinct object. This option disables that behaviour, so constants can be equal to others.")
128 (
"timeout,t", po::value<int>(),
129 "Timeout in seconds. (Default UINT32_MAX).")
130 (
"show-default-schedule",
131 "Display the build-in default schedule and halt.")
132 (
"schedule,s",po::value<string>(),
133 "Instead of running with fixed parameters, use a schedule from the specified file. Use value \"default\" for the default schedule. If no --timeout is specified use 600s.")
134 (
"tptp", po::value<string>(),
135 "Specify a path for the TPTP. Alternative to using the TPTP environment variable.")
136 (
"path", po::value<string>(),
137 "Specify the path for output files other than the one produced by --output. Alternative to using the CONNECTPP_PATH environment variable.");
139 po::options_description conversion_options(
"Clause conversion");
140 conversion_options.add_options()
142 "Don't apply definitional transformation for any formula.")
144 "Apply definitional transformation to all formulas.")
145 (
"reorder,r", po::value<int>(),
146 "Reorder the clauses a specified number of times.")
148 "Randomly reorder the clauses.")
150 "Don't miniscope when converting to CNF.")
152 "Show translation of first-order formulas to clauses and halt.");
154 po::options_description output_options(
"Output formatting");
155 output_options.add_options()
156 (
"verbosity,v", po::value<int>(),
157 "Set verbosity level (0-3). Default is 2.")
159 "Don't use colour to highlight output.")
161 "Include substitutions when writing output.")
162 (
"indent", po::value<int>(),
163 "Set indentation size. (Default 4.)")
164 (
"out-int", po::value<int>(),
165 "Interval for updating output (default 50,000).");
167 po::options_description search_options(
"Search control");
168 search_options.add_options()
170 "Use all start clauses. (Overides other start clause options.)")
172 "Use all positive/negative start clauses, according to representation (currently always negative). (Interacts with other start clause options.)")
174 "Use all conjecture clauses as start clauses. (Interacts with other start clause options.)")
176 "Only use one start clause. (Interacts with other start clause options.)")
178 "Don't use the regularity test.")
180 "Compute reductions for all literals in the clause, not just the first one.")
182 "Compute extensions for all literals in the clause, not just the first one.")
184 "When using lemmata, consider all literals in the clause, not just the first one.")
186 "Do not use lemmata.");
188 po::options_description backtrack_options(
"Backtracking");
189 backtrack_options.add_options()
191 "Do not limit any backtracking.")
192 (
"lemmata-backtrack",
193 "Do not limit backtracking for lemmata.")
194 (
"reduction-backtrack",
195 "Do not limit backtracking for reductions.")
196 (
"extension-backtrack",
197 "Do not limit backtracking for extensions.")
198 (
"explore-left-trees",
199 "Apply backtracking within left extension trees.")
200 (
"complete,c", po::value<int>(),
201 "Start again with a complete search on reaching the specified depth. (Default UINT32_MAX.)");
203 po::options_description depth_options(
"Depth limiting");
204 depth_options.add_options()
205 (
"depth-limit,d", po::value<int>(),
206 "Maximum depth/path length. (Default UINT32_MAX.)")
207 (
"start-depth", po::value<int>(),
208 "Initial depth/path length. (Default 1.)")
209 (
"depth-increment", po::value<int>(),
210 "Increment for iterative deepening. (Default 1.)")
211 (
"limit-by-tree-depth",
212 "Use tree depth (not path length) for deepening.");
214 po::options_description proof_options(
"Proof generation");
215 proof_options.add_options()
217 "Generate a proof compatible with the TPTP. Note that what constitutes a TPTP-compatible proof in connection calculus is currently a moving target, so the format is subject to change. Output is to stdout.")
219 "Generate Prolog format files proof.pl and matrix.pl and store in the $CONNECTPP_PATH directory. You can check these using the check_proof utility.")
221 "Verify any proof found using the internal proof checker. Use this version to get a detailed description of the verification sent to stdout.")
223 "Verify any proof found using the internal proof checker. Use this version for a quiet verification that only adds \"Verified\" or \"FaliedVerification\" to the output string.");
225 po::options_description latex_options(
"LaTeX output");
226 latex_options.add_options()
227 (
"latex", po::value<string>(),
228 "Make a LaTeX file containing a typeset proof. Use \"default\" for \"./latex_proof.tex\" or specify a destination.")
230 "Include substitutions in the LaTeX proof.")
232 "Typeset the latex proof in a tiny font.")
234 "Don't include the matrix in the LaTeX proof.");
236 po::options_description all_options(
"Options");
237 all_options.add(main_options)
238 .add(conversion_options)
241 .add(backtrack_options)
246 po::positional_options_description pos_opts;
247 pos_opts.add(
"input", -1);
248 po::variables_map vars_map;
250 po::store(po::command_line_parser(argc, argv).
251 options(all_options).
252 positional(pos_opts).
258 catch (boost::program_options::error& err) {
259 cout <<
"% SZS status Error for "
260 << params::problem_name <<
" : " << err.what() << endl;
263 po::notify(vars_map);
268 if (vars_map.count(
"help")) {
269 cout << all_options << endl;
272 if (vars_map.count(
"version")) {
273 cout <<
"Connect++ Version V" << VERSION <<
"." << endl;
274 cout <<
"Copyright (C) 2021-24 Sean Holden. All rights reserved." << endl;
277 if (vars_map.count(
"verbosity")) {
278 int v = vars_map[
"verbosity"].as<
int>();
279 if (v >= 0 && v <= 3)
280 params::verbosity = v;
282 cerr <<
"Verbosity should be between 0 and 5. Using default." << endl;
284 VPrint show(params::verbosity);
285 if (vars_map.count(
"sub-output")) {
286 params::output_terms_with_substitution =
true;
288 if (vars_map.count(
"indent")) {
289 int i = vars_map[
"indent"].as<
int>();
290 if (i >= 0 && i <= UINT8_MAX)
291 params::indent_size = i;
293 cerr <<
"Indent size is negative or too large. Using default." << endl;
295 if (vars_map.count(
"out-int")) {
296 int i = vars_map[
"out-int"].as<
int>();
297 if (i > 0 && i <= UINT32_MAX)
298 params::output_frequency = i;
300 cerr <<
"Interval is negative or too large. Using default." << endl;
302 if (vars_map.count(
"no-equality")) {
303 params::add_equality_axioms =
false;
305 if (vars_map.count(
"equality-last")) {
306 params::equality_axioms_at_start =
false;
308 if (vars_map.count(
"all-distinct-objects")) {
309 params::all_distinct_objects =
true;
311 if (vars_map.count(
"no-distinct-objects")) {
312 if (params::all_distinct_objects) {
313 cerr <<
"Cancelled --all-distinct-objects." << endl;
314 params::all_distinct_objects =
false;
316 params::no_distinct_objects =
true;
318 if (vars_map.count(
"timeout")) {
319 params::timeout =
true;
320 int t = vars_map[
"timeout"].as<
int>();
323 params::timeout_value = t;
325 cerr <<
"Timeout is too small. Using 10 seconds." << endl;
326 params::timeout_value = 10;
330 cerr <<
"Timeout should be positive. Using default." << endl;
332 if (vars_map.count(
"show-default-schedule")) {
333 params::set_default_schedule();
334 cout << params::default_schedule << endl;
337 if (vars_map.count(
"path")) {
338 params::connectpp_path = vars_map[
"path"].as<
string>();
342 params::LaTeX_proof_path
343 = params::pwd_path / params::LaTeX_proof_path;
344 params::Prolog_matrix_path
345 = params::connectpp_path / params::Prolog_matrix_path;
346 params::Prolog_proof_path
347 = params::connectpp_path / params::Prolog_proof_path;
348 params::output_summary_path
349 = params::pwd_path / params::output_summary_path;
351 if (vars_map.count(
"output")) {
352 params::write_output_summary =
true;
353 string op = vars_map[
"output"].as<
string>();
355 params::output_summary_path = op;
357 if (vars_map.count(
"all-definitional")) {
358 params::all_definitional =
true;
360 if (vars_map.count(
"no-definitional")) {
361 params::no_definitional =
true;
362 if (params::all_definitional) {
363 cerr <<
"Setting --no-definitional has cancelled --all-definitional." << endl;
364 params::all_definitional =
false;
368 if (vars_map.count(
"schedule")) {
369 params::use_schedule =
true;
370 if (!params::timeout) {
371 params::timeout =
true;
372 params::timeout_value = 600;
374 params::schedule_path = vars_map[
"schedule"].as<
string>();
376 schedule.read_schedule_from_file(params::schedule_path);
378 catch (std::exception& err) {
379 cout <<
"% SZS status Error for "
380 << params::problem_name <<
" : " << err.what() << endl;
388 if (vars_map.count(
"tptp")) {
389 params::tptp_path = vars_map[
"tptp"].as<
string>();
391 if (vars_map.count(
"reorder")) {
392 int n = vars_map[
"reorder"].as<
int>();
394 params::deterministic_reorder =
true;
395 params::number_of_reorders = n;
398 cerr <<
"Number of re-orders should be positive. Skipping." << endl;
400 if (vars_map.count(
"random-reorder")) {
401 params::random_reorder =
true;
403 if (vars_map.count(
"no-miniscope")) {
404 params::miniscope =
false;
406 if (vars_map.count(
"show-clauses")) {
407 params::show_clauses =
true;
409 if (vars_map.count(
"no-colour")) {
410 params::use_colours =
false;
430 fs::path initial_path;
431 bool found_file =
false;
432 if (vars_map.count(
"input")) {
434 initial_path = vars_map[
"input"].as<
string>();
437 if (initial_path.is_relative()) {
439 if (fs::exists(initial_path)) {
443 initial_path = fs::canonical(initial_path);
445 catch (std::filesystem::filesystem_error& err) {
446 cout <<
"% SZS status Error for "
447 << params::problem_name <<
" : "
448 << err.what() << endl;
456 fs::path tptp_path(params::tptp_path);
457 initial_path = tptp_path / initial_path;
459 if (fs::exists(initial_path)) {
462 initial_path = fs::canonical(initial_path);
464 catch (std::filesystem::filesystem_error& err) {
465 cout <<
"% SZS status Error for "
466 << params::problem_name <<
" : "
467 << err.what() << endl;
476 if (initial_path.is_absolute() && fs::exists(initial_path)) {
479 initial_path = fs::canonical(initial_path);
481 catch (std::filesystem::filesystem_error& err) {
482 cout <<
"% SZS status Error for "
483 << params::problem_name <<
" : "
484 << err.what() << endl;
492 cout <<
"% SZS status Error for "
493 << params::problem_name <<
" : no problem specified." << endl;
498 cout <<
"% SZS status Error for "
499 << params::problem_name <<
" : the specified file does not exist." << endl;
503 params::full_problem_path = initial_path;
504 params::full_problem_path.remove_filename();
505 params::problem_name = initial_path.stem().string();
506 fs::path path = initial_path;
512 if (vars_map.count(
"depth-limit")) {
513 int l = vars_map[
"depth-limit"].as<
int>();
515 params::depth_limit = l;
517 cerr <<
"Depth limit should be positive. Using default." << endl;
519 if (vars_map.count(
"start-depth")) {
520 int l = vars_map[
"start-depth"].as<
int>();
521 if (l > 1 && l <= params::depth_limit)
522 params::start_depth = l;
524 cerr <<
"Start depth should be positive and bounded by the maximum depth. Using default." << endl;
526 if (vars_map.count(
"depth-increment")) {
527 int l = vars_map[
"depth-increment"].as<
int>();
529 params::depth_increment = l;
531 cerr <<
"Depth increment should be positive. Using default." << endl;
533 if (vars_map.count(
"limit-by-tree-depth")) {
534 params::limit_by_tree_depth =
true;
548 if (vars_map.count(
"restrict-start")) {
549 params::restrict_start =
true;
551 if (vars_map.count(
"pos-neg-start")) {
552 params::all_pos_neg_start =
true;
554 if (vars_map.count(
"conjecture-start")) {
555 params::conjecture_start =
true;
557 if (vars_map.count(
"all-start")) {
558 show(2,
string(
"--all-start set. This cancels all other start options."),
true);
568 if (vars_map.count(
"no-regularity")) {
569 params::use_regularity_test =
false;
571 if (vars_map.count(
"lemmata-backtrack")) {
572 params::limit_bt_lemmas =
false;
574 if (vars_map.count(
"reduction-backtrack")) {
575 params::limit_bt_reductions =
false;
577 if (vars_map.count(
"extension-backtrack")) {
578 params::limit_bt_extensions =
false;
580 if (vars_map.count(
"explore-left-trees")) {
581 params::limit_bt_extensions_left_tree =
false;
583 if (vars_map.count(
"all-backtrack")) {
584 show(2,
string(
"--all-backtrack set. This prevails over all other backtracking options."),
true);
587 if (vars_map.count(
"all-reductions")) {
588 params::limit_reductions =
false;
590 if (vars_map.count(
"all-extensions")) {
591 params::limit_extensions =
false;
593 if (vars_map.count(
"all-lemmata")) {
594 params::limit_lemmata =
false;
596 if (vars_map.count(
"no-lemmata")) {
597 params::use_lemmata =
false;
599 if (vars_map.count(
"complete")) {
600 int d = vars_map[
"complete"].as<
int>();
601 if (d >= params::start_depth)
602 params::switch_to_complete = d;
604 cerr <<
"Switch to complete search must happen after start depth. Using start depth." << endl;
605 params::switch_to_complete = params::start_depth;
608 if (vars_map.count(
"latex")) {
609 params::generate_LaTeX_proof =
true;
610 params::build_proof =
true;
611 string lp = vars_map[
"latex"].as<
string>();
613 params::LaTeX_proof_path = lp;
615 if (vars_map.count(
"sub-latex")) {
616 params::sub_LaTeX_proof =
true;
618 if (vars_map.count(
"tiny-latex")) {
619 params::latex_tiny_proof =
true;
621 if (vars_map.count(
"latex-no-matrix")) {
622 params::latex_include_matrix =
false;
624 if (vars_map.count(
"tptp-proof")) {
625 params::generate_tptp_proof =
true;
626 params::build_proof =
true;
628 if (vars_map.count(
"prolog-proof")) {
629 params::generate_Prolog_proof =
true;
630 params::build_proof =
true;
632 if (vars_map.count(
"verify")) {
633 params::verify_proof =
true;
634 params::build_proof =
true;
636 if (vars_map.count(
"full-verify")) {
637 params::verify_proof =
true;
638 params::verify_proof_verbose =
true;
639 params::build_proof =
true;
653 show(1,
string(
"Connect++ V"));
654 show(1,
string(VERSION));
655 show(1,
string(
" started at: "));
656 time_t date_and_time;
657 time(&date_and_time);
658 show(1, asctime(localtime(&date_and_time)));
666 show(1,
string(
"Reading from: "));
667 show(1, path.c_str(),
true);
668 bool found_conjecture =
false;
673 catch (std::exception& err) {
674 cout <<
"% SZS status Error for "
675 << params::problem_name <<
" : "
676 << err.what() << endl;
680 chrono::milliseconds parse_time =
681 chrono::duration_cast<chrono::milliseconds>(chrono::steady_clock::now() - startTime);
682 show(1,
string(
"Total parse and conversion time: "));
683 show(1, std::to_string(parse_time.count()));
684 show(1,
string(
" milliseconds."),
true);
687 show(2,
string(
"Starting proof attempt for: "),
false);
688 show(2, params::problem_name,
true);
692 if (params::verbosity >= 2) {
695 ProverOutcome prover_outcome;
696 ProverOutcome final_outcome;
697 final_outcome = ProverOutcome::TimeOut;
707 if (!params::use_schedule) {
714 if (params::deterministic_reorder) {
717 if (params::random_reorder) {
723 if (params::timeout) {
724 chrono::seconds timeout_duration(params::timeout_value);
730 prover_outcome = prover.
prove();
731 final_outcome = prover_outcome;
746 if (!params::timeout) {
747 params::timeout =
true;
748 params::timeout_value = 600;
753 chrono::milliseconds time_chunk((params::timeout_value * 1000) / 100);
754 chrono::steady_clock::time_point start_time = startTime;
755 chrono::milliseconds chunk_time;
760 size_t schedule_step_number = 1;
761 pair<bool, unsigned int> next_schedule =
763 if (params::verbosity > 0)
768 while (next_schedule.first) {
769 show(1,
string(
"Schedule step "));
770 show(1, std::to_string(schedule_step_number));
771 show(1,
string(
": "));
772 show(1,
schedule.step_to_string(schedule_step_number - 1),
true);
774 if (next_schedule.second == 0) {
775 prover.
set_timeout(startTime + chrono::seconds(params::timeout_value));
777 else if (schedule_step_number == 1) {
778 prover.
set_timeout(startTime + (next_schedule.second * time_chunk));
781 prover.
set_timeout(start_time + (next_schedule.second * time_chunk));
784 prover_outcome = prover.
prove();
786 if (prover_outcome == ProverOutcome::Valid ||
787 prover_outcome == ProverOutcome::Error ||
788 prover_outcome == ProverOutcome::False) {
789 final_outcome = prover_outcome;
793 chunk_time = chrono::duration_cast<chrono::milliseconds>(chrono::steady_clock::now() - start_time);
796 show(1,
string(
"Timeout after "));
797 show(1, std::to_string(chunk_time.count()));
798 show(1,
string(
" milliseconds"),
true);
800 start_time = chrono::steady_clock::now();
801 schedule_step_number++;
802 next_schedule =
schedule.set_next_schedule();
812 prover.show_statistics();
816 chrono::milliseconds runTime =
817 chrono::duration_cast<chrono::milliseconds>(chrono::steady_clock::now() - startTime);
818 show(1,
string(
"Total run time: "));
819 show(1, std::to_string(runTime.count()));
820 show(1,
string(
" milliseconds."),
true);
844 cout <<
"% SZS status ";
845 switch (final_outcome) {
846 case ProverOutcome::Valid:
849 outcome =
"Unsatisfiable";
853 if (simplified_has_axioms) {
856 outcome =
"ContradictoryAxioms";
859 else if (conj_false || neg_conj_removed) {
860 outcome =
"ContradictoryAxioms";
864 else if (conj_missing) {
865 outcome =
"Unsatisfiable";
879 if (neg_conj_removed) {
888 case ProverOutcome::False:
891 outcome =
"Satisfiable";
894 if (simplified_has_axioms) {
898 else if (conj_false || neg_conj_removed) {
899 outcome =
"CounterSatisfiable";
901 else if (conj_missing) {
902 outcome =
"Satisfiable";
905 outcome =
"CounterSatisfiable";
913 else if (neg_conj_removed) {
918 outcome =
"CounterSatisfiable";
922 case ProverOutcome::PathLenLimit:
925 case ProverOutcome::Error:
928 case ProverOutcome::TimeOut:
935 cout << outcome <<
" for " << params::problem_name;
939 bool verified =
false;
940 if (params::verify_proof && final_outcome == ProverOutcome::Valid) {
947 vector<pair<string, vector<size_t>>>
952 get<0>(inds), get<3>(inds));
954 bool verification_outcome;
955 string outcome_string;
956 if (params::verify_proof_verbose) {
957 pair<bool, string> outcome = checker.check_proof_verbose();
958 verification_outcome = outcome.first;
959 outcome_string = outcome.second;
962 verification_outcome = checker.check_proof();
965 if (verification_outcome) {
967 cout <<
" : Verified";
970 cout <<
" : FailedVerification";
973 if (params::verify_proof_verbose) {
974 cout << endl <<
"% SZS output start Proof for " << params::problem_name << endl << endl;
975 cout << outcome_string << endl;
976 cout <<
"% SZS output end Proof for " << params::problem_name << endl;
983 if (params::write_output_summary) {
985 std::ofstream out_file(params::output_summary_path);
986 out_file <<
"ProblemName: " << params::problem_name << endl;
987 if (found_conjecture)
988 out_file <<
"ConjectureFound" << endl;
990 out_file <<
"NoConjectureFound" << endl;
993 out_file <<
"ProblemStatus: " << status << endl;
994 out_file <<
"ProverOutcome: " << outcome << endl;
995 if (params::verify_proof && final_outcome == ProverOutcome::Valid) {
997 out_file <<
"Verified" << endl;
999 out_file <<
"FailedVerification" << endl;
1002 out_file <<
"NoVerify" << endl;
1003 out_file <<
"Time: " << runTime.count() << endl;
1006 catch (std::exception& err) {
1007 cerr <<
"Error: can't write output summary." << endl;
1013 if (params::generate_tptp_proof && (final_outcome == ProverOutcome::Valid)) {
1014 cout <<
"% SZS output start Proof for " << params::problem_name << endl;
1015 cout << params::tptp_conversion_string;
1017 cout <<
"% SZS output end Proof for " << params::problem_name << endl;
1019 return EXIT_SUCCESS;
Mechanism for looking after functions.
Management of Predicate objects.
Prover using a pair of stacks to conduct the proof search.
void read_from_tptp_file(const string &, bool &, size_t &)
Obviously, reads a problem from a TPTP file.
bool problem_has_true_conjecture() const
Find out whether the problem's conjecture is $true.
void random_reorder()
Randomly reorder the matrix.
void show_tptp_proof()
Show a Prolog-formatted proof.
bool problem_is_cnf_only() const
Find out whether the problem is CNF only.
void set_problem_path(fs::path &p)
Set the path for the problem being solved. U.
void deterministic_reorder(uint32_t n)
Deterministically reorder the matrix n times.
void show_matrix()
Show a nicely formatted matrix.
bool problem_has_missing_conjecture() const
Find out whether the problem's conjecture is missing, in the sense that it didn't appear in the inp...
bool problem_has_negated_conjecture_removed() const
Find out whether the problem's negated conjecture was simplified out.
void set_timeout(chrono::steady_clock::time_point time)
Set a timeout.
bool simplified_problem_has_fof_axioms() const
Find out from the parser whether the problem had axioms after simplification.
string get_status() const
Straightforward get method.
bool problem_has_fof_axioms() const
Find out from the parser whether the problem had axioms before simplification.
std::tuple< VariableIndex *, FunctionIndex *, PredicateIndex *, TermIndex * > get_indexes()
Straightforward get method.
vector< pair< string, vector< size_t > > > get_internal_proof() const
Get an internal representation of the proof stack.
Matrix & get_matrix()
Get a reference to the matrix.
bool problem_has_false_conjecture() const
Find out whether the problem's conjecture is $false.
ProverOutcome prove()
Here is where the magic happens.
Look after terms, (ideally) using hash consing to avoid storing copies of terms.
Storage of named variables, and management of new, anonymous variables.
Wrap up the parsing process and the operation of a schedule in a single class.
Hide all the global stuff in this namespace.
static void set_all_backtrack()
Self-explanatory.
static void set_all_start()
Self-explanatory.
static bool no_start_options()
Self-explanatory.
static void correct_missing_start_options()
Self-explanatory.