Context Navigation

source: vis_dev/glu-2.1/src/cuBdd/cuddAddApply.c @ 10

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

Line
1	/CFile*********************************************************************
2
3	FileName [cuddAddApply.c]
4
5	PackageName [cudd]
6
7	Synopsis [Apply functions for ADDs and their operators.]
8
9	Description [External procedures included in this module:
10	<ul>
11	<li> Cudd_addApply()
12	<li> Cudd_addMonadicApply()
13	<li> Cudd_addPlus()
14	<li> Cudd_addTimes()
15	<li> Cudd_addThreshold()
16	<li> Cudd_addSetNZ()
17	<li> Cudd_addDivide()
18	<li> Cudd_addMinus()
19	<li> Cudd_addMinimum()
20	<li> Cudd_addMaximum()
21	<li> Cudd_addOneZeroMaximum()
22	<li> Cudd_addDiff()
23	<li> Cudd_addAgreement()
24	<li> Cudd_addOr()
25	<li> Cudd_addNand()
26	<li> Cudd_addNor()
27	<li> Cudd_addXor()
28	<li> Cudd_addXnor()
29	</ul>
30	Internal procedures included in this module:
31	<ul>
32	<li> cuddAddApplyRecur()
33	<li> cuddAddMonadicApplyRecur()
34	</ul>]
35
36	Author [Fabio Somenzi]
37
38	Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
39
40	All rights reserved.
41
42	Redistribution and use in source and binary forms, with or without
43	modification, are permitted provided that the following conditions
44	are met:
45
46	Redistributions of source code must retain the above copyright
47	notice, this list of conditions and the following disclaimer.
48
49	Redistributions in binary form must reproduce the above copyright
50	notice, this list of conditions and the following disclaimer in the
51	documentation and/or other materials provided with the distribution.
52
53	Neither the name of the University of Colorado nor the names of its
54	contributors may be used to endorse or promote products derived from
55	this software without specific prior written permission.
56
57	THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
58	"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
59	LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
60	FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
61	COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
62	INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
63	BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
64	LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
65	CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
66	LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
67	ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
68	POSSIBILITY OF SUCH DAMAGE.]
69
70	******************************************************************************/
71
72	#include "util.h"
73	#include "cuddInt.h"
74
75	/---------------------------------------------------------------------------/
76	/* Constant declarations */
77	/---------------------------------------------------------------------------/
78
79
80	/---------------------------------------------------------------------------/
81	/* Stucture declarations */
82	/---------------------------------------------------------------------------/
83
84
85	/---------------------------------------------------------------------------/
86	/* Type declarations */
87	/---------------------------------------------------------------------------/
88
89
90	/---------------------------------------------------------------------------/
91	/* Variable declarations */
92	/---------------------------------------------------------------------------/
93
94	#ifndef lint
95	static char rcsid[] DD_UNUSED = "$Id: cuddAddApply.c,v 1.17 2004/08/13 18:04:45 fabio Exp $";
96	#endif
97
98
99	/---------------------------------------------------------------------------/
100	/* Macro declarations */
101	/---------------------------------------------------------------------------/
102
103
104	/AutomaticStart***********************************************************/
105
106	/---------------------------------------------------------------------------/
107	/* Static function prototypes */
108	/---------------------------------------------------------------------------/
109
110
111	/AutomaticEnd*************************************************************/
112
113
114	/---------------------------------------------------------------------------/
115	/* Definition of exported functions */
116	/---------------------------------------------------------------------------/
117
118	/Function******************************************************************
119
120	Synopsis [Applies op to the corresponding discriminants of f and g.]
121
122	Description [Applies op to the corresponding discriminants of f and g.
123	Returns a pointer to the result if succssful; NULL otherwise.]
124
125	SideEffects [None]
126
127	SeeAlso [Cudd_addMonadicApply Cudd_addPlus Cudd_addTimes
128	Cudd_addThreshold Cudd_addSetNZ Cudd_addDivide Cudd_addMinus Cudd_addMinimum
129	Cudd_addMaximum Cudd_addOneZeroMaximum Cudd_addDiff Cudd_addAgreement
130	Cudd_addOr Cudd_addNand Cudd_addNor Cudd_addXor Cudd_addXnor]
131
132	******************************************************************************/
133	DdNode *
134	Cudd_addApply(
135	DdManager * dd,
136	DD_AOP op,
137	DdNode * f,
138	DdNode * g)
139	{
140	DdNode *res;
141
142	do {
143	dd->reordered = 0;
144	res = cuddAddApplyRecur(dd,op,f,g);
145	} while (dd->reordered == 1);
146	return(res);
147
148	} /* end of Cudd_addApply */
149
150
151	/Function******************************************************************
152
153	Synopsis [Integer and floating point addition.]
154
155	Description [Integer and floating point addition. Returns NULL if not
156	a terminal case; f+g otherwise.]
157
158	SideEffects [None]
159
160	SeeAlso [Cudd_addApply]
161
162	******************************************************************************/
163	DdNode *
164	Cudd_addPlus(
165	DdManager * dd,
166	DdNode ** f,
167	DdNode ** g)
168	{
169	DdNode *res;
170	DdNode F, G;
171	CUDD_VALUE_TYPE value;
172
173	F = f; G = g;
174	if (F == DD_ZERO(dd)) return(G);
175	if (G == DD_ZERO(dd)) return(F);
176	if (cuddIsConstant(F) && cuddIsConstant(G)) {
177	value = cuddV(F)+cuddV(G);
178	res = cuddUniqueConst(dd,value);
179	return(res);
180	}
181	if (F > G) { /* swap f and g */
182	*f = G;
183	*g = F;
184	}
185	return(NULL);
186
187	} /* end of Cudd_addPlus */
188
189
190	/Function******************************************************************
191
192	Synopsis [Integer and floating point multiplication.]
193
194	Description [Integer and floating point multiplication. Returns NULL
195	if not a terminal case; f * g otherwise. This function can be used also
196	to take the AND of two 0-1 ADDs.]
197
198	SideEffects [None]
199
200	SeeAlso [Cudd_addApply]
201
202	******************************************************************************/
203	DdNode *
204	Cudd_addTimes(
205	DdManager * dd,
206	DdNode ** f,
207	DdNode ** g)
208	{
209	DdNode *res;
210	DdNode F, G;
211	CUDD_VALUE_TYPE value;
212
213	F = f; G = g;
214	if (F == DD_ZERO(dd) \|\| G == DD_ZERO(dd)) return(DD_ZERO(dd));
215	if (F == DD_ONE(dd)) return(G);
216	if (G == DD_ONE(dd)) return(F);
217	if (cuddIsConstant(F) && cuddIsConstant(G)) {
218	value = cuddV(F)*cuddV(G);
219	res = cuddUniqueConst(dd,value);
220	return(res);
221	}
222	if (F > G) { /* swap f and g */
223	*f = G;
224	*g = F;
225	}
226	return(NULL);
227
228	} /* end of Cudd_addTimes */
229
230
231	/Function******************************************************************
232
233	Synopsis [f if f>=g; 0 if f<g.]
234
235	Description [Threshold operator for Apply (f if f >=g; 0 if f<g).
236	Returns NULL if not a terminal case; f op g otherwise.]
237
238	SideEffects [None]
239
240	SeeAlso [Cudd_addApply]
241
242	******************************************************************************/
243	DdNode *
244	Cudd_addThreshold(
245	DdManager * dd,
246	DdNode ** f,
247	DdNode ** g)
248	{
249	DdNode F, G;
250
251	F = f; G = g;
252	if (F == G \|\| F == DD_PLUS_INFINITY(dd)) return(F);
253	if (cuddIsConstant(F) && cuddIsConstant(G)) {
254	if (cuddV(F) >= cuddV(G)) {
255	return(F);
256	} else {
257	return(DD_ZERO(dd));
258	}
259	}
260	return(NULL);
261
262	} /* end of Cudd_addThreshold */
263
264
265	/Function******************************************************************
266
267	Synopsis [This operator sets f to the value of g wherever g != 0.]
268
269	Description [This operator sets f to the value of g wherever g != 0.
270	Returns NULL if not a terminal case; f op g otherwise.]
271
272	SideEffects [None]
273
274	SeeAlso [Cudd_addApply]
275
276	******************************************************************************/
277	DdNode *
278	Cudd_addSetNZ(
279	DdManager * dd,
280	DdNode ** f,
281	DdNode ** g)
282	{
283	DdNode F, G;
284
285	F = f; G = g;
286	if (F == G) return(F);
287	if (F == DD_ZERO(dd)) return(G);
288	if (G == DD_ZERO(dd)) return(F);
289	if (cuddIsConstant(G)) return(G);
290	return(NULL);
291
292	} /* end of Cudd_addSetNZ */
293
294
295	/Function******************************************************************
296
297	Synopsis [Integer and floating point division.]
298
299	Description [Integer and floating point division. Returns NULL if not
300	a terminal case; f / g otherwise.]
301
302	SideEffects [None]
303
304	SeeAlso [Cudd_addApply]
305
306	******************************************************************************/
307	DdNode *
308	Cudd_addDivide(
309	DdManager * dd,
310	DdNode ** f,
311	DdNode ** g)
312	{
313	DdNode *res;
314	DdNode F, G;
315	CUDD_VALUE_TYPE value;
316
317	F = f; G = g;
318	/* We would like to use F == G -> F/G == 1, but F and G may
319	** contain zeroes. */
320	if (F == DD_ZERO(dd)) return(DD_ZERO(dd));
321	if (G == DD_ONE(dd)) return(F);
322	if (cuddIsConstant(F) && cuddIsConstant(G)) {
323	value = cuddV(F)/cuddV(G);
324	res = cuddUniqueConst(dd,value);
325	return(res);
326	}
327	return(NULL);
328
329	} /* end of Cudd_addDivide */
330
331
332	/Function******************************************************************
333
334	Synopsis [Integer and floating point subtraction.]
335
336	Description [Integer and floating point subtraction. Returns NULL if
337	not a terminal case; f - g otherwise.]
338
339	SideEffects [None]
340
341	SeeAlso [Cudd_addApply]
342
343	******************************************************************************/
344	DdNode *
345	Cudd_addMinus(
346	DdManager * dd,
347	DdNode ** f,
348	DdNode ** g)
349	{
350	DdNode *res;
351	DdNode F, G;
352	CUDD_VALUE_TYPE value;
353
354	F = f; G = g;
355	if (F == G) return(DD_ZERO(dd));
356	if (F == DD_ZERO(dd)) return(cuddAddNegateRecur(dd,G));
357	if (G == DD_ZERO(dd)) return(F);
358	if (cuddIsConstant(F) && cuddIsConstant(G)) {
359	value = cuddV(F)-cuddV(G);
360	res = cuddUniqueConst(dd,value);
361	return(res);
362	}
363	return(NULL);
364
365	} /* end of Cudd_addMinus */
366
367
368	/Function******************************************************************
369
370	Synopsis [Integer and floating point min.]
371
372	Description [Integer and floating point min for Cudd_addApply.
373	Returns NULL if not a terminal case; min(f,g) otherwise.]
374
375	SideEffects [None]
376
377	SeeAlso [Cudd_addApply]
378
379	******************************************************************************/
380	DdNode *
381	Cudd_addMinimum(
382	DdManager * dd,
383	DdNode ** f,
384	DdNode ** g)
385	{
386	DdNode F, G;
387
388	F = f; G = g;
389	if (F == DD_PLUS_INFINITY(dd)) return(G);
390	if (G == DD_PLUS_INFINITY(dd)) return(F);
391	if (F == G) return(F);
392	#if 0
393	/* These special cases probably do not pay off. */
394	if (F == DD_MINUS_INFINITY(dd)) return(F);
395	if (G == DD_MINUS_INFINITY(dd)) return(G);
396	#endif
397	if (cuddIsConstant(F) && cuddIsConstant(G)) {
398	if (cuddV(F) <= cuddV(G)) {
399	return(F);
400	} else {
401	return(G);
402	}
403	}
404	if (F > G) { /* swap f and g */
405	*f = G;
406	*g = F;
407	}
408	return(NULL);
409
410	} /* end of Cudd_addMinimum */
411
412
413	/Function******************************************************************
414
415	Synopsis [Integer and floating point max.]
416
417	Description [Integer and floating point max for Cudd_addApply.
418	Returns NULL if not a terminal case; max(f,g) otherwise.]
419
420	SideEffects [None]
421
422	SeeAlso [Cudd_addApply]
423
424	******************************************************************************/
425	DdNode *
426	Cudd_addMaximum(
427	DdManager * dd,
428	DdNode ** f,
429	DdNode ** g)
430	{
431	DdNode F, G;
432
433	F = f; G = g;
434	if (F == G) return(F);
435	if (F == DD_MINUS_INFINITY(dd)) return(G);
436	if (G == DD_MINUS_INFINITY(dd)) return(F);
437	#if 0
438	/* These special cases probably do not pay off. */
439	if (F == DD_PLUS_INFINITY(dd)) return(F);
440	if (G == DD_PLUS_INFINITY(dd)) return(G);
441	#endif
442	if (cuddIsConstant(F) && cuddIsConstant(G)) {
443	if (cuddV(F) >= cuddV(G)) {
444	return(F);
445	} else {
446	return(G);
447	}
448	}
449	if (F > G) { /* swap f and g */
450	*f = G;
451	*g = F;
452	}
453	return(NULL);
454
455	} /* end of Cudd_addMaximum */
456
457
458	/Function******************************************************************
459
460	Synopsis [Returns 1 if f > g and 0 otherwise.]
461
462	Description [Returns 1 if f > g and 0 otherwise. Used in
463	conjunction with Cudd_addApply. Returns NULL if not a terminal
464	case.]
465
466	SideEffects [None]
467
468	SeeAlso [Cudd_addApply]
469
470	******************************************************************************/
471	DdNode *
472	Cudd_addOneZeroMaximum(
473	DdManager * dd,
474	DdNode ** f,
475	DdNode ** g)
476	{
477
478	if (f == g) return(DD_ZERO(dd));
479	if (*g == DD_PLUS_INFINITY(dd))
480	return DD_ZERO(dd);
481	if (cuddIsConstant(f) && cuddIsConstant(g)) {
482	if (cuddV(f) > cuddV(g)) {
483	return(DD_ONE(dd));
484	} else {
485	return(DD_ZERO(dd));
486	}
487	}
488
489	return(NULL);
490
491	} /* end of Cudd_addOneZeroMaximum */
492
493
494	/Function******************************************************************
495
496	Synopsis [Returns plusinfinity if f=g; returns min(f,g) if f!=g.]
497
498	Description [Returns NULL if not a terminal case; f op g otherwise,
499	where f op g is plusinfinity if f=g; min(f,g) if f!=g.]
500
501	SideEffects [None]
502
503	SeeAlso [Cudd_addApply]
504
505	******************************************************************************/
506	DdNode *
507	Cudd_addDiff(
508	DdManager * dd,
509	DdNode ** f,
510	DdNode ** g)
511	{
512	DdNode F, G;
513
514	F = f; G = g;
515	if (F == G) return(DD_PLUS_INFINITY(dd));
516	if (F == DD_PLUS_INFINITY(dd)) return(G);
517	if (G == DD_PLUS_INFINITY(dd)) return(F);
518	if (cuddIsConstant(F) && cuddIsConstant(G)) {
519	if (cuddV(F) != cuddV(G)) {
520	if (cuddV(F) < cuddV(G)) {
521	return(F);
522	} else {
523	return(G);
524	}
525	} else {
526	return(DD_PLUS_INFINITY(dd));
527	}
528	}
529	return(NULL);
530
531	} /* end of Cudd_addDiff */
532
533
534	/Function******************************************************************
535
536	Synopsis [f if f==g; background if f!=g.]
537
538	Description [Returns NULL if not a terminal case; f op g otherwise,
539	where f op g is f if f==g; background if f!=g.]
540
541	SideEffects [None]
542
543	SeeAlso [Cudd_addApply]
544
545	******************************************************************************/
546	DdNode *
547	Cudd_addAgreement(
548	DdManager * dd,
549	DdNode ** f,
550	DdNode ** g)
551	{
552	DdNode F, G;
553
554	F = f; G = g;
555	if (F == G) return(F);
556	if (F == dd->background) return(F);
557	if (G == dd->background) return(G);
558	if (cuddIsConstant(F) && cuddIsConstant(G)) return(dd->background);
559	return(NULL);
560
561	} /* end of Cudd_addAgreement */
562
563
564	/Function******************************************************************
565
566	Synopsis [Disjunction of two 0-1 ADDs.]
567
568	Description [Disjunction of two 0-1 ADDs. Returns NULL
569	if not a terminal case; f OR g otherwise.]
570
571	SideEffects [None]
572
573	SeeAlso [Cudd_addApply]
574
575	******************************************************************************/
576	DdNode *
577	Cudd_addOr(
578	DdManager * dd,
579	DdNode ** f,
580	DdNode ** g)
581	{
582	DdNode F, G;
583
584	F = f; G = g;
585	if (F == DD_ONE(dd) \|\| G == DD_ONE(dd)) return(DD_ONE(dd));
586	if (cuddIsConstant(F)) return(G);
587	if (cuddIsConstant(G)) return(F);
588	if (F == G) return(F);
589	if (F > G) { /* swap f and g */
590	*f = G;
591	*g = F;
592	}
593	return(NULL);
594
595	} /* end of Cudd_addOr */
596
597
598	/Function******************************************************************
599
600	Synopsis [NAND of two 0-1 ADDs.]
601
602	Description [NAND of two 0-1 ADDs. Returns NULL
603	if not a terminal case; f NAND g otherwise.]
604
605	SideEffects [None]
606
607	SeeAlso [Cudd_addApply]
608
609	******************************************************************************/
610	DdNode *
611	Cudd_addNand(
612	DdManager * dd,
613	DdNode ** f,
614	DdNode ** g)
615	{
616	DdNode F, G;
617
618	F = f; G = g;
619	if (F == DD_ZERO(dd) \|\| G == DD_ZERO(dd)) return(DD_ONE(dd));
620	if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd));
621	if (F > G) { /* swap f and g */
622	*f = G;
623	*g = F;
624	}
625	return(NULL);
626
627	} /* end of Cudd_addNand */
628
629
630	/Function******************************************************************
631
632	Synopsis [NOR of two 0-1 ADDs.]
633
634	Description [NOR of two 0-1 ADDs. Returns NULL
635	if not a terminal case; f NOR g otherwise.]
636
637	SideEffects [None]
638
639	SeeAlso [Cudd_addApply]
640
641	******************************************************************************/
642	DdNode *
643	Cudd_addNor(
644	DdManager * dd,
645	DdNode ** f,
646	DdNode ** g)
647	{
648	DdNode F, G;
649
650	F = f; G = g;
651	if (F == DD_ONE(dd) \|\| G == DD_ONE(dd)) return(DD_ZERO(dd));
652	if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ONE(dd));
653	if (F > G) { /* swap f and g */
654	*f = G;
655	*g = F;
656	}
657	return(NULL);
658
659	} /* end of Cudd_addNor */
660
661
662	/Function******************************************************************
663
664	Synopsis [XOR of two 0-1 ADDs.]
665
666	Description [XOR of two 0-1 ADDs. Returns NULL
667	if not a terminal case; f XOR g otherwise.]
668
669	SideEffects [None]
670
671	SeeAlso [Cudd_addApply]
672
673	******************************************************************************/
674	DdNode *
675	Cudd_addXor(
676	DdManager * dd,
677	DdNode ** f,
678	DdNode ** g)
679	{
680	DdNode F, G;
681
682	F = f; G = g;
683	if (F == G) return(DD_ZERO(dd));
684	if (F == DD_ONE(dd) && G == DD_ZERO(dd)) return(DD_ONE(dd));
685	if (G == DD_ONE(dd) && F == DD_ZERO(dd)) return(DD_ONE(dd));
686	if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd));
687	if (F > G) { /* swap f and g */
688	*f = G;
689	*g = F;
690	}
691	return(NULL);
692
693	} /* end of Cudd_addXor */
694
695
696	/Function******************************************************************
697
698	Synopsis [XNOR of two 0-1 ADDs.]
699
700	Description [XNOR of two 0-1 ADDs. Returns NULL
701	if not a terminal case; f XNOR g otherwise.]
702
703	SideEffects [None]
704
705	SeeAlso [Cudd_addApply]
706
707	******************************************************************************/
708	DdNode *
709	Cudd_addXnor(
710	DdManager * dd,
711	DdNode ** f,
712	DdNode ** g)
713	{
714	DdNode F, G;
715
716	F = f; G = g;
717	if (F == G) return(DD_ONE(dd));
718	if (F == DD_ONE(dd) && G == DD_ONE(dd)) return(DD_ONE(dd));
719	if (G == DD_ZERO(dd) && F == DD_ZERO(dd)) return(DD_ONE(dd));
720	if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd));
721	if (F > G) { /* swap f and g */
722	*f = G;
723	*g = F;
724	}
725	return(NULL);
726
727	} /* end of Cudd_addXnor */
728
729
730	/Function******************************************************************
731
732	Synopsis [Applies op to the discriminants of f.]
733
734	Description [Applies op to the discriminants of f.
735	Returns a pointer to the result if succssful; NULL otherwise.]
736
737	SideEffects [None]
738
739	SeeAlso [Cudd_addApply Cudd_addLog]
740
741	******************************************************************************/
742	DdNode *
743	Cudd_addMonadicApply(
744	DdManager * dd,
745	DD_MAOP op,
746	DdNode * f)
747	{
748	DdNode *res;
749
750	do {
751	dd->reordered = 0;
752	res = cuddAddMonadicApplyRecur(dd,op,f);
753	} while (dd->reordered == 1);
754	return(res);
755
756	} /* end of Cudd_addMonadicApply */
757
758
759	/Function******************************************************************
760
761	Synopsis [Natural logarithm of an ADD.]
762
763	Description [Natural logarithm of an ADDs. Returns NULL
764	if not a terminal case; log(f) otherwise. The discriminants of f must
765	be positive double's.]
766
767	SideEffects [None]
768
769	SeeAlso [Cudd_addMonadicApply]
770
771	******************************************************************************/
772	DdNode *
773	Cudd_addLog(
774	DdManager * dd,
775	DdNode * f)
776	{
777	if (cuddIsConstant(f)) {
778	CUDD_VALUE_TYPE value = log(cuddV(f));
779	DdNode *res = cuddUniqueConst(dd,value);
780	return(res);
781	}
782	return(NULL);
783
784	} /* end of Cudd_addLog */
785
786
787	/---------------------------------------------------------------------------/
788	/* Definition of internal functions */
789	/---------------------------------------------------------------------------/
790
791
792	/Function******************************************************************
793
794	Synopsis [Performs the recursive step of Cudd_addApply.]
795
796	Description [Performs the recursive step of Cudd_addApply. Returns a
797	pointer to the result if successful; NULL otherwise.]
798
799	SideEffects [None]
800
801	SeeAlso [cuddAddMonadicApplyRecur]
802
803	******************************************************************************/
804	DdNode *
805	cuddAddApplyRecur(
806	DdManager * dd,
807	DD_AOP op,
808	DdNode * f,
809	DdNode * g)
810	{
811	DdNode *res,
812	fv, fvn, gv, gvn,
813	T, E;
814	unsigned int ford, gord;
815	unsigned int index;
816	DD_CTFP cacheOp;
817
818	/* Check terminal cases. Op may swap f and g to increase the
819	* cache hit rate.
820	*/
821	statLine(dd);
822	res = (*op)(dd,&f,&g);
823	if (res != NULL) return(res);
824
825	/* Check cache. */
826	cacheOp = (DD_CTFP) op;
827	res = cuddCacheLookup2(dd,cacheOp,f,g);
828	if (res != NULL) return(res);
829
830	/* Recursive step. */
831	ford = cuddI(dd,f->index);
832	gord = cuddI(dd,g->index);
833	if (ford <= gord) {
834	index = f->index;
835	fv = cuddT(f);
836	fvn = cuddE(f);
837	} else {
838	index = g->index;
839	fv = fvn = f;
840	}
841	if (gord <= ford) {
842	gv = cuddT(g);
843	gvn = cuddE(g);
844	} else {
845	gv = gvn = g;
846	}
847
848	T = cuddAddApplyRecur(dd,op,fv,gv);
849	if (T == NULL) return(NULL);
850	cuddRef(T);
851
852	E = cuddAddApplyRecur(dd,op,fvn,gvn);
853	if (E == NULL) {
854	Cudd_RecursiveDeref(dd,T);
855	return(NULL);
856	}
857	cuddRef(E);
858
859	res = (T == E) ? T : cuddUniqueInter(dd,(int)index,T,E);
860	if (res == NULL) {
861	Cudd_RecursiveDeref(dd, T);
862	Cudd_RecursiveDeref(dd, E);
863	return(NULL);
864	}
865	cuddDeref(T);
866	cuddDeref(E);
867
868	/* Store result. */
869	cuddCacheInsert2(dd,cacheOp,f,g,res);
870
871	return(res);
872
873	} /* end of cuddAddApplyRecur */
874
875
876	/Function******************************************************************
877
878	Synopsis [Performs the recursive step of Cudd_addMonadicApply.]
879
880	Description [Performs the recursive step of Cudd_addMonadicApply. Returns a
881	pointer to the result if successful; NULL otherwise.]
882
883	SideEffects [None]
884
885	SeeAlso [cuddAddApplyRecur]
886
887	******************************************************************************/
888	DdNode *
889	cuddAddMonadicApplyRecur(
890	DdManager * dd,
891	DD_MAOP op,
892	DdNode * f)
893	{
894	DdNode res, ft, fe, T, *E;
895	unsigned int index;
896
897	/* Check terminal cases. */
898	statLine(dd);
899	res = (*op)(dd,f);
900	if (res != NULL) return(res);
901
902	/* Check cache. */
903	res = cuddCacheLookup1(dd,op,f);
904	if (res != NULL) return(res);
905
906	/* Recursive step. */
907	index = f->index;
908	ft = cuddT(f);
909	fe = cuddE(f);
910
911	T = cuddAddMonadicApplyRecur(dd,op,ft);
912	if (T == NULL) return(NULL);
913	cuddRef(T);
914
915	E = cuddAddMonadicApplyRecur(dd,op,fe);
916	if (E == NULL) {
917	Cudd_RecursiveDeref(dd,T);
918	return(NULL);
919	}
920	cuddRef(E);
921
922	res = (T == E) ? T : cuddUniqueInter(dd,(int)index,T,E);
923	if (res == NULL) {
924	Cudd_RecursiveDeref(dd, T);
925	Cudd_RecursiveDeref(dd, E);
926	return(NULL);
927	}
928	cuddDeref(T);
929	cuddDeref(E);
930
931	/* Store result. */
932	cuddCacheInsert1(dd,op,f,res);
933
934	return(res);
935
936	} /* end of cuddAddMonadicApplyRecur */
937
938
939	/---------------------------------------------------------------------------/
940	/* Definition of static functions */
941	/---------------------------------------------------------------------------/
942

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

Download in other formats: