Skip to content

Commit 3d3e3e3

Browse files
giomascegiomasce
committed
Make namespace std explicit everywhere.
1 parent 9849976 commit 3d3e3e3

38 files changed

+971
-1044
lines changed

‎apps/generalizable_theorems.cpp

+16-18
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,6 @@
1212
#include "parsing/unif.h"
1313
#include "utils/utils.h"
1414

15-
using namespace std;
16-
1715
class Reactor {
1816
public:
1917
Reactor(LibraryToolbox &tb, size_t hyps_num) :
@@ -23,7 +21,7 @@ class Reactor {
2321
for (size_t i = 0; i < hyps_num; i++) {
2422
LabTok type;
2523
SymTok type_sym = tb.get_turnstile_alias();
26-
tie(type, ignore) = tb.new_temp_var(type_sym);
24+
std::tie(type, std::ignore) = tb.new_temp_var(type_sym);
2725
this->hypotheses.push_back(type);
2826
}
2927
}
@@ -59,8 +57,8 @@ class Reactor {
5957

6058
bool process_assertion(const Assertion &ass) {
6159
ParsingTree< SymTok, LabTok > thesis;
62-
vector< ParsingTree< SymTok, LabTok > > hyps;
63-
tie(hyps, thesis) = tb.refresh_assertion(ass);
60+
std::vector< ParsingTree< SymTok, LabTok > > hyps;
61+
std::tie(hyps, thesis) = tb.refresh_assertion(ass);
6462
assert(stack.size() >= hyps.size());
6563
for (size_t i = 0; i < hyps.size(); i++) {
6664
this->unificator.add_parsing_trees(this->stack[this->stack.size()-hyps.size()+i], hyps[i]);
@@ -88,8 +86,8 @@ class Reactor {
8886
return substitute(this->stack.at(0), this->is_var, this->subst);
8987
}
9088

91-
vector< ParsingTree< SymTok, LabTok > > get_hypotheses() {
92-
vector< ParsingTree< SymTok, LabTok > > ret;
89+
std::vector< ParsingTree< SymTok, LabTok > > get_hypotheses() {
90+
std::vector< ParsingTree< SymTok, LabTok > > ret;
9391
for (const auto &hyp_lab : this->hypotheses) {
9492
SubstMap< SymTok, LabTok >::iterator it = subst.find(hyp_lab);
9593
if (it != subst.end()) {
@@ -108,9 +106,9 @@ class Reactor {
108106
LibraryToolbox &tb;
109107
const std::function< bool(LabTok) > &is_var;
110108
BilateralUnificator< SymTok, LabTok > unificator;
111-
vector< ParsingTree< SymTok, LabTok > > stack;
109+
std::vector< ParsingTree< SymTok, LabTok > > stack;
112110
//map< size_t, LabTok > hypotheses;
113-
vector< LabTok > hypotheses;
111+
std::vector< LabTok > hypotheses;
114112
SubstMap< SymTok, LabTok > subst;
115113
};
116114

@@ -189,29 +187,29 @@ void find_generalizable_theorems() {
189187
}
190188

191189
if (!generalizables.empty()) {
192-
cout << "GENERALIZABLE THEOREM (" << tb.resolve_label(ass.get_thesis()) << ")" << endl;
193-
cout << "Theorem: " << tb.print_sentence(reactor.get_theorem()) << endl;
190+
std::cout << "GENERALIZABLE THEOREM (" << tb.resolve_label(ass.get_thesis()) << ")" << std::endl;
191+
std::cout << "Theorem: " << tb.print_sentence(reactor.get_theorem()) << std::endl;
194192
if (ass.get_ess_hyps().size() != 0) {
195-
cout << "with hypotheses:" << endl;
193+
std::cout << "with hypotheses:" << std::endl;
196194
for (const auto &hyp : reactor.get_hypotheses()) {
197-
cout << " * " << tb.print_sentence(hyp) << endl;
195+
std::cout << " * " << tb.print_sentence(hyp) << std::endl;
198196
}
199197
}
200-
cout << "Substitution map for generalizable variables:" << endl;
198+
std::cout << "Substitution map for generalizable variables:" << std::endl;
201199
for (const auto &x : generalizables) {
202200
ParsingTree< SymTok, LabTok > pt;
203201
pt.label = x.first;
204-
cout << " * " << tb.print_sentence(pt) << ": " << tb.print_sentence(x.second) << endl;
202+
std::cout << " * " << tb.print_sentence(pt) << ": " << tb.print_sentence(x.second) << std::endl;
205203
}
206204
if (!not_generalizables.empty()) {
207-
cout << "Substitution map for other variables:" << endl;
205+
std::cout << "Substitution map for other variables:" << std::endl;
208206
for (const auto &x : not_generalizables) {
209207
ParsingTree< SymTok, LabTok > pt;
210208
pt.label = x.first;
211-
cout << " * " << tb.print_sentence(pt) << ": " << tb.print_sentence(x.second) << endl;
209+
std::cout << " * " << tb.print_sentence(pt) << ": " << tb.print_sentence(x.second) << std::endl;
212210
}
213211
}
214-
cout << endl;
212+
std::cout << std::endl;
215213
}
216214

217215
tb.release_temp_var_frame();

‎apps/learning.cpp

+53-55
Original file line numberDiff line numberDiff line change
@@ -11,21 +11,19 @@
1111
#include "parsing/unif.h"
1212
#include "utils/utils.h"
1313

14-
using namespace std;
15-
1614
void print_parsing_tree(const ParsingTree< SymTok, LabTok > &pt) {
1715
bool first = true;
1816
for (const auto &child : pt.children) {
1917
if (!first) {
20-
cout << " ";
18+
std::cout << " ";
2119
}
2220
print_parsing_tree(child);
2321
first = false;
2422
}
2523
if (!first) {
26-
cout << " ";
24+
std::cout << " ";
2725
}
28-
cout << pt.children.size() << " " << pt.label;
26+
std::cout << pt.children.size() << " " << pt.label;
2927
}
3028

3129
void print_trace(const ProofTree< Sentence > &pt, const LibraryToolbox &tb, const Assertion &ass) {
@@ -39,17 +37,17 @@ void print_trace(const ProofTree< Sentence > &pt, const LibraryToolbox &tb, cons
3937
auto it = find(ass.get_ess_hyps().begin(), ass.get_ess_hyps().end(), pt.label);
4038
auto parsing_tree = tb.parse_sentence(pt.sentence.begin()+1, pt.sentence.end(), tb.get_turnstile_alias());
4139
if (it == ass.get_ess_hyps().end()) {
42-
cout << "# " << essentials_num << " " << tb.resolve_label(pt.label) << " " << tb.print_sentence(pt.sentence, SentencePrinter::STYLE_PLAIN) << endl;
43-
//cout << essentials_num << " " << pt.label << " " << tb.print_sentence(pt.sentence, SentencePrinter::STYLE_NUMBERS) << endl;
44-
cout << essentials_num << " " << pt.label << " ";
40+
std::cout << "# " << essentials_num << " " << tb.resolve_label(pt.label) << " " << tb.print_sentence(pt.sentence, SentencePrinter::STYLE_PLAIN) << std::endl;
41+
//std::cout << essentials_num << " " << pt.label << " " << tb.print_sentence(pt.sentence, SentencePrinter::STYLE_NUMBERS) << std::endl;
42+
std::cout << essentials_num << " " << pt.label << " ";
4543
print_parsing_tree(parsing_tree);
46-
cout << endl;
44+
std::cout << std::endl;
4745
} else {
48-
cout << "# 0 _hyp" << (it - ass.get_ess_hyps().begin()) << " " << tb.print_sentence(pt.sentence, SentencePrinter::STYLE_PLAIN) << endl;
49-
//cout << "0 0 " << tb.print_sentence(pt.sentence, SentencePrinter::STYLE_NUMBERS) << endl;
50-
cout << "0 0 ";
46+
std::cout << "# 0 _hyp" << (it - ass.get_ess_hyps().begin()) << " " << tb.print_sentence(pt.sentence, SentencePrinter::STYLE_PLAIN) << std::endl;
47+
//std::cout << "0 0 " << tb.print_sentence(pt.sentence, SentencePrinter::STYLE_NUMBERS) << std::endl;
48+
std::cout << "0 0 ";
5149
print_parsing_tree(parsing_tree);
52-
cout << endl;
50+
std::cout << std::endl;
5351
}
5452
}
5553

@@ -80,14 +78,14 @@ struct ProofStat {
8078
size_t ess_hyp_steps = 0;
8179
};
8280

83-
ostream &operator<<(ostream &os, const ProofStat &stat) {
81+
std::ostream &operator<<(std::ostream &os, const ProofStat &stat) {
8482
return os << stat.proof_size << " " << stat.ess_proof_size << " " << stat.ess_hyp_num << " " << stat.ess_hyp_steps;
8583
}
8684

8785
struct StepContext {
8886
ParsingTree2< SymTok, LabTok > thesis;
89-
vector< ParsingTree2< SymTok, LabTok > > hypotheses;
90-
set< pair< LabTok, LabTok > > dists;
87+
std::vector< ParsingTree2< SymTok, LabTok > > hypotheses;
88+
std::set< std::pair< LabTok, LabTok > > dists;
9189
};
9290

9391
namespace boost {
@@ -107,10 +105,10 @@ struct hash< StepContext > {
107105

108106
struct StepProof {
109107
LabTok label;
110-
vector< StepContext > children;
108+
std::vector< StepContext > children;
111109
};
112110

113-
unordered_map< StepContext, StepProof, boost::hash< StepContext > > mega_map;
111+
std::unordered_map< StepContext, StepProof, boost::hash< StepContext > > mega_map;
114112

115113
void proof_stat_unwind_tree(const ProofTree< Sentence > &pt, const Assertion &ass, ProofStat &stat) {
116114
if (pt.essential) {
@@ -133,7 +131,7 @@ int proofs_stats_main(int argc, char *argv[]) {
133131
//auto &tb = data.tb;
134132

135133
TextProgressBar tpb(100, (double) lib.get_assertions().size());
136-
vector< pair< LabTok, ProofStat > > proofs_stats;
134+
std::vector< std::pair< LabTok, ProofStat > > proofs_stats;
137135
for (const Assertion &ass : lib.get_assertions()) {
138136
if (!ass.is_valid()) {
139137
continue;
@@ -152,7 +150,7 @@ int proofs_stats_main(int argc, char *argv[]) {
152150
//stat.proof_size = proof.get_labels().size();
153151
stat.ess_hyp_num = ass.get_ess_hyps().size();
154152
proof_stat_unwind_tree(exec->get_proof_tree(), ass, stat);
155-
proofs_stats.push_back(make_pair(ass.get_thesis(), stat));
153+
proofs_stats.push_back(std::make_pair(ass.get_thesis(), stat));
156154
tpb.report(ass.get_thesis());
157155
}
158156
tpb.finished();
@@ -162,7 +160,7 @@ int proofs_stats_main(int argc, char *argv[]) {
162160
});
163161

164162
for (size_t i = 0; i < 20; i++) {
165-
cout << lib.resolve_label(proofs_stats[i].first) << ": " << proofs_stats[i].second << endl;
163+
std::cout << lib.resolve_label(proofs_stats[i].first) << ": " << proofs_stats[i].second << std::endl;
166164
}
167165

168166
return 0;
@@ -172,14 +170,14 @@ static_block {
172170
}
173171

174172
void gen_theorems(const BilateralUnificator< SymTok, LabTok > &unif,
175-
const vector< ParsingTree2< SymTok, LabTok > > &open_hyps,
176-
const vector< LabTok > &steps,
173+
const std::vector< ParsingTree2< SymTok, LabTok > > &open_hyps,
174+
const std::vector< LabTok > &steps,
177175
size_t hyps_pos,
178-
const vector< const Assertion* > &useful_asses,
176+
const std::vector< const Assertion* > &useful_asses,
179177
const ParsingTree2< SymTok, LabTok > &final_thesis,
180178
LibraryToolbox &tb,
181179
size_t depth,
182-
const function< void(const ParsingTree2< SymTok, LabTok >&, const vector< ParsingTree2< SymTok, LabTok > >&, const vector< LabTok >&, LibraryToolbox&)> &callback) {
180+
const std::function< void(const ParsingTree2< SymTok, LabTok >&, const std::vector< ParsingTree2< SymTok, LabTok > >&, const std::vector< LabTok >&, LibraryToolbox&)> &callback) {
183181
if (depth == 0 || hyps_pos == open_hyps.size()) {
184182
auto unif2 = unif;
185183
SubstMap2< SymTok, LabTok > subst;
@@ -189,7 +187,7 @@ void gen_theorems(const BilateralUnificator< SymTok, LabTok > &unif,
189187
return;
190188
}
191189
auto thesis = substitute2(final_thesis, tb.get_standard_is_var(), subst);
192-
vector< ParsingTree2< SymTok, LabTok > > hyps;
190+
std::vector< ParsingTree2< SymTok, LabTok > > hyps;
193191
for (const auto &hyp : open_hyps) {
194192
hyps.push_back(substitute2(hyp, tb.get_standard_is_var(), subst));
195193
}
@@ -200,14 +198,14 @@ void gen_theorems(const BilateralUnificator< SymTok, LabTok > &unif,
200198
tb.new_temp_var_frame();
201199
const Assertion &ass = *assp;
202200
ParsingTree2< SymTok, LabTok > thesis;
203-
vector< ParsingTree2< SymTok, LabTok > > hyps;
201+
std::vector< ParsingTree2< SymTok, LabTok > > hyps;
204202
tie(hyps, thesis) = tb.refresh_assertion2(ass);
205203
auto unif2 = unif;
206204
auto steps2 = steps;
207205
unif2.add_parsing_trees2(open_hyps[hyps_pos], thesis);
208206
steps2.push_back(ass.get_thesis());
209207
if (unif2.is_unifiable()) {
210-
//cout << "Attaching " << tb.resolve_label(ass.get_thesis()) << " in position " << hyps_pos << endl;
208+
//std::cout << "Attaching " << tb.resolve_label(ass.get_thesis()) << " in position " << hyps_pos << std::endl;
211209
auto open_hyps2 = open_hyps;
212210
open_hyps2.erase(open_hyps2.begin() + hyps_pos);
213211
open_hyps2.insert(open_hyps2.end(), hyps.begin(), hyps.end());
@@ -219,17 +217,17 @@ void gen_theorems(const BilateralUnificator< SymTok, LabTok > &unif,
219217
}
220218

221219
size_t count = 0;
222-
void print_theorem(const ParsingTree2< SymTok, LabTok > &thesis, const vector< ParsingTree2< SymTok, LabTok > >&hyps, const vector< LabTok > &steps, LibraryToolbox &tb) {
220+
void print_theorem(const ParsingTree2< SymTok, LabTok > &thesis, const std::vector< ParsingTree2< SymTok, LabTok > >&hyps, const std::vector< LabTok > &steps, LibraryToolbox &tb) {
223221
::count++;
224222
bool finished = hyps.empty();
225223
if (::count % 10000 == 0 || finished) {
226-
cout << ::count << endl;
227-
cout << tb.print_sentence(thesis) << endl;
228-
cout << "with the hypotheses:" << endl;
224+
std::cout << ::count << std::endl;
225+
std::cout << tb.print_sentence(thesis) << std::endl;
226+
std::cout << "with the hypotheses:" << std::endl;
229227
for (const auto &hyp : hyps) {
230-
cout << " * " << tb.print_sentence(hyp) << endl;
228+
std::cout << " * " << tb.print_sentence(hyp) << std::endl;
231229
}
232-
cout << "Proved with steps: " << tb.print_proof(steps) << endl;
230+
std::cout << "Proved with steps: " << tb.print_proof(steps) << std::endl;
233231
}
234232
if (finished) {
235233
exit(0);
@@ -240,8 +238,8 @@ void print_theorem(const ParsingTree2< SymTok, LabTok > &thesis, const vector< P
240238
}
241239

242240
int gen_random_theorems_main(int argc, char *argv[]) {
243-
random_device rand_dev;
244-
mt19937 rand_mt;
241+
std::random_device rand_dev;
242+
std::mt19937 rand_mt;
245243
rand_mt.seed(rand_dev());
246244

247245
auto &data = get_set_mm();
@@ -253,7 +251,7 @@ int gen_random_theorems_main(int argc, char *argv[]) {
253251
//LabTok target_label = lib.get_label(target_label_str);
254252
//auto target_pt = tb.get_parsed_sents2()[target_label];
255253

256-
ostringstream oss;
254+
std::ostringstream oss;
257255
for (int i = 1; i < argc; i++) {
258256
oss << argv[i] << " ";
259257
}
@@ -262,27 +260,27 @@ int gen_random_theorems_main(int argc, char *argv[]) {
262260
auto target_pt = pt_to_pt2(target_pt1);
263261
LabTok target_label = 0;
264262

265-
vector< const Assertion* > useful_asses;
263+
std::vector< const Assertion* > useful_asses;
266264
for (const auto &ass : lib.get_assertions()) {
267265
if (ass.is_valid() && lib.get_sentence(ass.get_thesis()).at(0) == tb.get_turnstile()) {
268266
/*if (ass.get_thesis() >= target_label) {
269267
break;
270268
}*/
271269
if (ass.is_theorem() && ass.has_proof() && ass.get_proof_operator(lib)->is_trivial()) {
272-
//cout << "Proof for " << lib.resolve_label(ass.get_thesis()) << " is trivial" << endl;
270+
//std::cout << "Proof for " << lib.resolve_label(ass.get_thesis()) << " is trivial" << std::endl;
273271
} else {
274272
if (ass.get_thesis() != target_label && ass.get_thesis()) {
275273
useful_asses.push_back(&ass);
276274
}
277275
}
278276
}
279277
}
280-
sort(useful_asses.begin(), useful_asses.end(), [&lib](const auto &x, const auto &y) {
278+
std::sort(useful_asses.begin(), useful_asses.end(), [&lib](const auto &x, const auto &y) {
281279
return x->get_ess_hyps().size() < y->get_ess_hyps().size() || (x->get_ess_hyps().size() == y->get_ess_hyps().size() && lib.get_sentence(x->get_thesis()).size() > lib.get_sentence(y->get_thesis()).size());
282280
});
283-
cout << "There are " << useful_asses.size() << " useful assertions" << endl;
281+
std::cout << "There are " << useful_asses.size() << " useful assertions" << std::endl;
284282

285-
set< LabTok > target_vars;
283+
std::set< LabTok > target_vars;
286284
collect_variables2(target_pt, standard_is_var, target_vars);
287285
std::function< bool(LabTok) > is_var = [&target_vars,&standard_is_var](LabTok x) {
288286
if (target_vars.find(x) != target_vars.end()) {
@@ -292,26 +290,26 @@ int gen_random_theorems_main(int argc, char *argv[]) {
292290
};
293291

294292
BilateralUnificator< SymTok, LabTok > unif(is_var);
295-
vector< ParsingTree2< SymTok, LabTok > > open_hyps;
293+
std::vector< ParsingTree2< SymTok, LabTok > > open_hyps;
296294
LabTok th_label;
297-
tie(th_label, ignore) = tb.new_temp_var(tb.get_turnstile_alias());
295+
std::tie(th_label, std::ignore) = tb.new_temp_var(tb.get_turnstile_alias());
298296
ParsingTree2< SymTok, LabTok > final_thesis = var_parsing_tree(th_label, tb.get_turnstile_alias());
299297
final_thesis = target_pt;
300298
open_hyps.push_back(final_thesis);
301-
vector< LabTok > steps;
299+
std::vector< LabTok > steps;
302300

303301
gen_theorems(unif, open_hyps, steps, 0, useful_asses, final_thesis, tb, 2, print_theorem);
304302
return 0;
305303

306304
for (size_t i = 0; i < 5; i++) {
307305
if (open_hyps.empty()) {
308-
cout << "Terminating early" << endl;
306+
std::cout << "Terminating early" << std::endl;
309307
break;
310308
}
311309
while (true) {
312310
// Select a random hypothesis, a random open hypothesis and let them match
313-
size_t ass_idx = uniform_int_distribution< size_t >(0, useful_asses.size()-1)(rand_mt);
314-
size_t hyp_idx = uniform_int_distribution< size_t >(0, open_hyps.size()-1)(rand_mt);
311+
size_t ass_idx = std::uniform_int_distribution< size_t >(0, useful_asses.size()-1)(rand_mt);
312+
size_t hyp_idx = std::uniform_int_distribution< size_t >(0, open_hyps.size()-1)(rand_mt);
315313
const Assertion &ass = *useful_asses[ass_idx];
316314
if (i == 0 && ass.get_ess_hyps().size() == 0) {
317315
continue;
@@ -320,12 +318,12 @@ int gen_random_theorems_main(int argc, char *argv[]) {
320318
continue;
321319
}
322320
ParsingTree2< SymTok, LabTok > thesis;
323-
vector< ParsingTree2< SymTok, LabTok > > hyps;
321+
std::vector< ParsingTree2< SymTok, LabTok > > hyps;
324322
tie(hyps, thesis) = tb.refresh_assertion2(ass);
325323
auto unif2 = unif;
326324
unif2.add_parsing_trees2(open_hyps[hyp_idx], thesis);
327325
if (unif2.unify2().first) {
328-
cout << "Attaching " << tb.resolve_label(ass.get_thesis()) << " in position " << hyp_idx << endl;
326+
std::cout << "Attaching " << tb.resolve_label(ass.get_thesis()) << " in position " << hyp_idx << std::endl;
329327
unif = unif2;
330328
open_hyps.erase(open_hyps.begin() + hyp_idx);
331329
open_hyps.insert(open_hyps.end(), hyps.begin(), hyps.end());
@@ -339,14 +337,14 @@ int gen_random_theorems_main(int argc, char *argv[]) {
339337
tie(res, subst) = unif.unify2();
340338

341339
if (res) {
342-
cout << "Unification succedeed and proved:" << endl;
343-
cout << tb.print_sentence(substitute2(final_thesis, tb.get_standard_is_var(), subst)) << endl;
344-
cout << "with the hypotheses:" << endl;
340+
std::cout << "Unification succedeed and proved:" << std::endl;
341+
std::cout << tb.print_sentence(substitute2(final_thesis, tb.get_standard_is_var(), subst)) << std::endl;
342+
std::cout << "with the hypotheses:" << std::endl;
345343
for (const auto &hyp : open_hyps) {
346-
cout << " * " << tb.print_sentence(substitute2(hyp, tb.get_standard_is_var(), subst)) << endl;
344+
std::cout << " * " << tb.print_sentence(substitute2(hyp, tb.get_standard_is_var(), subst)) << std::endl;
347345
}
348346
} else {
349-
cout << "Unification failed" << endl;
347+
std::cout << "Unification failed" << std::endl;
350348
}
351349

352350
return 0;

0 commit comments

Comments
 (0)