Context Navigation

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

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

Line
1	/CFile*********************************************************************
2
3	FileName [cuddApprox.c]
4
5	PackageName [cudd]
6
7	Synopsis [Procedures to approximate a given BDD.]
8
9	Description [External procedures provided by this module:
10	<ul>
11	<li> Cudd_UnderApprox()
12	<li> Cudd_OverApprox()
13	<li> Cudd_RemapUnderApprox()
14	<li> Cudd_RemapOverApprox()
15	<li> Cudd_BiasedUnderApprox()
16	<li> Cudd_BiasedOverApprox()
17	</ul>
18	Internal procedures included in this module:
19	<ul>
20	<li> cuddUnderApprox()
21	<li> cuddRemapUnderApprox()
22	<li> cuddBiasedUnderApprox()
23	</ul>
24	Static procedures included in this module:
25	<ul>
26	<li> gatherInfoAux()
27	<li> gatherInfo()
28	<li> computeSavings()
29	<li> UAmarkNodes()
30	<li> UAbuildSubset()
31	<li> updateRefs()
32	<li> RAmarkNodes()
33	<li> BAmarkNodes()
34	<li> RAbuildSubset()
35	</ul>
36	]
37
38	SeeAlso [cuddSubsetHB.c cuddSubsetSP.c cuddGenCof.c]
39
40	Author [Fabio Somenzi]
41
42	Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
43
44	All rights reserved.
45
46	Redistribution and use in source and binary forms, with or without
47	modification, are permitted provided that the following conditions
48	are met:
49
50	Redistributions of source code must retain the above copyright
51	notice, this list of conditions and the following disclaimer.
52
53	Redistributions in binary form must reproduce the above copyright
54	notice, this list of conditions and the following disclaimer in the
55	documentation and/or other materials provided with the distribution.
56
57	Neither the name of the University of Colorado nor the names of its
58	contributors may be used to endorse or promote products derived from
59	this software without specific prior written permission.
60
61	THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
62	"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
63	LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
64	FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
65	COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
66	INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
67	BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
68	LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
69	CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
70	LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
71	ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
72	POSSIBILITY OF SUCH DAMAGE.]
73
74	******************************************************************************/
75
76	#ifdef __STDC__
77	#include <float.h>
78	#else
79	#define DBL_MAX_EXP 1024
80	#endif
81	#include "util.h"
82	#include "cuddInt.h"
83
84	/---------------------------------------------------------------------------/
85	/* Constant declarations */
86	/---------------------------------------------------------------------------/
87
88	#define NOTHING 0
89	#define REPLACE_T 1
90	#define REPLACE_E 2
91	#define REPLACE_N 3
92	#define REPLACE_TT 4
93	#define REPLACE_TE 5
94
95	#define DONT_CARE 0
96	#define CARE 1
97	#define TOTAL_CARE 2
98	#define CARE_ERROR 3
99
100	/---------------------------------------------------------------------------/
101	/* Stucture declarations */
102	/---------------------------------------------------------------------------/
103
104	/---------------------------------------------------------------------------/
105	/* Type declarations */
106	/---------------------------------------------------------------------------/
107
108	/* Data structure to store the information on each node. It keeps the
109	** number of minterms of the function rooted at this node in terms of
110	** the number of variables specified by the user; the number of
111	** minterms of the complement; the impact of the number of minterms of
112	** this function on the number of minterms of the root function; the
113	** reference count of the node from within the root function; the
114	** reference count of the node from an internal node; and the flag
115	** that says whether the node should be replaced and how. */
116	typedef struct NodeData {
117	double mintermsP; /* minterms for the regular node */
118	double mintermsN; /* minterms for the complemented node */
119	int functionRef; /* references from within this function */
120	char care; /* node intersects care set */
121	char replace; /* replacement decision */
122	short int parity; /* 1: even; 2: odd; 3: both */
123	DdNode resultP; / result for even parity */
124	DdNode resultN; / result for odd parity */
125	} NodeData;
126
127	typedef struct ApproxInfo {
128	DdNode one; / one constant */
129	DdNode zero; / BDD zero constant */
130	NodeData page; / per-node information */
131	st_table table; / hash table to access the per-node info */
132	int index; /* index of the current node */
133	double max; /* max number of minterms */
134	int size; /* how many nodes are left */
135	double minterms; /* how many minterms are left */
136	} ApproxInfo;
137
138	/* Item of the queue used in the levelized traversal of the BDD. */
139	#ifdef __osf__
140	#pragma pointer_size save
141	#pragma pointer_size short
142	#endif
143	typedef struct GlobalQueueItem {
144	struct GlobalQueueItem *next;
145	struct GlobalQueueItem *cnext;
146	DdNode *node;
147	double impactP;
148	double impactN;
149	} GlobalQueueItem;
150
151	typedef struct LocalQueueItem {
152	struct LocalQueueItem *next;
153	struct LocalQueueItem *cnext;
154	DdNode *node;
155	int localRef;
156	} LocalQueueItem;
157	#ifdef __osf__
158	#pragma pointer_size restore
159	#endif
160
161
162	/---------------------------------------------------------------------------/
163	/* Variable declarations */
164	/---------------------------------------------------------------------------/
165
166	#ifndef lint
167	static char rcsid[] DD_UNUSED = "$Id: cuddApprox.c,v 1.25 2004/08/13 18:04:46 fabio Exp $";
168	#endif
169
170	/---------------------------------------------------------------------------/
171	/* Macro declarations */
172	/---------------------------------------------------------------------------/
173
174	/AutomaticStart***********************************************************/
175
176	/---------------------------------------------------------------------------/
177	/* Static function prototypes */
178	/---------------------------------------------------------------------------/
179
180	static void updateParity (DdNode node, ApproxInfo info, int newparity);
181	static NodeData * gatherInfoAux (DdNode node, ApproxInfo info, int parity);
182	static ApproxInfo * gatherInfo (DdManager dd, DdNode node, int numVars, int parity);
183	static int computeSavings (DdManager dd, DdNode f, DdNode skip, ApproxInfo info, DdLevelQueue *queue);
184	static int updateRefs (DdManager dd, DdNode f, DdNode skip, ApproxInfo info, DdLevelQueue *queue);
185	static int UAmarkNodes (DdManager dd, DdNode f, ApproxInfo *info, int threshold, int safe, double quality);
186	static DdNode * UAbuildSubset (DdManager dd, DdNode node, ApproxInfo *info);
187	static int RAmarkNodes (DdManager dd, DdNode f, ApproxInfo *info, int threshold, double quality);
188	static int BAmarkNodes (DdManager dd, DdNode f, ApproxInfo *info, int threshold, double quality1, double quality0);
189	static DdNode * RAbuildSubset (DdManager dd, DdNode node, ApproxInfo *info);
190	static int BAapplyBias (DdManager dd, DdNode f, DdNode b, ApproxInfo info, DdHashTable *cache);
191
192	/AutomaticEnd*************************************************************/
193
194
195	/---------------------------------------------------------------------------/
196	/* Definition of exported functions */
197	/---------------------------------------------------------------------------/
198
199	/Function******************************************************************
200
201	Synopsis [Extracts a dense subset from a BDD with Shiple's
202	underapproximation method.]
203
204	Description [Extracts a dense subset from a BDD. This procedure uses
205	a variant of Tom Shiple's underapproximation method. The main
206	difference from the original method is that density is used as cost
207	function. Returns a pointer to the BDD of the subset if
208	successful. NULL if the procedure runs out of memory. The parameter
209	numVars is the maximum number of variables to be used in minterm
210	calculation. The optimal number should be as close as possible to
211	the size of the support of f. However, it is safe to pass the value
212	returned by Cudd_ReadSize for numVars when the number of variables
213	is under 1023. If numVars is larger than 1023, it will cause
214	overflow. If a 0 parameter is passed then the procedure will compute
215	a value which will avoid overflow but will cause underflow with 2046
216	variables or more.]
217
218	SideEffects [None]
219
220	SeeAlso [Cudd_SubsetShortPaths Cudd_SubsetHeavyBranch Cudd_ReadSize]
221
222	******************************************************************************/
223	DdNode *
224	Cudd_UnderApprox(
225	DdManager * dd /* manager */,
226	DdNode * f /* function to be subset */,
227	int numVars /* number of variables in the support of f */,
228	int threshold /* when to stop approximation */,
229	int safe /* enforce safe approximation */,
230	double quality /* minimum improvement for accepted changes */)
231	{
232	DdNode *subset;
233
234	do {
235	dd->reordered = 0;
236	subset = cuddUnderApprox(dd, f, numVars, threshold, safe, quality);
237	} while (dd->reordered == 1);
238
239	return(subset);
240
241	} /* end of Cudd_UnderApprox */
242
243
244	/Function******************************************************************
245
246	Synopsis [Extracts a dense superset from a BDD with Shiple's
247	underapproximation method.]
248
249	Description [Extracts a dense superset from a BDD. The procedure is
250	identical to the underapproximation procedure except for the fact that it
251	works on the complement of the given function. Extracting the subset
252	of the complement function is equivalent to extracting the superset
253	of the function.
254	Returns a pointer to the BDD of the superset if successful. NULL if
255	intermediate result causes the procedure to run out of memory. The
256	parameter numVars is the maximum number of variables to be used in
257	minterm calculation. The optimal number
258	should be as close as possible to the size of the support of f.
259	However, it is safe to pass the value returned by Cudd_ReadSize for
260	numVars when the number of variables is under 1023. If numVars is
261	larger than 1023, it will overflow. If a 0 parameter is passed then
262	the procedure will compute a value which will avoid overflow but
263	will cause underflow with 2046 variables or more.]
264
265	SideEffects [None]
266
267	SeeAlso [Cudd_SupersetHeavyBranch Cudd_SupersetShortPaths Cudd_ReadSize]
268
269	******************************************************************************/
270	DdNode *
271	Cudd_OverApprox(
272	DdManager * dd /* manager */,
273	DdNode * f /* function to be superset */,
274	int numVars /* number of variables in the support of f */,
275	int threshold /* when to stop approximation */,
276	int safe /* enforce safe approximation */,
277	double quality /* minimum improvement for accepted changes */)
278	{
279	DdNode subset, g;
280
281	g = Cudd_Not(f);
282	do {
283	dd->reordered = 0;
284	subset = cuddUnderApprox(dd, g, numVars, threshold, safe, quality);
285	} while (dd->reordered == 1);
286
287	return(Cudd_NotCond(subset, (subset != NULL)));
288
289	} /* end of Cudd_OverApprox */
290
291
292	/Function******************************************************************
293
294	Synopsis [Extracts a dense subset from a BDD with the remapping
295	underapproximation method.]
296
297	Description [Extracts a dense subset from a BDD. This procedure uses
298	a remapping technique and density as the cost function.
299	Returns a pointer to the BDD of the subset if
300	successful. NULL if the procedure runs out of memory. The parameter
301	numVars is the maximum number of variables to be used in minterm
302	calculation. The optimal number should be as close as possible to
303	the size of the support of f. However, it is safe to pass the value
304	returned by Cudd_ReadSize for numVars when the number of variables
305	is under 1023. If numVars is larger than 1023, it will cause
306	overflow. If a 0 parameter is passed then the procedure will compute
307	a value which will avoid overflow but will cause underflow with 2046
308	variables or more.]
309
310	SideEffects [None]
311
312	SeeAlso [Cudd_SubsetShortPaths Cudd_SubsetHeavyBranch Cudd_UnderApprox Cudd_ReadSize]
313
314	******************************************************************************/
315	DdNode *
316	Cudd_RemapUnderApprox(
317	DdManager * dd /* manager */,
318	DdNode * f /* function to be subset */,
319	int numVars /* number of variables in the support of f */,
320	int threshold /* when to stop approximation */,
321	double quality /* minimum improvement for accepted changes */)
322	{
323	DdNode *subset;
324
325	do {
326	dd->reordered = 0;
327	subset = cuddRemapUnderApprox(dd, f, numVars, threshold, quality);
328	} while (dd->reordered == 1);
329
330	return(subset);
331
332	} /* end of Cudd_RemapUnderApprox */
333
334
335	/Function******************************************************************
336
337	Synopsis [Extracts a dense superset from a BDD with the remapping
338	underapproximation method.]
339
340	Description [Extracts a dense superset from a BDD. The procedure is
341	identical to the underapproximation procedure except for the fact that it
342	works on the complement of the given function. Extracting the subset
343	of the complement function is equivalent to extracting the superset
344	of the function.
345	Returns a pointer to the BDD of the superset if successful. NULL if
346	intermediate result causes the procedure to run out of memory. The
347	parameter numVars is the maximum number of variables to be used in
348	minterm calculation. The optimal number
349	should be as close as possible to the size of the support of f.
350	However, it is safe to pass the value returned by Cudd_ReadSize for
351	numVars when the number of variables is under 1023. If numVars is
352	larger than 1023, it will overflow. If a 0 parameter is passed then
353	the procedure will compute a value which will avoid overflow but
354	will cause underflow with 2046 variables or more.]
355
356	SideEffects [None]
357
358	SeeAlso [Cudd_SupersetHeavyBranch Cudd_SupersetShortPaths Cudd_ReadSize]
359
360	******************************************************************************/
361	DdNode *
362	Cudd_RemapOverApprox(
363	DdManager * dd /* manager */,
364	DdNode * f /* function to be superset */,
365	int numVars /* number of variables in the support of f */,
366	int threshold /* when to stop approximation */,
367	double quality /* minimum improvement for accepted changes */)
368	{
369	DdNode subset, g;
370
371	g = Cudd_Not(f);
372	do {
373	dd->reordered = 0;
374	subset = cuddRemapUnderApprox(dd, g, numVars, threshold, quality);
375	} while (dd->reordered == 1);
376
377	return(Cudd_NotCond(subset, (subset != NULL)));
378
379	} /* end of Cudd_RemapOverApprox */
380
381
382	/Function******************************************************************
383
384	Synopsis [Extracts a dense subset from a BDD with the biased
385	underapproximation method.]
386
387	Description [Extracts a dense subset from a BDD. This procedure uses
388	a biased remapping technique and density as the cost function. The bias
389	is a function. This procedure tries to approximate where the bias is 0
390	and preserve the given function where the bias is 1.
391	Returns a pointer to the BDD of the subset if
392	successful. NULL if the procedure runs out of memory. The parameter
393	numVars is the maximum number of variables to be used in minterm
394	calculation. The optimal number should be as close as possible to
395	the size of the support of f. However, it is safe to pass the value
396	returned by Cudd_ReadSize for numVars when the number of variables
397	is under 1023. If numVars is larger than 1023, it will cause
398	overflow. If a 0 parameter is passed then the procedure will compute
399	a value which will avoid overflow but will cause underflow with 2046
400	variables or more.]
401
402	SideEffects [None]
403
404	SeeAlso [Cudd_SubsetShortPaths Cudd_SubsetHeavyBranch Cudd_UnderApprox
405	Cudd_RemapUnderApprox Cudd_ReadSize]
406
407	******************************************************************************/
408	DdNode *
409	Cudd_BiasedUnderApprox(
410	DdManager dd / manager */,
411	DdNode f / function to be subset */,
412	DdNode b / bias function */,
413	int numVars /* number of variables in the support of f */,
414	int threshold /* when to stop approximation */,
415	double quality1 /* minimum improvement for accepted changes when b=1 */,
416	double quality0 /* minimum improvement for accepted changes when b=0 */)
417	{
418	DdNode *subset;
419
420	do {
421	dd->reordered = 0;
422	subset = cuddBiasedUnderApprox(dd, f, b, numVars, threshold, quality1,
423	quality0);
424	} while (dd->reordered == 1);
425
426	return(subset);
427
428	} /* end of Cudd_BiasedUnderApprox */
429
430
431	/Function******************************************************************
432
433	Synopsis [Extracts a dense superset from a BDD with the biased
434	underapproximation method.]
435
436	Description [Extracts a dense superset from a BDD. The procedure is
437	identical to the underapproximation procedure except for the fact that it
438	works on the complement of the given function. Extracting the subset
439	of the complement function is equivalent to extracting the superset
440	of the function.
441	Returns a pointer to the BDD of the superset if successful. NULL if
442	intermediate result causes the procedure to run out of memory. The
443	parameter numVars is the maximum number of variables to be used in
444	minterm calculation. The optimal number
445	should be as close as possible to the size of the support of f.
446	However, it is safe to pass the value returned by Cudd_ReadSize for
447	numVars when the number of variables is under 1023. If numVars is
448	larger than 1023, it will overflow. If a 0 parameter is passed then
449	the procedure will compute a value which will avoid overflow but
450	will cause underflow with 2046 variables or more.]
451
452	SideEffects [None]
453
454	SeeAlso [Cudd_SupersetHeavyBranch Cudd_SupersetShortPaths
455	Cudd_RemapOverApprox Cudd_BiasedUnderApprox Cudd_ReadSize]
456
457	******************************************************************************/
458	DdNode *
459	Cudd_BiasedOverApprox(
460	DdManager dd / manager */,
461	DdNode f / function to be superset */,
462	DdNode b / bias function */,
463	int numVars /* number of variables in the support of f */,
464	int threshold /* when to stop approximation */,
465	double quality1 /* minimum improvement for accepted changes when b=1*/,
466	double quality0 /* minimum improvement for accepted changes when b=0 */)
467	{
468	DdNode subset, g;
469
470	g = Cudd_Not(f);
471	do {
472	dd->reordered = 0;
473	subset = cuddBiasedUnderApprox(dd, g, b, numVars, threshold, quality1,
474	quality0);
475	} while (dd->reordered == 1);
476
477	return(Cudd_NotCond(subset, (subset != NULL)));
478
479	} /* end of Cudd_BiasedOverApprox */
480
481
482	/---------------------------------------------------------------------------/
483	/* Definition of internal functions */
484	/---------------------------------------------------------------------------/
485
486
487	/Function******************************************************************
488
489	Synopsis [Applies Tom Shiple's underappoximation algorithm.]
490
491	Description [Applies Tom Shiple's underappoximation algorithm. Proceeds
492	in three phases:
493	<ul>
494	<li> collect information on each node in the BDD; this is done via DFS.
495	<li> traverse the BDD in top-down fashion and compute for each node
496	whether its elimination increases density.
497	<li> traverse the BDD via DFS and actually perform the elimination.
498	</ul>
499	Returns the approximated BDD if successful; NULL otherwise.]
500
501	SideEffects [None]
502
503	SeeAlso [Cudd_UnderApprox]
504
505	******************************************************************************/
506	DdNode *
507	cuddUnderApprox(
508	DdManager * dd /* DD manager */,
509	DdNode * f /* current DD */,
510	int numVars /* maximum number of variables */,
511	int threshold /* threshold under which approximation stops */,
512	int safe /* enforce safe approximation */,
513	double quality /* minimum improvement for accepted changes */)
514	{
515	ApproxInfo *info;
516	DdNode *subset;
517	int result;
518
519	if (f == NULL) {
520	fprintf(dd->err, "Cannot subset, nil object\n");
521	return(NULL);
522	}
523
524	if (Cudd_IsConstant(f)) {
525	return(f);
526	}
527
528	/* Create table where node data are accessible via a hash table. */
529	info = gatherInfo(dd, f, numVars, safe);
530	if (info == NULL) {
531	(void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
532	dd->errorCode = CUDD_MEMORY_OUT;
533	return(NULL);
534	}
535
536	/* Mark nodes that should be replaced by zero. */
537	result = UAmarkNodes(dd, f, info, threshold, safe, quality);
538	if (result == 0) {
539	(void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
540	FREE(info->page);
541	st_free_table(info->table);
542	FREE(info);
543	dd->errorCode = CUDD_MEMORY_OUT;
544	return(NULL);
545	}
546
547	/* Build the result. */
548	subset = UAbuildSubset(dd, f, info);
549	#if 1
550	if (subset && info->size < Cudd_DagSize(subset))
551	(void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n",
552	info->size, Cudd_DagSize(subset));
553	#endif
554	FREE(info->page);
555	st_free_table(info->table);
556	FREE(info);
557
558	#ifdef DD_DEBUG
559	if (subset != NULL) {
560	cuddRef(subset);
561	#if 0
562	(void) Cudd_DebugCheck(dd);
563	(void) Cudd_CheckKeys(dd);
564	#endif
565	if (!Cudd_bddLeq(dd, subset, f)) {
566	(void) fprintf(dd->err, "Wrong subset\n");
567	dd->errorCode = CUDD_INTERNAL_ERROR;
568	}
569	cuddDeref(subset);
570	}
571	#endif
572	return(subset);
573
574	} /* end of cuddUnderApprox */
575
576
577	/Function******************************************************************
578
579	Synopsis [Applies the remapping underappoximation algorithm.]
580
581	Description [Applies the remapping underappoximation algorithm.
582	Proceeds in three phases:
583	<ul>
584	<li> collect information on each node in the BDD; this is done via DFS.
585	<li> traverse the BDD in top-down fashion and compute for each node
586	whether remapping increases density.
587	<li> traverse the BDD via DFS and actually perform the elimination.
588	</ul>
589	Returns the approximated BDD if successful; NULL otherwise.]
590
591	SideEffects [None]
592
593	SeeAlso [Cudd_RemapUnderApprox]
594
595	******************************************************************************/
596	DdNode *
597	cuddRemapUnderApprox(
598	DdManager * dd /* DD manager */,
599	DdNode * f /* current DD */,
600	int numVars /* maximum number of variables */,
601	int threshold /* threshold under which approximation stops */,
602	double quality /* minimum improvement for accepted changes */)
603	{
604	ApproxInfo *info;
605	DdNode *subset;
606	int result;
607
608	if (f == NULL) {
609	fprintf(dd->err, "Cannot subset, nil object\n");
610	dd->errorCode = CUDD_INVALID_ARG;
611	return(NULL);
612	}
613
614	if (Cudd_IsConstant(f)) {
615	return(f);
616	}
617
618	/* Create table where node data are accessible via a hash table. */
619	info = gatherInfo(dd, f, numVars, TRUE);
620	if (info == NULL) {
621	(void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
622	dd->errorCode = CUDD_MEMORY_OUT;
623	return(NULL);
624	}
625
626	/* Mark nodes that should be replaced by zero. */
627	result = RAmarkNodes(dd, f, info, threshold, quality);
628	if (result == 0) {
629	(void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
630	FREE(info->page);
631	st_free_table(info->table);
632	FREE(info);
633	dd->errorCode = CUDD_MEMORY_OUT;
634	return(NULL);
635	}
636
637	/* Build the result. */
638	subset = RAbuildSubset(dd, f, info);
639	#if 1
640	if (subset && info->size < Cudd_DagSize(subset))
641	(void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n",
642	info->size, Cudd_DagSize(subset));
643	#endif
644	FREE(info->page);
645	st_free_table(info->table);
646	FREE(info);
647
648	#ifdef DD_DEBUG
649	if (subset != NULL) {
650	cuddRef(subset);
651	#if 0
652	(void) Cudd_DebugCheck(dd);
653	(void) Cudd_CheckKeys(dd);
654	#endif
655	if (!Cudd_bddLeq(dd, subset, f)) {
656	(void) fprintf(dd->err, "Wrong subset\n");
657	}
658	cuddDeref(subset);
659	dd->errorCode = CUDD_INTERNAL_ERROR;
660	}
661	#endif
662	return(subset);
663
664	} /* end of cuddRemapUnderApprox */
665
666
667	/Function******************************************************************
668
669	Synopsis [Applies the biased remapping underappoximation algorithm.]
670
671	Description [Applies the biased remapping underappoximation algorithm.
672	Proceeds in three phases:
673	<ul>
674	<li> collect information on each node in the BDD; this is done via DFS.
675	<li> traverse the BDD in top-down fashion and compute for each node
676	whether remapping increases density.
677	<li> traverse the BDD via DFS and actually perform the elimination.
678	</ul>
679	Returns the approximated BDD if successful; NULL otherwise.]
680
681	SideEffects [None]
682
683	SeeAlso [Cudd_BiasedUnderApprox]
684
685	******************************************************************************/
686	DdNode *
687	cuddBiasedUnderApprox(
688	DdManager dd / DD manager */,
689	DdNode f / current DD */,
690	DdNode b / bias function */,
691	int numVars /* maximum number of variables */,
692	int threshold /* threshold under which approximation stops */,
693	double quality1 /* minimum improvement for accepted changes when b=1 */,
694	double quality0 /* minimum improvement for accepted changes when b=0 */)
695	{
696	ApproxInfo *info;
697	DdNode *subset;
698	int result;
699	DdHashTable *cache;
700
701	if (f == NULL) {
702	fprintf(dd->err, "Cannot subset, nil object\n");
703	dd->errorCode = CUDD_INVALID_ARG;
704	return(NULL);
705	}
706
707	if (Cudd_IsConstant(f)) {
708	return(f);
709	}
710
711	/* Create table where node data are accessible via a hash table. */
712	info = gatherInfo(dd, f, numVars, TRUE);
713	if (info == NULL) {
714	(void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
715	dd->errorCode = CUDD_MEMORY_OUT;
716	return(NULL);
717	}
718
719	cache = cuddHashTableInit(dd,2,2);
720	result = BAapplyBias(dd, Cudd_Regular(f), b, info, cache);
721	if (result == CARE_ERROR) {
722	(void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
723	cuddHashTableQuit(cache);
724	FREE(info->page);
725	st_free_table(info->table);
726	FREE(info);
727	dd->errorCode = CUDD_MEMORY_OUT;
728	return(NULL);
729	}
730	cuddHashTableQuit(cache);
731
732	/* Mark nodes that should be replaced by zero. */
733	result = BAmarkNodes(dd, f, info, threshold, quality1, quality0);
734	if (result == 0) {
735	(void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
736	FREE(info->page);
737	st_free_table(info->table);
738	FREE(info);
739	dd->errorCode = CUDD_MEMORY_OUT;
740	return(NULL);
741	}
742
743	/* Build the result. */
744	subset = RAbuildSubset(dd, f, info);
745	#if 1
746	if (subset && info->size < Cudd_DagSize(subset))
747	(void) fprintf(dd->err, "Wrong prediction: %d versus actual %d\n",
748	info->size, Cudd_DagSize(subset));
749	#endif
750	FREE(info->page);
751	st_free_table(info->table);
752	FREE(info);
753
754	#ifdef DD_DEBUG
755	if (subset != NULL) {
756	cuddRef(subset);
757	#if 0
758	(void) Cudd_DebugCheck(dd);
759	(void) Cudd_CheckKeys(dd);
760	#endif
761	if (!Cudd_bddLeq(dd, subset, f)) {
762	(void) fprintf(dd->err, "Wrong subset\n");
763	}
764	cuddDeref(subset);
765	dd->errorCode = CUDD_INTERNAL_ERROR;
766	}
767	#endif
768	return(subset);
769
770	} /* end of cuddBiasedUnderApprox */
771
772
773	/---------------------------------------------------------------------------/
774	/* Definition of static functions */
775	/---------------------------------------------------------------------------/
776
777
778	/Function******************************************************************
779
780	Synopsis [Recursively update the parity of the paths reaching a node.]
781
782	Description [Recursively update the parity of the paths reaching a node.
783	Assumes that node is regular and propagates the invariant.]
784
785	SideEffects [None]
786
787	SeeAlso [gatherInfoAux]
788
789	******************************************************************************/
790	static void
791	updateParity(
792	DdNode * node /* function to analyze */,
793	ApproxInfo * info /* info on BDD */,
794	int newparity /* new parity for node */)
795	{
796	NodeData *infoN;
797	DdNode *E;
798
799	if (!st_lookup(info->table, node, &infoN)) return;
800	if ((infoN->parity & newparity) != 0) return;
801	infoN->parity \|= newparity;
802	if (Cudd_IsConstant(node)) return;
803	updateParity(cuddT(node),info,newparity);
804	E = cuddE(node);
805	if (Cudd_IsComplement(E)) {
806	updateParity(Cudd_Not(E),info,3-newparity);
807	} else {
808	updateParity(E,info,newparity);
809	}
810	return;
811
812	} /* end of updateParity */
813
814
815	/Function******************************************************************
816
817	Synopsis [Recursively counts minterms and computes reference counts
818	of each node in the BDD.]
819
820	Description [Recursively counts minterms and computes reference
821	counts of each node in the BDD. Similar to the cuddCountMintermAux
822	which recursively counts the number of minterms for the dag rooted
823	at each node in terms of the total number of variables (max). It assumes
824	that the node pointer passed to it is regular and it maintains the
825	invariant.]
826
827	SideEffects [None]
828
829	SeeAlso [gatherInfo]
830
831	******************************************************************************/
832	static NodeData *
833	gatherInfoAux(
834	DdNode * node /* function to analyze */,
835	ApproxInfo * info /* info on BDD */,
836	int parity /* gather parity information */)
837	{
838	DdNode N, Nt, *Ne;
839	NodeData infoN, infoT, *infoE;
840
841	N = Cudd_Regular(node);
842
843	/* Check whether entry for this node exists. */
844	if (st_lookup(info->table, N, &infoN)) {
845	if (parity) {
846	/* Update parity and propagate. */
847	updateParity(N, info, 1 + (int) Cudd_IsComplement(node));
848	}
849	return(infoN);
850	}
851
852	/* Compute the cofactors. */
853	Nt = Cudd_NotCond(cuddT(N), N != node);
854	Ne = Cudd_NotCond(cuddE(N), N != node);
855
856	infoT = gatherInfoAux(Nt, info, parity);
857	if (infoT == NULL) return(NULL);
858	infoE = gatherInfoAux(Ne, info, parity);
859	if (infoE == NULL) return(NULL);
860
861	infoT->functionRef++;
862	infoE->functionRef++;
863
864	/* Point to the correct location in the page. */
865	infoN = &(info->page[info->index++]);
866	infoN->parity \|= 1 + (short) Cudd_IsComplement(node);
867
868	infoN->mintermsP = infoT->mintermsP/2;
869	infoN->mintermsN = infoT->mintermsN/2;
870	if (Cudd_IsComplement(Ne) ^ Cudd_IsComplement(node)) {
871	infoN->mintermsP += infoE->mintermsN/2;
872	infoN->mintermsN += infoE->mintermsP/2;
873	} else {
874	infoN->mintermsP += infoE->mintermsP/2;
875	infoN->mintermsN += infoE->mintermsN/2;
876	}
877
878	/* Insert entry for the node in the table. */
879	if (st_insert(info->table,(char )N, (char )infoN) == ST_OUT_OF_MEM) {
880	return(NULL);
881	}
882	return(infoN);
883
884	} /* end of gatherInfoAux */
885
886
887	/Function******************************************************************
888
889	Synopsis [Gathers information about each node.]
890
891	Description [Counts minterms and computes reference counts of each
892	node in the BDD . The minterm count is separately computed for the
893	node and its complement. This is to avoid cancellation
894	errors. Returns a pointer to the data structure holding the
895	information gathered if successful; NULL otherwise.]
896
897	SideEffects [None]
898
899	SeeAlso [cuddUnderApprox gatherInfoAux]
900
901	******************************************************************************/
902	static ApproxInfo *
903	gatherInfo(
904	DdManager * dd /* manager */,
905	DdNode * node /* function to be analyzed */,
906	int numVars /* number of variables node depends on */,
907	int parity /* gather parity information */)
908	{
909	ApproxInfo *info;
910	NodeData *infoTop;
911
912	/* If user did not give numVars value, set it to the maximum
913	** exponent that the pow function can take. The -1 is due to the
914	** discrepancy in the value that pow takes and the value that
915	** log gives.
916	*/
917	if (numVars == 0) {
918	numVars = DBL_MAX_EXP - 1;
919	}
920
921	info = ALLOC(ApproxInfo,1);
922	if (info == NULL) {
923	dd->errorCode = CUDD_MEMORY_OUT;
924	return(NULL);
925	}
926	info->max = pow(2.0,(double) numVars);
927	info->one = DD_ONE(dd);
928	info->zero = Cudd_Not(info->one);
929	info->size = Cudd_DagSize(node);
930	/* All the information gathered will be stored in a contiguous
931	** piece of memory, which is allocated here. This can be done
932	** efficiently because we have counted the number of nodes of the
933	** BDD. info->index points to the next available entry in the array
934	** that stores the per-node information. */
935	info->page = ALLOC(NodeData,info->size);
936	if (info->page == NULL) {
937	dd->errorCode = CUDD_MEMORY_OUT;
938	FREE(info);
939	return(NULL);
940	}
941	memset(info->page, 0, info->size * sizeof(NodeData)); /* clear all page */
942	info->table = st_init_table(st_ptrcmp,st_ptrhash);
943	if (info->table == NULL) {
944	FREE(info->page);
945	FREE(info);
946	return(NULL);
947	}
948	/* We visit the DAG in post-order DFS. Hence, the constant node is
949	** in first position, and the root of the DAG is in last position. */
950
951	/* Info for the constant node: Initialize only fields different from 0. */
952	if (st_insert(info->table, (char )info->one, (char )info->page) == ST_OUT_OF_MEM) {
953	FREE(info->page);
954	FREE(info);
955	st_free_table(info->table);
956	return(NULL);
957	}
958	info->page[0].mintermsP = info->max;
959	info->index = 1;
960
961	infoTop = gatherInfoAux(node,info,parity);
962	if (infoTop == NULL) {
963	FREE(info->page);
964	st_free_table(info->table);
965	FREE(info);
966	return(NULL);
967	}
968	if (Cudd_IsComplement(node)) {
969	info->minterms = infoTop->mintermsN;
970	} else {
971	info->minterms = infoTop->mintermsP;
972	}
973
974	infoTop->functionRef = 1;
975	return(info);
976
977	} /* end of gatherInfo */
978
979
980	/Function******************************************************************
981
982	Synopsis [Counts the nodes that would be eliminated if a given node
983	were replaced by zero.]
984
985	Description [Counts the nodes that would be eliminated if a given
986	node were replaced by zero. This procedure uses a queue passed by
987	the caller for efficiency: since the queue is left empty at the
988	endof the search, it can be reused as is by the next search. Returns
989	the count (always striclty positive) if successful; 0 otherwise.]
990
991	SideEffects [None]
992
993	SeeAlso [cuddUnderApprox]
994
995	******************************************************************************/
996	static int
997	computeSavings(
998	DdManager * dd,
999	DdNode * f,
1000	DdNode * skip,
1001	ApproxInfo * info,
1002	DdLevelQueue * queue)
1003	{
1004	NodeData *infoN;
1005	LocalQueueItem *item;
1006	DdNode *node;
1007	int savings = 0;
1008
1009	node = Cudd_Regular(f);
1010	skip = Cudd_Regular(skip);
1011	/* Insert the given node in the level queue. Its local reference
1012	** count is set equal to the function reference count so that the
1013	** search will continue from it when it is retrieved. */
1014	item = (LocalQueueItem *)
1015	cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
1016	if (item == NULL)
1017	return(0);
1018	(void) st_lookup(info->table, node, &infoN);
1019	item->localRef = infoN->functionRef;
1020
1021	/* Process the queue. */
1022	while (queue->first != NULL) {
1023	item = (LocalQueueItem *) queue->first;
1024	node = item->node;
1025	cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1026	if (node == skip) continue;
1027	(void) st_lookup(info->table, node, &infoN);
1028	if (item->localRef != infoN->functionRef) {
1029	/* This node is shared. */
1030	continue;
1031	}
1032	savings++;
1033	if (!cuddIsConstant(cuddT(node))) {
1034	item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
1035	cuddI(dd,cuddT(node)->index));
1036	if (item == NULL) return(0);
1037	item->localRef++;
1038	}
1039	if (!Cudd_IsConstant(cuddE(node))) {
1040	item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
1041	cuddI(dd,Cudd_Regular(cuddE(node))->index));
1042	if (item == NULL) return(0);
1043	item->localRef++;
1044	}
1045	}
1046
1047	#ifdef DD_DEBUG
1048	/* At the end of a local search the queue should be empty. */
1049	assert(queue->size == 0);
1050	#endif
1051	return(savings);
1052
1053	} /* end of computeSavings */
1054
1055
1056	/Function******************************************************************
1057
1058	Synopsis [Update function reference counts.]
1059
1060	Description [Update function reference counts to account for replacement.
1061	Returns the number of nodes saved if successful; 0 otherwise.]
1062
1063	SideEffects [None]
1064
1065	SeeAlso [UAmarkNodes RAmarkNodes]
1066
1067	******************************************************************************/
1068	static int
1069	updateRefs(
1070	DdManager * dd,
1071	DdNode * f,
1072	DdNode * skip,
1073	ApproxInfo * info,
1074	DdLevelQueue * queue)
1075	{
1076	NodeData *infoN;
1077	LocalQueueItem *item;
1078	DdNode *node;
1079	int savings = 0;
1080
1081	node = Cudd_Regular(f);
1082	/* Insert the given node in the level queue. Its function reference
1083	** count is set equal to 0 so that the search will continue from it
1084	** when it is retrieved. */
1085	item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
1086	if (item == NULL)
1087	return(0);
1088	(void) st_lookup(info->table, node, &infoN);
1089	infoN->functionRef = 0;
1090
1091	if (skip != NULL) {
1092	/* Increase the function reference count of the node to be skipped
1093	** by 1 to account for the node pointing to it that will be created. */
1094	skip = Cudd_Regular(skip);
1095	(void) st_lookup(info->table, skip, &infoN);
1096	infoN->functionRef++;
1097	}
1098
1099	/* Process the queue. */
1100	while (queue->first != NULL) {
1101	item = (LocalQueueItem *) queue->first;
1102	node = item->node;
1103	cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1104	(void) st_lookup(info->table, node, &infoN);
1105	if (infoN->functionRef != 0) {
1106	/* This node is shared or must be skipped. */
1107	continue;
1108	}
1109	savings++;
1110	if (!cuddIsConstant(cuddT(node))) {
1111	item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
1112	cuddI(dd,cuddT(node)->index));
1113	if (item == NULL) return(0);
1114	(void) st_lookup(info->table, cuddT(node), &infoN);
1115	infoN->functionRef--;
1116	}
1117	if (!Cudd_IsConstant(cuddE(node))) {
1118	item = (LocalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
1119	cuddI(dd,Cudd_Regular(cuddE(node))->index));
1120	if (item == NULL) return(0);
1121	(void) st_lookup(info->table, Cudd_Regular(cuddE(node)), &infoN);
1122	infoN->functionRef--;
1123	}
1124	}
1125
1126	#ifdef DD_DEBUG
1127	/* At the end of a local search the queue should be empty. */
1128	assert(queue->size == 0);
1129	#endif
1130	return(savings);
1131
1132	} /* end of updateRefs */
1133
1134
1135	/Function******************************************************************
1136
1137	Synopsis [Marks nodes for replacement by zero.]
1138
1139	Description [Marks nodes for replacement by zero. Returns 1 if successful;
1140	0 otherwise.]
1141
1142	SideEffects [None]
1143
1144	SeeAlso [cuddUnderApprox]
1145
1146	******************************************************************************/
1147	static int
1148	UAmarkNodes(
1149	DdManager * dd /* manager */,
1150	DdNode * f /* function to be analyzed */,
1151	ApproxInfo * info /* info on BDD */,
1152	int threshold /* when to stop approximating */,
1153	int safe /* enforce safe approximation */,
1154	double quality /* minimum improvement for accepted changes */)
1155	{
1156	DdLevelQueue *queue;
1157	DdLevelQueue *localQueue;
1158	NodeData *infoN;
1159	GlobalQueueItem *item;
1160	DdNode *node;
1161	double numOnset;
1162	double impactP, impactN;
1163	int savings;
1164
1165	#if 0
1166	(void) printf("initial size = %d initial minterms = %g\n",
1167	info->size, info->minterms);
1168	#endif
1169	queue = cuddLevelQueueInit(dd->size,sizeof(GlobalQueueItem),info->size);
1170	if (queue == NULL) {
1171	return(0);
1172	}
1173	localQueue = cuddLevelQueueInit(dd->size,sizeof(LocalQueueItem),
1174	dd->initSlots);
1175	if (localQueue == NULL) {
1176	cuddLevelQueueQuit(queue);
1177	return(0);
1178	}
1179	node = Cudd_Regular(f);
1180	item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
1181	if (item == NULL) {
1182	cuddLevelQueueQuit(queue);
1183	cuddLevelQueueQuit(localQueue);
1184	return(0);
1185	}
1186	if (Cudd_IsComplement(f)) {
1187	item->impactP = 0.0;
1188	item->impactN = 1.0;
1189	} else {
1190	item->impactP = 1.0;
1191	item->impactN = 0.0;
1192	}
1193	while (queue->first != NULL) {
1194	/* If the size of the subset is below the threshold, quit. */
1195	if (info->size <= threshold)
1196	break;
1197	item = (GlobalQueueItem *) queue->first;
1198	node = item->node;
1199	node = Cudd_Regular(node);
1200	(void) st_lookup(info->table, node, &infoN);
1201	if (safe && infoN->parity == 3) {
1202	cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1203	continue;
1204	}
1205	impactP = item->impactP;
1206	impactN = item->impactN;
1207	numOnset = infoN->mintermsP * impactP + infoN->mintermsN * impactN;
1208	savings = computeSavings(dd,node,NULL,info,localQueue);
1209	if (savings == 0) {
1210	cuddLevelQueueQuit(queue);
1211	cuddLevelQueueQuit(localQueue);
1212	return(0);
1213	}
1214	cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1215	#if 0
1216	(void) printf("node %p: impact = %g/%g numOnset = %g savings %d\n",
1217	node, impactP, impactN, numOnset, savings);
1218	#endif
1219	if ((1 - numOnset / info->minterms) >
1220	quality * (1 - (double) savings / info->size)) {
1221	infoN->replace = TRUE;
1222	info->size -= savings;
1223	info->minterms -=numOnset;
1224	#if 0
1225	(void) printf("replace: new size = %d new minterms = %g\n",
1226	info->size, info->minterms);
1227	#endif
1228	savings -= updateRefs(dd,node,NULL,info,localQueue);
1229	assert(savings == 0);
1230	continue;
1231	}
1232	if (!cuddIsConstant(cuddT(node))) {
1233	item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
1234	cuddI(dd,cuddT(node)->index));
1235	item->impactP += impactP/2.0;
1236	item->impactN += impactN/2.0;
1237	}
1238	if (!Cudd_IsConstant(cuddE(node))) {
1239	item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
1240	cuddI(dd,Cudd_Regular(cuddE(node))->index));
1241	if (Cudd_IsComplement(cuddE(node))) {
1242	item->impactP += impactN/2.0;
1243	item->impactN += impactP/2.0;
1244	} else {
1245	item->impactP += impactP/2.0;
1246	item->impactN += impactN/2.0;
1247	}
1248	}
1249	}
1250
1251	cuddLevelQueueQuit(queue);
1252	cuddLevelQueueQuit(localQueue);
1253	return(1);
1254
1255	} /* end of UAmarkNodes */
1256
1257
1258	/Function******************************************************************
1259
1260	Synopsis [Builds the subset BDD.]
1261
1262	Description [Builds the subset BDD. Based on the info table,
1263	replaces selected nodes by zero. Returns a pointer to the result if
1264	successful; NULL otherwise.]
1265
1266	SideEffects [None]
1267
1268	SeeAlso [cuddUnderApprox]
1269
1270	******************************************************************************/
1271	static DdNode *
1272	UAbuildSubset(
1273	DdManager * dd /* DD manager */,
1274	DdNode * node /* current node */,
1275	ApproxInfo * info /* node info */)
1276	{
1277
1278	DdNode Nt, Ne, N, t, e, r;
1279	NodeData *infoN;
1280
1281	if (Cudd_IsConstant(node))
1282	return(node);
1283
1284	N = Cudd_Regular(node);
1285
1286	if (st_lookup(info->table, N, &infoN)) {
1287	if (infoN->replace == TRUE) {
1288	return(info->zero);
1289	}
1290	if (N == node ) {
1291	if (infoN->resultP != NULL) {
1292	return(infoN->resultP);
1293	}
1294	} else {
1295	if (infoN->resultN != NULL) {
1296	return(infoN->resultN);
1297	}
1298	}
1299	} else {
1300	(void) fprintf(dd->err,
1301	"Something is wrong, ought to be in info table\n");
1302	dd->errorCode = CUDD_INTERNAL_ERROR;
1303	return(NULL);
1304	}
1305
1306	Nt = Cudd_NotCond(cuddT(N), Cudd_IsComplement(node));
1307	Ne = Cudd_NotCond(cuddE(N), Cudd_IsComplement(node));
1308
1309	t = UAbuildSubset(dd, Nt, info);
1310	if (t == NULL) {
1311	return(NULL);
1312	}
1313	cuddRef(t);
1314
1315	e = UAbuildSubset(dd, Ne, info);
1316	if (e == NULL) {
1317	Cudd_RecursiveDeref(dd,t);
1318	return(NULL);
1319	}
1320	cuddRef(e);
1321
1322	if (Cudd_IsComplement(t)) {
1323	t = Cudd_Not(t);
1324	e = Cudd_Not(e);
1325	r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
1326	if (r == NULL) {
1327	Cudd_RecursiveDeref(dd, e);
1328	Cudd_RecursiveDeref(dd, t);
1329	return(NULL);
1330	}
1331	r = Cudd_Not(r);
1332	} else {
1333	r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
1334	if (r == NULL) {
1335	Cudd_RecursiveDeref(dd, e);
1336	Cudd_RecursiveDeref(dd, t);
1337	return(NULL);
1338	}
1339	}
1340	cuddDeref(t);
1341	cuddDeref(e);
1342
1343	if (N == node) {
1344	infoN->resultP = r;
1345	} else {
1346	infoN->resultN = r;
1347	}
1348
1349	return(r);
1350
1351	} /* end of UAbuildSubset */
1352
1353
1354	/Function******************************************************************
1355
1356	Synopsis [Marks nodes for remapping.]
1357
1358	Description [Marks nodes for remapping. Returns 1 if successful; 0
1359	otherwise.]
1360
1361	SideEffects [None]
1362
1363	SeeAlso [cuddRemapUnderApprox]
1364
1365	******************************************************************************/
1366	static int
1367	RAmarkNodes(
1368	DdManager * dd /* manager */,
1369	DdNode * f /* function to be analyzed */,
1370	ApproxInfo * info /* info on BDD */,
1371	int threshold /* when to stop approximating */,
1372	double quality /* minimum improvement for accepted changes */)
1373	{
1374	DdLevelQueue *queue;
1375	DdLevelQueue *localQueue;
1376	NodeData infoN, infoT, *infoE;
1377	GlobalQueueItem *item;
1378	DdNode node, T, *E;
1379	DdNode shared; / grandchild shared by the two children of node */
1380	double numOnset;
1381	double impact, impactP, impactN;
1382	double minterms;
1383	int savings;
1384	int replace;
1385
1386	#if 0
1387	(void) fprintf(dd->out,"initial size = %d initial minterms = %g\n",
1388	info->size, info->minterms);
1389	#endif
1390	queue = cuddLevelQueueInit(dd->size,sizeof(GlobalQueueItem),info->size);
1391	if (queue == NULL) {
1392	return(0);
1393	}
1394	localQueue = cuddLevelQueueInit(dd->size,sizeof(LocalQueueItem),
1395	dd->initSlots);
1396	if (localQueue == NULL) {
1397	cuddLevelQueueQuit(queue);
1398	return(0);
1399	}
1400	/* Enqueue regular pointer to root and initialize impact. */
1401	node = Cudd_Regular(f);
1402	item = (GlobalQueueItem *)
1403	cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
1404	if (item == NULL) {
1405	cuddLevelQueueQuit(queue);
1406	cuddLevelQueueQuit(localQueue);
1407	return(0);
1408	}
1409	if (Cudd_IsComplement(f)) {
1410	item->impactP = 0.0;
1411	item->impactN = 1.0;
1412	} else {
1413	item->impactP = 1.0;
1414	item->impactN = 0.0;
1415	}
1416	/* The nodes retrieved here are guaranteed to be non-terminal.
1417	** The initial node is not terminal because constant nodes are
1418	** dealt with in the calling procedure. Subsequent nodes are inserted
1419	** only if they are not terminal. */
1420	while (queue->first != NULL) {
1421	/* If the size of the subset is below the threshold, quit. */
1422	if (info->size <= threshold)
1423	break;
1424	item = (GlobalQueueItem *) queue->first;
1425	node = item->node;
1426	#ifdef DD_DEBUG
1427	assert(item->impactP >= 0 && item->impactP <= 1.0);
1428	assert(item->impactN >= 0 && item->impactN <= 1.0);
1429	assert(!Cudd_IsComplement(node));
1430	assert(!Cudd_IsConstant(node));
1431	#endif
1432	if (!st_lookup(info->table, node, &infoN)) {
1433	cuddLevelQueueQuit(queue);
1434	cuddLevelQueueQuit(localQueue);
1435	return(0);
1436	}
1437	#ifdef DD_DEBUG
1438	assert(infoN->parity >= 1 && infoN->parity <= 3);
1439	#endif
1440	if (infoN->parity == 3) {
1441	/* This node can be reached through paths of different parity.
1442	** It is not safe to replace it, because remapping will give
1443	** an incorrect result, while replacement by 0 may cause node
1444	** splitting. */
1445	cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1446	continue;
1447	}
1448	T = cuddT(node);
1449	E = cuddE(node);
1450	shared = NULL;
1451	impactP = item->impactP;
1452	impactN = item->impactN;
1453	if (Cudd_bddLeq(dd,T,E)) {
1454	/* Here we know that E is regular. */
1455	#ifdef DD_DEBUG
1456	assert(!Cudd_IsComplement(E));
1457	#endif
1458	(void) st_lookup(info->table, T, &infoT);
1459	(void) st_lookup(info->table, E, &infoE);
1460	if (infoN->parity == 1) {
1461	impact = impactP;
1462	minterms = infoE->mintermsP/2.0 - infoT->mintermsP/2.0;
1463	if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
1464	savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
1465	if (savings == 1) {
1466	cuddLevelQueueQuit(queue);
1467	cuddLevelQueueQuit(localQueue);
1468	return(0);
1469	}
1470	} else {
1471	savings = 1;
1472	}
1473	replace = REPLACE_E;
1474	} else {
1475	#ifdef DD_DEBUG
1476	assert(infoN->parity == 2);
1477	#endif
1478	impact = impactN;
1479	minterms = infoT->mintermsN/2.0 - infoE->mintermsN/2.0;
1480	if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
1481	savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
1482	if (savings == 1) {
1483	cuddLevelQueueQuit(queue);
1484	cuddLevelQueueQuit(localQueue);
1485	return(0);
1486	}
1487	} else {
1488	savings = 1;
1489	}
1490	replace = REPLACE_T;
1491	}
1492	numOnset = impact * minterms;
1493	} else if (Cudd_bddLeq(dd,E,T)) {
1494	/* Here E may be complemented. */
1495	DdNode *Ereg = Cudd_Regular(E);
1496	(void) st_lookup(info->table, T, &infoT);
1497	(void) st_lookup(info->table, Ereg, &infoE);
1498	if (infoN->parity == 1) {
1499	impact = impactP;
1500	minterms = infoT->mintermsP/2.0 -
1501	((E == Ereg) ? infoE->mintermsP : infoE->mintermsN)/2.0;
1502	if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
1503	savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
1504	if (savings == 1) {
1505	cuddLevelQueueQuit(queue);
1506	cuddLevelQueueQuit(localQueue);
1507	return(0);
1508	}
1509	} else {
1510	savings = 1;
1511	}
1512	replace = REPLACE_T;
1513	} else {
1514	#ifdef DD_DEBUG
1515	assert(infoN->parity == 2);
1516	#endif
1517	impact = impactN;
1518	minterms = ((E == Ereg) ? infoE->mintermsN :
1519	infoE->mintermsP)/2.0 - infoT->mintermsN/2.0;
1520	if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
1521	savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
1522	if (savings == 1) {
1523	cuddLevelQueueQuit(queue);
1524	cuddLevelQueueQuit(localQueue);
1525	return(0);
1526	}
1527	} else {
1528	savings = 1;
1529	}
1530	replace = REPLACE_E;
1531	}
1532	numOnset = impact * minterms;
1533	} else {
1534	DdNode *Ereg = Cudd_Regular(E);
1535	DdNode *TT = cuddT(T);
1536	DdNode *ET = Cudd_NotCond(cuddT(Ereg), Cudd_IsComplement(E));
1537	if (T->index == Ereg->index && TT == ET) {
1538	shared = TT;
1539	replace = REPLACE_TT;
1540	} else {
1541	DdNode *TE = cuddE(T);
1542	DdNode *EE = Cudd_NotCond(cuddE(Ereg), Cudd_IsComplement(E));
1543	if (T->index == Ereg->index && TE == EE) {
1544	shared = TE;
1545	replace = REPLACE_TE;
1546	} else {
1547	replace = REPLACE_N;
1548	}
1549	}
1550	numOnset = infoN->mintermsP * impactP + infoN->mintermsN * impactN;
1551	savings = computeSavings(dd,node,shared,info,localQueue);
1552	if (shared != NULL) {
1553	NodeData *infoS;
1554	(void) st_lookup(info->table, Cudd_Regular(shared), &infoS);
1555	if (Cudd_IsComplement(shared)) {
1556	numOnset -= (infoS->mintermsN * impactP +
1557	infoS->mintermsP * impactN)/2.0;
1558	} else {
1559	numOnset -= (infoS->mintermsP * impactP +
1560	infoS->mintermsN * impactN)/2.0;
1561	}
1562	savings--;
1563	}
1564	}
1565
1566	cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1567	#if 0
1568	if (replace == REPLACE_T \|\| replace == REPLACE_E)
1569	(void) printf("node %p: impact = %g numOnset = %g savings %d\n",
1570	node, impact, numOnset, savings);
1571	else
1572	(void) printf("node %p: impact = %g/%g numOnset = %g savings %d\n",
1573	node, impactP, impactN, numOnset, savings);
1574	#endif
1575	if ((1 - numOnset / info->minterms) >
1576	quality * (1 - (double) savings / info->size)) {
1577	infoN->replace = replace;
1578	info->size -= savings;
1579	info->minterms -=numOnset;
1580	#if 0
1581	(void) printf("remap(%d): new size = %d new minterms = %g\n",
1582	replace, info->size, info->minterms);
1583	#endif
1584	if (replace == REPLACE_N) {
1585	savings -= updateRefs(dd,node,NULL,info,localQueue);
1586	} else if (replace == REPLACE_T) {
1587	savings -= updateRefs(dd,node,E,info,localQueue);
1588	} else if (replace == REPLACE_E) {
1589	savings -= updateRefs(dd,node,T,info,localQueue);
1590	} else {
1591	#ifdef DD_DEBUG
1592	assert(replace == REPLACE_TT \|\| replace == REPLACE_TE);
1593	#endif
1594	savings -= updateRefs(dd,node,shared,info,localQueue) - 1;
1595	}
1596	assert(savings == 0);
1597	} else {
1598	replace = NOTHING;
1599	}
1600	if (replace == REPLACE_N) continue;
1601	if ((replace == REPLACE_E \|\| replace == NOTHING) &&
1602	!cuddIsConstant(cuddT(node))) {
1603	item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
1604	cuddI(dd,cuddT(node)->index));
1605	if (replace == REPLACE_E) {
1606	item->impactP += impactP;
1607	item->impactN += impactN;
1608	} else {
1609	item->impactP += impactP/2.0;
1610	item->impactN += impactN/2.0;
1611	}
1612	}
1613	if ((replace == REPLACE_T \|\| replace == NOTHING) &&
1614	!Cudd_IsConstant(cuddE(node))) {
1615	item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
1616	cuddI(dd,Cudd_Regular(cuddE(node))->index));
1617	if (Cudd_IsComplement(cuddE(node))) {
1618	if (replace == REPLACE_T) {
1619	item->impactP += impactN;
1620	item->impactN += impactP;
1621	} else {
1622	item->impactP += impactN/2.0;
1623	item->impactN += impactP/2.0;
1624	}
1625	} else {
1626	if (replace == REPLACE_T) {
1627	item->impactP += impactP;
1628	item->impactN += impactN;
1629	} else {
1630	item->impactP += impactP/2.0;
1631	item->impactN += impactN/2.0;
1632	}
1633	}
1634	}
1635	if ((replace == REPLACE_TT \|\| replace == REPLACE_TE) &&
1636	!Cudd_IsConstant(shared)) {
1637	item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(shared),
1638	cuddI(dd,Cudd_Regular(shared)->index));
1639	if (Cudd_IsComplement(shared)) {
1640	if (replace == REPLACE_T) {
1641	item->impactP += impactN;
1642	item->impactN += impactP;
1643	} else {
1644	item->impactP += impactN/2.0;
1645	item->impactN += impactP/2.0;
1646	}
1647	} else {
1648	if (replace == REPLACE_T) {
1649	item->impactP += impactP;
1650	item->impactN += impactN;
1651	} else {
1652	item->impactP += impactP/2.0;
1653	item->impactN += impactN/2.0;
1654	}
1655	}
1656	}
1657	}
1658
1659	cuddLevelQueueQuit(queue);
1660	cuddLevelQueueQuit(localQueue);
1661	return(1);
1662
1663	} /* end of RAmarkNodes */
1664
1665
1666	/Function******************************************************************
1667
1668	Synopsis [Marks nodes for remapping.]
1669
1670	Description [Marks nodes for remapping. Returns 1 if successful; 0
1671	otherwise.]
1672
1673	SideEffects [None]
1674
1675	SeeAlso [cuddRemapUnderApprox]
1676
1677	******************************************************************************/
1678	static int
1679	BAmarkNodes(
1680	DdManager dd / manager */,
1681	DdNode f / function to be analyzed */,
1682	ApproxInfo info / info on BDD */,
1683	int threshold /* when to stop approximating */,
1684	double quality1 /* minimum improvement for accepted changes when b=1 */,
1685	double quality0 /* minimum improvement for accepted changes when b=0 */)
1686	{
1687	DdLevelQueue *queue;
1688	DdLevelQueue *localQueue;
1689	NodeData infoN, infoT, *infoE;
1690	GlobalQueueItem *item;
1691	DdNode node, T, *E;
1692	DdNode shared; / grandchild shared by the two children of node */
1693	double numOnset;
1694	double impact, impactP, impactN;
1695	double minterms;
1696	double quality;
1697	int savings;
1698	int replace;
1699
1700	#if 0
1701	(void) fprintf(dd->out,"initial size = %d initial minterms = %g\n",
1702	info->size, info->minterms);
1703	#endif
1704	queue = cuddLevelQueueInit(dd->size,sizeof(GlobalQueueItem),info->size);
1705	if (queue == NULL) {
1706	return(0);
1707	}
1708	localQueue = cuddLevelQueueInit(dd->size,sizeof(LocalQueueItem),
1709	dd->initSlots);
1710	if (localQueue == NULL) {
1711	cuddLevelQueueQuit(queue);
1712	return(0);
1713	}
1714	/* Enqueue regular pointer to root and initialize impact. */
1715	node = Cudd_Regular(f);
1716	item = (GlobalQueueItem *)
1717	cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
1718	if (item == NULL) {
1719	cuddLevelQueueQuit(queue);
1720	cuddLevelQueueQuit(localQueue);
1721	return(0);
1722	}
1723	if (Cudd_IsComplement(f)) {
1724	item->impactP = 0.0;
1725	item->impactN = 1.0;
1726	} else {
1727	item->impactP = 1.0;
1728	item->impactN = 0.0;
1729	}
1730	/* The nodes retrieved here are guaranteed to be non-terminal.
1731	** The initial node is not terminal because constant nodes are
1732	** dealt with in the calling procedure. Subsequent nodes are inserted
1733	** only if they are not terminal. */
1734	while (queue->first != NULL) {
1735	/* If the size of the subset is below the threshold, quit. */
1736	if (info->size <= threshold)
1737	break;
1738	item = (GlobalQueueItem *) queue->first;
1739	node = item->node;
1740	#ifdef DD_DEBUG
1741	assert(item->impactP >= 0 && item->impactP <= 1.0);
1742	assert(item->impactN >= 0 && item->impactN <= 1.0);
1743	assert(!Cudd_IsComplement(node));
1744	assert(!Cudd_IsConstant(node));
1745	#endif
1746	if (!st_lookup(info->table, node, &infoN)) {
1747	cuddLevelQueueQuit(queue);
1748	cuddLevelQueueQuit(localQueue);
1749	return(0);
1750	}
1751	quality = infoN->care ? quality1 : quality0;
1752	#ifdef DD_DEBUG
1753	assert(infoN->parity >= 1 && infoN->parity <= 3);
1754	#endif
1755	if (infoN->parity == 3) {
1756	/* This node can be reached through paths of different parity.
1757	** It is not safe to replace it, because remapping will give
1758	** an incorrect result, while replacement by 0 may cause node
1759	** splitting. */
1760	cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1761	continue;
1762	}
1763	T = cuddT(node);
1764	E = cuddE(node);
1765	shared = NULL;
1766	impactP = item->impactP;
1767	impactN = item->impactN;
1768	if (Cudd_bddLeq(dd,T,E)) {
1769	/* Here we know that E is regular. */
1770	#ifdef DD_DEBUG
1771	assert(!Cudd_IsComplement(E));
1772	#endif
1773	(void) st_lookup(info->table, T, &infoT);
1774	(void) st_lookup(info->table, E, &infoE);
1775	if (infoN->parity == 1) {
1776	impact = impactP;
1777	minterms = infoE->mintermsP/2.0 - infoT->mintermsP/2.0;
1778	if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
1779	savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
1780	if (savings == 1) {
1781	cuddLevelQueueQuit(queue);
1782	cuddLevelQueueQuit(localQueue);
1783	return(0);
1784	}
1785	} else {
1786	savings = 1;
1787	}
1788	replace = REPLACE_E;
1789	} else {
1790	#ifdef DD_DEBUG
1791	assert(infoN->parity == 2);
1792	#endif
1793	impact = impactN;
1794	minterms = infoT->mintermsN/2.0 - infoE->mintermsN/2.0;
1795	if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
1796	savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
1797	if (savings == 1) {
1798	cuddLevelQueueQuit(queue);
1799	cuddLevelQueueQuit(localQueue);
1800	return(0);
1801	}
1802	} else {
1803	savings = 1;
1804	}
1805	replace = REPLACE_T;
1806	}
1807	numOnset = impact * minterms;
1808	} else if (Cudd_bddLeq(dd,E,T)) {
1809	/* Here E may be complemented. */
1810	DdNode *Ereg = Cudd_Regular(E);
1811	(void) st_lookup(info->table, T, &infoT);
1812	(void) st_lookup(info->table, Ereg, &infoE);
1813	if (infoN->parity == 1) {
1814	impact = impactP;
1815	minterms = infoT->mintermsP/2.0 -
1816	((E == Ereg) ? infoE->mintermsP : infoE->mintermsN)/2.0;
1817	if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
1818	savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
1819	if (savings == 1) {
1820	cuddLevelQueueQuit(queue);
1821	cuddLevelQueueQuit(localQueue);
1822	return(0);
1823	}
1824	} else {
1825	savings = 1;
1826	}
1827	replace = REPLACE_T;
1828	} else {
1829	#ifdef DD_DEBUG
1830	assert(infoN->parity == 2);
1831	#endif
1832	impact = impactN;
1833	minterms = ((E == Ereg) ? infoE->mintermsN :
1834	infoE->mintermsP)/2.0 - infoT->mintermsN/2.0;
1835	if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
1836	savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
1837	if (savings == 1) {
1838	cuddLevelQueueQuit(queue);
1839	cuddLevelQueueQuit(localQueue);
1840	return(0);
1841	}
1842	} else {
1843	savings = 1;
1844	}
1845	replace = REPLACE_E;
1846	}
1847	numOnset = impact * minterms;
1848	} else {
1849	DdNode *Ereg = Cudd_Regular(E);
1850	DdNode *TT = cuddT(T);
1851	DdNode *ET = Cudd_NotCond(cuddT(Ereg), Cudd_IsComplement(E));
1852	if (T->index == Ereg->index && TT == ET) {
1853	shared = TT;
1854	replace = REPLACE_TT;
1855	} else {
1856	DdNode *TE = cuddE(T);
1857	DdNode *EE = Cudd_NotCond(cuddE(Ereg), Cudd_IsComplement(E));
1858	if (T->index == Ereg->index && TE == EE) {
1859	shared = TE;
1860	replace = REPLACE_TE;
1861	} else {
1862	replace = REPLACE_N;
1863	}
1864	}
1865	numOnset = infoN->mintermsP * impactP + infoN->mintermsN * impactN;
1866	savings = computeSavings(dd,node,shared,info,localQueue);
1867	if (shared != NULL) {
1868	NodeData *infoS;
1869	(void) st_lookup(info->table, Cudd_Regular(shared), &infoS);
1870	if (Cudd_IsComplement(shared)) {
1871	numOnset -= (infoS->mintermsN * impactP +
1872	infoS->mintermsP * impactN)/2.0;
1873	} else {
1874	numOnset -= (infoS->mintermsP * impactP +
1875	infoS->mintermsN * impactN)/2.0;
1876	}
1877	savings--;
1878	}
1879	}
1880
1881	cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1882	#if 0
1883	if (replace == REPLACE_T \|\| replace == REPLACE_E)
1884	(void) printf("node %p: impact = %g numOnset = %g savings %d\n",
1885	node, impact, numOnset, savings);
1886	else
1887	(void) printf("node %p: impact = %g/%g numOnset = %g savings %d\n",
1888	node, impactP, impactN, numOnset, savings);
1889	#endif
1890	if ((1 - numOnset / info->minterms) >
1891	quality * (1 - (double) savings / info->size)) {
1892	infoN->replace = replace;
1893	info->size -= savings;
1894	info->minterms -=numOnset;
1895	#if 0
1896	(void) printf("remap(%d): new size = %d new minterms = %g\n",
1897	replace, info->size, info->minterms);
1898	#endif
1899	if (replace == REPLACE_N) {
1900	savings -= updateRefs(dd,node,NULL,info,localQueue);
1901	} else if (replace == REPLACE_T) {
1902	savings -= updateRefs(dd,node,E,info,localQueue);
1903	} else if (replace == REPLACE_E) {
1904	savings -= updateRefs(dd,node,T,info,localQueue);
1905	} else {
1906	#ifdef DD_DEBUG
1907	assert(replace == REPLACE_TT \|\| replace == REPLACE_TE);
1908	#endif
1909	savings -= updateRefs(dd,node,shared,info,localQueue) - 1;
1910	}
1911	assert(savings == 0);
1912	} else {
1913	replace = NOTHING;
1914	}
1915	if (replace == REPLACE_N) continue;
1916	if ((replace == REPLACE_E \|\| replace == NOTHING) &&
1917	!cuddIsConstant(cuddT(node))) {
1918	item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
1919	cuddI(dd,cuddT(node)->index));
1920	if (replace == REPLACE_E) {
1921	item->impactP += impactP;
1922	item->impactN += impactN;
1923	} else {
1924	item->impactP += impactP/2.0;
1925	item->impactN += impactN/2.0;
1926	}
1927	}
1928	if ((replace == REPLACE_T \|\| replace == NOTHING) &&
1929	!Cudd_IsConstant(cuddE(node))) {
1930	item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
1931	cuddI(dd,Cudd_Regular(cuddE(node))->index));
1932	if (Cudd_IsComplement(cuddE(node))) {
1933	if (replace == REPLACE_T) {
1934	item->impactP += impactN;
1935	item->impactN += impactP;
1936	} else {
1937	item->impactP += impactN/2.0;
1938	item->impactN += impactP/2.0;
1939	}
1940	} else {
1941	if (replace == REPLACE_T) {
1942	item->impactP += impactP;
1943	item->impactN += impactN;
1944	} else {
1945	item->impactP += impactP/2.0;
1946	item->impactN += impactN/2.0;
1947	}
1948	}
1949	}
1950	if ((replace == REPLACE_TT \|\| replace == REPLACE_TE) &&
1951	!Cudd_IsConstant(shared)) {
1952	item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(shared),
1953	cuddI(dd,Cudd_Regular(shared)->index));
1954	if (Cudd_IsComplement(shared)) {
1955	if (replace == REPLACE_T) {
1956	item->impactP += impactN;
1957	item->impactN += impactP;
1958	} else {
1959	item->impactP += impactN/2.0;
1960	item->impactN += impactP/2.0;
1961	}
1962	} else {
1963	if (replace == REPLACE_T) {
1964	item->impactP += impactP;
1965	item->impactN += impactN;
1966	} else {
1967	item->impactP += impactP/2.0;
1968	item->impactN += impactN/2.0;
1969	}
1970	}
1971	}
1972	}
1973
1974	cuddLevelQueueQuit(queue);
1975	cuddLevelQueueQuit(localQueue);
1976	return(1);
1977
1978	} /* end of BAmarkNodes */
1979
1980
1981	/Function******************************************************************
1982
1983	Synopsis [Builds the subset BDD for cuddRemapUnderApprox.]
1984
1985	Description [Builds the subset BDDfor cuddRemapUnderApprox. Based
1986	on the info table, performs remapping or replacement at selected
1987	nodes. Returns a pointer to the result if successful; NULL
1988	otherwise.]
1989
1990	SideEffects [None]
1991
1992	SeeAlso [cuddRemapUnderApprox]
1993
1994	******************************************************************************/
1995	static DdNode *
1996	RAbuildSubset(
1997	DdManager * dd /* DD manager */,
1998	DdNode * node /* current node */,
1999	ApproxInfo * info /* node info */)
2000	{
2001	DdNode Nt, Ne, N, t, e, r;
2002	NodeData *infoN;
2003
2004	if (Cudd_IsConstant(node))
2005	return(node);
2006
2007	N = Cudd_Regular(node);
2008
2009	Nt = Cudd_NotCond(cuddT(N), Cudd_IsComplement(node));
2010	Ne = Cudd_NotCond(cuddE(N), Cudd_IsComplement(node));
2011
2012	if (st_lookup(info->table, N, &infoN)) {
2013	if (N == node ) {
2014	if (infoN->resultP != NULL) {
2015	return(infoN->resultP);
2016	}
2017	} else {
2018	if (infoN->resultN != NULL) {
2019	return(infoN->resultN);
2020	}
2021	}
2022	if (infoN->replace == REPLACE_T) {
2023	r = RAbuildSubset(dd, Ne, info);
2024	return(r);
2025	} else if (infoN->replace == REPLACE_E) {
2026	r = RAbuildSubset(dd, Nt, info);
2027	return(r);
2028	} else if (infoN->replace == REPLACE_N) {
2029	return(info->zero);
2030	} else if (infoN->replace == REPLACE_TT) {
2031	DdNode *Ntt = Cudd_NotCond(cuddT(cuddT(N)),
2032	Cudd_IsComplement(node));
2033	int index = cuddT(N)->index;
2034	DdNode *e = info->zero;
2035	DdNode *t = RAbuildSubset(dd, Ntt, info);
2036	if (t == NULL) {
2037	return(NULL);
2038	}
2039	cuddRef(t);
2040	if (Cudd_IsComplement(t)) {
2041	t = Cudd_Not(t);
2042	e = Cudd_Not(e);
2043	r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
2044	if (r == NULL) {
2045	Cudd_RecursiveDeref(dd, t);
2046	return(NULL);
2047	}
2048	r = Cudd_Not(r);
2049	} else {
2050	r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
2051	if (r == NULL) {
2052	Cudd_RecursiveDeref(dd, t);
2053	return(NULL);
2054	}
2055	}
2056	cuddDeref(t);
2057	return(r);
2058	} else if (infoN->replace == REPLACE_TE) {
2059	DdNode *Nte = Cudd_NotCond(cuddE(cuddT(N)),
2060	Cudd_IsComplement(node));
2061	int index = cuddT(N)->index;
2062	DdNode *t = info->one;
2063	DdNode *e = RAbuildSubset(dd, Nte, info);
2064	if (e == NULL) {
2065	return(NULL);
2066	}
2067	cuddRef(e);
2068	e = Cudd_Not(e);
2069	r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
2070	if (r == NULL) {
2071	Cudd_RecursiveDeref(dd, e);
2072	return(NULL);
2073	}
2074	r =Cudd_Not(r);
2075	cuddDeref(e);
2076	return(r);
2077	}
2078	} else {
2079	(void) fprintf(dd->err,
2080	"Something is wrong, ought to be in info table\n");
2081	dd->errorCode = CUDD_INTERNAL_ERROR;
2082	return(NULL);
2083	}
2084
2085	t = RAbuildSubset(dd, Nt, info);
2086	if (t == NULL) {
2087	return(NULL);
2088	}
2089	cuddRef(t);
2090
2091	e = RAbuildSubset(dd, Ne, info);
2092	if (e == NULL) {
2093	Cudd_RecursiveDeref(dd,t);
2094	return(NULL);
2095	}
2096	cuddRef(e);
2097
2098	if (Cudd_IsComplement(t)) {
2099	t = Cudd_Not(t);
2100	e = Cudd_Not(e);
2101	r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
2102	if (r == NULL) {
2103	Cudd_RecursiveDeref(dd, e);
2104	Cudd_RecursiveDeref(dd, t);
2105	return(NULL);
2106	}
2107	r = Cudd_Not(r);
2108	} else {
2109	r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
2110	if (r == NULL) {
2111	Cudd_RecursiveDeref(dd, e);
2112	Cudd_RecursiveDeref(dd, t);
2113	return(NULL);
2114	}
2115	}
2116	cuddDeref(t);
2117	cuddDeref(e);
2118
2119	if (N == node) {
2120	infoN->resultP = r;
2121	} else {
2122	infoN->resultN = r;
2123	}
2124
2125	return(r);
2126
2127	} /* end of RAbuildSubset */
2128
2129
2130	/Function******************************************************************
2131
2132	Synopsis [Finds don't care nodes.]
2133
2134	Description [Finds don't care nodes by traversing f and b in parallel.
2135	Returns the care status of the visited f node if successful; CARE_ERROR
2136	otherwise.]
2137
2138	SideEffects [None]
2139
2140	SeeAlso [cuddBiasedUnderApprox]
2141
2142	******************************************************************************/
2143	static int
2144	BAapplyBias(
2145	DdManager *dd,
2146	DdNode *f,
2147	DdNode *b,
2148	ApproxInfo *info,
2149	DdHashTable *cache)
2150	{
2151	DdNode one, zero, *res;
2152	DdNode Ft, Fe, B, Bt, *Be;
2153	unsigned int topf, topb;
2154	NodeData *infoF;
2155	int careT, careE;
2156
2157	one = DD_ONE(dd);
2158	zero = Cudd_Not(one);
2159
2160	if (!st_lookup(info->table, f, &infoF))
2161	return(CARE_ERROR);
2162	if (f == one) return(TOTAL_CARE);
2163	if (b == zero) return(infoF->care);
2164	if (infoF->care == TOTAL_CARE) return(TOTAL_CARE);
2165
2166	if ((f->ref != 1 \|\| Cudd_Regular(b)->ref != 1) &&
2167	(res = cuddHashTableLookup2(cache,f,b)) != NULL) {
2168	if (res->ref == 0) {
2169	cache->manager->dead++;
2170	cache->manager->constants.dead++;
2171	}
2172	return(infoF->care);
2173	}
2174
2175	topf = dd->perm[f->index];
2176	B = Cudd_Regular(b);
2177	topb = cuddI(dd,B->index);
2178	if (topf <= topb) {
2179	Ft = cuddT(f); Fe = cuddE(f);
2180	} else {
2181	Ft = Fe = f;
2182	}
2183	if (topb <= topf) {
2184	/* We know that b is not constant because f is not. */
2185	Bt = cuddT(B); Be = cuddE(B);
2186	if (Cudd_IsComplement(b)) {
2187	Bt = Cudd_Not(Bt);
2188	Be = Cudd_Not(Be);
2189	}
2190	} else {
2191	Bt = Be = b;
2192	}
2193
2194	careT = BAapplyBias(dd, Ft, Bt, info, cache);
2195	if (careT == CARE_ERROR)
2196	return(CARE_ERROR);
2197	careE = BAapplyBias(dd, Cudd_Regular(Fe), Be, info, cache);
2198	if (careE == CARE_ERROR)
2199	return(CARE_ERROR);
2200	if (careT == TOTAL_CARE && careE == TOTAL_CARE) {
2201	infoF->care = TOTAL_CARE;
2202	} else {
2203	infoF->care = CARE;
2204	}
2205
2206	if (f->ref != 1 \|\| Cudd_Regular(b)->ref != 1) {
2207	ptrint fanout = (ptrint) f->ref * Cudd_Regular(b)->ref;
2208	cuddSatDec(fanout);
2209	if (!cuddHashTableInsert2(cache,f,b,one,fanout)) {
2210	return(CARE_ERROR);
2211	}
2212	}
2213	return(infoF->care);
2214
2215	} /* end of BAapplyBias */

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

Download in other formats: