Skip to content

Commit e0dbf2a

Browse files
petr-bauchpetr-bauch
authored
Merge pull request #2959 from xbauch/cleanup_minibdd
Cleanup error handling in solvers/miniBDD
2 parents f5d5715 + 004a4a4 commit e0dbf2a

File tree

2 files changed

+62
-49
lines changed

2 files changed

+62
-49
lines changed

‎src/solvers/miniBDD/miniBDD.cpp‎

Lines changed: 51 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
1313

1414
#include "miniBDD.h"
1515

16-
#include <cassert>
16+
#include <util/invariant.h>
1717

1818
#include <iostream>
1919

@@ -22,8 +22,8 @@ Author: Daniel Kroening, kroening@kroening.com
2222

2323
void mini_bdd_nodet::remove_reference()
2424
{
25-
// NOLINTNEXTLINE(build/deprecated)
26-
assert(reference_counter!=0);
25+
PRECONDITION_WITH_DIAGNOSTICS(
26+
reference_counter != 0, "all references were already removed");
2727

2828
reference_counter--;
2929

@@ -209,10 +209,12 @@ class mini_bdd_applyt
209209

210210
mini_bddt mini_bdd_applyt::APP_rec(const mini_bddt &x, const mini_bddt &y)
211211
{
212-
// NOLINTNEXTLINE(build/deprecated)
213-
assert(x.is_initialized() && y.is_initialized());
214-
// NOLINTNEXTLINE(build/deprecated)
215-
assert(x.node->mgr==y.node->mgr);
212+
PRECONDITION_WITH_DIAGNOSTICS(
213+
x.is_initialized() && y.is_initialized(),
214+
"apply can only be called on initialized BDDs");
215+
PRECONDITION_WITH_DIAGNOSTICS(
216+
x.node->mgr == y.node->mgr,
217+
"apply can only be called on BDDs with the same manager");
216218

217219
// dynamic programming
218220
std::pair<unsigned, unsigned> key(x.node_number(), y.node_number());
@@ -273,10 +275,13 @@ mini_bddt mini_bdd_applyt::APP_non_rec(
273275
auto &t=stack.top();
274276
const mini_bddt &x=t.x;
275277
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);
278+
279+
INVARIANT(
280+
x.is_initialized() && y.is_initialized(),
281+
"apply can only be called on initialized BDDs");
282+
INVARIANT(
283+
x.node->mgr == y.node->mgr,
284+
"apply can only be called on BDDs with the same manager");
280285

281286
switch(t.phase)
282287
{
@@ -302,36 +307,42 @@ mini_bddt mini_bdd_applyt::APP_non_rec(
302307
{
303308
t.var=x.var();
304309
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);
310+
311+
INVARIANT(
312+
x.low().var() > t.var, "applying won't break variable order");
313+
INVARIANT(
314+
y.low().var() > t.var, "applying won't break variable order");
315+
INVARIANT(
316+
x.high().var() > t.var, "applying won't break variable order");
317+
INVARIANT(
318+
y.high().var() > t.var, "applying won't break variable order");
319+
313320
stack.push(stack_elementt(t.lr, x.low(), y.low()));
314321
stack.push(stack_elementt(t.hr, x.high(), y.high()));
315322
}
316323
else if(x.var()<y.var())
317324
{
318325
t.var=x.var();
319326
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);
327+
328+
INVARIANT(
329+
x.low().var() > t.var, "applying won't break variable order");
330+
INVARIANT(
331+
x.high().var() > t.var, "applying won't break variable order");
332+
324333
stack.push(stack_elementt(t.lr, x.low(), y));
325334
stack.push(stack_elementt(t.hr, x.high(), y));
326335
}
327336
else /* x.var() > y.var() */
328337
{
329338
t.var=y.var();
330339
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);
340+
341+
INVARIANT(
342+
y.low().var() > t.var, "applying won't break variable order");
343+
INVARIANT(
344+
y.high().var() > t.var, "applying won't break variable order");
345+
335346
stack.push(stack_elementt(t.lr, x, y.low()));
336347
stack.push(stack_elementt(t.hr, x, y.high()));
337348
}
@@ -350,8 +361,8 @@ mini_bddt mini_bdd_applyt::APP_non_rec(
350361
}
351362
}
352363

353-
// NOLINTNEXTLINE(build/deprecated)
354-
assert(u.is_initialized());
364+
POSTCONDITION_WITH_DIAGNOSTICS(
365+
u.is_initialized(), "the resulting BDD is initialized");
355366

356367
return u;
357368
}
@@ -378,8 +389,8 @@ mini_bddt mini_bddt::operator^(const mini_bddt &other) const
378389

379390
mini_bddt mini_bddt::operator!() const
380391
{
381-
// NOLINTNEXTLINE(build/deprecated)
382-
assert(is_initialized());
392+
PRECONDITION_WITH_DIAGNOSTICS(
393+
is_initialized(), "BDD has to be initialized for negation");
383394
return node->mgr->True()^*this;
384395
}
385396

@@ -421,12 +432,13 @@ mini_bddt mini_bdd_mgrt::mk(
421432
const mini_bddt &low,
422433
const mini_bddt &high)
423434
{
435+
PRECONDITION_WITH_DIAGNOSTICS(
436+
var <= var_table.size(), "cannot make a BDD for an unknown variable");
437+
PRECONDITION_WITH_DIAGNOSTICS(
438+
low.var() > var, "low-edge would break variable ordering");
424439
// NOLINTNEXTLINE(build/deprecated)
425-
assert(var<=var_table.size());
426-
// NOLINTNEXTLINE(build/deprecated)
427-
assert(low.var()>var);
428-
// NOLINTNEXTLINE(build/deprecated)
429-
assert(high.var()>var);
440+
PRECONDITION_WITH_DIAGNOSTICS(
441+
high.var() > var, "high-edge would break variable ordering");
430442

431443
if(low.node_number()==high.node_number())
432444
return low;
@@ -525,8 +537,9 @@ mini_bddt restrictt::RES(const mini_bddt &u)
525537
{
526538
// replace 'var' in 'u' by constant 'value'
527539

528-
// NOLINTNEXTLINE(build/deprecated)
529-
assert(u.is_initialized());
540+
PRECONDITION_WITH_DIAGNOSTICS(
541+
u.is_initialized(),
542+
"restricting variables can only be done in initialized BDDs");
530543
mini_bdd_mgrt *mgr=u.node->mgr;
531544

532545
mini_bddt t;

‎src/solvers/miniBDD/miniBDD.inc‎

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
#include <cassert>
1+
#include <util/invariant.h>
22

33
// inline functions
44

@@ -18,7 +18,7 @@ inline mini_bddt::mini_bddt(class mini_bdd_nodet *_node):node(_node)
1818

1919
inline mini_bddt &mini_bddt::operator=(const mini_bddt &x)
2020
{
21-
assert(&x!=this);
21+
PRECONDITION_WITH_DIAGNOSTICS(&x != this, "cannot assign itself");
2222
clear();
2323

2424
node=x.node;
@@ -35,45 +35,45 @@ inline mini_bddt::~mini_bddt()
3535

3636
inline bool mini_bddt::is_constant() const
3737
{
38-
assert(is_initialized());
38+
PRECONDITION_WITH_DIAGNOSTICS(is_initialized(), "BDD has to be initialized");
3939
return node->node_number<=1;
4040
}
4141

4242
inline bool mini_bddt::is_true() const
4343
{
44-
assert(is_initialized());
44+
PRECONDITION_WITH_DIAGNOSTICS(is_initialized(), "BDD has to be initialized");
4545
return node->node_number==1;
4646
}
4747

4848
inline bool mini_bddt::is_false() const
4949
{
50-
assert(is_initialized());
50+
PRECONDITION_WITH_DIAGNOSTICS(is_initialized(), "BDD has to be initialized");
5151
return node->node_number==0;
5252
}
5353

5454
inline unsigned mini_bddt::var() const
5555
{
56-
assert(is_initialized());
56+
PRECONDITION_WITH_DIAGNOSTICS(is_initialized(), "BDD has to be initialized");
5757
return node->var;
5858
}
5959

6060
inline unsigned mini_bddt::node_number() const
6161
{
62-
assert(is_initialized());
62+
PRECONDITION_WITH_DIAGNOSTICS(is_initialized(), "BDD has to be initialized");
6363
return node->node_number;
6464
}
6565

6666
inline const mini_bddt &mini_bddt::low() const
6767
{
68-
assert(is_initialized());
69-
assert(node->node_number>=2);
68+
PRECONDITION_WITH_DIAGNOSTICS(is_initialized(), "BDD has to be initialized");
69+
PRECONDITION_WITH_DIAGNOSTICS(node->node_number >= 2, "only non-terminal nodes have out-going edges");
7070
return node->low;
7171
}
7272

7373
inline const mini_bddt &mini_bddt::high() const
7474
{
75-
assert(is_initialized());
76-
assert(node->node_number>=2);
75+
PRECONDITION_WITH_DIAGNOSTICS(is_initialized(), "BDD has to be initialized");
76+
PRECONDITION_WITH_DIAGNOSTICS(node->node_number >= 2, "only non-terminal nodes have out-going edges");
7777
return node->high;
7878
}
7979

0 commit comments

Comments
 (0)