2.12.2021, 9:00 - 11:00: Due to updates GitLab may be unavailable for some minutes between 09:00 and 11:00.

Commit 0202cf09 authored by Mahmoud Khaled's avatar Mahmoud Khaled
Browse files

adding cudd 3.0

parent 99736795
File added
This diff is collapsed.
Copyright (c) 1995-2004, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions
are met:
Redistributions of source code must retain the above copyright
notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its
contributors may be used to endorse or promote products derived from
this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
POSSIBILITY OF SUCH DAMAGE.
ACLOCAL_AMFLAGS = -I m4
include_HEADERS = cudd/cudd.h
if DDDMP
include_HEADERS += dddmp/dddmp.h
endif
if OBJ
include_HEADERS += cplusplus/cuddObj.hh
endif
check_PROGRAMS =
check_SCRIPTS =
dist_check_DATA =
EXTRA_DIST = README RELEASE.NOTES LICENSE groups.dox
TESTS =
CLEANFILES =
noinst_LTLIBRARIES =
TEST_LOG_DRIVER = env AM_TAP_AWK='$(AWK)' $(SHELL) \
$(top_srcdir)/build-aux/tap-driver.sh
do_subst = sed \
-e 's,[@]EXEEXT[@],$(EXEEXT),g' \
-e 's,[@]srcdir[@],$(srcdir),g'
include $(top_srcdir)/cudd/Included.am
include $(top_srcdir)/util/Included.am
include $(top_srcdir)/st/Included.am
include $(top_srcdir)/epd/Included.am
include $(top_srcdir)/mtr/Included.am
include $(top_srcdir)/dddmp/Included.am
include $(top_srcdir)/cplusplus/Included.am
include $(top_srcdir)/nanotrav/Included.am
include $(top_srcdir)/doc/Included.am
dist-hook:
rm -rf `find $(distdir) -name .svn`
.PHONY :
all: html/index.html doc/cudd.pdf
if HAVE_DOXYGEN
html/index.html: Doxyfile $(lib_LTLIBRARIES)
@if $(AM_V_P); then dest='2>&1'; else dest='> /dev/null 2>&1'; fi; \
eval "$(DOXYGEN) $< $${dest}"
clean-local:
rm -rf html doxygen_sqlite3.db
else
html/index.html:
endif
CLEANFILES += $(check_SCRIPTS)
This diff is collapsed.
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
Fabio@Colorado.EDU
http://vlsi.colorado.edu/~fabio
Release 3.0.0 of Cudd uses autotools for its build. It can also
produce a shared library. The shared library contains the core CUDD
functions, and, optionally, the dddmp functions and the C++ wrapper.
It is now safe to use separate CUDD managers in different threads.
There are changes in the API, discussed later. The documentation is
now extracted from the code by Doxygen. About a dozen bugs were fixed
in seldom-used functions.
The switch to autotools means that one no longer needs to edit the
configuration section of the main Makefile. It was also instrumental
in providing shared library support (via libtool) on multiple
platforms and a "check" make target worth its name. Initial support
for cross compilation has been added.
Build time is significantly longer, especially the first time, and
especially when shared libraries are enabled. In return one gets
dependency tracking, support for VPATH builds, packaging of
distributions, and so on.
The CUDD package and its sub-packages now expose significantly fewer
details of their implementations to the applications. It is now
possible to compile a CUDD-based application while including only the
cudd.h header and linking only libcudd.a (or the equivalent shared
library). A few const type qualifiers have been added to APIs too.
Some macros have been turned into functions to improve encapsulation,
namely Cudd_T, Cudd_E, Cudd_V, and Cudd_IsConstant. Another API
change brought about by this restructuring is that the digits of
arbitrary-precision integers are now always 32-bit wide. As a
consequence, the function Cudd_ApaIntDivision is now deprecated.
The malloc/realloc/free wrappers in safe_mem.c have been simplified
and made more consistent with the standard functions. (The majority
of what the wrappers did was supplying functionality that any modern
compliant implementation of C would supply anyway.) Some parts of the
util library are no longer distributed with CUDD. (They were never
used by it.)
Applications that call functions from the mtr or epd packages now have
to explicitly include their headers _before_ including cudd.h.
Applications that access data structures that are no longer exposed
should declare their close kinship with those data structure by
including the internal headers.
There is a new function in the API, Cudd_PrintSummary, that is
analogous to Cudd_PrintDebug, but only prints one line using
arbitrary-precision arithmetic to compute the number of minterms. The
function Cudd_ApaPrintExponential now behaves like printf of glibc with
a "g" conversion specifier. These changes were motivated by the
discrepancies between printfs on Linux and Windows that affected "make
check."
CUDD now explicitly calls an implementation of qsort that is included
in the util library. While this version of qsort has been shipped
with CUDD since Release 1.0.0, it was up to the application to decide
whether to link it or not. However, dynamic linking on Windows and OS
X makes it difficult to replace the system qsort with a function of
the same name; hence, there is now a util_qsort in the CUDD library.
(The main reasons for not using the system qsort are repeatability and
performance of variable reordering.) To use the system qsort,
configure CUDD with the --with-system-qsort option. Keep in mind that
some tests in "make check" may fail in this case by producing variable
orders different from the reference ones.
The random number generator is now local to a manager. The interface
has changed accordingly. The only global variable in the whole
package is the one used to store the out-of-memory handler. As long
as it is not modified, distinct CUDD managers can be run in different
threads.
Even with a portable sort routine and random number generator, CUDD
does not guarantee the same output on all platforms. For instance,
the simulated annealing reordering algorithm uses floating-point
arithmetic, and the results on i686 machines occasionally differ from
those on x86_64 machines.
In the C++ wrapper, the default error handler now throws an exception
instead of failing. A new function helps in handling failed memory
allocations: Cudd_InstallOutOfMemoryHandler; it can be used to modify
the default behavior, which is to terminate the program. There are a
few new functions in the C++ API and a substantial clean-up has taken
place. Several functions have had some of their parameters given
default values, and in a few cases the order of the parameters has
been changed to improve consistency.
New functions:
DD_OOMFP Cudd_InstallOutOfMemoryHandler(DD_OOMFP newHandler);
DD_OOMFP Cudd_RegisterOutOfMemoryCallback(DdManager *unique, DD_OOMFP callback);
void Cudd_UnregisterOutOfMemoryCallback(DdManager *unique);
void Cudd_OutOfMemSilent(size_t size);
DdNode * Cudd_bddInterpolate(DdManager * dd, DdNode * l, DdNode * u);
int Cudd_VarsAreSymmetric(DdManager * dd, DdNode * f, int index1, int index2);
int Cudd_PrintSummary(DdManager * dd, DdNode * f, int n, int mode);
void Cudd_FreeApaNumber(DdApaNumber number);
char * Cudd_ApaStringDecimal(int digits, DdConstApaNumber number);
long double Cudd_LdblCountMinterm(DdManager const *manager, DdNode *node,
int nvars);
int Cudd_EpdPrintMinterm(DdManager const * dd, DdNode * node, int nvars);
st_table * st_init_table_with_params_and_arg(st_compare_arg_t,
st_hash_arg_t, void const *, int, int, double, int);
st_table * st_init_table_with_arg(st_compare_arg_t, st_hash_arg_t,
void const *);
void ABDD::summary(int nvars, int mode = 0) const;
DD_OOMFP Cudd::InstallOutOfMemoryHandler(DD_OOMFP newHandler) const;
DD_OOMFP RegisterOutOfMemoryCallback(DD_OOMFP callback) const;
void UnregisterOutOfMemoryCallback(void) const;
BDD computeCube(std::vector<BDD> const & vars) const;
ADD computeCube(std::vector<ADD> const & vars) const;
BDD BDD::Interpolate(const BDD& u) const;
bool BDD::VarAreSymmetric(int index1, int index2) const;
std::string ApaStringDecimal(int digits, DdApaNumber number) const;
void Cudd::ApaPrintExponential(int digits, DdApaNumber number,
int precision = 6, FILE * fp = stdout) const;
void ApaPrintMintermExp(int nvars, int precision = 6, FILE * fp = stdout) const;
long double LdblCountMinterm(int nvars) const;
ADD Cudd::Harwell(FILE * fp, std::vector<ADD>& x, std::vector<ADD>& y,
std::vector<ADD>& xn, std::vector<ADD>& yn_,
int * m, int * n, int bx = 0, int sx = 2, int by = 1,
int sy = 2, int pr = 0) const;
ADD Cudd::Read(FILE * fp, std::vector<ADD>& x, std::vector<ADD>& y,
std::vector<ADD>& xn, std::vector<ADD>& yn_, int * m, int * n,
int bx = 0, int sx = 2, int by = 1, int sy = 2) const;
BDD Cudd::Read(FILE * fp, std::vector<BDD>& x, std::vector<BDD>& y,
int * m, int * n, int bx = 0, int sx = 2, int by = 1,
int sy = 2) const;
std::string Cudd::OrderString(void) const;
Special thanks go to Hubert Garavel for the many discussions that have
greatly contributed to shaping this new CUDD release.
----------------------------------------------------------------------
Release 2.6.0 of Cudd is the first release to compile out of the box
with MinGW-w64. This is achieved primarily by using types and macros
defined in inttypes.h. The only visible changes in the API are some
parameter types that are now "size_t" instead of "unsinged long."
Support for multi-threaded applications has been slightly enhanced.
The Makefile has been slightly enhanced and finally supports creation
of top-level tag files for both emacs and vi.
The code has been cleaned up a bit so that all warnings that would be
produced by gcc with "-Wextra" have been removed. The tests run by
nanotrav/tst.sh and obj/testobj cover a bit more of the package's
functionality.
----------------------------------------------------------------------
Release 2.5.1 of Cudd improves support for multi-threaded applications.
Specifically, an application may now register a callback function that
is called from time to time to check whether computation should be
terminated because another thread has found the result.
The C++ interface allows the application to register variable names with
the manager and implements operator<< for BDDs. The interfaces of
SolveEqn and VerifySol now take std::vectors instead of plain arrays.
Fixed a few bugs in CUDD and a bug in the mtr package.
Added const qualifiers to dumping function interfaces
(Cudd_DumpDot,...).
The Makefile now supports gmake's -j option. Change "@+" back to "@" if
this causes problems with your make program.
Buggy documentation that was shipped with 2.5.0 has been fixed.
New functions:
int Cudd_bddIsVar(DdManager * dd, DdNode * f);
void Cudd_RegisterTerminationCallback(DdManager *unique,
void Cudd_UnregisterTerminationCallback(DdManager *unique);
void Cudd_SetApplicationHook(DdManager *dd, void * value);
void * Cudd_ReadApplicationHook(DdManager *dd);
char * Cudd_FactoredFormString(DdManager *dd, DdNode *f,
char const * const * inames);
----------------------------------------------------------------------
Releas 2.5.0 of Cudd introduces the ability to set timeouts. The
function that is interrupted returns NULL (which the application must
be prepared to handle,) but the BDDs are uncorrupted and the invoking
program can continue to use the manager.
In addition, reordering is now aware of timeouts, so that it gives up
when a timeout is approaching to give the invoking program a chance to
obtain some results.
The response time to the timeout is not immediate, though most of the time
it is well below one second. Checking for timeouts has a small overhead.
In experiments, less than 1% has been observed on average.
Creation of BDD managers with many variables (e.g., tens or hundreds
of thousands) is now much more efficient. Computing small supports of
BDDs when there are many variables is also much more efficient, but
this has been at the cost of separating the function for BDDs and ADDs
(Cudd_Support) from that for ZDDs (Cudd_zddSupport).
The C++ interface has undergone a major upgrade.
The handling of variable gruops in reordering has been much improved.
(Thanks to Arie Gurfinkel for a very detailed bug report!) A handful
of other bugs have been fixed as well.
New Functions:
unsigned long Cudd_ReadStartTime(DdManager *unique);
unsigned long Cudd_ReadElapsedTime(DdManager *unique);
void Cudd_SetStartTime(DdManager *unique, unsigned long st);
void Cudd_ResetStartTime(DdManager *unique);
unsigned long Cudd_ReadTimeLimit(DdManager *unique);
void Cudd_SetTimeLimit(DdManager *unique, unsigned long tl);
void Cudd_UpdateTimeLimit(DdManager * unique);
void Cudd_IncreaseTimeLimit(DdManager * unique, unsigned long increase);
void Cudd_UnsetTimeLimit(DdManager *unique);
int Cudd_TimeLimited(DdManager *unique);
unsigned int Cudd_ReadMaxReorderings (DdManager *dd);
void Cudd_SetMaxReorderings (DdManager *dd, unsigned int mr);
unsigned int Cudd_ReadOrderRandomization(DdManager * dd);
void Cudd_SetOrderRandomization(DdManager * dd, unsigned int factor);
int Cudd_PrintGroupedOrder(DdManager * dd, const char *str, void *data);
int Cudd_EnableOrderingMonitoring(DdManager *dd);
int Cudd_DisableOrderingMonitoring(DdManager *dd);
int Cudd_OrderingMonitoring(DdManager *dd);
DdNode * Cudd_bddExistAbstractLimit(DdManager * manager, DdNode * f, DdNode * cube, unsigned int limit);
DdNode * Cudd_bddIteLimit (DdManager *dd, DdNode *f, DdNode *g, DdNode *h, unsigned int limit);
DdNode * Cudd_bddOrLimit (DdManager *dd, DdNode *f, DdNode *g, unsigned int limit);
DdNode * Cudd_bddXnorLimit (DdManager *dd, DdNode *f, DdNode *g, unsigned int limit);
int Cudd_CheckCube (DdManager *dd, DdNode *g);
DdNode * Cudd_bddMaximallyExpand(DdManager *dd, DdNode *lb, DdNode *ub, DdNode *f);
DdNode * Cudd_bddLargestPrimeUnate(DdManager *dd , DdNode *f, DdNode *phaseBdd);
int Cudd_Reserve(DdManager *manager, int amount);
int Cudd_SupportIndices(DdManager * dd, DdNode * f, int **indices);
int Cudd_VectorSupportIndices(DdManager * dd, DdNode ** F, int n, int **indices);
DdNode * Cudd_zddSupport(DdManager * dd, DdNode * f);
Changed prototypes:
unsigned int Cudd_ReadReorderings (DdManager *dd);
----------------------------------------------------------------------
Release 2.4.2 of Cudd features several bug fixes. The most important
are those that prevented Cudd from making full use of up to 4 GB of
memory when using 32-bit pointers. A handful of bugs were discovered by
Coverity. (Thanks to Christian Stangier!)
This release can be compiled with either 64-bit pointers or 32-bit
pointers on x86_64 platforms if sizeof(long) = sizeof(void *) = 8 and
sizeof(int) = 4. This is known as the LP64 model. For 32-bit pointers,
one usually needs supplementary libraries. On Ubuntu and Debian Linux,
one needs g++-multilib, which can be installed with
"apt-get install g++-multilib."
Added functions
DdNode *Cudd_Inequality (DdManager * dd, int N, int c, DdNode ** x,
DdNode ** y);
DdNode * Cudd_Disequality (DdManager * dd, int N, int c, DdNode ** x,
DdNode ** y);
DdNode * Cudd_bddInterval (DdManager * dd, int N, DdNode ** x,
unsigned int lowerB, unsigned int upperB);
Changed prototypes:
int Cudd_DumpBlif (DdManager *dd, int n, DdNode **f, char
**inames, char **onames, char *mname, FILE *fp, int mv);
int Cudd_DumpBlifBody (DdManager *dd, int n, DdNode **f, char
**inames, char **onames, FILE *fp, int mv);
The additional parameter allows the caller to choose between plain blif
and blif-MV.
----------------------------------------------------------------------
Release 2.4.1 of Cudd features one major change with respect to previous
releases. The licensing terms are now explicitly stated.
This diff is collapsed.
#! /bin/sh
# Wrapper for Microsoft lib.exe
me=ar-lib
scriptversion=2012-03-01.08; # UTC
# Copyright (C) 2010-2013 Free Software Foundation, Inc.
# Written by Peter Rosin <peda@lysator.liu.se>.
#
# This program is free software; you can redistribute it and/or modify
# it under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 2, or (at your option)
# any later version.
#
# This program is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
# GNU General Public License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program. If not, see <http://www.gnu.org/licenses/>.
# As a special exception to the GNU General Public License, if you
# distribute this file as part of a program that contains a
# configuration script generated by Autoconf, you may include it under
# the same distribution terms that you use for the rest of that program.
# This file is maintained in Automake, please report
# bugs to <bug-automake@gnu.org> or send patches to
# <automake-patches@gnu.org>.
# func_error message
func_error ()
{
echo "$me: $1" 1>&2
exit 1
}
file_conv=
# func_file_conv build_file
# Convert a $build file to $host form and store it in $file
# Currently only supports Windows hosts.
func_file_conv ()
{
file=$1
case $file in
/ | /[!/]*) # absolute file, and not a UNC file
if test -z "$file_conv"; then