Class for representing nodes in a tableau proof. More...

#include <TableauProof.hpp>

Collaboration diagram for TableauProofNode:

[legend]

Public Member Functions
	TableauProofNode ()
	Basic constructor.

	TableauProofNode (Literal &_lit)
	Nearly all the work here is done by constructors.

	TableauProofNode (Clause &_c)
	Nearly all the work here is done by constructors.

	TableauProofNode (Clause &_c, Literal &_lit)
	Nearly all the work here is done by constructors.

	~TableauProofNode ()
	Usual destructor for this sort of thing. Remember to delete what needs deleting.

string	path_to_tptp_string ()

string	parent_to_tptp_string ()

string	make_path_string ()

string	lemmas_to_string ()

Private Attributes
TableauNodeType	type

TableauProofNode *	parent

ClauseNum	t
	A node in the tableau is identified by ‘t : l’.

ClauseNum	t_child
	Nodes maintain the t value for children.

LitNum	l
	A node in the tableau is identified by ‘t : l’.

LitNum	l_child
	Nodes maintain the l value for children.

Clause	c_output
	A node is associated with a clause.

Clause	c_remaining
	Starts equal to c. At each step in constructing the tableau a single literal is dealt with in a child. This keeps track of the remaining clause.

size_t	matrix_id
	Some nodes need to produce output referring to a clause in the matrix.

Literal	lit
	Literal associated with the node.

vector< PathPair >	p
	Paths are stored both as collections of literals and collections of t:l pairs. Both are needed for construction and producing output.

vector< Literal >	path
	Paths are stored both as collections of literals and collections of t:l pairs. Both are needed for construction and producing output.

Substitution	sub
	Substitution associated with reduction, extension or lemma.

size_t	depth
	Where are we in the tree? Used for backtracking.

bool	needs_lemma_link
	Used in producing LaTex output to indicate that a link has to be added.

bool	needs_reduction_link
	Used in producing LaTex output to indicate that a link has to be added.

PathPair	reduction_node
	Which node is associated with this one?

size_t	lemma_reduction_node
	Which node is associated with this one?

vector< size_t >	lemma_list
	Lemma lists are kept as both numbers and pointer to other nodes. Both are needed.

vector< TableauProofNode * >	lemma_list_p

TableauProofNode *	lemma
	Lemma associated with a reduction or extension.

size_t	lemma_number
	Numerical identifier for a lemma.

bool	lemma_is_used
	Used in producing LaTeX output so that only used lemmas are displayed.

vector< TableauProofNode * >	children
	Children of this node.

Friends
class	TableauProof

Detailed Description

Class for representing nodes in a tableau proof.

See the documentation for TableauProof for details.

Definition at line 53 of file TableauProof.hpp.

Constructor & Destructor Documentation

◆ TableauProofNode() [1/4]

TableauProofNode::TableauProofNode ( )

inline

Basic constructor.

Definition at line 159 of file TableauProof.hpp.

    : type(TableauNodeType::False)
    , parent(nullptr)
    , t(0)
    , t_child(0)
    , l(0)
    , l_child(0)
    , c_output()
    , c_remaining()
    , matrix_id(0)
    , lit()
    , p() 
    , path()
    , sub()
    , depth(0)
    , needs_reduction_link(false)
    , needs_lemma_link(false)
    , reduction_node()
    , lemma_reduction_node(0)
    , lemma_list()
    , lemma_list_p()
    , lemma(nullptr)
    , lemma_number(0)
    , lemma_is_used(false)
    , children() 
    {}

◆ TableauProofNode() [2/4]

TableauProofNode::TableauProofNode ( Literal & _lit )

inline

Nearly all the work here is done by constructors.

Definition at line 188 of file TableauProof.hpp.

    : TableauProofNode() {
        type = TableauNodeType::Connection;
        lit = _lit;
    }

◆ TableauProofNode() [3/4]

TableauProofNode::TableauProofNode ( Clause & _c )

inline

Nearly all the work here is done by constructors.

Definition at line 196 of file TableauProof.hpp.

    : TableauProofNode() {
        type = TableauNodeType::Start;
        c_output = _c;
        c_remaining = _c;
    }

◆ TableauProofNode() [4/4]

TableauProofNode::TableauProofNode	(	Clause &	_c,
		Literal &	_lit )

inline

Nearly all the work here is done by constructors.

Definition at line 205 of file TableauProof.hpp.

   : TableauProofNode() {
        type = TableauNodeType::Extension;
        lit = _lit;
        c_output = _c;
        c_remaining = _c;
    }

◆ ~TableauProofNode()

TableauProofNode::~TableauProofNode ( )

inline

Usual destructor for this sort of thing. Remember to delete what needs deleting.

Definition at line 216 of file TableauProof.hpp.

                        { 
        delete lemma;
        for (TableauProofNode* child : children) 
            delete child;
    }

Member Function Documentation

◆ lemmas_to_string()

string TableauProofNode::lemmas_to_string ( )

Definition at line 72 of file TableauProof.cpp.

                                          {
        string s;
        for (size_t l : lemma_list) {
            s += to_string(l);
            s += "\\ ";
        }
        return s;
    }

◆ make_path_string()

string TableauProofNode::make_path_string ( )

Definition at line 58 of file TableauProof.cpp.

                                          {
    string s;
    if (!params::tptp_proof_show_paths) {
        s += "parent(";
        s += parent_to_tptp_string();
    }
    else {
        s += "path(";
        s += path_to_tptp_string();
    }
    s += ")";
    return s;
}

◆ parent_to_tptp_string()

string TableauProofNode::parent_to_tptp_string ( )

Definition at line 49 of file TableauProof.cpp.

                                               {
    string s("t");
    PathPair p2(parent->p.back());
    s += to_string(p2.first);
    s += ":";
    s += to_string(p2.second);
    return s;
}

◆ path_to_tptp_string()

string TableauProofNode::path_to_tptp_string ( )

Definition at line 30 of file TableauProof.cpp.

                                             {
    string s("[");
    vector<PathPair> p2(parent->p);
 
    for (int i = p2.size() - 1; i >= 0; i--) {
        if (i > 0) {
            s += "t";
        }
        s += to_string(p2[i].first);
        s += ":";
        s += to_string(p2[i].second);
        if (i > 0) {
            s += ",";
        }
    }
    s += "]";
    return s;
}

Friends And Related Symbol Documentation

◆ TableauProof

friend class TableauProof

friend

Definition at line 226 of file TableauProof.hpp.

Member Data Documentation

◆ c_output

Clause TableauProofNode::c_output

private

A node is associated with a clause.

Definition at line 78 of file TableauProof.hpp.

◆ c_remaining

Clause TableauProofNode::c_remaining

private

Starts equal to c. At each step in constructing the tableau a single literal is dealt with in a child. This keeps track of the remaining clause.

Definition at line 84 of file TableauProof.hpp.

◆ children

vector<TableauProofNode*> TableauProofNode::children

private

Children of this node.

Definition at line 154 of file TableauProof.hpp.

◆ depth

size_t TableauProofNode::depth

private

Where are we in the tree? Used for backtracking.

Definition at line 113 of file TableauProof.hpp.

◆ l

LitNum TableauProofNode::l

private

A node in the tableau is identified by ‘t : l’.

Definition at line 70 of file TableauProof.hpp.

◆ l_child

LitNum TableauProofNode::l_child

private

Nodes maintain the l value for children.

Definition at line 74 of file TableauProof.hpp.

◆ lemma

TableauProofNode* TableauProofNode::lemma

private

Lemma associated with a reduction or extension.

Definition at line 141 of file TableauProof.hpp.

◆ lemma_is_used

bool TableauProofNode::lemma_is_used

private

Used in producing LaTeX output so that only used lemmas are displayed.

Definition at line 150 of file TableauProof.hpp.

◆ lemma_list

vector<size_t> TableauProofNode::lemma_list

private

Lemma lists are kept as both numbers and pointer to other nodes. Both are needed.

Definition at line 136 of file TableauProof.hpp.

◆ lemma_list_p

vector<TableauProofNode*> TableauProofNode::lemma_list_p

private

Definition at line 137 of file TableauProof.hpp.

◆ lemma_number

size_t TableauProofNode::lemma_number

private

Numerical identifier for a lemma.

Definition at line 145 of file TableauProof.hpp.

◆ lemma_reduction_node

size_t TableauProofNode::lemma_reduction_node

private

Which node is associated with this one?

Definition at line 131 of file TableauProof.hpp.

◆ lit

Literal TableauProofNode::lit

private

Literal associated with the node.

Definition at line 93 of file TableauProof.hpp.

◆ matrix_id

size_t TableauProofNode::matrix_id

private

Some nodes need to produce output referring to a clause in the matrix.

Definition at line 89 of file TableauProof.hpp.

◆ needs_lemma_link

bool TableauProofNode::needs_lemma_link

private

Used in producing LaTex output to indicate that a link has to be added.

Definition at line 118 of file TableauProof.hpp.

◆ needs_reduction_link

bool TableauProofNode::needs_reduction_link

private

Used in producing LaTex output to indicate that a link has to be added.

Definition at line 123 of file TableauProof.hpp.

◆ p

vector<PathPair> TableauProofNode::p

private

Paths are stored both as collections of literals and collections of t:l pairs. Both are needed for construction and producing output.

Definition at line 99 of file TableauProof.hpp.

◆ parent

TableauProofNode* TableauProofNode::parent

private

Definition at line 56 of file TableauProof.hpp.

◆ path

vector<Literal> TableauProofNode::path

private

Paths are stored both as collections of literals and collections of t:l pairs. Both are needed for construction and producing output.

Definition at line 105 of file TableauProof.hpp.

◆ reduction_node

PathPair TableauProofNode::reduction_node

private

Which node is associated with this one?

Definition at line 127 of file TableauProof.hpp.

◆ sub

Substitution TableauProofNode::sub

private

Substitution associated with reduction, extension or lemma.

Definition at line 109 of file TableauProof.hpp.

◆ t

ClauseNum TableauProofNode::t

private

A node in the tableau is identified by ‘t : l’.

Definition at line 61 of file TableauProof.hpp.

◆ t_child

ClauseNum TableauProofNode::t_child

private

Nodes maintain the t value for children.

Definition at line 65 of file TableauProof.hpp.

◆ type

TableauNodeType TableauProofNode::type

private

Definition at line 55 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

Public Member Functions

Private Attributes

Friends

Detailed Description

Constructor & Destructor Documentation

◆ TableauProofNode() [1/4]

◆ TableauProofNode() [2/4]

◆ TableauProofNode() [3/4]

◆ TableauProofNode() [4/4]

◆ ~TableauProofNode()

Member Function Documentation

◆ lemmas_to_string()

◆ make_path_string()

◆ parent_to_tptp_string()

◆ path_to_tptp_string()

Friends And Related Symbol Documentation

◆ TableauProof

Member Data Documentation

◆ c_output

◆ c_remaining

◆ children

◆ depth

◆ l

◆ l_child

◆ lemma

◆ lemma_is_used

◆ lemma_list

◆ lemma_list_p

◆ lemma_number

◆ lemma_reduction_node

◆ lit

◆ matrix_id

◆ needs_lemma_link

◆ needs_reduction_link

◆ p

◆ parent

◆ path

◆ reduction_node

◆ sub

◆ t

◆ t_child

◆ type