alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* rsc/bdd.h (bdd_existcomp, bdd_forallcomp,

Browse source 
bdd_uniquecomp, bdd_appexcomp, bdd_appallcomp,
bdd_appunicomp): Declare for C and C++.
* src/bddop.c (CACHEID_EXISTC, CACHEID_FORALLC,
CACHEID_UNIQUEC, CACHEID_APPEXC, CACHEID_APPALC,
CACHEID_APPUNCC): New macros.
(quatvarsetcomp): New variables.
(varset2vartable): Take a second argument to indicate negation,
set quatvarsetcomp.
(INVARSET): Honor quatvarsetcomp.
(quantify): New function, extracted from bdd_exist, bdd_forall,
and bdd_appunicomp.
(bdd_exist, bdd_forall, bdd_appunicomp): Use quantify.
(bdd_existcomp, bdd_forallcomp, bdd_appunicompcomp): New functions.
(appquantify): New function, extracted from bdd_appex, bdd_appall,
and bdd_appuni.
(bdd_appex, bdd_appall, bdd_appuni): Use appquantify.
(bdd_appexcomp, bdd_appallcomp, bdd_appunicomp): New functions.

* src/bddop.c (bdd_support): Return bddtrue when the support
is empty, because variable sets are conjunctions.
This commit is contained in:
Alexandre Duret-Lutz 2003-07-17 14:09:03 +00:00
parent f63c67b507
commit 4bf6c52bea
3 changed files with 243 additions and 206 deletions
Download patch file Download diff file Expand all files Collapse all files

24
buddy/ChangeLog
View file

@ -1,3 +1,27 @@
2003-07-17 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* rsc/bdd.h (bdd_existcomp, bdd_forallcomp,
bdd_uniquecomp, bdd_appexcomp, bdd_appallcomp,
bdd_appunicomp): Declare for C and C++.
* src/bddop.c (CACHEID_EXISTC, CACHEID_FORALLC,
CACHEID_UNIQUEC, CACHEID_APPEXC, CACHEID_APPALC,
CACHEID_APPUNCC): New macros.
(quatvarsetcomp): New variables.
(varset2vartable): Take a second argument to indicate negation,
set quatvarsetcomp.
(INVARSET): Honor quatvarsetcomp.
(quantify): New function, extracted from bdd_exist, bdd_forall,
and bdd_appunicomp.
(bdd_exist, bdd_forall, bdd_appunicomp): Use quantify.
(bdd_existcomp, bdd_forallcomp, bdd_appunicompcomp): New functions.
(appquantify): New function, extracted from bdd_appex, bdd_appall,
and bdd_appuni.
(bdd_appex, bdd_appall, bdd_appuni): Use appquantify.
(bdd_appexcomp, bdd_appallcomp, bdd_appunicomp): New functions.
* src/bddop.c (bdd_support): Return bddtrue when the support
is empty, because variable sets are conjunctions.
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. * src/pairs.c (bdd_mergepairs): New function.

32
buddy/src/bdd.h
View file

@ -28,7 +28,7 @@
========================================================================*/ ========================================================================*/
/************************************************************************* /*************************************************************************
$Header: /Volumes/CVS/repository/spot/spot/buddy/src/bdd.h,v 1.4 2003/05/22 15:07:27 aduret Exp $ $Header: /Volumes/CVS/repository/spot/spot/buddy/src/bdd.h,v 1.5 2003/07/17 14:09:04 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
@ -293,11 +293,17 @@ extern BDD bdd_compose(BDD, BDD, BDD);
extern BDD bdd_veccompose(BDD, bddPair*); extern BDD bdd_veccompose(BDD, bddPair*);
extern BDD bdd_simplify(BDD, BDD); extern BDD bdd_simplify(BDD, BDD);
extern BDD bdd_exist(BDD, BDD); extern BDD bdd_exist(BDD, BDD);
extern BDD bdd_existcomp(BDD, BDD);
extern BDD bdd_forall(BDD, BDD); extern BDD bdd_forall(BDD, BDD);
extern BDD bdd_forallcomp(BDD, BDD);
extern BDD bdd_unique(BDD, BDD); extern BDD bdd_unique(BDD, BDD);
extern BDD bdd_uniquecomp(BDD, BDD);
extern BDD bdd_appex(BDD, BDD, int, BDD); extern BDD bdd_appex(BDD, BDD, int, BDD);
extern BDD bdd_appexcomp(BDD, BDD, int, BDD);
extern BDD bdd_appall(BDD, BDD, int, BDD); extern BDD bdd_appall(BDD, BDD, int, BDD);
extern BDD bdd_appallcomp(BDD, BDD, int, BDD);
extern BDD bdd_appuni(BDD, BDD, int, BDD); extern BDD bdd_appuni(BDD, BDD, int, BDD);
extern BDD bdd_appunicomp(BDD, BDD, int, BDD);
extern BDD bdd_support(BDD); extern BDD bdd_support(BDD);
extern BDD bdd_satone(BDD); extern BDD bdd_satone(BDD);
extern BDD bdd_satoneset(BDD, BDD, BDD); extern BDD bdd_satoneset(BDD, BDD, BDD);
@ -489,11 +495,17 @@ private:
friend bdd bdd_restrict(const bdd &, const bdd &); friend bdd bdd_restrict(const bdd &, const bdd &);
friend bdd bdd_constrain(const bdd &, const bdd &); friend bdd bdd_constrain(const bdd &, const bdd &);
friend bdd bdd_exist(const bdd &, const bdd &); friend bdd bdd_exist(const bdd &, const bdd &);
friend bdd bdd_existcomp(const bdd &, const bdd &);
friend bdd bdd_forall(const bdd &, const bdd &); friend bdd bdd_forall(const bdd &, const bdd &);
friend bdd bdd_forallcomp(const bdd &, const bdd &);
friend bdd bdd_unique(const bdd &, const bdd &); friend bdd bdd_unique(const bdd &, const bdd &);
friend bdd bdd_uniquecomp(const bdd &, const bdd &);
friend bdd bdd_appex(const bdd &, const bdd &, int, const bdd &); friend bdd bdd_appex(const bdd &, const bdd &, int, const bdd &);
friend bdd bdd_appexcomp(const bdd &, const bdd &, int, const bdd &);
friend bdd bdd_appall(const bdd &, const bdd &, int, const bdd &); friend bdd bdd_appall(const bdd &, const bdd &, int, const bdd &);
friend bdd bdd_appallcomp(const bdd &, const bdd &, int, const bdd &);
friend bdd bdd_appuni(const bdd &, const bdd &, int, const bdd &); friend bdd bdd_appuni(const bdd &, const bdd &, int, const bdd &);
friend bdd bdd_appunicomp(const bdd &, const bdd &, int, const bdd &);
friend bdd bdd_replace(const bdd &, bddPair*); friend bdd bdd_replace(const bdd &, bddPair*);
friend bdd bdd_compose(const bdd &, const bdd &, int); friend bdd bdd_compose(const bdd &, const bdd &, int);
friend bdd bdd_veccompose(const bdd &, bddPair*); friend bdd bdd_veccompose(const bdd &, bddPair*);
@ -641,21 +653,39 @@ inline bdd bdd_ite(const bdd &f, const bdd &g, const bdd &h)
inline bdd bdd_exist(const bdd &r, const bdd &var) inline bdd bdd_exist(const bdd &r, const bdd &var)
{ return bdd_exist(r.root, var.root); } { return bdd_exist(r.root, var.root); }
inline bdd bdd_existcomp(const bdd &r, const bdd &var)
{ return bdd_existcomp(r.root, var.root); }
inline bdd bdd_forall(const bdd &r, const bdd &var) inline bdd bdd_forall(const bdd &r, const bdd &var)
{ return bdd_forall(r.root, var.root); } { return bdd_forall(r.root, var.root); }
inline bdd bdd_forallcomp(const bdd &r, const bdd &var)
{ return bdd_forallcomp(r.root, var.root); }
inline bdd bdd_unique(const bdd &r, const bdd &var) inline bdd bdd_unique(const bdd &r, const bdd &var)
{ return bdd_unique(r.root, var.root); } { return bdd_unique(r.root, var.root); }
inline bdd bdd_uniquecomp(const bdd &r, const bdd &var)
{ return bdd_uniquecomp(r.root, var.root); }
inline bdd bdd_appex(const bdd &l, const bdd &r, int op, const bdd &var) inline bdd bdd_appex(const bdd &l, const bdd &r, int op, const bdd &var)
{ return bdd_appex(l.root, r.root, op, var.root); } { return bdd_appex(l.root, r.root, op, var.root); }
inline bdd bdd_appexcomp(const bdd &l, const bdd &r, int op, const bdd &var)
{ return bdd_appexcomp(l.root, r.root, op, var.root); }
inline bdd bdd_appall(const bdd &l, const bdd &r, int op, const bdd &var) inline bdd bdd_appall(const bdd &l, const bdd &r, int op, const bdd &var)
{ return bdd_appall(l.root, r.root, op, var.root); } { return bdd_appall(l.root, r.root, op, var.root); }
inline bdd bdd_appallcomp(const bdd &l, const bdd &r, int op, const bdd &var)
{ return bdd_appallcomp(l.root, r.root, op, var.root); }
inline bdd bdd_appuni(const bdd &l, const bdd &r, int op, const bdd &var) inline bdd bdd_appuni(const bdd &l, const bdd &r, int op, const bdd &var)
{ return bdd_appuni(l.root, r.root, op, var.root); } { return bdd_appuni(l.root, r.root, op, var.root); }
inline bdd bdd_appunicomp(const bdd &l, const bdd &r, int op, const bdd &var)
{ return bdd_appunicomp(l.root, r.root, op, var.root); }
inline bdd bdd_support(const bdd &r) inline bdd bdd_support(const bdd &r)
{ return bdd_support(r.root); } { return bdd_support(r.root); }

381
buddy/src/bddop.c
View file

@ -28,7 +28,7 @@
========================================================================*/ ========================================================================*/
/************************************************************************* /*************************************************************************
$Header: /Volumes/CVS/repository/spot/spot/buddy/src/bddop.c,v 1.6 2003/05/22 12:09:20 aduret Exp $ $Header: /Volumes/CVS/repository/spot/spot/buddy/src/bddop.c,v 1.7 2003/07/17 14:09:04 aduret Exp $
FILE: bddop.c FILE: bddop.c
DESCR: BDD operators DESCR: BDD operators
AUTH: Jorn Lind AUTH: Jorn Lind
@ -62,6 +62,12 @@
#define CACHEID_APPEX 0x3 #define CACHEID_APPEX 0x3
#define CACHEID_APPAL 0x4 #define CACHEID_APPAL 0x4
#define CACHEID_APPUN 0x5 #define CACHEID_APPUN 0x5
#define CACHEID_EXISTC 0x6
#define CACHEID_FORALLC 0x7
#define CACHEID_UNIQUEC 0x8
#define CACHEID_APPEXC 0x9
#define CACHEID_APPALC 0xA
#define CACHEID_APPUNC 0xB
/* Number of boolean operators */ /* Number of boolean operators */
@ -89,6 +95,7 @@ static int appexop; /* Current operator for appex */
static int appexid; /* Current cache id for appex */ static int appexid; /* Current cache id for appex */
static int quantid; /* Current cache id for quantifications */ static int quantid; /* Current cache id for quantifications */
static int *quantvarset; /* Current variable set for quant. */ static int *quantvarset; /* Current variable set for quant. */
static int quantvarsetcomp; /* Should quantvarset be complemented? */
static int quantvarsetID; /* Current id used in quantvarset */ static int quantvarsetID; /* Current id used in quantvarset */
static int quantlast; /* Current last variable to be quant. */ static int quantlast; /* Current last variable to be quant. */
static int replaceid; /* Current cache id for replace */ static int replaceid; /* Current cache id for replace */
@ -140,7 +147,7 @@ static double satcount_rec(int);
static double satcountln_rec(int); static double satcountln_rec(int);
static void varprofile_rec(int); static void varprofile_rec(int);
static double bdd_pathcount_rec(BDD); static double bdd_pathcount_rec(BDD);
static int varset2vartable(BDD); static int varset2vartable(BDD, int);
static int varset2svartable(BDD); static int varset2svartable(BDD);
@ -164,8 +171,10 @@ static int varset2svartable(BDD);
#define log1p(a) (log(1.0+a)) #define log1p(a) (log(1.0+a))
#define INVARSET(a) (quantvarset[a] == quantvarsetID) /* unsigned check */ /* unsigned check */
#define INSVARSET(a) (abs(quantvarset[a]) == quantvarsetID) /* signed check */ #define INVARSET(a) ((quantvarset[a] == quantvarsetID) ^ quantvarsetcomp)
/* signed check */
#define INSVARSET(a) (abs(quantvarset[a]) == quantvarsetID)
/************************************************************************* /*************************************************************************
Setup and shutdown Setup and shutdown
@ -1532,17 +1541,7 @@ static BDD simplify_rec(BDD f, BDD d)
/*=== QUANTIFICATION ===================================================*/ /*=== QUANTIFICATION ===================================================*/
/* static BDD quantify(BDD r, BDD var, int op, int comp, int id)
NAME {* bdd\_exist *}
SECTION {* operator *}
SHORT {* existential quantification of variables *}
PROTO {* BDD bdd_exist(BDD r, BDD var) *}
DESCR {* Removes all occurences in {\tt r} of variables in the set
{\tt var} by existential quantification. *}
ALSO {* bdd\_forall, bdd\_unique, bdd\_makeset *}
RETURN {* The quantified BDD. *}
*/
BDD bdd_exist(BDD r, BDD var)
{ {
BDD res; BDD res;
firstReorder = 1; firstReorder = 1;
@ -1550,18 +1549,18 @@ BDD bdd_exist(BDD r, BDD var)
CHECKa(r, bddfalse); CHECKa(r, bddfalse);
CHECKa(var, bddfalse); CHECKa(var, bddfalse);
if (var < 2) /* Empty set */ if (var < 2 && !comp) /* Empty set */
return r; return r;
again: again:
if (setjmp(bddexception) == 0) if (setjmp(bddexception) == 0)
{ {
if (varset2vartable(var) < 0) if (varset2vartable(var, comp) < 0)
return bddfalse; return bddfalse;
INITREF; INITREF;
quantid = (var << 3) | CACHEID_EXIST; /* FIXME: range */ quantid = (var << 4) | id; /* FIXME: range */
applyop = bddop_or; applyop = op;
if (!firstReorder) if (!firstReorder)
bdd_disable_reorder(); bdd_disable_reorder();
@ -1582,6 +1581,36 @@ BDD bdd_exist(BDD r, BDD var)
return res; return res;
} }
/*
NAME {* bdd\_exist *}
SECTION {* operator *}
SHORT {* existential quantification of variables *}
PROTO {* BDD bdd_exist(BDD r, BDD var) *}
DESCR {* Removes all occurences in {\tt r} of variables in the set
{\tt var} by existential quantification. *}
ALSO {* bdd\_existcomp, bdd\_forall, bdd\_forallcomp, bdd\_unique, bdd\_uniquecomp, bdd\_makeset *}
RETURN {* The quantified BDD. *}
*/
BDD bdd_exist(BDD r, BDD var)
{
return quantify(r, var, bddop_or, 0, CACHEID_EXIST);
}
/*
NAME {* bdd\_existcomp *}
SECTION {* operator *}
SHORT {* existential quantification of other variables *}
PROTO {* BDD bdd_existcomp(BDD r, BDD var) *}
DESCR {* Removes all occurences in {\tt r} of variables not in the set
{\tt var} by existential quantification. *}
ALSO {* bdd\_exist, bdd\_existcomp, bdd\_forall, bdd\_forallcomp, bdd\_unique, bdd\_uniquecomp, bdd\_makeset *}
RETURN {* The quantified BDD. *}
*/
BDD bdd_existcomp(BDD r, BDD var)
{
return quantify(r, var, bddop_or, 1, CACHEID_EXISTC);
}
/* /*
NAME {* bdd\_forall *} NAME {* bdd\_forall *}
@ -1590,47 +1619,27 @@ SHORT {* universal quantification of variables *}
PROTO {* BDD bdd_forall(BDD r, BDD var) *} PROTO {* BDD bdd_forall(BDD r, BDD var) *}
DESCR {* Removes all occurences in {\tt r} of variables in the set DESCR {* Removes all occurences in {\tt r} of variables in the set
{\tt var} by universal quantification. *} {\tt var} by universal quantification. *}
ALSO {* bdd\_exist, bdd\_unique, bdd\_makeset *} ALSO {* bdd\_exist, bdd\_existcomp, bdd\_forallcomp, bdd\_unique, bdd\_uniquecomp, bdd\_makeset *}
RETURN {* The quantified BDD. *} RETURN {* The quantified BDD. *}
*/ */
BDD bdd_forall(BDD r, BDD var) BDD bdd_forall(BDD r, BDD var)
{ {
BDD res; return quantify(r, var, bddop_and, 0, CACHEID_EXIST);
firstReorder = 1;
CHECKa(r, bddfalse);
CHECKa(var, bddfalse);
if (var < 2) /* Empty set */
return r;
again:
if (setjmp(bddexception) == 0)
{
if (varset2vartable(var) < 0)
return bddfalse;
INITREF;
quantid = (var << 3) | CACHEID_FORALL;
applyop = bddop_and;
if (!firstReorder)
bdd_disable_reorder();
res = quant_rec(r);
if (!firstReorder)
bdd_enable_reorder();
}
else
{
bdd_checkreorder();
if (firstReorder-- == 1)
goto again;
res = BDDZERO; /* avoid warning about res being uninitialized */
} }
checkresize(); /*
return res; NAME {* bdd\_forallcomp *}
SECTION {* operator *}
SHORT {* universal quantification of other variables *}
PROTO {* BDD bdd_forallcomp(BDD r, BDD var) *}
DESCR {* Removes all occurences in {\tt r} of variables in the set
{\tt var} by universal quantification. *}
ALSO {* bdd\_exist, bdd\_existcomp, bdd\_forall, bdd\_unique, bdd\_uniquecomp, bdd\_makeset *}
RETURN {* The quantified BDD. *}
*/
BDD bdd_forallcomp(BDD r, BDD var)
{
return quantify(r, var, bddop_and, 1, CACHEID_EXISTC);
} }
@ -1644,47 +1653,30 @@ DESCR {* Removes all occurences in {\tt r} of variables in the set
uses a XOR operator instead of an OR operator as in the uses a XOR operator instead of an OR operator as in the
existential quantification, and an AND operator as in the existential quantification, and an AND operator as in the
universal quantification. *} universal quantification. *}
ALSO {* bdd\_exist, bdd\_forall, bdd\_makeset *} ALSO {* bdd\_exist, bdd\_existcomp, bdd\_forall, bdd\_forallcomp, bdd\_unique, bdd\_uniquecomp, bdd\_makeset *}
RETURN {* The quantified BDD. *} RETURN {* The quantified BDD. *}
*/ */
BDD bdd_unique(BDD r, BDD var) BDD bdd_unique(BDD r, BDD var)
{ {
BDD res; return quantify(r, var, bddop_xor, 0, CACHEID_UNIQUE);
firstReorder = 1;
CHECKa(r, bddfalse);
CHECKa(var, bddfalse);
if (var < 2) /* Empty set */
return r;
again:
if (setjmp(bddexception) == 0)
{
if (varset2vartable(var) < 0)
return bddfalse;
INITREF;
quantid = (var << 3) | CACHEID_UNIQUE;
applyop = bddop_xor;
if (!firstReorder)
bdd_disable_reorder();
res = quant_rec(r);
if (!firstReorder)
bdd_enable_reorder();
}
else
{
bdd_checkreorder();
if (firstReorder-- == 1)
goto again;
res = BDDZERO; /* avoid warning about res being uninitialized */
} }
checkresize(); /*
return res; NAME {* bdd\_uniquecomp *}
SECTION {* operator *}
SHORT {* unique quantification of other variables *}
PROTO {* BDD bdd_uniquecomp(BDD r, BDD var) *}
DESCR {* Removes all occurences in {\tt r} of variables now in the set
{\tt var} by unique quantification. This type of quantification
uses a XOR operator instead of an OR operator as in the
existential quantification, and an AND operator as in the
universal quantification. *}
ALSO {* bdd\_exist, bdd\_existcomp, bdd\_forall, bdd\_forallcomp, bdd\_uniquecomp, bdd\_makeset *}
RETURN {* The quantified BDD. *}
*/
BDD bdd_uniquecomp(BDD r, BDD var)
{
return quantify(r, var, bddop_xor, 1, CACHEID_UNIQUEC);
} }
@ -1728,25 +1720,8 @@ static int quant_rec(int r)
/*=== APPLY & QUANTIFY =================================================*/ /*=== APPLY & QUANTIFY =================================================*/
/* static BDD appquantify(BDD l, BDD r, int opr, BDD var,
NAME {* bdd\_appex *} int qop, int comp, int qid)
SECTION {* operator *}
SHORT {* apply operation and existential quantification *}
PROTO {* BDD bdd_appex(BDD left, BDD right, int opr, BDD var) *}
DESCR {* Applies the binary operator {\tt opr} to the arguments
{\tt left} and {\tt right} and then performs an existential
quantification of the variables from the variable set
{\tt var}. This is done in a bottom up manner such that both the
apply and quantification is done on the lower nodes before
stepping up to the higher nodes. This makes the {\tt bdd\_appex}
function much more efficient than an apply operation followed
by a quantification. If the operator is a conjunction then this
is similar to the relational product of the two BDDs.
\index{relational product} *}
ALSO {* bdd\_appall, bdd\_appuni, bdd\_apply, bdd\_exist, bdd\_forall, bdd\_unique, bdd\_makeset *}
RETURN {* The result of the operation. *}
*/
BDD bdd_appex(BDD l, BDD r, int opr, BDD var)
{ {
BDD res; BDD res;
firstReorder = 1; firstReorder = 1;
@ -1761,20 +1736,20 @@ BDD bdd_appex(BDD l, BDD r, int opr, BDD var)
return bddfalse; return bddfalse;
} }
if (var < 2) /* Empty set */ if (var < 2 && !comp) /* Empty set */
return bdd_apply(l,r,opr); return bdd_apply(l,r,opr);
again: again:
if (setjmp(bddexception) == 0) if (setjmp(bddexception) == 0)
{ {
if (varset2vartable(var) < 0) if (varset2vartable(var, comp) < 0)
return bddfalse; return bddfalse;
INITREF; INITREF;
applyop = bddop_or; applyop = qop;
appexop = opr; appexop = opr;
appexid = (var << 5) | (appexop << 1); /* FIXME: range! */ appexid = (var << 5) | (appexop << 1); /* FIXME: range! */
quantid = (appexid << 3) | CACHEID_APPEX; quantid = (appexid << 4) | qid;
if (!firstReorder) if (!firstReorder)
bdd_disable_reorder(); bdd_disable_reorder();
@ -1795,6 +1770,51 @@ BDD bdd_appex(BDD l, BDD r, int opr, BDD var)
return res; return res;
} }
/*
NAME {* bdd\_appex *}
SECTION {* operator *}
SHORT {* apply operation and existential quantification *}
PROTO {* BDD bdd_appex(BDD left, BDD right, int opr, BDD var) *}
DESCR {* Applies the binary operator {\tt opr} to the arguments
{\tt left} and {\tt right} and then performs an existential
quantification of the variables from the variable set
{\tt var}. This is done in a bottom up manner such that both the
apply and quantification is done on the lower nodes before
stepping up to the higher nodes. This makes the {\tt bdd\_appex}
function much more efficient than an apply operation followed
by a quantification. If the operator is a conjunction then this
is similar to the relational product of the two BDDs.
\index{relational product} *}
ALSO {* bdd\_appexcomp, bdd\_appall, bdd\_appallcomp, bdd\_appuni, bdd\_appunicomp, bdd\_apply, bdd\_exist, bdd\_existcomp, bdd\_forall, bdd\_forallcomp, bdd\_unique, bdd\_uniquecomp, bdd\_makeset *}
RETURN {* The result of the operation. *}
*/
BDD bdd_appex(BDD l, BDD r, int opr, BDD var)
{
return appquantify(l, r, opr, var, bddop_or, 0, CACHEID_APPEX);
}
/*
NAME {* bdd\_appexcomp *}
SECTION {* operator *}
SHORT {* apply operation and (complemented) existential quantification *}
PROTO {* BDD bdd_appexcomp(BDD left, BDD right, int opr, BDD var) *}
DESCR {* Applies the binary operator {\tt opr} to the arguments
{\tt left} and {\tt right} and then performs an existential
quantification of the variables which are not in the variable set
{\tt var}. This is done in a bottom up manner such that both the
apply and quantification is done on the lower nodes before
stepping up to the higher nodes. This makes the {\tt bdd\_appexcomp}
function much more efficient than an apply operation followed
by a quantification. *}
ALSO {* bdd\_appex, bdd\_appall, bdd\_appallcomp, bdd\_appuni, bdd\_appunicomp, bdd\_apply, bdd\_exist, bdd\_existcomp, bdd\_forall, bdd\_forallcomp, bdd\_unique, bdd\_uniquecomp, bdd\_makeset *}
RETURN {* The result of the operation. *}
*/
BDD bdd_appexcomp(BDD l, BDD r, int opr, BDD var)
{
return appquantify(l, r, opr, var, bddop_or, 1, CACHEID_APPEXC);
}
/* /*
NAME {* bdd\_appall *} NAME {* bdd\_appall *}
@ -1809,56 +1829,34 @@ DESCR {* Applies the binary operator {\tt opr} to the arguments
stepping up to the higher nodes. This makes the {\tt bdd\_appall} stepping up to the higher nodes. This makes the {\tt bdd\_appall}
function much more efficient than an apply operation followed function much more efficient than an apply operation followed
by a quantification. *} by a quantification. *}
ALSO {* bdd\_appex, bdd\_appuni, bdd\_apply, bdd\_exist, bdd\_forall, bdd\_unique, bdd\_makeset *} ALSO {* bdd\_appex, bdd\_appexcomp, bdd\_appallcomp, bdd\_appuni, bdd\_appunicomp, bdd\_apply, bdd\_exist, bdd\_existcomp, bdd\_forall, bdd\_forallcomp, bdd\_unique, bdd\_uniquecomp, bdd\_makeset *}
RETURN {* The result of the operation. *} RETURN {* The result of the operation. *}
*/ */
BDD bdd_appall(BDD l, BDD r, int opr, BDD var) BDD bdd_appall(BDD l, BDD r, int opr, BDD var)
{ {
BDD res; return appquantify(l, r, opr, var, bddop_and, 0, CACHEID_APPAL);
firstReorder = 1;
CHECKa(l, bddfalse);
CHECKa(r, bddfalse);
CHECKa(var, bddfalse);
if (opr<0 || opr>bddop_invimp)
{
bdd_error(BDD_OP);
return bddfalse;
} }
if (var < 2) /* Empty set */
return bdd_apply(l,r,opr);
again: /*
if (setjmp(bddexception) == 0) NAME {* bdd\_appallcomp *}
SECTION {* operator *}
SHORT {* apply operation and (complemented) universal quantification *}
PROTO {* BDD bdd_appall(BDD left, BDD right, int opr, BDD var) *}
DESCR {* Applies the binary operator {\tt opr} to the arguments
{\tt left} and {\tt right} and then performs an universal
quantification of the variables which are not in the variable set
{\tt var}. This is done in a bottom up manner such that both the
apply and quantification is done on the lower nodes before
stepping up to the higher nodes. This makes the
{\tt bdd\_appallcomp} function much more efficient than an
apply operation followed by a quantification. *}
ALSO {* bdd\_appex, bdd\_appexcomp, bdd\_appall, bdd\_appuni, bdd\_appunicomp, bdd\_apply, bdd\_exist, bdd\_existcomp, bdd\_forall, bdd\_forallcomp, bdd\_unique, bdd\_uniquecomp, bdd\_makeset *}
RETURN {* The result of the operation. *}
*/
BDD bdd_appallcomp(BDD l, BDD r, int opr, BDD var)
{ {
if (varset2vartable(var) < 0) return appquantify(l, r, opr, var, bddop_and, 1, CACHEID_APPALC);
return bddfalse;
INITREF;
applyop = bddop_and;
appexop = opr;
appexid = (var << 5) | (appexop << 1) | 1; /* FIXME: range! */
quantid = (appexid << 3) | CACHEID_APPAL;
if (!firstReorder)
bdd_disable_reorder();
res = appquant_rec(l, r);
if (!firstReorder)
bdd_enable_reorder();
}
else
{
bdd_checkreorder();
if (firstReorder-- == 1)
goto again;
res = BDDZERO; /* avoid warning about res being uninitialized */
}
checkresize();
return res;
} }
@ -1875,56 +1873,34 @@ DESCR {* Applies the binary operator {\tt opr} to the arguments
stepping up to the higher nodes. This makes the {\tt bdd\_appuni} stepping up to the higher nodes. This makes the {\tt bdd\_appuni}
function much more efficient than an apply operation followed function much more efficient than an apply operation followed
by a quantification. *} by a quantification. *}
ALSO {* bdd\_appex, bdd\_appall, bdd\_apply, bdd\_exist, bdd\_unique, bdd\_forall, bdd\_makeset *} ALSO {* bdd\_appex, bdd\_appexcomp, bdd\_appall, bdd\_appallcomp, bdd\_appuni, bdd\_appunicomp, bdd\_apply, bdd\_exist, bdd\_existcomp, bdd\_forall, bdd\_forallcomp, bdd\_unique, bdd\_uniquecomp, bdd\_makeset *}
RETURN {* The result of the operation. *} RETURN {* The result of the operation. *}
*/ */
BDD bdd_appuni(BDD l, BDD r, int opr, BDD var) BDD bdd_appuni(BDD l, BDD r, int opr, BDD var)
{ {
BDD res; return appquantify(l, r, opr, var, bddop_xor, 0, CACHEID_APPUN);
firstReorder = 1;
CHECKa(l, bddfalse);
CHECKa(r, bddfalse);
CHECKa(var, bddfalse);
if (opr<0 || opr>bddop_invimp)
{
bdd_error(BDD_OP);
return bddfalse;
} }
if (var < 2) /* Empty set */
return bdd_apply(l,r,opr);
again: /*
if (setjmp(bddexception) == 0) NAME {* bdd\_appunicomp *}
SECTION {* operator *}
SHORT {* apply operation and unique (complemented) quantification *}
PROTO {* BDD bdd_appunicomp(BDD left, BDD right, int opr, BDD var) *}
DESCR {* Applies the binary operator {\tt opr} to the arguments
{\tt left} and {\tt right} and then performs a unique
quantification of the variables which are not in the variable set
{\tt var}. This is done in a bottom up manner such that both the
apply and quantification is done on the lower nodes before
stepping up to the higher nodes. This makes the
{\tt bdd\_appunicomp} function much more efficient than an
apply operation followed by a quantification. *}
ALSO {* bdd\_appex, bdd\_appexcomp, bdd\_appall, bdd\_appallcomp, bdd\_appuni, bdd\_apply, bdd\_exist, bdd\_existcomp, bdd\_forall, bdd\_forallcomp, bdd\_unique, bdd\_uniquecomp, bdd\_makeset *}
RETURN {* The result of the operation. *}
*/
BDD bdd_appunicomp(BDD l, BDD r, int opr, BDD var)
{ {
if (varset2vartable(var) < 0) return appquantify(l, r, opr, var, bddop_xor, 1, CACHEID_APPUNC);
return bddfalse;
INITREF;
applyop = bddop_xor;
appexop = opr;
appexid = (var << 5) | (appexop << 1) | 1; /* FIXME: range! */
quantid = (appexid << 3) | CACHEID_APPUN;
if (!firstReorder)
bdd_disable_reorder();
res = appquant_rec(l, r);
if (!firstReorder)
bdd_enable_reorder();
}
else
{
bdd_checkreorder();
if (firstReorder-- == 1)
goto again;
res = BDDZERO; /* avoid warning about res being uninitialized */
}
checkresize();
return res;
} }
@ -2062,8 +2038,9 @@ BDD bdd_support(BDD r)
CHECKa(r, bddfalse); CHECKa(r, bddfalse);
/* Variable sets are conjunctions, so the empty support is bddtrue. */
if (r < 2) if (r < 2)
return bddfalse; return bddtrue;
/* On-demand allocation of support set */ /* On-demand allocation of support set */
if (supportSize < bddvarnum) if (supportSize < bddvarnum)
@ -2770,14 +2747,15 @@ static double bdd_pathcount_rec(BDD r)
Other internal functions Other internal functions
*************************************************************************/ *************************************************************************/
static int varset2vartable(BDD r) static int varset2vartable(BDD r, int comp)
{ {
BDD n; BDD n;
if (r < 2) if (r < 2 && !comp)
return bdd_error(BDD_VARSET); return bdd_error(BDD_VARSET);
quantvarsetID++; quantvarsetID++;
quantvarsetcomp = comp;
if (quantvarsetID == INT_MAX) if (quantvarsetID == INT_MAX)
{ {
@ -2791,6 +2769,11 @@ static int varset2vartable(BDD r)
quantlast = LEVEL(n); quantlast = LEVEL(n);
} }
/* When the varset is complemented, make sure all variables will
be tested. */
if (comp)
quantlast = bddvarnum;
return 0; return 0;
} }