Connect++ 0.7.0
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
TableauProof.cpp
1/*
2
3Copyright © 2023-26 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 "TableauProof.hpp"
26
27//------------------------------------------------------------------
28// TableauProofNode
29//------------------------------------------------------------------
30string TableauProofNode::path_to_tptp_string() {
31 string s("[");
32 vector<PathPair> p2(parent->p);
33
34 for (int i = p2.size() - 1; i >= 0; i--) {
35 if (i > 0) {
36 s += "t";
37 }
38 s += to_string(p2[i].first);
39 s += ":";
40 s += to_string(p2[i].second);
41 if (i > 0) {
42 s += ",";
43 }
44 }
45 s += "]";
46 return s;
47}
48//------------------------------------------------------------------
49string TableauProofNode::parent_to_tptp_string() {
50 string s("t");
51 PathPair p2(parent->p.back());
52 s += to_string(p2.first);
53 s += ":";
54 s += to_string(p2.second);
55 return s;
56}
57//------------------------------------------------------------------
58string TableauProofNode::make_path_string() {
59 string s;
60 if (!params::tptp_proof_show_paths) {
61 s += "parent(";
62 s += parent_to_tptp_string();
63 }
64 else {
65 s += "path(";
66 s += path_to_tptp_string();
67 }
68 s += ")";
69 return s;
70}
71//------------------------------------------------------------------
72string TableauProofNode::lemmas_to_string() {
73 string s;
74 for (size_t l : lemma_list) {
75 s += to_string(l);
76 s += "\\ ";
77 }
78 return s;
79 }
80//------------------------------------------------------------------
81// TableauProof
82//------------------------------------------------------------------
83void TableauProof::build() {
84 for (size_t i = 0; i < stack_size; i++) {
85 StackItem si ((*stack_p)[i]);
86 Clause C;
87 LitNum L;
88 ClauseNum C2;
89 LitNum L2;
90 LitNum P;
91 size_t lemma_index;
92 Literal next_node_literal;
93 Literal complementary_literal;
94 Literal negated_literal;
95 Literal removed_literal;
96 size_t path_index;
97 TableauProofNode* new_node;
98 TableauProofNode* connection_node;
99 TableauProofNode* false_node;
100 Substitution s;
101 Unifier u;
102 size_t new_depth;
103 UnificationOutcome u_result;
104 Literal lemma_literal;
105 switch (si.item_type) {
106 case StackItemType::Start:
107 matrix_p->make_copy_with_new_unique_vars(si.this_action.C_2, C, *vi, *ti);
108 root = new TableauProofNode(C);
109 current_node = root;
110 current_node->p.push_back(PathPair(0,0));
111 current_node->t_child = ++t_count;
112 current_node->l_child++;
113 current_node->matrix_id = si.this_action.C_2;
114 clauses_used_in_proof.insert(matrix_p->get_name(si.this_action.C_2));
115 break;
116 case StackItemType::Axiom:
117 break;
118 case StackItemType::Reduction:
119 L = si.this_action.Lindex;
120 P = si.this_action.index_in_path;
121
122 // Here we only need to remove the literal...
123 next_node_literal = current_node->c_remaining[L];
124 current_node->c_remaining.drop_literal(L);
125
126 // ...make reduction and $false nodes ...
127 connection_node = new TableauProofNode(next_node_literal);
128 connection_node->parent = current_node;
129 connection_node->type = TableauNodeType::Reduction;
130 connection_node->depth = current_node->depth + 1;
131
132 connection_node->lemma = new TableauProofNode(next_node_literal);
133 connection_node->lemma->type = TableauNodeType::Lemma;
134 connection_node->lemma->lemma_number = ++lemma_count;
135 connection_node->lemma->parent = connection_node;
136
137 connection_node->lemma_list = current_node->lemma_list;
138 current_node->lemma_list.push_back(lemma_count);
139 connection_node->lemma_list_p = current_node->lemma_list_p;
140 current_node->lemma_list_p.push_back(connection_node->lemma);
141
142 connection_node->t = current_node->t_child;
143 connection_node->l = current_node->l_child;
144 connection_node->p = current_node->p;
145 connection_node->p.push_back(PathPair(connection_node->t,
146 connection_node->l));
147 current_node->l_child++;
148
149 false_node = new TableauProofNode();
150 false_node->parent = connection_node;
151 false_node->depth = current_node->depth + 2;
152 false_node->t = ++t_count;
153 false_node->p = connection_node->p;
154 false_node->p.push_back(PathPair(false_node->t, 0));
155 false_node->needs_reduction_link = true;
156 false_node->reduction_node = current_node->p[P+1];
157
158 complementary_literal = current_node->path[P];
159 negated_literal = complementary_literal;
160 negated_literal.invert();
161 u_result = u(negated_literal, next_node_literal);
162 if (u_result != UnificationOutcome::Succeed ||
163 !next_node_literal.is_compatible_with(&negated_literal)) {
164 cerr << "There's a problem with your reduction unification." << endl;
165 exit(EXIT_FAILURE);
166 }
167 else {
168 false_node->sub = u.get_substitution();
169 }
170 current_node->children.push_back(connection_node);
171 connection_node->children.push_back(false_node);
172 break;
173 case StackItemType::LeftBranch:
174 L = si.this_action.Lindex;
175 C2 = si.this_action.C_2;
176 L2 = si.this_action.Lprime;
177
178 // Remove from c_remaining the next literal to make a node for.
179 next_node_literal = current_node->c_remaining[L];
180 current_node->c_remaining.drop_literal(L);
181
182 right_stack.push_back(current_node->depth);
183
184 // Make the clause copy for the new node.
185 matrix_p->make_copy_with_new_unique_vars(C2, C, *vi, *ti);
186 //cout << C << endl;
187
188 // Get the complementary literal and find the unification.
189 complementary_literal = C[L2];
190 negated_literal = complementary_literal;
191 negated_literal.invert();
192 u_result = u(negated_literal, next_node_literal);
193
194 // Make a new node. removed_literal is the one needed
195 // for the child making a connection.
196 new_node = new TableauProofNode(C, next_node_literal);
197 if (u_result != UnificationOutcome::Succeed ||
198 !next_node_literal.is_compatible_with(&negated_literal)) {
199 cerr << "There's a problem with your extension unification." << endl;
200 exit(EXIT_FAILURE);
201 }
202 else {
203 new_node->sub = u.get_substitution();
204 }
205 new_node->parent = current_node;
206 new_node->t = current_node->t_child;
207 new_node->t_child = ++t_count;
208 removed_literal = new_node->c_remaining[L2];
209 new_node->c_remaining.drop_literal(L2);
210 new_node->depth = current_node->depth + 1;
211 new_node->path = current_node->path;
212 new_node->path.push_back(next_node_literal);
213
214 new_node->lemma = new TableauProofNode(next_node_literal);
215 new_node->lemma->type = TableauNodeType::Lemma;
216 new_node->lemma->lemma_number = ++lemma_count;
217 new_node->lemma->parent = new_node;
218
219 new_node->lemma_list = current_node->lemma_list;
220 current_node->lemma_list.push_back(lemma_count);
221 new_node->lemma_list_p = current_node->lemma_list_p;
222 current_node->lemma_list_p.push_back(new_node->lemma);
223
224 new_node->l = current_node->l_child;
225 new_node->l_child = 1;
226 new_node->matrix_id = C2;
227 current_node->l_child++;
228 new_node->p = current_node->p;
229 new_node->p.push_back(PathPair(new_node->t, new_node->l));
230
231 // Now set up the new child.
232 current_node->children.push_back(new_node);
233
234 // Now add the connection and $false nodes.
235 connection_node = new TableauProofNode(complementary_literal);
236 connection_node->parent = new_node;
237 connection_node->depth = current_node->depth + 2;
238
239 connection_node->t = t_count;
240 connection_node->l = new_node->l_child;
241 new_node->l_child++;
242 connection_node->p = new_node->p;
243 connection_node->p.push_back(PathPair(connection_node->t,
244 connection_node->l));
245
246 false_node = new TableauProofNode();
247 false_node->parent = connection_node;
248 false_node->depth = current_node->depth + 3;
249
250 false_node->t = ++t_count;
251
252 connection_node->children.push_back(false_node);
253 new_node->children.push_back(connection_node);
254
255 current_node = new_node;
256 clauses_used_in_proof.insert(matrix_p->get_name(C2));
257 break;
258 case StackItemType::RightBranch:
259 new_depth = right_stack.back();
260 right_stack.pop_back();
261 while (current_node->depth != new_depth) {
262 current_node = current_node->parent;
263 }
264 break;
265 case StackItemType::Lemmata:
266 L = si.this_action.Lindex;
267 lemma_index = si.this_action.index_in_lemmata;
268
269 next_node_literal = current_node->c_remaining[L];
270 current_node->c_remaining.drop_literal(L);
271
272 // ...make reduction and $false nodes ...
273 connection_node = new TableauProofNode(next_node_literal);
274 connection_node->parent = current_node;
275 connection_node->depth = current_node->depth + 1;
276 connection_node->t = current_node->t_child;
277 connection_node->l = current_node->l_child;
278 connection_node->p = current_node->p;
279 connection_node->p.push_back(PathPair(connection_node->t,
280 connection_node->l));
281
282 current_node->l_child++;
283 current_node->children.push_back(connection_node);
284
285 lemma_literal = current_node->lemma_list_p[lemma_index]->lit;
286 new_node = new TableauProofNode(lemma_literal);
287 new_node->type = TableauNodeType::LemmaExtension;
288 new_node->parent = connection_node;
289 new_node->t = ++t_count;
290 new_node->l = 1;
291 new_node->parent = connection_node;
292 new_node->lemma_reduction_node = current_node->lemma_list[lemma_index];
293 new_node->needs_lemma_link = true;
294 new_node->p = connection_node->p;
295 new_node->p.push_back(PathPair(new_node->t,
296 new_node->l));
297
298 // Possibly not needed, but include for now. Check unification works
299 // and store result. Remember not to apply it though!
300 //lemma_literal.invert();
301 u_result = u(next_node_literal, lemma_literal);
302 if (u_result != UnificationOutcome::Succeed ||
303 !next_node_literal.is_compatible_with(&lemma_literal)) {
304 cerr << "There's a problem with your lemma unification." << endl;
305 exit(EXIT_FAILURE);
306 }
307 else {
308 new_node->sub = u.get_substitution();
309 }
310 u.backtrack();
311
312 current_node->lemma_list_p[lemma_index]->lemma_is_used=true;
313
314 connection_node->children.push_back(new_node);
315
316 false_node = new TableauProofNode();
317 false_node->parent = new_node;
318 false_node->depth = current_node->depth + 2;
319 false_node->t = ++t_count;
320 false_node->p = connection_node->p;
321 false_node->p.push_back(PathPair(false_node->t, 0));
322
323 new_node->children.push_back(false_node);
324 break;
325 default:
326 cerr << "Something is really wrong..." << endl;
327 break;
328 }
329
330 }
331}
332//------------------------------------------------------------------
333string TableauProof::tableau_to_tptp_string(TableauProofNode* p) const {
334 string s;
335 string s2;
336 size_t lemma_b1;
337 size_t lemma_b2;
338 Literal inverted_literal;
339 Clause reordered_clause;
340 bool subbed = !params::tptp_proof_no_subs;
341 switch(p->type) {
342 case TableauNodeType::Start:
343 s += "cnf(t1, plain, ";
344 for (TableauProofNode* q : p->children) {
345 reordered_clause.add_lit(q->lit);
346 }
347 s += reordered_clause.to_tptp_string(subbed);
348 s += ",\n inference(start, [status(thm), parent(0:0)], [";
349 s += matrix_p->get_name(p->matrix_id);
350 s += "]) ).";
351 s += "\n\n";
352 for (TableauProofNode* q : p->children) {
353 s += tableau_to_tptp_string(q);
354 }
355 break;
356 case TableauNodeType::Extension:
357 s += "cnf(t";
358 s += to_string(p->t_child);
359 s += ", plain, ";
360 for (TableauProofNode* q : p->children) {
361 reordered_clause.add_lit(q->lit);
362 }
363 s += reordered_clause.to_tptp_string(subbed);
364 s += ",\n inference(extension, [status(thm), ";
365 s += p->children[0]->make_path_string();
366 if (params::tptp_proof_show_subs && p->sub.size() > 0) {
367 s += ", ";
368 s += p->sub.to_tptp_string(subbed);
369 }
370 s += "], [";
371 s += matrix_p->get_name(p->matrix_id);
372 s += "]) ).";
373 s += "\n\n";
374 for (TableauProofNode* q : p->children) {
375 s += tableau_to_tptp_string(q);
376 }
377 s += tableau_to_tptp_string(p->lemma);
378 break;
379 case TableauNodeType::Connection:
380 if (p->children[0]->type != TableauNodeType::LemmaExtension) {
381 s += "cnf(t";
382 s += to_string(p->children[0]->t);
383 s += ", plain, $false,\n";
384 s += " inference(connection, [status(thm), ";
385 s += p->children[0]->make_path_string();
386 s += "], [t";
387 s += to_string(p->t);
388 s += ":";
389 s += to_string(p->l);
390 s += ",t";
391 s += to_string(p->parent->t);
392 s += ":";
393 s += to_string(p->parent->l);
394 s += "]) ).";
395 s += "\n\n";
396 }
397 else {
398 s += tableau_to_tptp_string(p->children[0]);
399 }
400 break;
401 case TableauNodeType::Reduction:
402 s += "cnf(t";
403 s += to_string(p->children[0]->t);
404 s += ", plain, $false,\n";
405 s += " inference(reduction, [status(thm), ";
406 s += p->children[0]->make_path_string();
407 if (params::tptp_proof_show_subs && p->sub.size() > 0) {
408 s += ", ";
409 s += p->sub.to_tptp_string(subbed);
410 }
411 s += "], [t";
412 s += to_string(p->t);
413 s += ":";
414 s += to_string(p->l);
415 s += ",t";
416 s += to_string(p->children[0]->reduction_node.first);
417 s += ":";
418 s += to_string(p->children[0]->reduction_node.second);
419 s += "]) ).";
420 s += "\n\n";
421 s += tableau_to_tptp_string(p->lemma);
422 break;
423 case TableauNodeType::Lemma:
424 if (p != nullptr && p->lemma_is_used) {
425 s += "cnf(l";
426 s += to_string(p->lemma_number);
427 s += ", lemma, ";
428 inverted_literal = p->lit;
429 inverted_literal.invert();
430 s += inverted_literal.to_tptp_string(subbed);
431 s += ",\n inference(lemma, [status(cth), ";
432 s += p->make_path_string();
433 s += ", below(";
434 lemma_b1 = p->parent->parent->t;
435 lemma_b2 = p->parent->parent->l;
436 if (lemma_b1 != 0) {
437 s += "t";
438 }
439 s += to_string(lemma_b1);
440 s += ":";
441 s += to_string(lemma_b2);
442 s += ")], [t";
443 s += to_string(p->parent->t);
444 s += ":";
445 s += to_string(p->parent->l);
446 s += "]) ).";
447 s += "\n\n";
448 }
449 break;
450 case TableauNodeType::LemmaExtension:
451 s += "cnf(t";
452 s += to_string(p->t);
453 s += ", plain, ";
454 inverted_literal = p->lit;
455 inverted_literal.invert();
456 s += inverted_literal.to_tptp_string(subbed);
457 s += ",\n inference(lemma_extension, [status(thm), ";
458 s += p->make_path_string();
459 //if (params::tptp_proof_show_subs && p->sub.size() > 0) {
460 // s += ", ";
461 // s += p->sub.to_tptp_string(subbed);
462 //}
463 s += "], [l";
464 s += to_string(p->lemma_reduction_node);
465 s += ":";
466 s += to_string(1);
467 s += "]) ).";
468 s += "\n\n";
469
470 s += "cnf(t";
471 s += to_string(p->children[0]->t);
472 s += ", plain, $false,\n";
473 s += " inference(connection, [status(thm), ";
474 s += p->children[0]->make_path_string();
475 s += "], [t";
476 s += to_string(p->t);
477 s += ":";
478 s += to_string(p->l);
479 s += ",t";
480 s += to_string(p->parent->t);
481 s += ":";
482 s += to_string(p->parent->l);
483 s += "]) ).";
484 s += "\n\n";
485 break;
486 case TableauNodeType::False:
487 break;
488 default:
489 break;
490 }
491 return s;
492}
493//------------------------------------------------------------------
494string TableauProof::lit_t_l_to_LaTeX(TableauProofNode* _p) const {
495 string s;
496 s += "{$";
497 Literal literal = _p->lit;
498 if (_p->type == TableauNodeType::LemmaExtension) {
499 literal.invert();
500 }
501 s += literal.make_LaTeX(params::sub_LaTeX_proof);
502 s += "$";
503 if (params::latex_tableau_subs && _p->sub.size() > 0) {
504 s += "\\\\ $";
505 s += _p->sub.make_LaTeX(params::sub_LaTeX_proof);
506 s += "$";
507 }
508 s += "\\\\ $[$t";
509 s += to_string(_p->t);
510 s += ":";
511 s += to_string(_p->l);
512 s += "$]$";
513
514 s += "}, align=center, name=t";
515 s += to_string(_p->t);
516 s += "-";
517 s += to_string(_p->l);
518 return s;
519}
520//------------------------------------------------------------------
521string TableauProof::tableau_to_LaTeX(TableauProofNode* p) const {
522 string s;
523 Literal inverted_literal;
524 switch(p->type) {
525 case TableauNodeType::Start:
526 s += "[{[0:0]}, name=0-0";
527 for (TableauProofNode* q : p->children)
528 s += tableau_to_LaTeX(q);
529 s += "]";
530 break;
531 case TableauNodeType::Extension:
532 case TableauNodeType::Reduction:
533 s += "[";
534 s += lit_t_l_to_LaTeX(p);
535 for (TableauProofNode* q : p->children)
536 s += tableau_to_LaTeX(q);
537 if (p->lemma != nullptr)
538 s += tableau_to_LaTeX(p->lemma);
539 s += "]";
540 break;
541 case TableauNodeType::Connection:
542 case TableauNodeType::LemmaExtension:
543 s += "[";
544 s += lit_t_l_to_LaTeX(p);
545 for (TableauProofNode* q : p->children)
546 s += tableau_to_LaTeX(q);
547 s += "]";
548 break;
549 case TableauNodeType::Lemma:
550 if (p->lemma_is_used) {
551 s += "[{$";
552 inverted_literal = p->lit;
553 inverted_literal.invert();
554 s += inverted_literal.make_LaTeX(params::sub_LaTeX_proof);
555 s += "$ \\\\ $[$l";
556 s += to_string(p->lemma_number);
557 s += "$]$}, align=center, ellipse, name=l";
558 s += to_string(p->lemma_number);
559 s += "]";
560 }
561 break;
562 case TableauNodeType::False:
563 s += "[{$\\ensuremath{\\mathtt{\\$false}}$ \\\\ $[$t";
564 s += to_string(p->t);
565 s += "$]$}, align=center, name=t";
566 s += to_string(p->t);
567 s += "]";
568 break;
569 default:
570 break;
571 }
572 if (p->needs_reduction_link) {
573 s += "{ \\draw[<-,dotted] () to[out=south,in=south] (t";
574 s += to_string(p->reduction_node.first);
575 s += "-";
576 s += to_string(p->reduction_node.second);
577 s += ");}";
578 }
579 if (p->needs_lemma_link) {
580 s += "{ \\draw[<-,dashed] () to[out=south west,in=east] (l";
581 s += to_string(p->lemma_reduction_node);
582 s += ");}";
583 }
584 return s;
585}
586//------------------------------------------------------------------
587string TableauProof::make_LaTeX() const {
588 string s;
589 s += "\\begin{forest}";
590 s += "for tree=draw, for tree=rounded corners=5mm, for tree=thick";
591 s += tableau_to_LaTeX(root);
592 s += "\\end{forest}";
593 return s;
594}
595//------------------------------------------------------------------
596pair<string, string> TableauProof::lit_t_l_to_Graphviz(TableauProofNode* _p,
597 const string& _parent) const {
598 string s;
599 string name("\"t");
600 Literal literal = _p->lit;
601 if (_p->type == TableauNodeType::LemmaExtension) {
602 literal.invert();
603 }
604 name += to_string(_p->t);
605 name += "-";
606 name += to_string(_p->l);
607 name += "\"";
608 s += name;
609 s += " [style=filled, fillcolor=mintcream, fontname=Courier label=\"";
610 s += literal.make_Graphviz(params::sub_Graphviz_proof);
611 if (params::graphviz_tableau_subs && _p->sub.size() > 0) {
612 s += "\n";
613 s += _p->sub.make_Graphviz(params::sub_Graphviz_proof);
614 }
615 s += "\n[";
616 s += to_string(_p->t);
617 s += ":";
618 s += to_string(_p->l);
619 s += "]";
620 s += "\"];\n";
621 s += _parent;
622 s += " -> ";
623 s += name;
624 s += " ;\n";
625 return pair<string, string>(name, s);
626}
627//------------------------------------------------------------------
628string TableauProof::tableau_to_Graphviz(TableauProofNode* p,
629 const string& _parent) const {
630 string s;
631 pair<string, string> sp;
632 Literal inverted_literal;
633 string name;
634 switch(p->type) {
635 case TableauNodeType::Start:
636 s += "\"0-0\" [fontname=Courier label=\"[0:0]\"];\n";
637 for (TableauProofNode* q : p->children)
638 s += tableau_to_Graphviz(q, "\"0-0\"");
639 break;
640 case TableauNodeType::Extension:
641 case TableauNodeType::Reduction:
642 sp = lit_t_l_to_Graphviz(p, _parent);
643 name = sp.first;
644 s += sp.second;
645 for (TableauProofNode* q : p->children)
646 s += tableau_to_Graphviz(q, sp.first);
647 if (p->lemma != nullptr)
648 s += tableau_to_Graphviz(p->lemma, sp.first);
649 break;
650 case TableauNodeType::Connection:
651 case TableauNodeType::LemmaExtension:
652 sp = lit_t_l_to_Graphviz(p, _parent);
653 name = sp.first;
654 s += sp.second;
655 for (TableauProofNode* q : p->children)
656 s += tableau_to_Graphviz(q, sp.first);
657 break;
658 case TableauNodeType::Lemma:
659 if (p->lemma_is_used) {
660 inverted_literal = p->lit;
661 inverted_literal.invert();
662 name += "\"l";
663 name += to_string(p->lemma_number);
664 name += "\"";
665 s += name;
666 s += " [style=filled, fillcolor=lightblue, shape=box, fontname=Courier label=\"";
667 s += inverted_literal.make_Graphviz(params::sub_Graphviz_proof);
668 s += "\nl";
669 s += to_string(p->lemma_number);
670 s += "\"];\n";
671 s += _parent;
672 s += "->";
673 s += name;
674 s += ";\n";
675 }
676 break;
677 case TableauNodeType::False:
678 name += "\"t";
679 name += to_string(p->t);
680 name += "\"";
681 s += name;
682 s += " [style=filled, fillcolor=lightcyan, fontname=Courier label=\"$false\nt";
683 s += to_string(p->t);
684 s += "\"];\n";
685 s += _parent;
686 s += "->";
687 s += name;
688 s += ";\n";
689 break;
690 default:
691 break;
692 }
693 if (p->needs_reduction_link) {
694 s += "\"t";
695 s += to_string(p->reduction_node.first);
696 s += "-";
697 s += to_string(p->reduction_node.second);
698 s += "\" -> ";
699 s += name;
700 s += " [style=dashed];\n";
701 }
702 if (p->needs_lemma_link) {
703 s += "\"l";
704 s += to_string(p->lemma_reduction_node);
705 s += "\" -> ";
706 s += name;
707 s += " [style=dotted];\n";
708 }
709 return s;
710}
711//------------------------------------------------------------------
712string TableauProof::make_Graphviz(const path& problem_path) const {
713 string s;
714 s += "digraph \"";
715 s += problem_path.filename().string();
716 s += "\" {\n";
717 s += "size=\"";
718 s += std::to_string(params::graphviz_width);
719 s += ",";
720 s += std::to_string(params::graphviz_height);
721 s += "\";\n";
722 s += "labelloc=\"t\"\nlabel=\"Connect++ proof for: ";
723 s += problem_path.filename().string();
724 s += "\";\n";
725 s += tableau_to_Graphviz(root);
726 s += "\n}\n";
727 return s;
728}
729
730
731
Clause
Representation of clauses.
Definition Clause.hpp:52
Clause::to_tptp_string
string to_tptp_string(bool=false) const
Convert to a string that is compatible with the TPTP.
Definition Clause.cpp:272
Clause::add_lit
void add_lit(const Literal &)
Add a literal, making sure you don't duplicate.
Definition Clause.cpp:96
Clause::drop_literal
void drop_literal(LitNum)
Get rid of the specified Literal.
Definition Clause.cpp:168
Literal
Basic representation of literals, bundling together (pointers to) a Predicate, a collection of argume...
Definition Literal.hpp:50
Literal::make_LaTeX
string make_LaTeX(bool=false) const
Make a useable LaTeX version.
Definition Literal.cpp:253
Literal::is_compatible_with
bool is_compatible_with(const Literal *) const
Literals can only be unified if the polarity and actual predicate are the same.
Definition Literal.cpp:84
Literal::to_tptp_string
string to_tptp_string(bool=false) const
Convert to a string in a format compatible with the TPTP.
Definition Literal.cpp:225
Literal::invert
void invert()
Basic manipulation - entirely self-explanatory.
Definition Literal.hpp:107
Literal::make_Graphviz
string make_Graphviz(bool=false) const
Make a useable Graphviz version.
Definition Literal.cpp:270
Matrix::get_name
string get_name(size_t _i) const
Retrieve the name of one of the clauses in the matrix.
Definition Matrix.hpp:333
Matrix::make_copy_with_new_unique_vars
void make_copy_with_new_unique_vars(size_t, Clause &, VariableIndex &, TermIndex &) const
Make a new copy of a clause in the matrix.
Definition Matrix.cpp:327
Substitution
General representation of a substitution.
Definition Substitution.hpp:57
Substitution::make_LaTeX
string make_LaTeX(bool=false) const
Make a useable LaTeX representation.
Definition Substitution.cpp:53
Substitution::size
size_t size() const
Trivial get method.
Definition Substitution.hpp:74
Substitution::to_tptp_string
string to_tptp_string(bool=false) const
Make a string representation in the TPTP format.
Definition Substitution.cpp:39
Substitution::make_Graphviz
string make_Graphviz(bool=false) const
Make a useable Graphviz representation.
Definition Substitution.cpp:66
TableauProof::clauses_used_in_proof
unordered_set< string > clauses_used_in_proof
When you produce the proof you want to know which clauses were actually used so that you can limit th...
Definition TableauProof.hpp:262
TableauProofNode
Class for representing nodes in a tableau proof.
Definition TableauProof.hpp:53
TableauProofNode::needs_lemma_link
bool needs_lemma_link
Used in producing LaTex output to indicate that a link has to be added.
Definition TableauProof.hpp:118
TableauProofNode::matrix_id
size_t matrix_id
Some nodes need to produce output referring to a clause in the matrix.
Definition TableauProof.hpp:89
TableauProofNode::sub
Substitution sub
Substitution associated with reduction, extension or lemma.
Definition TableauProof.hpp:109
TableauProofNode::l
LitNum l
A node in the tableau is identified by ‘t : l’.
Definition TableauProof.hpp:70
TableauProofNode::t_child
ClauseNum t_child
Nodes maintain the t value for children.
Definition TableauProof.hpp:65
TableauProofNode::reduction_node
PathPair reduction_node
Which node is associated with this one?
Definition TableauProof.hpp:127
TableauProofNode::t
ClauseNum t
A node in the tableau is identified by ‘t : l’.
Definition TableauProof.hpp:61
TableauProofNode::path
vector< Literal > path
Paths are stored both as collections of literals and collections of t:l pairs. Both are needed for co...
Definition TableauProof.hpp:105
TableauProofNode::lemma_list
vector< size_t > lemma_list
Lemma lists are kept as both numbers and pointer to other nodes. Both are needed.
Definition TableauProof.hpp:136
TableauProofNode::lemma_is_used
bool lemma_is_used
Used in producing LaTeX output so that only used lemmas are displayed.
Definition TableauProof.hpp:150
TableauProofNode::children
vector< TableauProofNode * > children
Children of this node.
Definition TableauProof.hpp:154
TableauProofNode::p
vector< PathPair > p
Paths are stored both as collections of literals and collections of t:l pairs. Both are needed for co...
Definition TableauProof.hpp:99
TableauProofNode::needs_reduction_link
bool needs_reduction_link
Used in producing LaTex output to indicate that a link has to be added.
Definition TableauProof.hpp:123
TableauProofNode::lemma
TableauProofNode * lemma
Lemma associated with a reduction or extension.
Definition TableauProof.hpp:141
TableauProofNode::lit
Literal lit
Literal associated with the node.
Definition TableauProof.hpp:93
TableauProofNode::l_child
LitNum l_child
Nodes maintain the l value for children.
Definition TableauProof.hpp:74
TableauProofNode::depth
size_t depth
Where are we in the tree? Used for backtracking.
Definition TableauProof.hpp:113
TableauProofNode::lemma_reduction_node
size_t lemma_reduction_node
Which node is associated with this one?
Definition TableauProof.hpp:131
TableauProofNode::lemma_number
size_t lemma_number
Numerical identifier for a lemma.
Definition TableauProof.hpp:145
TableauProofNode::c_remaining
Clause c_remaining
Starts equal to c. At each step in constructing the tableau a single literal is dealt with in a child...
Definition TableauProof.hpp:84
Unifier
Wrap up various applications of unificiation into a single class: all the unification you need to do ...
Definition Unifier.hpp:89
Unifier::backtrack
void backtrack()
Apply the backtracking process to the substitution that has been constructed.
Definition Unifier.cpp:195
Unifier::get_substitution
Substitution get_substitution() const
Trivial get methods for the result.
Definition Unifier.hpp:122
StackItem
Stack items: each contains its own material for generating possible next inferences.
Definition StackItem.hpp:54