TableauProof Class Reference

Class for representing a tableau proof in a format that allows extraction of TPTP-format proofs, LaTeX representations and so on. More...

#include <TableauProof.hpp>

Collaboration diagram for TableauProof:

Public Member Functions
	TableauProof (Stack *_stack_p, Matrix *_matrix_p, VariableIndex *_vi, TermIndex *_ti)
void	build ()
string	make_tptp ()
string	make_LaTeX () const
string	make_Graphviz (const path &) const
void	show_clauses_used_in_proof ()
unordered_set< string >	get_clauses_used_in_proof () const

Private Member Functions
string	tableau_to_LaTeX (TableauProofNode *) const
string	tableau_to_Graphviz (TableauProofNode *, const string &="") const
string	tableau_to_tptp_string (TableauProofNode *) const
string	lit_t_l_to_LaTeX (TableauProofNode *) const
pair< string, string >	lit_t_l_to_Graphviz (TableauProofNode *, const string &) const

Private Attributes
Stack *	stack_p
size_t	stack_size
Matrix *	matrix_p
VariableIndex *	vi
TermIndex *	ti
size_t	t_count
size_t	lemma_count
TableauProofNode *	root
TableauProofNode *	current_node
vector< size_t >	right_stack
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 the printing of the clause conversion process to the parts that are actually needed.

Detailed Description

Class for representing a tableau proof in a format that allows extraction of TPTP-format proofs, LaTeX representations and so on.

Some of the methods build the data structure from the stack used by the theorem prover; some convert it to other formats. Doing this directly from the stack representation is actually not a particularly straightforward conversion, hence the use of a separate class rather than just trying to put it in ProofPrinter.

Building this thing is, to be honest, not a straightforward exercise. You should think carefully before messing with the "build" method.

Definition at line 242 of file TableauProof.hpp.

Constructor & Destructor Documentation

TableauProof()

TableauProof::TableauProof ( Stack * _stack_p, Matrix * _matrix_p, VariableIndex * _vi, TermIndex * _ti )

inline

Definition at line 271 of file TableauProof.hpp.

    : stack_p(_stack_p)
    , matrix_p(_matrix_p)
    , vi(_vi)
    , ti(_ti)
    , t_count(0)
    , lemma_count(0)
    , root(nullptr)
    , current_node(nullptr)
    , right_stack()
    , clauses_used_in_proof()
    {
        stack_size = _stack_p->size();
    }

~TableauProof()

TableauProof::~TableauProof ( )

inline

Definition at line 286 of file TableauProof.hpp.

{ delete root; }

Member Function Documentation

build()

void TableauProof::build

(

)

Definition at line 83 of file TableauProof.cpp.

                         {
    for (size_t i = 0; i < stack_size; i++) {
        StackItem si ((*stack_p)[i]);
        Clause C;
        LitNum L;
        ClauseNum C2;
        LitNum L2;
        LitNum P;
        size_t lemma_index;
        Literal next_node_literal;
        Literal complementary_literal;
        Literal negated_literal;
        Literal removed_literal;
        size_t path_index;
        TableauProofNode* new_node;
        TableauProofNode* connection_node;
        TableauProofNode* false_node;
        Substitution s;
        Unifier u;
        size_t new_depth;
        UnificationOutcome u_result;
        Literal lemma_literal;
        switch (si.item_type) {
            case StackItemType::Start:
                matrix_p->make_copy_with_new_unique_vars(si.this_action.C_2, C, *vi, *ti);
                root = new TableauProofNode(C);
                current_node = root;
                current_node->p.push_back(PathPair(0,0));
                current_node->t_child = ++t_count;
                current_node->l_child++;
                current_node->matrix_id = si.this_action.C_2;
                clauses_used_in_proof.insert(matrix_p->get_name(si.this_action.C_2));
                break;
            case StackItemType::Axiom:
                break;
            case StackItemType::Reduction:
                L = si.this_action.Lindex;
                P = si.this_action.index_in_path;
                
                // Here we only need to remove the literal...
                next_node_literal = current_node->c_remaining[L];
                current_node->c_remaining.drop_literal(L);
                
                // ...make reduction and $false nodes ...
                connection_node = new TableauProofNode(next_node_literal);
                connection_node->parent = current_node;
                connection_node->type = TableauNodeType::Reduction;
                connection_node->depth = current_node->depth + 1;
           
                connection_node->lemma = new TableauProofNode(next_node_literal);
                connection_node->lemma->type = TableauNodeType::Lemma;
                connection_node->lemma->lemma_number = ++lemma_count;
                connection_node->lemma->parent = connection_node;
 
                connection_node->lemma_list = current_node->lemma_list;
                current_node->lemma_list.push_back(lemma_count);
                connection_node->lemma_list_p = current_node->lemma_list_p;
                current_node->lemma_list_p.push_back(connection_node->lemma);
 
                connection_node->t = current_node->t_child;
                connection_node->l = current_node->l_child;
                connection_node->p = current_node->p;
                connection_node->p.push_back(PathPair(connection_node->t, 
                                                  connection_node->l));
                current_node->l_child++;
 
                false_node = new TableauProofNode();
                false_node->parent = connection_node;
                false_node->depth = current_node->depth + 2;
                false_node->t = ++t_count;
                false_node->p = connection_node->p;
                false_node->p.push_back(PathPair(false_node->t, 0));
                false_node->needs_reduction_link = true;
                false_node->reduction_node = current_node->p[P+1];
 
                complementary_literal = current_node->path[P];
                negated_literal = complementary_literal;
                negated_literal.invert();
                u_result = u(negated_literal, next_node_literal);
                if (u_result != UnificationOutcome::Succeed || 
                    !next_node_literal.is_compatible_with(&negated_literal)) {
                        cerr << "There's a problem with your reduction unification." << endl;
                        exit(EXIT_FAILURE);
                }
                else {
                    false_node->sub = u.get_substitution();
                }
                current_node->children.push_back(connection_node);
                connection_node->children.push_back(false_node);
                break;
            case StackItemType::LeftBranch:
                L = si.this_action.Lindex;
                C2 = si.this_action.C_2;
                L2 = si.this_action.Lprime;
                
                // Remove from c_remaining the next literal to make a node for.
                next_node_literal = current_node->c_remaining[L];
                current_node->c_remaining.drop_literal(L);
 
                right_stack.push_back(current_node->depth);
 
                // Make the clause copy for the new node.
                matrix_p->make_copy_with_new_unique_vars(C2, C, *vi, *ti);
                //cout << C << endl;
 
                // Get the complementary literal and find the unification.
                complementary_literal = C[L2];
                negated_literal = complementary_literal;
                negated_literal.invert();
                u_result = u(negated_literal, next_node_literal);
                
                // Make a new node. removed_literal is the one needed 
                // for the child making a connection.
                new_node = new TableauProofNode(C, next_node_literal);
                if (u_result != UnificationOutcome::Succeed || 
                    !next_node_literal.is_compatible_with(&negated_literal)) {
                        cerr << "There's a problem with your extension unification." << endl;
                        exit(EXIT_FAILURE);
                }
                else {
                    new_node->sub = u.get_substitution();
                }
                new_node->parent = current_node;
                new_node->t = current_node->t_child;
                new_node->t_child = ++t_count;
                removed_literal = new_node->c_remaining[L2];
                new_node->c_remaining.drop_literal(L2);
                new_node->depth = current_node->depth + 1;
                new_node->path = current_node->path;
                new_node->path.push_back(next_node_literal);
        
                new_node->lemma = new TableauProofNode(next_node_literal);
                new_node->lemma->type = TableauNodeType::Lemma;
                new_node->lemma->lemma_number = ++lemma_count;
                new_node->lemma->parent = new_node;
 
                new_node->lemma_list = current_node->lemma_list;
                current_node->lemma_list.push_back(lemma_count);
                new_node->lemma_list_p = current_node->lemma_list_p;
                current_node->lemma_list_p.push_back(new_node->lemma);
 
                new_node->l = current_node->l_child;
                new_node->l_child = 1;
                new_node->matrix_id = C2;
                current_node->l_child++;
                new_node->p = current_node->p;
                new_node->p.push_back(PathPair(new_node->t, new_node->l));
                
                // Now set up the new child.
                current_node->children.push_back(new_node);
                
                // Now add the connection and $false nodes.
                connection_node = new TableauProofNode(complementary_literal);
                connection_node->parent = new_node;
                connection_node->depth = current_node->depth + 2;
 
                connection_node->t = t_count;
                connection_node->l = new_node->l_child;
                new_node->l_child++;
                connection_node->p = new_node->p;
                connection_node->p.push_back(PathPair(connection_node->t, 
                                                      connection_node->l));
 
                false_node = new TableauProofNode();
                false_node->parent = connection_node;
                false_node->depth = current_node->depth + 3;
 
                false_node->t = ++t_count;
 
                connection_node->children.push_back(false_node);
                new_node->children.push_back(connection_node);
 
                current_node = new_node;
                clauses_used_in_proof.insert(matrix_p->get_name(C2));
                break;
            case StackItemType::RightBranch:
                new_depth = right_stack.back();
                right_stack.pop_back();
                while (current_node->depth != new_depth) {
                    current_node = current_node->parent;
                }
                break;
            case StackItemType::Lemmata:
                L = si.this_action.Lindex;
                lemma_index = si.this_action.index_in_lemmata;
 
                next_node_literal = current_node->c_remaining[L];
                current_node->c_remaining.drop_literal(L);
                
                // ...make reduction and $false nodes ...
                connection_node = new TableauProofNode(next_node_literal);
                connection_node->parent = current_node;
                connection_node->depth = current_node->depth + 1;
                connection_node->t = current_node->t_child;
                connection_node->l = current_node->l_child;
                connection_node->p = current_node->p;
                connection_node->p.push_back(PathPair(connection_node->t, 
                                                  connection_node->l));
                
                current_node->l_child++;
                current_node->children.push_back(connection_node);
 
                lemma_literal = current_node->lemma_list_p[lemma_index]->lit;
                new_node = new TableauProofNode(lemma_literal);
                new_node->type = TableauNodeType::LemmaExtension;
                new_node->parent = connection_node;
                new_node->t = ++t_count;
                new_node->l = 1; 
                new_node->parent = connection_node;
                new_node->lemma_reduction_node = current_node->lemma_list[lemma_index];
                new_node->needs_lemma_link = true;
                new_node->p = connection_node->p;
                new_node->p.push_back(PathPair(new_node->t, 
                                                      new_node->l));
 
                // Possibly not needed, but include for now. Check unification works 
                // and store result. Remember not to apply it though!
                //lemma_literal.invert();
                u_result = u(next_node_literal, lemma_literal);
                if (u_result != UnificationOutcome::Succeed || 
                    !next_node_literal.is_compatible_with(&lemma_literal)) {
                    cerr << "There's a problem with your lemma unification." << endl;
                    exit(EXIT_FAILURE);
                }
                else {
                    new_node->sub = u.get_substitution();
                }
                u.backtrack();
 
                current_node->lemma_list_p[lemma_index]->lemma_is_used=true;
 
                connection_node->children.push_back(new_node);
 
                false_node = new TableauProofNode();
                false_node->parent = new_node;
                false_node->depth = current_node->depth + 2;
                false_node->t = ++t_count;
                false_node->p = connection_node->p;
                false_node->p.push_back(PathPair(false_node->t, 0));
 
                new_node->children.push_back(false_node);
                break;
            default:
                cerr << "Something is really wrong..." << endl;
                break;
        }
        
    }
}

get_clauses_used_in_proof()

unordered_set< string > TableauProof::get_clauses_used_in_proof ( ) const

inline

Definition at line 302 of file TableauProof.hpp.

                                                            {
        return clauses_used_in_proof;
    }

lit_t_l_to_Graphviz()

pair< string, string > TableauProof::lit_t_l_to_Graphviz ( TableauProofNode * _p, const string & _parent ) const

private

Definition at line 596 of file TableauProof.cpp.

                                                                      {
    string s;
    string name("\"t");
    Literal literal = _p->lit;
    if (_p->type == TableauNodeType::LemmaExtension) {
        literal.invert();
    }
    name += to_string(_p->t);
    name += "-";
    name += to_string(_p->l);
    name += "\"";
    s += name;
    s += " [style=filled, fillcolor=mintcream, fontname=Courier label=\"";
    s += literal.make_Graphviz(params::sub_Graphviz_proof);
    if (params::graphviz_tableau_subs && _p->sub.size() > 0) {
        s += "\n";
        s += _p->sub.make_Graphviz(params::sub_Graphviz_proof);
    }
    s += "\n[";
    s += to_string(_p->t);
    s += ":";
    s += to_string(_p->l);
    s += "]";
    s += "\"];\n";
    s += _parent;
    s += " -> ";
    s += name;
    s += " ;\n";
    return pair<string, string>(name, s);
}

lit_t_l_to_LaTeX()

string TableauProof::lit_t_l_to_LaTeX ( TableauProofNode * _p ) const

private

Definition at line 494 of file TableauProof.cpp.

                                                                {
    string s;
    s += "{$";
    Literal literal = _p->lit;
    if (_p->type == TableauNodeType::LemmaExtension) {
        literal.invert();
    }
    s += literal.make_LaTeX(params::sub_LaTeX_proof);
    s += "$";
     if (params::latex_tableau_subs && _p->sub.size() > 0) {
        s += "\\\\ $";
        s += _p->sub.make_LaTeX(params::sub_LaTeX_proof);
        s += "$";
    }
    s += "\\\\ $[$t";
    s += to_string(_p->t);
    s += ":";
    s += to_string(_p->l);
    s += "$]$";
   
    s += "}, align=center, name=t";
    s += to_string(_p->t);
    s += "-";
    s += to_string(_p->l);
    return s;
}

make_Graphviz()

string TableauProof::make_Graphviz

(

const path &

problem_path

)

const

Definition at line 712 of file TableauProof.cpp.

                                                                 {
    string s;
    s += "digraph \"";
    s += problem_path.filename().string();
    s += "\" {\n";
    s += "size=\"";
    s += std::to_string(params::graphviz_width);
    s += ",";
    s += std::to_string(params::graphviz_height);
    s += "\";\n";
    s += "labelloc=\"t\"\nlabel=\"Connect++ proof for: ";
    s += problem_path.filename().string();
    s += "\";\n";
    s += tableau_to_Graphviz(root);
    s += "\n}\n";
    return s;
}

make_LaTeX()

string TableauProof::make_LaTeX

(

)

const

Definition at line 587 of file TableauProof.cpp.

                                      {
    string s;
    s += "\\begin{forest}";
    s += "for tree=draw, for tree=rounded corners=5mm, for tree=thick";
    s += tableau_to_LaTeX(root);
    s += "\\end{forest}";
    return s;
}

make_tptp()

string TableauProof::make_tptp ( )

inline

Definition at line 289 of file TableauProof.hpp.

                       {
        return tableau_to_tptp_string(root);
    };

show_clauses_used_in_proof()

void TableauProof::show_clauses_used_in_proof ( )

inline

Definition at line 294 of file TableauProof.hpp.

                                      {
        string result;
        for (const string& s : clauses_used_in_proof) {
            result += s;
            result += "\n";
        }
        cout << result << endl;
    }

tableau_to_Graphviz()

string TableauProof::tableau_to_Graphviz ( TableauProofNode * p, const string & _parent = "" ) const

private

Definition at line 628 of file TableauProof.cpp.

                                                                      {
    string s;
    pair<string, string> sp;
    Literal inverted_literal;
    string name;
    switch(p->type) {
        case TableauNodeType::Start:
             s += "\"0-0\" [fontname=Courier label=\"[0:0]\"];\n";
            for (TableauProofNode* q : p->children) 
                s += tableau_to_Graphviz(q, "\"0-0\"");
            break;
        case TableauNodeType::Extension:
        case TableauNodeType::Reduction:
            sp = lit_t_l_to_Graphviz(p, _parent);
            name = sp.first;
            s += sp.second;
            for (TableauProofNode* q : p->children) 
                s += tableau_to_Graphviz(q, sp.first);
            if (p->lemma != nullptr) 
                s += tableau_to_Graphviz(p->lemma, sp.first);
            break;
        case TableauNodeType::Connection:
        case TableauNodeType::LemmaExtension:
            sp = lit_t_l_to_Graphviz(p, _parent);
            name = sp.first;
            s += sp.second;
            for (TableauProofNode* q : p->children) 
                s += tableau_to_Graphviz(q, sp.first);
            break;
        case TableauNodeType::Lemma:
            if (p->lemma_is_used) {
                inverted_literal = p->lit;
                inverted_literal.invert();
                name += "\"l";
                name += to_string(p->lemma_number);
                name += "\"";    
                s += name;
                s += " [style=filled, fillcolor=lightblue, shape=box, fontname=Courier label=\"";
                s += inverted_literal.make_Graphviz(params::sub_Graphviz_proof);
                s += "\nl";
                s += to_string(p->lemma_number);
                s += "\"];\n"; 
                s += _parent;
                s += "->";
                s += name;
                s += ";\n";
            } 
            break;
        case TableauNodeType::False:
            name += "\"t";
            name += to_string(p->t);
            name += "\"";
            s += name;
            s += " [style=filled, fillcolor=lightcyan, fontname=Courier label=\"$false\nt";
            s += to_string(p->t);
            s += "\"];\n";
            s += _parent;
            s += "->";
            s += name;
            s += ";\n";
            break;
        default:
            break;
    }
    if (p->needs_reduction_link) {
        s += "\"t";
        s += to_string(p->reduction_node.first);
        s += "-";
        s += to_string(p->reduction_node.second);
        s += "\" -> ";
        s += name;
        s += " [style=dashed];\n";            
    }
    if (p->needs_lemma_link) {
        s += "\"l";
        s += to_string(p->lemma_reduction_node);
        s += "\" -> ";
        s += name;
        s += " [style=dotted];\n";   
    }
    return s;
}

tableau_to_LaTeX()

string TableauProof::tableau_to_LaTeX ( TableauProofNode * p ) const

private

Definition at line 521 of file TableauProof.cpp.

                                                               {
    string s;
    Literal inverted_literal;
    switch(p->type) {
        case TableauNodeType::Start:
            s += "[{[0:0]}, name=0-0";
            for (TableauProofNode* q : p->children) 
                s += tableau_to_LaTeX(q);
            s += "]";
            break;
        case TableauNodeType::Extension:
        case TableauNodeType::Reduction:
            s += "[";
            s += lit_t_l_to_LaTeX(p);
            for (TableauProofNode* q : p->children) 
                s += tableau_to_LaTeX(q);
            if (p->lemma != nullptr) 
                s += tableau_to_LaTeX(p->lemma);
            s += "]";
            break;
        case TableauNodeType::Connection:
        case TableauNodeType::LemmaExtension:
            s += "[";
            s += lit_t_l_to_LaTeX(p);
            for (TableauProofNode* q : p->children) 
                s += tableau_to_LaTeX(q);
            s += "]";
            break;
        case TableauNodeType::Lemma:
            if (p->lemma_is_used) {
                s += "[{$";
                inverted_literal = p->lit;
                inverted_literal.invert();
                s += inverted_literal.make_LaTeX(params::sub_LaTeX_proof);
                s += "$ \\\\ $[$l";
                s += to_string(p->lemma_number);
                s += "$]$}, align=center, ellipse, name=l";
                s += to_string(p->lemma_number);
                s += "]";
            }
            break;
        case TableauNodeType::False:
            s += "[{$\\ensuremath{\\mathtt{\\$false}}$ \\\\ $[$t";
            s += to_string(p->t);
            s += "$]$}, align=center, name=t";
            s += to_string(p->t);
            s += "]";
            break;
        default:
            break;
    }
    if (p->needs_reduction_link) {
        s += "{ \\draw[<-,dotted] () to[out=south,in=south] (t";
        s += to_string(p->reduction_node.first);
        s += "-";
        s += to_string(p->reduction_node.second);
        s += ");}";            
    }
    if (p->needs_lemma_link) {
        s += "{ \\draw[<-,dashed] () to[out=south west,in=east] (l";
        s += to_string(p->lemma_reduction_node);
        s += ");}";       
    }
    return s;
}

tableau_to_tptp_string()

string TableauProof::tableau_to_tptp_string ( TableauProofNode * p ) const

private

Definition at line 333 of file TableauProof.cpp.

                                                                     {
    string s;
    string s2;
    size_t lemma_b1;
    size_t lemma_b2;
    Literal inverted_literal;
    Clause reordered_clause;
    bool subbed = !params::tptp_proof_no_subs;
    switch(p->type) {
        case TableauNodeType::Start:
            s += "cnf(t1, plain,            ";
            for (TableauProofNode* q : p->children) {
                reordered_clause.add_lit(q->lit);
            }
            s += reordered_clause.to_tptp_string(subbed);
            s += ",\n    inference(start, [status(thm), parent(0:0)], [";
            s += matrix_p->get_name(p->matrix_id);
            s += "])  ).";
            s += "\n\n";
            for (TableauProofNode* q : p->children) {
                s += tableau_to_tptp_string(q);
            }
            break;
        case TableauNodeType::Extension:
            s += "cnf(t";
            s += to_string(p->t_child);
            s += ", plain,            ";
            for (TableauProofNode* q : p->children) {
                reordered_clause.add_lit(q->lit);
            }
            s += reordered_clause.to_tptp_string(subbed);
            s += ",\n    inference(extension, [status(thm), ";
            s += p->children[0]->make_path_string();
            if (params::tptp_proof_show_subs && p->sub.size() > 0) {
                s += ", ";
                s += p->sub.to_tptp_string(subbed);
            }
            s += "], [";
            s += matrix_p->get_name(p->matrix_id);
            s += "])  ).";
            s += "\n\n";
            for (TableauProofNode* q : p->children) {
                s += tableau_to_tptp_string(q);
            }
            s += tableau_to_tptp_string(p->lemma);
            break;
        case TableauNodeType::Connection:
            if (p->children[0]->type != TableauNodeType::LemmaExtension) {
                s += "cnf(t";
                s += to_string(p->children[0]->t);
                s += ", plain,            $false,\n";
                s += "    inference(connection, [status(thm), ";
                s += p->children[0]->make_path_string();
                s += "], [t";
                s += to_string(p->t);
                s += ":";
                s += to_string(p->l);
                s += ",t";
                s += to_string(p->parent->t);
                s += ":";
                s += to_string(p->parent->l);
                s += "])  ).";
                s += "\n\n";
            }
            else {
                s += tableau_to_tptp_string(p->children[0]);
            }
            break;
        case TableauNodeType::Reduction:
            s += "cnf(t";
            s += to_string(p->children[0]->t);
            s += ", plain,            $false,\n";
            s += "    inference(reduction, [status(thm), ";
            s += p->children[0]->make_path_string();
            if (params::tptp_proof_show_subs && p->sub.size() > 0) {
                s += ", ";
                s += p->sub.to_tptp_string(subbed);
            }
            s += "], [t";
            s += to_string(p->t);
            s += ":";
            s += to_string(p->l);
            s += ",t";
            s += to_string(p->children[0]->reduction_node.first);
            s += ":";
            s += to_string(p->children[0]->reduction_node.second);
            s += "])  ).";
            s += "\n\n";
            s += tableau_to_tptp_string(p->lemma);
            break;
        case TableauNodeType::Lemma:
            if (p != nullptr && p->lemma_is_used) {
                s += "cnf(l";
                s += to_string(p->lemma_number);
                s += ", lemma,            ";
                inverted_literal = p->lit;
                inverted_literal.invert();
                s += inverted_literal.to_tptp_string(subbed);
                s += ",\n    inference(lemma, [status(cth), ";
                s += p->make_path_string();
                s += ", below(";
                lemma_b1 = p->parent->parent->t;
                lemma_b2 = p->parent->parent->l;
                if (lemma_b1 != 0) {
                    s += "t"; 
                }
                s += to_string(lemma_b1);
                s += ":";
                s += to_string(lemma_b2);
                s += ")], [t";
                s += to_string(p->parent->t);
                s += ":";
                s += to_string(p->parent->l);
                s += "])  ).";
                s += "\n\n";
            }
            break;
        case TableauNodeType::LemmaExtension:
            s += "cnf(t";
            s += to_string(p->t);
            s += ", plain,            ";
            inverted_literal = p->lit;
            inverted_literal.invert();
            s += inverted_literal.to_tptp_string(subbed);    
            s += ",\n    inference(lemma_extension, [status(thm), ";
            s += p->make_path_string();
            //if (params::tptp_proof_show_subs && p->sub.size() > 0) {
            //    s += ", ";
            //    s += p->sub.to_tptp_string(subbed);
            //}
            s += "], [l";
            s += to_string(p->lemma_reduction_node);
            s += ":";
            s += to_string(1);
            s += "])  ).";
            s += "\n\n";
            
            s += "cnf(t";
            s += to_string(p->children[0]->t);
            s += ", plain,            $false,\n";
            s += "    inference(connection, [status(thm), ";
            s += p->children[0]->make_path_string();
            s += "], [t";
            s += to_string(p->t);
            s += ":";
            s += to_string(p->l);
            s += ",t";
            s += to_string(p->parent->t);
            s += ":";
            s += to_string(p->parent->l);
            s += "])  ).";
            s += "\n\n";
            break;
        case TableauNodeType::False:
            break;
        default:
            break;
    }
    return s;
}

Member Data Documentation

clauses_used_in_proof

unordered_set<string> TableauProof::clauses_used_in_proof

private

When you produce the proof you want to know which clauses were actually used so that you can limit the printing of the clause conversion process to the parts that are actually needed.

Definition at line 262 of file TableauProof.hpp.

current_node

TableauProofNode* TableauProof::current_node

private

Definition at line 253 of file TableauProof.hpp.

lemma_count

size_t TableauProof::lemma_count

private

Definition at line 250 of file TableauProof.hpp.

matrix_p

Matrix* TableauProof::matrix_p

private

Definition at line 246 of file TableauProof.hpp.

right_stack

vector<size_t> TableauProof::right_stack

private

Definition at line 255 of file TableauProof.hpp.

root

TableauProofNode* TableauProof::root

private

Definition at line 252 of file TableauProof.hpp.

stack_p

Stack* TableauProof::stack_p

private

Definition at line 244 of file TableauProof.hpp.

stack_size

size_t TableauProof::stack_size

private

Definition at line 245 of file TableauProof.hpp.

t_count

size_t TableauProof::t_count

private

Definition at line 249 of file TableauProof.hpp.

ti

TermIndex* TableauProof::ti

private

Definition at line 248 of file TableauProof.hpp.

vi

VariableIndex* TableauProof::vi

private

Definition at line 247 of file TableauProof.hpp.

---

The documentation for this class was generated from the following files:

• /Users/sbh11/Desktop/connection-prover/c++/connect++/source/misc/TableauProof.hpp
• /Users/sbh11/Desktop/connection-prover/c++/connect++/source/misc/TableauProof.cpp