Connect++ 0.6.1
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
VariableIndex.cpp
1/*
2
3Copyright © 2023-25 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 "VariableIndex.hpp"
26
27//----------------------------------------------------------------------
28VariableIndex::VariableIndex()
29: vars()
30, cached_vars()
31, name_index()
32, next_index(0)
33, next_unique_index(0)
34, first_anon_variable(0)
35, highest_anon_variable(0)
36, all_names_added(false)
37, backtrack_points()
38{}
39//----------------------------------------------------------------------
40VariableIndex::~VariableIndex() {
41 for (size_t i = 0; i < vars.size(); i++)
42 delete vars[i];
43 for (size_t i = 0; i < cached_vars.size(); i++)
44 delete cached_vars[i];
45}
46//----------------------------------------------------------------------
48 Variable* new_var = nullptr;
49 if (!all_names_added) {
50 auto i = name_index.find(name);
51 if (i == name_index.end()) {
52 new_var = new Variable(next_index++, name);
53 vars.push_back(new_var);
54 name_index.insert(MapType(name, new_var));
55 }
56 else {
57 new_var = i->second;
58 }
59 }
60 else {
61 cerr << "You can't add any more named variables." << endl;
62 }
63 return new_var;
64}
65//----------------------------------------------------------------------
70//----------------------------------------------------------------------
72 for (size_t i = 0; i < vars.size(); i++)
73 vars[i]->remove_substitution();
74}
75//----------------------------------------------------------------------
77 if (!all_names_added) {
79 }
80 Variable* new_var = nullptr;
81 // You can recycle an anonymous variable that was used
82 // earlier then freed up under backtracking.
84 new_var = vars[next_index++];
85 new_var->remove_substitution();
86 }
87 // You need to actually generate a new anonymous variable.
88 else {
90 string name("_");
91 name += to_string(next_index);
92 new_var = new Variable(next_index++, name);
93 vars.push_back(new_var);
94 }
95 return new_var;
96}
97//----------------------------------------------------------------------
99 string name(params::unique_var_prefix);
100 name += to_string(next_unique_index);
102 return add_named_var(name);
103}
104//----------------------------------------------------------------------
106 string name(params::unique_var_prefix);
107 name += to_string(next_unique_index);
109 Variable* new_var = new Variable(0, name);
110 cached_vars.push_back(new_var);
111 name_index.insert(MapType(name, new_var));
112 return new_var;
113}
114//----------------------------------------------------------------------
115Variable* VariableIndex::find_variable(const string& var_name) {
116 Variable* var = nullptr;
117 istringstream st(var_name);
118 char c;
119 st >> c;
120 if (c == '_') {
121 ID id;
122 st >> id;
123 if (id < next_index)
124 var = vars[id];
125 else
126 cerr << "That anonymous variable doesn't exist" << endl;
127 }
128 else {
129 auto i = name_index.find(var_name);
130 if (i != name_index.end())
131 var = i->second;
132 else
133 cerr << "That named variable doesn't exist" << endl;
134 }
135 return var;
136}
137//----------------------------------------------------------------------
141//----------------------------------------------------------------------
146//----------------------------------------------------------------------
148 if (backtrack_points.size() > 0) {
150 backtrack_points.pop_back();
151 }
152 else
153 cerr << "There's nowhere left to backtrack to." << endl;
154}
155//----------------------------------------------------------------------
157 while (backtrack_points.back() != id) {
158 backtrack_points.pop_back();
159 }
160 next_index = id;
161 backtrack_points.pop_back();
162}
163//----------------------------------------------------------------------
165 if (all_names_added) {
166 backtrack_points.clear();
168 }
169}
170//----------------------------------------------------------------------
171ostream& operator<<(ostream& out, const VariableIndex& vi) {
172 out << "Variable Index" << endl;
173 out << "--------------" << endl;
174 ID id = 0;
175 auto i = vi.backtrack_points.begin();
176 for (Variable* v : vi.vars) {
177 if (id == vi.next_index)
178 break;
179 out << *v << " ";
180 if (i != vi.backtrack_points.end()) {
181 if (id == *i) {
182 out << " <- Backtrack point";
183 i++;
184 }
185 }
186 out << endl;
187 id++;
188 }
189 out << "Highest anon id: " << vi.highest_anon_variable;
190 return out;
191}
Basic representation of variables.
Definition Variable.hpp:58
void remove_substitution()
Self-explanatory, but be careful!
Definition Variable.hpp:121
Storage of named variables, and management of new, anonymous and unique variables.
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 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.
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 * > cached_vars
All the cached variables made.
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.
Variable * add_cached_var()
Cached variables are dealt with separately as there's no need to keep track of them like the others.
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.