miniBDD: added a non-recursive variant of APPLY #1144

kroening · 2017-07-15T14:24:26Z

This adds a non-recursive variant of APPLY, for systems that have limited stacks.
The commit retains the recursive variant, which is much easier to read.

kroening · 2017-07-15T14:24:39Z

A performance comparison would be interesting.

tautschnig

See detailed comments plus all the linter's complaints.

tautschnig · 2017-07-17T06:41:51Z

src/solvers/miniBDD/miniBDD.cpp


  G[key]=u;

  return u;
 }

+mini_bddt mini_bdd_applyt::APP_non_rec(const mini_bddt &_x, const mini_bddt &_y)
+{
+  struct e


Contesting for the least descriptive type name of the year? :-) In absence of any comment, this isn't exactly helping readability.

it should also end on t

e -> et? ;)

technically, t would be ok

tautschnig · 2017-07-17T06:45:07Z

src/solvers/miniBDD/miniBDD.cpp

+      break;
+
+    default:
+      assert(false);


There is no case other than INIT or FINISH, the default is unnecessary.

tautschnig · 2017-07-17T06:47:16Z

src/solvers/miniBDD/miniBDD.cpp

+    e(mini_bddt &_result, const mini_bddt &_x, const mini_bddt &_y):
+      result(_result), x(_x), y(_y), var(0), phase(INIT) { }
+    mini_bddt &result, x, y, lr, hr;
+    std::pair<unsigned, unsigned> key;


Why is key not being initialised? (It is done via a separate assignment later on for some reason.)

mgudemann · 2017-07-17T10:14:41Z

src/solvers/miniBDD/miniBDD.cpp


  G[key]=u;

  return u;
 }

+mini_bddt mini_bdd_applyt::APP_non_rec(const mini_bddt &_x, const mini_bddt &_y)
+{
+  struct e


it should also end on t

mgudemann · 2017-07-17T11:25:17Z

src/solvers/miniBDD/miniBDD.cpp

+    mini_bddt &result, x, y, lr, hr;
+    std::pair<unsigned, unsigned> key;
+    unsigned var;
+    enum { INIT, FINISH } phase;


I'd prefer

enum class phaset { INIT, FINISH}; phaset phase;

mgudemann · 2017-07-17T11:28:41Z

src/solvers/miniBDD/miniBDD.cpp

+    }
+  }
+
+  assert(u.is_initialized());


should be POSTCONDITION

mgudemann · 2017-07-17T11:29:57Z

src/solvers/miniBDD/miniBDD.cpp

+            assert(x.low().var()>t.var);
+            assert(y.low().var()>t.var);
+            assert(x.high().var()>t.var);
+            assert(y.high().var()>t.var);


INVARIANT instead of assert

This is un-obvious: there is some intent to maintain MiniBDD as a library that can be separately distributed.

In that case please add linter overrides (and possibly the above explanation).

mgudemann · 2017-07-17T11:41:00Z

@kroening I did some tests with EBMC on 4 smv models from AIG_SMV_08.tgz. Those were the ones I found that required less than 1m and more than just 1s. So the non-recursive variant is quicker on the micro-benchmark

Name	Status	recursive	non-recursive
bj08vendingcycle.aig.smv	KO	45.3s	41.8s
pdtvisvending06.aig.smv	OK	7.6s	6.3s
pdtvisrethersqo1.aig.smv	OK	43.8s	29.9s
pdtvisvending03.aig.smv	OK	8.7s	7.1s

this is average run-time over 10 runs, with the patch for operator< applied, only difference is

commit db2da98cee960e4601dccc8c0cd34f73b11ff325
Author: Daniel Kroening <[email protected]>
Date:   Sat Jul 15 15:23:11 2017 +0100

    added a non-recursive variant of APPLY

kroening · 2017-07-17T14:59:27Z

@mgudemann oh, wow, this is bigger than I thought it would be.

mgudemann · 2017-07-17T15:51:48Z

@kroening I'll see whether I find others that use a non-trivial amount of time and also do not require excessive resources when using BDDs. The above are all converted from AIG, that may skew the results a bit. I'll see whether I find other .smv or Verilog files.

kroening · 2017-07-19T11:58:18Z

Ready to go?

mgudemann · 2017-07-19T15:41:31Z

I did a small benchmark on the .sv files of the regression tests which are compatible with the BDD engine

name	status	recursive	non-recursive
viseisenberg.sv	KO	4.53	4.42
eijks208o.sv	OK	24.3	25.27
bobcount.sv	OK	0.36	0.39
visbakery.sv	KO	38.89	39.15

which shows a very slight advantage for the recursive variant with the exception of the first model. In conclusion I think the recursive version can be significantly worse (maybe if the recursion depth is very high?) and in the best case is slighly better (as it is shorter / less complex?)

Overall, this is ready for merge.

tautschnig · 2017-07-19T22:15:26Z

src/solvers/miniBDD/miniBDD.cpp

+          {
+            t.var=x.var();
+            t.phase=stack_elementt::phaset::FINISH;
+            assert(x.low().var()>t.var);


Linter overrides, please.

tautschnig · 2017-07-19T22:16:13Z

src/solvers/miniBDD/miniBDD.cpp

+    case stack_elementt::phaset::INIT:
+      {
+        // dynamic programming
+        t.key=std::pair<unsigned, unsigned>(x.node_number(), y.node_number());


I think I've asked this before: why is this not part of the constructor?

As said before I'm unhappy about the absence of tests, but I don't want to stand in the way of others approving of this.

peterschrammel · 2017-08-01T15:01:57Z

src/solvers/miniBDD/miniBDD.cpp

@@ -22,6 +22,7 @@ Author: Daniel Kroening, [email protected]

 void mini_bdd_nodet::remove_reference()
 {
+  // NOLINTNEXTLINE(build/deprecated)


Use PRECONDITION(), INVARIANT(), etc from https://github.com/diffblue/cbmc/blob/master/src/util/invariant.h rather than silencing the linter.

See #1144 (comment).

kroening requested review from tautschnig and mgudemann July 15, 2017 14:25

tautschnig previously requested changes Jul 17, 2017

View reviewed changes

mgudemann suggested changes Jul 17, 2017

View reviewed changes

kroening force-pushed the miniBDD-non-recursive-apply branch from db2da98 to 8a8f5f2 Compare July 17, 2017 15:18

kroening force-pushed the miniBDD-non-recursive-apply branch from 8a8f5f2 to bda4ec5 Compare July 19, 2017 11:58

mgudemann approved these changes Jul 19, 2017

View reviewed changes

tautschnig reviewed Jul 19, 2017

View reviewed changes

Daniel Kroening added 2 commits July 20, 2017 22:32

added a non-recursive variant of APPLY

564f64c

disable linter for assertions

a71ca41

kroening force-pushed the miniBDD-non-recursive-apply branch from bda4ec5 to a71ca41 Compare July 20, 2017 21:32

peterschrammel added the enhancement label Aug 1, 2017

peterschrammel reviewed Aug 1, 2017

View reviewed changes

kroening merged commit 8e70eaa into master Aug 3, 2017

kroening deleted the miniBDD-non-recursive-apply branch August 3, 2017 20:51

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

miniBDD: added a non-recursive variant of APPLY #1144

miniBDD: added a non-recursive variant of APPLY #1144

kroening commented Jul 15, 2017

kroening commented Jul 15, 2017

tautschnig left a comment

tautschnig Jul 17, 2017

mgudemann Jul 17, 2017

kroening Jul 17, 2017

mgudemann Jul 19, 2017

tautschnig Jul 17, 2017

kroening Jul 19, 2017

tautschnig Jul 17, 2017

mgudemann Jul 17, 2017

mgudemann Jul 17, 2017

mgudemann Jul 17, 2017

mgudemann Jul 17, 2017

kroening Jul 17, 2017

tautschnig Jul 17, 2017

mgudemann commented Jul 17, 2017

kroening commented Jul 17, 2017

mgudemann commented Jul 17, 2017

kroening commented Jul 19, 2017

mgudemann commented Jul 19, 2017

tautschnig Jul 19, 2017

kroening Jul 20, 2017

tautschnig Jul 19, 2017

kroening Jul 20, 2017

peterschrammel Aug 1, 2017

tautschnig Aug 1, 2017

peterschrammel Aug 1, 2017

miniBDD: added a non-recursive variant of APPLY #1144

miniBDD: added a non-recursive variant of APPLY #1144

Conversation

kroening commented Jul 15, 2017

kroening commented Jul 15, 2017

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mgudemann commented Jul 17, 2017

kroening commented Jul 17, 2017

mgudemann commented Jul 17, 2017

kroening commented Jul 19, 2017

mgudemann commented Jul 19, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment