Matrix.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 MATRIX_HPP
#define MATRIX_HPP
 
#include<iostream>
#include<fstream>
#include<filesystem>
#include<iomanip>
#include<string>
#include<vector>
#include<tuple>
#include<algorithm>
#include<random>
 
#include "InferenceItem.hpp"
#include "Clause.hpp"
#include "ClauseComparisons.hpp"
#include "Unifier.hpp"
#include "Reorder.hpp"
 
using std::pair;
using std::tuple;
using std::vector;
using std::ostream;
using std::endl;
using std::setw;
using std::cout;
using std::filesystem::path;
 
using MatrixPairType = pair<ClauseNum, LitNum>;
using LiteralClausePairType = pair<Literal,Clause>;
class Matrix {
private:
    vector<Clause> clauses;
    vector<bool> positive_clauses;
    vector<bool> negative_clauses;
    vector<bool> ground_clauses;
    vector<string> clause_roles;
    uint32_t num_equals;
    vector<Clause> clauses_copy;
    vector<string> roles_copy;
    bool copy_saved;
    vector<vector<MatrixPairType>> index;
    vector<vector<LiteralClausePairType>> literal_clause_index; 
    static std::mt19937 d;
    void make_clauses_copy() {
      clauses_copy.clear();
      clauses_copy = clauses;
      roles_copy.clear();
      roles_copy = clause_roles;
    }
    void rebuild_index(vector<Clause>&, vector<string>&);
    template<class Comparison>
    void sort_clauses(Comparison comparison) {
      /*
      * Combine the clauses with their roles.
      */
      vector<ClauseAndRole> cr;
      size_t s = clauses.size();
      for (size_t i = 0; i < s; i++) {
        cr.push_back(ClauseAndRole(clauses[i], clause_roles[i]));
      }
      /*
      * Sort them according to the relevant ordering.
      */
      std::sort(cr.begin(), cr.end(), comparison);
      /*
      * Split them again and re-build the index.
      */
      clauses.clear();
      positive_clauses.clear();
      negative_clauses.clear();
      clause_roles.clear();
      size_t s2 = index.size();
      index.clear();
      index = vector<vector<MatrixPairType> >(s2, vector<MatrixPairType>());
      for (size_t i = 0; i < s; i++) {
        add_clause(cr[i].first, cr[i].second);
      }
    }
public:
    Matrix()
    : clauses()
    , index()
    , literal_clause_index()
    , positive_clauses()
    , negative_clauses()
    , ground_clauses()
    , clause_roles()
    , clauses_copy()
    , roles_copy()
    , copy_saved(false)
    {}
    Matrix(size_t);
    Matrix(const Matrix&) = delete;
    Matrix(const Matrix&&) = delete;
    Matrix& operator=(const Matrix&) = delete;
    Matrix& operator=(const Matrix&&) = delete;
    ClauseNum get_num_clauses() const { return clauses.size(); }
    inline size_t get_index_entry_size(size_t _i) const {
      return index[_i].size();
    }
    inline MatrixPairType get_index_entry(size_t _i, size_t _j) const {
      return (index[_i])[_j];
    }
    const Clause& operator[](size_t i) const { return clauses[i]; }
    inline const Literal& inspect_literal(size_t i, size_t j) { 
      return (clauses[i])[j]; 
    }
    inline const Literal& inspect_index_literal(size_t i, size_t j) { 
      return (literal_clause_index[i])[j].first; 
    }
    bool is_positive(size_t i) const { return positive_clauses[i]; }
    bool is_negative(size_t i) const { return negative_clauses[i]; }
    bool is_ground(size_t i) const { return ground_clauses[i]; }
    bool is_conjecture(size_t i) const;
    inline void set_num_equals(uint32_t n) { num_equals = n; } 
    pair<bool,size_t> find_start() const;
    void set_num_preds(size_t);
    void add_clause(Clause&, string = "");
    void deterministic_reorder(size_t);
    void random_reorder();
    void random_reorder_literals();
    void move_equals_to_start();
    /*
    * Iteration on a Matrix is just iteration over the Clauses.
    */
    vector<Clause>::const_iterator cbegin() const { return clauses.cbegin(); }
    vector<Clause>::const_iterator cend() const { return clauses.cend(); }
    vector<Clause>::iterator begin() { return clauses.begin(); }
    vector<Clause>::iterator end() { return clauses.end(); }
    string to_string() const;
    string make_LaTeX(bool = false) const;
    void write_to_prolog_file(const path&) const;
    void show_tptp() const;
    void sort_clauses_by_increasing_size() {
      ClauseLengthCompare comparison;
      sort_clauses<ClauseLengthCompare>(comparison);
    }
    void get_literal_clause_pair(LitNum, size_t, Literal&, Clause&) const;
 
    friend ostream& operator<<(ostream&, const Matrix&);
};
 
 
#endif