Skip to content

Commit 8e70eaa

Browse files
author
Daniel Kroening
authored
Merge pull request #1144 from diffblue/miniBDD-non-recursive-apply
miniBDD: added a non-recursive variant of APPLY
2 parents eb96b70 + a71ca41 commit 8e70eaa

File tree

1 file changed

+130
-9
lines changed

1 file changed

+130
-9
lines changed

‎src/solvers/miniBDD/miniBDD.cpp

+130-9
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@ Author: Daniel Kroening, [email protected]
2222

2323
void mini_bdd_nodet::remove_reference()
2424
{
25+
// NOLINTNEXTLINE(build/deprecated)
2526
assert(reference_counter!=0);
2627

2728
reference_counter--;
@@ -194,20 +195,23 @@ class mini_bdd_applyt
194195

195196
mini_bddt operator()(const mini_bddt &x, const mini_bddt &y)
196197
{
197-
return APP(x, y);
198+
return APP_non_rec(x, y);
198199
}
199200

200201
protected:
201202
bool (*fkt)(bool, bool);
202-
mini_bddt APP(const mini_bddt &x, const mini_bddt &y);
203+
mini_bddt APP_rec(const mini_bddt &x, const mini_bddt &y);
204+
mini_bddt APP_non_rec(const mini_bddt &x, const mini_bddt &y);
203205

204206
typedef std::map<std::pair<unsigned, unsigned>, mini_bddt> Gt;
205207
Gt G;
206208
};
207209

208-
mini_bddt mini_bdd_applyt::APP(const mini_bddt &x, const mini_bddt &y)
210+
mini_bddt mini_bdd_applyt::APP_rec(const mini_bddt &x, const mini_bddt &y)
209211
{
212+
// NOLINTNEXTLINE(build/deprecated)
210213
assert(x.is_initialized() && y.is_initialized());
214+
// NOLINTNEXTLINE(build/deprecated)
211215
assert(x.node->mgr==y.node->mgr);
212216

213217
// dynamic programming
@@ -224,22 +228,134 @@ mini_bddt mini_bdd_applyt::APP(const mini_bddt &x, const mini_bddt &y)
224228
u=mini_bddt(fkt(x.is_true(), y.is_true())?mgr->True():mgr->False());
225229
else if(x.var()==y.var())
226230
u=mgr->mk(x.var(),
227-
APP(x.low(), y.low()),
228-
APP(x.high(), y.high()));
231+
APP_rec(x.low(), y.low()),
232+
APP_rec(x.high(), y.high()));
229233
else if(x.var()<y.var())
230234
u=mgr->mk(x.var(),
231-
APP(x.low(), y),
232-
APP(x.high(), y));
235+
APP_rec(x.low(), y),
236+
APP_rec(x.high(), y));
233237
else /* x.var() > y.var() */
234238
u=mgr->mk(y.var(),
235-
APP(x, y.low()),
236-
APP(x, y.high()));
239+
APP_rec(x, y.low()),
240+
APP_rec(x, y.high()));
237241

238242
G[key]=u;
239243

240244
return u;
241245
}
242246

247+
mini_bddt mini_bdd_applyt::APP_non_rec(
248+
const mini_bddt &_x,
249+
const mini_bddt &_y)
250+
{
251+
struct stack_elementt
252+
{
253+
stack_elementt(
254+
mini_bddt &_result,
255+
const mini_bddt &_x,
256+
const mini_bddt &_y):
257+
result(_result), x(_x), y(_y),
258+
key(x.node_number(), y.node_number()),
259+
var(0), phase(phaset::INIT) { }
260+
mini_bddt &result, x, y, lr, hr;
261+
std::pair<unsigned, unsigned> key;
262+
unsigned var;
263+
enum class phaset { INIT, FINISH } phase;
264+
};
265+
266+
mini_bddt u; // return value
267+
268+
std::stack<stack_elementt> stack;
269+
stack.push(stack_elementt(u, _x, _y));
270+
271+
while(!stack.empty())
272+
{
273+
auto &t=stack.top();
274+
const mini_bddt &x=t.x;
275+
const mini_bddt &y=t.y;
276+
// NOLINTNEXTLINE(build/deprecated)
277+
assert(x.is_initialized() && y.is_initialized());
278+
// NOLINTNEXTLINE(build/deprecated)
279+
assert(x.node->mgr==y.node->mgr);
280+
281+
switch(t.phase)
282+
{
283+
case stack_elementt::phaset::INIT:
284+
{
285+
// dynamic programming
286+
Gt::const_iterator G_it=G.find(t.key);
287+
if(G_it!=G.end())
288+
{
289+
t.result=G_it->second;
290+
stack.pop();
291+
}
292+
else
293+
{
294+
if(x.is_constant() && y.is_constant())
295+
{
296+
bool result_truth=fkt(x.is_true(), y.is_true());
297+
const mini_bdd_mgrt &mgr=*x.node->mgr;
298+
t.result=result_truth?mgr.True():mgr.False();
299+
stack.pop();
300+
}
301+
else if(x.var()==y.var())
302+
{
303+
t.var=x.var();
304+
t.phase=stack_elementt::phaset::FINISH;
305+
// NOLINTNEXTLINE(build/deprecated)
306+
assert(x.low().var()>t.var);
307+
// NOLINTNEXTLINE(build/deprecated)
308+
assert(y.low().var()>t.var);
309+
// NOLINTNEXTLINE(build/deprecated)
310+
assert(x.high().var()>t.var);
311+
// NOLINTNEXTLINE(build/deprecated)
312+
assert(y.high().var()>t.var);
313+
stack.push(stack_elementt(t.lr, x.low(), y.low()));
314+
stack.push(stack_elementt(t.hr, x.high(), y.high()));
315+
}
316+
else if(x.var()<y.var())
317+
{
318+
t.var=x.var();
319+
t.phase=stack_elementt::phaset::FINISH;
320+
// NOLINTNEXTLINE(build/deprecated)
321+
assert(x.low().var()>t.var);
322+
// NOLINTNEXTLINE(build/deprecated)
323+
assert(x.high().var()>t.var);
324+
stack.push(stack_elementt(t.lr, x.low(), y));
325+
stack.push(stack_elementt(t.hr, x.high(), y));
326+
}
327+
else /* x.var() > y.var() */
328+
{
329+
t.var=y.var();
330+
t.phase=stack_elementt::phaset::FINISH;
331+
// NOLINTNEXTLINE(build/deprecated)
332+
assert(y.low().var()>t.var);
333+
// NOLINTNEXTLINE(build/deprecated)
334+
assert(y.high().var()>t.var);
335+
stack.push(stack_elementt(t.lr, x, y.low()));
336+
stack.push(stack_elementt(t.hr, x, y.high()));
337+
}
338+
}
339+
}
340+
break;
341+
342+
case stack_elementt::phaset::FINISH:
343+
{
344+
mini_bdd_mgrt *mgr=x.node->mgr;
345+
t.result=mgr->mk(t.var, t.lr, t.hr);
346+
G[t.key]=t.result;
347+
stack.pop();
348+
}
349+
break;
350+
}
351+
}
352+
353+
// NOLINTNEXTLINE(build/deprecated)
354+
assert(u.is_initialized());
355+
356+
return u;
357+
}
358+
243359
bool equal_fkt(bool x, bool y)
244360
{
245361
return x==y;
@@ -262,6 +378,7 @@ mini_bddt mini_bddt::operator^(const mini_bddt &other) const
262378

263379
mini_bddt mini_bddt::operator!() const
264380
{
381+
// NOLINTNEXTLINE(build/deprecated)
265382
assert(is_initialized());
266383
return node->mgr->True()^*this;
267384
}
@@ -304,8 +421,11 @@ mini_bddt mini_bdd_mgrt::mk(
304421
const mini_bddt &low,
305422
const mini_bddt &high)
306423
{
424+
// NOLINTNEXTLINE(build/deprecated)
307425
assert(var<=var_table.size());
426+
// NOLINTNEXTLINE(build/deprecated)
308427
assert(low.var()>var);
428+
// NOLINTNEXTLINE(build/deprecated)
309429
assert(high.var()>var);
310430

311431
if(low.node_number()==high.node_number())
@@ -399,6 +519,7 @@ mini_bddt restrictt::RES(const mini_bddt &u)
399519
{
400520
// replace 'var' in 'u' by constant 'value'
401521

522+
// NOLINTNEXTLINE(build/deprecated)
402523
assert(u.is_initialized());
403524
mini_bdd_mgrt *mgr=u.node->mgr;
404525

0 commit comments

Comments
 (0)