* src/bdd.h: Declare bdd_copypair().
* src/pairs.c (bdd_copypair, bdd_pairalloc): New functions. (bdd_newpair): Use bdd_pairalloc.
This commit is contained in:
parent
38f7ae9a46
commit
ed8ae1ed55
3 changed files with 106 additions and 60 deletions
|
|
@ -1,3 +1,9 @@
|
||||||
|
2003-05-19 Alexandre Duret-Lutz <aduret@src.lip6.fr>
|
||||||
|
|
||||||
|
* 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 <aduret@src.lip6.fr>
|
2003-05-12 Alexandre Duret-Lutz <aduret@src.lip6.fr>
|
||||||
|
|
||||||
* src/kernel.c (bdd_default_errhandler): Call abort(), not exit(1).
|
* src/kernel.c (bdd_default_errhandler): Call abort(), not exit(1).
|
||||||
|
|
@ -13,9 +19,9 @@
|
||||||
* src/Makefile.am (AM_CPPFLAGS): New variable.
|
* src/Makefile.am (AM_CPPFLAGS): New variable.
|
||||||
|
|
||||||
* configure.ac, Makefile.am, src/Makefile.am, doc/Makefile.am,
|
* 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/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/internal/Makefile.am, examples/milner/Makefile.am,
|
||||||
examples/money/Makefile.am, examples/queen/Makefile.am,
|
examples/money/Makefile.am, examples/queen/Makefile.am,
|
||||||
examples/solitar/Makefile.am, m4/debug.m4, m4/gccwarns.m4,
|
examples/solitar/Makefile.am, m4/debug.m4, m4/gccwarns.m4,
|
||||||
|
|
@ -26,9 +32,9 @@
|
||||||
examples/internal/makefile, examples/milner/makefile,
|
examples/internal/makefile, examples/milner/makefile,
|
||||||
examples/money/makefile, examples/queen/makefile,
|
examples/money/makefile, examples/queen/makefile,
|
||||||
examples/solitare/makefile : Delete.
|
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/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/solitare/solitare.cxx: Include iostream.
|
||||||
* examples/calculator/parser.y: Rename as ...
|
* examples/calculator/parser.y: Rename as ...
|
||||||
* examples/calculator/parser.yxx: ... this. Remove spurious
|
* examples/calculator/parser.yxx: ... this. Remove spurious
|
||||||
|
|
@ -39,9 +45,8 @@
|
||||||
* examples/calculator/lexer.l: Rename as ...
|
* examples/calculator/lexer.l: Rename as ...
|
||||||
* examples/calculator/lexer.lxx: ... this. Include parser.h
|
* examples/calculator/lexer.lxx: ... this. Include parser.h
|
||||||
instead of tokens.h.
|
instead of tokens.h.
|
||||||
* examples/calculator/slist.h
|
* examples/calculator/slist.h
|
||||||
(voidSList::voisSListElem, SList::ite): Fix friend usage.
|
(voidSList::voisSListElem, SList::ite): Fix friend usage.
|
||||||
* src/kernel.h (DEFAULT_CLOCK): Default to 60 if not already
|
* src/kernel.h (DEFAULT_CLOCK): Default to 60 if not already
|
||||||
defined.
|
defined.
|
||||||
* README: Update build instruction, and file listing.
|
* README: Update build instruction, and file listing.
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
/*========================================================================
|
/*========================================================================
|
||||||
Copyright (C) 1996-2002 by Jorn Lind-Nielsen
|
Copyright (C) 1996-2002 by Jorn Lind-Nielsen
|
||||||
All rights reserved
|
All rights reserved
|
||||||
|
|
||||||
Permission is hereby granted, without written agreement and without
|
Permission is hereby granted, without written agreement and without
|
||||||
license or royalty fees, to use, reproduce, prepare derivative
|
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
|
FILE: bdd.h
|
||||||
DESCR: C,C++ User interface for the BDD package
|
DESCR: C,C++ User interface for the BDD package
|
||||||
AUTH: Jorn Lind
|
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 maxnodenum} & user defined maximum number of bdd nodes \\
|
||||||
{\tt freenodes} & number of currently free nodes \\
|
{\tt freenodes} & number of currently free nodes \\
|
||||||
{\tt minfreenodes} & minimum number of nodes that should be left after a
|
{\tt minfreenodes} & minimum number of nodes that should be left after a
|
||||||
garbage collection. \\
|
garbage collection. \\
|
||||||
{\tt varnum} & number of defined bdd variables \\
|
{\tt varnum} & number of defined bdd variables \\
|
||||||
{\tt cachesize} & number of entries in the internal caches \\
|
{\tt cachesize} & number of entries in the internal caches \\
|
||||||
{\tt gbcnum} & number of garbage collections done until now
|
{\tt gbcnum} & number of garbage collections done until now
|
||||||
|
|
@ -200,7 +200,7 @@ SECTION {* operator *}
|
||||||
SHORT {* relational product *}
|
SHORT {* relational product *}
|
||||||
PROTO {* #define bdd_relprod(a,b,var) bdd_appex(a,b,bddop_and,var) *}
|
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
|
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. *}
|
afterwards. *}
|
||||||
RETURN {* The relational product or {\tt bddfalse} on errors. *}
|
RETURN {* The relational product or {\tt bddfalse} on errors. *}
|
||||||
ALSO {* bdd\_appex *}
|
ALSO {* bdd\_appex *}
|
||||||
|
|
@ -220,13 +220,13 @@ typedef void (*bdd2inthandler)(int,int);
|
||||||
typedef int (*bddsizehandler)(void);
|
typedef int (*bddsizehandler)(void);
|
||||||
typedef void (*bddfilehandler)(FILE *, int);
|
typedef void (*bddfilehandler)(FILE *, int);
|
||||||
typedef void (*bddallsathandler)(char*, int);
|
typedef void (*bddallsathandler)(char*, int);
|
||||||
|
|
||||||
extern bddinthandler bdd_error_hook(bddinthandler);
|
extern bddinthandler bdd_error_hook(bddinthandler);
|
||||||
extern bddgbchandler bdd_gbc_hook(bddgbchandler);
|
extern bddgbchandler bdd_gbc_hook(bddgbchandler);
|
||||||
extern bdd2inthandler bdd_resize_hook(bdd2inthandler);
|
extern bdd2inthandler bdd_resize_hook(bdd2inthandler);
|
||||||
extern bddinthandler bdd_reorder_hook(bddinthandler);
|
extern bddinthandler bdd_reorder_hook(bddinthandler);
|
||||||
extern bddfilehandler bdd_file_hook(bddfilehandler);
|
extern bddfilehandler bdd_file_hook(bddfilehandler);
|
||||||
|
|
||||||
extern int bdd_init(int, int);
|
extern int bdd_init(int, int);
|
||||||
extern void bdd_done(void);
|
extern void bdd_done(void);
|
||||||
extern int bdd_setvarnum(int);
|
extern int bdd_setvarnum(int);
|
||||||
|
|
@ -263,6 +263,7 @@ extern BDD bdd_delref(BDD);
|
||||||
extern void bdd_gbc(void);
|
extern void bdd_gbc(void);
|
||||||
extern int bdd_scanset(BDD, int**, int*);
|
extern int bdd_scanset(BDD, int**, int*);
|
||||||
extern BDD bdd_makeset(int *, int);
|
extern BDD bdd_makeset(int *, int);
|
||||||
|
extern bddPair* bdd_copypair(bddPair*);
|
||||||
extern bddPair* bdd_newpair(void);
|
extern bddPair* bdd_newpair(void);
|
||||||
extern int bdd_setpair(bddPair*, int, int);
|
extern int bdd_setpair(bddPair*, int, int);
|
||||||
extern int bdd_setpairs(bddPair*, int*, 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 int* bdd_varprofile(BDD);
|
||||||
extern double bdd_pathcount(BDD);
|
extern double bdd_pathcount(BDD);
|
||||||
|
|
||||||
|
|
||||||
/* In file "bddio.c" */
|
/* In file "bddio.c" */
|
||||||
|
|
||||||
extern void bdd_printall(void);
|
extern void bdd_printall(void);
|
||||||
|
|
@ -395,7 +396,7 @@ extern const BDD bddtrue;
|
||||||
#define BDD_BREAK (-9) /* User called break */
|
#define BDD_BREAK (-9) /* User called break */
|
||||||
#define BDD_VARNUM (-10) /* Different number of vars. for vector pair */
|
#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 */
|
#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_OP (-12) /* Unknown operator */
|
||||||
#define BDD_VARSET (-13) /* Illegal variable set */
|
#define BDD_VARSET (-13) /* Illegal variable set */
|
||||||
#define BDD_VARBLK (-14) /* Bad variable block operation */
|
#define BDD_VARBLK (-14) /* Bad variable block operation */
|
||||||
|
|
@ -431,9 +432,9 @@ class bdd
|
||||||
~bdd(void) { bdd_delref(root); }
|
~bdd(void) { bdd_delref(root); }
|
||||||
|
|
||||||
int id(void) const;
|
int id(void) const;
|
||||||
|
|
||||||
bdd operator=(const bdd &r);
|
bdd operator=(const bdd &r);
|
||||||
|
|
||||||
bdd operator&(const bdd &r) const;
|
bdd operator&(const bdd &r) const;
|
||||||
bdd operator&=(const bdd &r);
|
bdd operator&=(const bdd &r);
|
||||||
bdd operator^(const bdd &r) const;
|
bdd operator^(const bdd &r) const;
|
||||||
|
|
@ -451,7 +452,7 @@ class bdd
|
||||||
bdd operator<<=(const bdd &r);
|
bdd operator<<=(const bdd &r);
|
||||||
int operator==(const bdd &r) const;
|
int operator==(const bdd &r) const;
|
||||||
int operator!=(const bdd &r) const;
|
int operator!=(const bdd &r) const;
|
||||||
|
|
||||||
private:
|
private:
|
||||||
BDD root;
|
BDD root;
|
||||||
|
|
||||||
|
|
@ -506,7 +507,7 @@ private:
|
||||||
friend int bdd_anodecountpp(const bdd *, int);
|
friend int bdd_anodecountpp(const bdd *, int);
|
||||||
friend int* bdd_varprofile(const bdd &);
|
friend int* bdd_varprofile(const bdd &);
|
||||||
friend double bdd_pathcount(const bdd &);
|
friend double bdd_pathcount(const bdd &);
|
||||||
|
|
||||||
friend void bdd_fprinttable(FILE *, const bdd &);
|
friend void bdd_fprinttable(FILE *, const bdd &);
|
||||||
friend void bdd_printtable(const bdd &);
|
friend void bdd_printtable(const bdd &);
|
||||||
friend void bdd_fprintset(FILE *, const bdd &);
|
friend void bdd_fprintset(FILE *, const bdd &);
|
||||||
|
|
@ -519,7 +520,7 @@ private:
|
||||||
friend int bdd_save(FILE*, const bdd &);
|
friend int bdd_save(FILE*, const bdd &);
|
||||||
friend int bdd_fnload(char*, bdd &);
|
friend int bdd_fnload(char*, bdd &);
|
||||||
friend int bdd_load(FILE*, bdd &);
|
friend int bdd_load(FILE*, bdd &);
|
||||||
|
|
||||||
friend bdd fdd_ithvarpp(int, int);
|
friend bdd fdd_ithvarpp(int, int);
|
||||||
friend bdd fdd_ithsetpp(int);
|
friend bdd fdd_ithsetpp(int);
|
||||||
friend bdd fdd_domainpp(int);
|
friend bdd fdd_domainpp(int);
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
/*========================================================================
|
/*========================================================================
|
||||||
Copyright (C) 1996-2002 by Jorn Lind-Nielsen
|
Copyright (C) 1996-2002 by Jorn Lind-Nielsen
|
||||||
All rights reserved
|
All rights reserved
|
||||||
|
|
||||||
Permission is hereby granted, without written agreement and without
|
Permission is hereby granted, without written agreement and without
|
||||||
license or royalty fees, to use, reproduce, prepare derivative
|
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
|
FILE: pairs.c
|
||||||
DESCR: Pair management for BDD package.
|
DESCR: Pair management for BDD package.
|
||||||
AUTH: Jorn Lind
|
AUTH: Jorn Lind
|
||||||
|
|
@ -74,7 +74,7 @@ void bdd_pairs_done(void)
|
||||||
static int update_pairsid(void)
|
static int update_pairsid(void)
|
||||||
{
|
{
|
||||||
pairsid++;
|
pairsid++;
|
||||||
|
|
||||||
if (pairsid == (INT_MAX >> 2))
|
if (pairsid == (INT_MAX >> 2))
|
||||||
{
|
{
|
||||||
bddPair *p;
|
bddPair *p;
|
||||||
|
|
@ -98,7 +98,7 @@ void bdd_register_pair(bddPair *p)
|
||||||
void bdd_pairs_vardown(int level)
|
void bdd_pairs_vardown(int level)
|
||||||
{
|
{
|
||||||
bddPair *p;
|
bddPair *p;
|
||||||
|
|
||||||
for (p=pairs ; p!=NULL ; p=p->next)
|
for (p=pairs ; p!=NULL ; p=p->next)
|
||||||
{
|
{
|
||||||
int tmp;
|
int tmp;
|
||||||
|
|
@ -106,18 +106,37 @@ void bdd_pairs_vardown(int level)
|
||||||
tmp = p->result[level];
|
tmp = p->result[level];
|
||||||
p->result[level] = p->result[level+1];
|
p->result[level] = p->result[level+1];
|
||||||
p->result[level+1] = tmp;
|
p->result[level+1] = tmp;
|
||||||
|
|
||||||
if (p->last == level)
|
if (p->last == level)
|
||||||
p->last++;
|
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)
|
int bdd_pairs_resize(int oldsize, int newsize)
|
||||||
{
|
{
|
||||||
bddPair *p;
|
bddPair *p;
|
||||||
int n;
|
int n;
|
||||||
|
|
||||||
for (p=pairs ; p!=NULL ; p=p->next)
|
for (p=pairs ; p!=NULL ; p=p->next)
|
||||||
{
|
{
|
||||||
if ((p->result=(BDD*)realloc(p->result,sizeof(BDD)*newsize)) == NULL)
|
if ((p->result=(BDD*)realloc(p->result,sizeof(BDD)*newsize)) == NULL)
|
||||||
|
|
@ -137,7 +156,7 @@ SECTION {* kernel *}
|
||||||
SHORT {* creates an empty variable pair table *}
|
SHORT {* creates an empty variable pair table *}
|
||||||
PROTO {* bddPair *bdd_newpair(void) *}
|
PROTO {* bddPair *bdd_newpair(void) *}
|
||||||
DESCR {* Variable pairs of the type {\tt bddPair} are used in
|
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
|
other variables. This function allocates such an empty table. The
|
||||||
table can be freed by a call to {\em bdd\_freepair}. *}
|
table can be freed by a call to {\em bdd\_freepair}. *}
|
||||||
RETURN {* Returns a new table of pairs. *}
|
RETURN {* Returns a new table of pairs. *}
|
||||||
|
|
@ -147,26 +166,48 @@ bddPair *bdd_newpair(void)
|
||||||
{
|
{
|
||||||
int n;
|
int n;
|
||||||
bddPair *p;
|
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 ; n<bddvarnum ; n++)
|
for (n=0 ; n<bddvarnum ; n++)
|
||||||
p->result[n] = bdd_ithvar(bddlevel2var[n]);
|
p->result[n] = bdd_ithvar(bddlevel2var[n]);
|
||||||
|
|
||||||
p->id = update_pairsid();
|
p->id = update_pairsid();
|
||||||
p->last = -1;
|
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 ; n<bddvarnum ; n++)
|
||||||
|
p->result[n] = from->result[n];
|
||||||
|
|
||||||
|
p->id = update_pairsid();
|
||||||
|
p->last = -1;
|
||||||
|
|
||||||
bdd_register_pair(p);
|
bdd_register_pair(p);
|
||||||
return p;
|
return p;
|
||||||
}
|
}
|
||||||
|
|
@ -180,7 +221,7 @@ SHORT {* set one variable pair *}
|
||||||
PROTO {* int bdd_setpair(bddPair *pair, int oldvar, int newvar)
|
PROTO {* int bdd_setpair(bddPair *pair, int oldvar, int newvar)
|
||||||
int bdd_setbddpair(bddPair *pair, BDD oldvar, BDD newvar) *}
|
int bdd_setbddpair(bddPair *pair, BDD oldvar, BDD newvar) *}
|
||||||
DESCR {* Adds the pair {\tt (oldvar,newvar)} to the table of pairs
|
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
|
with {\tt newvar} in a call to {\tt bdd\_replace}. In the first
|
||||||
version {\tt newvar} is an integer representing the variable
|
version {\tt newvar} is an integer representing the variable
|
||||||
to be replaced with the old variable.
|
to be replaced with the old variable.
|
||||||
|
|
@ -197,7 +238,7 @@ int bdd_setpair(bddPair *pair, int oldvar, int newvar)
|
||||||
{
|
{
|
||||||
if (pair == NULL)
|
if (pair == NULL)
|
||||||
return 0;
|
return 0;
|
||||||
|
|
||||||
if (oldvar < 0 || oldvar > bddvarnum-1)
|
if (oldvar < 0 || oldvar > bddvarnum-1)
|
||||||
return bdd_error(BDD_VAR);
|
return bdd_error(BDD_VAR);
|
||||||
if (newvar < 0 || newvar > bddvarnum-1)
|
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]] );
|
bdd_delref( pair->result[bddvar2level[oldvar]] );
|
||||||
pair->result[bddvar2level[oldvar]] = bdd_ithvar(newvar);
|
pair->result[bddvar2level[oldvar]] = bdd_ithvar(newvar);
|
||||||
pair->id = update_pairsid();
|
pair->id = update_pairsid();
|
||||||
|
|
||||||
if (bddvar2level[oldvar] > pair->last)
|
if (bddvar2level[oldvar] > pair->last)
|
||||||
pair->last = bddvar2level[oldvar];
|
pair->last = bddvar2level[oldvar];
|
||||||
|
|
||||||
return 0;
|
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 bdd_setbddpair(bddPair *pair, int oldvar, BDD newvar)
|
||||||
{
|
{
|
||||||
int oldlevel;
|
int oldlevel;
|
||||||
|
|
||||||
if (pair == NULL)
|
if (pair == NULL)
|
||||||
return 0;
|
return 0;
|
||||||
|
|
||||||
|
|
@ -225,14 +266,14 @@ int bdd_setbddpair(bddPair *pair, int oldvar, BDD newvar)
|
||||||
if (oldvar < 0 || oldvar >= bddvarnum)
|
if (oldvar < 0 || oldvar >= bddvarnum)
|
||||||
return bdd_error(BDD_VAR);
|
return bdd_error(BDD_VAR);
|
||||||
oldlevel = bddvar2level[oldvar];
|
oldlevel = bddvar2level[oldvar];
|
||||||
|
|
||||||
bdd_delref( pair->result[oldlevel] );
|
bdd_delref( pair->result[oldlevel] );
|
||||||
pair->result[oldlevel] = bdd_addref(newvar);
|
pair->result[oldlevel] = bdd_addref(newvar);
|
||||||
pair->id = update_pairsid();
|
pair->id = update_pairsid();
|
||||||
|
|
||||||
if (oldlevel > pair->last)
|
if (oldlevel > pair->last)
|
||||||
pair->last = oldlevel;
|
pair->last = oldlevel;
|
||||||
|
|
||||||
return 0;
|
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)
|
PROTO {* int bdd_setpairs(bddPair *pair, int *oldvar, int *newvar, int size)
|
||||||
int bdd_setbddpairs(bddPair *pair, int *oldvar, BDD *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}
|
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. *}
|
RETURN {* Zero on success, otherwise a negative error code. *}
|
||||||
ALSO {* bdd\_newpair, bdd\_setpair, bdd\_replace, bdd\_compose *}
|
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;
|
int n,e;
|
||||||
if (pair == NULL)
|
if (pair == NULL)
|
||||||
return 0;
|
return 0;
|
||||||
|
|
||||||
for (n=0 ; n<size ; n++)
|
for (n=0 ; n<size ; n++)
|
||||||
if ((e=bdd_setpair(pair, oldvar[n], newvar[n])) < 0)
|
if ((e=bdd_setpair(pair, oldvar[n], newvar[n])) < 0)
|
||||||
return e;
|
return e;
|
||||||
|
|
||||||
return 0;
|
return 0;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -268,11 +309,11 @@ int bdd_setbddpairs(bddPair *pair, int *oldvar, BDD *newvar, int size)
|
||||||
int n,e;
|
int n,e;
|
||||||
if (pair == NULL)
|
if (pair == NULL)
|
||||||
return 0;
|
return 0;
|
||||||
|
|
||||||
for (n=0 ; n<size ; n++)
|
for (n=0 ; n<size ; n++)
|
||||||
if ((e=bdd_setbddpair(pair, oldvar[n], newvar[n])) < 0)
|
if ((e=bdd_setbddpair(pair, oldvar[n], newvar[n])) < 0)
|
||||||
return e;
|
return e;
|
||||||
|
|
||||||
return 0;
|
return 0;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -283,16 +324,16 @@ SECTION {* kernel *}
|
||||||
SHORT {* frees a table of pairs *}
|
SHORT {* frees a table of pairs *}
|
||||||
PROTO {* void bdd_freepair(bddPair *pair) *}
|
PROTO {* void bdd_freepair(bddPair *pair) *}
|
||||||
DESCR {* Frees the table of pairs {\tt pair} that has been allocated
|
DESCR {* Frees the table of pairs {\tt pair} that has been allocated
|
||||||
by a call to {\tt bdd\_newpair}. *}
|
by a call to {\tt bdd\_newpair}. *}
|
||||||
ALSO {* bdd\_replace, bdd\_newpair, bdd\_setpair, bdd\_resetpair *}
|
ALSO {* bdd\_replace, bdd\_newpair, bdd\_setpair, bdd\_resetpair *}
|
||||||
*/
|
*/
|
||||||
void bdd_freepair(bddPair *p)
|
void bdd_freepair(bddPair *p)
|
||||||
{
|
{
|
||||||
int n;
|
int n;
|
||||||
|
|
||||||
if (p == NULL)
|
if (p == NULL)
|
||||||
return;
|
return;
|
||||||
|
|
||||||
if (pairs != p)
|
if (pairs != p)
|
||||||
{
|
{
|
||||||
bddPair *bp = pairs;
|
bddPair *bp = pairs;
|
||||||
|
|
@ -318,7 +359,7 @@ SECTION {* kernel *}
|
||||||
SHORT {* clear all variable pairs *}
|
SHORT {* clear all variable pairs *}
|
||||||
PROTO {* void bdd_resetpair(bddPair *pair) *}
|
PROTO {* void bdd_resetpair(bddPair *pair) *}
|
||||||
DESCR {* Resets the table of pairs {\tt pair} by setting all substitutions
|
DESCR {* Resets the table of pairs {\tt pair} by setting all substitutions
|
||||||
to their default values (that is no change). *}
|
to their default values (that is no change). *}
|
||||||
ALSO {* bdd\_newpair, bdd\_setpair, bdd\_freepair *}
|
ALSO {* bdd\_newpair, bdd\_setpair, bdd\_freepair *}
|
||||||
*/
|
*/
|
||||||
void bdd_resetpair(bddPair *p)
|
void bdd_resetpair(bddPair *p)
|
||||||
|
|
@ -332,4 +373,3 @@ void bdd_resetpair(bddPair *p)
|
||||||
|
|
||||||
|
|
||||||
/* EOF */
|
/* EOF */
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue