Connect++ 0.1
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
VariableIndex.hpp
1/*
2
3Copyright © 2023 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#ifndef VARIABLEINDEX_HPP
26#define VARIABLEINDEX_HPP
27
28#include<iostream>
29#include<iomanip>
30#include<string>
31#include<sstream>
32#include<vector>
33#include<unordered_map>
34
35#include "Variable.hpp"
36
37using std::string;
38using std::pair;
39using std::vector;
40using std::iostream;
41using std::endl;
42using std::cerr;
43using std::unordered_map;
44using std::istringstream;
45using std::to_string;
46
47using MapType = pair<string, Variable*>;
48
62private:
66 vector<Variable*> vars;
70 unordered_map<string, Variable*> name_index;
75 ID next_index;
83 ID first_anon_variable;
88 ID highest_anon_variable;
96 bool all_names_added;
101 vector<ID> backtrack_points;
102public:
111 VariableIndex(const VariableIndex&) = delete;
112 VariableIndex(const VariableIndex&&) = delete;
113 VariableIndex& operator=(const VariableIndex&) = delete;
114 VariableIndex& operator=(const VariableIndex&&) = delete;
118 inline ID get_next_index() const { return next_index; }
122 inline ID get_first_anon_variable() const { return first_anon_variable; }
126 inline ID get_highest_anon_variable() const { return highest_anon_variable; }
130 inline bool get_all_names_added() const { return all_names_added; }
134 inline size_t get_num_backtracks() const { return backtrack_points.size(); }
144 Variable* add_named_var(const string&);
161 Variable* find_variable(const string&);
169 void set_all_names_added();
173 void clear_substitutions();
184 void add_backtrack_point();
197 void backtrack();
208 void reset();
209
210 friend ostream& operator<<(ostream&, const VariableIndex&);
211};
212
213#endif
Basic representation of variables.
Definition Variable.hpp:58
Storage of named variables, and management of new, anonymous variables.
Definition VariableIndex.hpp:61
ID get_next_index() const
Straightforward access function.
Definition VariableIndex.hpp:118
void reset()
Get rid of all the markers used for backtracking.
Definition VariableIndex.cpp:143
void clear_substitutions()
Undo all substitutions made, to anything, ever.
Definition VariableIndex.cpp:67
Variable * add_named_var(const string &)
Add a variable with the specified name to the index.
Definition VariableIndex.cpp:43
ID get_first_anon_variable() const
Straightforward access function.
Definition VariableIndex.hpp:122
ID add_named_backtrack_point()
Same as add_backtrack_point, but return an identifier allowing multiple levels of backtracking using ...
Definition VariableIndex.cpp:121
void set_all_names_added()
Call this to indicate that only anonymous variables can now be created.
Definition VariableIndex.cpp:62
bool get_all_names_added() const
Straightforward access function.
Definition VariableIndex.hpp:130
size_t get_num_backtracks() const
Straightforward access function.
Definition VariableIndex.hpp:134
void backtrack_to_named_point(ID)
Backtrack, possibly multiple times, to the specified point.
Definition VariableIndex.cpp:135
Variable * add_anon_var()
Add an anonymous variable.
Definition VariableIndex.cpp:72
void backtrack()
Backtrack to the last marker.
Definition VariableIndex.cpp:126
void add_backtrack_point()
Add a backtrack point.
Definition VariableIndex.cpp:117
ID get_highest_anon_variable() const
Straightforward access function.
Definition VariableIndex.hpp:126
Variable * find_variable(const string &)
Look up a variable by name.
Definition VariableIndex.cpp:94
VariableIndex(const VariableIndex &)=delete
Copying this would be a very silly idea, so explicitly disallow it.