Connect++ 0.3.0
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
StackProver.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 "StackProver.hpp"
26
27//----------------------------------------------------------------------
29: num_preds(0)
30, var_index()
31, fun_index()
32, term_index()
33, pred_index()
34, sub_stack()
35, results()
36, matrix()
37, path()
38, new_C()
39, lemmata()
40, u()
41, action(InferenceItemType::Start)
42, si(nullptr)
43, current_depth_limit(0)
44, current_depth(1)
45, depth_limit_reached(false)
46, status()
47, stack()
48, right_branch_stack()
49, backtrack(false)
50, proof_printer(&stack)
51, problem_path()
52, output_interval(params::output_frequency)
53, reductions_tried(0)
54, extensions_tried(0)
55, lemmata_tried(0)
56, right_branches_started(0)
57, proof_count(0)
58, use_timeout(false)
59, end_time()
60, show(params::verbosity)
61, cnf_only(false)
62, conjecture_true(false)
63, conjecture_false(false)
64, conjecture_missing(false)
65, negated_conjecture_removed(false)
66, fof_has_axioms(false)
67, simplified_fof_has_axioms(false)
68{}
69//----------------------------------------------------------------------
71 num_preds = n;
74}
75//----------------------------------------------------------------------
76void StackProver::read_from_tptp_file(const string& file_name,
77 bool& found_conjecture,
78 size_t& fof_size) {
80 parser.parse_tptp_from_file(file_name);
81 status = parser.get_problem_status();
82 bool equality = parser.equality_used();
83 found_conjecture = parser.conjecture_present();
84 fof_size = parser.number_of_fof_formulas();
85 Predicate* equals_predicate = parser.get_equals_predicate();
93 parser.clear();
95 /*
96 * num_preds for Matrix is set by parser.
97 */
99
100 if (params::show_clauses) {
101 std::exit(EXIT_SUCCESS);
102 }
103
104 if (status != string("")) {
105 show(1, string("Problem status found: "));
106 show(1, status, true);
107 }
108 if (equality && params::add_equality_axioms) {
109 show(1, string("Problem involves equality: adding axioms for =."), true);
110 add_equality_axioms(equals_predicate);
111 if (params::equality_axioms_at_start) {
113 }
114 }
115 /*
116 * Any further variables will be anonymous.
117 */
119
120 if (params::generate_Prolog_proof && params::build_proof) {
121 matrix.write_to_prolog_file(params::Prolog_matrix_path);
122 }
123 }
124//----------------------------------------------------------------------
126 /*
127 * Equality axioms as described in Handbook of Automated
128 * Reasoning, Volume 1, page 615.
129 */
130 Arity max_fun_arity = fun_index.find_maximum_arity();
131 Arity max_pred_arity = pred_index.find_maximum_arity();
132 /*
133 * You need at least three variables to describe these, and
134 * twice as many as the arity of the biggest predicate or
135 * function.
136 */
137 uint32_t max_arity = max_fun_arity;
138 if (max_pred_arity > max_arity)
139 max_arity = max_pred_arity;
140 if (max_arity < 3)
141 max_arity = 3;
142 vector<Term*> xs;
143 vector<Term*> ys;
144 string xvar("__eqx_");
145 string yvar("__eqy_");
146 for (size_t i = 0; i < max_arity; i++) {
147 Variable* xvarp = var_index.add_named_var(xvar + std::to_string(i));
148 Variable* yvarp = var_index.add_named_var(yvar + std::to_string(i));
149 xs.push_back(term_index.add_variable_term(xvarp));
150 ys.push_back(term_index.add_variable_term(yvarp));
151 }
152 /*
153 * How you construct these depends on which representation you're using.
154 * It's easy enough to show that the difference is only a case
155 * of swapping negations. See for example "Equality Preprocessing in
156 * Connection Calculi", Oliver and Otten.
157 */
158 bool pol = !params::positive_representation;
159 uint32_t n_added = 0;
160 /*
161 * Axiom for reflexivity.
162 */
163 vector<Term*> ref;
164 ref.push_back(xs[0]);
165 ref.push_back(xs[0]);
166 Literal reflexive(equals_predicate, ref, 2, pol);
167 Clause ref_c;
168 ref_c.add_lit(reflexive);
169 matrix.add_clause(ref_c, "equality");
170 n_added++;
171 /*
172 * Axiom for symmetry.
173 */
174 vector<Term*> xy;
175 xy.push_back(xs[0]);
176 xy.push_back(xs[1]);
177 vector<Term*> yx;
178 yx.push_back(xs[1]);
179 yx.push_back(xs[0]);
180 Literal sym1(equals_predicate, xy, 2, !pol);
181 Literal sym2(equals_predicate, yx, 2, pol);
182 Clause sym_c;
183 sym_c.add_lit(sym1);
184 sym_c.add_lit(sym2);
185 matrix.add_clause(sym_c, "equality");
186 n_added++;
187 /*
188 * Axiom for transitivity.
189 */
190 vector<Term*> yz;
191 yz.push_back(xs[1]);
192 yz.push_back(xs[2]);
193 vector<Term*> xz;
194 xz.push_back(xs[0]);
195 xz.push_back(xs[2]);
196 Literal tr1(equals_predicate, xy, 2, !pol);
197 Literal tr2(equals_predicate, yz, 2, !pol);
198 Literal tr3(equals_predicate, xz, 2, pol);
199 Clause tr_c;
200 tr_c.add_lit(tr1);
201 tr_c.add_lit(tr2);
202 tr_c.add_lit(tr3);
203 matrix.add_clause(tr_c, "equality");
204 n_added++;
205 /*
206 * Function substitution.
207 */
208 for (size_t j = 0; j < fun_index.get_size(); j++) {
209 Function* p = fun_index[j];
210 Arity ar = p->get_arity();
211 if (ar > 0) {
212 Clause c;
213 vector<Term*> x1xn;
214 vector<Term*> y1yn;
215 for (size_t i = 0; i < ar; i++) {
216 x1xn.push_back(xs[i]);
217 y1yn.push_back(ys[i]);
218 vector<Term*> xiyi;
219 xiyi.push_back(xs[i]);
220 xiyi.push_back(ys[i]);
221 Literal eq_lit(equals_predicate, xiyi, 2, !pol);
222 c.add_lit(eq_lit);
223 }
224 vector<Term*> t;
225 t.push_back(term_index.add_function_term(p, x1xn));
226 t.push_back(term_index.add_function_term(p, y1yn));
227 Literal f_lit(equals_predicate, t, 2, pol);
228 c.add_lit(f_lit);
229 matrix.add_clause(c, "equality");
230 n_added++;
231 }
232 }
233 /*
234 * Predicate substitution.
235 */
236 for (size_t j = 0; j < pred_index.get_num_preds(); j++) {
237 Predicate* p = pred_index[j];
238 Arity ar = p->get_arity();
239 if (ar > 0 && p != equals_predicate) {
240 Clause c;
241 vector<Term*> x1xn;
242 vector<Term*> y1yn;
243 for (size_t i = 0; i < ar; i++) {
244 x1xn.push_back(xs[i]);
245 y1yn.push_back(ys[i]);
246 vector<Term*> xiyi;
247 xiyi.push_back(xs[i]);
248 xiyi.push_back(ys[i]);
249 Literal eq_lit(equals_predicate, xiyi, 2, !pol);
250 c.add_lit(eq_lit);
251 }
252 Literal p_lit1(p, x1xn, ar, !pol);
253 Literal p_lit2(p, y1yn, ar, pol);
254 c.add_lit(p_lit1);
255 c.add_lit(p_lit2);
256 matrix.add_clause(c, "equality");
257 n_added++;
258 }
259 }
260 /*
261 * Distinct objects
262 */
263 Arity min_arity = fun_index.find_minimum_arity();
264 if (!params::no_distinct_objects && min_arity == 0) {
265 vector<Term*> all_distinct_constants;
266 vector<Term*> empty_args;
267 for (size_t i = 0; i < fun_index.get_size(); i++) {
268 Function* p = fun_index[i];
269 Arity ar = p->get_arity();
270 // Remember, you don't want to do this for Skolem constants.
271 string name = p->get_name();
272 string prefix = name.string::substr(0,params::unique_skolem_prefix.length());
273 bool is_skolem = (params::unique_skolem_prefix.string::compare(0, string::npos, prefix) == 0) &&
274 (params::unique_skolem_prefix.length() < name.length());
275 bool is_quoted = (name[0] == '\"' && name[name.size() - 1] == '\"');
276 if (ar == 0 &&
277 !is_skolem &&
278 (params::all_distinct_objects || is_quoted)) {
279 Term* t = term_index.add_function_term(p, empty_args);
280 all_distinct_constants.push_back(t);
281 }
282 }
283 size_t s = all_distinct_constants.size();
284 if (s > 1) {
285 for (size_t i = s - 1; i > 0; i--) {
286 for (size_t j = 0; j < i; j++) {
287 Clause c;
288 vector<Term*> args;
289 args.push_back(all_distinct_constants[i]);
290 args.push_back(all_distinct_constants[j]);
291 Literal eq_lit(equals_predicate, args, 2, !pol);
292 c.add_lit(eq_lit);
293 matrix.add_clause(c, "distinct_objects");
294 n_added++;
295 }
296 }
297 }
298 }
299 matrix.set_num_equals(n_added);
300}
301//----------------------------------------------------------------------
303 /*
304 * Don't waste your time if the regularity test applies.
305 */
306 if (params::use_regularity_test && !path.test_for_regularity(new_C))
307 return;
308 /*
309 * Don't try to populate axioms.
310 */
311 if (new_C.size() == 0) {
312 return;
313 }
314 /*
315 * NOTE: As these are being stacked, lemmata are actually tried
316 * first.
317 */
318 /*
319 * Extensions
320 */
321 if (params::limit_extensions)
323 else
325 /*
326 * Reductions
327 */
328 if (params::limit_reductions)
330 else
332 /*
333 * Lemmata
334 */
335 if (params::use_lemmata) {
336 if (params::limit_lemmata)
338 else
340 }
341}
342//----------------------------------------------------------------------
344 bool result = ((params::limit_by_tree_depth && (current_depth == current_depth_limit))
345 ||
346 (!params::limit_by_tree_depth && (si->p.length() == current_depth_limit)));
347 if (result)
348 depth_limit_reached = true;
349 return result;
350}
351//----------------------------------------------------------------------
352bool StackProver::axiom() const {
353 return si->c.empty();
354}
355//----------------------------------------------------------------------
357 /*
358 * Add a new StackItem using the next action from the list stored
359 * in the StackItem currently in play. If necessary, also
360 * add something to right_branch_stack. Populate the new list of
361 * actions and update si.
362 */
363 action = si->actions.back();
364 si->actions.pop_back();
366 /*
367 * Why are the scope rules for switch so odd???
368 */
369 Clause old_C;
370 Lemmata old_Lem;
371 switch (action.T) {
372 //----------------------------------------------------------------------
373 //----------------------------------------------------------------------
374 //----------------------------------------------------------------------
375 // Lemmata.
376 //----------------------------------------------------------------------
377 //----------------------------------------------------------------------
378 //----------------------------------------------------------------------
379 case InferenceItemType::Lemma:
381 /*
382 * If you are restricting backtracking for lemmata then
383 * at this point you can remove all alternatives.
384 */
385 if (params::limit_bt_lemmas)
387 /*
388 * Work out the new state.
389 */
390 new_C = si->c;
392 path = si->p;
393 lemmata = si->l;
394 /*
395 * Extend the stack.
396 */
397 stack.push_back(StackItem(StackItemType::Lemmata, new_C, path,
399 stack.back().set_this_action(action);
400 break;
401 //----------------------------------------------------------------------
402 //----------------------------------------------------------------------
403 //----------------------------------------------------------------------
404 // Reduction.
405 //----------------------------------------------------------------------
406 //----------------------------------------------------------------------
407 //----------------------------------------------------------------------
408 case InferenceItemType::Reduction:
410 /*
411 * If you are restricting backtracking for reductions then
412 * at this point you can remove all alternatives.
413 */
414 if (params::limit_bt_reductions)
416 /*
417 * Reductions have a substitution, so apply it and remember
418 * in case you need to undo it later.
419 */
422 /*
423 * Work out the new state.
424 */
425 new_C = si->c;
427 path = si->p;
428 lemmata = si->l;
430 /*
431 * Extend the stack.
432 */
433 stack.push_back(StackItem(StackItemType::Reduction, new_C, path,
435 stack.back().set_this_action(action);
436 break;
437 //----------------------------------------------------------------------
438 //----------------------------------------------------------------------
439 //----------------------------------------------------------------------
440 // Extension.
441 //----------------------------------------------------------------------
442 //----------------------------------------------------------------------
443 //----------------------------------------------------------------------
444 case InferenceItemType::Extension:
446 /*
447 * You're going to generate new variables, so remember where to
448 * backtrack to.
449 */
451 /*
452 * This is an Extension, so you're going to add something to
453 * right_branch_stack.
454 */
455 path = si->p;
456 old_C = si->c;
458 old_Lem = si->l;
459 old_Lem.push_back(action.L);
460 /*
461 * DON'T do populate_stack_item here! That can wait until you actually
462 * use the right branch. In fact it *has* to wait because we might
463 * apply substitutions that affect it.
464 */
465 right_branch_stack.push_back(StackItem(StackItemType::RightBranch, old_C,
466 path, old_Lem, current_depth));
467 /*
468 * The right branch needs to know where to restrict backtracking.
469 */
470 right_branch_stack.back().set_bt_restriction_index(stack.size() - 1);
471 /*
472 * Now you can deal with the left branch.
473 */
474 new_C = matrix[action.C_2].make_copy_with_new_vars(var_index, term_index);
475 /*
476 * Extensions have a substitution, so apply it and remember
477 * in case you need to undo it later.
478 */
481 /*
482 * Work out the new state.
483 */
485 path.push(action.L);
486 lemmata = si->l;
487 /*
488 * Extend the stack.
489 */
490 stack.push_back(StackItem(StackItemType::LeftBranch, new_C, path,
492 stack.back().set_this_action(action);
493 break;
494 default:
495 cerr << "PANIC!!! You should only have a lemmata, reduction or an extension here!"
496 << endl;
497 break;
498 }
499 /*
500 * Finally, move si on and work out the next bunch of possible actions.
501 */
502 si = &stack.back();
504}
505//----------------------------------------------------------------------
507 /*
508 * When you're moving forward in the search and you hit an axiom,
509 * you need to see whether there are right branches still needing
510 * to be dealt with.
511 *
512 * Note that an empty right_branch_stack - meaning that you've
513 * found a proof - is dealt with by go().
514 *
515 * this_action does not get populated for the new StackItem in
516 * this case.
517 */
519 /*
520 * Move the next right branch to the stack.
521 */
522 stack.push_back(right_branch_stack.back());
523 right_branch_stack.pop_back();
524 /*
525 * Reset si.
526 */
527 si = &stack.back();
528 /*
529 * Set up the new state.
530 */
531 new_C = si->c;
532 path = si->p;
533 lemmata = si->l;
535 /*
536 * We deliberately delayed doing this, so do it now. (See
537 * documentation for StackProver::extend_with_action.)
538 */
540 /*
541 * At this point you are starting a right branch, so
542 * if you are restricting backtracking you remove all
543 * alternatives from the relevant point in the stack.
544 */
545 if (params::limit_bt_extensions) {
546 stack[si->bt_restriction_index].restrict_backtrack();
547 }
548}
549//----------------------------------------------------------------------
551 backtrack = true;
552 stack.pop_back();
553 si = &stack.back();
555}
556//----------------------------------------------------------------------
560}
561//----------------------------------------------------------------------
564}
565//----------------------------------------------------------------------
567 /*
568 * You're backtracking through a left branch, so you
569 * need to remember to get rid of the corresponding
570 * right branch as well.
571 */
572 right_branch_stack.pop_back();
576}
577//----------------------------------------------------------------------
598 /*
599 * If you're not limiting backtracking for extensions, or
600 * you *are*, but you're still exploring left trees, then this
601 * is straightforward: just put the item back on right_branch_stack
602 * so that it gets explored again later.
603 */
604 if (!params::limit_bt_extensions ||
605 ((params::limit_bt_extensions || params::limit_bt_all) &&
606 !params::limit_bt_extensions_left_tree)) {
607 /*
608 * Why is this necessary? After we backtrack we may make different
609 * substitutions, so in revisiting the right branch different
610 * possibilties may apply, so we re-compute them later.
611 */
612 stack.back().clear();
613 right_branch_stack.push_back(stack.back());
615 return;
616 }
617 /*
618 * We know we are limiting backtracking for extensions, and we
619 * are not exploring the left tree.
620 *
621 * Care is needed if you're not backtracking within the left
622 * part of the tree. You need to move back down the stack,
623 * deleting everything while also making sure that sub_stack
624 * and var_index are correctly maintained. Also, you don't
625 * want to return anything to right_branch_stack.
626 *
627 * This goes back to where the relevant literal was selected.
628 * Thus if you are not limiting the possibilities to only those
629 * for the first literal, it's open to the backtracking
630 * restriction to leave other possibilites to be tried, and
631 * they get picked up from this point.
632 */
633 if (params::limit_bt_extensions_left_tree) {
634 size_t target_index = si->bt_restriction_index;
635 size_t current_index = stack.size() - 1;
636 while (current_index > target_index) {
637 switch (si->item_type) {
638 case StackItemType::Lemmata:
639 break;
640 case StackItemType::Reduction:
642 break;
643 case StackItemType::LeftBranch:
646 break;
647 case StackItemType::RightBranch:
648 break;
649 default:
650 cerr << "Something is VERY WRONG!" << endl;
651 break;
652 }
654 current_index--;
655 }
656 }
657}
658//----------------------------------------------------------------------
659ProverResult StackProver::go() {
660 /*
661 * Having set up a single entry on the stack, containing a start
662 * state, search for a proof.
663 *
664 * Either you return by ending at the start state with nothing left
665 * to try, by finding a proof, by depth limiting or by timing out.
666 *
667 * The backtrack variable is important here - when true you are
668 * (surprise surprise) backtracking. So mostly each case in the
669 * following switch is divided according to whether you're going
670 * forward or backtracking.
671 */
672 while(true) {
673 /*
674 * Test for and deal with a timeout.
675 */
676 if (use_timeout && chrono::steady_clock::now() > end_time)
677 return ProverResult::TimeOut;
678 /*
679 * Say what's going on.
680 */
681 if (output_interval.tick() && params::verbosity >= 2) {
682 cout << cursor_symbols::Cursor::to_column(1);
684 cout << "Reductions: " << reductions_tried << " Extensions: " << extensions_tried;
685 cout << " Lemmata: " << lemmata_tried << " Right branches: " << right_branches_started;
686 cout << " Stack size: " << stack.size();
687 cout.flush();
688 }
689 /*
690 * si must point to the back of the stack at this point.
691 *
692 * Remember that extend_with_action will deal with this for you.
693 */
694 switch (si->item_type) {
695 //----------------------------------------------------------------
696 //----------------------------------------------------------------
697 //----------------------------------------------------------------
698 // Deal with the start state. Essentially straightforward. Just
699 // deal with a completed search, otherwise work out the
700 // possibly actions and get on with it.
701 //----------------------------------------------------------------
702 //----------------------------------------------------------------
703 //----------------------------------------------------------------
704 case StackItemType::Start:
705 backtrack = false;
706 if (si->actions.empty())
707 return ProverResult::OptionsExhausted;
708 else
710 break;
711 //----------------------------------------------------------------
712 //----------------------------------------------------------------
713 //----------------------------------------------------------------
714 // Lemmata. Again, mostly straightforward.
715 //----------------------------------------------------------------
716 //----------------------------------------------------------------
717 //----------------------------------------------------------------
718 case StackItemType::Lemmata:
719 /*
720 * Operation is essentially similar to the reduction case.
721 *
722 * First deal with moving forward.
723 */
724 if (!backtrack) {
725 if (axiom()) {
726 /*
727 * Either you've found a proof or you try a right branch.
728 */
729 if (right_branch_stack.empty())
730 return ProverResult::Valid;
731 else
733 }
734 /*
735 * Backtrack because of depth limiting.
736 */
737 else if (depth_limited())
739 /*
740 * Backtrack because there's nothing left to try.
741 */
742 else if (si->actions.empty())
744 /*
745 * There must be something left to try, so try it.
746 */
747 else
749 }
750 /*
751 * We are moving down the stack.
752 */
753 else {
754 /*
755 * If you're backtracking then you need to jump over axioms.
756 */
757 if (axiom())
759 /*
760 * If you're not at an axiom then you can start going forward
761 * again.
762 */
763 else
764 backtrack = false;
765 }
766 break;
767 //----------------------------------------------------------------
768 //----------------------------------------------------------------
769 //----------------------------------------------------------------
770 // Reduction. Almost identical to Lemmata, but note the
771 // slightly different backtracking requirement to take account
772 // of undoing the substitution.
773 //----------------------------------------------------------------
774 //----------------------------------------------------------------
775 //----------------------------------------------------------------
776 case StackItemType::Reduction:
777 /*
778 * We are moving up the stack.
779 */
780 if (!backtrack) {
781 if (axiom()) {
782 /*
783 * Either you've found a proof or you try a right branch.
784 */
785 if (right_branch_stack.empty())
786 return ProverResult::Valid;
787 else
789 }
790 /*
791 * Backtrack because of depth limiting.
792 */
793 else if (depth_limited())
795 /*
796 * Backtrack because there's nothing left to try.
797 */
798 else if (si->actions.empty())
800 /*
801 * There must be something left to try, so try it.
802 */
803 else
805 }
806 /*
807 * We are moving down the stack.
808 */
809 else {
810 /*
811 * If you're backtracking then you need to jump over axioms.
812 */
813 if (axiom())
815 /*
816 * If you're not at an axiom then you can start going forward
817 * again.
818 */
819 else
820 backtrack = false;
821 }
822 break;
823 //----------------------------------------------------------------
824 //----------------------------------------------------------------
825 //----------------------------------------------------------------
826 // Left branch of Extension. Mostly similar to the Reduction
827 // and Lemmata cases, but the backtrack is again different to
828 // take care of the new variables, the substitution, and the
829 // right_branch_stack.
830 //----------------------------------------------------------------
831 //----------------------------------------------------------------
832 //----------------------------------------------------------------
833 case StackItemType::LeftBranch:
834 /*
835 * Operation is essentially similar to the Reduction and
836 * Lemmata cases. See those for corresponding comments.
837 */
838 if (!backtrack) {
839 if (axiom())
841 else if (depth_limited())
843 else if (si->actions.empty())
845 else
847 }
848 /*
849 * We are moving down the stack.
850 */
851 else {
852 if (axiom())
854 else
855 backtrack = false;
856 }
857 break;
858 //----------------------------------------------------------------
859 //----------------------------------------------------------------
860 //----------------------------------------------------------------
861 // Right branch of Extension. Mostly similar to the Reduction
862 // and Lemmata cases, but the backtrack is now much more
863 // delicate. See the documentation for right_extension_backtrack.
864 //----------------------------------------------------------------
865 //----------------------------------------------------------------
866 //----------------------------------------------------------------
867 case StackItemType::RightBranch:
868 /*
869 * Operation is essentially similar to the reduction case.
870 */
871 if (!backtrack) {
872 if (axiom()) {
873 if (right_branch_stack.empty())
874 return ProverResult::Valid;
875 else
877 }
878 else if (depth_limited())
880 else if (si->actions.empty())
882 else
884 }
885 /*
886 * We are moving down the stack.
887 */
888 else {
889 if (axiom())
891 else
892 backtrack = false;
893 }
894 break;
895 //----------------------------------------------------------------
896 default:
897 cerr << "Something is VERY WRONG!" << endl;
898 break;
899 }
900 }
901 return ProverResult::Error;
902}
903//----------------------------------------------------------------------
904// Set start clauses according to current options.
905//
906// Note that restrict_start with !all_pos_neg_start and !conjecture_start
907// should never be available as it would make no sense.
908//
909// all_pos_neg_start along with conjecture_start are on a best-effort
910// basis - you may end up with nothing.
911//----------------------------------------------------------------------
913 results.clear();
914 size_t m_size = matrix.get_num_clauses();
915 /*
916 * Make sure noone has messed up and not set any start
917 * clause optionss.
918 */
921 /*
922 * The allstart option overides everything else so this is easy.
923 */
924 if (params::all_start) {
925 for (size_t i = 0; i < m_size; i++) {
926 results.push_back(StartClauseStatus::Start);
927 }
928 return;
929 }
930 bool first_clause_included = false;
931 /*
932 * params::all_pos_neg_start indicates use of positive
933 * or negative start clauses according to the representation.
934 * When you don't also have conjecture_start, either include
935 * all, or just the first possibility found.
936 */
937 if (params::all_pos_neg_start && !params::conjecture_start) {
938 for (size_t i = 0; i < m_size; i++) {
939 if (
940 (
941 (params::positive_representation && matrix.is_positive(i))
942 ||
943 (!params::positive_representation && matrix.is_negative(i))
944 )
945 &&
946 (!(params::restrict_start && first_clause_included))
947 ) {
948 results.push_back(StartClauseStatus::Start);
949 first_clause_included = true;
950 }
951 else {
952 results.push_back(StartClauseStatus::NoStart);
953 }
954 }
955 }
956 /*
957 * Similar case if you have conjecture_start but not all_pos_neg_start.
958 */
959 else if (!params::all_pos_neg_start && params::conjecture_start) {
960 for (size_t i = 0; i < m_size; i++) {
961 if (matrix.is_conjecture(i)
962 &&
963 (!(params::restrict_start && first_clause_included))) {
964 results.push_back(StartClauseStatus::Start);
965 first_clause_included = true;
966 }
967 else {
968 results.push_back(StartClauseStatus::NoStart);
969 }
970 }
971 }
972 /*
973 * The tricky case is when you want to combine pos/neg clauses,
974 * conjecture clauses, and restriction in some other way.
975 *
976 * Assume here that you have all_pos_neg_start and conjecture_start.
977 */
978 else {
979 for (size_t i = 0; i < m_size; i++) {
980 if (matrix.is_conjecture(i)
981 &&
982 (
983 (params::positive_representation && matrix.is_positive(i))
984 ||
985 (!params::positive_representation && matrix.is_negative(i))
986 )
987 &&
988 !(params::restrict_start && first_clause_included)) {
989 results.push_back(StartClauseStatus::Start);
990 first_clause_included = true;
991 }
992 else {
993 results.push_back(StartClauseStatus::NoStart);
994 }
995 }
996 }
997 /*
998 * There's a rare possibility that---because either there was no
999 * (negated) conjecture clause in the problem, or they were
1000 * simplified out---at this point no start clause has been
1001 * selected. If that's the case, either use all positive/negative
1002 * clauses or just the first, according to the parameters set.
1003 *
1004 * Note: this must choose at least one start clause because problems
1005 * without a positive and negative clause have already been solved.
1006 */
1007 if (!first_clause_included) {
1008 if (params::verbosity > 2) {
1009 cout << "Note: you're asking for a conjecture to start, but there are none!" << endl;
1010 cout << " depending on the other parameter settings, we will use one or " << endl;
1011 cout << " all of the negative clauses." << endl;
1012 }
1013 // Don't forget this! If you get here you have a whole bunch of
1014 // NoStart in results!
1015 results.clear();
1016 for (size_t i = 0; i < m_size; i++) {
1017 if ((
1018 (params::positive_representation && matrix.is_positive(i))
1019 ||
1020 (!params::positive_representation && matrix.is_negative(i))
1021 ) &&
1022 !(params::restrict_start && first_clause_included)) {
1023 results.push_back(StartClauseStatus::Start);
1024 first_clause_included = true;
1025 }
1026 else {
1027 results.push_back(StartClauseStatus::NoStart);
1028 }
1029 }
1030 }
1031}
1032//----------------------------------------------------------------------
1033//----------------------------------------------------------------------
1034//----------------------------------------------------------------------
1035// Find a single proof using iterative deepening search.
1036//----------------------------------------------------------------------
1037//----------------------------------------------------------------------
1038//----------------------------------------------------------------------
1039ProverOutcome StackProver::prove() {
1040 pair<bool, size_t> start_clause = matrix.find_start();
1041 /*
1042 * If the initial clauses don't have a positive and a negative
1043 * clause then the problem is trivial.
1044 */
1045 if (!start_clause.first) {
1046 return ProverOutcome::False;
1047 }
1048 /*
1049 * Deal with the possible ways to set up start clause(s) according to
1050 * the options. Keep track of which start clauses are in use, and if
1051 * necessary what outcomes for them have been seen so far.
1052 */
1054 /*
1055 * Main loop for iterative deepening search.
1056 */
1057 bool switched_to_complete = false;
1058 for (current_depth_limit = params::start_depth;
1059 current_depth_limit <= params::depth_limit;
1060 current_depth_limit += params::depth_increment) {
1061 /*
1062 * See if the parameters dictate that it's time to convert to
1063 * a complete search.
1064 */
1065 if (current_depth_limit >= params::switch_to_complete
1066 && !switched_to_complete) {
1068 /*
1069 * You may have changed some parameters, so make sure all relevant
1070 * start clauses now get tried.
1071 */
1073 current_depth_limit = params::start_depth;
1074 switched_to_complete = true;
1075 colour_string::ColourString cs(params::use_colours);
1076 show.nl(1);
1077 show(1, cs("Switching to complete search.").orange(), true);
1078 }
1079 show.nl(1);
1080 show(1, string("SEARCH TO DEPTH: "));
1081 show(1, std::to_string(current_depth_limit), true);
1082 /*
1083 * Generate each possible start move, and try to prove from
1084 * it.
1085 */
1086 size_t start_clause_index = 0;
1087 for (const Clause& C : matrix) {
1088 /*
1089 * Find the next start clause.
1090 */
1091 if (results[start_clause_index] == StartClauseStatus::NoStart
1092 || results[start_clause_index] == StartClauseStatus::False) {
1093 start_clause_index++;
1094 continue;
1095 }
1096 /*
1097 * Reset everything to use the current start clause.
1098 *
1099 * TODO: this is slightly messy at present because
1100 * the var_index doesn't necessarily get reset in the
1101 * most efficient way possible if a previous schedule
1102 * attempt timed out. (You'd need to go back down
1103 * the stack and backtrack it as necessary.) This is
1104 * of course irrelevant
1105 * because it just means you might not get full re-use of
1106 * new variable names, but all the same it would be nice
1107 * to fix.
1108 */
1112 /*
1113 * Say what's going on.
1114 */
1115 show(1, string("START from clause "));
1116 show(1, std::to_string(start_clause_index + 1));
1117 show(1, string(" of "));
1118 show(1, std::to_string(matrix.get_num_clauses()));
1119 show(2, string(": "));
1120 show(2, new_C.to_string(), true);
1121 cout.flush();
1122 /*
1123 * Set up the initial stack item containing the start clause, and
1124 * populate it.
1125 */
1126 StackItem start_item(StackItemType::Start, new_C, path, lemmata, 1);
1127 start_item.set_this_action(InferenceItem(InferenceItemType::Start, start_clause_index));
1128 stack.push_back(start_item);
1129 si = &stack.back();
1131 /*
1132 * Start with depth 1, as this makes sense when reading output if you're
1133 * using depth of recursion or path length.
1134 */
1135 current_depth = 1;
1136 /*
1137 * Liftoff!!!
1138 */
1139 ProverResult result = go();
1140 /*
1141 * Dealing with the outcome takes some care and depends on
1142 * the parameters being used.
1143 */
1144 switch (result) {
1145 case ProverResult::Valid:
1146 proof_count++;
1147 if (params::build_proof) {
1148 if (params::generate_LaTeX_proof) {
1149 proof_printer.make_LaTeX(params::LaTeX_proof_path,
1151 matrix.make_LaTeX());
1152 }
1153 if (params::generate_Prolog_proof) {
1154 fs::path prolog_path = params::Prolog_proof_path;
1155 proof_printer.make_Prolog(prolog_path);
1156 }
1157 }
1158 show(1, string(": Found proof number "));
1159 show(1, std::to_string(proof_count), true);
1160 return ProverOutcome::Valid;
1161 break;
1162 case ProverResult::Error:
1163 return ProverOutcome::Error;
1164 break;
1165 case ProverResult::TimeOut:
1166 return ProverOutcome::TimeOut;
1167 break;
1168 case ProverResult::OptionsExhausted:
1169 /*
1170 * If you ran out of options because you reached the depth
1171 * limit then you still need to continue.
1172 */
1173 if (depth_limit_reached) {
1174 show(1, string(": Depth limited"), true);
1175 }
1176 /*
1177 * If you ran out of options without reaching the depth limit, then
1178 * what you do depends on whether or not the search is complete.
1179 */
1180 else {
1182 results[start_clause_index] = StartClauseStatus::False;
1183 show(1, string(": False"), true);
1184 }
1185 }
1186 start_clause_index++;
1187 break;
1188 default:
1189 return ProverOutcome::Error;
1190 break;
1191 }
1192 /*
1193 * This is necessary. Yes, I've checked. Think about it: you need
1194 * one extra backtrack to undo the new variables generated when you
1195 * make a start clause.
1196 */
1198 }
1199 /*
1200 * Loop for start moves ends here.
1201 *
1202 * If everything was False then the theorem is False, otherwise
1203 * at least one attempt was depth-limited.
1204 */
1205 bool all_false = true;
1206 for (StartClauseStatus& outcome : results) {
1207 if (outcome == StartClauseStatus::Start) {
1208 all_false = false;
1209 break;
1210 }
1211 }
1212 if (all_false)
1213 return ProverOutcome::False;
1214 }
1215 /*
1216 * Iterative deepening loop ends here.
1217 */
1218 return ProverOutcome::PathLenLimit;
1219}
1220//----------------------------------------------------------------------
1221vector<pair<string, vector<size_t>>> StackProver::get_internal_proof() const {
1223}
1224//----------------------------------------------------------------------
1225void StackProver::show_stack() {
1226 cout << "--------------------------------------------------------" << endl;
1227 cout << "Stack:" << endl;
1228 cout << "--------------------------------------------------------" << endl;
1229 for (auto s : stack) {
1230 cout << s << endl;
1231 }
1232 cout << "--------------------------------------------------------" << endl;
1233}
1234//----------------------------------------------------------------------
1235void StackProver::show_right_stack() {
1236 cout << "--------------------------------------------------------" << endl;
1237 cout << "Right Stack:" << endl;
1238 cout << "--------------------------------------------------------" << endl;
1239 for (auto s : right_branch_stack) {
1240 cout << s << endl;
1241 }
1242 cout << "--------------------------------------------------------" << endl;
1243}
1244//----------------------------------------------------------------------
1245void StackProver::show_statistics() const {
1246 verbose_print::VPrint show(params::verbosity);
1247 show(1, string("Reductions: "));
1248 show(1, std::to_string(reductions_tried));
1249 show(1, string(" Extensions: "));
1250 show(1, std::to_string(extensions_tried));
1251 show(1, string(" Lemmata: "));
1252 show(1, std::to_string(lemmata_tried));
1253 show(1, string(" Right branches: "));
1254 show(1, std::to_string(right_branches_started), true);
1255}
1256//----------------------------------------------------------------------
1257ostream& operator<<(ostream& out, const StackProver& p) {
1258 out << "Current state of the RecursiveProver object" << endl;
1259 out << "-------------------------------------------" << endl << endl;
1260 out << p.var_index << endl;
1261 out << p.fun_index << endl;
1262 out << p.term_index << endl;
1263 out << p.path << endl;
1264 out << p.matrix << endl;
1265 return out;
1266}
Representation of clauses.
Definition Clause.hpp:52
bool empty() const
Straightforward get method.
Definition Clause.hpp:82
Clause make_copy_with_new_vars(VariableIndex &, TermIndex &) const
Make a copy of an entire clause, introducing new variables.
Definition Clause.cpp:98
void add_lit(const Literal &)
Add a literal, making sure you don't duplicate.
Definition Clause.cpp:87
size_t size() const
Straightforward get method.
Definition Clause.hpp:78
string to_string(bool=false) const
Convert to a string.
Definition Clause.cpp:202
void drop_literal(LitNum)
Get rid of the specified Literal.
Definition Clause.cpp:135
Basic representation of functions.
Definition Function.hpp:54
Arity get_arity() const
Most basic access function.
Definition Function.hpp:89
string get_name() const
Most basic access function.
Definition Function.hpp:85
Arity find_minimum_arity() const
Find the smallest arity appearing for any Function in the index.
size_t get_size() const
Self-explanatory.
Arity find_maximum_arity() const
Find the largest arity appearing for any Function in the index.
bool tick()
Definition Interval.hpp:54
Representation of the lemma list.
Definition Lemmata.hpp:49
void find_initial_lemmata(vector< InferenceItem > &, Clause &)
Find all lemmata that are applicable, but only for the initial Literal in a Clause.
Definition Lemmata.cpp:33
void find_all_lemmata(vector< InferenceItem > &, Clause &)
Find all lemmata that are applicable, given a Clause.
Definition Lemmata.cpp:56
void push_back(const Literal &)
Self-explanatory.
Definition Lemmata.cpp:28
Basic representation of literals, bundling together (pointers to) a Predicate, a collection of argume...
Definition Literal.hpp:50
void move_equals_to_start()
Self-explanatory.
Definition Matrix.cpp:167
ClauseNum get_num_clauses() const
Straightforward get method.
Definition Matrix.hpp:191
string make_LaTeX(bool=false) const
Make a usable LaTeX representation.
Definition Matrix.cpp:257
void add_clause(Clause &, string="")
Add a Clause to the Matrix and update the index accordingly.
Definition Matrix.cpp:91
bool is_negative(size_t i) const
Is a particular Clause negative?.
Definition Matrix.hpp:211
void find_limited_extensions(Unifier &, vector< InferenceItem > &, Clause &, VariableIndex &, TermIndex &)
Find all possible extensions given a Clause, but only consider the first Literal in the Clause.
Definition Matrix.cpp:212
void find_all_extensions(Unifier &, vector< InferenceItem > &, Clause &, VariableIndex &, TermIndex &)
Find all possible extensions given a Clause, considering all Literals in the Clause.
Definition Matrix.cpp:222
bool is_conjecture(size_t i) const
Is a particular Clause a conjecture?
Definition Matrix.cpp:46
void write_to_prolog_file(const path &) const
Write to a file that can be read by Prolog.
Definition Matrix.cpp:270
void set_num_equals(uint32_t n)
Straightforward set method.
Definition Matrix.hpp:223
bool is_positive(size_t i) const
Is a particular Clause positive?.
Definition Matrix.hpp:205
void set_num_preds(size_t)
Make an empty index.
Definition Matrix.cpp:42
pair< bool, size_t > find_start() const
Use a simple heuristic to find a good start clause.
Definition Matrix.cpp:51
Basic representation of predicates: here just names, ids and arities.
Definition Predicate.hpp:51
Arity get_arity() const
Basic get method.
Definition Predicate.hpp:90
size_t get_num_preds() const
Basic get method.
Arity find_maximum_arity() const
Find the largest arity appearing in the index.
void make_Prolog(const path &)
Convert to a form suitable for use by the Prolog proof checker and write to a file.
void make_LaTeX(const path &, const path &, const string &)
Convert to LaTeX and store in the specified file.
vector< pair< string, vector< size_t > > > make_internal() const
Make a simple data structure representing the proof stack.
uint32_t length() const
Straightforward get method.
void push(const Literal &)
Add a new Literal to the Path.
void set_num_preds(size_t num_predicates)
Set method for num_predicates.
bool test_for_regularity(Clause &) const
Regularity test.
void find_limited_reductions(Unifier &, vector< InferenceItem > &, Clause &)
Given a Clause, find all possible reductions given the current Path, but only for the first Literal i...
void find_all_reductions(Unifier &, vector< InferenceItem > &, Clause &)
Given a Clause, find all possible reductions given the current Path.
Prover using a pair of stacks to conduct the proof search.
void set_num_preds(size_t)
Set the number of predicates.
bool depth_limit_reached
Self-explanatary.
void process_axiom_forward()
Start a right branch to continue from an axiom.
string status
Problem status, if found in input file.
void read_from_tptp_file(const string &, bool &, size_t &)
Obviously, reads a problem from a TPTP file.
vector< StartClauseStatus > results
This is populated by the StackProver::set_up_start_clauses method.
bool negated_conjecture_removed
Keep track of whether the parser simplified the conjecture away.
uint32_t lemmata_tried
We'll be keeping some simple statistics about the search process.
void lemmata_backtrack()
One of several different kinds of backtracking.
void reset_for_start()
Reset everything so that you can start from a specified start clause.
uint32_t current_depth_limit
Self-explanatary.
InferenceItem action
Stores the next action from the current StackItem.
void set_up_start_clauses()
The start clauses to use depend on the settings, and the settings can change.
size_t num_preds
How many prdicates does the problem of interest have?
bool fof_has_axioms
Keep track of whether the parser found that it's an FOF problem with axioms before simplification.
vector< StackItem > stack
Main stack: this is constructed by the search process and, if completed, represents a proof.
ProverResult go()
This runs the proof search from a given Start Move.
Matrix matrix
A copy of the matrix you're working with.
PredicateIndex pred_index
This class needs one of each kind of index to keep track of Variables, Terms etc.
vector< StackItem > right_branch_stack
We build the proof by trying the left branches of extensions first: this stack keeps track of the rig...
ProofPrinter proof_printer
You need one of these to print LaTeX output or any kind of proof certificate.
void extend_with_action()
Take a single inference (action) and update the stacks accordingly.
bool cnf_only
Keep track of whether there were any FOF formulas in the problem file.
SimplePath path
At any point in the search process this is a copy of the path for the current node in the proof being...
FunctionIndex fun_index
This class needs one of each kind of index to keep track of Variables, Terms etc.
void populate_stack_item()
Fill the vector of possible actions with everything available.
Lemmata lemmata
At any point in the search process this is a copy of the list of lemmata for the current node in the ...
uint32_t extensions_tried
We'll be keeping some simple statistics about the search process.
uint32_t current_depth
Self-explanatary.
void add_equality_axioms(Predicate *)
After reading a problem in which = and/or != appears, add the axioms for equality.
bool simplified_fof_has_axioms
Keep track of whether the parser found that it's an FOF problem with axioms after simplification.
bool conjecture_missing
Keep track of whether the parser found a conjecture in the problem file.
TermIndex term_index
This class needs one of each kind of index to keep track of Variables, Terms etc.
uint32_t proof_count
If we're searching for multiple proofs, keep count of which one this is.
bool conjecture_false
Keep track of whether the parser found the conjecture to be false.
VariableIndex var_index
This class needs one of each kind of index to keep track of Variables, Terms etc.
void backtrack_once()
Basic, single step backtrack on the stack.
bool depth_limited()
Test for the depth limit.
bool conjecture_true
Keep track of whether the parser found the conjecture to be true.
void left_extension_backtrack()
One of several different kinds of backtracking.
uint32_t right_branches_started
We'll be keeping some simple statistics about the search process.
bool backtrack
Are we moving up or down the stack?
chrono::steady_clock::time_point end_time
When do we stop because of a timeout?
vector< pair< string, vector< size_t > > > get_internal_proof() const
Get an internal representation of the proof stack.
StackItem * si
Pointer to the current StackItem.
Clause new_C
At any point in the search process this is a copy of the clause for the current node in the proof bei...
void right_extension_backtrack()
One of several different kinds of backtracking.
fs::path problem_path
Path for the problem of interest.
StackProver()
You only need a basic constructor.
bool use_timeout
Are we using a timeout?
void reduction_backtrack()
One of several different kinds of backtracking.
uint32_t reductions_tried
We'll be keeping some simple statistics about the search process.
SubstitutionStack sub_stack
There is a separate stack to make application and removal of substitutions straightforward.
verbose_print::VPrint show
Set up printing according to verbosity.
Unifier u
We need a single Unifier to use throught the process.
bool axiom() const
Test to see if you're at an axiom.
ProverOutcome prove()
Here is where the magic happens.
Interval output_interval
How often do you output updates about progress?
void apply() const
Apply a substitution everywhere.
void backtrack()
Remove variables from the stack, and remove substitutions as you go, as far back as the most recent b...
void push_all(Substitution &)
Take all the substitutions provided and add the corresponding variables to the stack.
Wrap up everything the TPTP parser needs to do inside a single class.
bool simplified_fof_has_axioms() const
Where there any axioms for an FOF problem after simplification?
string get_problem_status()
The parse tries to identify the problem status.
void clear()
Clear everything associated with the TPTP parser.
bool parse_tptp_from_file(const string &)
Main method to parse from a TPTP file to the data structures needed by the prover.
bool fof_conjecture_is_missing() const
Was there a conjecture clause in the problem file?
bool equality_used()
Did equality turn up anywhere in the parse?
bool conjecture_present() const
Did a conjecture turn up anywhere in the parse?
bool fof_has_axioms() const
Where there any axioms for an FOF problem before simplification?
bool fof_conjecture_is_false() const
Self-explanatory.
bool fof_conjecture_is_true() const
Self-explanatory.
Predicate * get_equals_predicate() const
If equality turned up anywhere in the parse it will have been turned into an actual Predicate,...
bool problem_is_cnf_only() const
Self-explanatory.
size_t number_of_fof_formulas() const
How many first-order formulas turned up in the parse?
bool fof_negated_conjecture_removed() const
Was there a conjecture clause that got simplified away?
General representation of terms.
Definition Term.hpp:62
Term * add_function_term(Function *, const vector< Term * > &)
Self-explanatory: add a Term containing a function to the index.
Definition TermIndex.cpp:73
Term * add_variable_term(Variable *)
Self-explanatory: add a Term containing a variable to the index.
Definition TermIndex.cpp:56
Basic representation of variables.
Definition Variable.hpp:58
Variable * add_named_var(const string &)
Add a variable with the specified name to the index.
void set_all_names_added()
Call this to indicate that only anonymous variables can now be created.
void backtrack()
Backtrack to the last marker.
void add_backtrack_point()
Add a backtrack point.
Simple addition of colour to strings and ostreams.
static string erase_line(uint8_t n)
Definition cursor.hpp:157
void nl(uint8_t, uint8_t=1)
Full representation of inferences, beyond just the name.
LitNum Lindex
The index of the literal within the clause being used.
LitNum Lprime
The index of the literal in C_2 being used.
Substitution sigma
A copy of the substitution that makes the rule applicable.
Literal L
The Literal that is used to make the inference.
ClauseNum C_2
For extensions, the number of the clause for which a fresh copy is being made.
InferenceItemType T
What kind of inference is this?
Stack items: each contains its own stack of possible next inferences.
Definition StackItem.hpp:51
void restrict_backtrack()
Adjust the collection of actions to limit backtracking.
Definition StackItem.cpp:51
SimplePath p
Each node in the proof tree is a tuple of clause, matrix, path, lemmata: this is the path.
Definition StackItem.hpp:65
vector< InferenceItem > actions
Actions available to try.
Definition StackItem.hpp:84
uint32_t depth
How deep in the proof tree are we?
Definition StackItem.hpp:88
size_t bt_restriction_index
Pointer that allows a right branch to know where to delete alternatives for restricted backtracking.
void set_this_action(const InferenceItem &inf_i)
Basic set method.
Lemmata l
Each node in the proof tree is a tuple of clause, matrix, path, lemmata: this is the lemmata.
Definition StackItem.hpp:70
Clause c
Each node in the proof tree is a tuple of clause, matrix, path, lemmata: this is the clause.
Definition StackItem.hpp:60
StackItemType item_type
What type of StackItem is this?
Definition StackItem.hpp:55
Structure containing all the command line and other options.
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.