diff --git a/buddy/.cvsignore b/buddy/.cvsignore new file mode 100644 index 000000000..8ecb47c0f --- /dev/null +++ b/buddy/.cvsignore @@ -0,0 +1,8 @@ +Makefile.in +Makefile +aclocal.m4 +configure +tools +config.log +config.status +libtool diff --git a/buddy/ChangeLog b/buddy/ChangeLog new file mode 100644 index 000000000..92a0ff65b --- /dev/null +++ b/buddy/ChangeLog @@ -0,0 +1,35 @@ +2003-05-05 Alexandre Duret-Lutz + + * configure.ac, Makefile.am, src/Makefile.am, doc/Makefile.am, + examples/Makefile.am, examples/Makefile.def, + examples/adder/Makefile.am, examples/calculator/Makefile.am, + examples/cmilner/Makefile.am, examples/fdd/Makefile.am, + examples/internal/Makefile.am, examples/milner/Makefile.am, + examples/money/Makefile.am, examples/queen/Makefile.am, + examples/solitar/Makefile.am, m4/debug.m4, m4/gccwarns.m4, + ChangeLog, INSTALL: New files. + * config, makefile, src/makefile, doc/makefile, + examples/adder/makefile, examples/calculator/makefile + examples/cmilner/makefile, examples/fdd/makefile, + examples/internal/makefile, examples/milner/makefile, + examples/money/makefile, examples/queen/makefile, + examples/solitare/makefile : Delete. + * examples/adder/adder.cxx, examples/fdd/statespace.cxx, + examples/internal/bddtest.cxx, examples/milner/milner.cxx, + examples/money/money.cxx, examples/queen/queen.cxx, + examples/solitare/solitare.cxx: Include iostream. + * examples/calculator/parser.y: Rename as ... + * examples/calculator/parser.yxx: ... this. Remove spurious + comas in %token, %right, and %left arguments. + * examples/calculator/parser.h: Rename as ... + * examples/calculator/parser_.h: ... this, because the bison + rule with output parser.h (not tokens.h) from parser.y. + * examples/calculator/lexer.l: Rename as ... + * examples/calculator/lexer.lxx: ... this. Include parser.h + instead of tokens.h. + * examples/calculator/slist.h + (voidSList::voisSListElem, SList::ite): Fix friend usage. + * src/kernel.h (DEFAULT_CLOCK): Default to 60 if not already + defined. + * README: Update build instruction, and file listing. + diff --git a/buddy/INSTALL b/buddy/INSTALL new file mode 100644 index 000000000..54caf7c19 --- /dev/null +++ b/buddy/INSTALL @@ -0,0 +1,229 @@ +Copyright (C) 1994, 1995, 1996, 1999, 2000, 2001, 2002 Free Software +Foundation, Inc. + + This file is free documentation; the Free Software Foundation gives +unlimited permission to copy, distribute and modify it. + +Basic Installation +================== + + These are generic installation instructions. + + The `configure' shell script attempts to guess correct values for +various system-dependent variables used during compilation. It uses +those values to create a `Makefile' in each directory of the package. +It may also create one or more `.h' files containing system-dependent +definitions. Finally, it creates a shell script `config.status' that +you can run in the future to recreate the current configuration, and a +file `config.log' containing compiler output (useful mainly for +debugging `configure'). + + It can also use an optional file (typically called `config.cache' +and enabled with `--cache-file=config.cache' or simply `-C') that saves +the results of its tests to speed up reconfiguring. (Caching is +disabled by default to prevent problems with accidental use of stale +cache files.) + + If you need to do unusual things to compile the package, please try +to figure out how `configure' could check whether to do them, and mail +diffs or instructions to the address given in the `README' so they can +be considered for the next release. If you are using the cache, and at +some point `config.cache' contains results you don't want to keep, you +may remove or edit it. + + The file `configure.ac' (or `configure.in') is used to create +`configure' by a program called `autoconf'. You only need +`configure.ac' if you want to change it or regenerate `configure' using +a newer version of `autoconf'. + +The simplest way to compile this package is: + + 1. `cd' to the directory containing the package's source code and type + `./configure' to configure the package for your system. If you're + using `csh' on an old version of System V, you might need to type + `sh ./configure' instead to prevent `csh' from trying to execute + `configure' itself. + + Running `configure' takes awhile. While running, it prints some + messages telling which features it is checking for. + + 2. Type `make' to compile the package. + + 3. Optionally, type `make check' to run any self-tests that come with + the package. + + 4. Type `make install' to install the programs and any data files and + documentation. + + 5. You can remove the program binaries and object files from the + source code directory by typing `make clean'. To also remove the + files that `configure' created (so you can compile the package for + a different kind of computer), type `make distclean'. There is + also a `make maintainer-clean' target, but that is intended mainly + for the package's developers. If you use it, you may have to get + all sorts of other programs in order to regenerate files that came + with the distribution. + +Compilers and Options +===================== + + Some systems require unusual options for compilation or linking that +the `configure' script does not know about. Run `./configure --help' +for details on some of the pertinent environment variables. + + You can give `configure' initial values for configuration parameters +by setting variables in the command line or in the environment. Here +is an example: + + ./configure CC=c89 CFLAGS=-O2 LIBS=-lposix + + *Note Defining Variables::, for more details. + +Compiling For Multiple Architectures +==================================== + + You can compile the package for more than one kind of computer at the +same time, by placing the object files for each architecture in their +own directory. To do this, you must use a version of `make' that +supports the `VPATH' variable, such as GNU `make'. `cd' to the +directory where you want the object files and executables to go and run +the `configure' script. `configure' automatically checks for the +source code in the directory that `configure' is in and in `..'. + + If you have to use a `make' that does not support the `VPATH' +variable, you have to compile the package for one architecture at a +time in the source code directory. After you have installed the +package for one architecture, use `make distclean' before reconfiguring +for another architecture. + +Installation Names +================== + + By default, `make install' will install the package's files in +`/usr/local/bin', `/usr/local/man', etc. You can specify an +installation prefix other than `/usr/local' by giving `configure' the +option `--prefix=PATH'. + + You can specify separate installation prefixes for +architecture-specific files and architecture-independent files. If you +give `configure' the option `--exec-prefix=PATH', the package will use +PATH as the prefix for installing programs and libraries. +Documentation and other data files will still use the regular prefix. + + In addition, if you use an unusual directory layout you can give +options like `--bindir=PATH' to specify different values for particular +kinds of files. Run `configure --help' for a list of the directories +you can set and what kinds of files go in them. + + If the package supports it, you can cause programs to be installed +with an extra prefix or suffix on their names by giving `configure' the +option `--program-prefix=PREFIX' or `--program-suffix=SUFFIX'. + +Optional Features +================= + + Some packages pay attention to `--enable-FEATURE' options to +`configure', where FEATURE indicates an optional part of the package. +They may also pay attention to `--with-PACKAGE' options, where PACKAGE +is something like `gnu-as' or `x' (for the X Window System). The +`README' should mention any `--enable-' and `--with-' options that the +package recognizes. + + For packages that use the X Window System, `configure' can usually +find the X include and library files automatically, but if it doesn't, +you can use the `configure' options `--x-includes=DIR' and +`--x-libraries=DIR' to specify their locations. + +Specifying the System Type +========================== + + There may be some features `configure' cannot figure out +automatically, but needs to determine by the type of machine the package +will run on. Usually, assuming the package is built to be run on the +_same_ architectures, `configure' can figure that out, but if it prints +a message saying it cannot guess the machine type, give it the +`--build=TYPE' option. TYPE can either be a short name for the system +type, such as `sun4', or a canonical name which has the form: + + CPU-COMPANY-SYSTEM + +where SYSTEM can have one of these forms: + + OS KERNEL-OS + + See the file `config.sub' for the possible values of each field. If +`config.sub' isn't included in this package, then this package doesn't +need to know the machine type. + + If you are _building_ compiler tools for cross-compiling, you should +use the `--target=TYPE' option to select the type of system they will +produce code for. + + If you want to _use_ a cross compiler, that generates code for a +platform different from the build platform, you should specify the +"host" platform (i.e., that on which the generated programs will +eventually be run) with `--host=TYPE'. + +Sharing Defaults +================ + + If you want to set default values for `configure' scripts to share, +you can create a site shell script called `config.site' that gives +default values for variables like `CC', `cache_file', and `prefix'. +`configure' looks for `PREFIX/share/config.site' if it exists, then +`PREFIX/etc/config.site' if it exists. Or, you can set the +`CONFIG_SITE' environment variable to the location of the site script. +A warning: not all `configure' scripts look for a site script. + +Defining Variables +================== + + Variables not defined in a site shell script can be set in the +environment passed to `configure'. However, some packages may run +configure again during the build, and the customized values of these +variables may be lost. In order to avoid this problem, you should set +them in the `configure' command line, using `VAR=value'. For example: + + ./configure CC=/usr/local2/bin/gcc + +will cause the specified gcc to be used as the C compiler (unless it is +overridden in the site shell script). + +`configure' Invocation +====================== + + `configure' recognizes the following options to control how it +operates. + +`--help' +`-h' + Print a summary of the options to `configure', and exit. + +`--version' +`-V' + Print the version of Autoconf used to generate the `configure' + script, and exit. + +`--cache-file=FILE' + Enable the cache: use and save the results of the tests in FILE, + traditionally `config.cache'. FILE defaults to `/dev/null' to + disable caching. + +`--config-cache' +`-C' + Alias for `--cache-file=config.cache'. + +`--quiet' +`--silent' +`-q' + Do not print messages saying which checks are being made. To + suppress all normal output, redirect it to `/dev/null' (any error + messages will still be shown). + +`--srcdir=DIR' + Look for the package's source code in directory DIR. Usually + `configure' can determine that directory automatically. + +`configure' also accepts some other, not widely useful, options. Run +`configure --help' for more details. + diff --git a/buddy/Makefile.am b/buddy/Makefile.am new file mode 100644 index 000000000..51b6aaa85 --- /dev/null +++ b/buddy/Makefile.am @@ -0,0 +1,5 @@ +ACLOCAL_AMFLAGS = -I m4 + +SUBDIRS = src examples doc + +EXTRA_DIST = CHANGES m4/debug.m4 m4/gccwarns.m4 diff --git a/buddy/README b/buddy/README index 4e7c7d29e..a0aa17818 100644 --- a/buddy/README +++ b/buddy/README @@ -1,7 +1,7 @@ ========================================================================== *** BuDDy *** Binary Decision Diagrams - Library Package v2.2 + Library Package v2.2a -------------------------------------------------------------------------- Copyright (C) 1996-2002 by Jorn Lind-Nielsen All rights reserved @@ -45,15 +45,38 @@ --- INSTALLING ------------------------------------------------------ --------------------------------------------------------------------- -2) Edit the file "config" to specify your compiler options and -where the package is to be installed. +The following commands should build and install the library. -3) type "make" to make the binary. + ./configure + make + make install -4) type "make install" to copy the BDD files to their appropriate -directories. +`./configure' accepts many arguments to tune your installation. +The following options are noteworthy: -5) type "make examples" to make the examples + --includedir=/somewhere/include + Specify where header files will be installed. + + --libdir=/somewhere/lib + Specify where libraries will be installed. + + --disable-shared + Do not build the shared library for BuDDy. + + --disable-static + Do not build the static library for BuDDy. + + --enable-swap-count + Count number of fundamental variable swaps (for debugging) + + --enable-cache-stats + Gather statistical information about operator and unique node + caching (for debugging) + +Run `./configure --help' for a complete listing, and see +the INSTALL file for generic intrustions. + +Run `make check' to build the examples. --------------------------------------------------------------------- @@ -91,7 +114,8 @@ examples: Example files 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 -------------------------------------------------------- diff --git a/buddy/config b/buddy/config deleted file mode 100644 index 25886737a..000000000 --- a/buddy/config +++ /dev/null @@ -1,46 +0,0 @@ -# ============================================================== -# Makefile for the BuDDy package -# - Edit the lines below to configure -# ============================================================== - -# --- Your compiler flags -CFLAGS = -g -ansi -Wmissing-prototypes -Wall - -# --- Where to install the library (directory, no trailing slash) -LIBDIR = /usr/local/lib - -# --- Where to install the include file (directory, no trailing slash) -INCDIR = /usr/local/include - -# --- Your C compiler -CC = gcc - -# --- Your C++ compiler -CPP = g++ - -# Some machines are missing "CLOCKS_PER_SEC". Please define a default value -# If you do not know this, then leave it as it is. -CLOCK=60 - -CLOCKFLAG = -DDEFAULT_CLOCK=$(CLOCK) - -# Debugging and statistical flags. Possible values are: -# -DSWAPCOUNT : Count number of fundamental variable swaps -# -DCACHESTATS : Gather statistical information about operator and -# unique node caching -DEBUGFLAGS = - -# Some of the BuDDy library needs 64 bit arithmetics. -# With gnu C++, Microsoft C++ and KAI C++ this is part of the -# language and used by BuDDy. With other compilers BuDDy need -# to implement the math it self -- which is a bit slower. If -# you now of a 64 bit unsigned integer type on your platform -# then define that in the BUDDYUINT64 variable. Example: -# BUDDYUINT64 = -DBUDDYUINT64="long long" - - -# -------------------------------------------------------------- -# Do not touch -# -------------------------------------------------------------- -DFLAGS = $(CLOCKFLAG) $(DEBUGFLAGS) $(BUDDYUINT64) - diff --git a/buddy/configure.ac b/buddy/configure.ac new file mode 100644 index 000000000..98fc76a70 --- /dev/null +++ b/buddy/configure.ac @@ -0,0 +1,33 @@ +AC_PREREQ([2.57]) +AC_INIT([buddy], [2.2a]) +AC_CONFIG_AUX_DIR([tools]) +AM_INIT_AUTOMAKE([foreign nostdinc no-define 1.7.3]) + +AC_PROG_CC + +AM_PROG_LEX +AC_PROG_YACC + +AC_PROG_CXX + +AC_PROG_LIBTOOL + +buddy_DEBUG_FLAGS + +AC_CONFIG_FILES([ + Makefile + src/Makefile + doc/Makefile + examples/Makefile + examples/adder/Makefile + examples/calculator/Makefile + examples/cmilner/Makefile + examples/fdd/Makefile + examples/internal/Makefile + examples/milner/Makefile + examples/money/Makefile + examples/queen/Makefile + examples/solitare/Makefile +]) + +AC_OUTPUT diff --git a/buddy/doc/.cvsignore b/buddy/doc/.cvsignore new file mode 100644 index 000000000..3dda72986 --- /dev/null +++ b/buddy/doc/.cvsignore @@ -0,0 +1,2 @@ +Makefile.in +Makefile diff --git a/buddy/doc/Makefile.am b/buddy/doc/Makefile.am new file mode 100644 index 000000000..467fd57d2 --- /dev/null +++ b/buddy/doc/Makefile.am @@ -0,0 +1 @@ +EXTRA_DIST = bddnotes.ps buddy.ps tech.txt diff --git a/buddy/doc/makefile b/buddy/doc/makefile deleted file mode 100644 index ad6a457e4..000000000 --- a/buddy/doc/makefile +++ /dev/null @@ -1 +0,0 @@ -clean: diff --git a/buddy/examples/.cvsignore b/buddy/examples/.cvsignore new file mode 100644 index 000000000..3dda72986 --- /dev/null +++ b/buddy/examples/.cvsignore @@ -0,0 +1,2 @@ +Makefile.in +Makefile diff --git a/buddy/examples/Makefile.am b/buddy/examples/Makefile.am new file mode 100644 index 000000000..da71976af --- /dev/null +++ b/buddy/examples/Makefile.am @@ -0,0 +1,11 @@ +SUBDIRS = \ + adder \ + calculator \ + cmilner \ + fdd \ + internal \ + milner \ + money \ + queen \ + solitare + diff --git a/buddy/examples/Makefile.def b/buddy/examples/Makefile.def new file mode 100644 index 000000000..cf497aa6c --- /dev/null +++ b/buddy/examples/Makefile.def @@ -0,0 +1,2 @@ +AM_CPPFLAGS = -I$(top_srcdir)/src +LDADD = $(top_builddir)/src/libbdd.la diff --git a/buddy/examples/adder/.cvsignore b/buddy/examples/adder/.cvsignore new file mode 100644 index 000000000..c502d4ab2 --- /dev/null +++ b/buddy/examples/adder/.cvsignore @@ -0,0 +1,4 @@ +Makefile.in +Makefile +adder +.deps diff --git a/buddy/examples/adder/Makefile.am b/buddy/examples/adder/Makefile.am new file mode 100644 index 000000000..d9ec1d9b5 --- /dev/null +++ b/buddy/examples/adder/Makefile.am @@ -0,0 +1,3 @@ +include ../Makefile.def +check_PROGRAMS = adder +adder_SOURCES = adder.cxx diff --git a/buddy/examples/adder/adder.cxx b/buddy/examples/adder/adder.cxx index 6ade992eb..bb17ef945 100644 --- a/buddy/examples/adder/adder.cxx +++ b/buddy/examples/adder/adder.cxx @@ -7,8 +7,11 @@ #include #include #include +#include #include "bdd.h" +using namespace std; + int N; bdd *ainp; diff --git a/buddy/examples/adder/makefile b/buddy/examples/adder/makefile deleted file mode 100644 index 1c0179e8d..000000000 --- a/buddy/examples/adder/makefile +++ /dev/null @@ -1,36 +0,0 @@ -# -------------------------------- -# Makefile for adder test example -# -------------------------------- - -# --- Compiler flags -CFLAGS = -g -pedantic -Wall -ansi -L../../src -I../../src - -# --- C++ compiler -CPP = g++ - -# --- C compiler -CC = gcc - - -# --- Do not touch --- - -.SUFFIXES: .cxx .c - -.cxx.o: - $(CPP) $(CFLAGS) -c $< - -.c.o: - $(CC) $(CFLAGS) -c $< - -adder: adder.o bddlib - $(CPP) $(CFLAGS) adder.o -o adder -lbdd -lm - -bddlib: - cd ../..; make - -clean: - rm -f *~ - rm -f *.o - rm -f adder - -adder.o: ../../src/bdd.h diff --git a/buddy/examples/calculator/.cvsignore b/buddy/examples/calculator/.cvsignore new file mode 100644 index 000000000..68ff4364d --- /dev/null +++ b/buddy/examples/calculator/.cvsignore @@ -0,0 +1,6 @@ +Makefile.in +Makefile +lexer.cxx +parser.cxx +parser.h +.deps diff --git a/buddy/examples/calculator/Makefile.am b/buddy/examples/calculator/Makefile.am new file mode 100644 index 000000000..3598778f0 --- /dev/null +++ b/buddy/examples/calculator/Makefile.am @@ -0,0 +1,25 @@ +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 + diff --git a/buddy/examples/calculator/hashtbl.cxx b/buddy/examples/calculator/hashtbl.cxx index 805646305..7a7965499 100644 --- a/buddy/examples/calculator/hashtbl.cxx +++ b/buddy/examples/calculator/hashtbl.cxx @@ -1,5 +1,5 @@ /************************************************************************* - $Header: /Volumes/CVS/repository/spot/spot/buddy/examples/calculator/Attic/hashtbl.cxx,v 1.1 2003/05/05 10:57:55 aduret Exp $ + $Header: /Volumes/CVS/repository/spot/spot/buddy/examples/calculator/Attic/hashtbl.cxx,v 1.2 2003/05/05 13:44:53 aduret Exp $ FILE: hashtbl.cc DESCR: Compiler hash table AUTH: Jorn Lind diff --git a/buddy/examples/calculator/hashtbl.h b/buddy/examples/calculator/hashtbl.h index 56dd09574..1e2bb0182 100644 --- a/buddy/examples/calculator/hashtbl.h +++ b/buddy/examples/calculator/hashtbl.h @@ -1,5 +1,5 @@ /************************************************************************* - $Header: /Volumes/CVS/repository/spot/spot/buddy/examples/calculator/Attic/hashtbl.h,v 1.1 2003/05/05 10:57:55 aduret Exp $ + $Header: /Volumes/CVS/repository/spot/spot/buddy/examples/calculator/Attic/hashtbl.h,v 1.2 2003/05/05 13:44:54 aduret Exp $ FILE: hashtbl.h DESCR: Compiler hashtable AUTH: Jorn Lind diff --git a/buddy/examples/calculator/lexer.l b/buddy/examples/calculator/lexer.lxx similarity index 99% rename from buddy/examples/calculator/lexer.l rename to buddy/examples/calculator/lexer.lxx index 7818adb25..0049dd6c8 100644 --- a/buddy/examples/calculator/lexer.l +++ b/buddy/examples/calculator/lexer.lxx @@ -7,8 +7,8 @@ %{ #include #include +#include "parser_.h" #include "parser.h" -#include "tokens.h" %} diff --git a/buddy/examples/calculator/makefile b/buddy/examples/calculator/makefile deleted file mode 100644 index ccab052cc..000000000 --- a/buddy/examples/calculator/makefile +++ /dev/null @@ -1,48 +0,0 @@ -# --------------------------- -# 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 - bison -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 ../..; make - -clean: - rm -f *~ examples/*~ - rm -f *.o - rm -f bddcalc parser.cxx lexer.cxx - -# --- Needed for the author's Cygwin compiler -export BISONLIB=/cygnus/cygwin-b20/share/ - diff --git a/buddy/examples/calculator/parser.h b/buddy/examples/calculator/parser.h index 7b59b0067..b8b784816 100644 --- a/buddy/examples/calculator/parser.h +++ b/buddy/examples/calculator/parser.h @@ -1,44 +1,118 @@ -/************************************************************************* - FILE: parser.h - DESCR: parser defs. for BDD calculator - AUTH: Jorn Lind - DATE: (C) may 1999 -*************************************************************************/ +/* A Bison parser, made by GNU Bison 1.875b. */ -#ifndef _PARSER_H -#define _PARSER_H +/* Skeleton parser for Yacc-like parsing with Bison, + Copyright (C) 1984, 1989, 1990, 2000, 2001, 2002, 2003 Free Software Foundation, Inc. -#include -#include "bdd.h" + 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. -#define MAXIDLEN 32 /* Max. number of allowed characters in an identifier */ + 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. -struct token /* BISON token data */ -{ - char id[MAXIDLEN+1]; - char *str; - int ival; - bdd *bval; -}; + You should have received a copy of the GNU General Public License + along with this program; if not, write to the Free Software + Foundation, Inc., 59 Temple Place - Suite 330, + Boston, MA 02111-1307, USA. */ -#define YYSTYPE token -#define YY_SKIP_YYWRAP -#define YY_NO_UNPUT -#define yywrap() (1) +/* As a special exception, when this file is copied by Bison into a + Bison output file, you may use that output file without restriction. + This special exception was added by the Free Software Foundation + in version 1.24 of Bison. */ -extern YYSTYPE yylval; /* Declare for flex user */ -extern void yyerror(char *,...); /* Declare for flex and bison */ -extern FILE *yyin; -extern int yylex(void); /* Declare for bison */ -extern int yyparse(void); /* Declare for bison user */ -extern int linenum; /* Declare for error handler */ +/* Tokens. */ +#ifndef YYTOKENTYPE +# define YYTOKENTYPE + /* Put the tokens into the symbol table, so that GDB and other debuggers + know about them. */ + enum yytokentype { + T_id = 258, + T_str = 259, + T_intval = 260, + T_true = 261, + T_false = 262, + T_initial = 263, + T_inputs = 264, + T_actions = 265, + T_size = 266, + T_dumpdot = 267, + T_autoreorder = 268, + T_reorder = 269, + T_win2 = 270, + T_win2ite = 271, + T_sift = 272, + T_siftite = 273, + T_none = 274, + T_cache = 275, + T_tautology = 276, + T_print = 277, + T_lpar = 278, + T_rpar = 279, + T_equal = 280, + T_semi = 281, + T_dot = 282, + T_forall = 283, + T_exist = 284, + T_biimp = 285, + T_imp = 286, + T_nor = 287, + T_or = 288, + T_xor = 289, + T_and = 290, + T_nand = 291, + T_not = 292 + }; +#endif +#define T_id 258 +#define T_str 259 +#define T_intval 260 +#define T_true 261 +#define T_false 262 +#define T_initial 263 +#define T_inputs 264 +#define T_actions 265 +#define T_size 266 +#define T_dumpdot 267 +#define T_autoreorder 268 +#define T_reorder 269 +#define T_win2 270 +#define T_win2ite 271 +#define T_sift 272 +#define T_siftite 273 +#define T_none 274 +#define T_cache 275 +#define T_tautology 276 +#define T_print 277 +#define T_lpar 278 +#define T_rpar 279 +#define T_equal 280 +#define T_semi 281 +#define T_dot 282 +#define T_forall 283 +#define T_exist 284 +#define T_biimp 285 +#define T_imp 286 +#define T_nor 287 +#define T_or 288 +#define T_xor 289 +#define T_and 290 +#define T_nand 291 +#define T_not 292 + + + + +#if ! defined (YYSTYPE) && ! defined (YYSTYPE_IS_DECLARED) +typedef int YYSTYPE; +# define yystype YYSTYPE /* obsolescent; will be withdrawn */ +# define YYSTYPE_IS_DECLARED 1 +# define YYSTYPE_IS_TRIVIAL 1 +#endif + +extern YYSTYPE yylval; - /* Use this instead of strdup() to avoid malloc() */ -inline char *sdup(const char *s) -{ - return strcpy(new char[strlen(s)+1], s); -} -#endif /* _PARSER_H */ -/* EOF */ diff --git a/buddy/examples/calculator/parser.y b/buddy/examples/calculator/parser.yxx similarity index 96% rename from buddy/examples/calculator/parser.y rename to buddy/examples/calculator/parser.yxx index ba68a539f..3f814c761 100644 --- a/buddy/examples/calculator/parser.y +++ b/buddy/examples/calculator/parser.yxx @@ -8,13 +8,15 @@ %{ #include #include -#include +#include #include #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 /************************************************************************* diff --git a/buddy/examples/calculator/parser_.h b/buddy/examples/calculator/parser_.h new file mode 100644 index 000000000..7b59b0067 --- /dev/null +++ b/buddy/examples/calculator/parser_.h @@ -0,0 +1,44 @@ +/************************************************************************* + FILE: parser.h + DESCR: parser defs. for BDD calculator + AUTH: Jorn Lind + DATE: (C) may 1999 +*************************************************************************/ + +#ifndef _PARSER_H +#define _PARSER_H + +#include +#include "bdd.h" + +#define MAXIDLEN 32 /* Max. number of allowed characters in an identifier */ + +struct token /* BISON token data */ +{ + char id[MAXIDLEN+1]; + char *str; + int ival; + bdd *bval; +}; + +#define YYSTYPE token +#define YY_SKIP_YYWRAP +#define YY_NO_UNPUT +#define yywrap() (1) + +extern YYSTYPE yylval; /* Declare for flex user */ +extern void yyerror(char *,...); /* Declare for flex and bison */ +extern FILE *yyin; +extern int yylex(void); /* Declare for bison */ +extern int yyparse(void); /* Declare for bison user */ +extern int linenum; /* Declare for error handler */ + + /* Use this instead of strdup() to avoid malloc() */ +inline char *sdup(const char *s) +{ + return strcpy(new char[strlen(s)+1], s); +} + +#endif /* _PARSER_H */ + +/* EOF */ diff --git a/buddy/examples/calculator/slist.h b/buddy/examples/calculator/slist.h index aba90cd92..37b3199c0 100644 --- a/buddy/examples/calculator/slist.h +++ b/buddy/examples/calculator/slist.h @@ -1,5 +1,5 @@ /************************************************************************* - $Header: /Volumes/CVS/repository/spot/spot/buddy/examples/calculator/Attic/slist.h,v 1.1 2003/05/05 10:57:55 aduret Exp $ + $Header: /Volumes/CVS/repository/spot/spot/buddy/examples/calculator/Attic/slist.h,v 1.2 2003/05/05 13:44:55 aduret Exp $ FILE: slist.h DESCR: Single linked list AUTH: Jorn Lind @@ -28,7 +28,7 @@ protected: private: voidSListElem(void *d) { data=d; next=NULL; } - friend voidSList; + friend class voidSList; }; public: @@ -169,7 +169,7 @@ public: int operator==(ite x) { return x.next==next; } private: voidSListElem *next; - friend SList; + friend class SList; }; ~SList(void) { for (ite x=first() ; x.more() ; x++) delete &(*x); } diff --git a/buddy/examples/calculator/tokens.h b/buddy/examples/calculator/tokens.h deleted file mode 100644 index 007490412..000000000 --- a/buddy/examples/calculator/tokens.h +++ /dev/null @@ -1,41 +0,0 @@ -#ifndef YYSTYPE -#define YYSTYPE int -#endif -#define T_id 257 -#define T_str 258 -#define T_intval 259 -#define T_true 260 -#define T_false 261 -#define T_initial 262 -#define T_inputs 263 -#define T_actions 264 -#define T_size 265 -#define T_dumpdot 266 -#define T_autoreorder 267 -#define T_reorder 268 -#define T_win2 269 -#define T_win2ite 270 -#define T_sift 271 -#define T_siftite 272 -#define T_none 273 -#define T_cache 274 -#define T_tautology 275 -#define T_print 276 -#define T_lpar 277 -#define T_rpar 278 -#define T_equal 279 -#define T_semi 280 -#define T_dot 281 -#define T_exist 282 -#define T_forall 283 -#define T_biimp 284 -#define T_imp 285 -#define T_or 286 -#define T_nor 287 -#define T_xor 288 -#define T_nand 289 -#define T_and 290 -#define T_not 291 - - -extern YYSTYPE yylval; diff --git a/buddy/examples/cmilner/.cvsignore b/buddy/examples/cmilner/.cvsignore new file mode 100644 index 000000000..e440fafda --- /dev/null +++ b/buddy/examples/cmilner/.cvsignore @@ -0,0 +1,3 @@ +Makefile.in +Makefile +.deps diff --git a/buddy/examples/cmilner/Makefile.am b/buddy/examples/cmilner/Makefile.am new file mode 100644 index 000000000..09a9ab7e0 --- /dev/null +++ b/buddy/examples/cmilner/Makefile.am @@ -0,0 +1,4 @@ +include ../Makefile.def +EXTRA_DIST = readme +check_PROGRAMS = milner +milner_SOURCES = milner.c diff --git a/buddy/examples/cmilner/makefile b/buddy/examples/cmilner/makefile deleted file mode 100644 index 222fcdea0..000000000 --- a/buddy/examples/cmilner/makefile +++ /dev/null @@ -1,36 +0,0 @@ -# -------------------------------- -# Makefile for milner test example -# -------------------------------- - -# --- Compiler flags -CFLAGS = -O3 -pedantic -Wall -ansi -L../../src -I../../src - -# --- C++ compiler -CPP = g++ - -# --- C compiler -CC = gcc - - -# --- Do not touch --- - -.SUFFIXES: .cxx .c - -.cxx.o: - $(CPP) $(CFLAGS) -c $< - -.c.o: - $(CC) $(CFLAGS) -c $< - -milner: milner.o bddlib - $(CC) $(CFLAGS) milner.o -o milner -lbdd -lm - -bddlib: - cd ../..; make - -clean: - rm -f *~ - rm -f *.o - rm -f milner - -milner.o: ../../src/bdd.h diff --git a/buddy/examples/fdd/.cvsignore b/buddy/examples/fdd/.cvsignore new file mode 100644 index 000000000..e440fafda --- /dev/null +++ b/buddy/examples/fdd/.cvsignore @@ -0,0 +1,3 @@ +Makefile.in +Makefile +.deps diff --git a/buddy/examples/fdd/Makefile.am b/buddy/examples/fdd/Makefile.am new file mode 100644 index 000000000..5fea74700 --- /dev/null +++ b/buddy/examples/fdd/Makefile.am @@ -0,0 +1,3 @@ +include ../Makefile.def +check_PROGRAMS = statespace +statespace_SOURCES = statespace.cxx diff --git a/buddy/examples/fdd/makefile b/buddy/examples/fdd/makefile deleted file mode 100644 index 8f4db89ee..000000000 --- a/buddy/examples/fdd/makefile +++ /dev/null @@ -1,36 +0,0 @@ -# -------------------------------- -# Makefile for FDD test example -# -------------------------------- - -# --- Compiler flags -CFLAGS = -O3 -pedantic -Wall -ansi -L../../src -I../../src - -# --- C++ compiler -CPP = g++ - -# --- C compiler -CC = gcc - - -# --- Do not touch --- - -.SUFFIXES: .cxx .c - -.cxx.o: - $(CPP) $(CFLAGS) -c $< - -.c.o: - $(CC) $(CFLAGS) -c $< - -statespace: statespace.o bddlib - $(CPP) $(CFLAGS) statespace.o -o statespace -lbdd -lm - -bddlib: - cd ../../src; make - -clean: - rm -f *~ - rm -f *.o - rm -f statespace - -statespace.o: ../../src/fdd.h diff --git a/buddy/examples/fdd/statespace.cxx b/buddy/examples/fdd/statespace.cxx index f1b4fc88f..395f0bb6c 100644 --- a/buddy/examples/fdd/statespace.cxx +++ b/buddy/examples/fdd/statespace.cxx @@ -6,7 +6,9 @@ * 0 -> 1 -> 2 -> 3 -> 4 -> 5 -> -> 7 -> 0 */ +#include #include "fdd.h" +using namespace std; /* Use the transition relation "transRel" to iterate through the statespace */ diff --git a/buddy/examples/internal/.cvsignore b/buddy/examples/internal/.cvsignore new file mode 100644 index 000000000..e440fafda --- /dev/null +++ b/buddy/examples/internal/.cvsignore @@ -0,0 +1,3 @@ +Makefile.in +Makefile +.deps diff --git a/buddy/examples/internal/Makefile.am b/buddy/examples/internal/Makefile.am new file mode 100644 index 000000000..eb8820a5d --- /dev/null +++ b/buddy/examples/internal/Makefile.am @@ -0,0 +1,3 @@ +include ../Makefile.def +check_PROGRAMS = bddtest +bddtest_SOURCES = bddtest.cxx diff --git a/buddy/examples/internal/bddtest.cxx b/buddy/examples/internal/bddtest.cxx index ac154982e..1400cb214 100644 --- a/buddy/examples/internal/bddtest.cxx +++ b/buddy/examples/internal/bddtest.cxx @@ -1,6 +1,8 @@ #include #include #include +#include +using namespace std; static const int varnum = 5; diff --git a/buddy/examples/internal/makefile b/buddy/examples/internal/makefile deleted file mode 100644 index df42c2b58..000000000 --- a/buddy/examples/internal/makefile +++ /dev/null @@ -1,38 +0,0 @@ -# -------------------------------- -# Makefile for internal tests -# -------------------------------- - -# --- Compiler flags -CFLAGS = -g -pedantic -Wall -ansi -L../../src -I../../src - -# --- C++ compiler -CPP = g++ - -# --- C compiler -CC = gcc - - -# --- Do not touch --- - -.SUFFIXES: .cxx .c - -.cxx.o: - $(CPP) $(CFLAGS) -c $< - -.c.o: - $(CC) $(CFLAGS) -c $< - -bddtest: bddtest.o bddlib - $(CPP) $(CFLAGS) bddtest.o -o bddtest -lbdd -lm - -bddlib: - cd ../..; make - -clean: - rm -f *~ - rm -f *.o - rm -f bddtest - -bddtest.o: ../../src/bdd.h - - diff --git a/buddy/examples/milner/.cvsignore b/buddy/examples/milner/.cvsignore new file mode 100644 index 000000000..e440fafda --- /dev/null +++ b/buddy/examples/milner/.cvsignore @@ -0,0 +1,3 @@ +Makefile.in +Makefile +.deps diff --git a/buddy/examples/milner/Makefile.am b/buddy/examples/milner/Makefile.am new file mode 100644 index 000000000..6ee02dc92 --- /dev/null +++ b/buddy/examples/milner/Makefile.am @@ -0,0 +1,4 @@ +include ../Makefile.def +EXTRA_DIST = readme +check_PROGRAMS = milner +milner_SOURCES = milner.cxx diff --git a/buddy/examples/milner/makefile b/buddy/examples/milner/makefile deleted file mode 100644 index 1cf229551..000000000 --- a/buddy/examples/milner/makefile +++ /dev/null @@ -1,36 +0,0 @@ -# -------------------------------- -# Makefile for milner test example -# -------------------------------- - -# --- Compiler flags -CFLAGS = -g -pedantic -Wall -ansi -L../../src -I../../src - -# --- C++ compiler -CPP = g++ - -# --- C compiler -CC = gcc - - -# --- Do not touch --- - -.SUFFIXES: .cxx .c - -.cxx.o: - $(CPP) $(CFLAGS) -c $< - -.c.o: - $(CC) $(CFLAGS) -c $< - -milner: milner.o bddlib - $(CPP) $(CFLAGS) milner.o -o milner -lbdd -lm - -bddlib: - cd ../../src; make - -clean: - rm -f *~ - rm -f *.o - rm -f milner - -milner.o: ../../src/bdd.h diff --git a/buddy/examples/milner/milner.cxx b/buddy/examples/milner/milner.cxx index 5105452d7..8fc52fea1 100644 --- a/buddy/examples/milner/milner.cxx +++ b/buddy/examples/milner/milner.cxx @@ -3,6 +3,8 @@ #include #include #include "bdd.h" +#include +using namespace std; int N; // Number of cyclers bdd normvar; // Current state variables diff --git a/buddy/examples/money/.cvsignore b/buddy/examples/money/.cvsignore new file mode 100644 index 000000000..e440fafda --- /dev/null +++ b/buddy/examples/money/.cvsignore @@ -0,0 +1,3 @@ +Makefile.in +Makefile +.deps diff --git a/buddy/examples/money/Makefile.am b/buddy/examples/money/Makefile.am new file mode 100644 index 000000000..5e59d3e5d --- /dev/null +++ b/buddy/examples/money/Makefile.am @@ -0,0 +1,3 @@ +include ../Makefile.def +check_PROGRAMS = money +money_SOURCES = money.cxx diff --git a/buddy/examples/money/makefile b/buddy/examples/money/makefile deleted file mode 100644 index 46b052d9f..000000000 --- a/buddy/examples/money/makefile +++ /dev/null @@ -1,36 +0,0 @@ -# -------------------------------- -# Makefile for BVEC example -# -------------------------------- - -# --- Compiler flags -CFLAGS = -O3 -pedantic -Wall -ansi -L../../src -I../../src - -# --- C++ compiler -CPP = g++ - -# --- C compiler -CC = gcc - - -# --- Do not touch --- - -.SUFFIXES: .cxx .c - -.cxx.o: - $(CPP) $(CFLAGS) -c $< - -.c.o: - $(CC) $(CFLAGS) -c $< - -money: money.o bddlib - $(CPP) $(CFLAGS) money.o -o money -lbdd -lm - -bddlib: - cd ../../src; make - -clean: - rm -f *~ - rm -f *.o - rm -f money - -money.o: ../../src/bvec.h ../../src/fdd.h ../../src/bdd.h diff --git a/buddy/examples/money/money.cxx b/buddy/examples/money/money.cxx index deb7d0ce8..26ede1d8a 100644 --- a/buddy/examples/money/money.cxx +++ b/buddy/examples/money/money.cxx @@ -1,4 +1,6 @@ #include "bvec.h" +#include +using namespace std; /* Find a solution to the send-more-money example * The problem is to assign values for the digits s,e,n,d,m,o,r,y diff --git a/buddy/examples/queen/.cvsignore b/buddy/examples/queen/.cvsignore new file mode 100644 index 000000000..e440fafda --- /dev/null +++ b/buddy/examples/queen/.cvsignore @@ -0,0 +1,3 @@ +Makefile.in +Makefile +.deps diff --git a/buddy/examples/queen/Makefile.am b/buddy/examples/queen/Makefile.am new file mode 100644 index 000000000..94c2f2eed --- /dev/null +++ b/buddy/examples/queen/Makefile.am @@ -0,0 +1,3 @@ +include ../Makefile.def +check_PROGRAMS = queen +queen_SOURCES = queen.cxx diff --git a/buddy/examples/queen/makefile b/buddy/examples/queen/makefile deleted file mode 100644 index 9454bd55a..000000000 --- a/buddy/examples/queen/makefile +++ /dev/null @@ -1,37 +0,0 @@ -# --------------------------------- -# Makefile for N-queen test example -# --------------------------------- - -# --- Compiler flags -CFLAGS = -O3 -pedantic -Wall -ansi -L../../src -I../../src - -# --- C++ compiler -CPP = g++ - -# --- C compiler -CC = gcc - - -# --- Do not touch --- - -.SUFFIXES: .cxx .c - -.cxx.o: - $(CPP) $(CFLAGS) -c $< - -.c.o: - $(CC) $(CFLAGS) -c $< - -queen: queen.o bddlib - $(CPP) $(CFLAGS) queen.o -o queen -lbdd -lm - -bddlib: - cd ../..; make - -clean: - rm -f *~ - rm -f *.o - rm -f queen - -queen.o: ../../src/bdd.h - diff --git a/buddy/examples/queen/queen.cxx b/buddy/examples/queen/queen.cxx index eb5aaa13c..85f878914 100644 --- a/buddy/examples/queen/queen.cxx +++ b/buddy/examples/queen/queen.cxx @@ -26,7 +26,9 @@ **************************************************************************/ #include +#include #include "bdd.h" +using namespace std; int N; /* Size of the chess board */ bdd **X; /* BDD variable array */ diff --git a/buddy/examples/solitare/.cvsignore b/buddy/examples/solitare/.cvsignore new file mode 100644 index 000000000..e440fafda --- /dev/null +++ b/buddy/examples/solitare/.cvsignore @@ -0,0 +1,3 @@ +Makefile.in +Makefile +.deps diff --git a/buddy/examples/solitare/Makefile.am b/buddy/examples/solitare/Makefile.am new file mode 100644 index 000000000..5082e1c73 --- /dev/null +++ b/buddy/examples/solitare/Makefile.am @@ -0,0 +1,3 @@ +include ../Makefile.def +check_PROGRAMS = solitare +solitare_SOURCES = solitare.cxx diff --git a/buddy/examples/solitare/makefile b/buddy/examples/solitare/makefile deleted file mode 100644 index 903535862..000000000 --- a/buddy/examples/solitare/makefile +++ /dev/null @@ -1,36 +0,0 @@ -# -------------------------------- -# Makefile for solitare test example -# -------------------------------- - -# --- Compiler flags -CFLAGS = -O3 -pedantic -Wall -ansi -L../../src -I../../src - -# --- C++ compiler -CPP = g++ - -# --- C compiler -CC = gcc - - -# --- Do not touch --- - -.SUFFIXES: .cxx .c - -.cxx.o: - $(CPP) $(CFLAGS) -c $< - -.c.o: - $(CC) $(CFLAGS) -c $< - -solitare: solitare.o bddlib - $(CPP) $(CFLAGS) solitare.o -o solitare -lbdd -lm - -bddlib: - cd ../..; make - -clean: - rm -f *~ - rm -f *.o - rm -f solitare - -milner.o: ../../src/bdd.h diff --git a/buddy/examples/solitare/solitare.cxx b/buddy/examples/solitare/solitare.cxx index 2ce3e9328..5f0bc2216 100644 --- a/buddy/examples/solitare/solitare.cxx +++ b/buddy/examples/solitare/solitare.cxx @@ -2,7 +2,11 @@ #include #include #include +#include #include "bdd.h" +using std::cout; +using std::endl; +using std::flush; float dummyStateNum; // Use to remove the number of states defined by the // next-state variables diff --git a/buddy/m4/debug.m4 b/buddy/m4/debug.m4 new file mode 100644 index 000000000..afc0fb20e --- /dev/null +++ b/buddy/m4/debug.m4 @@ -0,0 +1,25 @@ +AC_DEFUN([buddy_DEBUG_FLAGS], +[AC_ARG_ENABLE([swap-count], + [AC_HELP_STRING([--enable-swap-count], + [Count number of fundamental variable swaps (for debugging)])]) +case $enable_swap_count in + yes) + AC_DEFINE([SWAPCOUNT], 1, + [Define to 1 to count number of fundamental variable swaps + (for debugging).]) + ;; +esac + +AC_ARG_ENABLE([cache-stats], + [AC_HELP_STRING([--enable-cache-stats], + [Gather statistical information about operator and unique node caching (for debugging)])]) +case $enable_cache_stats in + yes) + AC_DEFINE([CACHESTATS], 1, + [Defube to 1 to gather statistical information about operator and unique node caching (for debugging).]) + ;; +esac +]) + + + \ No newline at end of file diff --git a/buddy/m4/gccwarns.m4 b/buddy/m4/gccwarns.m4 new file mode 100644 index 000000000..57024922b --- /dev/null +++ b/buddy/m4/gccwarns.m4 @@ -0,0 +1,51 @@ +dnl Check if the compiler supports useful warning options. There's a few that +dnl we don't use, simply because they're too noisy: +dnl +dnl -ansi (prevents declaration of functions like strdup, and because +dnl it makes warning in system headers). +dnl -Wconversion (useful in older versions of gcc, but not in gcc 2.7.x) +dnl -Wtraditional (combines too many unrelated messages, only a few useful) +dnl -Wredundant-decls (system headers make this too noisy) +dnl -pedantic +dnl -Wunreachable-code (broken, see GCC PR/7827) +dnl -Wredundant-decls (too many warnings in GLIBC's header with old GCC) +dnl +dnl A few other options have been left out because they are annoying in C++. + +AC_DEFUN([CF_GCC_WARNINGS], +[if test -n "$GCC"; then + AC_CACHE_CHECK([for $GCC warning options], ac_cv_prog_gxx_warn_flags, + [ + cat > conftest.$ac_ext < $(RD)/doc/makefile - mkdir $(RD)/examples/milner - cp examples/milner/* $(RD)/examples/milner - mkdir $(RD)/examples/cmilner - cp examples/cmilner/* $(RD)/examples/cmilner - mkdir $(RD)/examples/adder - cp examples/adder/* $(RD)/examples/adder - mkdir $(RD)/examples/queen - cp examples/queen/* $(RD)/examples/queen - mkdir $(RD)/examples/fdd - cp examples/fdd/* $(RD)/examples/fdd - mkdir $(RD)/examples/calculator - mkdir $(RD)/examples/calculator/examples - cp -R examples/calculator/* $(RD)/examples/calculator - mkdir $(RD)/examples/solitare - cp examples/solitare/* $(RD)/examples/solitare - mkdir $(RD)/examples/money - cp examples/money/* $(RD)/examples/money - mkdir $(RD)/examples/internal - cp examples/internal/* $(RD)/examples/internal - tar -cvf $(TARGET)$(VERSION).tar $(RD)/* - gzip $(TARGET)$(VERSION).tar - rm -fr $(RD) - @cat RELEASE - - - diff --git a/buddy/src/.cvsignore b/buddy/src/.cvsignore new file mode 100644 index 000000000..3f6060398 --- /dev/null +++ b/buddy/src/.cvsignore @@ -0,0 +1,6 @@ +*.lo +*.la +.libs +.deps +Makefile.in +Makefile diff --git a/buddy/src/Makefile.am b/buddy/src/Makefile.am new file mode 100644 index 000000000..793c7cb47 --- /dev/null +++ b/buddy/src/Makefile.am @@ -0,0 +1,29 @@ +include_HEADERS = bdd.h fdd.h bvec.h + +lib_LTLIBRARIES = libbdd.la +libbdd_la_SOURCES = \ + bddio.c \ + bddop.c \ + bddtree.h \ + bvec.c \ + cache.c \ + cache.h \ + cppext.cxx \ + fdd.c \ + imatrix.c \ + imatrix.h \ + kernel.c \ + kernel.h \ + pairs.c \ + prime.c \ + prime.h \ + reorder.c \ + tree.c + +# See the `Updating version info' node of the Libtool manual before +# changing this. +libbdd_la_LDFLAGS = -version-info 0:0:0 + +check_PROGRAMS = bddtest +bddtest_SOURCES = bddtest.cxx +bddtest_LDADD = ./libbdd.la diff --git a/buddy/src/bdd.h b/buddy/src/bdd.h index c32647e76..4e2a1f5d5 100644 --- a/buddy/src/bdd.h +++ b/buddy/src/bdd.h @@ -28,7 +28,7 @@ ========================================================================*/ /************************************************************************* - $Header: /Volumes/CVS/repository/spot/spot/buddy/src/bdd.h,v 1.1 2003/05/05 10:57:56 aduret Exp $ + $Header: /Volumes/CVS/repository/spot/spot/buddy/src/bdd.h,v 1.2 2003/05/05 13:45:04 aduret Exp $ FILE: bdd.h DESCR: C,C++ User interface for the BDD package AUTH: Jorn Lind diff --git a/buddy/src/bddio.c b/buddy/src/bddio.c index a73daec7f..689ff29ff 100644 --- a/buddy/src/bddio.c +++ b/buddy/src/bddio.c @@ -28,7 +28,7 @@ ========================================================================*/ /************************************************************************* - $Header: /Volumes/CVS/repository/spot/spot/buddy/src/bddio.c,v 1.1 2003/05/05 10:57:56 aduret Exp $ + $Header: /Volumes/CVS/repository/spot/spot/buddy/src/bddio.c,v 1.2 2003/05/05 13:45:04 aduret Exp $ FILE: bddio.c DESCR: File I/O routines for BDD package AUTH: Jorn Lind diff --git a/buddy/src/bddop.c b/buddy/src/bddop.c index 93e0e6a7c..6dfeeaae5 100644 --- a/buddy/src/bddop.c +++ b/buddy/src/bddop.c @@ -28,7 +28,7 @@ ========================================================================*/ /************************************************************************* - $Header: /Volumes/CVS/repository/spot/spot/buddy/src/bddop.c,v 1.1 2003/05/05 10:57:56 aduret Exp $ + $Header: /Volumes/CVS/repository/spot/spot/buddy/src/bddop.c,v 1.2 2003/05/05 13:45:04 aduret Exp $ FILE: bddop.c DESCR: BDD operators AUTH: Jorn Lind diff --git a/buddy/src/bddtree.h b/buddy/src/bddtree.h index a7f3c49ef..be1e8f185 100644 --- a/buddy/src/bddtree.h +++ b/buddy/src/bddtree.h @@ -28,7 +28,7 @@ ========================================================================*/ /************************************************************************* - $Header: /Volumes/CVS/repository/spot/spot/buddy/src/bddtree.h,v 1.1 2003/05/05 10:57:56 aduret Exp $ + $Header: /Volumes/CVS/repository/spot/spot/buddy/src/bddtree.h,v 1.2 2003/05/05 13:45:05 aduret Exp $ FILE: tree.h DESCR: Trees for BDD variables AUTH: Jorn Lind diff --git a/buddy/src/bvec.c b/buddy/src/bvec.c index 6f7a8d8ee..937fefb37 100644 --- a/buddy/src/bvec.c +++ b/buddy/src/bvec.c @@ -28,7 +28,7 @@ ========================================================================*/ /************************************************************************* - $Header: /Volumes/CVS/repository/spot/spot/buddy/src/bvec.c,v 1.1 2003/05/05 10:57:56 aduret Exp $ + $Header: /Volumes/CVS/repository/spot/spot/buddy/src/bvec.c,v 1.2 2003/05/05 13:45:05 aduret Exp $ FILE: bvec.c DESCR: Boolean vector arithmetics using BDDs AUTH: Jorn Lind diff --git a/buddy/src/bvec.h b/buddy/src/bvec.h index 7ffa94b11..922b56f13 100644 --- a/buddy/src/bvec.h +++ b/buddy/src/bvec.h @@ -28,7 +28,7 @@ ========================================================================*/ /************************************************************************* - $Header: /Volumes/CVS/repository/spot/spot/buddy/src/bvec.h,v 1.1 2003/05/05 10:57:56 aduret Exp $ + $Header: /Volumes/CVS/repository/spot/spot/buddy/src/bvec.h,v 1.2 2003/05/05 13:45:05 aduret Exp $ FILE: bvec.h DESCR: Boolean (BDD) vector handling AUTH: Jorn Lind diff --git a/buddy/src/cache.c b/buddy/src/cache.c index a286b4bdb..c361361ed 100644 --- a/buddy/src/cache.c +++ b/buddy/src/cache.c @@ -28,7 +28,7 @@ ========================================================================*/ /************************************************************************* - $Header: /Volumes/CVS/repository/spot/spot/buddy/src/cache.c,v 1.1 2003/05/05 10:57:56 aduret Exp $ + $Header: /Volumes/CVS/repository/spot/spot/buddy/src/cache.c,v 1.2 2003/05/05 13:45:05 aduret Exp $ FILE: cache.c DESCR: Cache class for caching apply/exist etc. results in BDD package AUTH: Jorn Lind diff --git a/buddy/src/cache.h b/buddy/src/cache.h index 4ebe2aa48..dcd9ba527 100644 --- a/buddy/src/cache.h +++ b/buddy/src/cache.h @@ -28,7 +28,7 @@ ========================================================================*/ /************************************************************************* - $Header: /Volumes/CVS/repository/spot/spot/buddy/src/cache.h,v 1.1 2003/05/05 10:57:56 aduret Exp $ + $Header: /Volumes/CVS/repository/spot/spot/buddy/src/cache.h,v 1.2 2003/05/05 13:45:05 aduret Exp $ FILE: cache.h DESCR: Cache class for caching apply/exist etc. results AUTH: Jorn Lind diff --git a/buddy/src/cppext.cxx b/buddy/src/cppext.cxx index 403390c93..a3110fb4f 100644 --- a/buddy/src/cppext.cxx +++ b/buddy/src/cppext.cxx @@ -28,7 +28,7 @@ ========================================================================*/ /************************************************************************* - $Header: /Volumes/CVS/repository/spot/spot/buddy/src/cppext.cxx,v 1.1 2003/05/05 10:57:56 aduret Exp $ + $Header: /Volumes/CVS/repository/spot/spot/buddy/src/cppext.cxx,v 1.2 2003/05/05 13:45:06 aduret Exp $ FILE: cppext.cxx DESCR: C++ extension of BDD package AUTH: Jorn Lind diff --git a/buddy/src/fdd.c b/buddy/src/fdd.c index 363781e18..639622bd4 100644 --- a/buddy/src/fdd.c +++ b/buddy/src/fdd.c @@ -28,7 +28,7 @@ ========================================================================*/ /************************************************************************* - $Header: /Volumes/CVS/repository/spot/spot/buddy/src/fdd.c,v 1.1 2003/05/05 10:57:56 aduret Exp $ + $Header: /Volumes/CVS/repository/spot/spot/buddy/src/fdd.c,v 1.2 2003/05/05 13:45:06 aduret Exp $ FILE: fdd.c DESCR: Finite domain extensions to BDD package AUTH: Jorn Lind diff --git a/buddy/src/fdd.h b/buddy/src/fdd.h index b9d89d931..3f4c53f59 100644 --- a/buddy/src/fdd.h +++ b/buddy/src/fdd.h @@ -28,7 +28,7 @@ ========================================================================*/ /************************************************************************* - $Header: /Volumes/CVS/repository/spot/spot/buddy/src/fdd.h,v 1.1 2003/05/05 10:57:56 aduret Exp $ + $Header: /Volumes/CVS/repository/spot/spot/buddy/src/fdd.h,v 1.2 2003/05/05 13:45:07 aduret Exp $ FILE: fdd.h DESCR: Finite domain data with BDDs AUTH: Jorn Lind diff --git a/buddy/src/kernel.c b/buddy/src/kernel.c index b06a46f0f..17319dc5f 100644 --- a/buddy/src/kernel.c +++ b/buddy/src/kernel.c @@ -28,7 +28,7 @@ ========================================================================*/ /************************************************************************* - $Header: /Volumes/CVS/repository/spot/spot/buddy/src/kernel.c,v 1.1 2003/05/05 10:57:57 aduret Exp $ + $Header: /Volumes/CVS/repository/spot/spot/buddy/src/kernel.c,v 1.2 2003/05/05 13:45:07 aduret Exp $ FILE: kernel.c DESCR: implements the bdd kernel functions. AUTH: Jorn Lind diff --git a/buddy/src/kernel.h b/buddy/src/kernel.h index 6b27497d7..95a763833 100644 --- a/buddy/src/kernel.h +++ b/buddy/src/kernel.h @@ -28,7 +28,7 @@ ========================================================================*/ /************************************************************************* - $Header: /Volumes/CVS/repository/spot/spot/buddy/src/kernel.h,v 1.1 2003/05/05 10:57:57 aduret Exp $ + $Header: /Volumes/CVS/repository/spot/spot/buddy/src/kernel.h,v 1.2 2003/05/05 13:45:07 aduret Exp $ FILE: kernel.h DESCR: Kernel specific definitions for BDD package AUTH: Jorn Lind @@ -167,7 +167,12 @@ extern bddCacheStat bddcachestats; #define BDDZERO 0 #ifndef CLOCKS_PER_SEC -#define CLOCKS_PER_SEC DEFAULT_CLOCK + /* Pass `CPPFLAGS=-DDEFAULT_CLOCK=1000' as an argument to ./configure + to override this setting. */ +# ifndef DEFAULT_CLOCK +# define DEFAULT_CLOCK 60 +# endif +# define CLOCKS_PER_SEC DEFAULT_CLOCK #endif #define DEFAULTMAXNODEINC 50000 diff --git a/buddy/src/makefile b/buddy/src/makefile deleted file mode 100644 index 9a95b1a21..000000000 --- a/buddy/src/makefile +++ /dev/null @@ -1,49 +0,0 @@ -# ============================================================== -# Makefile for BDD source -# - Do not touch -# ============================================================== - -# --- full object list -OBJ = bddio.o bddop.o bvec.o cache.o cppext.o fdd.o imatrix.o kernel.o \ - pairs.o prime.o reorder.o tree.o -CFILES = bddio.c bddop.c bvec.c cache.c fdd.c imatrix.c kernel.c \ - pairs.c prime.c reorder.c tree.c -CCFILES = cppext.cxx - -include ../config - -# -------------------------------------------------------------- -# Code generation -# -------------------------------------------------------------- - -.SUFFIXES: .cxx .c - -.cxx.o: - $(CPP) $(CFLAGS) $(DFLAGS) -c $< - -.c.o: - $(CC) $(CFLAGS) $(DFLAGS) -c $< - - -# -------------------------------------------------------------- -# The primary targets. -# -------------------------------------------------------------- - -libbdd.a: $(OBJ) ../config - ar r libbdd.a $(OBJ) - ranlib libbdd.a - -clean: - rm -f lib$(TARGET).a - rm -f *.o core *~ - rm -f libbdd.a - rm -f bddtest - -depend: - gcc -MM $(CFLAGS) $(DFLAGS) $(CFILES) > depend.inf - g++ -MM $(CFLAGS) $(DFLAGS) $(CCFILES) >> depend.inf - -bddtest: libbdd.a bddtest.cxx ../config - $(CPP) $(CFLAGS) $(DFLAGS) bddtest.cxx -o bddtest -L. -lbdd -### -include depend.inf diff --git a/buddy/src/pairs.c b/buddy/src/pairs.c index 269ae0d43..bd05af81b 100644 --- a/buddy/src/pairs.c +++ b/buddy/src/pairs.c @@ -28,7 +28,7 @@ ========================================================================*/ /************************************************************************* - $Header: /Volumes/CVS/repository/spot/spot/buddy/src/pairs.c,v 1.1 2003/05/05 10:57:57 aduret Exp $ + $Header: /Volumes/CVS/repository/spot/spot/buddy/src/pairs.c,v 1.2 2003/05/05 13:45:08 aduret Exp $ FILE: pairs.c DESCR: Pair management for BDD package. AUTH: Jorn Lind diff --git a/buddy/src/prime.c b/buddy/src/prime.c index af53106f8..8e4d4e9a7 100644 --- a/buddy/src/prime.c +++ b/buddy/src/prime.c @@ -28,7 +28,7 @@ ========================================================================*/ /************************************************************************* - $Header: /Volumes/CVS/repository/spot/spot/buddy/src/prime.c,v 1.1 2003/05/05 10:57:57 aduret Exp $ + $Header: /Volumes/CVS/repository/spot/spot/buddy/src/prime.c,v 1.2 2003/05/05 13:45:08 aduret Exp $ FILE: prime.c DESCR: Prime number calculations AUTH: Jorn Lind diff --git a/buddy/src/prime.h b/buddy/src/prime.h index 01c229a15..0d7693077 100644 --- a/buddy/src/prime.h +++ b/buddy/src/prime.h @@ -28,7 +28,7 @@ ========================================================================*/ /************************************************************************* - $Header: /Volumes/CVS/repository/spot/spot/buddy/src/prime.h,v 1.1 2003/05/05 10:57:57 aduret Exp $ + $Header: /Volumes/CVS/repository/spot/spot/buddy/src/prime.h,v 1.2 2003/05/05 13:45:08 aduret Exp $ FILE: prime.c DESCR: Prime number calculations AUTH: Jorn Lind diff --git a/buddy/src/reorder.c b/buddy/src/reorder.c index a1f003997..018cfeeb3 100644 --- a/buddy/src/reorder.c +++ b/buddy/src/reorder.c @@ -28,7 +28,7 @@ ========================================================================*/ /************************************************************************* - $Header: /Volumes/CVS/repository/spot/spot/buddy/src/reorder.c,v 1.1 2003/05/05 10:57:57 aduret Exp $ + $Header: /Volumes/CVS/repository/spot/spot/buddy/src/reorder.c,v 1.2 2003/05/05 13:45:08 aduret Exp $ FILE: reorder.c DESCR: BDD reordering functions AUTH: Jorn Lind diff --git a/buddy/src/tree.c b/buddy/src/tree.c index 961c97cb5..d75610821 100644 --- a/buddy/src/tree.c +++ b/buddy/src/tree.c @@ -28,7 +28,7 @@ ========================================================================*/ /************************************************************************* - $Header: /Volumes/CVS/repository/spot/spot/buddy/src/tree.c,v 1.1 2003/05/05 10:57:57 aduret Exp $ + $Header: /Volumes/CVS/repository/spot/spot/buddy/src/tree.c,v 1.2 2003/05/05 13:45:08 aduret Exp $ FILE: tree.c DESCR: Trees for BDD variables AUTH: Jorn Lind