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

* src/pairs.c (bdd_mergepairs): New function.

(bdd_copypair): Revert 2003-05-20's change.  Use bdd_addref
to copy result variables.
parent 039412ea
2003-05-22 Alexandre Duret-Lutz <aduret@src.lip6.fr> 2003-05-22 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/pairs.c (bdd_mergepairs): New function.
(bdd_copypair): Revert 2003-05-20's change. Use bdd_addref
to copy result variables.
* src/bdd.h (BDD_INVMERGE): New error code.
(bdd_mergepairs): Declare.
* src/kernel.c (errorstrings): Add string of BDDINV.
* src/bddop.c (bdd_simplify): Typo in doc, s/domaine/domain/. * src/bddop.c (bdd_simplify): Typo in doc, s/domaine/domain/.
2003-05-20 Alexandre Duret-Lutz <aduret@src.lip6.fr> 2003-05-20 Alexandre Duret-Lutz <aduret@src.lip6.fr>
......
...@@ -28,7 +28,7 @@ ...@@ -28,7 +28,7 @@
========================================================================*/ ========================================================================*/
/************************************************************************* /*************************************************************************
$Header: /Volumes/CVS/repository/spot/spot/buddy/src/bdd.h,v 1.3 2003/05/19 15:58:44 aduret Exp $ $Header: /Volumes/CVS/repository/spot/spot/buddy/src/bdd.h,v 1.4 2003/05/22 15:07:27 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
...@@ -264,6 +264,7 @@ extern void bdd_gbc(void); ...@@ -264,6 +264,7 @@ 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_copypair(bddPair*);
extern bddPair* bdd_mergepairs(bddPair*, 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);
...@@ -410,7 +411,9 @@ extern const BDD bddtrue; ...@@ -410,7 +411,9 @@ extern const BDD bddtrue;
#define BVEC_SHIFT (-21) /* Illegal shift-left/right parameter */ #define BVEC_SHIFT (-21) /* Illegal shift-left/right parameter */
#define BVEC_DIVZERO (-22) /* Division by zero */ #define BVEC_DIVZERO (-22) /* Division by zero */
#define BDD_ERRNUM 24 #define BDD_INVMERGE (-23) /* Merging clashing rewriting rules */
#define BDD_ERRNUM 25
/************************************************************************* /*************************************************************************
If this file is included from a C++ compiler then the following If this file is included from a C++ compiler then the following
......
...@@ -28,7 +28,7 @@ ...@@ -28,7 +28,7 @@
========================================================================*/ ========================================================================*/
/************************************************************************* /*************************************************************************
$Header: /Volumes/CVS/repository/spot/spot/buddy/src/kernel.c,v 1.4 2003/05/20 08:22:36 aduret Exp $ $Header: /Volumes/CVS/repository/spot/spot/buddy/src/kernel.c,v 1.5 2003/05/22 15:07:27 aduret Exp $
FILE: kernel.c FILE: kernel.c
DESCR: implements the bdd kernel functions. DESCR: implements the bdd kernel functions.
AUTH: Jorn Lind AUTH: Jorn Lind
...@@ -133,7 +133,8 @@ static char *errorstrings[BDD_ERRNUM] = ...@@ -133,7 +133,8 @@ static char *errorstrings[BDD_ERRNUM] =
"Bad size argument", "Bad size argument",
"Mismatch in bitvector size", "Mismatch in bitvector size",
"Illegal shift-left/right parameter", "Illegal shift-left/right parameter",
"Division by zero" }; "Division by zero",
"Unmergeable rewritings."};
/*=== OTHER INTERNAL DEFINITIONS =======================================*/ /*=== OTHER INTERNAL DEFINITIONS =======================================*/
......
...@@ -28,7 +28,7 @@ ...@@ -28,7 +28,7 @@
========================================================================*/ ========================================================================*/
/************************************************************************* /*************************************************************************
$Header: /Volumes/CVS/repository/spot/spot/buddy/src/pairs.c,v 1.6 2003/05/22 12:07:52 aduret Exp $ $Header: /Volumes/CVS/repository/spot/spot/buddy/src/pairs.c,v 1.7 2003/05/22 15:07:27 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
...@@ -203,7 +203,8 @@ bddPair *bdd_copypair(bddPair *from) ...@@ -203,7 +203,8 @@ bddPair *bdd_copypair(bddPair *from)
if (p == NULL) if (p == NULL)
return NULL; return NULL;
memcpy(p->result, from->result, bddvarnum * sizeof(*p->result)); for (n=0 ; n<bddvarnum ; n++)
p->result[n] = bdd_addref(from->result[n]);
p->id = update_pairsid(); p->id = update_pairsid();
p->last = from->last; p->last = from->last;
...@@ -212,6 +213,59 @@ bddPair *bdd_copypair(bddPair *from) ...@@ -212,6 +213,59 @@ bddPair *bdd_copypair(bddPair *from)
return p; return p;
} }
/*
NAME {* bdd\_mergepairs *}
SECTION {* kernel *}
SHORT {* merge two pair tables *}
PROTO {* bddPair *bdd_mergepairs(bddPair *left, bddPairs *right) *}
DESCR {* Create a table of pairs that can be used to perform the
rewritings of both {\tt left} and {\tt right}. This cannot work if
the two tables contain incompatible rewrite pairs (for instance
if left rewrite 1 to 2, and right rewrite 1 to 3).
This function allocates a new table. The
table can be freed by a call to {\tt bdd\_freepair}. *}
RETURN {* Returns a new table of pairs. *}
ALSO {* bdd\_newpair, bdd\_freepair, bdd\_replace, bdd\_setpair, bdd\_setpairs *}
*/
bddPair *bdd_mergepairs(bddPair *left, bddPair *right)
{
int n;
bddPair *p;
p = bdd_copypair(left);
if (p == NULL)
return NULL;
for (n=0; n<bddvarnum; n++)
{
bdd nl = bdd_ithvar(n);
/* If P performs no rewriting for N, blindly use that of RIGHT. */
if (nl == p->result[n])
{
bdd_delref(p->result[n]);
p->result[n] = bdd_addref(right->result[n]);
}
else
/* If P rewrites N, make sure RIGHT doesn't rewrite it, or that
it rewrites it to the same variable. */
if (nl != right->result[n] && right->result[n] != p->result[n])
{
bdd_freepair(p);
bdd_error(BDD_INVMERGE);
return NULL;
}
}
if (p->last < right->last)
p->last = right->last;
/* We don't have to update the ID, because this pair was not
used since bdd_copypair were called. */
return p;
}
/* /*
NAME {* bdd\_setpair *} NAME {* bdd\_setpair *}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment