Context Navigation

source: vis_dev/glu-2.1/src/cuBdd/cuddAndAbs.c @ 8

Last change on this file since 8 was 8, checked in by cecile, 13 years ago
src glu
File size: 11.2 KB

Rev	Line
[8]	1	/CFile*********************************************************************
	2
	3	FileName [cuddAndAbs.c]
	4
	5	PackageName [cudd]
	6
	7	Synopsis [Combined AND and existential abstraction for BDDs]
	8
	9	Description [External procedures included in this module:
	10	<ul>
	11	<li> Cudd_bddAndAbstract()
	12	<li> Cudd_bddAndAbstractLimit()
	13	</ul>
	14	Internal procedures included in this module:
	15	<ul>
	16	<li> cuddBddAndAbstractRecur()
	17	</ul>]
	18
	19	Author [Fabio Somenzi]
	20
	21	Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
	22
	23	All rights reserved.
	24
	25	Redistribution and use in source and binary forms, with or without
	26	modification, are permitted provided that the following conditions
	27	are met:
	28
	29	Redistributions of source code must retain the above copyright
	30	notice, this list of conditions and the following disclaimer.
	31
	32	Redistributions in binary form must reproduce the above copyright
	33	notice, this list of conditions and the following disclaimer in the
	34	documentation and/or other materials provided with the distribution.
	35
	36	Neither the name of the University of Colorado nor the names of its
	37	contributors may be used to endorse or promote products derived from
	38	this software without specific prior written permission.
	39
	40	THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
	41	"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
	42	LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
	43	FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
	44	COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
	45	INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
	46	BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
	47	LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
	48	CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
	49	LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
	50	ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
	51	POSSIBILITY OF SUCH DAMAGE.]
	52
	53	******************************************************************************/
	54
	55	#include "util.h"
	56	#include "cuddInt.h"
	57
	58
	59	/---------------------------------------------------------------------------/
	60	/* Constant declarations */
	61	/---------------------------------------------------------------------------/
	62
	63
	64	/---------------------------------------------------------------------------/
	65	/* Stucture declarations */
	66	/---------------------------------------------------------------------------/
	67
	68
	69	/---------------------------------------------------------------------------/
	70	/* Type declarations */
	71	/---------------------------------------------------------------------------/
	72
	73
	74	/---------------------------------------------------------------------------/
	75	/* Variable declarations */
	76	/---------------------------------------------------------------------------/
	77
	78	#ifndef lint
	79	static char rcsid[] DD_UNUSED = "$Id: cuddAndAbs.c,v 1.19 2004/08/13 18:04:46 fabio Exp $";
	80	#endif
	81
	82
	83	/---------------------------------------------------------------------------/
	84	/* Macro declarations */
	85	/---------------------------------------------------------------------------/
	86
	87
	88	/AutomaticStart***********************************************************/
	89
	90	/---------------------------------------------------------------------------/
	91	/* Static function prototypes */
	92	/---------------------------------------------------------------------------/
	93
	94
	95	/AutomaticEnd*************************************************************/
	96
	97
	98	/---------------------------------------------------------------------------/
	99	/* Definition of exported functions */
	100	/---------------------------------------------------------------------------/
	101
	102
	103	/Function******************************************************************
	104
	105	Synopsis [Takes the AND of two BDDs and simultaneously abstracts the
	106	variables in cube.]
	107
	108	Description [Takes the AND of two BDDs and simultaneously abstracts
	109	the variables in cube. The variables are existentially abstracted.
	110	Returns a pointer to the result is successful; NULL otherwise.
	111	Cudd_bddAndAbstract implements the semiring matrix multiplication
	112	algorithm for the boolean semiring.]
	113
	114	SideEffects [None]
	115
	116	SeeAlso [Cudd_addMatrixMultiply Cudd_addTriangle Cudd_bddAnd]
	117
	118	******************************************************************************/
	119	DdNode *
	120	Cudd_bddAndAbstract(
	121	DdManager * manager,
	122	DdNode * f,
	123	DdNode * g,
	124	DdNode * cube)
	125	{
	126	DdNode *res;
	127
	128	do {
	129	manager->reordered = 0;
	130	res = cuddBddAndAbstractRecur(manager, f, g, cube);
	131	} while (manager->reordered == 1);
	132	return(res);
	133
	134	} /* end of Cudd_bddAndAbstract */
	135
	136
	137	/Function******************************************************************
	138
	139	Synopsis [Takes the AND of two BDDs and simultaneously abstracts the
	140	variables in cube. Returns NULL if too many nodes are required.]
	141
	142	Description [Takes the AND of two BDDs and simultaneously abstracts
	143	the variables in cube. The variables are existentially abstracted.
	144	Returns a pointer to the result is successful; NULL otherwise.
	145	In particular, if the number of new nodes created exceeds
	146	<code>limit</code>, this function returns NULL.]
	147
	148	SideEffects [None]
	149
	150	SeeAlso [Cudd_bddAndAbstract]
	151
	152	******************************************************************************/
	153	DdNode *
	154	Cudd_bddAndAbstractLimit(
	155	DdManager * manager,
	156	DdNode * f,
	157	DdNode * g,
	158	DdNode * cube,
	159	unsigned int limit)
	160	{
	161	DdNode *res;
	162	unsigned int saveLimit = manager->maxLive;
	163
	164	manager->maxLive = (manager->keys - manager->dead) +
	165	(manager->keysZ - manager->deadZ) + limit;
	166	do {
	167	manager->reordered = 0;
	168	res = cuddBddAndAbstractRecur(manager, f, g, cube);
	169	} while (manager->reordered == 1);
	170	manager->maxLive = saveLimit;
	171	return(res);
	172
	173	} /* end of Cudd_bddAndAbstractLimit */
	174
	175
	176	/---------------------------------------------------------------------------/
	177	/* Definition of internal functions */
	178	/---------------------------------------------------------------------------/
	179
	180
	181	/Function******************************************************************
	182
	183	Synopsis [Takes the AND of two BDDs and simultaneously abstracts the
	184	variables in cube.]
	185
	186	Description [Takes the AND of two BDDs and simultaneously abstracts
	187	the variables in cube. The variables are existentially abstracted.
	188	Returns a pointer to the result is successful; NULL otherwise.]
	189
	190	SideEffects [None]
	191
	192	SeeAlso [Cudd_bddAndAbstract]
	193
	194	******************************************************************************/
	195	DdNode *
	196	cuddBddAndAbstractRecur(
	197	DdManager * manager,
	198	DdNode * f,
	199	DdNode * g,
	200	DdNode * cube)
	201	{
	202	DdNode F, ft, fe, G, gt, ge;
	203	DdNode one, zero, r, t, *e;
	204	unsigned int topf, topg, topcube, top, index;
	205
	206	statLine(manager);
	207	one = DD_ONE(manager);
	208	zero = Cudd_Not(one);
	209
	210	/* Terminal cases. */
	211	if (f == zero \|\| g == zero \|\| f == Cudd_Not(g)) return(zero);
	212	if (f == one && g == one) return(one);
	213
	214	if (cube == one) {
	215	return(cuddBddAndRecur(manager, f, g));
	216	}
	217	if (f == one \|\| f == g) {
	218	return(cuddBddExistAbstractRecur(manager, g, cube));
	219	}
	220	if (g == one) {
	221	return(cuddBddExistAbstractRecur(manager, f, cube));
	222	}
	223	/* At this point f, g, and cube are not constant. */
	224
	225	if (f > g) { /* Try to increase cache efficiency. */
	226	DdNode *tmp = f;
	227	f = g;
	228	g = tmp;
	229	}
	230
	231	/* Here we can skip the use of cuddI, because the operands are known
	232	** to be non-constant.
	233	*/
	234	F = Cudd_Regular(f);
	235	G = Cudd_Regular(g);
	236	topf = manager->perm[F->index];
	237	topg = manager->perm[G->index];
	238	top = ddMin(topf, topg);
	239	topcube = manager->perm[cube->index];
	240
	241	while (topcube < top) {
	242	cube = cuddT(cube);
	243	if (cube == one) {
	244	return(cuddBddAndRecur(manager, f, g));
	245	}
	246	topcube = manager->perm[cube->index];
	247	}
	248	/* Now, topcube >= top. */
	249
	250	/* Check cache. */
	251	if (F->ref != 1 \|\| G->ref != 1) {
	252	r = cuddCacheLookup(manager, DD_BDD_AND_ABSTRACT_TAG, f, g, cube);
	253	if (r != NULL) {
	254	return(r);
	255	}
	256	}
	257
	258	if (topf == top) {
	259	index = F->index;
	260	ft = cuddT(F);
	261	fe = cuddE(F);
	262	if (Cudd_IsComplement(f)) {
	263	ft = Cudd_Not(ft);
	264	fe = Cudd_Not(fe);
	265	}
	266	} else {
	267	index = G->index;
	268	ft = fe = f;
	269	}
	270
	271	if (topg == top) {
	272	gt = cuddT(G);
	273	ge = cuddE(G);
	274	if (Cudd_IsComplement(g)) {
	275	gt = Cudd_Not(gt);
	276	ge = Cudd_Not(ge);
	277	}
	278	} else {
	279	gt = ge = g;
	280	}
	281
	282	if (topcube == top) { /* quantify */
	283	DdNode *Cube = cuddT(cube);
	284	t = cuddBddAndAbstractRecur(manager, ft, gt, Cube);
	285	if (t == NULL) return(NULL);
	286	/* Special case: 1 OR anything = 1. Hence, no need to compute
	287	** the else branch if t is 1. Likewise t + t * anything == t.
	288	** Notice that t == fe implies that fe does not depend on the
	289	** variables in Cube. Likewise for t == ge.
	290	*/
	291	if (t == one \|\| t == fe \|\| t == ge) {
	292	if (F->ref != 1 \|\| G->ref != 1)
	293	cuddCacheInsert(manager, DD_BDD_AND_ABSTRACT_TAG,
	294	f, g, cube, t);
	295	return(t);
	296	}
	297	cuddRef(t);
	298	/* Special case: t + !t * anything == t + anything. */
	299	if (t == Cudd_Not(fe)) {
	300	e = cuddBddExistAbstractRecur(manager, ge, Cube);
	301	} else if (t == Cudd_Not(ge)) {
	302	e = cuddBddExistAbstractRecur(manager, fe, Cube);
	303	} else {
	304	e = cuddBddAndAbstractRecur(manager, fe, ge, Cube);
	305	}
	306	if (e == NULL) {
	307	Cudd_IterDerefBdd(manager, t);
	308	return(NULL);
	309	}
	310	if (t == e) {
	311	r = t;
	312	cuddDeref(t);
	313	} else {
	314	cuddRef(e);
	315	r = cuddBddAndRecur(manager, Cudd_Not(t), Cudd_Not(e));
	316	if (r == NULL) {
	317	Cudd_IterDerefBdd(manager, t);
	318	Cudd_IterDerefBdd(manager, e);
	319	return(NULL);
	320	}
	321	r = Cudd_Not(r);
	322	cuddRef(r);
	323	Cudd_DelayedDerefBdd(manager, t);
	324	Cudd_DelayedDerefBdd(manager, e);
	325	cuddDeref(r);
	326	}
	327	} else {
	328	t = cuddBddAndAbstractRecur(manager, ft, gt, cube);
	329	if (t == NULL) return(NULL);
	330	cuddRef(t);
	331	e = cuddBddAndAbstractRecur(manager, fe, ge, cube);
	332	if (e == NULL) {
	333	Cudd_IterDerefBdd(manager, t);
	334	return(NULL);
	335	}
	336	if (t == e) {
	337	r = t;
	338	cuddDeref(t);
	339	} else {
	340	cuddRef(e);
	341	if (Cudd_IsComplement(t)) {
	342	r = cuddUniqueInter(manager, (int) index,
	343	Cudd_Not(t), Cudd_Not(e));
	344	if (r == NULL) {
	345	Cudd_IterDerefBdd(manager, t);
	346	Cudd_IterDerefBdd(manager, e);
	347	return(NULL);
	348	}
	349	r = Cudd_Not(r);
	350	} else {
	351	r = cuddUniqueInter(manager,(int)index,t,e);
	352	if (r == NULL) {
	353	Cudd_IterDerefBdd(manager, t);
	354	Cudd_IterDerefBdd(manager, e);
	355	return(NULL);
	356	}
	357	}
	358	cuddDeref(e);
	359	cuddDeref(t);
	360	}
	361	}
	362
	363	if (F->ref != 1 \|\| G->ref != 1)
	364	cuddCacheInsert(manager, DD_BDD_AND_ABSTRACT_TAG, f, g, cube, r);
	365	return (r);
	366
	367	} /* end of cuddBddAndAbstractRecur */
	368
	369
	370	/---------------------------------------------------------------------------/
	371	/* Definition of static functions */
	372	/---------------------------------------------------------------------------/
	373

Note: See TracBrowser for help on using the repository browser.

Download in other formats: