Mucke

News

The new source release version 0.4.6 is a port to gcc 4.1.3.

Switched to BSD license.

Issues

The current release forces the former flag '-ret' to be asserted all the time and fixes a bug in the rangify code. Now it is possible to specify bit access for enumeration access symbols inside of classes:

enum E { reg, green, blue };
class C { E a, b; };

bool f(C c) c.a = c.b;
bool g(C c) c.a[0] = c.b[0] & c.a[1] = c.b[1];

forall C c. f(c) <-> g(c);

This should actually produce the same BDD for both f and g. Finally we introduced a new flag '-df' which allows to divert the dump of a predicate to a file. The name of the file is the name of the predicate with a '.dump' suffix.

Download

[ mucke-0.4.6.tar.gz ]

Since Mucke is written in C++ and the language C++ compilers accept has been quite a moving target in the past, you are on your own when trying to compile Mucke with a recent C++ compiler.

License

We use a variant of a BSD style license, which allows the use of Mucke in any way you want, provided you acknowledge the work of the original author in an approriate way as detailed in the COPYRIGHT notice which comes with the sources.

Notes

As in former releases, Mucke is configured with the BDD library ABCD as default. During initialization ABCD tries to grab half of all the available memory. This may slow down the start up of Mucke quite a bit. To restrict the initial memory usage, you can generate a '.abcdbmanrc' file that contains a line saying 'MB 10' that tells 'abcdbman' to use only the given amount of memory, e.g. 10 MB in this case, initially.

You can also just give '-bman simplebman.so' or '-bman longbman.so' as commmand line options to Mucke. These options tell Mucke to use the BDD library BDDSimple respectively the BDD library of David Long instead of ABCD.

Old Versions

[ mucke-0.4.5.tar.gz ]