ProofChecker.hpp

/*
 
Copyright © 2023-24 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 PROOFCHECKER_HPP
#define PROOFCHECKER_HPP
 
#include<iostream>
#include<string>
#include<vector>
 
#include "Matrix.hpp"
#include "Unifier.hpp"
 
using std::vector;
using std::pair;
using std::get;
 
using ProofLine = pair<string, vector<size_t>>;
using ProofType = vector<ProofLine>;
using RightStackItem = std::tuple<Clause, 
                                  vector<Literal>, 
                                  vector<Literal>,
                                  size_t>;
 
class ProofChecker {
private:
    VariableIndex* vi;
    TermIndex* ti;
    Matrix& matrix;
    Clause C;
    vector<Literal> P;
    vector<Literal> Lem;
    ProofType proof;
    Unifier u;
    vector<RightStackItem> r_stack;
    size_t num_subs;
    bool C_i_ok(size_t) const;
    bool Lit_i_ok(size_t) const;
    bool P_i_ok(size_t) const;
    bool Lem_i_ok(size_t) const;
    string state_to_string() const;
public:
    ProofChecker() = delete;
    ProofChecker(Matrix&, const ProofType&, VariableIndex*, TermIndex*);
    pair<bool, string> check_proof_verbose();
    bool check_proof();
};
 
#endif