FunctionIndex.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 FUNCTIONINDEX_HPP
#define FUNCTIONINDEX_HPP
 
#include<iostream>
#include<iomanip>
#include<string>
#include<vector>
#include<unordered_map>
 
#include "Function.hpp"
#include "FunctionHash.hpp"
 
using std::pair;
using std::setw;
using std::ostream;
using std::string;
using std::vector;
using std::unordered_map;
using std::cerr;
using std::endl;
 
using FunIndexType = pair<string, Arity>;
using FunMapType = pair<FunIndexType, Function*>;
 
class FunctionIndex {
private:
    vector<Function*> funs;
    unordered_map<pair<string, Arity>, Function*, fun_hash> name_index;
    ID next_index;
    uint32_t skolem_function_number;
public:
    FunctionIndex();
    FunctionIndex(const FunctionIndex&) = delete;
    FunctionIndex(const FunctionIndex&&) = delete;
    FunctionIndex& operator=(const FunctionIndex&) = delete;
     FunctionIndex& operator=(const FunctionIndex&&) = delete;
    ~FunctionIndex();
    size_t get_size() const { return funs.size(); }
    Function* add_function(const string&, Arity);
    Function* make_skolem_function(Arity);
    Function* find_function(const string&, Arity);
    Arity find_maximum_arity() const;
    Arity find_minimum_arity() const;
    Function* operator[](size_t i) { return funs[i]; }
    
    friend ostream& operator<<(ostream&, const FunctionIndex&);
};
 
#endif