Skip to content

Commit 806c7b4

Browse files
authored
Merge pull request #5770 from tautschnig/forall-nodes
Remove forall_nodes
2 parents cb9f69a + 571c265 commit 806c7b4

File tree

2 files changed

+36
-40
lines changed

2 files changed

+36
-40
lines changed

.clang-format

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,6 @@ ForEachMacros: [
4242
'Forall_objects',
4343
'forall_valid_objects',
4444
'Forall_valid_objects',
45-
'forall_nodes',
4645
'forall_literals',
4746
'Forall_literals',
4847
'forall_operands',

src/solvers/bdd/miniBDD/miniBDD.cpp

Lines changed: 36 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -17,9 +17,6 @@ Author: Daniel Kroening, [email protected]
1717

1818
#include <iostream>
1919

20-
#define forall_nodes(it) \
21-
for(nodest::const_iterator it = nodes.begin(); it != nodes.end(); it++)
22-
2320
void mini_bdd_nodet::remove_reference()
2421
{
2522
PRECONDITION_WITH_DIAGNOSTICS(
@@ -65,9 +62,11 @@ void mini_bdd_mgrt::DumpDot(std::ostream &out, bool suppress_zero) const
6562
"{ node [shape=plaintext,fontname=\"Times Italic\",fontsize=24] \" "
6663
<< var_table[v].label << " \" }; ";
6764

68-
forall_nodes(u)
69-
if(u->var == (v + 1) && u->reference_counter != 0)
70-
out << '"' << u->node_number << "\"; ";
65+
for(const auto &u : nodes)
66+
{
67+
if(u.var == (v + 1) && u.reference_counter != 0)
68+
out << '"' << u.node_number << "\"; ";
69+
}
7170

7271
out << "}\n";
7372
}
@@ -83,22 +82,21 @@ void mini_bdd_mgrt::DumpDot(std::ostream &out, bool suppress_zero) const
8382

8483
out << '\n';
8584

86-
forall_nodes(u)
85+
for(const auto &u : nodes)
8786
{
88-
if(u->reference_counter == 0)
87+
if(u.reference_counter == 0)
8988
continue;
90-
if(u->node_number <= 1)
89+
if(u.node_number <= 1)
9190
continue;
9291

93-
if(!suppress_zero || u->high.node_number() != 0)
94-
out << '"' << u->node_number << '"' << " -> " << '"'
95-
<< u->high.node_number() << '"'
92+
if(!suppress_zero || u.high.node_number() != 0)
93+
out << '"' << u.node_number << '"' << " -> " << '"'
94+
<< u.high.node_number() << '"'
9695
<< " [style=solid,arrowsize=\".75\"];\n";
9796

98-
if(!suppress_zero || u->low.node_number() != 0)
99-
out << '"' << u->node_number << '"' << " -> " << '"'
100-
<< u->low.node_number() << '"'
101-
<< " [style=dashed,arrowsize=\".75\"];\n";
97+
if(!suppress_zero || u.low.node_number() != 0)
98+
out << '"' << u.node_number << '"' << " -> " << '"' << u.low.node_number()
99+
<< '"' << " [style=dashed,arrowsize=\".75\"];\n";
102100

103101
out << '\n';
104102
}
@@ -128,9 +126,9 @@ void mini_bdd_mgrt::DumpTikZ(
128126

129127
unsigned previous = 0;
130128

131-
forall_nodes(u)
129+
for(const auto &u : nodes)
132130
{
133-
if(u->var == (v + 1) && u->reference_counter != 0)
131+
if(u.var == (v + 1) && u.reference_counter != 0)
134132
{
135133
out << " \\node[xshift=0cm, BDDnode, ";
136134

@@ -139,11 +137,11 @@ void mini_bdd_mgrt::DumpTikZ(
139137
else
140138
out << "right of=n" << previous;
141139

142-
out << "] (n" << u->node_number << ") {";
140+
out << "] (n" << u.node_number << ") {";
143141
if(node_numbers)
144-
out << "\\small $" << u->node_number << "$";
142+
out << "\\small $" << u.node_number << "$";
145143
out << "};\n";
146-
previous = u->node_number;
144+
previous = u.node_number;
147145
}
148146
}
149147

@@ -164,17 +162,17 @@ void mini_bdd_mgrt::DumpTikZ(
164162
out << " % edges\n";
165163
out << '\n';
166164

167-
forall_nodes(u)
165+
for(const auto &u : nodes)
168166
{
169-
if(u->reference_counter != 0 && u->node_number >= 2)
167+
if(u.reference_counter != 0 && u.node_number >= 2)
170168
{
171-
if(!suppress_zero || u->low.node_number() != 0)
172-
out << " \\draw[->,dashed] (n" << u->node_number << ") -> (n"
173-
<< u->low.node_number() << ");\n";
169+
if(!suppress_zero || u.low.node_number() != 0)
170+
out << " \\draw[->,dashed] (n" << u.node_number << ") -> (n"
171+
<< u.low.node_number() << ");\n";
174172

175-
if(!suppress_zero || u->high.node_number() != 0)
176-
out << " \\draw[->] (n" << u->node_number << ") -> (n"
177-
<< u->high.node_number() << ");\n";
173+
if(!suppress_zero || u.high.node_number() != 0)
174+
out << " \\draw[->] (n" << u.node_number << ") -> (n"
175+
<< u.high.node_number() << ");\n";
178176
}
179177
}
180178

@@ -490,23 +488,22 @@ void mini_bdd_mgrt::DumpTable(std::ostream &out) const
490488
out << "\\# & \\mathit{var} & \\mathit{low} &"
491489
" \\mathit{high} \\\\\\hline\n";
492490

493-
forall_nodes(it)
491+
for(const auto &n : nodes)
494492
{
495-
out << it->node_number << " & ";
493+
out << n.node_number << " & ";
496494

497-
if(it->node_number == 0 || it->node_number == 1)
498-
out << it->var << " & & \\\\";
499-
else if(it->reference_counter == 0)
495+
if(n.node_number == 0 || n.node_number == 1)
496+
out << n.var << " & & \\\\";
497+
else if(n.reference_counter == 0)
500498
out << "- & - & - \\\\";
501499
else
502-
out << it->var << "\\," << var_table[it->var - 1].label << " & "
503-
<< it->low.node_number() << " & " << it->high.node_number()
504-
<< " \\\\";
500+
out << n.var << "\\," << var_table[n.var - 1].label << " & "
501+
<< n.low.node_number() << " & " << n.high.node_number() << " \\\\";
505502

506-
if(it->node_number == 1)
503+
if(n.node_number == 1)
507504
out << "\\hline";
508505

509-
out << " % " << it->reference_counter << '\n';
506+
out << " % " << n.reference_counter << '\n';
510507
}
511508
}
512509

0 commit comments

Comments
 (0)