Connect++ 0.6.0
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
PredicateIndex.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 "PredicateIndex.hpp"
26
27PredicateIndex::PredicateIndex()
28: preds()
29, name_index()
30, next_index(0)
31, next_definitional_id(0)
32{
33}
34//----------------------------------------------------------------------
35PredicateIndex::~PredicateIndex() {
36 for (size_t i = 0; i < preds.size(); i++)
37 delete preds[i];
38}
39//----------------------------------------------------------------------
41 Arity arity) {
42 Predicate* new_pred = nullptr;
43 auto i = name_index.find(PredIndexType(name, arity));
44 if (i == name_index.end()) {
45 new_pred = new Predicate(next_index++, name, arity);
46 preds.push_back(new_pred);
47 name_index.insert(PredMapType(PredIndexType(name, arity), new_pred));
48 }
49 else {
50 new_pred = i->second;
51 }
52 return new_pred;
53}
54//----------------------------------------------------------------------
56 Arity arity) {
57 Predicate* pred = nullptr;
58 auto i = name_index.find(PredIndexType(fun_name, arity));
59 if (i != name_index.end())
60 pred = i->second;
61 else
62 cerr << "That predicate name doesn't exist" << endl;
63 return pred;
64}
65//----------------------------------------------------------------------
67 Arity result = 0;
68 for (size_t i = 0; i < preds.size(); i++) {
69 Arity current = preds[i]->get_arity();
70 if (current > result)
71 result = current;
72 }
73 return result;
74}
75//----------------------------------------------------------------------
77 auto i = name_index.find(PredIndexType(string("$true"), 0));
78 if (i != name_index.end())
79 return true;
80 i = name_index.find(PredIndexType(string("$false"), 0));
81 if (i != name_index.end())
82 return true;
83 return false;
84}
85//----------------------------------------------------------------------
86ostream& operator<<(ostream& out, const PredicateIndex& pi) {
87 out << "Predicate Index" << endl;
88 out << "---------------" << endl;
89 for (Predicate* p : pi.preds) {
90 out << *p << endl;
91 }
92 return out;
93}
Basic representation of predicates: here just names, ids and arities.
Definition Predicate.hpp:51
Management of Predicate objects.
vector< Predicate * > preds
Pointers to all predicates.
Predicate * find_predicate(const string &, Arity)
Self-explanatory.
Predicate * add_predicate(const string &, Arity)
Self-explanatory.
bool true_false_added() const
Sometimes $true and $false appear in the TPTP collection. See if you included them during the parsing...
ID next_index
Automatically generate IDs.
Arity find_maximum_arity() const
Find the largest arity appearing in the index.
unordered_map< PredIndexType, Predicate *, fun_hash > name_index
Fast lookup using name and arity.