Commit aa4a582f authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Merge BuDDy 2.3.

* examples/calculator/, examples/internal/: Were renamed as ...
* examples/bddcalc/, examples/bddtest/: ... these.
* configure.ac: Adjust version and output Makefiles.
* examples/Makefile.am (SUBDIRS): Adjust subdir renaming.
* examples/cmilner/milner.c, examples/fdd/statespace.cxx: Were
renamed as ...
* examples/cmilner/cmilner.c, examples/fdd/fdd.cxx: ... these.
* examples/cmilner/Makefile.am, examples/fdd/Makefile.am: Adjust
accordingly.
* src/Makefile.am (AM_CPPFLAGS): Define VERSION.
parent 805b6fb7
2004-06-28 Alexandre Duret-Lutz <adl@src.lip6.fr>
Merge BuDDy 2.3.
* examples/calculator/, examples/internal/: Were renamed as ...
* examples/bddcalc/, examples/bddtest/: ... these.
* configure.ac: Adjust version and output Makefiles.
* examples/Makefile.am (SUBDIRS): Adjust subdir renaming.
* examples/cmilner/milner.c, examples/fdd/statespace.cxx: Were
renamed as ...
* examples/cmilner/cmilner.c, examples/fdd/fdd.cxx: ... these.
* examples/cmilner/Makefile.am, examples/fdd/Makefile.am: Adjust
accordingly.
* src/Makefile.am (AM_CPPFLAGS): Define VERSION.
2004-01-07 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/bddop.c (bdd_support): Free supportSet if it needs to be
......
==========================================================================
*** BuDDy ***
Binary Decision Diagrams
Library Package v2.2a
Library Package v2.3a
--------------------------------------------------------------------------
Copyright (C) 1996-2002 by Jorn Lind-Nielsen
All rights reserved
......@@ -32,12 +32,27 @@
==========================================================================
---------------------------------------------------------------------
--- PREFACE --------------------------------------------------------
---------------------------------------------------------------------
BuDDy was originally developed by Jorn Lind-Nielsen as a part of his
Phd thesis.
After using BuDDy as a BDD library for long time ( while getting some
support from Jorn through Email ), I have been suggested by Jorn to take
ownership of the project and move it to SourceForge.
I invite all users who are interested to participate in the development
to contact me. ( I always have desired tasks / features awaiting... )
I hope that BuDDy will prosper under my management.
Haim Cohen
haimcohen2002@hotmail.com
---------------------------------------------------------------------
--- REQUIREMENTS ----------------------------------------------------
---------------------------------------------------------------------
* A (not to old) C++ compiler
* A (not too old) C++ compiler. I use g++ 3.3.3
* A machine that supports 32 bit integers
......@@ -54,10 +69,10 @@ The following commands should build and install the library.
`./configure' accepts many arguments to tune your installation.
The following options are noteworthy:
--includedir=/somewhere/include
--includedir=/somewhere/include
Specify where header files will be installed.
--libdir=/somewhere/lib
--libdir=/somewhere/lib
Specify where libraries will be installed.
--disable-shared
......@@ -70,7 +85,7 @@ The following options are noteworthy:
Count number of fundamental variable swaps (for debugging)
--enable-cache-stats
Gather statistical information about operator and unique node
Gather statistical information about operator and unique node
caching (for debugging)
Run `./configure --help' for a complete listing, and see
......@@ -89,8 +104,8 @@ could be:
g++ -I/usr/local/include myfile.cc -o myfile -L/usr/local/lib -lbdd
Your machine may be setup to use the above directories auto-
matically, so you might be able to do:
Your machine may be setup to use the above directories automatically,
so you might be able to do:
g++ myfile.cc -o myfile -lbdd
......@@ -102,41 +117,17 @@ matically, so you might be able to do:
src: All files needed for the BuDDy package.
examples: Example files
fdd: An example of use of the FDD interface.
calculator: An example of a BDD calculator. Uses reordering.
bddcalc: An example of a BDD calculator. Uses reordering.
adder: Construction of a N-bit adder. Uses reordering.
milner: A calculation of the reachable statespace for Milner's
milner: A calculation of the reachable state space for Milner's
scheduler. C++.
cmilner: As above but purely in ANSI-C.
queen: Solution to the N-queen chess problem.
solitare: Solution to a solitare game.
money: Solution to the send-more-money problem (bvec demo).
internal: Some internal regression tests.
bddtest : Some internal tests.
doc: Documentation.
buddy.ps: Package documentation.
bddnotes.ps: BDD introduction notes.
tools: Tools used during the build.
m4: A couple of macros used to build ./configure.
---------------------------------------------------------------------
--- FEEDBACK --------------------------------------------------------
---------------------------------------------------------------------
Please do not hesitate to send any questions or bug reports to:
Jorn Lind-Nielsen: buddy@itu.dk
(or maybe jorn_lind_nielsen@hotmail.com or jln@fjeldgruppen.dk)
It may take some time to get an answer since BuDDy do not have that
much focus any more - but I'll try to give a reasonable answer
in (finite) time.
New updates and other info can be found at:
http://www.it-c.dk/research/buddy/
(or http://www.itu.dk/research/buddy)
Hope you find some use for this software
Jorn Lind-Nielsen
AC_PREREQ([2.57])
AC_INIT([buddy], [2.2a])
AC_INIT([buddy], [2.3a])
AC_CONFIG_AUX_DIR([tools])
AM_INIT_AUTOMAKE([foreign nostdinc no-define 1.7.3])
......@@ -22,10 +22,10 @@ AC_CONFIG_FILES([
doc/Makefile
examples/Makefile
examples/adder/Makefile
examples/calculator/Makefile
examples/bddcalc/Makefile
examples/bddtest/Makefile
examples/cmilner/Makefile
examples/fdd/Makefile
examples/internal/Makefile
examples/milner/Makefile
examples/money/Makefile
examples/queen/Makefile
......
EXTRA_DIST = bddnotes.ps buddy.pdf tech.txt
EXTRA_DIST = bddnotes.ps buddy.pdf
****************************************************************************
How to create your own internal BDD functions.
****************************************************************************
PLEASE NOTE
That interrupting variable reordering has been introduced after this document was written.
===[ Functions that do not change or produce new BDDs ]=====================
I'll do this by example. Take "bdd_satcount" that counts the number of
satisfying assignments that makes a BDD true.
Almost all functions consists of some introduction followed by a
recursion through the BDD.
* Use the type BDD for all references (numbers) to BDD nodes.
* External BDD variables used internally in the package are
defined in "kernel.h"
* Macros for reading BDD nodes are:
LEVEL(r)
LOW(r)
HIGH(r)
ISCONST(r) => true if r is one of the terminals
double bdd_satcount(BDD r)
{
double size=1;
int n;
CHECKa(r, 0.0); /* CHECK for valid nodes - defined in kernel.h */
miscid = CACHEID_SATCOU; /* Setup global variables. This is
used extensively instead of passing
arguments to the recursive functions,
for faster recursive calls */
for (n=0 ; n<LEVEL(r) ; n++) /* Setup whatever is needed for the */
size *= 2; /* recursion */
return size * bdd_satcount_rec(r); /* Do the recurison */
}
Cache tables are used for storing intermidiate results when doing BDD
operations. These are defined as static in the top of bddop.c (the
code is in cache.c) and they should be setup, cleared and delete at
the top of bddop.c in the functions bdd_operator_init,
bdd_operator_done, bdd_operator_reset.
static double bdd_satcount_rec(BDD root)
{
BddCacheData *entry; /* Entry pointer in the cache */
BddNode *node;
double size, s;
int m;
if (ISCONST(root)) /* Check for the constant terminals */
return root;
/* Lookup entry in the cache table used for this function */
entry = BddCache_lookup(&misccache, SATCOUHASH(root));
if (entry->a == root && entry->c == miscid)
return entry->r.dres;
/* Do whatever calculations are needed */
size = 0;
s = 1;
for (m=LEVEL(root)+1 ; m<LEVEL(LOW(root)) ; m++)
s *= 2;
size += s * bdd_satcount_rec(LOW(root)); /* Recurse on low part */
s = 1;
for (m=LEVEL(root)+1 ; m<LEVEL(HIGH(root)) ; m++)
s *= 2;
size += s * bdd_satcount_rec(HIGH(root)); /* Recurse on high part */
/* Insert result in cache table */
entry->a = root;
entry->c = miscid;
entry->r.dres = size;
return size; /* Return result */
}
===[ Functions that produces new BDDs ]=====================================
Functions that produces BDD nodes must take great care to avoid
loosing intermidiate nodes when automatic garbage collections
occur. This is doneby stacking each intermidiate result until they are no more used. This stack is check by the garbage collector.
Macros for accessing the stack:
INITREF: Reset the stack
PUSHREF(n): Push the node 'n' on the stack
READREF(p): Read 'p' positions down the stack
POPREF(p): Pop 'p' nodes off the stack.
Again I'll illustrate this with an example - the NOT operator.
BDD bdd_not(BDD r)
{
int res;
CHECKa(r, bddfalse); /* Validate arguments */
INITREF; /* Important! resets the stack */
res = not_rec(r); /* Recurse */
checkreorder(res); /* Check to see if a reordering was called for */
return res; /* Return result */
}
static BDD not_rec(BDD r)
{
BddCacheData *entry; /* Cache entry pointer */
BDD res;
if (ISZERO(r)) /* Check constant terminals */
return BDDONE;
if (ISONE(r))
return BDDZERO;
/* Lookup in cache */
entry = BddCache_lookup(&applycache, NOTHASH(r));
if (entry->a == r && entry->c == bddop_not)
return entry->r.res;
/* Recurse AND push result on the reference stack */
PUSHREF( not_rec(LOW(r)) );
PUSHREF( not_rec(HIGH(r)) );
/* Create a new BDD node */
res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
/* Pop result off the stack */
POPREF(2);
/* Insert in cache */
entry->a = r;
entry->c = bddop_not;
entry->r.res = res;
/* Return the result */
return res;
}
===[ Documentation ]========================================================
ALL entries visible to the user should be documentet by an commented
section like the one shown here, placed right before the code.
Each doc. entry consist of a keyword followed by {* ... text
... *}. The entries are:
NAME: Name of the function.
SECTION: Which part to place the documentation in.
SHORT: One line description of the code.
PROTO: The exact prototype.
DESCR: Multiline description of the code.
ALSO: Other relevant stuff.
RETURN: The returned value.
/*
NAME {* bdd\_satcount *}
SECTION {* info *}
SHORT {* Calculates the number of satisfying variable assignments *}
PROTO {* double bdd_satcount(BDD r) *}
DESCR {* Calculates how many possible variable assignments there exists
such that {\tt r} is satisfied, taking all defined variables
into account. *}
ALSO {* bdd\_satone, bdd\_fullsatone, bdd\_satcountln *}
RETURN {* The number of possible assignments. *}
*/
SUBDIRS = \
adder \
calculator \
bddcalc \
bddtest \
cmilner \
fdd \
internal \
milner \
money \
queen \
solitare
......@@ -27,7 +27,7 @@ bdd *xout;
void build_adder(void)
{
int n;
for (n=0 ; n<N ; n++)
{
if (n > 0)
......@@ -48,9 +48,10 @@ void build_adder(void)
int main(int argc, char **argv)
{
using namespace std ;
int method=BDD_REORDER_NONE;
int n;
if(argc < 2 || argc > 3)
{
cout << "usage: adder N R\n";
......@@ -59,7 +60,7 @@ int main(int argc, char **argv)
cout << " in this case 'adder' starts with a worst case ordering\n";
exit(1);
}
N = atoi(argv[1]);
if (N <= 0)
{
......@@ -90,17 +91,15 @@ int main(int argc, char **argv)
if (strcmp(argv[2], "rand") == 0)
method = BDD_REORDER_RANDOM;
}
long c0 = clock();
bdd_init(500,1000);
bdd_setvarnum(2*N);
ainp = new bdd[N];
binp = new bdd[N];
co = new bdd[N];
xout = new bdd[N];
for (n=0 ; n<N ; n++)
{
if (method == BDD_REORDER_NONE)
......@@ -124,28 +123,22 @@ int main(int argc, char **argv)
//bdd_autoreorder(method);
//bdd_reorder_verbose(2);
build_adder();
if (method != BDD_REORDER_NONE)
{
cout << "Sizes before reordering:\n";
for (n=0 ; n<N ; n++)
cout << "Out[" << n << "]: " << bdd_nodecount(xout[n]) << " nodes\n";
long c1 = clock();
cout << (float)(c1-c0)/(float)(CLOCKS_PER_SEC) << " sec.\n";
bdd_reorder(method);
cout << "Sizes after reordering:\n";
}
else
cout << "Sizes:\n";
long c1 = clock();
for (n=0 ; n<N ; n++)
cout << "Out[" << n << "]: " << bdd_nodecount(xout[n]) << " nodes\n";
cout << (float)(c1-c0)/(float)(CLOCKS_PER_SEC) << " sec.\n";
}
......@@ -155,7 +148,7 @@ int main(int argc, char **argv)
bdd setval(int val, int v)
{
bdd x = bddtrue;
for (int n=0 ; n<N ; n++)
{
if (val & 1)
......@@ -187,7 +180,7 @@ int test_vector(bdd av, bdd bv, int a, int b)
for (int n=0 ; n<N ; n++)
{
bdd resv = av & bv & xout[n];
if (resv == bddfalse && (res & 1) || resv != bddfalse && !(res & 1))
return 0;
......@@ -201,7 +194,7 @@ int test_vector(bdd av, bdd bv, int a, int b)
int test_adder(void)
{
int m = 1 << N;
for (int a=0 ; a<m ; a++)
{
for (int b=0 ; b<m ; b++)
......
Makefile.in
Makefile
lexer.cxx
parser.cxx
parser.h
.deps
.libs
bddcalc
include ../Makefile.def
EXTRA_DIST = \
readme \
example.cal \
examples/c432.cal \
examples/c499.cal \
examples/c1355.cal \
examples/c1908.cal \
examples/c2670.cal \
examples/c3540.cal \
examples/readme
AM_YFLAGS = -d
BUILT_SOURCES = parser.h
check_PROGRAMS = bddcalc
bddcalc_SOURCES = \
hashtbl.h \
hashtbl.cxx \
lexer.lxx \
parser.yxx \
parser_.h \
slist.h
......@@ -7,8 +7,8 @@
%{
#include <string.h>
#include <stdlib.h>
#include "parser_.h"
#include "parser.h"
#include "tokens.h"
%}
......
# ---------------------------
# Makefile for BDD calculator
# ---------------------------
all: bddcalc
# --- Compiler flags
CFLAGS = -O3 -pedantic -Wall -ansi -L../../src -I../../src
# --- C++ compiler
CPP = g++
# --- C compiler
CC = gcc
# --- You may need to change these according to your flex and bison versions
parser.cxx: parser.h parser.y
yacc -d -o parser.cxx parser.y
mv parser.cxx.h tokens.h
lexer.cxx: tokens.h parser.h lexer.l
flex -olexer.cxx lexer.l
# --- Do not touch ---
.SUFFIXES: .cxx .c
.cxx.o:
$(CPP) $(CFLAGS) -c $<
.c.o:
$(CC) $(CFLAGS) -c $<
bddcalc: parser.o lexer.o hashtbl.o bddlib
$(CPP) $(CFLAGS) parser.o lexer.o hashtbl.o -o bddcalc -lbdd -lm
bddlib:
cd ../../src ; make
clean:
rm -f *~ examples/*~
rm -f *.o
rm -f bddcalc parser.cxx lexer.cxx
......@@ -6,15 +6,17 @@
*************************************************************************/
%{
#include <string>
#include <string.h>
#include <stdarg.h>
#include <fstream>
#include <getopt.h>
#define IMPLEMENTSLIST /* Special for list template handling */
#include "slist.h"
#include "hashtbl.h"
#include "parser.h"
#include "parser_.h"
using namespace std;
/* Definitions for storing and caching of identifiers */
#define inputTag 0
#define exprTag 1
......@@ -64,23 +66,23 @@ void actPrint(token *id);
Token definitions
*************************************************************************/
%token T_id, T_str, T_intval, T_true, T_false
%token T_id T_str T_intval T_true T_false
%token T_initial, T_inputs, T_actions
%token T_size, T_dumpdot
%token T_autoreorder, T_reorder, T_win2, T_win2ite, T_sift, T_siftite, T_none
%token T_cache, T_tautology, T_print
%token T_initial T_inputs T_actions
%token T_size T_dumpdot
%token T_autoreorder T_reorder T_win2 T_win2ite T_sift T_siftite T_none
%token T_cache T_tautology T_print
%token T_lpar, T_rpar
%token T_lpar T_rpar
%token T_equal
%token T_semi, T_dot
%token T_semi T_dot
%right T_exist, T_forall, T_dot
%right T_exist T_forall T_dot
%left T_biimp
%left T_imp
%left T_or, T_nor
%left T_or T_nor
%left T_xor
%left T_nand, T_and
%left T_nand T_and
%right T_not
/*************************************************************************
......@@ -201,7 +203,6 @@ print:
void usage(void)
{
using namespace std ;
cerr << "USAGE: bddcalc [-hg] file\n";
cerr << " -h : print this message\n";
cerr << " -g : disable garbage collection info\n";
......@@ -210,7 +211,6 @@ void usage(void)
int main(int ac, char **av)
{
using namespace std ;
int c;
while ((c=getopt(ac, av, "hg")) != EOF)
......@@ -389,7 +389,6 @@ void actQuantVar1(token *res, token *id)
void actSize(token *id)
{
using namespace std ;
hashData hd;
if (names.lookup(id->id,hd) == 0)
......@@ -404,7 +403,6 @@ void actSize(token *id)
void actDot(token *fname, token *id)
{
using namespace std ;
hashData hd;
if (names.lookup(id->id,hd) == 0)
......@@ -434,7 +432,6 @@ void actCache(void)
void actTautology(token *id)
{
using namespace std ;
hashData hd;
if (names.lookup(id->id,hd) == 0)
......@@ -451,7 +448,6 @@ void actTautology(token *id)
void actPrint(token *id)
{
using namespace std ;
hashData hd;