TableauProof.hpp

/*
 
Copyright © 2023-26 Sean Holden. All rights reserved.
 
*/
/*
 
This file is part of Connect++.
 
Connect++ is free software: you can redistribute it and/or modify it 
under the terms of the GNU General Public License as published by the 
Free Software Foundation, either version 3 of the License, or (at your 
option) any later version.
 
Connect++ is distributed in the hope that it will be useful, but WITHOUT 
ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or 
FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for 
more details.
 
You should have received a copy of the GNU General Public License along 
with Connect++. If not, see <https://www.gnu.org/licenses/>. 
 
*/
 
#ifndef TABLEAUPROOF_HPP
#define TABLEAUPROOF_HPP
 
#include<iostream>
#include<vector>
#include<unordered_set>
 
#include "Stack.hpp"
#include "Matrix.hpp"
#include "SimplePath.hpp"
 
using std::vector;
using std::unordered_set;
using std::filesystem::path;
 
using PathPair = pair<size_t, size_t>;
 
enum class TableauNodeType {
    Start, Extension, Connection, Reduction, Lemma, LemmaExtension, False 
};
class TableauProofNode {
private:
    TableauNodeType type;
    TableauProofNode* parent;
    ClauseNum           t; 
    ClauseNum           t_child;
    LitNum              l;
    LitNum              l_child;
    Clause              c_output;
    Clause              c_remaining;
    size_t              matrix_id;
    Literal             lit;
    vector<PathPair>    p;
    vector<Literal>     path;
    Substitution        sub;
    size_t              depth;
    bool                needs_lemma_link;
    bool                needs_reduction_link;
    PathPair            reduction_node;
    size_t              lemma_reduction_node;
    vector<size_t>      lemma_list;
    vector<TableauProofNode*> lemma_list_p;
    TableauProofNode*   lemma;
    size_t              lemma_number;
    bool                lemma_is_used;
    vector<TableauProofNode*> children;
public:
    TableauProofNode() 
    : 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(Literal& _lit) 
    : TableauProofNode() {
        type = TableauNodeType::Connection;
        lit = _lit;
    }
    TableauProofNode(Clause& _c) 
    : TableauProofNode() {
        type = TableauNodeType::Start;
        c_output = _c;
        c_remaining = _c;
    }
   TableauProofNode(Clause& _c, Literal& _lit) 
   : TableauProofNode() {
        type = TableauNodeType::Extension;
        lit = _lit;
        c_output = _c;
        c_remaining = _c;
    }
    ~TableauProofNode() { 
        delete lemma;
        for (TableauProofNode* child : children) 
            delete child;
    }
    string path_to_tptp_string();
    string parent_to_tptp_string();
    string make_path_string();
    string lemmas_to_string();
   
    friend class TableauProof;
};
class TableauProof {
private:
    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;
 
    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;
public:
    TableauProof() = delete;
    TableauProof(Stack* _stack_p, Matrix* _matrix_p, 
                 VariableIndex* _vi, TermIndex* _ti) 
    : 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() { delete root; }
 
    void build();
    string make_tptp() {
        return tableau_to_tptp_string(root);
    };
    string make_LaTeX() const;
    string make_Graphviz(const path&) const;
    void show_clauses_used_in_proof() {
        string result;
        for (const string& s : clauses_used_in_proof) {
            result += s;
            result += "\n";
        }
        cout << result << endl;
    }
    unordered_set<string> get_clauses_used_in_proof() const {
        return clauses_used_in_proof;
    }
};
 
#endif