StackProver.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 STACKPROVER_HPP
#define STACKPROVER_HPP
 
#include<iostream>
#include<string>
#include<filesystem>
#include <chrono>
 
#include "FunctionIndex.hpp"
#include "PredicateIndex.hpp"
#include "StackItem.hpp"
#include "Matrix.hpp"
#include "TPTPParser.hpp"
#include "ProverOutcome.hpp"
#include "SubstitutionStack.hpp"
#include "ProofPrinter.hpp"
#include "Interval.hpp"
#include "cursor.hpp"
#include "PathUtilities.hpp"
#include "vic_strings.hpp"
 
using std::string;
using std::get;
 
namespace fs = std::filesystem;
namespace chrono = std::chrono;
 
using namespace tptp_parser;
 
class StackProver {
private:
    size_t num_preds;
    VariableIndex var_index;
    FunctionIndex fun_index;
    TermIndex term_index;
    PredicateIndex pred_index;
    SubstitutionStack sub_stack;
    vector<StartClauseStatus> results;
    Matrix matrix;
    SimplePath path;
    Clause new_C;
    Lemmata lemmata;
    Unifier u;
    InferenceItem action;
    StackItem* si;
    uint32_t current_depth_limit;
    uint32_t current_depth;
    bool depth_limit_reached;
    string status;
    vector<StackItem> stack;
    vector<StackItem> right_branch_stack;
    bool backtrack;
    ProofPrinter proof_printer;
    fs::path problem_path;
    Interval output_interval;
    uint32_t reductions_tried;
    uint32_t extensions_tried;
    uint32_t lemmata_tried;
    uint32_t right_branches_started;
    uint32_t proof_count;
    bool use_timeout;
    chrono::steady_clock::time_point end_time;
    verbose_print::VPrint show;
    //----------------------------------------------------------------------
    //----------------------------------------------------------------------
    //----------------------------------------------------------------------
    // Here is where the heavy lifting happens.
    //----------------------------------------------------------------------
    //----------------------------------------------------------------------
    //----------------------------------------------------------------------
    ProverResult go();
    void populate_stack_item();
    void extend_with_action();
    bool depth_limited();
    bool axiom() const;
    void process_axiom_forward();
    void backtrack_once();
    void reduction_backtrack();
    void lemmata_backtrack();
    void left_extension_backtrack();
    void right_extension_backtrack();
    void set_up_start_clauses();
    void reset_for_start() {
      depth_limit_reached = false;
      si = nullptr;
      backtrack = false;
      path.clear();
      stack.clear();
      lemmata.clear();
      right_branch_stack.clear();
      sub_stack.clear();
    }
    bool cnf_only;
    bool conjecture_true;
    bool conjecture_false;
    bool conjecture_missing;
    bool negated_conjecture_removed;
    bool fof_has_axioms;
    bool simplified_fof_has_axioms;
public:
    StackProver();
    StackProver(const StackProver&) = delete;
    StackProver(const StackProver&&) = delete;
    StackProver& operator=(const StackProver&) = delete;
    StackProver& operator=(const StackProver&&) = delete;
    std::tuple<VariableIndex*, FunctionIndex*, PredicateIndex*, TermIndex*> get_indexes() {
      auto result = std::make_tuple(&var_index, &fun_index, &pred_index, &term_index);
      return result;
    }
    string get_status() const { return status; }
    void set_timeout(chrono::steady_clock::time_point time) {
      use_timeout = true;
      end_time = time;
    }
    void set_problem_path(fs::path& p) { problem_path = p; }
    void set_num_preds(size_t);
    void read_from_tptp_file(const string&, bool&, size_t&);
    void add_equality_axioms(Predicate*);
    void deterministic_reorder(uint32_t n) {
      matrix.deterministic_reorder(n);
    }
    void random_reorder() {
      matrix.random_reorder();
    }
    void show_matrix() {
      cout << "Matrix:" << endl;
      cout << matrix.to_string() << endl;
    }
    Matrix& get_matrix() {
      return matrix;
    };
    bool problem_is_cnf_only() const {
      return cnf_only;
    }
    bool problem_has_true_conjecture() const {
      return conjecture_true;
    }
    bool problem_has_false_conjecture() const {
      return conjecture_false;
    }
    bool problem_has_missing_conjecture() const {
      return conjecture_missing;
    }
    bool problem_has_negated_conjecture_removed() const {
      return negated_conjecture_removed;
    }
    bool problem_has_fof_axioms() const {
      return fof_has_axioms;
    }
    bool simplified_problem_has_fof_axioms() const {
      return simplified_fof_has_axioms;
    }
    void show_tptp_proof() {
      cout << endl << "% Problem matrix:" << endl;
      matrix.show_tptp();
      cout << endl << "% Proof stack:" << endl;
      proof_printer.show_tptp();
    }
    ProverOutcome prove();
    vector<pair<string, vector<size_t>>> get_internal_proof() const;
    /* 
    * The remaining material is really just for debugging.
    */
    void show_matrix() const { cout << matrix << endl; }
    void show_path() const { cout << path << endl; }
    void show_stack();
    void show_right_stack();
    void show_term_index() { cout << term_index << endl; }
    void show_statistics() const;
    friend ostream& operator<<(ostream&, const StackProver&);
};
 
#endif