TermIndex.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 TERMINDEX_HPP
#define TERMINDEX_HPP
 
#include <iostream>
#include <vector>
#include <unordered_map>
 
#include "TermHash.hpp"
 
using std::unordered_map;
using std::vector;
using std::ostream;
using std::endl;
 
class TermIndex {
private:
    unordered_map<Term, Term*, term_hash> index;
    vector<Term*> term_pointers;
    Term* find(const Term&);
public:
    TermIndex() : index(), term_pointers() {}
    ~TermIndex();
    TermIndex(const TermIndex&) = delete;
    TermIndex(const TermIndex&&) = delete;
    TermIndex& operator=(const TermIndex&) = delete;
    TermIndex& operator=(const TermIndex&&) = delete;
    size_t get_size() const { return term_pointers.size(); }
    Term* add_variable_term(Variable*);
    Term* add_function_term(Function*, const vector<Term*>&);
    Term* replace_variable_in_term(Variable*, Variable*, Term*);
    Term* replace_variable_in_term_with_term(Term*, Variable*, Term*);
 
    friend ostream& operator<<(ostream&, const TermIndex&);
};
 
#endif