Connect++ 0.6.0
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
FunctionIndex.cpp
1/*
2
3Copyright © 2023-24 Sean Holden. All rights reserved.
4
5*/
6/*
7
8This file is part of Connect++.
9
10Connect++ is free software: you can redistribute it and/or modify it
11under the terms of the GNU General Public License as published by the
12Free Software Foundation, either version 3 of the License, or (at your
13option) any later version.
14
15Connect++ is distributed in the hope that it will be useful, but WITHOUT
16ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
17FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for
18more details.
19
20You should have received a copy of the GNU General Public License along
21with Connect++. If not, see <https://www.gnu.org/licenses/>.
22
23*/
24
25#include "FunctionIndex.hpp"
26//----------------------------------------------------------------------
27FunctionIndex::FunctionIndex()
28: funs()
29, name_index()
30, next_index(0)
31, skolem_function_number(1)
32{}
33//----------------------------------------------------------------------
34FunctionIndex::~FunctionIndex() {
35 for (size_t i = 0; i < funs.size(); i++)
36 delete funs[i];
37}
38//----------------------------------------------------------------------
39Function* FunctionIndex::add_function(const string& name, Arity arity) {
40 Function* new_fun = nullptr;
41 auto i = name_index.find(FunIndexType(name, arity));
42 if (i == name_index.end()) {
43 new_fun = new Function(next_index++, name, arity);
44 funs.push_back(new_fun);
45 name_index.insert(FunMapType(FunIndexType(name, arity),
46 new_fun));
47 }
48 else {
49 new_fun = i->second;
50 }
51 return new_fun;
52}
53//----------------------------------------------------------------------
55 string name(params::unique_skolem_prefix);
56 name += std::to_string(skolem_function_number++);
57 return add_function(name, arity);
58}
59//----------------------------------------------------------------------
60Function* FunctionIndex::find_function(const string& fun_name,
61 Arity arity) {
62 Function* fun = nullptr;
63 auto i = name_index.find(FunIndexType(fun_name, arity));
64 if (i != name_index.end())
65 fun = i->second;
66 else
67 cerr << "That function name doesn't exist" << endl;
68 return fun;
69}
70//----------------------------------------------------------------------
72 Arity result = 0;
73 for (size_t i = 0; i < funs.size(); i++) {
74 Arity current = funs[i]->get_arity();
75 if (current > result)
76 result = current;
77 }
78 return result;
79}
80//----------------------------------------------------------------------
82 Arity result = UINT32_MAX;
83 for (size_t i = 0; i < funs.size(); i++) {
84 Arity current = funs[i]->get_arity();
85 if (current < result)
86 result = current;
87 }
88 return result;
89}
90//----------------------------------------------------------------------
91ostream& operator<<(ostream& out, const FunctionIndex& fi) {
92 out << "Function Index" << endl;
93 out << "--------------" << endl;
94 for (Function* f : fi.funs) {
95 out << *f << endl;
96 }
97 return out;
98}
Basic representation of functions.
Definition Function.hpp:54
Mechanism for looking after functions.
unordered_map< pair< string, Arity >, Function *, fun_hash > name_index
Fast lookup from name/arity to pointer to the Function.
Arity find_minimum_arity() const
Find the smallest arity appearing for any Function in the index.
ID next_index
Keep track of ids for adding new Functions.
Arity find_maximum_arity() const
Find the largest arity appearing for any Function in the index.
Function * find_function(const string &, Arity)
Look up a stored Function by name and arity.
Function * add_function(const string &, Arity)
Add a new function to the index.
uint32_t skolem_function_number
Automate the naming of Skolem functions.
vector< Function * > funs
Pointers to all the Functions used.
Function * make_skolem_function(Arity)
Add a new Skolem function. Naming is automatic.