Context Navigation

← Previous Revision
Latest Revision
Next Revision →
Blame
Revision Log

cuddApprox.c @ 88

Last change on this file since 88 was 13, checked in by cecile, 13 years ago
library glu 2.3
File size: 66.6 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.27 2009/02/19 16:16:51 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 \|= (short) 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 \|= (short) (1 + 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 = (char) 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	item->impactP += impactN;
1641	item->impactN += impactP;
1642	} else {
1643	item->impactP += impactP;
1644	item->impactN += impactN;
1645	}
1646	}
1647	}
1648
1649	cuddLevelQueueQuit(queue);
1650	cuddLevelQueueQuit(localQueue);
1651	return(1);
1652
1653	} /* end of RAmarkNodes */
1654
1655
1656	/Function******************************************************************
1657
1658	Synopsis [Marks nodes for remapping.]
1659
1660	Description [Marks nodes for remapping. Returns 1 if successful; 0
1661	otherwise.]
1662
1663	SideEffects [None]
1664
1665	SeeAlso [cuddRemapUnderApprox]
1666
1667	******************************************************************************/
1668	static int
1669	BAmarkNodes(
1670	DdManager dd / manager */,
1671	DdNode f / function to be analyzed */,
1672	ApproxInfo info / info on BDD */,
1673	int threshold /* when to stop approximating */,
1674	double quality1 /* minimum improvement for accepted changes when b=1 */,
1675	double quality0 /* minimum improvement for accepted changes when b=0 */)
1676	{
1677	DdLevelQueue *queue;
1678	DdLevelQueue *localQueue;
1679	NodeData infoN, infoT, *infoE;
1680	GlobalQueueItem *item;
1681	DdNode node, T, *E;
1682	DdNode shared; / grandchild shared by the two children of node */
1683	double numOnset;
1684	double impact, impactP, impactN;
1685	double minterms;
1686	double quality;
1687	int savings;
1688	int replace;
1689
1690	#if 0
1691	(void) fprintf(dd->out,"initial size = %d initial minterms = %g\n",
1692	info->size, info->minterms);
1693	#endif
1694	queue = cuddLevelQueueInit(dd->size,sizeof(GlobalQueueItem),info->size);
1695	if (queue == NULL) {
1696	return(0);
1697	}
1698	localQueue = cuddLevelQueueInit(dd->size,sizeof(LocalQueueItem),
1699	dd->initSlots);
1700	if (localQueue == NULL) {
1701	cuddLevelQueueQuit(queue);
1702	return(0);
1703	}
1704	/* Enqueue regular pointer to root and initialize impact. */
1705	node = Cudd_Regular(f);
1706	item = (GlobalQueueItem *)
1707	cuddLevelQueueEnqueue(queue,node,cuddI(dd,node->index));
1708	if (item == NULL) {
1709	cuddLevelQueueQuit(queue);
1710	cuddLevelQueueQuit(localQueue);
1711	return(0);
1712	}
1713	if (Cudd_IsComplement(f)) {
1714	item->impactP = 0.0;
1715	item->impactN = 1.0;
1716	} else {
1717	item->impactP = 1.0;
1718	item->impactN = 0.0;
1719	}
1720	/* The nodes retrieved here are guaranteed to be non-terminal.
1721	** The initial node is not terminal because constant nodes are
1722	** dealt with in the calling procedure. Subsequent nodes are inserted
1723	** only if they are not terminal. */
1724	while (queue->first != NULL) {
1725	/* If the size of the subset is below the threshold, quit. */
1726	if (info->size <= threshold)
1727	break;
1728	item = (GlobalQueueItem *) queue->first;
1729	node = item->node;
1730	#ifdef DD_DEBUG
1731	assert(item->impactP >= 0 && item->impactP <= 1.0);
1732	assert(item->impactN >= 0 && item->impactN <= 1.0);
1733	assert(!Cudd_IsComplement(node));
1734	assert(!Cudd_IsConstant(node));
1735	#endif
1736	if (!st_lookup(info->table, node, &infoN)) {
1737	cuddLevelQueueQuit(queue);
1738	cuddLevelQueueQuit(localQueue);
1739	return(0);
1740	}
1741	quality = infoN->care ? quality1 : quality0;
1742	#ifdef DD_DEBUG
1743	assert(infoN->parity >= 1 && infoN->parity <= 3);
1744	#endif
1745	if (infoN->parity == 3) {
1746	/* This node can be reached through paths of different parity.
1747	** It is not safe to replace it, because remapping will give
1748	** an incorrect result, while replacement by 0 may cause node
1749	** splitting. */
1750	cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1751	continue;
1752	}
1753	T = cuddT(node);
1754	E = cuddE(node);
1755	shared = NULL;
1756	impactP = item->impactP;
1757	impactN = item->impactN;
1758	if (Cudd_bddLeq(dd,T,E)) {
1759	/* Here we know that E is regular. */
1760	#ifdef DD_DEBUG
1761	assert(!Cudd_IsComplement(E));
1762	#endif
1763	(void) st_lookup(info->table, T, &infoT);
1764	(void) st_lookup(info->table, E, &infoE);
1765	if (infoN->parity == 1) {
1766	impact = impactP;
1767	minterms = infoE->mintermsP/2.0 - infoT->mintermsP/2.0;
1768	if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
1769	savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
1770	if (savings == 1) {
1771	cuddLevelQueueQuit(queue);
1772	cuddLevelQueueQuit(localQueue);
1773	return(0);
1774	}
1775	} else {
1776	savings = 1;
1777	}
1778	replace = REPLACE_E;
1779	} else {
1780	#ifdef DD_DEBUG
1781	assert(infoN->parity == 2);
1782	#endif
1783	impact = impactN;
1784	minterms = infoT->mintermsN/2.0 - infoE->mintermsN/2.0;
1785	if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
1786	savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
1787	if (savings == 1) {
1788	cuddLevelQueueQuit(queue);
1789	cuddLevelQueueQuit(localQueue);
1790	return(0);
1791	}
1792	} else {
1793	savings = 1;
1794	}
1795	replace = REPLACE_T;
1796	}
1797	numOnset = impact * minterms;
1798	} else if (Cudd_bddLeq(dd,E,T)) {
1799	/* Here E may be complemented. */
1800	DdNode *Ereg = Cudd_Regular(E);
1801	(void) st_lookup(info->table, T, &infoT);
1802	(void) st_lookup(info->table, Ereg, &infoE);
1803	if (infoN->parity == 1) {
1804	impact = impactP;
1805	minterms = infoT->mintermsP/2.0 -
1806	((E == Ereg) ? infoE->mintermsP : infoE->mintermsN)/2.0;
1807	if (infoT->functionRef == 1 && !Cudd_IsConstant(T)) {
1808	savings = 1 + computeSavings(dd,T,NULL,info,localQueue);
1809	if (savings == 1) {
1810	cuddLevelQueueQuit(queue);
1811	cuddLevelQueueQuit(localQueue);
1812	return(0);
1813	}
1814	} else {
1815	savings = 1;
1816	}
1817	replace = REPLACE_T;
1818	} else {
1819	#ifdef DD_DEBUG
1820	assert(infoN->parity == 2);
1821	#endif
1822	impact = impactN;
1823	minterms = ((E == Ereg) ? infoE->mintermsN :
1824	infoE->mintermsP)/2.0 - infoT->mintermsN/2.0;
1825	if (infoE->functionRef == 1 && !Cudd_IsConstant(E)) {
1826	savings = 1 + computeSavings(dd,E,NULL,info,localQueue);
1827	if (savings == 1) {
1828	cuddLevelQueueQuit(queue);
1829	cuddLevelQueueQuit(localQueue);
1830	return(0);
1831	}
1832	} else {
1833	savings = 1;
1834	}
1835	replace = REPLACE_E;
1836	}
1837	numOnset = impact * minterms;
1838	} else {
1839	DdNode *Ereg = Cudd_Regular(E);
1840	DdNode *TT = cuddT(T);
1841	DdNode *ET = Cudd_NotCond(cuddT(Ereg), Cudd_IsComplement(E));
1842	if (T->index == Ereg->index && TT == ET) {
1843	shared = TT;
1844	replace = REPLACE_TT;
1845	} else {
1846	DdNode *TE = cuddE(T);
1847	DdNode *EE = Cudd_NotCond(cuddE(Ereg), Cudd_IsComplement(E));
1848	if (T->index == Ereg->index && TE == EE) {
1849	shared = TE;
1850	replace = REPLACE_TE;
1851	} else {
1852	replace = REPLACE_N;
1853	}
1854	}
1855	numOnset = infoN->mintermsP * impactP + infoN->mintermsN * impactN;
1856	savings = computeSavings(dd,node,shared,info,localQueue);
1857	if (shared != NULL) {
1858	NodeData *infoS;
1859	(void) st_lookup(info->table, Cudd_Regular(shared), &infoS);
1860	if (Cudd_IsComplement(shared)) {
1861	numOnset -= (infoS->mintermsN * impactP +
1862	infoS->mintermsP * impactN)/2.0;
1863	} else {
1864	numOnset -= (infoS->mintermsP * impactP +
1865	infoS->mintermsN * impactN)/2.0;
1866	}
1867	savings--;
1868	}
1869	}
1870
1871	cuddLevelQueueDequeue(queue,cuddI(dd,node->index));
1872	#if 0
1873	if (replace == REPLACE_T \|\| replace == REPLACE_E)
1874	(void) printf("node %p: impact = %g numOnset = %g savings %d\n",
1875	node, impact, numOnset, savings);
1876	else
1877	(void) printf("node %p: impact = %g/%g numOnset = %g savings %d\n",
1878	node, impactP, impactN, numOnset, savings);
1879	#endif
1880	if ((1 - numOnset / info->minterms) >
1881	quality * (1 - (double) savings / info->size)) {
1882	infoN->replace = (char) replace;
1883	info->size -= savings;
1884	info->minterms -=numOnset;
1885	#if 0
1886	(void) printf("remap(%d): new size = %d new minterms = %g\n",
1887	replace, info->size, info->minterms);
1888	#endif
1889	if (replace == REPLACE_N) {
1890	savings -= updateRefs(dd,node,NULL,info,localQueue);
1891	} else if (replace == REPLACE_T) {
1892	savings -= updateRefs(dd,node,E,info,localQueue);
1893	} else if (replace == REPLACE_E) {
1894	savings -= updateRefs(dd,node,T,info,localQueue);
1895	} else {
1896	#ifdef DD_DEBUG
1897	assert(replace == REPLACE_TT \|\| replace == REPLACE_TE);
1898	#endif
1899	savings -= updateRefs(dd,node,shared,info,localQueue) - 1;
1900	}
1901	assert(savings == 0);
1902	} else {
1903	replace = NOTHING;
1904	}
1905	if (replace == REPLACE_N) continue;
1906	if ((replace == REPLACE_E \|\| replace == NOTHING) &&
1907	!cuddIsConstant(cuddT(node))) {
1908	item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,cuddT(node),
1909	cuddI(dd,cuddT(node)->index));
1910	if (replace == REPLACE_E) {
1911	item->impactP += impactP;
1912	item->impactN += impactN;
1913	} else {
1914	item->impactP += impactP/2.0;
1915	item->impactN += impactN/2.0;
1916	}
1917	}
1918	if ((replace == REPLACE_T \|\| replace == NOTHING) &&
1919	!Cudd_IsConstant(cuddE(node))) {
1920	item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(cuddE(node)),
1921	cuddI(dd,Cudd_Regular(cuddE(node))->index));
1922	if (Cudd_IsComplement(cuddE(node))) {
1923	if (replace == REPLACE_T) {
1924	item->impactP += impactN;
1925	item->impactN += impactP;
1926	} else {
1927	item->impactP += impactN/2.0;
1928	item->impactN += impactP/2.0;
1929	}
1930	} else {
1931	if (replace == REPLACE_T) {
1932	item->impactP += impactP;
1933	item->impactN += impactN;
1934	} else {
1935	item->impactP += impactP/2.0;
1936	item->impactN += impactN/2.0;
1937	}
1938	}
1939	}
1940	if ((replace == REPLACE_TT \|\| replace == REPLACE_TE) &&
1941	!Cudd_IsConstant(shared)) {
1942	item = (GlobalQueueItem *) cuddLevelQueueEnqueue(queue,Cudd_Regular(shared),
1943	cuddI(dd,Cudd_Regular(shared)->index));
1944	if (Cudd_IsComplement(shared)) {
1945	if (replace == REPLACE_T) {
1946	item->impactP += impactN;
1947	item->impactN += impactP;
1948	} else {
1949	item->impactP += impactN/2.0;
1950	item->impactN += impactP/2.0;
1951	}
1952	} else {
1953	if (replace == REPLACE_T) {
1954	item->impactP += impactP;
1955	item->impactN += impactN;
1956	} else {
1957	item->impactP += impactP/2.0;
1958	item->impactN += impactN/2.0;
1959	}
1960	}
1961	}
1962	}
1963
1964	cuddLevelQueueQuit(queue);
1965	cuddLevelQueueQuit(localQueue);
1966	return(1);
1967
1968	} /* end of BAmarkNodes */
1969
1970
1971	/Function******************************************************************
1972
1973	Synopsis [Builds the subset BDD for cuddRemapUnderApprox.]
1974
1975	Description [Builds the subset BDDfor cuddRemapUnderApprox. Based
1976	on the info table, performs remapping or replacement at selected
1977	nodes. Returns a pointer to the result if successful; NULL
1978	otherwise.]
1979
1980	SideEffects [None]
1981
1982	SeeAlso [cuddRemapUnderApprox]
1983
1984	******************************************************************************/
1985	static DdNode *
1986	RAbuildSubset(
1987	DdManager * dd /* DD manager */,
1988	DdNode * node /* current node */,
1989	ApproxInfo * info /* node info */)
1990	{
1991	DdNode Nt, Ne, N, t, e, r;
1992	NodeData *infoN;
1993
1994	if (Cudd_IsConstant(node))
1995	return(node);
1996
1997	N = Cudd_Regular(node);
1998
1999	Nt = Cudd_NotCond(cuddT(N), Cudd_IsComplement(node));
2000	Ne = Cudd_NotCond(cuddE(N), Cudd_IsComplement(node));
2001
2002	if (st_lookup(info->table, N, &infoN)) {
2003	if (N == node ) {
2004	if (infoN->resultP != NULL) {
2005	return(infoN->resultP);
2006	}
2007	} else {
2008	if (infoN->resultN != NULL) {
2009	return(infoN->resultN);
2010	}
2011	}
2012	if (infoN->replace == REPLACE_T) {
2013	r = RAbuildSubset(dd, Ne, info);
2014	return(r);
2015	} else if (infoN->replace == REPLACE_E) {
2016	r = RAbuildSubset(dd, Nt, info);
2017	return(r);
2018	} else if (infoN->replace == REPLACE_N) {
2019	return(info->zero);
2020	} else if (infoN->replace == REPLACE_TT) {
2021	DdNode *Ntt = Cudd_NotCond(cuddT(cuddT(N)),
2022	Cudd_IsComplement(node));
2023	int index = cuddT(N)->index;
2024	e = info->zero;
2025	t = RAbuildSubset(dd, Ntt, info);
2026	if (t == NULL) {
2027	return(NULL);
2028	}
2029	cuddRef(t);
2030	if (Cudd_IsComplement(t)) {
2031	t = Cudd_Not(t);
2032	e = Cudd_Not(e);
2033	r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
2034	if (r == NULL) {
2035	Cudd_RecursiveDeref(dd, t);
2036	return(NULL);
2037	}
2038	r = Cudd_Not(r);
2039	} else {
2040	r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
2041	if (r == NULL) {
2042	Cudd_RecursiveDeref(dd, t);
2043	return(NULL);
2044	}
2045	}
2046	cuddDeref(t);
2047	return(r);
2048	} else if (infoN->replace == REPLACE_TE) {
2049	DdNode *Nte = Cudd_NotCond(cuddE(cuddT(N)),
2050	Cudd_IsComplement(node));
2051	int index = cuddT(N)->index;
2052	t = info->one;
2053	e = RAbuildSubset(dd, Nte, info);
2054	if (e == NULL) {
2055	return(NULL);
2056	}
2057	cuddRef(e);
2058	e = Cudd_Not(e);
2059	r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
2060	if (r == NULL) {
2061	Cudd_RecursiveDeref(dd, e);
2062	return(NULL);
2063	}
2064	r =Cudd_Not(r);
2065	cuddDeref(e);
2066	return(r);
2067	}
2068	} else {
2069	(void) fprintf(dd->err,
2070	"Something is wrong, ought to be in info table\n");
2071	dd->errorCode = CUDD_INTERNAL_ERROR;
2072	return(NULL);
2073	}
2074
2075	t = RAbuildSubset(dd, Nt, info);
2076	if (t == NULL) {
2077	return(NULL);
2078	}
2079	cuddRef(t);
2080
2081	e = RAbuildSubset(dd, Ne, info);
2082	if (e == NULL) {
2083	Cudd_RecursiveDeref(dd,t);
2084	return(NULL);
2085	}
2086	cuddRef(e);
2087
2088	if (Cudd_IsComplement(t)) {
2089	t = Cudd_Not(t);
2090	e = Cudd_Not(e);
2091	r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
2092	if (r == NULL) {
2093	Cudd_RecursiveDeref(dd, e);
2094	Cudd_RecursiveDeref(dd, t);
2095	return(NULL);
2096	}
2097	r = Cudd_Not(r);
2098	} else {
2099	r = (t == e) ? t : cuddUniqueInter(dd, N->index, t, e);
2100	if (r == NULL) {
2101	Cudd_RecursiveDeref(dd, e);
2102	Cudd_RecursiveDeref(dd, t);
2103	return(NULL);
2104	}
2105	}
2106	cuddDeref(t);
2107	cuddDeref(e);
2108
2109	if (N == node) {
2110	infoN->resultP = r;
2111	} else {
2112	infoN->resultN = r;
2113	}
2114
2115	return(r);
2116
2117	} /* end of RAbuildSubset */
2118
2119
2120	/Function******************************************************************
2121
2122	Synopsis [Finds don't care nodes.]
2123
2124	Description [Finds don't care nodes by traversing f and b in parallel.
2125	Returns the care status of the visited f node if successful; CARE_ERROR
2126	otherwise.]
2127
2128	SideEffects [None]
2129
2130	SeeAlso [cuddBiasedUnderApprox]
2131
2132	******************************************************************************/
2133	static int
2134	BAapplyBias(
2135	DdManager *dd,
2136	DdNode *f,
2137	DdNode *b,
2138	ApproxInfo *info,
2139	DdHashTable *cache)
2140	{
2141	DdNode one, zero, *res;
2142	DdNode Ft, Fe, B, Bt, *Be;
2143	unsigned int topf, topb;
2144	NodeData *infoF;
2145	int careT, careE;
2146
2147	one = DD_ONE(dd);
2148	zero = Cudd_Not(one);
2149
2150	if (!st_lookup(info->table, f, &infoF))
2151	return(CARE_ERROR);
2152	if (f == one) return(TOTAL_CARE);
2153	if (b == zero) return(infoF->care);
2154	if (infoF->care == TOTAL_CARE) return(TOTAL_CARE);
2155
2156	if ((f->ref != 1 \|\| Cudd_Regular(b)->ref != 1) &&
2157	(res = cuddHashTableLookup2(cache,f,b)) != NULL) {
2158	if (res->ref == 0) {
2159	cache->manager->dead++;
2160	cache->manager->constants.dead++;
2161	}
2162	return(infoF->care);
2163	}
2164
2165	topf = dd->perm[f->index];
2166	B = Cudd_Regular(b);
2167	topb = cuddI(dd,B->index);
2168	if (topf <= topb) {
2169	Ft = cuddT(f); Fe = cuddE(f);
2170	} else {
2171	Ft = Fe = f;
2172	}
2173	if (topb <= topf) {
2174	/* We know that b is not constant because f is not. */
2175	Bt = cuddT(B); Be = cuddE(B);
2176	if (Cudd_IsComplement(b)) {
2177	Bt = Cudd_Not(Bt);
2178	Be = Cudd_Not(Be);
2179	}
2180	} else {
2181	Bt = Be = b;
2182	}
2183
2184	careT = BAapplyBias(dd, Ft, Bt, info, cache);
2185	if (careT == CARE_ERROR)
2186	return(CARE_ERROR);
2187	careE = BAapplyBias(dd, Cudd_Regular(Fe), Be, info, cache);
2188	if (careE == CARE_ERROR)
2189	return(CARE_ERROR);
2190	if (careT == TOTAL_CARE && careE == TOTAL_CARE) {
2191	infoF->care = TOTAL_CARE;
2192	} else {
2193	infoF->care = CARE;
2194	}
2195
2196	if (f->ref != 1 \|\| Cudd_Regular(b)->ref != 1) {
2197	ptrint fanout = (ptrint) f->ref * Cudd_Regular(b)->ref;
2198	cuddSatDec(fanout);
2199	if (!cuddHashTableInsert2(cache,f,b,one,fanout)) {
2200	return(CARE_ERROR);
2201	}
2202	}
2203	return(infoF->care);
2204
2205	} /* end of BAapplyBias */

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

Context Navigation

source: vis_dev/glu-2.3/src/cuBdd/cuddApprox.c @ 88

Download in other formats: