Connect++ 0.5.0
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
VariableIndex.hpp
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#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;
108public:
117 VariableIndex(const VariableIndex&) = delete;
118 VariableIndex(const VariableIndex&&) = delete;
119 VariableIndex& operator=(const VariableIndex&) = delete;
120 VariableIndex& operator=(const VariableIndex&&) = delete;
124 inline ID get_next_index() const { return next_index; }
128 inline ID get_first_anon_variable() const { return first_anon_variable; }
136 inline bool get_all_names_added() const { return all_names_added; }
140 inline size_t get_num_backtracks() const { return backtrack_points.size(); }
150 Variable* add_named_var(const string&);
174 Variable* find_variable(const string&);
182 void set_all_names_added();
186 void clear_substitutions();
197 void add_backtrack_point();
210 void backtrack();
221 void reset();
222
223 friend ostream& operator<<(ostream&, const VariableIndex&);
224};
225
226#endif
Basic representation of variables.
Definition Variable.hpp:58
Storage of named variables, and management of new, anonymous and unique variables.
ID get_next_index() const
Straightforward access function.
Variable * add_unique_var()
Add a unique variable when converting to CNF.
void reset()
Get rid of all the markers used for backtracking.
ID next_unique_index
When converting to CNF you need new, unique variables, but they need to be treated separately from an...
vector< ID > backtrack_points
Backtrack points stored as indices in the vars vector.
void clear_substitutions()
Undo all substitutions made, to anything, ever.
Variable * add_named_var(const string &)
Add a variable with the specified name to the index.
ID get_first_anon_variable() const
Straightforward access function.
ID next_index
Keep track of automatically generated Variable indices.
ID add_named_backtrack_point()
Same as add_backtrack_point, but return an identifier allowing multiple levels of backtracking using ...
ID first_anon_variable
Set after you've added all the named variables for the problem.
void set_all_names_added()
Call this to indicate that only anonymous variables can now be created.
bool get_all_names_added() const
Straightforward access function.
size_t get_num_backtracks() const
Straightforward access function.
ID highest_anon_variable
Keep track of how many anonymous Variables you currently have available.
void backtrack_to_named_point(ID)
Backtrack, possibly multiple times, to the specified point.
vector< Variable * > vars
All the variables made, named, unique and anonymous.
Variable * add_anon_var()
Add an anonymous variable.
void backtrack()
Backtrack to the last marker.
void add_backtrack_point()
Add a backtrack point.
ID get_highest_anon_variable() const
Straightforward access function.
unordered_map< string, Variable * > name_index
Fast lookup of Variables by name.
bool all_names_added
Set after you've added all the named variables for the problem.
Variable * find_variable(const string &)
Look up a variable by name.
VariableIndex(const VariableIndex &)=delete
Copying this would be a very silly idea, so explicitly disallow it.