Connect++ 0.3.0
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
connect++.cpp
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#include <iostream>
26#include <vector>
27#include <chrono>
28#include <filesystem>
29#include <ctime>
30#include <cstdlib>
31#include <csignal>
32
33#include <boost/program_options.hpp>
34
35#include "connect++-version.hpp"
36
37#include "StackProver.hpp"
38#include "Schedule.hpp"
39#include "ProofChecker.hpp"
40
41using std::cout;
42using std::endl;
43using std::get;
44
45namespace fs = std::filesystem;
46namespace chrono = std::chrono;
47namespace po = boost::program_options;
48
49using namespace verbose_print;
50using namespace boost::spirit;
51
52/*
53* Various signal handlers.
54*/
55void SIGINT_handler(int p) {
56 cout << endl << "% SZS status Error for "
57 << params::problem_name
58 << " : terminated by SIGINT." << endl;
59 exit(EXIT_FAILURE);
60}
61void SIGXCPU_handler(int p) {
62 cout << endl << "% SZS status Timeout for "
63 << params::problem_name
64 << " : terminated by SIGXCPU." << endl;
65 exit(EXIT_FAILURE);
66}
67void SIGALRM_handler(int p) {
68 cout << endl << "% SZS status Timeout for "
69 << params::problem_name
70 << " : terminated by SIGALRM." << endl;
71 exit(EXIT_FAILURE);
72}
73
74int main(int argc, char** argv) {
75 /*
76 * Start the timer...
77 */
78 chrono::steady_clock::time_point startTime;
79 startTime = chrono::steady_clock::now();
80 /*
81 * Set up handlers for signals.
82 */
83 std::signal(SIGINT, SIGINT_handler);
84 std::signal(SIGXCPU, SIGXCPU_handler);
85 std::signal(SIGALRM, SIGALRM_handler);
86 /*
87 * Pick up relevant environment variables for the
88 * TPTP library etc. Some of these may be overidden by a
89 * command line argument later.
90 */
91 char* tptp_env = getenv("TPTP");
92 if (tptp_env != nullptr) {
93 params::tptp_path = fs::path(tptp_env);
94 }
95 char* pwd_env = getenv("PWD");
96 if (pwd_env != nullptr) {
97 params::pwd_path = fs::path(pwd_env);
98 }
99 char* path_env = getenv("CONNECTPP_PATH");
100 if (path_env != nullptr) {
101 params::connectpp_path = fs::path(path_env);
102 }
103 else {
104 params::connectpp_path = params::pwd_path;
105 }
106 /*
107 * Initially, use the Boost Program Options library to decipher
108 * what's been added in the command line and deal with it.
109 */
110 po::options_description main_options("Basic options");
111 main_options.add_options()
112 ("help,h",
113 "Show this message.")
114 ("version",
115 "Show version number.")
116 ("input,i", po::value<string>(),
117 "Input filename.")
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\"" )
120 ("no-equality",
121 "Don't add equality axioms. (For example, if they were added elsewhere.) NOTE: also inhibits adding of distinct object axioms.")
122 ("equality-last",
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.");
138
139 po::options_description conversion_options("Clause conversion");
140 conversion_options.add_options()
141 ("no-definitional",
142 "Don't apply definitional transformation for any formula.")
143 ("all-definitional",
144 "Apply definitional transformation to all formulas.")
145 ("reorder,r", po::value<int>(),
146 "Reorder the clauses a specified number of times.")
147 ("random-reorder",
148 "Randomly reorder the clauses.")
149 ("no-miniscope",
150 "Don't miniscope when converting to CNF.")
151 ("show-clauses",
152 "Show translation of first-order formulas to clauses and halt.");
153
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.")
158 ("no-colour",
159 "Don't use colour to highlight output.")
160 ("sub-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).");
166
167 po::options_description search_options("Search control");
168 search_options.add_options()
169 ("all-start",
170 "Use all start clauses. (Overides other start clause options.)")
171 ("pos-neg-start",
172 "Use all positive/negative start clauses, according to representation (currently always negative). (Interacts with other start clause options.)")
173 ("conjecture-start",
174 "Use all conjecture clauses as start clauses. (Interacts with other start clause options.)")
175 ("restrict-start",
176 "Only use one start clause. (Interacts with other start clause options.)")
177 ("no-regularity",
178 "Don't use the regularity test.")
179 ("all-reductions",
180 "Compute reductions for all literals in the clause, not just the first one.")
181 ("all-extensions",
182 "Compute extensions for all literals in the clause, not just the first one.")
183 ("all-lemmata",
184 "When using lemmata, consider all literals in the clause, not just the first one.")
185 ("no-lemmata",
186 "Do not use lemmata.");
187
188 po::options_description backtrack_options("Backtracking");
189 backtrack_options.add_options()
190 ("all-backtrack",
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.)");
202
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.");
213
214 po::options_description proof_options("Proof generation");
215 proof_options.add_options()
216 ("tptp-proof",
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.")
218 ("prolog-proof",
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.")
220 ("full-verify",
221 "Verify any proof found using the internal proof checker. Use this version to get a detailed description of the verification sent to stdout.")
222 ("verify",
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.");
224
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.")
229 ("sub-latex",
230 "Include substitutions in the LaTeX proof.")
231 ("tiny-latex",
232 "Typeset the latex proof in a tiny font.")
233 ("latex-no-matrix",
234 "Don't include the matrix in the LaTeX proof.");
235
236 po::options_description all_options("Options");
237 all_options.add(main_options)
238 .add(conversion_options)
239 .add(output_options)
240 .add(search_options)
241 .add(backtrack_options)
242 .add(depth_options)
243 .add(proof_options)
244 .add(latex_options);
245
246 po::positional_options_description pos_opts;
247 pos_opts.add("input", -1);
248 po::variables_map vars_map;
249 try {
250 po::store(po::command_line_parser(argc, argv).
251 options(all_options).
252 positional(pos_opts).
253 run(), vars_map);
254 }
255 /*
256 * If the command line options are in error then we exit here.
257 */
258 catch (boost::program_options::error& err) {
259 cout << "% SZS status Error for "
260 << params::problem_name << " : " << err.what() << endl;
261 return EXIT_FAILURE;
262 }
263 po::notify(vars_map);
264 /*
265 * We had a correct parse of the command line, so now we deal with
266 * the options.
267 */
268 if (vars_map.count("help")) {
269 cout << all_options << endl;
270 return EXIT_SUCCESS;
271 }
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;
275 return EXIT_SUCCESS;
276 }
277 if (vars_map.count("verbosity")) {
278 int v = vars_map["verbosity"].as<int>();
279 if (v >= 0 && v <= 3)
280 params::verbosity = v;
281 else
282 cerr << "Verbosity should be between 0 and 5. Using default." << endl;
283 }
284 VPrint show(params::verbosity);
285 if (vars_map.count("sub-output")) {
286 params::output_terms_with_substitution = true;
287 }
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;
292 else
293 cerr << "Indent size is negative or too large. Using default." << endl;
294 }
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;
299 else
300 cerr << "Interval is negative or too large. Using default." << endl;
301 }
302 if (vars_map.count("no-equality")) {
303 params::add_equality_axioms = false;
304 }
305 if (vars_map.count("equality-last")) {
306 params::equality_axioms_at_start = false;
307 }
308 if (vars_map.count("all-distinct-objects")) {
309 params::all_distinct_objects = true;
310 }
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;
315 }
316 params::no_distinct_objects = true;
317 }
318 if (vars_map.count("timeout")) {
319 params::timeout = true;
320 int t = vars_map["timeout"].as<int>();
321 if (t > 0) {
322 if (t >= 10)
323 params::timeout_value = t;
324 else {
325 cerr << "Timeout is too small. Using 10 seconds." << endl;
326 params::timeout_value = 10;
327 }
328 }
329 else
330 cerr << "Timeout should be positive. Using default." << endl;
331 }
332 if (vars_map.count("show-default-schedule")) {
333 params::set_default_schedule();
334 cout << params::default_schedule << endl;
335 exit(EXIT_SUCCESS);
336 }
337 if (vars_map.count("path")) {
338 params::connectpp_path = vars_map["path"].as<string>();
339 }
340 // You should now have all the paths you need, so
341 // finalize them where possible.
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;
350
351 if (vars_map.count("output")) {
352 params::write_output_summary = true;
353 string op = vars_map["output"].as<string>();
354 if (op != "default")
355 params::output_summary_path = op;
356 }
357 if (vars_map.count("all-definitional")) {
358 params::all_definitional = true;
359 }
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;
365 }
366 }
368 if (vars_map.count("schedule")) {
369 params::use_schedule = true;
370 if (!params::timeout) {
371 params::timeout = true;
372 params::timeout_value = 600;
373 }
374 params::schedule_path = vars_map["schedule"].as<string>();
375 try {
376 schedule.read_schedule_from_file(params::schedule_path);
377 }
378 catch (std::exception& err) {
379 cout << "% SZS status Error for "
380 << params::problem_name << " : " << err.what() << endl;
381 return EXIT_FAILURE;
382 }
383 }
384 /*
385 * Note: overides $TPTP environment variable, which is read
386 * earlier.
387 */
388 if (vars_map.count("tptp")) {
389 params::tptp_path = vars_map["tptp"].as<string>();
390 }
391 if (vars_map.count("reorder")) {
392 int n = vars_map["reorder"].as<int>();
393 if (n > 0) {
394 params::deterministic_reorder = true;
395 params::number_of_reorders = n;
396 }
397 else
398 cerr << "Number of re-orders should be positive. Skipping." << endl;
399 }
400 if (vars_map.count("random-reorder")) {
401 params::random_reorder = true;
402 }
403 if (vars_map.count("no-miniscope")) {
404 params::miniscope = false;
405 }
406 if (vars_map.count("show-clauses")) {
407 params::show_clauses = true;
408 }
409 if (vars_map.count("no-colour")) {
410 params::use_colours = false;
411 }
412 /*
413 * Set up the path for the input file. A path to the TPTP may
414 * have been set by now either by picking up the $TPTP environment
415 * variable or using a command-line option.
416 *
417 * This looks really over-engineered, but the complexity that
418 * follows in dealing with TPTP includes probably makes that
419 * a good idea.
420 *
421 * The desired behaviour here is:
422 *
423 * - If it's an absolute path then we're done.
424 *
425 * - If it's a relative path then see if it exists.
426 *
427 * - If it doesn't exist then look for it relative
428 * $TPTP.
429 */
430 fs::path initial_path;
431 bool found_file = false;
432 if (vars_map.count("input")) {
433 // Get what was on the command line.
434 initial_path = vars_map["input"].as<string>();
435
436 // Is it relative?
437 if (initial_path.is_relative()) {
438 // If it's relative, does it exist?
439 if (fs::exists(initial_path)) {
440 // It's an existing, relative path, so expand it. Belt
441 // and braces - make sure you catch things...
442 try {
443 initial_path = fs::canonical(initial_path);
444 }
445 catch (std::filesystem::filesystem_error& err) {
446 cout << "% SZS status Error for "
447 << params::problem_name << " : "
448 << err.what() << endl;
449 return EXIT_FAILURE;
450 }
451 found_file = true;
452 }
453 // It's relative, but doesn't exist...
454 else {
455 // So see if it's relative to $TPTP.
456 fs::path tptp_path(params::tptp_path);
457 initial_path = tptp_path / initial_path;
458 // Does it exist now?
459 if (fs::exists(initial_path)) {
460 // Yes! Expand it. Belt and braces again...
461 try {
462 initial_path = fs::canonical(initial_path);
463 }
464 catch (std::filesystem::filesystem_error& err) {
465 cout << "% SZS status Error for "
466 << params::problem_name << " : "
467 << err.what() << endl;
468 return EXIT_FAILURE;
469 }
470 found_file = true;
471 }
472 }
473 }
474 else {
475 // It's an absolute path.
476 if (initial_path.is_absolute() && fs::exists(initial_path)) {
477 // Found it! Tidy it up. (Yes, belt and braces etc...)
478 try {
479 initial_path = fs::canonical(initial_path);
480 }
481 catch (std::filesystem::filesystem_error& err) {
482 cout << "% SZS status Error for "
483 << params::problem_name << " : "
484 << err.what() << endl;
485 return EXIT_FAILURE;
486 }
487 found_file = true;
488 }
489 }
490 }
491 else {
492 cout << "% SZS status Error for "
493 << params::problem_name << " : no problem specified." << endl;
494 return EXIT_FAILURE;
495 }
496 // Have we found an existibng file?
497 if (!found_file) {
498 cout << "% SZS status Error for "
499 << params::problem_name << " : the specified file does not exist." << endl;
500 return EXIT_FAILURE;
501 }
502 // At this point we have a nice, tidy absolute path.
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;
507
508 /*
509 * Finished sorting out the file/path. Back to the other
510 * options.
511 */
512 if (vars_map.count("depth-limit")) {
513 int l = vars_map["depth-limit"].as<int>();
514 if (l > 1)
515 params::depth_limit = l;
516 else
517 cerr << "Depth limit should be positive. Using default." << endl;
518 }
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;
523 else
524 cerr << "Start depth should be positive and bounded by the maximum depth. Using default." << endl;
525 }
526 if (vars_map.count("depth-increment")) {
527 int l = vars_map["depth-increment"].as<int>();
528 if (l > 0)
529 params::depth_increment = l;
530 else
531 cerr << "Depth increment should be positive. Using default." << endl;
532 }
533 if (vars_map.count("limit-by-tree-depth")) {
534 params::limit_by_tree_depth = true;
535 }
548 if (vars_map.count("restrict-start")) {
549 params::restrict_start = true;
550 }
551 if (vars_map.count("pos-neg-start")) {
552 params::all_pos_neg_start = true;
553 }
554 if (vars_map.count("conjecture-start")) {
555 params::conjecture_start = true;
556 }
557 if (vars_map.count("all-start")) {
558 show(2, string("--all-start set. This cancels all other start options."), true);
560 }
561 /*
562 * Careful! It is possible that no start options were set. If that's
563 * the case just set a sensible one.
564 */
567 }
568 if (vars_map.count("no-regularity")) {
569 params::use_regularity_test = false;
570 }
571 if (vars_map.count("lemmata-backtrack")) {
572 params::limit_bt_lemmas = false;
573 }
574 if (vars_map.count("reduction-backtrack")) {
575 params::limit_bt_reductions = false;
576 }
577 if (vars_map.count("extension-backtrack")) {
578 params::limit_bt_extensions = false;
579 }
580 if (vars_map.count("explore-left-trees")) {
581 params::limit_bt_extensions_left_tree = false;
582 }
583 if (vars_map.count("all-backtrack")) {
584 show(2, string("--all-backtrack set. This prevails over all other backtracking options."), true);
586 }
587 if (vars_map.count("all-reductions")) {
588 params::limit_reductions = false;
589 }
590 if (vars_map.count("all-extensions")) {
591 params::limit_extensions = false;
592 }
593 if (vars_map.count("all-lemmata")) {
594 params::limit_lemmata = false;
595 }
596 if (vars_map.count("no-lemmata")) {
597 params::use_lemmata = false;
598 }
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;
603 else {
604 cerr << "Switch to complete search must happen after start depth. Using start depth." << endl;
605 params::switch_to_complete = params::start_depth;
606 }
607 }
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>();
612 if (lp != "default")
613 params::LaTeX_proof_path = lp;
614 }
615 if (vars_map.count("sub-latex")) {
616 params::sub_LaTeX_proof = true;
617 }
618 if (vars_map.count("tiny-latex")) {
619 params::latex_tiny_proof = true;
620 }
621 if (vars_map.count("latex-no-matrix")) {
622 params::latex_include_matrix = false;
623 }
624 if (vars_map.count("tptp-proof")) {
625 params::generate_tptp_proof = true;
626 params::build_proof = true;
627 }
628 if (vars_map.count("prolog-proof")) {
629 params::generate_Prolog_proof = true;
630 params::build_proof = true;
631 }
632 if (vars_map.count("verify")) {
633 params::verify_proof = true;
634 params::build_proof = true;
635 }
636 if (vars_map.count("full-verify")) {
637 params::verify_proof = true;
638 params::verify_proof_verbose = true;
639 params::build_proof = true;
640 }
641 //------------------------------------------------------------------------
642 //------------------------------------------------------------------------
643 //------------------------------------------------------------------------
644 /*
645 * Now we're ready to start the party.
646 */
647 //------------------------------------------------------------------------
648 //------------------------------------------------------------------------
649 //------------------------------------------------------------------------
650 /*
651 * First, state the time we're starting at.
652 */
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)));
662 StackProver prover;
666 show(1, string("Reading from: "));
667 show(1, path.c_str(), true);
668 bool found_conjecture = false;
669 size_t fof_size = 0;
670 try {
671 prover.read_from_tptp_file(path.c_str(), found_conjecture, fof_size);
672 }
673 catch (std::exception& err) {
674 cout << "% SZS status Error for "
675 << params::problem_name << " : "
676 << err.what() << endl;
677 return EXIT_FAILURE;
678 }
679
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);
685
686 prover.set_problem_path(path);
687 show(2, string("Starting proof attempt for: "), false);
688 show(2, params::problem_name, true);
692 if (params::verbosity >= 2) {
693 prover.show_matrix();
694 }
695 ProverOutcome prover_outcome;
696 ProverOutcome final_outcome;
697 final_outcome = ProverOutcome::TimeOut;
698 //------------------------------------------------------------------------
699 //------------------------------------------------------------------------
700 //------------------------------------------------------------------------
701 /*
702 * No schedule.
703 */
704 //------------------------------------------------------------------------
705 //------------------------------------------------------------------------
706 //------------------------------------------------------------------------
707 if (!params::use_schedule) {
714 if (params::deterministic_reorder) {
715 prover.deterministic_reorder(params::number_of_reorders);
716 }
717 if (params::random_reorder) {
718 prover.random_reorder();
719 }
723 if (params::timeout) {
724 chrono::seconds timeout_duration(params::timeout_value);
725 prover.set_timeout(startTime + timeout_duration);
726 }
727 /*
728 * Run the prover.
729 */
730 prover_outcome = prover.prove();
731 final_outcome = prover_outcome;
732 }
733 //------------------------------------------------------------------------
734 //------------------------------------------------------------------------
735 //------------------------------------------------------------------------
736 /*
737 * A schedule is being used.
738 */
739 //------------------------------------------------------------------------
740 //------------------------------------------------------------------------
741 //------------------------------------------------------------------------
742 else {
746 if (!params::timeout) {
747 params::timeout = true;
748 params::timeout_value = 600;
749 }
750 /*
751 * Convert to milliseconds and get a standard chunk of time.
752 */
753 chrono::milliseconds time_chunk((params::timeout_value * 1000) / 100);
754 chrono::steady_clock::time_point start_time = startTime;
755 chrono::milliseconds chunk_time;
756 /*
757 * If we're using a schedule, then it's already been read from the relevant
758 * file, so we can start it now.
759 */
760 size_t schedule_step_number = 1;
761 pair<bool, unsigned int> next_schedule =
762 schedule.set_next_schedule();
763 if (params::verbosity > 0)
764 cout << endl;
765 /*
766 * Try each step of the schedule in turn.
767 */
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);
773
774 if (next_schedule.second == 0) {
775 prover.set_timeout(startTime + chrono::seconds(params::timeout_value));
776 }
777 else if (schedule_step_number == 1) {
778 prover.set_timeout(startTime + (next_schedule.second * time_chunk));
779 }
780 else {
781 prover.set_timeout(start_time + (next_schedule.second * time_chunk));
782 }
783
784 prover_outcome = prover.prove();
785
786 if (prover_outcome == ProverOutcome::Valid ||
787 prover_outcome == ProverOutcome::Error ||
788 prover_outcome == ProverOutcome::False) {
789 final_outcome = prover_outcome;
790 break;
791 }
792
793 chunk_time = chrono::duration_cast<chrono::milliseconds>(chrono::steady_clock::now() - start_time);
794
795 show.nl(1, 2);
796 show(1, string("Timeout after "));
797 show(1, std::to_string(chunk_time.count()));
798 show(1, string(" milliseconds"), true);
799
800 start_time = chrono::steady_clock::now();
801 schedule_step_number++;
802 next_schedule = schedule.set_next_schedule();
803 }
804 }
805 //------------------------------------------------------------------------
806 //------------------------------------------------------------------------
807 //------------------------------------------------------------------------
808 // We're done, so tidy up.
809 //------------------------------------------------------------------------
810 //------------------------------------------------------------------------
811 //------------------------------------------------------------------------
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);
821 /*
822 * Display the outcome.
823 *
824 * Note that there are a bunch of special cases here, depending on
825 * some possible outcomes of the original clause simplification:
826 *
827 * - You have fof (+cnf, +maybe equality) axioms, and the conjecture can be $false, or empty,
828 * or something.
829 *
830 * - You have no axioms (after simplification) and there's a conjecture
831 * which is not $true or $false but may be empty.
832 */
833 string status(prover.get_status());
834 string outcome;
835
836 bool cnf = prover.problem_is_cnf_only();
837 bool conj_true = prover.problem_has_true_conjecture();
838 bool conj_false = prover.problem_has_false_conjecture();
839 bool conj_missing = prover.problem_has_missing_conjecture();
840 bool neg_conj_removed = prover.problem_has_negated_conjecture_removed();
841 bool fof_has_axioms = prover.problem_has_fof_axioms();
842 bool simplified_has_axioms = prover.simplified_problem_has_fof_axioms();
843
844 cout << "% SZS status ";
845 switch (final_outcome) {
846 case ProverOutcome::Valid:
847 // It's a proved CNF-only problem.
848 if (cnf)
849 outcome = "Unsatisfiable";
850 // It's a proved FOF problem.
851 else {
852 // The problem has axioms.
853 if (simplified_has_axioms) {
854 // Axioms and $true conjecture.
855 if (conj_true) {
856 outcome = "ContradictoryAxioms";
857 }
858 // Axioms and $false conjecture.
859 else if (conj_false || neg_conj_removed) {
860 outcome = "ContradictoryAxioms";
861 }
862 // There was no conjecture. In this case we treat the
863 // axioms as a conjecture, according to the SZS specs.
864 else if (conj_missing) {
865 outcome = "Unsatisfiable";
866 }
867 // Axioms and negated conjecture.
868 else {
869 outcome = "Theorem";
870 }
871 }
872 // The problem doesn't have axioms. Uuurgh... we have to distinguish
873 // between problems that had none in the first place, and problems
874 // where they were simplified out.
875 //
876 // Luckily they turn out to be the same.
877 else {
878 // There's no conjecture because it was essentially $false.
879 if (neg_conj_removed) {
880 outcome = "Error";
881 }
882 // No axioms remaining, but there is a negated conjecture.
883 else
884 outcome = "Theorem";
885 }
886 }
887 break;
888 case ProverOutcome::False:
889 // It's a refuted CNF-only problem.
890 if (cnf)
891 outcome = "Satisfiable";
892 // It's a refuted FOF problem.
893 else {
894 if (simplified_has_axioms) {
895 if (conj_true) {
896 outcome = "Error";
897 }
898 else if (conj_false || neg_conj_removed) {
899 outcome = "CounterSatisfiable";
900 }
901 else if (conj_missing) {
902 outcome = "Satisfiable";
903 }
904 else {
905 outcome = "CounterSatisfiable";
906 }
907 }
908 else {
909 // There's no conjecture, and the axioms are $true.
910 if (conj_missing)
911 outcome = "Theorem";
912 // There's no conjecture because it was essentially $false.
913 else if (neg_conj_removed) {
914 outcome = "Error";
915 }
916 // No axioms remaining, but there is a negated conjecture.
917 else
918 outcome = "CounterSatisfiable";
919 }
920 }
921 break;
922 case ProverOutcome::PathLenLimit:
923 outcome = "GaveUp";
924 break;
925 case ProverOutcome::Error:
926 outcome = "Error";
927 break;
928 case ProverOutcome::TimeOut:
929 outcome = "Timeout";
930 break;
931 default:
932 outcome = "Error";
933 break;
934 }
935 cout << outcome << " for " << params::problem_name;
936 /*
937 * If needed, verify the proof.
938 */
939 bool verified = false;
940 if (params::verify_proof && final_outcome == ProverOutcome::Valid) {
941 std::tuple<VariableIndex*,
944 TermIndex*>
945 inds = prover.get_indexes();
946
947 vector<pair<string, vector<size_t>>>
948 internal_proof(prover.get_internal_proof());
949
950 ProofChecker checker(prover.get_matrix(),
951 internal_proof,
952 get<0>(inds), get<3>(inds));
953
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;
960 }
961 else {
962 verification_outcome = checker.check_proof();
963 }
964
965 if (verification_outcome) {
966 verified = true;
967 cout << " : Verified";
968 }
969 else {
970 cout << " : FailedVerification";
971 }
972
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;
977 }
978 }
979 cout << endl;
980 /*
981 * Leave a minimal file with some outcome information.
982 */
983 if (params::write_output_summary) {
984 try {
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;
989 else
990 out_file << "NoConjectureFound" << endl;
991 if (status == "")
992 status = "NoStatus";
993 out_file << "ProblemStatus: " << status << endl;
994 out_file << "ProverOutcome: " << outcome << endl;
995 if (params::verify_proof && final_outcome == ProverOutcome::Valid) {
996 if (verified)
997 out_file << "Verified" << endl;
998 else
999 out_file << "FailedVerification" << endl;
1000 }
1001 else
1002 out_file << "NoVerify" << endl;
1003 out_file << "Time: " << runTime.count() << endl;
1004 out_file.close();
1005 }
1006 catch (std::exception& err) {
1007 cerr << "Error: can't write output summary." << endl;
1008 }
1009 }
1010 /*
1011 * If necessary, write a TPTP proof to stdout.
1012 */
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;
1016 prover.show_tptp_proof();
1017 cout << "% SZS output end Proof for " << params::problem_name << endl;
1018 }
1019 return EXIT_SUCCESS;
1020}
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.
Definition TermIndex.hpp:75
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.
Definition Schedule.hpp:100
Hide all the global stuff in this namespace.
Definition Schedule.cpp:27
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.