diff --git a/buddy/ChangeLog b/buddy/ChangeLog index 6abf97a5b..ea760a74b 100644 --- a/buddy/ChangeLog +++ b/buddy/ChangeLog @@ -1,3 +1,9 @@ +2003-05-19 Alexandre Duret-Lutz + + * src/bdd.h: Declare bdd_copypair(). + * src/pairs.c (bdd_copypair, bdd_pairalloc): New functions. + (bdd_newpair): Use bdd_pairalloc. + 2003-05-12 Alexandre Duret-Lutz * src/kernel.c (bdd_default_errhandler): Call abort(), not exit(1). @@ -13,9 +19,9 @@ * src/Makefile.am (AM_CPPFLAGS): New variable. * configure.ac, Makefile.am, src/Makefile.am, doc/Makefile.am, - examples/Makefile.am, examples/Makefile.def, + examples/Makefile.am, examples/Makefile.def, examples/adder/Makefile.am, examples/calculator/Makefile.am, - examples/cmilner/Makefile.am, examples/fdd/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, @@ -26,9 +32,9 @@ 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/adder/adder.cxx, examples/fdd/statespace.cxx, examples/internal/bddtest.cxx, examples/milner/milner.cxx, - examples/money/money.cxx, examples/queen/queen.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 @@ -39,9 +45,8 @@ * examples/calculator/lexer.l: Rename as ... * examples/calculator/lexer.lxx: ... this. Include parser.h instead of tokens.h. - * examples/calculator/slist.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/src/bdd.h b/buddy/src/bdd.h index 4e2a1f5d5..804516700 100644 --- a/buddy/src/bdd.h +++ b/buddy/src/bdd.h @@ -1,6 +1,6 @@ /*======================================================================== - Copyright (C) 1996-2002 by Jorn Lind-Nielsen - All rights reserved + Copyright (C) 1996-2002 by Jorn Lind-Nielsen + All rights reserved Permission is hereby granted, without written agreement and without license or royalty fees, to use, reproduce, prepare derivative @@ -28,7 +28,7 @@ ========================================================================*/ /************************************************************************* - $Header: /Volumes/CVS/repository/spot/spot/buddy/src/bdd.h,v 1.2 2003/05/05 13:45:04 aduret Exp $ + $Header: /Volumes/CVS/repository/spot/spot/buddy/src/bdd.h,v 1.3 2003/05/19 15:58:44 aduret Exp $ FILE: bdd.h DESCR: C,C++ User interface for the BDD package AUTH: Jorn Lind @@ -104,7 +104,7 @@ DESCR {* The fields are \\[\baselineskip] \begin{tabular}{lp{10cm}} {\tt maxnodenum} & user defined maximum number of bdd nodes \\ {\tt freenodes} & number of currently free nodes \\ {\tt minfreenodes} & minimum number of nodes that should be left after a - garbage collection. \\ + garbage collection. \\ {\tt varnum} & number of defined bdd variables \\ {\tt cachesize} & number of entries in the internal caches \\ {\tt gbcnum} & number of garbage collections done until now @@ -200,7 +200,7 @@ SECTION {* operator *} SHORT {* relational product *} PROTO {* #define bdd_relprod(a,b,var) bdd_appex(a,b,bddop_and,var) *} DESCR {* Calculates the relational product of {\tt a} and {\tt b} as - {\tt a AND b} with the variables in {\tt var} quantified out + {\tt a AND b} with the variables in {\tt var} quantified out afterwards. *} RETURN {* The relational product or {\tt bddfalse} on errors. *} ALSO {* bdd\_appex *} @@ -220,13 +220,13 @@ typedef void (*bdd2inthandler)(int,int); typedef int (*bddsizehandler)(void); typedef void (*bddfilehandler)(FILE *, int); typedef void (*bddallsathandler)(char*, int); - + extern bddinthandler bdd_error_hook(bddinthandler); extern bddgbchandler bdd_gbc_hook(bddgbchandler); extern bdd2inthandler bdd_resize_hook(bdd2inthandler); extern bddinthandler bdd_reorder_hook(bddinthandler); extern bddfilehandler bdd_file_hook(bddfilehandler); - + extern int bdd_init(int, int); extern void bdd_done(void); extern int bdd_setvarnum(int); @@ -263,6 +263,7 @@ extern BDD bdd_delref(BDD); extern void bdd_gbc(void); extern int bdd_scanset(BDD, int**, int*); extern BDD bdd_makeset(int *, int); +extern bddPair* bdd_copypair(bddPair*); extern bddPair* bdd_newpair(void); extern int bdd_setpair(bddPair*, int, int); extern int bdd_setpairs(bddPair*, int*, int*, int); @@ -310,7 +311,7 @@ extern int bdd_anodecount(BDD *, int); extern int* bdd_varprofile(BDD); extern double bdd_pathcount(BDD); - + /* In file "bddio.c" */ extern void bdd_printall(void); @@ -395,7 +396,7 @@ extern const BDD bddtrue; #define BDD_BREAK (-9) /* User called break */ #define BDD_VARNUM (-10) /* Different number of vars. for vector pair */ #define BDD_NODES (-11) /* Tried to set max. number of nodes to be fewer */ - /* than there already has been allocated */ + /* than there already has been allocated */ #define BDD_OP (-12) /* Unknown operator */ #define BDD_VARSET (-13) /* Illegal variable set */ #define BDD_VARBLK (-14) /* Bad variable block operation */ @@ -431,9 +432,9 @@ class bdd ~bdd(void) { bdd_delref(root); } int id(void) const; - + bdd operator=(const bdd &r); - + bdd operator&(const bdd &r) const; bdd operator&=(const bdd &r); bdd operator^(const bdd &r) const; @@ -451,7 +452,7 @@ class bdd bdd operator<<=(const bdd &r); int operator==(const bdd &r) const; int operator!=(const bdd &r) const; - + private: BDD root; @@ -506,7 +507,7 @@ private: friend int bdd_anodecountpp(const bdd *, int); friend int* bdd_varprofile(const bdd &); friend double bdd_pathcount(const bdd &); - + friend void bdd_fprinttable(FILE *, const bdd &); friend void bdd_printtable(const bdd &); friend void bdd_fprintset(FILE *, const bdd &); @@ -519,7 +520,7 @@ private: friend int bdd_save(FILE*, const bdd &); friend int bdd_fnload(char*, bdd &); friend int bdd_load(FILE*, bdd &); - + friend bdd fdd_ithvarpp(int, int); friend bdd fdd_ithsetpp(int); friend bdd fdd_domainpp(int); diff --git a/buddy/src/pairs.c b/buddy/src/pairs.c index bd05af81b..4bfaecdea 100644 --- a/buddy/src/pairs.c +++ b/buddy/src/pairs.c @@ -1,6 +1,6 @@ /*======================================================================== - Copyright (C) 1996-2002 by Jorn Lind-Nielsen - All rights reserved + Copyright (C) 1996-2002 by Jorn Lind-Nielsen + All rights reserved Permission is hereby granted, without written agreement and without license or royalty fees, to use, reproduce, prepare derivative @@ -28,7 +28,7 @@ ========================================================================*/ /************************************************************************* - $Header: /Volumes/CVS/repository/spot/spot/buddy/src/pairs.c,v 1.2 2003/05/05 13:45:08 aduret Exp $ + $Header: /Volumes/CVS/repository/spot/spot/buddy/src/pairs.c,v 1.3 2003/05/19 15:58:44 aduret Exp $ FILE: pairs.c DESCR: Pair management for BDD package. AUTH: Jorn Lind @@ -74,7 +74,7 @@ void bdd_pairs_done(void) static int update_pairsid(void) { pairsid++; - + if (pairsid == (INT_MAX >> 2)) { bddPair *p; @@ -98,7 +98,7 @@ void bdd_register_pair(bddPair *p) void bdd_pairs_vardown(int level) { bddPair *p; - + for (p=pairs ; p!=NULL ; p=p->next) { int tmp; @@ -106,18 +106,37 @@ void bdd_pairs_vardown(int level) tmp = p->result[level]; p->result[level] = p->result[level+1]; p->result[level+1] = tmp; - + if (p->last == level) p->last++; } } +static bddPair *bdd_pairalloc() +{ + bddPair *p; + if ((p=(bddPair*)malloc(sizeof(bddPair))) == NULL) + { + bdd_error(BDD_MEMORY); + return NULL; + } + + if ((p->result=(BDD*)malloc(sizeof(BDD)*bddvarnum)) == NULL) + { + free(p); + bdd_error(BDD_MEMORY); + return NULL; + } + return p; +} + + int bdd_pairs_resize(int oldsize, int newsize) { bddPair *p; int n; - + for (p=pairs ; p!=NULL ; p=p->next) { if ((p->result=(BDD*)realloc(p->result,sizeof(BDD)*newsize)) == NULL) @@ -137,7 +156,7 @@ SECTION {* kernel *} SHORT {* creates an empty variable pair table *} PROTO {* bddPair *bdd_newpair(void) *} DESCR {* Variable pairs of the type {\tt bddPair} are used in - {\tt bdd\_replace} to define which variables to replace with + {\tt bdd\_replace} to define which variables to replace with other variables. This function allocates such an empty table. The table can be freed by a call to {\em bdd\_freepair}. *} RETURN {* Returns a new table of pairs. *} @@ -147,26 +166,48 @@ bddPair *bdd_newpair(void) { int n; bddPair *p; - - if ((p=(bddPair*)malloc(sizeof(bddPair))) == NULL) - { - bdd_error(BDD_MEMORY); - return NULL; - } - - if ((p->result=(BDD*)malloc(sizeof(BDD)*bddvarnum)) == NULL) - { - free(p); - bdd_error(BDD_MEMORY); - return NULL; - } + p = bdd_pairalloc(); + if (p == NULL) + return NULL; + for (n=0 ; nresult[n] = bdd_ithvar(bddlevel2var[n]); p->id = update_pairsid(); p->last = -1; - + + bdd_register_pair(p); + return p; +} + + +/* +NAME {* bdd\_copypair *} +SECTION {* kernel *} +SHORT {* clone a pair table *} +PROTO {* bddPair *bdd_copypair(bddPair *from) *} +DESCR {* Duplicate the table of pairs {\tt from}. + This function allocates the cloned table. The + table can be freed by a call to {\em bdd\_freepair}. *} +RETURN {* Returns a new table of pairs. *} +ALSO {* bdd\_newpair, bdd\_freepair, bdd\_replace, bdd\_setpair, bdd\_setpairs *} +*/ +bddPair *bdd_copypair(bddPair *from) +{ + int n; + bddPair *p; + + p = bdd_pairalloc(); + if (p == NULL) + return NULL; + + for (n=0 ; nresult[n] = from->result[n]; + + p->id = update_pairsid(); + p->last = -1; + bdd_register_pair(p); return p; } @@ -180,7 +221,7 @@ SHORT {* set one variable pair *} PROTO {* int bdd_setpair(bddPair *pair, int oldvar, int newvar) int bdd_setbddpair(bddPair *pair, BDD oldvar, BDD newvar) *} DESCR {* Adds the pair {\tt (oldvar,newvar)} to the table of pairs - {\tt pair}. This results in {\tt oldvar} being substituted + {\tt pair}. This results in {\tt oldvar} being substituted with {\tt newvar} in a call to {\tt bdd\_replace}. In the first version {\tt newvar} is an integer representing the variable to be replaced with the old variable. @@ -197,7 +238,7 @@ int bdd_setpair(bddPair *pair, int oldvar, int newvar) { if (pair == NULL) return 0; - + if (oldvar < 0 || oldvar > bddvarnum-1) return bdd_error(BDD_VAR); if (newvar < 0 || newvar > bddvarnum-1) @@ -206,10 +247,10 @@ int bdd_setpair(bddPair *pair, int oldvar, int newvar) bdd_delref( pair->result[bddvar2level[oldvar]] ); pair->result[bddvar2level[oldvar]] = bdd_ithvar(newvar); pair->id = update_pairsid(); - + if (bddvar2level[oldvar] > pair->last) pair->last = bddvar2level[oldvar]; - + return 0; } @@ -217,7 +258,7 @@ int bdd_setpair(bddPair *pair, int oldvar, int newvar) int bdd_setbddpair(bddPair *pair, int oldvar, BDD newvar) { int oldlevel; - + if (pair == NULL) return 0; @@ -225,14 +266,14 @@ int bdd_setbddpair(bddPair *pair, int oldvar, BDD newvar) if (oldvar < 0 || oldvar >= bddvarnum) return bdd_error(BDD_VAR); oldlevel = bddvar2level[oldvar]; - + bdd_delref( pair->result[oldlevel] ); pair->result[oldlevel] = bdd_addref(newvar); pair->id = update_pairsid(); - + if (oldlevel > pair->last) pair->last = oldlevel; - + return 0; } @@ -245,7 +286,7 @@ SHORT {* defines a whole set of pairs *} PROTO {* int bdd_setpairs(bddPair *pair, int *oldvar, int *newvar, int size) int bdd_setbddpairs(bddPair *pair, int *oldvar, BDD *newvar, int size) *} DESCR {* As for {\tt bdd\_setpair} but with {\tt oldvar} and {\tt newvar} - being arrays of variables (BDDs) of size {\tt size}. *} + being arrays of variables (BDDs) of size {\tt size}. *} RETURN {* Zero on success, otherwise a negative error code. *} ALSO {* bdd\_newpair, bdd\_setpair, bdd\_replace, bdd\_compose *} */ @@ -254,11 +295,11 @@ int bdd_setpairs(bddPair *pair, int *oldvar, int *newvar, int size) int n,e; if (pair == NULL) return 0; - + for (n=0 ; n