CUDD: CU Decision Diagram package - unofficial git mirror of https://web.archive.org/web/20180127051756/http://vlsi.colorado.edu/~fabio/CUDD/html/index.html (intro: https://web.archive.org/web/20150215010018/http://vlsi.colorado.edu/~fabio/CUDD/cuddIntro.html)
License: BSD 3-Clause "New" or "Revised" License
The CUDD package is a package written in C for the manipulation of
decision diagrams. It supports binary decision diagrams (BDDs),
algebraic decision diagrams (ADDs), and Zero-Suppressed BDDs (ZDDs).
This directory contains a set of packages that allow you to build a test
application based on the CUDD package.
The test application provided in this kit is called nanotrav and is a
simple-minded FSM traversal program. (See the README file and the man
page nanotrav.1 in the nanotrav directory for the details.) It is
included so that you can run a sanity check on your installation.
Also included in this distribution are the dddmp libray by Giampiero
Cabodi and Stefano Quer and a C++ object-oriented wrapper for CUDD.
BUILD AND INSTALLATION
In the simplest form, you can build the static libraries with:
./configure
make
make check
The configure script provides a few options, which can be listed with
./configure --help
Notable options include
--enable-silent-rules
--enable-shared
--enable-dddmp
--enable-obj
--with-system-qsort
The --enable-silent-rules option is a standard option that streamlines the
messages produced by the build process. The remaining options are specific
to CUDD.
The three "enable" options control the build of shared libraries. By
default, only static libraries are built. With --enable-shared, a
shared library for libcudd is built. (Before installation, it can be
found in cudd/.libs.)
The last two "enable" options control the inclusion of the dddmp
library and C++ wrapper in the shared library, which by default only
contains the core CUDD library.
The --with-system-qsort option requests use of the qsort from the
standard library instead of the portable one shipped with CUDD. This
option is provided for backward compatibility and is not otherwise
recommended. Some of the tests of "make check" may fail with the
system qsort because variable orders may be generated that are
different from the reference ones.
As an example, a more elaborate build command sequence may be:
./configure CC=clang CXX=clang++ --enable-silent-rules \
--enable-shared --enable-obj
make -j4 check
make install
which selects alternate compilers instead of gcc and g++, causes the
C++ wrapper to be included in the shared library, enables parallel
compilation (with -j4) and finally installs the shared library using
the default prefix /usr/local.
For those unfamiliar with libtool it may be worth noting that the
libraries it builds go in .libs subdirectories. One should also note
that with shared libraries enabled, the test programs immediately
visible to the user are shell scripts that make sure dynamic linking
works before installation. If you want to run valgrind on, say, a
dynamically linked nanotrav, specify the option --trace-children=yes.
PLATFORMS
This kit has been successfully built on the following configurations:
PC (x86 and x86_64) running Ubuntu with gcc and clang
PC (x86 and x86_64) running Ubuntu with g++
PC (x86 and x86_64) running Linux RedHat with gcc
PC (x86 and x86_64) running Linux RedHat with g++
PC (x86_64) running 32-bit Cygwin on Windows 7 and Vista with gcc
PC (x86_64) running 32-bit Cygwin on Windows 7 and Vista with g++
PC (x86_64) running 64-bit Cygwin on Windows 8.1 with gcc and g++
PC (x86_64) running MinGW-w64 on Windows 8.1 with gcc
In all these cases, the C++ wrapper was compiled with the matching C++
compiler (g++ for gcc and clang++ for clang). To compile under MSYS2
(MinGW-w64) one has to pass --build=x86_64-w64-mingw32 to ./configure.
SANITY CHECK
The directory `nanotrav' contains a simple application based on the
CUDD package. The `nanotrav' directory contains a man page that
describes the options nanotrav supports. The files *.blif are sample
input files for nanotrav. The *.out files are the reference output
files.
DOCUMENTATION
If doxygen is installed, running "make" puts HTML documentation for
the CUDD package in directory cudd-3.0.0/cudd/html. The recommended
starting point is index.html. The user's manual in PDF format is
built in cudd-3.0.0/doc if pdflatex and makeindex are installed.
Documentation for the dddmp library is in the dddmp/doc subdirectory.
FEEDBACK:
Send feedback to:
Fabio Somenzi
University of Colorado at Boulder
ECE Dept.
Boulder, CO 80309-0425
[email protected]
http://vlsi.colorado.edu/~fabio
During installation, at make, i get
CDPATH="${ZSH_VERSION+.}:" && cd . && /bin/bash /home/numair/Pictures/cudd/build-aux/missing aclocal-1.14 -I m4
/home/numair/Pictures/cudd/build-aux/missing: line 81: aclocal-1.14: command not found
WARNING: 'aclocal-1.14' is missing on your system.
You should only need it if you modified 'acinclude.m4' or
'configure.ac' or m4 files included by 'configure.ac'.
The 'aclocal' program is part of the GNU Automake package:
<http://www.gnu.org/software/automake>
It also requires GNU Autoconf, GNU m4 and Perl in order to run:
<http://www.gnu.org/software/autoconf>
<http://www.gnu.org/software/m4/>
<http://www.perl.org/>
Makefile:983: recipe for target 'aclocal.m4' failed
make: *** [aclocal.m4] Error 127
$ aclocal --version
aclocal (GNU automake) 1.15
Copyright (C) 2014 Free Software Foundation, Inc.
License GPLv2+: GNU GPL version 2 or later <http://gnu.org/licenses/gpl-2.0.html>
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.
Written by Tom Tromey <[email protected]>
and Alexandre Duret-Lutz <[email protected]>.
Hello,
I am using CUDD package for creating BDD from the given benchmark and then storing that BDD in a file, for one of my projects.
I have created the BDD, but I have a hard time storing that BDD in a file.
I have attached one simple example where I am creating the BDD and viewing it also.
test.txt
Can you walk me through storing the BDD in a file? Because struct like dddmpVarInfo has many variables and I am guessing we don't have to write each and every variable on our own?
Thanks and Regards,
Sincerely,
Aadil Hoda
IIT Guwahati, India
Hi, @ivmai
I've been using the cudd classic (in C), but wanted to try the C++ because of the much greater facility in constructing Boolean functions. I've been using it mainly to convert coherent (non-decreasing) Booleans to BDD to find all the minterms. So I would like to do something such as below (at much larger scale, with 1000s of vars). I was using the C function Cudd_PrintDebug(gbm, BDD, 2, 4); -- which gave me everything I needed, minterms and the var mapping.
Can you help me with the equivalent C++ interface function? Or refer me to the documentation? I've found function descriptors for C but not for C++.
`/* Top=a(b+c+de)./
int main()
{
Cudd mgr(0, 0);
BDD a = mgr.bddVar();
BDD b = mgr.bddVar();
BDD c = mgr.bddVar();
BDD d = mgr.bddVar();
BDD e = mgr.bddVar();
BDD top = a(b + c + d*e);
Cudd_PrintSummary(mgr, top, 2, 4);
/*Cudd_PrintMinterm(mgr, top)*/
/*int Cudd_EpdPrintMinterm(DdManager const * dd, DdNode * node, int nvars);*/
/*Cudd_EpdPrintMinterm(mgr, top, 5)*/
return 0
}`
The above doesn't work. Any pointers much appreciated!
Gui
There is no good dot tree dump for cudd... I wrote this one several years ago...
Please include the following function to cuddexport.c
in the cudd.h file include the following.. .
function declaration...
extern int Cudd_DumpDotTree (DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp);
in the file cuddexport.c add the following function...
/Function******************************************************************
Synopsis [Writes a dot file representing the argument DDs.]
Description [Writes a file representing the argument DDs in a format
suitable for the graph drawing program dot.
It returns 1 in case of success; 0 otherwise (e.g., out-of-memory,
file system full).
Cudd_DumpDot does not close the file: This is the caller
responsibility. Cudd_DumpDot uses a minimal unique subset of the
hexadecimal address of a node as name for it.
If the argument inames is non-null, it is assumed to hold the pointers
to the names of the inputs. Similarly for onames.
Cudd_DumpDot uses the following convention to draw arcs:
SideEffects [None]
SeeAlso [Cudd_DumpBlif Cudd_PrintDebug Cudd_DumpDDcal
Cudd_DumpDaVinci Cudd_DumpFactoredForm]
*****************************************************************************/
int
Cudd_DumpDotTree(
DdManager * dd / manager /,
int n / number of output nodes to be dumped /,
DdNode ** f / array of output nodes to be dumped /,
char ** inames / array of input names (or NULL) /,
char ** onames / array of output names (or NULL) /,
FILE * fp / pointer to the dump file */)
{
DdNode *support = NULL;
DdNode *scan;
int *sorted = NULL;
int nvars = dd->size;
st_table *visited = NULL;
st_generator *gen = NULL;
int retval;
int i, j;
int slots;
DdNodePtr *nodelist;
long refAddr, diff, mask;
/* Build a bit array with the support of f. */
sorted = ALLOC(int,nvars);
if (sorted == NULL) {
dd->errorCode = CUDD_MEMORY_OUT;
goto failure;
}
for (i = 0; i < nvars; i++) sorted[i] = 0;
/* Take the union of the supports of each output function. */
support = Cudd_VectorSupport(dd,f,n);
if (support == NULL) goto failure;
cuddRef(support);
scan = support;
while (!cuddIsConstant(scan)) {
sorted[scan->index] = 1;
scan = cuddT(scan);
}
Cudd_RecursiveDeref(dd,support);
support = NULL; /* so that we do not try to free it in case of failure */
/* Initialize symbol table for visited nodes. */
visited = st_init_table(st_ptrcmp, st_ptrhash);
if (visited == NULL) goto failure;
/* Collect all the nodes of this DD in the symbol table. */
for (i = 0; i < n; i++) {
retval = cuddCollectNodes(Cudd_Regular(f[i]),visited);
if (retval == 0) goto failure;
}
/* Find how many most significant hex digits are identical
** in the addresses of all the nodes. Build a mask based
** on this knowledge, so that digits that carry no information
** will not be printed. This is done in two steps.
** 1. We scan the symbol table to find the bits that differ
** in at least 2 addresses.
** 2. We choose one of the possible masks. There are 8 possible
** masks for 32-bit integer, and 16 possible masks for 64-bit
** integers.
*/
/* Find the bits that are different. */
refAddr = (long) Cudd_Regular(f[0]);
diff = 0;
gen = st_init_gen(visited);
if (gen == NULL) goto failure;
while (st_gen(gen, &scan, NULL)) {
diff |= refAddr ^ (long) scan;
}
st_free_gen(gen); gen = NULL;
/* Choose the mask. */
for (i = 0; (unsigned) i < 8 * sizeof(long); i += 4) {
mask = (1 << i) - 1;
if (diff <= mask) break;
}
/* Write the header and the global attributes. */
retval = fprintf(fp,"digraph \"DD\" {\n");
if (retval == EOF) return(0);
retval = fprintf(fp,
"size = \"7.5,10\"\ncenter = true;\nedge [dir = none];\n");
if (retval == EOF) return(0);
/* Write the input name subgraph by scanning the support array. */
retval = fprintf(fp,"{ node [shape = plaintext];\n");
if (retval == EOF) goto failure;
retval = fprintf(fp," edge [style = invis];\n");
if (retval == EOF) goto failure;
/* We use a name ("CONST NODES") with an embedded blank, because
** it is unlikely to appear as an input name.
*/
retval = fprintf(fp," \"CONST NODES\" [style = invis];\n");
if (retval == EOF) goto failure;
for (i = 0; i < nvars; i++) {
if (sorted[dd->invperm[i]]) {
if (inames == NULL || inames[dd->invperm[i]] == NULL) {
retval = fprintf(fp,"\" %d \" -> ", dd->invperm[i]);
} else {
retval = fprintf(fp,"\" %s \" -> ", inames[dd->invperm[i]]);
}
if (retval == EOF) goto failure;
}
}
retval = fprintf(fp,"\"CONST NODES\"; \n}\n");
if (retval == EOF) goto failure;
/* Write the output node subgraph. */
retval = fprintf(fp,"{ rank = same; node [shape = box]; edge [style = invis];\n");
if (retval == EOF) goto failure;
for (i = 0; i < n; i++) {
if (onames == NULL) {
retval = fprintf(fp,"\"F%d\"", i);
} else {
retval = fprintf(fp,"\" %s \"", onames[i]);
}
if (retval == EOF) goto failure;
if (i == n - 1) {
retval = fprintf(fp,"; }\n");
} else {
retval = fprintf(fp," -> ");
}
if (retval == EOF) goto failure;
}
/* Write rank info: All nodes with the same index have the same rank. */
for (i = 0; i < nvars; i++) {
if (sorted[dd->invperm[i]]) {
retval = fprintf(fp,"{ rank = same; ");
if (retval == EOF) goto failure;
if (inames == NULL || inames[dd->invperm[i]] == NULL) {
retval = fprintf(fp,"\" %d \";\n", dd->invperm[i]);
} else {
retval = fprintf(fp,"\" %s \";\n", inames[dd->invperm[i]]);
}
if (retval == EOF) goto failure;
nodelist = dd->subtables[i].nodelist;
slots = dd->subtables[i].slots;
for (j = 0; j < slots; j++) {
scan = nodelist[j];
while (scan != NULL) {
if (st_is_member(visited,(char *) scan)) {
retval = fprintf(fp,"\"%lx\";\n",
(unsigned long) ((mask & (long) scan) /
sizeof(DdNode)));
if (retval == EOF) goto failure;
}
scan = scan->next;
}
}
retval = fprintf(fp,"}\n");
if (retval == EOF) goto failure;
}
}
/* All constants have the same rank. */
retval = fprintf(fp,
"{ rank = same; \"CONST NODES\";\n{ node [shape = box]; ");
if (retval == EOF) goto failure;
nodelist = dd->constants.nodelist;
slots = dd->constants.slots;
for (j = 0; j < slots; j++) {
scan = nodelist[j];
while (scan != NULL) {
if (st_is_member(visited,(char *) scan)) {
retval = fprintf(fp,"\"%lx\";\n",
(unsigned long) ((mask & (long) scan) / sizeof(DdNode)));
if (retval == EOF) goto failure;
}
scan = scan->next;
}
}
retval = fprintf(fp,"}\n}\n");
if (retval == EOF) goto failure;
/* Write edge info. */
/* Edges from the output nodes. */
for (i = 0; i < n; i++) {
if (onames == NULL) {
retval = fprintf(fp,"\"F%d\"", i);
} else {
retval = fprintf(fp,"\" %s \"", onames[i]);
}
if (retval == EOF) goto failure;
/* Account for the possible complement on the root. */
if (Cudd_IsComplement(f[i])) {
retval = fprintf(fp," -> \"%lx\" [style = dotted];\n",
(unsigned long) ((mask & (long) f[i]) / sizeof(DdNode)));
} else {
retval = fprintf(fp," -> \"%lx\" [style = solid];\n",
(unsigned long) ((mask & (long) f[i]) / sizeof(DdNode)));
}
if (retval == EOF) goto failure;
}
/* Edges from internal nodes. */
for (i = 0; i < nvars; i++) {
if (sorted[dd->invperm[i]]) {
nodelist = dd->subtables[i].nodelist;
slots = dd->subtables[i].slots;
for (j = 0; j < slots; j++) {
scan = nodelist[j];
while (scan != NULL) {
if (st_is_member(visited,(char *) scan)) {
retval = fprintf(fp,
"\"%lx\" -> \"%lx\";\n",
(unsigned long) ((mask & (long) scan) /
sizeof(DdNode)),
(unsigned long) ((mask & (long) cuddT(scan)) /
sizeof(DdNode)));
if (retval == EOF) goto failure;
unsigned long parent = 0U;
if (Cudd_IsComplement(cuddE(scan)))
{
retval = fprintf(fp,
"\"%lx\" -> \"FAIL\" [style = dotted];\n",
(unsigned long) ((mask & (long) scan) /
sizeof(DdNode)),
(unsigned long) ((mask & (long) cuddE(scan)) /
sizeof(DdNode)));
}
else
{
retval = fprintf(fp,
"\"%lx\" -> \"%lx\" [style = dashed];\n",
(unsigned long) ((mask & (long) scan) /
sizeof(DdNode)),
(unsigned long) ((mask & (long) cuddE(scan)) /
sizeof(DdNode)));
}
#ifdef ORIG
if (Cudd_IsComplement(cuddE(scan))) {
retval = fprintf(fp,
"\"%lx\" -> \"%lx\" [style = dotted];\n",
(unsigned long) ((mask & (long) scan) /
sizeof(DdNode)),
(unsigned long) ((mask & (long) cuddE(scan)) /
sizeof(DdNode)));
} else {
retval = fprintf(fp,
"\"%lx\" -> \"%lx\" [style = dashed];\n",
(unsigned long) ((mask & (long) scan) /
sizeof(DdNode)),
(unsigned long) ((mask & (long) cuddE(scan)) /
sizeof(DdNode)));
}
#endif
if (retval == EOF) goto failure;
}
scan = scan->next;
}
}
}
}
/* Write constant labels. */
nodelist = dd->constants.nodelist;
slots = dd->constants.slots;
for (j = 0; j < slots; j++) {
scan = nodelist[j];
while (scan != NULL) {
if (st_is_member(visited,(char *) scan)) {
retval = fprintf(fp,"\"%lx\" [label = \"%g\"];\n",
(unsigned long) ((mask & (long) scan) / sizeof(DdNode)),
cuddV(scan));
if (retval == EOF) goto failure;
}
scan = scan->next;
}
}
/* Write trailer and return. */
retval = fprintf(fp,"}\n");
if (retval == EOF) goto failure;
st_free_table(visited);
FREE(sorted);
return(1);
failure:
if (sorted != NULL) FREE(sorted);
if (support != NULL) Cudd_RecursiveDeref(dd,support);
if (visited != NULL) st_free_table(visited);
return(0);
}
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
Django
The Web framework for perfectionists with deadlines.
Laravel
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
Microsoft
Open source projects and samples from Microsoft.
Google
Google ❤️ Open Source for everyone.
Alibaba
Alibaba Open Source for everyone
D3
Data-Driven Documents codes.
Tencent
China tencent open source team.